Skip to content

Commit

Permalink
Merge pull request #45 from pysmt/better_solver_converters
Browse files Browse the repository at this point in the history 
Cleaned up solver encoders, removing useless assertions.
  • Loading branch information
marcogario committed Mar 13, 2015
2 parents e378631 + fd221ad commit 880ffae
Show file tree
Hide file tree
Showing 6 changed files with 30 additions and 94 deletions.
2 changes: 1 addition & 1 deletion install.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -463,7 +463,7 @@ def main():
print("export PYTHONPATH=\"$PYTHONPATH:"+ ":".join(PATHS) + "\"")

with open(os.path.join(BASE_DIR, "set_paths.sh"), "a") as fout:
fout.write("export PYTHONPATH=\"$PYTHONPATH:"+ ":".join(PATHS) + "\"")
fout.write("export PYTHONPATH=\"$PYTHONPATH:"+ ":".join(PATHS) + "\"\n")


if __name__ == "__main__":
Expand Down
21 changes: 0 additions & 21 deletions pysmt/solvers/cvc4.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -176,62 +176,47 @@ def convert(self, formula):
return self.walk(formula)

def walk_and(self, formula, args):
assert len(args) >= 2
return self.mkExpr(CVC4.AND, args)

def walk_or(self, formula, args):
assert len(args) >= 2
return self.mkExpr(CVC4.OR, args)

def walk_not(self, formula, args):
assert len(args) == 1
return self.mkExpr(CVC4.NOT, args[0])

def walk_symbol(self, formula, args):
assert len(args) == 0
if formula not in self.declared_vars:
self.declare_variable(formula)
return self.declared_vars[formula]

def walk_iff(self, formula, args):
assert len(args) == 2
return self.mkExpr(CVC4.IFF, args[0], args[1])

def walk_implies(self, formula, args):
assert len(args) == 2
return self.mkExpr(CVC4.IMPLIES, args[0], args[1])

def walk_le(self, formula, args):
assert len(args) == 2
return self.mkExpr(CVC4.LEQ, args[0], args[1])

def walk_lt(self, formula, args):
assert len(args) == 2
return self.mkExpr(CVC4.LT, args[0], args[1])

def walk_ite(self, formula, args):
assert len(args) == 3
return self.mkExpr(CVC4.ITE, *args)

def walk_real_constant(self, formula, args):
assert len(args) == 0
assert type(formula.constant_value()) == Fraction
frac = formula.constant_value()
n,d = frac.numerator, frac.denominator
return self.mkConst(CVC4.Rational(n, d))

def walk_int_constant(self, formula, args):
assert len(args) == 0
assert type(formula.constant_value()) == int
return self.mkConst(CVC4.Rational(formula.constant_value()))

def walk_bool_constant(self, formula, args):
assert len(args) == 0
assert type(formula.constant_value()) == bool
return self.cvc4_exprMgr.mkBoolConst(formula.constant_value())

def walk_exists(self, formula, args):
assert len(args) == 1
(bound_formula, var_list) = \
self._rename_bound_variables(args[0], formula.quantifier_vars())
bound_vars_list = self.mkExpr(CVC4.BOUND_VAR_LIST, var_list)
Expand All @@ -240,7 +225,6 @@ def walk_exists(self, formula, args):
bound_formula)

def walk_forall(self, formula, args):
assert len(args) == 1
(bound_formula, var_list) = \
self._rename_bound_variables(args[0], formula.quantifier_vars())
bound_vars_list = self.mkExpr(CVC4.BOUND_VAR_LIST, var_list)
Expand All @@ -249,24 +233,19 @@ def walk_forall(self, formula, args):
bound_formula)

def walk_plus(self, formula, args):
assert len(args) >= 2
res = self.mkExpr(CVC4.PLUS, args)
return res

def walk_minus(self, formula, args):
assert len(args) == 2
return self.mkExpr(CVC4.MINUS, args[0], args[1])

def walk_equals(self, formula, args):
assert len(args) == 2
return self.mkExpr(CVC4.EQUAL, args[0], args[1])

def walk_times(self, formula, args):
assert len(args) == 2
return self.mkExpr(CVC4.MULT, args[0], args[1])

def walk_toreal(self, formula, args):
assert len(args) == 1
return self.mkExpr(CVC4.TO_REAL, args[0])

def walk_function(self, formula, args):
Expand Down
21 changes: 1 addition & 20 deletions pysmt/solvers/msat.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -458,27 +458,22 @@ def walk_or(self, formula, args):
return res

def walk_not(self, formula, args):
assert len(args) == 1
return mathsat.msat_make_not(self.msat_env, args[0])

def walk_symbol(self, formula, args):
assert len(args) == 0
if formula not in self.symbol_to_decl:
self.declare_variable(formula)
decl = self.symbol_to_decl[formula]
return mathsat.msat_make_constant(self.msat_env, decl)

def walk_le(self, formula, args):
assert len(args) == 2
return mathsat.msat_make_leq(self.msat_env, args[0], args[1])

def walk_lt(self, formula, args):
assert len(args) == 2
leq = mathsat.msat_make_leq(self.msat_env, args[1], args[0])
return mathsat.msat_make_not(self.msat_env, leq)

def walk_ite(self, formula, args):
assert len(args) == 3
i = args[0]
t = args[1]
e = args[2]
Expand All @@ -494,22 +489,19 @@ def walk_ite(self, formula, args):
return mathsat.msat_make_term_ite(self.msat_env, i, t, e)

def walk_real_constant(self, formula, args):
assert len(args) == 0
assert type(formula.constant_value()) == Fraction
frac = formula.constant_value()
n,d = frac.numerator, frac.denominator
rep = str(n) + "/" + str(d)
return mathsat.msat_make_number(self.msat_env, rep)

def walk_int_constant(self, formula, args):
assert len(args) == 0
assert type(formula.constant_value()) == int or \
type(formula.constant_value()) == long
rep = str(formula.constant_value())
return mathsat.msat_make_number(self.msat_env, rep)

def walk_bool_constant(self, formula, args):
assert len(args) == 0
if formula.constant_value():
return mathsat.msat_make_true(self.msat_env)
else:
Expand All @@ -528,27 +520,17 @@ def walk_plus(self, formula, args):
return res

def walk_minus(self, formula, args):
assert len(args) == 2
n_one = mathsat.msat_make_number(self.msat_env, "-1")
n_s2 = mathsat.msat_make_times(self.msat_env, n_one, args[1])
return mathsat.msat_make_plus(self.msat_env, args[0], n_s2)

def walk_equals(self, formula, args):
assert len(args) == 2
return mathsat.msat_make_equal(self.msat_env, args[0], args[1])

def walk_iff(self, formula, args):
assert len(args) == 2
lf = formula.arg(0)
rf = formula.arg(1)

li = self.walk_implies(self.mgr.Implies(lf, rf), [args[0], args[1]])
ri = self.walk_implies(self.mgr.Implies(rf, lf), [args[1], args[0]])

return mathsat.msat_make_and(self.msat_env, li, ri)
return mathsat.msat_make_iff(self.msat_env, args[0], args[1])

def walk_implies(self, formula, args):
assert len(args) == 2
neg = self.walk_not(self.mgr.Not(formula.arg(0)), [args[0]])
return mathsat.msat_make_or(self.msat_env, neg, args[1])

Expand All @@ -563,7 +545,6 @@ def walk_function(self, formula, args):
return mathsat.msat_make_uf(self.msat_env, decl, args)

def walk_toreal(self, formula, args):
assert len(args) == 1
# In mathsat toreal is implicit
return args[0]

Expand Down
17 changes: 0 additions & 17 deletions pysmt/solvers/yices.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -215,11 +215,9 @@ def walk_or(self, formula, args):
return libyices.yices_or(len(args), arr)

def walk_not(self, formula, args):
assert len(args) == 1
return libyices.yices_not(args[0])

def walk_symbol(self, formula, args):
assert len(args) == 0
symbol_type = formula.symbol_type()
var_type = self._type_to_yices(symbol_type)
term = libyices.yices_new_uninterpreted_term(var_type)
Expand All @@ -234,57 +232,47 @@ def _bound_symbol(self, var):
return term

def walk_iff(self, formula, args):
assert len(args) == 2
return libyices.yices_iff(args[0], args[1])

def walk_implies(self, formula, args):
assert len(args) == 2
return libyices.yices_implies(args[0], args[1])

def walk_le(self, formula, args):
assert len(args) == 2
return libyices.yices_arith_leq_atom(args[0], args[1])

def walk_lt(self, formula, args):
assert len(args) == 2
return libyices.yices_arith_lt_atom(args[0], args[1])

def walk_ite(self, formula, args):
assert len(args) == 3
i, t, e = args
return libyices.yices_ite(i, t, e)

def walk_real_constant(self, formula, args):
assert len(args) == 0
assert type(formula.constant_value()) == Fraction
frac = formula.constant_value()
n,d = frac.numerator, frac.denominator
rep = str(n) + "/" + str(d)
return libyices.yices_parse_rational(String(rep))

def walk_int_constant(self, formula, args):
assert len(args) == 0
assert type(formula.constant_value()) == int or \
type(formula.constant_value()) == long
rep = str(formula.constant_value())
return libyices.yices_parse_rational(String(rep))

def walk_bool_constant(self, formula, args):
assert len(args) == 0
if formula.constant_value():
return libyices.yices_true()
else:
return libyices.yices_false()

def walk_exists(self, formula, args):
assert len(args) == 1
(bound_formula, var_list) = \
self._rename_bound_variables(args[0], formula.quantifier_vars())
arr = (libyices.term_t * len(var_list))(*var_list)
return libyices.yices_exists(len(var_list), arr, bound_formula)

def walk_forall(self, formula, args):
assert len(args) == 1
(bound_formula, var_list) = \
self._rename_bound_variables(args[0], formula.quantifier_vars())
arr = (libyices.term_t * len(var_list))(*var_list)
Expand All @@ -306,24 +294,19 @@ def _rename_bound_variables(self, formula, variables):


def walk_plus(self, formula, args):
assert len(args) >= 2
arr = (libyices.term_t * len(args))(*args)
return libyices.yices_sum(len(args), arr)

def walk_minus(self, formula, args):
assert len(args) == 2
return libyices.yices_sub(args[0], args[1])

def walk_equals(self, formula, args):
assert len(args) == 2
return libyices.yices_arith_eq_atom(args[0], args[1])

def walk_times(self, formula, args):
assert len(args) == 2
return libyices.yices_mul(args[0], args[1])

def walk_toreal(self, formula, args):
assert len(args) == 1
return args[0]

def walk_function(self, formula, args):
Expand Down

0 comments on commit 880ffae

Please sign in to comment.