From c0a37b03d674ca0555e01b0aa4b345df806aea7a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 30 Mar 2022 13:55:21 -0500 Subject: [PATCH] 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. --- src/theory/datatypes/theory_datatypes.cpp | 5 ++++- src/theory/quantifiers/sygus_inst.cpp | 6 +++++- test/regress/cli/CMakeLists.txt | 2 ++ .../regress1/quantifiers/issue8456-2-syqi-ic.smt2 | 5 +++++ .../cli/regress1/quantifiers/issue8456-syqi-ic.smt2 | 13 +++++++++++++ 5 files changed, 29 insertions(+), 2 deletions(-) create mode 100644 test/regress/cli/regress1/quantifiers/issue8456-2-syqi-ic.smt2 create mode 100644 test/regress/cli/regress1/quantifiers/issue8456-syqi-ic.smt2 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& types) // type is is the same as x_i, and whose value will be used to instantiate x_i std::vector evals; std::vector 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& 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& 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) -- 2.30.2