Skip to content

Commit

Permalink
Merge ea1d797 into 8db6ee1
Browse files Browse the repository at this point in the history
  • Loading branch information
@mikand
mikand committed Mar 14, 2017
2 parents 8db6ee1 + ea1d797 commit f42ebb6
Show file tree
Hide file tree
Showing 6 changed files with 95 additions and 48 deletions.
14 changes: 13 additions & 1 deletion pysmt/fnode.py
View file
Expand Up @@ -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,
Expand Down Expand Up @@ -508,6 +508,18 @@ def serialize(self, threshold=None):
"""
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
Expand Down
14 changes: 14 additions & 0 deletions pysmt/shortcuts.py
View file
Expand Up @@ -37,6 +37,7 @@
import pysmt.typing as types
import pysmt.smtlib.parser
import pysmt.smtlib.script
import pysmt.smtlib.printers

# Import types from shortcuts
from pysmt.typing import INT, BOOL, REAL, BVType, FunctionType, ArrayType, Type
Expand Down Expand Up @@ -1105,3 +1106,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)
24 changes: 23 additions & 1 deletion pysmt/smtlib/printers.py
View file
Expand Up @@ -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
Expand Down Expand Up @@ -430,3 +430,25 @@ def walk_array_value(self, formula, args, **kwargs):
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
6 changes: 3 additions & 3 deletions pysmt/smtlib/script.py
View file
Expand Up @@ -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
Expand Down Expand Up @@ -131,9 +131,9 @@ def serialize(self, outstream=None, printer=None, daggify=False):
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()


Expand Down
83 changes: 41 additions & 42 deletions pysmt/test/test_printing.py
View file
Expand Up @@ -31,60 +31,59 @@

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):
Expand All @@ -96,25 +95,25 @@ def test_constant(self):
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])
Expand All @@ -127,18 +126,18 @@ def test_function(self):
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")
Expand Down
2 changes: 1 addition & 1 deletion pysmt/test/test_regressions.py
View file
Expand Up @@ -392,7 +392,7 @@ def test_smtlib_define_fun_serialization(self):
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")
Expand Down

0 comments on commit f42ebb6

Please sign in to comment.