The Context::forall and Context::exists functions were not structuring the S-expressions for variables correctly. This PR fixes that, and adds an example that uses quantifiers as a means of testing.
To demonstrate the problem, run the new example without the changes to src/context.rs. The example uses the following forall quantifier:
ctx.assert(
// For any pair of sets,
ctx.forall(
[("s1", ctx.atom("MySet")), ("s2", ctx.atom("MySet"))],
// One of the following is true:
ctx.or(
...
)
)
)
The problem is that the variable declarations (s1 MySet) and (s2 MySet) are not grouped together as a sub-list. The forall expression is supposed to have the shape:
(forall ((var1 Sort1) ... (varN SortN)) (body))
The same problem occurs for the exists function: the variable declaration (x MyElement) in the above trace should be a singleton list ((x MyElement)).
With the changes to src/context.rs, the example is fixed:
The
Context::forall
andContext::exists
functions were not structuring the S-expressions for variables correctly. This PR fixes that, and adds an example that uses quantifiers as a means of testing.To demonstrate the problem, run the new example without the changes to
src/context.rs
. The example uses the followingforall
quantifier:which produces the following trace:
The problem is that the variable declarations
(s1 MySet)
and(s2 MySet)
are not grouped together as a sub-list. The forall expression is supposed to have the shape:The same problem occurs for the
exists
function: the variable declaration(x MyElement)
in the above trace should be a singleton list((x MyElement))
.With the changes to
src/context.rs
, the example is fixed:Thanks for writing this library! Aside from this bug, I've found it easy to get up and running with it.