diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-10-14 11:14:02 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-14 16:14:02 +0000 |
| commit | 861dba0caea6c8bfa54bca58749323c4dbcfb282 (patch) | |
| tree | 68e91fdaa92312ffb3897a96e133a47e1936a751 | |
| parent | 588fb874c95005f1d379073a750b88a6ba5ee89a (diff) | |
Fix quantifiers variable elimination for parametric datatypes (#7358)
Fixes #7353.
| -rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 20 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/quantifiers/issue7353-var-elim-par-dt.smt2 | 9 |
3 files changed, 27 insertions, 3 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 7c7c7aade..52e90e26e 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/quantifiers_rewriter.h" +#include "expr/ascription_type.h" #include "expr/bound_var_manager.h" #include "expr/dtype.h" #include "expr/dtype_cons.h" @@ -895,12 +896,25 @@ bool QuantifiersRewriter::getVarElimLit(Node body, const DType& dt = datatypes::utils::datatypeOf(tester); const DTypeConstructor& c = dt[index]; std::vector<Node> newChildren; - newChildren.push_back(c.getConstructor()); + Node cons = c.getConstructor(); + TypeNode tspec; + // take into account if parametric + if (dt.isParametric()) + { + tspec = c.getSpecializedConstructorType(lit[0].getType()); + cons = nm->mkNode( + APPLY_TYPE_ASCRIPTION, nm->mkConst(AscriptionType(tspec)), cons); + } + else + { + tspec = cons.getType(); + } + newChildren.push_back(cons); std::vector<Node> newVars; BoundVarManager* bvm = nm->getBoundVarManager(); - for (unsigned j = 0, nargs = c.getNumArgs(); j < nargs; j++) + for (size_t j = 0, nargs = c.getNumArgs(); j < nargs; j++) { - TypeNode tn = c[j].getRangeType(); + TypeNode tn = tspec[j]; Node rn = nm->mkConst(Rational(j)); Node cacheVal = BoundVarManager::getCacheValue(body, lit, rn); Node v = bvm->mkBoundVar<QRewDtExpandAttribute>(cacheVal, tn); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 907dc22d1..79a493a1f 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -921,6 +921,7 @@ set(regress_0_tests regress0/quantifiers/issue6838-qpdt.smt2 regress0/quantifiers/issue6996-trivial-elim.smt2 regress0/quantifiers/issue6999-deq-elim.smt2 + regress0/quantifiers/issue7353-var-elim-par-dt.smt2 regress0/quantifiers/lra-triv-gn.smt2 regress0/quantifiers/macro-back-subs-sat.smt2 regress0/quantifiers/macros-int-real.smt2 diff --git a/test/regress/regress0/quantifiers/issue7353-var-elim-par-dt.smt2 b/test/regress/regress0/quantifiers/issue7353-var-elim-par-dt.smt2 new file mode 100644 index 000000000..8c9d9eb66 --- /dev/null +++ b/test/regress/regress0/quantifiers/issue7353-var-elim-par-dt.smt2 @@ -0,0 +1,9 @@ +(set-logic ALL) +(set-info :status sat) +(declare-datatype Option (par (T) ((none) (some (extractSome T))))) +(assert + (forall ((x (Option Int))) + (=> (and ((_ is some) x) + (= (extractSome x) 0)) + (= x (some 0))))) +(check-sat) |