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.

diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp
index 199b8aefde5a322b04fc8fcbd574c7786a3ed081..ed3a6a19e49358b12e6df38e1e28e2b628a2877e 100644 (file)
--- 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 441786b5f07a63c25ce1dd70d70227ce9dee93af..de40eee64533eb0aaae2cfe7520bd0480557dcb7 100644 (file)
--- 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 c255bb0de8f65a13fb0639a81e2c271bd3ae2ac9..153c59717a6667385b96ef09436a6b91666b0aa0 100644 (file)
--- 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 4209bf250125459fd4c65f1c2ae1e270b285cec9..3f55de3686003e3b527f26bb0860f2de465009eb 100644 (file)
--- 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 88f617e0225ab66f68921e165e503430f5f0eff0..8ffd7c685fd788072be36b766992501f255a5ebb 100644 (file)
--- 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 9910f31152aa11969522c9f0c277dce681d81ca4..d674421987438e793f0ab195963136820bf0debf 100644 (file)
--- 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 (file)
index 0000000..28dd912
--- /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)