Repository: pysmt/pysmt
Pull request #399 (2017-02-14 13:37:10)

Print SmtLib term as string shortcut and default to dag SmtLib representation
This PR addresses issues #396 and #397.

I introduced a shortcut ```smtlib_serialize``` and a method of FNode with the same name that return a string representation of the given formula. The ```daggify``` parameter is used to enable or disable the use of ```let``` operators to represent the formulae linearly.


Patch:
diff --git a/pysmt/fnode.py b/pysmt/fnode.py
index c77b9d4..91430cf 100644
--- a/pysmt/fnode.py
+++ b/pysmt/fnode.py
@@ -17,8 +17,8 @@
 #
 """FNode are the building blocks of formulae."""
 import collections
-
 import pysmt.environment
+import pysmt.smtlib
 from pysmt.operators import (FORALL, EXISTS, AND, OR, NOT, IMPLIES, IFF,
                              SYMBOL, FUNCTION,
                              REAL_CONSTANT, BOOL_CONSTANT, INT_CONSTANT,
@@ -508,6 +508,18 @@ class FNode(object):
         """
         return _env().serializer.serialize(self, threshold=threshold)
 
+    def to_smtlib(self, daggify=True):
+        """Returns a Smt-Lib string representation of the formula.
+
+        The daggify parameter can be used to switch from a linear-size
+        representation that uses 'let' operators to represent the
+        formula as a dag or a simpler (but possibly exponential)
+        representation that expands the formula as a tree.
+
+        See :py:class:`SmtPrinter`
+        """
+        return pysmt.smtlib.printers.to_smtlib(self, daggify=daggify)
+
     def is_function_application(self):
         """Test whether the node is a Function application."""
         return self.node_type() == FUNCTION
diff --git a/pysmt/shortcuts.py b/pysmt/shortcuts.py
index 940b7ca..645ec82 100644
--- a/pysmt/shortcuts.py
+++ b/pysmt/shortcuts.py
@@ -37,6 +37,7 @@ import pysmt.configuration as config
 import pysmt.environment
 import pysmt.smtlib.parser
 import pysmt.smtlib.script
+import pysmt.smtlib.printers
 
 
 def get_env():
@@ -1101,3 +1102,16 @@ def write_smtlib(formula, fname):
     with open(fname, "w") as fout:
         script = pysmt.smtlib.script.smtlibscript_from_formula(formula)
         script.serialize(fout)
+
+
+def to_smtlib(formula, daggify=True):
+    """Returns a Smt-Lib string representation of the formula.
+
+    The daggify parameter can be used to switch from a linear-size
+    representation that uses 'let' operators to represent the
+    formula as a dag or a simpler (but possibly exponential)
+    representation that expands the formula as a tree.
+
+    See :py:class:`SmtPrinter`
+    """
+    return pysmt.smtlib.printers.to_smtlib(formula, daggify=daggify)
diff --git a/pysmt/smtlib/printers.py b/pysmt/smtlib/printers.py
index 867f80a..aea9fdf 100644
--- a/pysmt/smtlib/printers.py
+++ b/pysmt/smtlib/printers.py
@@ -17,7 +17,7 @@
 #
 from functools import partial
 
-from six.moves import xrange
+from six.moves import xrange, cStringIO
 
 import pysmt.operators as op
 from pysmt.environment import get_env
@@ -430,3 +430,25 @@ class SmtDagPrinter(DagWalker):
             self.write(")")
         self.write("))")
         return sym
+
+
+def to_smtlib(formula, daggify=True):
+    """Returns a Smt-Lib string representation of the formula.
+
+    The daggify parameter can be used to switch from a linear-size
+    representation that uses 'let' operators to represent the
+    formula as a dag or a simpler (but possibly exponential)
+    representation that expands the formula as a tree.
+
+    See :py:class:`SmtPrinter`
+    """
+    buf = cStringIO()
+    p = None
+    if daggify:
+        p = SmtDagPrinter(buf)
+    else:
+        p = SmtPrinter(buf)
+    p.printer(formula)
+    res = buf.getvalue()
+    buf.close()
+    return res
diff --git a/pysmt/smtlib/script.py b/pysmt/smtlib/script.py
index 3073f73..5387d26 100644
--- a/pysmt/smtlib/script.py
+++ b/pysmt/smtlib/script.py
@@ -42,7 +42,7 @@ def check_sat_filter(log):
 
 
 class SmtLibCommand(namedtuple('SmtLibCommand', ['name', 'args'])):
-    def serialize(self, outstream=None, printer=None, daggify=False):
+    def serialize(self, outstream=None, printer=None, daggify=True):
         """Serializes the SmtLibCommand into outstream using the given printer.
 
         Exactly one of outstream or printer must be specified. When
@@ -131,9 +131,9 @@ class SmtLibCommand(namedtuple('SmtLibCommand', ['name', 'args'])):
         else:
             raise UnknownSmtLibCommandError(self.name)
 
-    def serialize_to_string(self):
+    def serialize_to_string(self, daggify=True):
         buf = cStringIO()
-        self.serialize(buf)
+        self.serialize(buf, daggify=daggify)
         return buf.getvalue()
 
 


Test patch:
diff --git a/pysmt/test/test_printing.py b/pysmt/test/test_printing.py
index fefb812..fe4fa8a 100644
--- a/pysmt/test/test_printing.py
+++ b/pysmt/test/test_printing.py
@@ -31,60 +31,59 @@ from pysmt.test.examples import get_str_example_formulae
 
 class TestPrinting(TestCase):
     def print_to_string(self, formula):
-        buf = cStringIO()
-        printer = SmtPrinter(buf)
-        printer.printer(formula)
-
-        return buf.getvalue()
+        return formula.to_smtlib(daggify=False)
 
     def test_real(self):
         f = Plus([ Real(1),
                    Symbol("x", REAL),
                    Symbol("y", REAL)])
 
-        f_string = self.print_to_string(f)
-        self.assertEqual(f_string, "(+ 1.0 x y)")
+        self.assertEqual(f.to_smtlib(daggify=False), "(+ 1.0 x y)")
+        self.assertEqual(f.to_smtlib(daggify=True), "(let ((.def_0 (+ 1.0 x y))) .def_0)")
 
     def test_boolean(self):
         x, y, z = Symbol("x"), Symbol("y"), Symbol("z")
         f = Or(And(Not(x), Iff(x, y)), Implies(x, z))
 
-        f_string = self.print_to_string(f)
-        self.assertEqual(f_string,
+        self.assertEqual(f.to_smtlib(daggify=False),
                           "(or (and (not x) (= x y)) (=> x z))")
+        self.assertEqual(f.to_smtlib(daggify=True),
+                          "(let ((.def_0 (=> x z))) (let ((.def_1 (= x y))) (let ((.def_2 (not x))) (let ((.def_3 (and .def_2 .def_1))) (let ((.def_4 (or .def_3 .def_0))) .def_4)))))")
 
     def test_int(self):
         p, q = Symbol("p", INT), Symbol("q", INT)
         f = Or(Equals(Times(p, Int(5)), Minus(p,q)),
                LT(p,q), LE(Int(6), Int(1)))
 
-        f_string = self.print_to_string(f)
-        self.assertEqual(f_string,
+        self.assertEqual(f.to_smtlib(daggify=False),
                           "(or (= (* p 5) (- p q)) (< p q) (<= 6 1))")
+        self.assertEqual(f.to_smtlib(daggify=True),
+                          "(let ((.def_0 (<= 6 1))) (let ((.def_1 (< p q))) (let ((.def_2 (- p q))) (let ((.def_3 (* p 5))) (let ((.def_4 (= .def_3 .def_2))) (let ((.def_5 (or .def_4 .def_1 .def_0))) .def_5))))))")
 
     def test_ite(self):
         x = Symbol("x")
         p, q = Symbol("p", INT), Symbol("q", INT)
 
         f = Ite(x, p, q)
-        f_string = self.print_to_string(f)
 
-        self.assertEqual(f_string,
-                          "(ite x p q)")
+        self.assertEqual(f.to_smtlib(daggify=False),
+                         "(ite x p q)")
+        self.assertEqual(f.to_smtlib(daggify=True),
+                         "(let ((.def_0 (ite x p q))) .def_0)")
 
     def test_quantifiers(self):
         x = Symbol("x")
         fa = ForAll([x], And(x, Not(x)))
         fe = Exists([x], And(x, Not(x)))
 
-        fa_string = self.print_to_string(fa)
-        fe_string = self.print_to_string(fe)
-
-        self.assertEqual(fa_string,
-                          "(forall ((x Bool)) (and x (not x)))")
-
-        self.assertEqual(fe_string,
-                          "(exists ((x Bool)) (and x (not x)))")
+        self.assertEqual(fa.to_smtlib(daggify=False),
+                         "(forall ((x Bool)) (and x (not x)))")
+        self.assertEqual(fe.to_smtlib(daggify=False),
+                         "(exists ((x Bool)) (and x (not x)))")
+        self.assertEqual(fa.to_smtlib(daggify=True),
+                         "(let ((.def_0 (forall ((x Bool)) (let ((.def_0 (not x))) (let ((.def_1 (and x .def_0))) .def_1))))).def_0)")
+        self.assertEqual(fe.to_smtlib(daggify=True),
+                         "(let ((.def_0 (exists ((x Bool)) (let ((.def_0 (not x))) (let ((.def_1 (and x .def_0))) .def_1))))).def_0)")
 
 
     def test_constant(self):
@@ -96,25 +95,25 @@ class TestPrinting(TestCase):
         i1 = Int(4)
         i2 = Int(-4)
 
-        b1_string = self.print_to_string(b1)
-        b2_string = self.print_to_string(b2)
+        self.assertEqual(b1.to_smtlib(daggify=True), "true")
+        self.assertEqual(b2.to_smtlib(daggify=True), "false")
 
-        self.assertEqual(b1_string, "true")
-        self.assertEqual(b2_string, "false")
+        self.assertEqual(r1.to_smtlib(daggify=True), "(/ 11 2)")
+        self.assertEqual(r2.to_smtlib(daggify=True), "5.0")
+        self.assertEqual(r3.to_smtlib(daggify=True), "(- (/ 11 2))")
 
-        r1_string = self.print_to_string(r1)
-        r2_string = self.print_to_string(r2)
-        r3_string = self.print_to_string(r3)
+        self.assertEqual(i1.to_smtlib(daggify=True), "4")
+        self.assertEqual(i2.to_smtlib(daggify=True), "(- 4)")
 
-        self.assertEqual(r1_string, "(/ 11 2)")
-        self.assertEqual(r2_string, "5.0")
-        self.assertEqual(r3_string, "(- (/ 11 2))")
+        self.assertEqual(b1.to_smtlib(daggify=False), "true")
+        self.assertEqual(b2.to_smtlib(daggify=False), "false")
 
-        i1_string = self.print_to_string(i1)
-        i2_string = self.print_to_string(i2)
+        self.assertEqual(r1.to_smtlib(daggify=False), "(/ 11 2)")
+        self.assertEqual(r2.to_smtlib(daggify=False), "5.0")
+        self.assertEqual(r3.to_smtlib(daggify=False), "(- (/ 11 2))")
 
-        self.assertEqual(i1_string, "4")
-        self.assertEqual(i2_string, "(- 4)")
+        self.assertEqual(i1.to_smtlib(daggify=False), "4")
+        self.assertEqual(i2.to_smtlib(daggify=False), "(- 4)")
 
     def test_function(self):
         f1_type = FunctionType(REAL, [REAL, REAL])
@@ -127,18 +126,18 @@ class TestPrinting(TestCase):
         f1 = Function(f1_symbol, [p,q])
         f2 = Function(f2_symbol, [])
 
-        f1_string = self.print_to_string(f1)
-        f2_string = self.print_to_string(f2)
+        self.assertEqual(f1.to_smtlib(daggify=False), "(f1 p q)")
+        self.assertEqual(f2.to_smtlib(daggify=False), "f2")
 
-        self.assertEqual(f1_string, "(f1 p q)")
-        self.assertEqual(f2_string, "f2")
+        self.assertEqual(f1.to_smtlib(daggify=True), "(let ((.def_0 (f1 p q))) .def_0)")
+        self.assertEqual(f2.to_smtlib(daggify=True), "f2")
 
     def test_toreal(self):
         p = Symbol("p", INT)
         rp = ToReal(p)
 
-        rp_string = self.print_to_string(rp)
-        self.assertEqual(rp_string, "(to_real p)")
+        self.assertEqual(rp.to_smtlib(daggify=False), "(to_real p)")
+        self.assertEqual(rp.to_smtlib(daggify=True), "(let ((.def_0 (to_real p))) .def_0)")
 
     def test_threshold_printing(self):
         x = Symbol("x")
diff --git a/pysmt/test/test_regressions.py b/pysmt/test/test_regressions.py
index 2aefcd1..bf5619c 100644
--- a/pysmt/test/test_regressions.py
+++ b/pysmt/test/test_regressions.py
@@ -392,7 +392,7 @@ class TestRegressions(TestCase):
         buffer_ = cStringIO(smtlib_input)
         s = parser.get_script(buffer_)
         for c in s:
-            res = c.serialize_to_string()
+            res = c.serialize_to_string(daggify=False)
         self.assertEqual(res, smtlib_input)
 
     @skipIfSolverNotAvailable("z3")