CODEWITHSUNDEEP
z3solversmt
user1367401
user1367401

Reputation: 1050

Symbolic variables in z3

Is there a way to make z3 solver emit "symbolic" solutions? For example, for equation:

1+x=c

the solution is x=c-1, but z3 always emits a specific model, like [c = 0, x = -1]. How to "define" c as a symbolic variable?

Upvotes: 2

Views: 725

Answers (1)

Leonardo de Moura
Leonardo de Moura

Reputation: 21475

Unfortunately, Z3 does not expose this kind of functionality. Although we use solvers internally, they are not exposed in the API. In future versions, we want to expose internal components such as: solver, Grobner bases procedures, etc. In the current version, we have a tactic called solve-eqs (see http://rise4fun.com/Z3Py/tutorial/strategies). It eliminates variables using a generalization of Gaussian elimination. However, this is a preprocessing step, and you do not have any control over which variables are eliminated.

Upvotes: 3

Related Questions