diff options
| -rw-r--r-- | src/theory/quantifiers/ceg_instantiator.cpp | 25 | ||||
| -rw-r--r-- | src/theory/quantifiers/ceg_instantiator.h | 50 | ||||
| -rw-r--r-- | src/theory/quantifiers/ceg_t_instantiator.cpp | 107 | ||||
| -rw-r--r-- | src/theory/quantifiers/ceg_t_instantiator.h | 34 | ||||
| -rw-r--r-- | test/regress/regress0/quantifiers/Makefile.am | 7 | ||||
| -rw-r--r-- | test/regress/regress0/quantifiers/qbv-inequality2.smt2 | 11 | ||||
| -rw-r--r-- | test/regress/regress0/quantifiers/qbv-multi-lit-uge.smt2 | 11 |
7 files changed, 200 insertions, 45 deletions
diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index b0a4da2af..02b2d3a1b 100644 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -283,7 +283,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e //[4] directly look at assertions if( vinst->hasProcessAssertion( this, sf, pv, effort ) ){ Trace("cbqi-inst-debug") << "[4] try based on assertions." << std::endl; - std::vector< Node > lits; + std::unordered_set< Node, NodeHashFunction > lits; //unsigned rmax = Theory::theoryOf( pv )==Theory::theoryOf( pv.getType() ) ? 1 : 2; for( unsigned r=0; r<2; r++ ){ TheoryId tid = r==0 ? Theory::theoryOf( pvtn ) : THEORY_UF; @@ -292,18 +292,25 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e if( ita!=d_curr_asserts.end() ){ for (unsigned j = 0; j<ita->second.size(); j++) { Node lit = ita->second[j]; - if( std::find( lits.begin(), lits.end(), lit )==lits.end() ){ - lits.push_back( lit ); - if( vinst->hasProcessAssertion( this, sf, pv, lit, effort ) ){ - Trace("cbqi-inst-debug2") << " look at " << lit << std::endl; + if( lits.find(lit)==lits.end() ){ + lits.insert(lit); + Node plit = + vinst->hasProcessAssertion(this, sf, pv, lit, effort); + if (!plit.isNull()) { + Trace("cbqi-inst-debug2") << " look at " << lit; + if (plit != lit) { + Trace("cbqi-inst-debug2") << "...processed to : " << plit; + } + Trace("cbqi-inst-debug2") << std::endl; // apply substitutions - Node slit = applySubstitutionToLiteral( lit, sf ); + Node slit = applySubstitutionToLiteral(plit, sf); if( !slit.isNull() ){ Trace("cbqi-inst-debug") << "...try based on literal " << slit << std::endl; // check if contains pv if( hasVariable( slit, pv ) ){ - if( vinst->processAssertion( this, sf, pv, slit, effort ) ){ - return true; + if (vinst->processAssertion(this, sf, pv, slit, lit, + effort)) { + return true; } } } @@ -312,7 +319,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e } } } - if( vinst->processAssertions( this, sf, pv, lits, effort ) ){ + if (vinst->processAssertions(this, sf, pv, effort)) { return true; } } diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h index 88b3465ad..8d7a9b5c3 100644 --- a/src/theory/quantifiers/ceg_instantiator.h +++ b/src/theory/quantifiers/ceg_instantiator.h @@ -272,15 +272,47 @@ public: // whether the instantiator implements processAssertion for any literal virtual bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; } - // whether the instantiator implements processAssertion for literal lit - virtual bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) { return false; } - // Called when the entailment: - // E |= lit - // holds in current context E. Typically, lit belongs to the list of current assertions. - // Returns true if an instantiation was successfully added via a recursive call - virtual bool processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) { return false; } - // Called after processAssertion is called for each literal asserted to the instantiator. - virtual bool processAssertions( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& lits, unsigned effort ) { return false; } + /** has process assertion + * + * Called when the entailment: + * E |= lit + * holds in current context E. Typically, lit belongs to the list of current + * assertions. + * + * This function is used to determine whether the instantiator implements + * processAssertion for literal lit. + * If this function returns null, then this intantiator does not handle the + * literal lit + * Otherwise, this function returns a literal lit' with the properties: + * (1) lit' is true in the current model, + * (2) lit' implies lit. + * where typically lit' = lit. + */ + virtual Node hasProcessAssertion(CegInstantiator* ci, SolvedForm& sf, Node pv, + Node lit, unsigned effort) { + return Node::null(); + } + /** process assertion + * Processes the assertion slit for variable pv + * + * lit is the substituted form (under sf) of a literal returned by + * hasProcessAssertion + * alit is the asserted literal, given as input to hasProcessAssertion + * + * Returns true if an instantiation was successfully added via a recursive call + */ + virtual bool processAssertion(CegInstantiator* ci, SolvedForm& sf, Node pv, + Node lit, Node alit, unsigned effort) { + return false; + } + /** process assertions + * Called after processAssertion is called for each literal asserted to the + * instantiator. + */ + virtual bool processAssertions(CegInstantiator* ci, SolvedForm& sf, Node pv, + unsigned effort) { + return false; + } //do we use the model value as instantiation for pv virtual bool useModelValue( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; } diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp index 981d33c2f..91c29c6de 100644 --- a/src/theory/quantifiers/ceg_t_instantiator.cpp +++ b/src/theory/quantifiers/ceg_t_instantiator.cpp @@ -263,14 +263,23 @@ bool ArithInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, N return false; } -bool ArithInstantiator::hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) { +Node ArithInstantiator::hasProcessAssertion(CegInstantiator* ci, SolvedForm& sf, + Node pv, Node lit, + unsigned effort) { Node atom = lit.getKind()==NOT ? lit[0] : lit; bool pol = lit.getKind()!=NOT; //arithmetic inequalities and disequalities - return atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol && atom[0].getType().isReal() ); + if (atom.getKind() == GEQ || + (atom.getKind() == EQUAL && !pol && atom[0].getType().isReal())) { + return lit; + } else { + return Node::null(); + } } -bool ArithInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) { +bool ArithInstantiator::processAssertion(CegInstantiator* ci, SolvedForm& sf, + Node pv, Node lit, Node alit, + unsigned effort) { Node atom = lit.getKind()==NOT ? lit[0] : lit; bool pol = lit.getKind()!=NOT; //arithmetic inequalities and disequalities @@ -385,8 +394,9 @@ bool ArithInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf, return false; } -bool ArithInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& lits, unsigned effort ) { - if( options::cbqiModel() ){ +bool ArithInstantiator::processAssertions(CegInstantiator* ci, SolvedForm& sf, + Node pv, unsigned effort) { + if (options::cbqiModel()) { bool use_inf = ci->useVtsInfinity() && ( d_type.isInteger() ? options::cbqiUseInfInt() : options::cbqiUseInfReal() ); bool upper_first = false; if( options::cbqiMinBounds() ){ @@ -868,11 +878,14 @@ void BvInstantiator::reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsig d_var_to_inst_id.clear(); d_inst_id_to_term.clear(); d_inst_id_to_status.clear(); + d_inst_id_to_alit.clear(); d_var_to_curr_inst_id.clear(); + d_alit_to_model_slack.clear(); } - -void BvInstantiator::processLiteral( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) { +void BvInstantiator::processLiteral(CegInstantiator* ci, SolvedForm& sf, + Node pv, Node lit, Node alit, + unsigned effort) { Assert( d_inverter!=NULL ); // find path to pv std::vector< unsigned > path; @@ -887,6 +900,7 @@ void BvInstantiator::processLiteral( CegInstantiator * ci, SolvedForm& sf, Node // store information for id and increment d_var_to_inst_id[pv].push_back( iid ); d_inst_id_to_term[iid] = inst; + d_inst_id_to_alit[iid] = alit; d_inst_id_counter++; }else{ // cleanup information if we failed to solve @@ -895,11 +909,52 @@ void BvInstantiator::processLiteral( CegInstantiator * ci, SolvedForm& sf, Node } } -bool BvInstantiator::hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) { - return true; +Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci, SolvedForm& sf, + Node pv, Node lit, unsigned effort) { + Node atom = lit.getKind() == NOT ? lit[0] : lit; + bool pol = lit.getKind() != NOT; + Kind k = atom.getKind(); + if (pol && k == EQUAL) { + // positively asserted equalities between bitvector terms we leave unmodifed + if (atom[0].getType().isBitVector()) { + return lit; + } + } else { + // for all other predicates, we convert them to a positive equality based on + // the current model M, e.g.: + // (not) s ~ t ---> s = t + ( s^M - t^M ) + if (k == EQUAL || k == BITVECTOR_ULT || k == BITVECTOR_ULE || + k == BITVECTOR_SLT || k == BITVECTOR_SLE) { + Node s = atom[0]; + Node t = atom[1]; + // only handle equalities between bitvectors + if (s.getType().isBitVector()) { + NodeManager* nm = NodeManager::currentNM(); + Node sm = ci->getModelValue(s); + Assert(!sm.isNull() && sm.isConst()); + Node tm = ci->getModelValue(t); + Assert(!tm.isNull() && tm.isConst()); + if (sm != tm) { + Node slack = + Rewriter::rewrite(nm->mkNode(kind::BITVECTOR_SUB, sm, tm)); + Assert(slack.isConst()); + // remember the slack value for the asserted literal + d_alit_to_model_slack[lit] = slack; + Node ret = nm->mkNode(kind::EQUAL, s, + nm->mkNode(kind::BITVECTOR_PLUS, t, slack)); + Trace("cegqi-bv") << "Process " << lit << " as " << ret + << ", slack is " << slack << std::endl; + return ret; + } + } + } + } + return Node::null(); } -bool BvInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) { +bool BvInstantiator::processAssertion(CegInstantiator* ci, SolvedForm& sf, + Node pv, Node lit, Node alit, + unsigned effort) { // if option enabled, use approach for word-level inversion for BV instantiation if( options::cbqiBv() ){ // get the best rewritten form of lit for solving for pv @@ -911,12 +966,13 @@ bool BvInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf, Nod Trace("cegqi-bv") << "...rewritten to " << rlit << std::endl; } } - processLiteral( ci, sf, pv, rlit, effort ); + processLiteral(ci, sf, pv, rlit, alit, effort); } return false; } -bool BvInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& lits, unsigned effort ) { +bool BvInstantiator::processAssertions(CegInstantiator* ci, SolvedForm& sf, + Node pv, unsigned effort) { std::unordered_map< Node, std::vector< unsigned >, NodeHashFunction >::iterator iti = d_var_to_inst_id.find( pv ); if( iti!=d_var_to_inst_id.end() ){ Trace("cegqi-bv") << "BvInstantiator::processAssertions for " << pv << std::endl; @@ -928,15 +984,30 @@ bool BvInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf, No // hence we randomize the list // this helps robustness, since picking the same literal every time may be lead to a stream of value instantiations std::random_shuffle( iti->second.begin(), iti->second.end() ); - + for( unsigned j=0; j<iti->second.size(); j++ ){ unsigned inst_id = iti->second[j]; Assert( d_inst_id_to_term.find(inst_id)!=d_inst_id_to_term.end() ); Node inst_term = d_inst_id_to_term[inst_id]; + Assert(d_inst_id_to_alit.find(inst_id) != d_inst_id_to_alit.end()); + Node alit = d_inst_id_to_alit[inst_id]; + + // get the slack value introduced for the asserted literal + Node curr_slack_val; + std::unordered_map<Node, Node, NodeHashFunction>::iterator itms = + d_alit_to_model_slack.find(alit); + if (itms != d_alit_to_model_slack.end()) { + curr_slack_val = itms->second; + } + // debug printing if( Trace.isOn("cegqi-bv") ){ Trace("cegqi-bv") << " [" << j << "] : "; Trace("cegqi-bv") << inst_term << std::endl; + if (!curr_slack_val.isNull()) { + Trace("cegqi-bv") << " ...with slack value : " << curr_slack_val + << std::endl; + } // process information about solved status std::unordered_map< unsigned, BvInverterStatus >::iterator its = d_inst_id_to_status.find( inst_id ); Assert( its!=d_inst_id_to_status.end() ); @@ -949,11 +1020,15 @@ bool BvInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf, No } Trace("cegqi-bv") << std::endl; } - // TODO : selection criteria across multiple literals goes here - - // currently, we use a naive heuristic which takes only the first solved term + + // currently we take select the first literal if( inst_ids_try.empty() ){ + // try the first one inst_ids_try.push_back( inst_id ); + } else { + // selection criteria across multiple literals goes here + + } } diff --git a/src/theory/quantifiers/ceg_t_instantiator.h b/src/theory/quantifiers/ceg_t_instantiator.h index 0880fe878..9f47e7211 100644 --- a/src/theory/quantifiers/ceg_t_instantiator.h +++ b/src/theory/quantifiers/ceg_t_instantiator.h @@ -43,9 +43,12 @@ public: bool hasProcessEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; } bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< TermProperties >& term_props, std::vector< Node >& terms, unsigned effort ); bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; } - bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ); - bool processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ); - bool processAssertions( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& lits, unsigned effort ); + Node hasProcessAssertion(CegInstantiator* ci, SolvedForm& sf, Node pv, + Node lit, unsigned effort); + bool processAssertion(CegInstantiator* ci, SolvedForm& sf, Node pv, Node lit, + Node alit, unsigned effort); + bool processAssertions(CegInstantiator* ci, SolvedForm& sf, Node pv, + unsigned effort); bool needsPostProcessInstantiationForVariable( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ); bool postProcessInstantiationForVariable( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort, std::vector< Node >& lemmas ); std::string identify() const { return "Arith"; } @@ -86,25 +89,38 @@ private: // point to the bv inverter class BvInverter * d_inverter; unsigned d_inst_id_counter; + /** information about solved forms */ std::unordered_map< Node, std::vector< unsigned >, NodeHashFunction > d_var_to_inst_id; std::unordered_map< unsigned, Node > d_inst_id_to_term; std::unordered_map< unsigned, BvInverterStatus > d_inst_id_to_status; + std::unordered_map<unsigned, Node> d_inst_id_to_alit; // variable to current id we are processing std::unordered_map< Node, unsigned, NodeHashFunction > d_var_to_curr_inst_id; + /** the amount of slack we added for asserted literals */ + std::unordered_map<Node, Node, NodeHashFunction> d_alit_to_model_slack; /** rewrite assertion for solve pv * returns a literal that is equivalent to lit that leads to best solved form for pv */ Node rewriteAssertionForSolvePv( Node pv, Node lit ); -private: - void processLiteral( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ); -public: + /** process literal, called from processAssertion + * lit is the literal to solve for pv that has been rewritten according to + * internal rules here. + * alit is the asserted literal that lit is derived from. + */ + void processLiteral(CegInstantiator* ci, SolvedForm& sf, Node pv, Node lit, + Node alit, unsigned effort); + + public: BvInstantiator( QuantifiersEngine * qe, TypeNode tn ); virtual ~BvInstantiator(); void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ); bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; } - bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ); - bool processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ); - bool processAssertions( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& lits, unsigned effort ); + Node hasProcessAssertion(CegInstantiator* ci, SolvedForm& sf, Node pv, + Node lit, unsigned effort); + bool processAssertion(CegInstantiator* ci, SolvedForm& sf, Node pv, Node lit, + Node alit, unsigned effort); + bool processAssertions(CegInstantiator* ci, SolvedForm& sf, Node pv, + unsigned effort); bool needsPostProcessInstantiationForVariable( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ); bool postProcessInstantiationForVariable( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort, std::vector< Node >& lemmas ); bool useModelValue( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; } diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index 3a8634d1e..14e5244b4 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -95,13 +95,16 @@ TESTS = \ qbv-test-invert-bvor.smt2 \ qbv-test-invert-bvlshr-0.smt2 \ qbv-test-invert-bvurem-1.smt2 \ - qbv-simple-2vars-vo.smt2 \ qbv-test-invert-concat-0.smt2 \ qbv-test-invert-concat-1.smt2 \ qbv-test-invert-shl.smt2 \ qbv-test-invert-udiv-0.smt2 \ qbv-test-invert-udiv-1.smt2 \ - qbv-test-urem-rewrite.smt2 + qbv-simple-2vars-vo.smt2 \ + qbv-test-urem-rewrite.smt2 \ + qbv-inequality2.smt2 \ + qbv-test-invert-bvult-1.smt2 + # regression can be solved with --finite-model-find --fmf-inst-engine # set3.smt2 diff --git a/test/regress/regress0/quantifiers/qbv-inequality2.smt2 b/test/regress/regress0/quantifiers/qbv-inequality2.smt2 new file mode 100644 index 000000000..d53715a2d --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-inequality2.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --cbqi-bv +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 32)) +(declare-fun b () (_ BitVec 32)) + + +(assert (forall ((x (_ BitVec 32))) (or (bvuge x (bvadd a b)) (bvule x b)))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-multi-lit-uge.smt2 b/test/regress/regress0/quantifiers/qbv-multi-lit-uge.smt2 new file mode 100644 index 000000000..d74a6cfea --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-multi-lit-uge.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --cbqi-bv +; EXPECT: sat +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 3)) +(declare-fun b () (_ BitVec 3)) +(declare-fun c () (_ BitVec 3)) + +(assert (forall ((x (_ BitVec 3))) (or (not (= (bvmul x a) b)) (bvuge x c)))) + +(check-sat) |