From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 31 Mar 2022 00:49:33 +0000 (-0500)
Subject: Fix case of Boolean skolem for ground term E-matching (#8447)
X-Git-Tag: cvc5-1.0.0~110
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bc25c9c4408616b905acec8d1868506a1f425e68;p=cvc5.git

Fix case of Boolean skolem for ground term E-matching (#8447)

Work towards fixing the second issue on cvc5/cvc5-projects#487, which now gives the same error as #8347.
---

diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index 5f87a5ac7..ef9a23f84 100644
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -145,8 +145,12 @@ uint64_t Trigger::addInstantiations()
     {
       if (!ee->hasTerm(gt))
       {
+        SkolemManager::SkolemFlags flags =
+            gt.getType().isBoolean() ? SkolemManager::SKOLEM_BOOL_TERM_VAR
+                                     : SkolemManager::SKOLEM_DEFAULT;
         SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
-        Node k = sm->mkPurifySkolem(gt, "gt");
+        Node k = sm->mkPurifySkolem(
+            gt, "gt", "introduced for ground subterms of triggers", flags);
         Node eq = k.eqNode(gt);
         Trace("trigger-gt-lemma")
             << "Trigger: ground term purify lemma: " << eq << std::endl;
diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp
index 8c9d0046b..e05624eb0 100644
--- a/src/theory/quantifiers/sygus_inst.cpp
+++ b/src/theory/quantifiers/sygus_inst.cpp
@@ -522,7 +522,11 @@ void SygusInst::registerCeLemma(Node q, std::vector<TypeNode>& types)
     // evaluation function, since we are not using the builtin support
     // 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");
+    SkolemManager::SkolemFlags flags = eval.getType().isBoolean()
+                                           ? SkolemManager::SKOLEM_BOOL_TERM_VAR
+                                           : SkolemManager::SKOLEM_DEFAULT;
+    Node k = sm->mkPurifySkolem(
+        eval, "eval", "evaluation variable for sygus-inst", flags);
     // 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.
diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 327a815c6..3374c2388 100644
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -1049,6 +1049,7 @@ set(regress_0_tests
   regress0/quantifiers/issue8001-mem-leak.smt2
   regress0/quantifiers/issue8159-3-qext-nterm.smt2
   regress0/quantifiers/issue8227-subs-shadow.smt2
+  regress0/quantifiers/issue8466-syqi-bool.smt2 
   regress0/quantifiers/lra-triv-gn.smt2
   regress0/quantifiers/macro-back-subs-sat.smt2
   regress0/quantifiers/macros-int-real.smt2
diff --git a/test/regress/cli/regress0/quantifiers/issue8466-syqi-bool.smt2 b/test/regress/cli/regress0/quantifiers/issue8466-syqi-bool.smt2
new file mode 100644
index 000000000..544fb479c
--- /dev/null
+++ b/test/regress/cli/regress0/quantifiers/issue8466-syqi-bool.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: -q --sygus-inst
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun a (Bool) Bool)
+(assert (forall ((b Bool)) (= (a b) (not b))))
+(check-sat)