3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00

add pretty printing to SMT2 from solver, add get_id to Ast objects

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-10-21 12:48:49 -07:00
parent 3ecffaa1e5
commit f3a04734d9

View file

@ -297,6 +297,11 @@ class AstRef(Z3PPObject):
"""Return a pointer to the corresponding C Z3_ast object."""
return self.ast
def get_id(self):
"""Return unique identifier for object. It can be used for hash-tables and maps."""
return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
def ctx_ref(self):
"""Return a reference to the C context where this AST node is stored."""
return self.ctx.ref()
@ -447,6 +452,10 @@ class SortRef(AstRef):
def as_ast(self):
return Z3_sort_to_ast(self.ctx_ref(), self.ast)
def get_id(self):
return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
def kind(self):
"""Return the Z3 internal kind of a sort. This method can be used to test if `self` is one of the Z3 builtin sorts.
@ -585,6 +594,9 @@ class FuncDeclRef(AstRef):
def as_ast(self):
return Z3_func_decl_to_ast(self.ctx_ref(), self.ast)
def get_id(self):
return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
def as_func_decl(self):
return self.ast
@ -730,6 +742,9 @@ class ExprRef(AstRef):
def as_ast(self):
return self.ast
def get_id(self):
return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
def sort(self):
"""Return the sort of expression `self`.
@ -1524,6 +1539,9 @@ class PatternRef(ExprRef):
def as_ast(self):
return Z3_pattern_to_ast(self.ctx_ref(), self.ast)
def get_id(self):
return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
def is_pattern(a):
"""Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation.
@ -1586,6 +1604,9 @@ class QuantifierRef(BoolRef):
def as_ast(self):
return self.ast
def get_id(self):
return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
def sort(self):
"""Return the Boolean sort."""
return BoolSort(self.ctx)
@ -6011,6 +6032,24 @@ class Solver(Z3PPObject):
"""
return Z3_solver_to_string(self.ctx.ref(), self.solver)
def to_smt2(self):
"""return SMTLIB2 formatted benchmark for solver's assertions"""
es = self.assertions()
sz = len(es)
sz1 = sz
if sz1 > 0:
sz1 -= 1
v = (Ast * sz1)()
for i in range(sz1):
v[i] = es[i].as_ast()
if sz > 0:
e = es[sz1].as_ast()
else:
e = BoolVal(True, self.ctx).as_ast()
return Z3_benchmark_to_smtlib_string(self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e)
def SolverFor(logic, ctx=None):
"""Create a solver customized for the given logic.