From 2523e3324a8d19ef3fa326045715055f7089d6e8 Mon Sep 17 00:00:00 2001 From: Makai Mann Date: Tue, 18 Dec 2018 14:01:56 -0800 Subject: [PATCH 1/6] Handle ARRAY_VALUE for CVC4 --- pysmt/solvers/cvc4.py | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/pysmt/solvers/cvc4.py b/pysmt/solvers/cvc4.py index 0d2e8e722..3c2e436ac 100644 --- a/pysmt/solvers/cvc4.py +++ b/pysmt/solvers/cvc4.py @@ -339,6 +339,13 @@ def walk_array_store(self, formula, args, **kwargs): def walk_array_select(self, formula, args, **kwargs): return self.mkExpr(CVC4.SELECT, args[0], args[1]) + def walk_array_value(self, formula, args, **kwargs): + arr_type = self.env.stc.get_type(formula) + rval = self.mkConst(CVC4.ArrayStoreAll(self._type_to_cvc4(arr_type), args[0])) + for i, c in enumerate(args[1::2]): + rval = self.mkExpr(CVC4.STORE, rval, c, args[(i*2)+2]) + return rval + def walk_minus(self, formula, args, **kwargs): return self.mkExpr(CVC4.MINUS, args[0], args[1]) From 461a7d3c7f2b5a7233bf0bc0255bda8714ca869a Mon Sep 17 00:00:00 2001 From: Makai Mann Date: Wed, 26 Dec 2018 09:23:23 -0800 Subject: [PATCH 2/6] Mark CVC4 for const array support --- pysmt/solvers/cvc4.py | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/pysmt/solvers/cvc4.py b/pysmt/solvers/cvc4.py index 3c2e436ac..1799c95c5 100644 --- a/pysmt/solvers/cvc4.py +++ b/pysmt/solvers/cvc4.py @@ -27,7 +27,7 @@ raise SolverAPINotFound import pysmt.typing as types -from pysmt.logics import PYSMT_LOGICS, ARRAYS_CONST_LOGICS +from pysmt.logics import PYSMT_LOGICS from pysmt.solvers.solver import Solver, Converter, SolverOptions from pysmt.exceptions import (SolverReturnedUnknownResultError, @@ -79,7 +79,6 @@ def __call__(self, solver): class CVC4Solver(Solver, SmtLibBasicSolver, SmtLibIgnoreMixin): LOGICS = PYSMT_LOGICS -\ - ARRAYS_CONST_LOGICS -\ set(l for l in PYSMT_LOGICS if not l.theory.linear) OptionsClass = CVC4Options From 545e1b5f101f718c40e54bff735f02c9f5cf5669 Mon Sep 17 00:00:00 2001 From: Makai Mann Date: Fri, 28 Dec 2018 11:08:03 -0800 Subject: [PATCH 3/6] Clean logic name -- not sure this is the best solution and still fails tests because of other issue --- pysmt/solvers/cvc4.py | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/pysmt/solvers/cvc4.py b/pysmt/solvers/cvc4.py index 1799c95c5..25d16ecfd 100644 --- a/pysmt/solvers/cvc4.py +++ b/pysmt/solvers/cvc4.py @@ -112,7 +112,9 @@ def reset_assertions(self): self.cvc4 = CVC4.SmtEngine(self.em); self.cvc4.thisown=1 self.options(self) self.declarations = set() - self.cvc4.setLogic(self.logic_name) + # remove extra characters from logic_name + logic = self.logic_name.replace("*", "") + self.cvc4.setLogic(logic) def declare_variable(self, var): raise NotImplementedError From f3b804b16857b821a0801c3d742c8de8a08b1b44 Mon Sep 17 00:00:00 2001 From: Makai Mann Date: Thu, 3 Jan 2019 22:38:39 -0800 Subject: [PATCH 4/6] Run arrays_const tests for cvc4 --- pysmt/test/test_solving.py | 1 - 1 file changed, 1 deletion(-) diff --git a/pysmt/test/test_solving.py b/pysmt/test/test_solving.py index 6016e4cf6..35633ba67 100644 --- a/pysmt/test/test_solving.py +++ b/pysmt/test/test_solving.py @@ -171,7 +171,6 @@ def test_examples_msat(self): def test_examples_cvc4(self): for (f, validity, satisfiability, logic) in get_example_formulae(): if not logic.theory.linear: continue - if logic.theory.arrays_const: continue try: v = is_valid(f, solver_name='cvc4', logic=logic) s = is_sat(f, solver_name='cvc4', logic=logic) From a3db7ec588bf7723fcc5832ce2f0276b088fff82 Mon Sep 17 00:00:00 2001 From: Makai Mann Date: Thu, 3 Jan 2019 18:51:24 -0800 Subject: [PATCH 5/6] Handle CVC4 arrays correctly in back --- force.rebuild | 0 pysmt/solvers/cvc4.py | 40 +++++++++++++++++++++++++++++++++++----- 2 files changed, 35 insertions(+), 5 deletions(-) create mode 100644 force.rebuild diff --git a/force.rebuild b/force.rebuild new file mode 100644 index 000000000..e69de29bb diff --git a/pysmt/solvers/cvc4.py b/pysmt/solvers/cvc4.py index 25d16ecfd..499dcdcf5 100644 --- a/pysmt/solvers/cvc4.py +++ b/pysmt/solvers/cvc4.py @@ -253,11 +253,7 @@ def back(self, expr): v = expr.getConstString() res = self.mgr.String(v.toString()) elif expr.getType().isArray(): - const_ = expr.getConstArrayStoreAll() - array_type = self._cvc4_type_to_type(const_.getType()) - base_value = self.back(const_.getExpr()) - res = self.mgr.Array(array_type.index_type, - base_value) + res = self.__arrays_back(expr) else: raise PysmtTypeError("Unsupported constant type:", expr.getType().toString()) @@ -266,6 +262,40 @@ def back(self, expr): return res + def __arrays_back(self, arr_expr): + ''' + Helper function to take a CVC4 array and make an Array + ''' + assert arr_expr.getType().isArray(), "Expecting a CVC4 array" + visit = [arr_expr] + visited = set() + cache = dict() + while visit: + expr = visit.pop() + if expr not in visited: + visit.append(expr) + visited.add(expr) + for c in expr.getChildren(): + visit.append(c) + else: + if expr.getType().isArray(): + if expr.getNumChildren() == 3: + children = expr.getChildren() + cache[expr.getId()] = self.mgr.Store(cache[children[0].getId()], + cache[children[1].getId()], + cache[children[2].getId()]) + else: + const_ = expr.getConstArrayStoreAll() + array_type = self._cvc4_type_to_type(const_.getType()) + base_value = self.back(const_.getExpr()) + cache[expr.getId()] = self.mgr.Array(array_type.index_type, + base_value) + else: + cache[expr.getId()] = self.back(expr) + + return cache[arr_expr.getId()] + + @catch_conversion_error def convert(self, formula): return self.walk(formula) From e19b1a4e50af1b73fd76f447c198322d904e3d25 Mon Sep 17 00:00:00 2001 From: Makai Mann Date: Mon, 1 Apr 2019 07:46:28 -0700 Subject: [PATCH 6/6] Incorporate feedback on __arrays_back --- pysmt/solvers/cvc4.py | 29 ++++++++++++++++------------- 1 file changed, 16 insertions(+), 13 deletions(-) diff --git a/pysmt/solvers/cvc4.py b/pysmt/solvers/cvc4.py index 499dcdcf5..e1ddc7998 100644 --- a/pysmt/solvers/cvc4.py +++ b/pysmt/solvers/cvc4.py @@ -267,33 +267,36 @@ def __arrays_back(self, arr_expr): Helper function to take a CVC4 array and make an Array ''' assert arr_expr.getType().isArray(), "Expecting a CVC4 array" - visit = [arr_expr] + to_visit = [arr_expr] visited = set() - cache = dict() - while visit: - expr = visit.pop() + pysmt_expr = dict() + while to_visit: + expr = to_visit.pop() if expr not in visited: - visit.append(expr) + to_visit.append(expr) visited.add(expr) for c in expr.getChildren(): - visit.append(c) + to_visit.append(c) else: if expr.getType().isArray(): if expr.getNumChildren() == 3: children = expr.getChildren() - cache[expr.getId()] = self.mgr.Store(cache[children[0].getId()], - cache[children[1].getId()], - cache[children[2].getId()]) + pysmt_expr[expr.getId()] = self.mgr.Store(pysmt_expr[children[0].getId()], + pysmt_expr[children[1].getId()], + pysmt_expr[children[2].getId()]) else: + # CVC4 stores arrays as a sequence of stores on a StoreAll node + # the StoreAll node keeps a constant of the element type at every index + # this is base_value below const_ = expr.getConstArrayStoreAll() array_type = self._cvc4_type_to_type(const_.getType()) base_value = self.back(const_.getExpr()) - cache[expr.getId()] = self.mgr.Array(array_type.index_type, - base_value) + pysmt_expr[expr.getId()] = self.mgr.Array(array_type.index_type, + base_value) else: - cache[expr.getId()] = self.back(expr) + pysmt_expr[expr.getId()] = self.back(expr) - return cache[arr_expr.getId()] + return pysmt_expr[arr_expr.getId()] @catch_conversion_error