From bc25c9c4408616b905acec8d1868506a1f425e68 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 30 Mar 2022 19:49:33 -0500 Subject: [PATCH] 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. --- src/theory/quantifiers/ematching/trigger.cpp | 6 +++++- src/theory/quantifiers/sygus_inst.cpp | 6 +++++- test/regress/cli/CMakeLists.txt | 1 + .../cli/regress0/quantifiers/issue8466-syqi-bool.smt2 | 6 ++++++ 4 files changed, 17 insertions(+), 2 deletions(-) create mode 100644 test/regress/cli/regress0/quantifiers/issue8466-syqi-bool.smt2 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& 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) -- 2.30.2