Fixes for sygus-inst (#8448)

Fixes two issues:

Symmetry breaking was disabled after latest refactoring of sygus options. This meant that the terms considered by sygus-inst were often redundant.
The instantiation constant attribute is set on evaluation variables. This avoids model-unsoundness issues with sygus-inst, which are caused by using the evaluation variable (itself) in instantiations.
The latter issue was discovered by trying the second issue from cvc5/cvc5-projects#487 with --sygus-inst, where it incorrectly says "sat" after the fix from #8447.

Fixed #8456. Fixes #8457.

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 72573e5695050bc22b1b2783c92b9ba41720c978..8bbd179c7a5ef18c055ba89879e5216aa73b565e 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -109,7 +109,10 @@ void TheoryDatatypes::finishInit()
   // We could but don't do congruence for DT_SIZE and DT_HEIGHT_BOUND here.
   // It also could make sense in practice to do congruence for APPLY_UF, but
   // this is not done.
-  if (getQuantifiersEngine() && options().quantifiers.sygus)
+  // Enable the sygus extension if we will introduce sygus datatypes. This
+  // is the case for sygus problems and when using sygus-inst.
+  if (getQuantifiersEngine()
+      && (options().quantifiers.sygus || options().quantifiers.sygusInst))
   {
     quantifiers::TermDbSygus* tds =
         getQuantifiersEngine()->getTermDatabaseSygus();

diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp
index 84a4ddb7b4292b163fbe9dc095c5df2b93752234..8c9d0046bee60161d256870b6652a77783b25aa6 100644 (file)
--- a/src/theory/quantifiers/sygus_inst.cpp
+++ b/src/theory/quantifiers/sygus_inst.cpp
@@ -498,6 +498,7 @@ void SygusInst::registerCeLemma(Node q, std::vector<TypeNode>& types)
   // type is is the same as x_i, and whose value will be used to instantiate x_i
   std::vector<Node> evals;
   std::vector<Node> inst_constants;
+  InstConstantAttribute ica;
   for (size_t i = 0, size = types.size(); i < size; ++i)
   {
     TypeNode tn = types[i];
@@ -505,7 +506,6 @@ void SygusInst::registerCeLemma(Node q, std::vector<TypeNode>& types)
 
     /* Create the instantiation constant and set attribute accordingly. */
     Node ic = nm->mkInstConstant(tn);
-    InstConstantAttribute ica;
     ic.setAttribute(ica, q);
     Trace("sygus-inst") << "Create " << ic << " for " << var << std::endl;
 
@@ -523,6 +523,10 @@ void SygusInst::registerCeLemma(Node q, std::vector<TypeNode>& types)
     // for evaluation functions. We use the DT_SYGUS_EVAL term so that the
     // skolem construction here is deterministic and reproducible.
     Node k = sm->mkPurifySkolem(eval, "eval");
+    // Requires instantiation constant attribute as well. This ensures that
+    // other instantiation methods, e.g. E-matching do not consider this term
+    // for instantiation, as it is model-unsound to do so.
+    k.setAttribute(ica, q);
 
     inst_constants.push_back(ic);
     evals.push_back(k);

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 4f37e2e2eb5e8825f600f2c3bd1209d7d6d7b777..47d07041356290ed3cedcabb2d27b1042de2a0b5 100644 (file)
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -2214,6 +2214,8 @@ set(regress_1_tests
   regress1/quantifiers/issue8157-duplicate-conflicts.smt2
   regress1/quantifiers/issue8344-cegqi-string-witness.smt2
   regress1/quantifiers/issue8410-vts-subtypes.smt2
+  regress1/quantifiers/issue8456-2-syqi-ic.smt2
+  regress1/quantifiers/issue8456-syqi-ic.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/issue8456-2-syqi-ic.smt2 b/test/regress/cli/regress1/quantifiers/issue8456-2-syqi-ic.smt2
new file mode 100644 (file)
index 0000000..97a1008
--- /dev/null
+++ b/test/regress/cli/regress1/quantifiers/issue8456-2-syqi-ic.smt2
@@ -0,0 +1,5 @@
+; COMMAND-LINE: --sygus-inst
+; EXPECT: unsat
+(set-logic ALL)
+(assert (and (forall ((v (Array (_ BitVec 1) Bool))) (select v (_ bv0 1)))))
+(check-sat)

diff --git a/test/regress/cli/regress1/quantifiers/issue8456-syqi-ic.smt2 b/test/regress/cli/regress1/quantifiers/issue8456-syqi-ic.smt2
new file mode 100644 (file)
index 0000000..e98274b
--- /dev/null
+++ b/test/regress/cli/regress1/quantifiers/issue8456-syqi-ic.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --sygus-inst
+; EXPECT: unsat
+(set-logic ALL)
+(declare-const x Bool)
+(declare-sort I 0)
+(declare-fun e () I)
+(declare-fun ex () I)
+(declare-fun t () I)
+(declare-fun r () I)
+(assert (distinct e ex))
+(assert (forall ((xt I)) (exists ((E I)) (= xt t))))
+(assert (or x (= t r)))
+(check-sat)