From 0524281144b562fea63adf10bc3f5d6f75883296 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 29 Nov 2017 18:17:16 -0600 Subject: [PATCH] Minor improvements and changes to defaults for cbqi bv (#1406) This makes it so that --cbqi-bv tries at most 2 instantiations per quantified formula (one based on inversions when applicable, one based on model values). This makes it so that we do not have exponential run time in the worst case. This helps significantly for psyco benchmarks which have many quantified variables. Enables --cbqi-bv by default and changes the default inequality mode to eq-boundary (which is the best performer overall), also enables extract removal by default Allows cbqiNestedQE to be used in the BV logic. Adds an option --cbqi-full which indicates whether we should try model value instantiations for bit-vectors (by default, this is done only for the pure BV logic). --- src/options/quantifiers_options | 8 ++++--- src/smt/smt_engine.cpp | 15 +++++++++++-- src/theory/quantifiers/ceg_instantiator.cpp | 10 ++++----- src/theory/quantifiers/ceg_instantiator.h | 2 +- src/theory/quantifiers/ceg_t_instantiator.cpp | 21 +++++++++++++++++-- src/theory/quantifiers/ceg_t_instantiator.h | 12 +++++++---- 6 files changed, 50 insertions(+), 18 deletions(-) diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 1a4275d77..4a7a9e8a7 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -299,6 +299,8 @@ option sygusStream --sygus-stream bool :default false # CEGQI applied to general quantified formulas option cbqi --cbqi bool :read-write :default false turns on counterexample-based quantifier instantiation +option cbqiFullEffort --cbqi-full bool :read-write :default false + turns on full effort counterexample-based quantifier instantiation, which may resort to model-value instantiation option recurseCbqi --cbqi-recurse bool :default true turns on recursive counterexample-based quantifier instantiation option cbqiSat --cbqi-sat bool :read-write :default true @@ -339,13 +341,13 @@ option quantEprMatching --quant-epr-match bool :default true use matching heuristics for EPR instantiation # CEGQI for BV -option cbqiBv --cbqi-bv bool :read-write :default false +option cbqiBv --cbqi-bv bool :read-write :default true use word-level inversion approach for counterexample-guided quantifier instantiation for bit-vectors option cbqiBvInterleaveValue --cbqi-bv-interleave-value bool :read-write :default false interleave model value instantiation with word-level inversion approach -option cbqiBvIneqMode --cbqi-bv-ineq=MODE CVC4::theory::quantifiers::CbqiBvIneqMode :read-write :default CVC4::theory::quantifiers::CBQI_BV_INEQ_EQ_SLACK :include "options/quantifiers_modes.h" :handler stringToCbqiBvIneqMode +option cbqiBvIneqMode --cbqi-bv-ineq=MODE CVC4::theory::quantifiers::CbqiBvIneqMode :read-write :default CVC4::theory::quantifiers::CBQI_BV_INEQ_EQ_BOUNDARY :include "options/quantifiers_modes.h" :handler stringToCbqiBvIneqMode choose mode for handling bit-vector inequalities with counterexample-guided instantiation -option cbqiBvRmExtract --cbqi-bv-rm-extract bool :read-write :default false +option cbqiBvRmExtract --cbqi-bv-rm-extract bool :read-write :default true replaces extract terms with variables for counterexample-guided instantiation for bit-vectors ### local theory extensions options diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 65dae6b8f..3a0cb297e 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1912,6 +1912,14 @@ void SmtEngine::setDefaults() { if( !options::cbqi.wasSetByUser() ){ options::cbqi.set( true ); } + // check whether we should apply full cbqi + if (d_logic.isPure(THEORY_BV)) + { + if (!options::cbqiFullEffort.wasSetByUser()) + { + options::cbqiFullEffort.set(true); + } + } } if( options::cbqi() ){ //must rewrite divk @@ -1931,8 +1939,11 @@ void SmtEngine::setDefaults() { options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL ); } }else{ - //only supported in pure arithmetic - options::cbqiNestedQE.set(false); + // only supported in pure arithmetic or pure BV + if (d_logic.isPure(THEORY_BV)) + { + options::cbqiNestedQE.set(false); + } } } //implied options... diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index 15bfbe9f9..cf2c51ec1 100644 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -460,11 +460,9 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i) } //[4] resort to using value in model. We do so if: - // - we are in a higher effort than CEG_INST_EFFORT_STANDARD, - // - if the variable is Boolean, or - // - if we are solving for a subfield of a datatype. - bool use_model_value = vinst->useModelValue(this, sf, pv, d_effort); - if ((d_effort > CEG_INST_EFFORT_STANDARD || use_model_value || is_cv) + // - if the instantiator uses model values at this effort, or + // - if we are solving for a subfield of a datatype (is_cv). + if ((vinst->useModelValue(this, sf, pv, d_effort) || is_cv) && vinst->allowModelValue(this, sf, pv, d_effort)) { #ifdef CVC4_ASSERTIONS @@ -478,7 +476,7 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i) Trace("cbqi-inst-debug") << "[4] " << i << "...try model value " << mv << std::endl; d_curr_iphase[pv] = CEG_INST_PHASE_MVALUE; CegInstEffort prev = d_effort; - if (!use_model_value) + 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; diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h index ab9c7ea05..126f0325f 100644 --- a/src/theory/quantifiers/ceg_instantiator.h +++ b/src/theory/quantifiers/ceg_instantiator.h @@ -691,7 +691,7 @@ public: Node pv, CegInstEffort effort) { - return false; + return effort > CEG_INST_EFFORT_STANDARD; } /** do we allow the model value as instantiation for pv? */ virtual bool allowModelValue(CegInstantiator* ci, diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp index 674f7c17e..4570d03c3 100644 --- a/src/theory/quantifiers/ceg_t_instantiator.cpp +++ b/src/theory/quantifiers/ceg_t_instantiator.cpp @@ -934,8 +934,9 @@ class CegInstantiatorBvInverterQuery : public BvInverterQuery CegInstantiator * d_ci; }; - -BvInstantiator::BvInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){ +BvInstantiator::BvInstantiator(QuantifiersEngine* qe, TypeNode tn) + : Instantiator(qe, tn), d_tried_assertion_inst(false) +{ // get the global inverter utility // this must be global since we need to: // * process Skolem functions properly across multiple variables within the same quantifier @@ -958,6 +959,7 @@ void BvInstantiator::reset(CegInstantiator* ci, d_inst_id_to_alit.clear(); d_var_to_curr_inst_id.clear(); d_alit_to_model_slack.clear(); + d_tried_assertion_inst = false; } void BvInstantiator::processLiteral(CegInstantiator* ci, @@ -1001,6 +1003,11 @@ Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci, Node lit, CegInstEffort effort) { + if (effort == CEG_INST_EFFORT_FULL) + { + // always use model values at full effort + return Node::null(); + } Node atom = lit.getKind() == NOT ? lit[0] : lit; bool pol = lit.getKind() != NOT; Kind k = atom.getKind(); @@ -1113,6 +1120,15 @@ bool BvInstantiator::processAssertion(CegInstantiator* ci, return false; } +bool BvInstantiator::useModelValue(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) +{ + return !d_tried_assertion_inst + && (effort < CEG_INST_EFFORT_FULL || options::cbqiFullEffort()); +} + bool BvInstantiator::processAssertions(CegInstantiator* ci, SolvedForm& sf, Node pv, @@ -1200,6 +1216,7 @@ bool BvInstantiator::processAssertions(CegInstantiator* ci, Trace("cegqi-bv") << "*** try " << pv << " -> " << inst_term << std::endl; d_var_to_curr_inst_id[pv] = inst_id; + d_tried_assertion_inst = true; if (ci->constructInstantiationInc( pv, inst_term, pv_prop_bv, sf, revertOnSuccess)) { diff --git a/src/theory/quantifiers/ceg_t_instantiator.h b/src/theory/quantifiers/ceg_t_instantiator.h index 4fb954d44..c2864acc5 100644 --- a/src/theory/quantifiers/ceg_t_instantiator.h +++ b/src/theory/quantifiers/ceg_t_instantiator.h @@ -214,13 +214,15 @@ class BvInstantiator : public Instantiator { SolvedForm& sf, Node pv, CegInstEffort effort) override; + /** use model value + * + * We allow model values if we have not already tried an assertion, + * and only at levels below full if cbqiFullEffort is false. + */ virtual bool useModelValue(CegInstantiator* ci, SolvedForm& sf, Node pv, - CegInstEffort effort) override - { - return true; - } + CegInstEffort effort) override; virtual std::string identify() const { return "Bv"; } private: // point to the bv inverter class @@ -235,6 +237,8 @@ class BvInstantiator : public Instantiator { std::unordered_map< Node, unsigned, NodeHashFunction > d_var_to_curr_inst_id; /** the amount of slack we added for asserted literals */ std::unordered_map d_alit_to_model_slack; + /** whether we have tried an instantiation based on assertion in this round */ + bool d_tried_assertion_inst; /** rewrite assertion for solve pv * returns a literal that is equivalent to lit that leads to best solved form for pv */ -- 2.30.2