diff options
| -rw-r--r-- | src/smt/smt_engine.cpp | 6 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_instantiation.cpp | 32 | ||||
| -rw-r--r-- | test/regress/Makefile.tests | 1 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/max2-bv.sy | 26 |
4 files changed, 55 insertions, 10 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 1e8ae4033..cabe825be 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1934,6 +1934,7 @@ void SmtEngine::setDefaults() { options::ceGuidedInst.set( true ); } } + // if sygus is enabled, set the defaults for sygus if( options::ceGuidedInst() ){ //counterexample-guided instantiation for sygus if( !options::cegqiSingleInvMode.wasSetByUser() ){ @@ -1945,6 +1946,11 @@ void SmtEngine::setDefaults() { if( !options::instNoEntail.wasSetByUser() ){ options::instNoEntail.set( false ); } + if (!options::cbqiFullEffort.wasSetByUser()) + { + // should use full effort cbqi for single invocation and repair const + options::cbqiFullEffort.set(true); + } if (options::sygusRew()) { options::sygusRewSynth.set(true); diff --git a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp index b3cb98bc5..1e0b36a3c 100644 --- a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp @@ -267,20 +267,32 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) { if( !conj->needsRefinement() ){ Trace("cegqi-engine-debug") << "Do conjecture check..." << std::endl; - std::vector<Node> clems; - conj->doSingleInvCheck(clems); - if (!clems.empty()) + if (conj->isSingleInvocation()) { - d_last_inst_si = true; - for (const Node& lem : clems) + std::vector<Node> clems; + conj->doSingleInvCheck(clems); + if (!clems.empty()) { - Trace("cegqi-lemma") - << "Cegqi::Lemma : single invocation instantiation : " << lem + d_last_inst_si = true; + for (const Node& lem : clems) + { + Trace("cegqi-lemma") + << "Cegqi::Lemma : single invocation instantiation : " << lem + << std::endl; + d_quantEngine->addLemma(lem); + } + d_statistics.d_cegqi_si_lemmas += clems.size(); + Trace("cegqi-engine") << " ...try single invocation." << std::endl; + } + else + { + // This can happen for non-monotonic instantiation strategies. We + // set --cbqi-full to ensure that for most strategies (e.g. BV), we + // are using a monotonic strategy. + Trace("cegqi-warn") + << " ...FAILED to add cbqi instantiation for single invocation!" << std::endl; - d_quantEngine->addLemma(lem); } - d_statistics.d_cegqi_si_lemmas += clems.size(); - Trace("cegqi-engine") << " ...try single invocation." << std::endl; return; } diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 08f64a925..e773bf698 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1549,6 +1549,7 @@ REG1_TESTS = \ regress1/sygus/list-head-x.sy \ regress1/sygus/logiccell_help.sy \ regress1/sygus/max.sy \ + regress1/sygus/max2-bv.sy \ regress1/sygus/multi-fun-polynomial2.sy \ regress1/sygus/nflat-fwd-3.sy \ regress1/sygus/nflat-fwd.sy \ diff --git a/test/regress/regress1/sygus/max2-bv.sy b/test/regress/regress1/sygus/max2-bv.sy new file mode 100644 index 000000000..297bd9179 --- /dev/null +++ b/test/regress/regress1/sygus/max2-bv.sy @@ -0,0 +1,26 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic BV) + +(synth-fun max2 ((x (BitVec 32))(y (BitVec 32))) (BitVec 32) +) + +(declare-var x (BitVec 32)) + +(declare-var y (BitVec 32)) + +(constraint +(bvuge (max2 x y) x) +) + +(constraint +(bvuge (max2 x y) y) +) + +(constraint +(or (= x (max2 x y)) (= y (max2 x y))) +) + +(check-synth) + + |