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
v
is found so thatv(T) = t
or 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 ...)
X
and 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? – Sprouse