From: Andrew Reynolds Date: Mon, 30 Aug 2021 19:10:27 +0000 (-0500) Subject: Fix quantifiers dynamic split module for parametric datatypes (#7085) X-Git-Tag: cvc5-1.0.0~1323 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9b89eb1c0a7c2e9b5be9b9a80e9e24473454ce52;p=cvc5.git Fix quantifiers dynamic split module for parametric datatypes (#7085) Fixes #6838. --- diff --git a/src/theory/datatypes/theory_datatypes_utils.cpp b/src/theory/datatypes/theory_datatypes_utils.cpp index 582f11c72..3b36ad2f2 100644 --- a/src/theory/datatypes/theory_datatypes_utils.cpp +++ b/src/theory/datatypes/theory_datatypes_utils.cpp @@ -28,12 +28,11 @@ namespace datatypes { namespace utils { /** get instantiate cons */ -Node getInstCons(Node n, const DType& dt, int index) +Node getInstCons(Node n, const DType& dt, size_t index) { - Assert(index >= 0 && index < (int)dt.getNumConstructors()); + Assert(index < dt.getNumConstructors()); std::vector children; NodeManager* nm = NodeManager::currentNM(); - children.push_back(dt[index].getConstructor()); TypeNode tn = n.getType(); for (unsigned i = 0, nargs = dt[index].getNumArgs(); i < nargs; i++) { @@ -41,30 +40,37 @@ Node getInstCons(Node n, const DType& dt, int index) APPLY_SELECTOR_TOTAL, dt[index].getSelectorInternal(tn, i), n); children.push_back(nc); } - Node n_ic = nm->mkNode(APPLY_CONSTRUCTOR, children); + Node n_ic = mkApplyCons(tn, dt, index, children); + Assert(n_ic.getType() == tn); + Assert(static_cast(isInstCons(n, n_ic, dt)) == index); + return n_ic; +} + +Node mkApplyCons(TypeNode tn, + const DType& dt, + size_t index, + const std::vector& children) +{ + Assert(tn.isDatatype()); + Assert(index < dt.getNumConstructors()); + Assert(dt[index].getNumArgs() == children.size()); + NodeManager* nm = NodeManager::currentNM(); + std::vector cchildren; + cchildren.push_back(dt[index].getConstructor()); + cchildren.insert(cchildren.end(), children.begin(), children.end()); if (dt.isParametric()) { // add type ascription for ambiguous constructor types - if (!n_ic.getType().isComparableTo(tn)) - { - Debug("datatypes-parametric") - << "DtInstantiate: ambiguous type for " << n_ic << ", ascribe to " - << n.getType() << std::endl; - Debug("datatypes-parametric") - << "Constructor is " << dt[index] << std::endl; - TypeNode tspec = dt[index].getSpecializedConstructorType(n.getType()); - Debug("datatypes-parametric") - << "Type specification is " << tspec << std::endl; - children[0] = nm->mkNode(APPLY_TYPE_ASCRIPTION, - nm->mkConst(AscriptionType(tspec)), - children[0]); - n_ic = nm->mkNode(APPLY_CONSTRUCTOR, children); - Assert(n_ic.getType() == tn); - } + Debug("datatypes-parametric") + << "Constructor is " << dt[index] << std::endl; + TypeNode tspec = dt[index].getSpecializedConstructorType(tn); + Debug("datatypes-parametric") + << "Type specification is " << tspec << std::endl; + cchildren[0] = nm->mkNode(APPLY_TYPE_ASCRIPTION, + nm->mkConst(AscriptionType(tspec)), + cchildren[0]); } - Assert(isInstCons(n, n_ic, dt) == index); - // n_ic = Rewriter::rewrite( n_ic ); - return n_ic; + return nm->mkNode(APPLY_CONSTRUCTOR, cchildren); } int isInstCons(Node t, Node n, const DType& dt) diff --git a/src/theory/datatypes/theory_datatypes_utils.h b/src/theory/datatypes/theory_datatypes_utils.h index 705e867b9..1a6e6619b 100644 --- a/src/theory/datatypes/theory_datatypes_utils.h +++ b/src/theory/datatypes/theory_datatypes_utils.h @@ -34,7 +34,17 @@ namespace utils { * This returns the term C( sel^{C,1}( n ), ..., sel^{C,m}( n ) ), * where C is the index^{th} constructor of datatype dt. */ -Node getInstCons(Node n, const DType& dt, int index); +Node getInstCons(Node n, const DType& dt, size_t index); +/** + * Apply constructor, taking into account whether the datatype is parametric. + * + * Return the index^th constructor of dt applied to children, where tn is the + * datatype type for dt, instantiated if dt is parametric. + */ +Node mkApplyCons(TypeNode tn, + const DType& dt, + size_t index, + const std::vector& children); /** is instantiation cons * * If this method returns a value >=0, then that value, call it index, diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp index cc2525b78..941b94d23 100644 --- a/src/theory/quantifiers/quant_split.cpp +++ b/src/theory/quantifiers/quant_split.cpp @@ -17,9 +17,10 @@ #include "expr/dtype.h" #include "expr/dtype_cons.h" -#include "theory/quantifiers/term_database.h" -#include "theory/quantifiers/first_order_model.h" #include "options/quantifiers_options.h" +#include "theory/datatypes/theory_datatypes_utils.h" +#include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/term_database.h" using namespace cvc5::kind; @@ -164,17 +165,18 @@ void QuantDSplit::check(Theory::Effort e, QEffort quant_e) for (unsigned j = 0, ncons = dt.getNumConstructors(); j < ncons; j++) { std::vector vars; + TypeNode dtjtn = dt[j].getSpecializedConstructorType(tn); + Assert(dtjtn.getNumChildren() == dt[j].getNumArgs() + 1); for (unsigned k = 0, nargs = dt[j].getNumArgs(); k < nargs; k++) { - TypeNode tns = dt[j][k].getRangeType(); + TypeNode tns = dtjtn[k]; Node v = nm->mkBoundVar(tns); vars.push_back(v); } std::vector bvs_cmb; bvs_cmb.insert(bvs_cmb.end(), bvs.begin(), bvs.end()); bvs_cmb.insert(bvs_cmb.end(), vars.begin(), vars.end()); - vars.insert(vars.begin(), dt[j].getConstructor()); - Node c = nm->mkNode(kind::APPLY_CONSTRUCTOR, vars); + Node c = datatypes::utils::mkApplyCons(tn, dt, j, vars); TNode ct = c; Node body = q[1].substitute(svar, ct); if (!bvs_cmb.empty()) diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index ec6d04c1d..dca8860fd 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -911,6 +911,7 @@ set(regress_0_tests regress0/quantifiers/issue5645-dt-cm-spurious.smt2 regress0/quantifiers/issue5693-prenex.smt2 regress0/quantifiers/issue6603-dt-bool-cegqi.smt2 + regress0/quantifiers/issue6838-qpdt.smt2 regress0/quantifiers/issue6996-trivial-elim.smt2 regress0/quantifiers/issue6999-deq-elim.smt2 regress0/quantifiers/lra-triv-gn.smt2 diff --git a/test/regress/regress0/quantifiers/issue6838-qpdt.smt2 b/test/regress/regress0/quantifiers/issue6838-qpdt.smt2 new file mode 100644 index 000000000..8aad3c708 --- /dev/null +++ b/test/regress/regress0/quantifiers/issue6838-qpdt.smt2 @@ -0,0 +1,5 @@ +(set-logic ALL) +(set-info :status unsat) +(declare-datatype Box (par (A) ((box (unbox A))))) +(assert (forall ((xy (Box Bool))) (unbox xy))) +(check-sat)