Repository: pysmt/pysmt
Pull request #703 (2021-11-26 09:24:01)

Added printing of annotations to smt lib printers
Added support of SMT-LIB annotations printing



Patch:
diff --git a/.mailmap b/.mailmap
index 688b159..8666395 100644
--- a/.mailmap
+++ b/.mailmap
@@ -4,6 +4,7 @@
 Ahmed Irfan <ahmed.irfan@alumni.unitn.it>  Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
 Ahmed Irfan <ahmed.irfan@alumni.unitn.it>  Ahmed Irfan <ahmed.irfan@alumni.unitn.it>
 Ahmed Irfan <ahmed.irfan@alumni.unitn.it>  Ahmed Irfan <irfan@fbk.eu>
+Alessandro Girardi <girardiale00@gmail.com> rayz1065 <rayz1065@gmail.com>
 Andrea Micheli <micheli.andrea@gmail.com>  mikand <micheli.andrea@gmail.com>
 Andrea Micheli <micheli.andrea@gmail.com>  MikAnd <micheli.andrea@gmail.com>
 Ankit raj ojha <anoj123anru@gmail.com>  ankit01ojha <anoj123anru@gmail.com>
diff --git a/CONTRIBUTORS b/CONTRIBUTORS
index 57baaa2..f411e7b 100644
--- a/CONTRIBUTORS
+++ b/CONTRIBUTORS
@@ -1,6 +1,7 @@
 Ahmed Irfan <ahmed.irfan@alumni.unitn.it>
 Alastair Reid <alastair.d.reid@gmail.com>
 Alberto Griggio <griggio@fbk.eu>
+Alessandro Girardi <girardiale00@gmail.com>
 Alexey Ignatiev <aignatiev@ciencias.ulisboa.pt>
 Anant Prasad <Anantprsd5@gmail.com>
 Andrea Micheli <micheli.andrea@gmail.com>
diff --git a/pysmt/smtlib/printers.py b/pysmt/smtlib/printers.py
index 126c959..c87c776 100644
--- a/pysmt/smtlib/printers.py
+++ b/pysmt/smtlib/printers.py
@@ -23,14 +23,46 @@ from pysmt.environment import get_env
 from pysmt.walkers import TreeWalker, DagWalker, handles
 from pysmt.utils import quote
 
+def write_annotations(f):
+    def resf(self, formula, *args, **kwargs):
+        annots = self.annotations
+        if annots is not None and formula in annots:
+            self.write("(! ")
+        res = f(self, formula, *args, **kwargs)
+        # all of the items must be yielded to avoid printing out of order
+        if res is not None:
+            for item in res:
+                yield item
+        if annots is not None and formula in annots:
+            for key, values in annots[formula].items():
+                self.write(f" :{key}")
+                for value in values:
+                    self.write(f" {value}")
+            self.write(')')
+    return resf
+
+def write_annotations_dag(f):
+    def resf(self, formula, *args, **kwargs):
+        annots = self.annotations
+        res = f(self, formula, *args, **kwargs)
+        if annots is None or formula not in annots:
+            return res
+        items = list()
+        for key, values in annots[formula].items():
+            items.append(f' :{key}')
+            items.extend(f' {v}' for v in values)
+        kv = ''.join(items)
+        return f'(! {res}{kv})'
+    return resf
 
 class SmtPrinter(TreeWalker):
 
-    def __init__(self, stream):
+    def __init__(self, stream, annotations=None):
         TreeWalker.__init__(self)
         self.stream = stream
         self.write = self.stream.write
         self.mgr = get_env().formula_manager
+        self.annotations = annotations
 
     def printer(self, f):
         self.walk(f)
@@ -39,6 +71,7 @@ class SmtPrinter(TreeWalker):
         """This is a complete printer"""
         raise NotImplementedError
 
+    @write_annotations
     def walk_nary(self, formula, operator):
         self.write("(%s" % operator)
         for s in formula.args():
@@ -86,18 +119,21 @@ class SmtPrinter(TreeWalker):
     def walk_array_select(self, formula): return self.walk_nary(formula, "select")
     def walk_array_store(self, formula): return self.walk_nary(formula, "store")
 
+    @write_annotations
     def walk_symbol(self, formula):
         self.write(quote(formula.symbol_name()))
 
     def walk_function(self, formula):
         return self.walk_nary(formula, quote(formula.function_name().symbol_name()))
 
+    @write_annotations
     def walk_int_constant(self, formula):
         if formula.constant_value() < 0:
             self.write("(- " + str(-formula.constant_value()) + ")")
         else:
             self.write(str(formula.constant_value()))
 
+    @write_annotations
     def walk_real_constant(self, formula):
         if formula.constant_value() < 0:
             template = "(- %s)"
@@ -113,15 +149,18 @@ class SmtPrinter(TreeWalker):
 
         self.write(res)
 
+    @write_annotations
     def walk_bool_constant(self, formula):
         if formula.constant_value():
             self.write("true")
         else:
             self.write("false")
 
+    @write_annotations
     def walk_bv_constant(self, formula):
         self.write("#b" + formula.bv_bin_str())
 
+    @write_annotations
     def walk_str_constant(self, formula):
         self.write('"' + formula.constant_value().replace('"', '""') + '"')
 
@@ -131,6 +170,7 @@ class SmtPrinter(TreeWalker):
     def walk_exists(self, formula):
         return self._walk_quantifier("exists", formula)
 
+    @write_annotations
     def _walk_quantifier(self, operator, formula):
         assert len(formula.quantifier_vars()) > 0
         self.write("(%s (" % operator)
@@ -144,6 +184,7 @@ class SmtPrinter(TreeWalker):
         yield formula.arg(0)
         self.write(")")
 
+    @write_annotations
     def walk_bv_extract(self, formula):
         self.write("((_ extract %d %d) " % (formula.bv_extract_end(),
                                             formula.bv_extract_start()))
@@ -151,6 +192,7 @@ class SmtPrinter(TreeWalker):
         self.write(")")
 
     @handles(op.BV_ROR, op.BV_ROL)
+    @write_annotations
     def walk_bv_rotate(self, formula):
         if formula.is_bv_ror():
             rotate_type = "rotate_right"
@@ -163,6 +205,7 @@ class SmtPrinter(TreeWalker):
         self.write(")")
 
     @handles(op.BV_ZEXT, op.BV_SEXT)
+    @write_annotations
     def walk_bv_extend(self, formula):
         if formula.is_bv_zext():
             extend_type = "zero_extend"
@@ -174,11 +217,13 @@ class SmtPrinter(TreeWalker):
         yield formula.arg(0)
         self.write(")")
 
+    @write_annotations
     def walk_str_length(self, formula):
         self.write("(str.len ")
         self.walk(formula.arg(0))
         self.write(")")
 
+    @write_annotations
     def walk_str_charat(self,formula, **kwargs):
         self.write("( str.at " )
         self.walk(formula.arg(0))
@@ -186,6 +231,7 @@ class SmtPrinter(TreeWalker):
         self.walk(formula.arg(1))
         self.write(")")
 
+    @write_annotations
     def walk_str_concat(self,formula, **kwargs):
         self.write("( str.++ " )
         for arg in formula.args():
@@ -193,6 +239,7 @@ class SmtPrinter(TreeWalker):
             self.write(" ")
         self.write(")")
 
+    @write_annotations
     def walk_str_contains(self,formula, **kwargs):
         self.write("( str.contains " )
         self.walk(formula.arg(0))
@@ -200,6 +247,7 @@ class SmtPrinter(TreeWalker):
         self.walk(formula.arg(1))
         self.write(")")
 
+    @write_annotations
     def walk_str_indexof(self,formula, **kwargs):
         self.write("( str.indexof " )
         self.walk(formula.arg(0))
@@ -209,6 +257,7 @@ class SmtPrinter(TreeWalker):
         self.walk(formula.arg(2))
         self.write(")")
 
+    @write_annotations
     def walk_str_replace(self,formula, **kwargs):
         self.write("( str.replace " )
         self.walk(formula.arg(0))
@@ -218,6 +267,7 @@ class SmtPrinter(TreeWalker):
         self.walk(formula.arg(2))
         self.write(")")
 
+    @write_annotations
     def walk_str_substr(self,formula, **kwargs):
         self.write("( str.substr " )
         self.walk(formula.arg(0))
@@ -227,6 +277,7 @@ class SmtPrinter(TreeWalker):
         self.walk(formula.arg(2))
         self.write(")")
 
+    @write_annotations
     def walk_str_prefixof(self,formula, **kwargs):
         self.write("( str.prefixof " )
         self.walk(formula.arg(0))
@@ -234,6 +285,7 @@ class SmtPrinter(TreeWalker):
         self.walk(formula.arg(1))
         self.write(")")
 
+    @write_annotations
     def walk_str_suffixof(self,formula, **kwargs):
         self.write("( str.suffixof " )
         self.walk(formula.arg(0))
@@ -241,16 +293,19 @@ class SmtPrinter(TreeWalker):
         self.walk(formula.arg(1))
         self.write(")")
 
+    @write_annotations
     def walk_str_to_int(self,formula, **kwargs):
         self.write("( str.to.int " )
         self.walk(formula.arg(0))
         self.write(")")
 
+    @write_annotations
     def walk_int_to_str(self,formula, **kwargs):
         self.write("( int.to.str " )
         self.walk(formula.arg(0))
         self.write(")")
 
+    @write_annotations
     def walk_array_value(self, formula):
         assign = formula.array_value_assigned_values_map()
         for _ in range(len(assign)):
@@ -270,7 +325,7 @@ class SmtPrinter(TreeWalker):
 
 class SmtDagPrinter(DagWalker):
 
-    def __init__(self, stream, template=".def_%d"):
+    def __init__(self, stream, template=".def_%d", annotations=None):
         DagWalker.__init__(self, invalidate_memoization=True)
         self.stream = stream
         self.write = self.stream.write
@@ -279,6 +334,7 @@ class SmtDagPrinter(DagWalker):
         self.template = template
         self.names = None
         self.mgr = get_env().formula_manager
+        self.annotations = annotations
 
     def _push_with_children_to_stack(self, formula, **kwargs):
         """Add children to the stack."""
@@ -312,6 +368,7 @@ class SmtDagPrinter(DagWalker):
         self.name_seed += 1
         return res
 
+    @write_annotations_dag
     def walk_nary(self, formula, args, operator):
         assert formula is not None
         sym = self._new_symbol()
@@ -440,18 +497,21 @@ class SmtDagPrinter(DagWalker):
     def walk_array_store(self, formula, args):
         return self.walk_nary(formula, args, "store")
 
+    @write_annotations_dag
     def walk_symbol(self, formula, **kwargs):
         return quote(formula.symbol_name())
 
     def walk_function(self, formula, args, **kwargs):
         return self.walk_nary(formula, args, quote(formula.function_name().symbol_name()))
 
+    @write_annotations_dag
     def walk_int_constant(self, formula, **kwargs):
         if formula.constant_value() < 0:
             return "(- " + str(-formula.constant_value()) + ")"
         else:
             return str(formula.constant_value())
 
+    @write_annotations_dag
     def walk_real_constant(self, formula, **kwargs):
         if formula.constant_value() < 0:
             template = "(- %s)"
@@ -465,6 +525,7 @@ class SmtDagPrinter(DagWalker):
         else:
             return template % (str(n) + ".0")
 
+    @write_annotations_dag
     def walk_bv_constant(self, formula, **kwargs):
         short_res = str(bin(formula.constant_value()))[2:]
         if formula.constant_value() >= 0:
@@ -475,12 +536,14 @@ class SmtDagPrinter(DagWalker):
         return "#b" + res
 
 
+    @write_annotations_dag
     def walk_bool_constant(self, formula, **kwargs):
         if formula.constant_value():
             return "true"
         else:
             return "false"
 
+    @write_annotations_dag
     def walk_str_constant(self, formula, **kwargs):
         return '"' + formula.constant_value().replace('"', '""') + '"'
 
@@ -490,6 +553,7 @@ class SmtDagPrinter(DagWalker):
     def walk_exists(self, formula, args, **kwargs):
         return self._walk_quantifier("exists", formula, args)
 
+    @write_annotations_dag
     def _walk_quantifier(self, operator, formula, args):
         assert args is None
         assert len(formula.quantifier_vars()) > 0
@@ -510,6 +574,7 @@ class SmtDagPrinter(DagWalker):
         self.write(")))")
         return sym
 
+    @write_annotations_dag
     def walk_bv_extract(self, formula, args, **kwargs):
         assert formula is not None
         sym = self._new_symbol()
@@ -524,6 +589,7 @@ class SmtDagPrinter(DagWalker):
         return sym
 
     @handles(op.BV_SEXT, op.BV_ZEXT)
+    @write_annotations_dag
     def walk_bv_extend(self, formula, args, **kwargs):
         #pylint: disable=unused-argument
         if formula.is_bv_zext():
@@ -543,6 +609,7 @@ class SmtDagPrinter(DagWalker):
         return sym
 
     @handles(op.BV_ROR, op.BV_ROL)
+    @write_annotations_dag
     def walk_bv_rotate(self, formula, args, **kwargs):
         #pylint: disable=unused-argument
         if formula.is_bv_ror():
@@ -561,12 +628,15 @@ class SmtDagPrinter(DagWalker):
         self.write("))) ")
         return sym
 
+    @write_annotations_dag
     def walk_str_length(self, formula, args, **kwargs):
         return "(str.len %s)" % args[0]
 
+    @write_annotations_dag
     def walk_str_charat(self,formula, args,**kwargs):
         return "( str.at %s %s )" % (args[0], args[1])
 
+    @write_annotations_dag
     def walk_str_concat(self, formula, args, **kwargs):
         sym = self._new_symbol()
         self.openings += 1
@@ -577,30 +647,39 @@ class SmtDagPrinter(DagWalker):
         self.write("))) ")
         return sym
 
+    @write_annotations_dag
     def walk_str_contains(self,formula, args, **kwargs):
         return "( str.contains %s %s)" % (args[0], args[1])
 
+    @write_annotations_dag
     def walk_str_indexof(self,formula, args, **kwargs):
         return "( str.indexof %s %s %s )" % (args[0], args[1], args[2])
 
+    @write_annotations_dag
     def walk_str_replace(self,formula, args, **kwargs):
         return "( str.replace %s %s %s )" % (args[0], args[1], args[2])
 
+    @write_annotations_dag
     def walk_str_substr(self,formula, args,**kwargs):
         return "( str.substr %s %s %s)" % (args[0], args[1], args[2])
 
+    @write_annotations_dag
     def walk_str_prefixof(self,formula, args,**kwargs):
         return "( str.prefixof %s %s )" % (args[0], args[1])
 
+    @write_annotations_dag
     def walk_str_suffixof(self,formula, args, **kwargs):
         return "( str.suffixof %s %s )" % (args[0], args[1])
 
+    @write_annotations_dag
     def walk_str_to_int(self,formula, args, **kwargs):
         return "( str.to.int %s )" % args[0]
 
+    @write_annotations_dag
     def walk_int_to_str(self,formula, args, **kwargs):
         return "( int.to.str %s )" % args[0]
 
+    @write_annotations_dag
     def walk_array_value(self, formula, args, **kwargs):
         sym = self._new_symbol()
         self.openings += 1
diff --git a/pysmt/smtlib/script.py b/pysmt/smtlib/script.py
index feb0a07..e66e34c 100644
--- a/pysmt/smtlib/script.py
+++ b/pysmt/smtlib/script.py
@@ -227,9 +227,9 @@ class SmtLibScript(object):
     def serialize(self, outstream, daggify=True):
         """Serializes the SmtLibScript expanding commands"""
         if daggify:
-            printer = SmtDagPrinter(outstream)
+            printer = SmtDagPrinter(outstream, annotations=self.annotations)
         else:
-            printer = SmtPrinter(outstream)
+            printer = SmtPrinter(outstream, annotations=self.annotations)
 
         for cmd in self.commands:
             cmd.serialize(printer=printer)


Test patch:
diff --git a/pysmt/test/test_printing.py b/pysmt/test/test_printing.py
index 5481750..c0ad4f2 100644
--- a/pysmt/test/test_printing.py
+++ b/pysmt/test/test_printing.py
@@ -23,6 +23,7 @@ from pysmt.shortcuts import Bool, Real, Int, Symbol, Function
 from pysmt.shortcuts import Times, Minus, Equals, LE, LT, ToReal, FreshSymbol
 from pysmt.typing import REAL, INT, FunctionType
 from pysmt.smtlib.printers import SmtPrinter, SmtDagPrinter
+from pysmt.smtlib.annotations import Annotations
 from pysmt.printers import smart_serialize
 from pysmt.test import TestCase, main
 from pysmt.test.examples import get_str_example_formulae
@@ -205,5 +206,28 @@ class TestPrinting(TestCase):
         s = f.serialize()
         self.assertIsNotNone(s)
 
+    def test_annotations(self):
+        x = Symbol('x')
+        x_next = Symbol('x.next')
+        f = Iff(x, Not(x_next))
+
+        ann = Annotations()
+        ann.add(x, 'next', x_next.symbol_name())
+        ann.add(f, 'trans', 'true')
+        ann.add(x, 'init', 'true')
+
+        tree_buf = StringIO()
+        dag_buf = StringIO()
+        tree_printer = SmtPrinter(tree_buf, annotations=ann)
+        dag_printer = SmtDagPrinter(dag_buf, annotations=ann)
+
+        dag_printer.printer(f)
+        tree_printer.printer(f)
+
+        self.assertEqual(tree_buf.getvalue(),
+                         "(! (= (! x :next x.next :init true) (not x.next)) :trans true)")
+        self.assertEqual(dag_buf.getvalue(),
+                         "(let ((.def_0 (not x.next))) (let ((.def_1 (= (! x :next x.next :init true) .def_0))) (! .def_1 :trans true)))")
+
 if __name__ == '__main__':
     main()