From 053ea68e4f102f781f2f4e53e3202b61e77a5f1b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 1 Apr 2022 20:27:01 -0500 Subject: [PATCH] Require that used model values are constant in CEGQI (#8528) Fixes #8520. --- .../quantifiers/cegqi/ceg_instantiator.cpp | 30 +++++++++++-------- test/regress/cli/CMakeLists.txt | 1 + .../quantifiers/issue8520-cegqi-nl-cov.smt2 | 7 +++++ 3 files changed, 26 insertions(+), 12 deletions(-) create mode 100644 test/regress/cli/regress1/quantifiers/issue8520-cegqi-nl-cov.smt2 diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index f10e59540..50623285d 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -643,25 +643,31 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i) // - the instantiator uses model values at this effort or // if we are solving for a subfield of a datatype (is_sv), and // - the instantiator allows model values. + // Furthermore, we only permit the value if it is constant, since the model + // may contain internal-only expressions, e.g. RANs. if ((options().quantifiers.cegqiMultiInst || !hasTriedInstantiation(pv)) && (vinst->useModelValue(this, sf, pv, d_effort) || is_sv) && vinst->allowModelValue(this, sf, pv, d_effort)) { Node mv = getModelValue( pv ); - TermProperties pv_prop_m; - Trace("cegqi-inst-debug") << "[4] " << i << "...try model value " << mv << std::endl; - d_curr_iphase[pv] = CEG_INST_PHASE_MVALUE; - CegInstEffort prev = d_effort; - if (d_effort < CEG_INST_EFFORT_STANDARD_MV) + if (mv.isConst()) { - // update the effort level to indicate we have used a model value - d_effort = CEG_INST_EFFORT_STANDARD_MV; - } - if (constructInstantiationInc(pv, mv, pv_prop_m, sf)) - { - return true; + TermProperties pv_prop_m; + Trace("cegqi-inst-debug") + << "[4] " << i << "...try model value " << mv << std::endl; + d_curr_iphase[pv] = CEG_INST_PHASE_MVALUE; + CegInstEffort prev = d_effort; + if (d_effort < CEG_INST_EFFORT_STANDARD_MV) + { + // update the effort level to indicate we have used a model value + d_effort = CEG_INST_EFFORT_STANDARD_MV; + } + if (constructInstantiationInc(pv, mv, pv_prop_m, sf)) + { + return true; + } + d_effort = prev; } - d_effort = prev; } Trace("cegqi-inst-debug") << "[No instantiation found for " << pv << "]" << std::endl; diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index f06d6a913..8fda24a13 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -2229,6 +2229,7 @@ set(regress_1_tests regress1/quantifiers/issue8456-2-syqi-ic.smt2 regress1/quantifiers/issue8456-syqi-ic.smt2 regress1/quantifiers/issue8497-syqi-str-fmf.smt2 + regress1/quantifiers/issue8520-cegqi-nl-cov.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/issue8520-cegqi-nl-cov.smt2 b/test/regress/cli/regress1/quantifiers/issue8520-cegqi-nl-cov.smt2 new file mode 100644 index 000000000..561e03d77 --- /dev/null +++ b/test/regress/cli/regress1/quantifiers/issue8520-cegqi-nl-cov.smt2 @@ -0,0 +1,7 @@ +; REQUIRES: poly +; COMMAND-LINE: --nl-cov +; EXPECT: unknown +(set-logic ALL) +(declare-fun e () Real) +(assert (forall ((x Real)) (distinct (* e e) (+ 1 (* x x (- 1)))))) +(check-sat) -- 2.30.2