Fix sygus-inst when combined with bounded string quantifiers (#8500)

Strings introduces bounded quantified formulas for reasoning about extended functions. We should not process these with sygus-inst.

Fixes #8497.

diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp
index e05624eb0640c6cfad9f03e8410b560c1b54c726..b4827a2e61cecf1b46a1749315fdd755d866826d 100644 (file)
--- a/src/theory/quantifiers/sygus_inst.cpp
+++ b/src/theory/quantifiers/sygus_inst.cpp
@@ -219,7 +219,10 @@ void SygusInst::reset_round(Theory::Effort e)
   for (uint32_t i = 0; i < nasserted; ++i)
   {
     Node q = model->getAssertedQuantifier(i);
-
+    if (!shouldProcess(q))
+    {
+      continue;
+    }
     if (model->isQuantifierActive(q))
     {
       d_active_quant.insert(q);
@@ -243,6 +246,19 @@ void SygusInst::reset_round(Theory::Effort e)
   }
 }
 
+bool SygusInst::shouldProcess(Node q)
+{
+  // Note that we currently process quantified formulas that other modules
+  // e.g. CEGQI have taken full ownership over.
+  // ignore internal quantifiers
+  QuantAttributes& qattr = d_qreg.getQuantAttributes();
+  if (qattr.isQuantBounded(q))
+  {
+    return false;
+  }
+  return true;
+}
+
 void SygusInst::check(Theory::Effort e, QEffort quant_e)
 {
   Trace("sygus-inst") << "Check " << e << ", " << quant_e << std::endl;

diff --git a/src/theory/quantifiers/sygus_inst.h b/src/theory/quantifiers/sygus_inst.h
index 20b118f28789b2a0bded18a9d608315e600b41fc..b2238544b114bebce249da217ad49f487fecbc19 100644 (file)
--- a/src/theory/quantifiers/sygus_inst.h
+++ b/src/theory/quantifiers/sygus_inst.h
@@ -111,6 +111,9 @@ class SygusInst : public QuantifiersModule
    */
   bool sendEvalUnfoldLemmas(const std::vector<Node>& lemmas);
 
+  /** Return true if this module should process quantified formula q */
+  bool shouldProcess(Node q);
+
   /* Maps quantifiers to a vector of instantiation constants. */
   std::unordered_map<Node, std::vector<Node>> d_inst_constants;
 

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 4a0b75460f02203ba9e19d97b129db162a24c0b3..54676cfe9be8de37e8eab5f092dd36e1b88c1e5f 100644 (file)
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -2225,6 +2225,7 @@ set(regress_1_tests
   regress1/quantifiers/issue8410-vts-subtypes.smt2
   regress1/quantifiers/issue8456-2-syqi-ic.smt2
   regress1/quantifiers/issue8456-syqi-ic.smt2
+  regress1/quantifiers/issue8497-syqi-str-fmf.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/issue8497-syqi-str-fmf.smt2 b/test/regress/cli/regress1/quantifiers/issue8497-syqi-str-fmf.smt2
new file mode 100644 (file)
index 0000000..5178871
--- /dev/null
+++ b/test/regress/cli/regress1/quantifiers/issue8497-syqi-str-fmf.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: -q --sygus-inst
+; EXPECT: sat
+(set-logic QF_SLIA)
+(declare-fun a () String)
+(declare-fun b () String)
+(assert (> (str.indexof a b 0) 2))
+(check-sat)