From f3a04734d9cd685f5921c368f648899246b094fc Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 21 Oct 2014 12:48:49 -0700
Subject: [PATCH] add pretty printing to SMT2 from solver, add get_id to Ast
 objects

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/python/z3.py | 39 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 39 insertions(+)

diff --git a/src/api/python/z3.py b/src/api/python/z3.py
index 82ba85472..470280630 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3.py
@@ -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.