From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 30 Mar 2022 18:55:21 +0000 (-0500)
Subject: Fixes for sygus-inst (#8448)
X-Git-Tag: cvc5-1.0.0~120
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c0a37b03d674ca0555e01b0aa4b345df806aea7a;p=cvc5.git

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 72573e569..8bbd179c7 100644
--- 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 84a4ddb7b..8c9d0046b 100644
--- 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 4f37e2e2e..47d070413 100644
--- 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
index 000000000..97a10086a
--- /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
index 000000000..e98274be5
--- /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)