#
# This file is part of pySMT.
#
# Copyright 2014 Andrea Micheli and Marco Gario
#
# Licensed under the Apache License, Version 2.0 (the "License");
# you may not use this file except in compliance with the License.
# You may obtain a copy of the License at
#
# http://www.apache.org/licenses/LICENSE-2.0
#
# Unless required by applicable law or agreed to in writing, software
# distributed under the License is distributed on an "AS IS" BASIS,
# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
# See the License for the specific language governing permissions and
# limitations under the License.
#
from functools import partial
from six.moves import xrange, cStringIO
import pysmt.operators as op
from pysmt.environment import get_env
from pysmt.walkers import TreeWalker, DagWalker, handles
from pysmt.utils import quote
[docs]class SmtPrinter(TreeWalker):
def __init__(self, stream):
TreeWalker.__init__(self)
self.stream = stream
self.write = self.stream.write
self.mgr = get_env().formula_manager
def printer(self, f):
self.walk(f)
[docs] def walk_threshold(self, formula):
"""This is a complete printer"""
raise NotImplementedError
def walk_nary(self, formula, operator):
self.write("(%s" % operator)
for s in formula.args():
self.write(" ")
yield s
self.write(")")
[docs] def walk_and(self, formula): return self.walk_nary(formula, "and")
[docs] def walk_or(self, formula): return self.walk_nary(formula, "or")
[docs] def walk_not(self, formula): return self.walk_nary(formula, "not")
[docs] def walk_implies(self, formula): return self.walk_nary(formula, "=>")
[docs] def walk_iff(self, formula): return self.walk_nary(formula, "=")
[docs] def walk_plus(self, formula): return self.walk_nary(formula, "+")
[docs] def walk_minus(self, formula): return self.walk_nary(formula, "-")
[docs] def walk_times(self, formula): return self.walk_nary(formula, "*")
[docs] def walk_equals(self, formula): return self.walk_nary(formula, "=")
[docs] def walk_le(self, formula): return self.walk_nary(formula, "<=")
[docs] def walk_lt(self, formula): return self.walk_nary(formula, "<")
[docs] def walk_ite(self, formula): return self.walk_nary(formula, "ite")
[docs] def walk_toreal(self, formula): return self.walk_nary(formula, "to_real")
[docs] def walk_div(self, formula): return self.walk_nary(formula, "/")
[docs] def walk_pow(self, formula): return self.walk_nary(formula, "pow")
[docs] def walk_bv_and(self, formula): return self.walk_nary(formula, "bvand")
[docs] def walk_bv_or(self, formula): return self.walk_nary(formula, "bvor")
[docs] def walk_bv_not(self, formula): return self.walk_nary(formula, "bvnot")
[docs] def walk_bv_xor(self, formula): return self.walk_nary(formula, "bvxor")
[docs] def walk_bv_add(self, formula): return self.walk_nary(formula, "bvadd")
[docs] def walk_bv_sub(self, formula): return self.walk_nary(formula, "bvsub")
[docs] def walk_bv_neg(self, formula): return self.walk_nary(formula, "bvneg")
[docs] def walk_bv_mul(self, formula): return self.walk_nary(formula, "bvmul")
[docs] def walk_bv_udiv(self, formula): return self.walk_nary(formula, "bvudiv")
[docs] def walk_bv_urem(self, formula): return self.walk_nary(formula, "bvurem")
[docs] def walk_bv_lshl(self, formula): return self.walk_nary(formula, "bvshl")
[docs] def walk_bv_lshr(self, formula): return self.walk_nary(formula, "bvlshr")
[docs] def walk_bv_ult(self, formula): return self.walk_nary(formula, "bvult")
[docs] def walk_bv_ule(self, formula): return self.walk_nary(formula, "bvule")
[docs] def walk_bv_slt(self, formula): return self.walk_nary(formula, "bvslt")
[docs] def walk_bv_sle(self, formula): return self.walk_nary(formula, "bvsle")
[docs] def walk_bv_concat(self, formula): return self.walk_nary(formula, "concat")
[docs] def walk_bv_comp(self, formula): return self.walk_nary(formula, "bvcomp")
[docs] def walk_bv_ashr(self, formula): return self.walk_nary(formula, "bvashr")
[docs] def walk_bv_sdiv(self, formula): return self.walk_nary(formula, "bvsdiv")
[docs] def walk_bv_srem(self, formula): return self.walk_nary(formula, "bvsrem")
[docs] def walk_bv_tonatural(self, formula): return self.walk_nary(formula, "bv2nat")
[docs] def walk_array_select(self, formula): return self.walk_nary(formula, "select")
[docs] def walk_array_store(self, formula): return self.walk_nary(formula, "store")
[docs] def walk_symbol(self, formula):
self.write(quote(formula.symbol_name()))
[docs] def walk_function(self, formula):
return self.walk_nary(formula, formula.function_name())
[docs] def walk_int_constant(self, formula):
if formula.constant_value() < 0:
self.write("(- " + str(-formula.constant_value()) + ")")
else:
self.write(str(formula.constant_value()))
[docs] def walk_real_constant(self, formula):
if formula.constant_value() < 0:
template = "(- %s)"
else:
template = "%s"
(n,d) = abs(formula.constant_value().numerator), \
formula.constant_value().denominator
if d != 1:
res = template % ( "(/ " + str(n) + " " + str(d) + ")" )
else:
res = template % (str(n) + ".0")
self.write(res)
[docs] def walk_bool_constant(self, formula):
if formula.constant_value():
self.write("true")
else:
self.write("false")
[docs] def walk_bv_constant(self, formula):
self.write("#b" + formula.bv_bin_str())
[docs] def walk_str_constant(self, formula):
self.write('"' + formula.constant_value().replace('"', '""') + '"')
[docs] def walk_forall(self, formula):
return self._walk_quantifier("forall", formula)
[docs] def walk_exists(self, formula):
return self._walk_quantifier("exists", formula)
def _walk_quantifier(self, operator, formula):
assert len(formula.quantifier_vars()) > 0
self.write("(%s (" % operator)
for s in formula.quantifier_vars():
self.write("(")
yield s
self.write(" %s)" % s.symbol_type().as_smtlib(False))
self.write(") ")
yield formula.arg(0)
self.write(")")
@handles(op.BV_ROR, op.BV_ROL)
def walk_bv_rotate(self, formula):
if formula.is_bv_ror():
rotate_type = "rotate_right"
else:
assert formula.is_bv_rol()
rotate_type = "rotate_left"
self.write("((_ %s %d) " % (rotate_type,
formula.bv_rotation_step()))
yield formula.arg(0)
self.write(")")
@handles(op.BV_ZEXT, op.BV_SEXT)
def walk_bv_extend(self, formula):
if formula.is_bv_zext():
extend_type = "zero_extend"
else:
assert formula.is_bv_sext()
extend_type = "sign_extend"
self.write("((_ %s %d) " % (extend_type,
formula.bv_extend_step()))
yield formula.arg(0)
self.write(")")
[docs] def walk_str_length(self, formula):
self.write("(str.len ")
self.walk(formula.arg(0))
self.write(")")
[docs] def walk_str_charat(self,formula, **kwargs):
self.write("( str.at " )
self.walk(formula.arg(0))
self.write(" ")
self.walk(formula.arg(1))
self.write(")")
[docs] def walk_str_concat(self,formula, **kwargs):
self.write("( str.++ " )
for arg in formula.args():
self.walk(arg)
self.write(" ")
self.write(")")
[docs] def walk_str_contains(self,formula, **kwargs):
self.write("( str.contains " )
self.walk(formula.arg(0))
self.write(" ")
self.walk(formula.arg(1))
self.write(")")
[docs] def walk_str_indexof(self,formula, **kwargs):
self.write("( str.indexof " )
self.walk(formula.arg(0))
self.write(" ")
self.walk(formula.arg(1))
self.write(" ")
self.walk(formula.arg(2))
self.write(")")
[docs] def walk_str_replace(self,formula, **kwargs):
self.write("( str.replace " )
self.walk(formula.arg(0))
self.write(" ")
self.walk(formula.arg(1))
self.write(" ")
self.walk(formula.arg(2))
self.write(")")
[docs] def walk_str_substr(self,formula, **kwargs):
self.write("( str.substr " )
self.walk(formula.arg(0))
self.write(" ")
self.walk(formula.arg(1))
self.write(" ")
self.walk(formula.arg(2))
self.write(")")
[docs] def walk_str_prefixof(self,formula, **kwargs):
self.write("( str.prefixof " )
self.walk(formula.arg(0))
self.write(" ")
self.walk(formula.arg(1))
self.write(")")
[docs] def walk_str_suffixof(self,formula, **kwargs):
self.write("( str.suffixof " )
self.walk(formula.arg(0))
self.write(" ")
self.walk(formula.arg(1))
self.write(")")
[docs] def walk_str_to_int(self,formula, **kwargs):
self.write("( str.to.int " )
self.walk(formula.arg(0))
self.write(")")
[docs] def walk_int_to_str(self,formula, **kwargs):
self.write("( int.to.str " )
self.walk(formula.arg(0))
self.write(")")
[docs] def walk_array_value(self, formula):
assign = formula.array_value_assigned_values_map()
for _ in xrange(len(assign)):
self.write("(store ")
self.write("((as const %s) " % formula.get_type().as_smtlib(False))
yield formula.array_value_default()
self.write(")")
for k in sorted(assign, key=str):
self.write(" ")
yield k
self.write(" ")
yield assign[k]
self.write(")")
[docs]class SmtDagPrinter(DagWalker):
def __init__(self, stream, template=".def_%d"):
DagWalker.__init__(self, invalidate_memoization=True)
self.stream = stream
self.write = self.stream.write
self.openings = 0
self.name_seed = 0
self.template = template
self.names = None
self.mgr = get_env().formula_manager
def _push_with_children_to_stack(self, formula, **kwargs):
"""Add children to the stack."""
# Deal with quantifiers
if formula.is_quantifier():
# 1. We invoke the relevant function (walk_exists or
# walk_forall) to print the formula
fun = self.functions[formula.node_type()]
res = fun(formula, args=None, **kwargs)
# 2. We memoize the result
key = self._get_key(formula, **kwargs)
self.memoization[key] = res
else:
DagWalker._push_with_children_to_stack(self, formula, **kwargs)
def printer(self, f):
self.openings = 0
self.name_seed = 0
self.names = set(quote(x.symbol_name()) for x in f.get_free_variables())
key = self.walk(f)
self.write(key)
self.write(")" * self.openings)
def _new_symbol(self):
while (self.template % self.name_seed) in self.names:
self.name_seed += 1
res = (self.template % self.name_seed)
self.name_seed += 1
return res
def walk_nary(self, formula, args, operator):
assert formula is not None
sym = self._new_symbol()
self.openings += 1
self.write("(let ((%s (%s" % (sym, operator))
for s in args:
self.write(" ")
self.write(s)
self.write("))) ")
return sym
[docs] def walk_and(self, formula, args):
return self.walk_nary(formula, args, "and")
[docs] def walk_or(self, formula, args):
return self.walk_nary(formula, args, "or")
[docs] def walk_not(self, formula, args):
return self.walk_nary(formula, args, "not")
[docs] def walk_implies(self, formula, args):
return self.walk_nary(formula, args, "=>")
[docs] def walk_iff(self, formula, args):
return self.walk_nary(formula, args, "=")
[docs] def walk_plus(self, formula, args):
return self.walk_nary(formula, args, "+")
[docs] def walk_minus(self, formula, args):
return self.walk_nary(formula, args, "-")
[docs] def walk_times(self, formula, args):
return self.walk_nary(formula, args, "*")
[docs] def walk_equals(self, formula, args):
return self.walk_nary(formula, args, "=")
[docs] def walk_le(self, formula, args):
return self.walk_nary(formula, args, "<=")
[docs] def walk_lt(self, formula, args):
return self.walk_nary(formula, args, "<")
[docs] def walk_ite(self, formula, args):
return self.walk_nary(formula, args, "ite")
[docs] def walk_toreal(self, formula, args):
return self.walk_nary(formula, args, "to_real")
[docs] def walk_div(self, formula, args):
return self.walk_nary(formula, args, "/")
[docs] def walk_pow(self, formula, args):
return self.walk_nary(formula, args, "pow")
[docs] def walk_bv_and(self, formula, args):
return self.walk_nary(formula, args, "bvand")
[docs] def walk_bv_or(self, formula, args):
return self.walk_nary(formula, args, "bvor")
[docs] def walk_bv_not(self, formula, args):
return self.walk_nary(formula, args, "bvnot")
[docs] def walk_bv_xor(self, formula, args):
return self.walk_nary(formula, args, "bvxor")
[docs] def walk_bv_add(self, formula, args):
return self.walk_nary(formula, args, "bvadd")
[docs] def walk_bv_sub(self, formula, args):
return self.walk_nary(formula, args, "bvsub")
[docs] def walk_bv_neg(self, formula, args):
return self.walk_nary(formula, args, "bvneg")
[docs] def walk_bv_mul(self, formula, args):
return self.walk_nary(formula, args, "bvmul")
[docs] def walk_bv_udiv(self, formula, args):
return self.walk_nary(formula, args, "bvudiv")
[docs] def walk_bv_urem(self, formula, args):
return self.walk_nary(formula, args, "bvurem")
[docs] def walk_bv_lshl(self, formula, args):
return self.walk_nary(formula, args, "bvshl")
[docs] def walk_bv_lshr(self, formula, args):
return self.walk_nary(formula, args, "bvlshr")
[docs] def walk_bv_ult(self, formula, args):
return self.walk_nary(formula, args, "bvult")
[docs] def walk_bv_ule(self, formula, args):
return self.walk_nary(formula, args, "bvule")
[docs] def walk_bv_slt(self, formula, args):
return self.walk_nary(formula, args, "bvslt")
[docs] def walk_bv_sle(self, formula, args):
return self.walk_nary(formula, args, "bvsle")
[docs] def walk_bv_concat(self, formula, args):
return self.walk_nary(formula, args, "concat")
[docs] def walk_bv_comp(self, formula, args):
return self.walk_nary(formula, args, "bvcomp")
[docs] def walk_bv_ashr(self, formula, args):
return self.walk_nary(formula, args, "bvashr")
[docs] def walk_bv_sdiv(self, formula, args):
return self.walk_nary(formula, args, "bvsdiv")
[docs] def walk_bv_srem(self, formula, args):
return self.walk_nary(formula, args, "bvsrem")
[docs] def walk_bv_tonatural(self, formula, args):
return self.walk_nary(formula, args, "bv2nat")
[docs] def walk_array_select(self, formula, args):
return self.walk_nary(formula, args, "select")
[docs] def walk_array_store(self, formula, args):
return self.walk_nary(formula, args, "store")
[docs] def walk_symbol(self, formula, **kwargs):
return quote(formula.symbol_name())
[docs] def walk_function(self, formula, args, **kwargs):
return self.walk_nary(formula, args, formula.function_name())
[docs] def walk_int_constant(self, formula, **kwargs):
if formula.constant_value() < 0:
return "(- " + str(-formula.constant_value()) + ")"
else:
return str(formula.constant_value())
[docs] def walk_real_constant(self, formula, **kwargs):
if formula.constant_value() < 0:
template = "(- %s)"
else:
template = "%s"
(n,d) = abs(formula.constant_value().numerator), \
formula.constant_value().denominator
if d != 1:
return template % ( "(/ " + str(n) + " " + str(d) + ")" )
else:
return template % (str(n) + ".0")
[docs] def walk_bv_constant(self, formula, **kwargs):
short_res = str(bin(formula.constant_value()))[2:]
if formula.constant_value() >= 0:
filler = "0"
else:
raise NotImplementedError
res = short_res.rjust(formula.bv_width(), filler)
return "#b" + res
[docs] def walk_bool_constant(self, formula, **kwargs):
if formula.constant_value():
return "true"
else:
return "false"
[docs] def walk_str_constant(self, formula, **kwargs):
return '"' + formula.constant_value().replace('"', '""') + '"'
[docs] def walk_forall(self, formula, args, **kwargs):
return self._walk_quantifier("forall", formula, args)
[docs] def walk_exists(self, formula, args, **kwargs):
return self._walk_quantifier("exists", formula, args)
def _walk_quantifier(self, operator, formula, args):
assert args is None
assert len(formula.quantifier_vars()) > 0
sym = self._new_symbol()
self.openings += 1
self.write("(let ((%s (%s (" % (sym, operator))
for s in formula.quantifier_vars():
self.write("(")
self.write(quote(s.symbol_name()))
self.write(" %s)" % s.symbol_type().as_smtlib(False))
self.write(") ")
subprinter = SmtDagPrinter(self.stream)
subprinter.printer(formula.arg(0))
self.write(")))")
return sym
@handles(op.BV_SEXT, op.BV_ZEXT)
def walk_bv_extend(self, formula, args, **kwargs):
#pylint: disable=unused-argument
if formula.is_bv_zext():
extend_type = "zero_extend"
else:
assert formula.is_bv_sext()
extend_type = "sign_extend"
sym = self._new_symbol()
self.openings += 1
self.write("(let ((%s ((_ %s %d)" % (sym, extend_type,
formula.bv_extend_step()))
for s in args:
self.write(" ")
self.write(s)
self.write("))) ")
return sym
@handles(op.BV_ROR, op.BV_ROL)
def walk_bv_rotate(self, formula, args, **kwargs):
#pylint: disable=unused-argument
if formula.is_bv_ror():
rotate_type = "rotate_right"
else:
assert formula.is_bv_rol()
rotate_type = "rotate_left"
sym = self._new_symbol()
self.openings += 1
self.write("(let ((%s ((_ %s %d)" % (sym, rotate_type,
formula.bv_rotation_step()))
for s in args:
self.write(" ")
self.write(s)
self.write("))) ")
return sym
[docs] def walk_str_length(self, formula, args, **kwargs):
return "(str.len %s)" % args[0]
[docs] def walk_str_charat(self,formula, args,**kwargs):
return "( str.at %s %s )" % (args[0], args[1])
[docs] def walk_str_concat(self, formula, args, **kwargs):
sym = self._new_symbol()
self.openings += 1
self.write("(let ((%s (%s" % (sym, "str.++ " ))
for s in args:
self.write(" ")
self.write(s)
self.write("))) ")
return sym
[docs] def walk_str_contains(self,formula, args, **kwargs):
return "( str.contains %s %s)" % (args[0], args[1])
[docs] def walk_str_indexof(self,formula, args, **kwargs):
return "( str.indexof %s %s %s )" % (args[0], args[1], args[2])
[docs] def walk_str_replace(self,formula, args, **kwargs):
return "( str.replace %s %s %s )" % (args[0], args[1], args[2])
[docs] def walk_str_substr(self,formula, args,**kwargs):
return "( str.substr %s %s %s)" % (args[0], args[1], args[2])
[docs] def walk_str_prefixof(self,formula, args,**kwargs):
return "( str.prefixof %s %s )" % (args[0], args[1])
[docs] def walk_str_suffixof(self,formula, args, **kwargs):
return "( str.suffixof %s %s )" % (args[0], args[1])
[docs] def walk_str_to_int(self,formula, args, **kwargs):
return "( str.to.int %s )" % args[0]
[docs] def walk_int_to_str(self,formula, args, **kwargs):
return "( int.to.str %s )" % args[0]
[docs] def walk_array_value(self, formula, args, **kwargs):
sym = self._new_symbol()
self.openings += 1
self.write("(let ((%s " % sym)
for _ in xrange((len(args) - 1) // 2):
self.write("(store ")
self.write("((as const %s) " % formula.get_type().as_smtlib(False))
self.write(args[0])
self.write(")")
for i, k in enumerate(args[1::2]):
self.write(" ")
self.write(k)
self.write(" ")
self.write(args[2*i + 2])
self.write(")")
self.write("))")
return sym
[docs]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