From 4a388e0b0cfb872e6bb8e8024542ba20aa9f3002 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 5 Apr 2022 10:45:46 -0500 Subject: [PATCH] Make inst constant attribute robust to purification variables (#8573) Fixes #8572. Certain combinations of cegqi/sygus-inst may be solution unsound when combined with E-matching, due to using skolems that have dependencies on instantiation constants are used in instantiations. --- src/theory/quantifiers/ematching/candidate_generator.cpp | 2 +- src/theory/quantifiers/equality_query.cpp | 2 +- src/theory/quantifiers/term_tuple_enumerator.cpp | 2 +- src/theory/quantifiers/term_util.cpp | 5 ++++- src/theory/quantifiers/term_util.h | 9 ++++++++- test/regress/cli/CMakeLists.txt | 1 + .../quantifiers/issue8572-sygus-inst-ic-purify.smt2 | 5 +++++ 7 files changed, 21 insertions(+), 5 deletions(-) create mode 100644 test/regress/cli/regress1/quantifiers/issue8572-sygus-inst-ic-purify.smt2 diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp index 199b8aefd..ed3a6a19e 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.cpp +++ b/src/theory/quantifiers/ematching/candidate_generator.cpp @@ -41,7 +41,7 @@ CandidateGenerator::CandidateGenerator(QuantifiersState& qs, TermRegistry& tr) bool CandidateGenerator::isLegalCandidate( Node n ){ return d_treg.getTermDatabase()->isTermActive(n) - && (!options::cegqi() || !quantifiers::TermUtil::hasInstConstAttr(n)); + && !quantifiers::TermUtil::hasInstConstAttr(n); } CandidateGeneratorQE::CandidateGeneratorQE(QuantifiersState& qs, diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp index 441786b5f..de40eee64 100644 --- a/src/theory/quantifiers/equality_query.cpp +++ b/src/theory/quantifiers/equality_query.cpp @@ -168,7 +168,7 @@ Node EqualityQuery::getInstance(Node n, //-2 : invalid, -1 : undesired, otherwise : smaller the score, the better int32_t EqualityQuery::getRepScore(Node n, Node q, size_t index, TypeNode v_tn) { - if (options().quantifiers.cegqi && quantifiers::TermUtil::hasInstConstAttr(n)) + if (quantifiers::TermUtil::hasInstConstAttr(n)) { // reject return -2; } diff --git a/src/theory/quantifiers/term_tuple_enumerator.cpp b/src/theory/quantifiers/term_tuple_enumerator.cpp index c255bb0de..153c59717 100644 --- a/src/theory/quantifiers/term_tuple_enumerator.cpp +++ b/src/theory/quantifiers/term_tuple_enumerator.cpp @@ -469,7 +469,7 @@ size_t TermTupleEnumeratorBasic::prepareTerms(size_t variableIx) for (size_t j = 0; j < ground_terms_count; j++) { Node gt = d_tdb->getTypeGroundTerm(type_node, j); - if (!options::cegqi() || !quantifiers::TermUtil::hasInstConstAttr(gt)) + if (!quantifiers::TermUtil::hasInstConstAttr(gt)) { Node rep = d_qs.getRepresentative(gt); if (repsFound.find(rep) == repsFound.end()) diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index 4209bf250..3f55de368 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -16,6 +16,7 @@ #include "theory/quantifiers/term_util.h" #include "expr/node_algorithm.h" +#include "expr/skolem_manager.h" #include "theory/arith/arith_msum.h" #include "theory/bv/theory_bv_utils.h" #include "theory/quantifiers/term_database.h" @@ -90,7 +91,9 @@ Node TermUtil::getInstConstAttr( Node n ) { return n.getAttribute(InstConstantAttribute()); } -bool TermUtil::hasInstConstAttr( Node n ) { +bool TermUtil::hasInstConstAttr(Node n) +{ + n = SkolemManager::getOriginalForm(n); return !getInstConstAttr(n).isNull(); } diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h index 88f617e02..8ffd7c685 100644 --- a/src/theory/quantifiers/term_util.h +++ b/src/theory/quantifiers/term_util.h @@ -68,7 +68,14 @@ class TermUtil static size_t getVariableNum(Node q, Node v); static Node getInstConstAttr( Node n ); - static bool hasInstConstAttr( Node n ); + /** + * Does n (or its original form) contain instantiation constants? This method + * is used for determining when a term is ineligible for instantiation. + * + * @param n the node to check. + * @return true if n has instantiation constants. + */ + static bool hasInstConstAttr(Node n); static Node getBoundVarAttr( Node n ); static bool hasBoundVarAttr( Node n ); diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index 9910f3115..d67442198 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -2235,6 +2235,7 @@ set(regress_1_tests regress1/quantifiers/issue8497-syqi-str-fmf.smt2 regress1/quantifiers/issue8517-exp-exp.smt2 regress1/quantifiers/issue8520-cegqi-nl-cov.smt2 + regress1/quantifiers/issue8572-sygus-inst-ic-purify.smt2 regress1/quantifiers/issue993.smt2 regress1/quantifiers/javafe.ast.StmtVec.009.smt2 regress1/quantifiers/lia-witness-div-pp.smt2 diff --git a/test/regress/cli/regress1/quantifiers/issue8572-sygus-inst-ic-purify.smt2 b/test/regress/cli/regress1/quantifiers/issue8572-sygus-inst-ic-purify.smt2 new file mode 100644 index 000000000..28dd91254 --- /dev/null +++ b/test/regress/cli/regress1/quantifiers/issue8572-sygus-inst-ic-purify.smt2 @@ -0,0 +1,5 @@ +; COMMAND-LINE: --strings-exp --sygus-inst +; EXPECT: unsat +(set-logic ALL) +(assert (forall ((e String)) (= 0 (ite (str.contains (str.substr e 0 (- (str.len e) 1)) "/") 1 0)))) +(check-sat) -- 2.30.2