From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 1 Apr 2022 04:25:05 +0000 (-0500)
Subject: Fix sygus-inst when combined with bounded string quantifiers (#8500)
X-Git-Tag: cvc5-1.0.0~74
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=469de059de55ad61b4f8601d4da6020ed42e368d;p=cvc5.git

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 e05624eb0..b4827a2e6 100644
--- 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 20b118f28..b2238544b 100644
--- 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 4a0b75460..54676cfe9 100644
--- 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
index 000000000..5178871a5
--- /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)