I want to parse a logical expression using DCG in Prolog.
The logical terms are represented as lists e.g. ['x','&&','y'] for x ∧ y the result should be the parse tree and(X,Y) (were X and Y are unassigned Prolog variables).
I implemented it and everything works as expected but I have one problem:
I can't figure out how to parse the variable 'x' and 'y' to get real Prolog variables X and Y for the later assignment of truth values.
I tried the following rule variations:
v(X) --> [X].:
This doesn't work of course, it only returnsand('x','y').
But can I maybe uniformly replace the logical variables in this term with Prolog variables? I know of the predicateterm_to_atom(which is proposed as a solution for a similar problem) but I don't think it can be used here to achieve the desired result.v(Y) --> [X], {nonvar(Y)}.:
This does return an unbound variable but of course a new one every time even if the logical variable ('x','y',...) was already in the term so['X','&&','X']gets evaluated toand(X,Y)which is not the desired result, either.
Is there any elegant or idiomatic solution to this problem?
Many thanks in advance!
EDIT:
The background to this question is that I'm trying to implement the DPLL-algorithm in Prolog. I thought it would by clever to directly parse the logical term to a Prolog-term to make easy use of the Prolog backtracking facility:
- Input: some logical term, e.g T =
[x,'&&',y] - Term after parsing:
[G_123,'&&',G_456](now featuring "real" Prolog variables) - Assign a value from { boolean(t), boolean(f) } to the first unbound variable in T.
- simplify the term.
- ... repeat or backtrack until a assignment
vis found so thatv(T) = tor the search space is depleted.
I'm pretty new to Prolog and honestly couldn't figure out a better approach. I'm very interested in better alternatives! (So I'm kinda half-shure that this is what I want ;-) and thank you very much for your support so far ...)
Xand theY? Do you insist on having an'x'map to anX? Or is it simply that you want to have all your'x'refer to the same variable in the final parse tree? - user1812457