From: Andrew Reynolds Date: Fri, 29 Sep 2017 12:23:22 +0000 (-0500) Subject: Initial working version of BV word-level instantiation (#1158) X-Git-Tag: cvc5-1.0.0~5598 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8011f2715fa6ba312fd766cab5249648598310d4;p=cvc5.git Initial working version of BV word-level instantiation (#1158) * Initial work on BV CEGQI, still working on avoid circular dependencies with inversion skolems. * Guard by option, minor notes. * Minor * Minor fixes. * Minor --- diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index c94360671..d5619ed77 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -287,7 +287,7 @@ option sygusCRefEval --sygus-cref-eval bool :default true option sygusCRefEvalMinExp --sygus-cref-eval-min-exp bool :default true use min explain for direct evaluation of refinement lemmas for conflict analysis -# approach applied to general quantified formulas +# CEGQI applied to general quantified formulas option cbqi --cbqi bool :read-write :default false turns on counterexample-based quantifier instantiation option recurseCbqi --cbqi-recurse bool :default true @@ -298,6 +298,8 @@ option cbqiModel --cbqi-model bool :read-write :default true guide instantiations by model values for counterexample-based quantifier instantiation option cbqiAll --cbqi-all bool :read-write :default false apply counterexample-based instantiation to all quantified formulas + +# CEGQI for arithmetic option cbqiUseInfInt --cbqi-use-inf-int bool :read-write :default false use integer infinity for vts in counterexample-based quantifier instantiation option cbqiUseInfReal --cbqi-use-inf-real bool :read-write :default false @@ -319,11 +321,16 @@ option cbqiInnermost --cbqi-innermost bool :read-write :default true option cbqiNestedQE --cbqi-nested-qe bool :read-write :default false process nested quantified formulas with quantifier elimination in counterexample-based quantifier instantiation +# CEGQI for EPR option quantEpr --quant-epr bool :default false :read-write infer whether in effectively propositional fragment, use for cbqi 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 + use word-level inversion approach for counterexample-guided quantifier instantiation for bit-vectors + ### local theory extensions options option localTheoryExt --local-t-ext bool :default false diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp index ddec91d49..75118dadc 100644 --- a/src/theory/quantifiers/ceg_t_instantiator.cpp +++ b/src/theory/quantifiers/ceg_t_instantiator.cpp @@ -842,6 +842,19 @@ Node BvInverter::getSolveVariable( TypeNode tn ) { } } +Node BvInverter::getInversionSkolemFor( Node cond, TypeNode tn ) { + std::unordered_map< Node, Node, NodeHashFunction >::iterator it = d_inversion_skolem_cache.find( cond ); + if( it==d_inversion_skolem_cache.end() ){ + Node skv = NodeManager::currentNM()->mkSkolem ("skvinv", tn, "created for BvInverter"); + Trace("cegqi-bv-skvinv") << "SKVINV : " << skv << " is the skolem associated with conditon " << cond << std::endl; + d_inversion_skolem_cache[cond] = skv; + return skv; + }else{ + Assert( it->second.getType()==tn ); + return it->second; + } +} + Node BvInverter::getPathToPv( Node lit, Node pv, Node sv, std::vector< unsigned >& path, std::unordered_set< TNode, TNodeHashFunction >& visited ) { if( visited.find( lit )==visited.end() ){ visited.insert( lit ); @@ -898,23 +911,29 @@ Node BvInverter::solve_bv_constraint( Node sv, Node sv_t, Node t, Kind rk, bool t = nm->mkNode( BITVECTOR_PLUS, t, sv_t[1-index] ); }else if( k==BITVECTOR_MULT ){ // t = skv (fresh skolem constant) + TypeNode solve_tn = sv_t[index].getType(); + Node x = getSolveVariable( solve_tn ); // with side condition: - // ctz(t) >= ctz(s) <-> skv * s = t + // ctz(t) >= ctz(s) <-> x * s = t // where // ctz(t) >= ctz(s) -> (t & -t) >= (s & -s) Node s = sv_t[1-index]; - Node skv = nm->mkSkolem ("skvinv", t.getType(), "created for BvInverter"); - // cache for substitution - BvInverterSkData d = BvInverterSkData (sv_t, t, k); - d_sk_inv.emplace(skv,d); // left hand side of side condition Node scl = nm->mkNode (BITVECTOR_UGE, nm->mkNode (BITVECTOR_AND, t, nm->mkNode (BITVECTOR_NEG, t)), nm->mkNode (BITVECTOR_AND, s, nm->mkNode (BITVECTOR_NEG, s))); // right hand side of side condition - Node scr = nm->mkNode (EQUAL, nm->mkNode (BITVECTOR_MULT, skv, s), t); + Node scr = nm->mkNode (EQUAL, nm->mkNode (BITVECTOR_MULT, x, s), t); + // overall side condition + Node sc = nm->mkNode (IMPLIES, scl, scr); // add side condition - status.d_conds.push_back (nm->mkNode (EQUAL, scl, scr)); + status.d_conds.push_back (sc); + + // get the skolem variable for this side condition + Node skv = getInversionSkolemFor (sc, solve_tn); + // cache for substitution + // map the skolem to its side condition + status.d_sk_inv[ skv ] = sc; t = skv; }else if( k==BITVECTOR_NEG || k==BITVECTOR_NOT ){ @@ -940,7 +959,7 @@ Node BvInverter::solve_bv_constraint( Node sv, Node sv_t, Node t, Kind rk, bool return t; }else{ Trace("bv-invert") << "bv-invert : Unknown relation kind for bit-vector literal " << rk << std::endl; - return Node::null(); + return t; } } @@ -987,76 +1006,59 @@ Node BvInverter::solve_bv_lit( Node sv, Node lit, bool pol, std::vector< unsigne return Node::null(); } -void BvInstantiator::reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { - d_inst_id_counter = 0; - d_var_to_inst_id.clear(); - d_inst_id_to_term.clear(); - d_inst_id_to_status.clear(); -} - +// this class can be used to query the model value through the CegInstaniator class class CegInstantiatorBvInverterModelQuery : public BvInverterModelQuery { protected: + // pointer to class that is able to query model values CegInstantiator * d_ci; public: CegInstantiatorBvInverterModelQuery( CegInstantiator * ci ) : BvInverterModelQuery(), d_ci( ci ){} + ~CegInstantiatorBvInverterModelQuery(){} + // get the model value of n Node getModelValue( Node n ) { return d_ci->getModelValue( n ); } }; +BvInstantiator::BvInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){ + //FIXME : this needs to be global!! Probably move to QuantifiersEngine + d_inverter = new BvInverter; +} + +BvInstantiator::~BvInstantiator(){ + delete d_inverter; +} + +void BvInstantiator::reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { + d_inst_id_counter = 0; + d_var_to_inst_id.clear(); + d_inst_id_to_term.clear(); + d_inst_id_to_status.clear(); + d_var_to_curr_inst_id.clear(); +} + + void BvInstantiator::processLiteral( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) { // find path to pv std::vector< unsigned > path; - Node sv = d_inverter.getSolveVariable( pv.getType() ); + Node sv = d_inverter->getSolveVariable( pv.getType() ); Node pvs = ci->getModelValue( pv ); - Node slit = d_inverter.getPathToPv( lit, pv, sv, pvs, path ); + Node slit = d_inverter->getPathToPv( lit, pv, sv, pvs, path ); if( !slit.isNull() ){ CegInstantiatorBvInverterModelQuery m( ci ); unsigned iid = d_inst_id_counter; - Node inst = d_inverter.solve_bv_lit( sv, slit, true, path, &m, d_inst_id_to_status[iid] ); + Node inst = d_inverter->solve_bv_lit( sv, slit, true, path, &m, d_inst_id_to_status[iid] ); if( !inst.isNull() ){ // 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_counter++; }else{ - // cleanup information + // cleanup information if we failed to solve d_inst_id_to_status.erase( iid ); } } - /* TODO: algebraic reasoning for bitvector instantiation - if( atom.getKind()==BITVECTOR_ULT || atom.getKind()==BITVECTOR_ULE ){ - for( unsigned t=0; t<2; t++ ){ - if( atom[t]==pv ){ - computeProgVars( atom[1-t] ); - if( d_inelig.find( atom[1-t] )==d_inelig.end() ){ - //only ground terms TODO: more - if( d_prog_var[atom[1-t]].empty() ){ - TermProperties pv_prop; - Node uval; - if( ( !pol && atom.getKind()==BITVECTOR_ULT ) || ( pol && atom.getKind()==BITVECTOR_ULE ) ){ - uval = atom[1-t]; - }else{ - uval = NodeManager::currentNM()->mkNode( (atom.getKind()==BITVECTOR_ULT)==(t==1) ? BITVECTOR_PLUS : BITVECTOR_SUB, atom[1-t], - bv::utils::mkConst(pvtn.getConst(), 1) ); - } - if( doAddInstantiationInc( pv, uval, pv_prop, sf, effort ) ){ - return true; - } - } - } - } - } - } - */ -} - -bool BvInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< TermProperties >& term_props, std::vector< Node >& terms, unsigned effort ) { - Assert( term_props[0].isBasic() ); - Assert( term_props[1].isBasic() ); - //processLiteral( ci, sf, pv, terms[0].eqNode( terms[1] ), effort ); - return false; } bool BvInstantiator::hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) { @@ -1064,23 +1066,130 @@ bool BvInstantiator::hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, } bool BvInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) { - //processLiteral( ci, sf, pv, lit, effort ); + Trace("cegqi-bv") << "BvInstantiator::processAssertion : solve " << pv << " in " << lit << std::endl; + if( options::cbqiBv() ){ + // if option enabled, use approach for word-level inversion for BV instantiation + processLiteral( ci, sf, pv, lit, effort ); + } return false; } bool BvInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& lits, unsigned effort ) { - std::map< Node, std::vector< unsigned > >::iterator iti = d_var_to_inst_id.find( pv ); + 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; // get inst id list - Trace("bv-inst") << "bv-inst : " << iti->second.size() << " candidate instantiations for " << pv << " : " << std::endl; + Trace("cegqi-bv") << " " << iti->second.size() << " candidate instantiations for " << pv << " : " << std::endl; + // the order of instantiation ids we will try + std::vector< unsigned > inst_ids_try; + for( unsigned j=0; jsecond.size(); j++ ){ - Trace("bv-inst") << "[" << j << "] : " << iti->second[j]; - // print information about solved status TODO - - Trace("bv-inst") << std::endl; + 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]; + // debug printing + if( Trace.isOn("cegqi-bv") ){ + Trace("cegqi-bv") << " [" << j << "] : "; + Trace("cegqi-bv") << inst_term << 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() ); + if( !(*its).second.d_conds.empty() ){ + Trace("cegqi-bv") << " ...with " << (*its).second.d_conds.size() << " side conditions : " << std::endl; + for( unsigned k=0; k<(*its).second.d_conds.size(); k++ ){ + Node cond = (*its).second.d_conds[k]; + Trace("cegqi-bv") << " " << cond << std::endl; + } + } + 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 + // TODO : randomize? + if( inst_ids_try.empty() ){ + inst_ids_try.push_back( inst_id ); + } } + + // now, try all instantiation ids we want to try + for( unsigned j = 0; jsecond[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]; + // try instantiation pv -> inst_term + TermProperties pv_prop_bv; + Trace("cegqi-bv") << "*** try " << pv << " -> " << inst_term << std::endl; + // TODO : need to track dependencies between inst_term and the free variables it depends on + // This should enforce that we do not introduce any circular dependencies when solving for further variables. + d_var_to_curr_inst_id[pv] = inst_id; + if( ci->doAddInstantiationInc( pv, inst_term, pv_prop_bv, sf, effort ) ){ + return true; + } + } + Trace("cegqi-bv") << "...failed to add instantiation for " << pv << std::endl; + d_var_to_curr_inst_id.erase( pv ); } return false; } + +bool BvInstantiator::needsPostProcessInstantiationForVariable( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { + // we may need to post-process the instantiation since inversion skolems need to be finalized + return d_var_to_curr_inst_id.find(pv)!=d_var_to_curr_inst_id.end(); +} + +bool BvInstantiator::postProcessInstantiationForVariable( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort, std::vector< Node >& lemmas ) { + Trace("cegqi-bv") << "BvInstantiator::postProcessInstantiation for " << pv << std::endl; + // first, eliminate bound variables from all skolem conditions + std::unordered_map< Node, unsigned, NodeHashFunction >::iterator iti = d_var_to_curr_inst_id.find( pv ); + Assert( iti!=d_var_to_curr_inst_id.end() ); + unsigned inst_id = iti->second; + std::unordered_map< unsigned, BvInverterStatus >::iterator its = d_inst_id_to_status.find( inst_id ); + Assert( its!=d_inst_id_to_status.end() ); + + // this maps temporary skolems (those with side conditions involving free variables) -> finalized skolems + std::vector< Node > sk_vars_add; + std::vector< Node > sk_subs_add; + for( std::unordered_map< Node, Node, NodeHashFunction >::iterator itk = its->second.d_sk_inv.begin(); + itk != its->second.d_sk_inv.end(); ++itk ){ + TNode curr_skv = itk->first; + Trace("cegqi-bv-debug") << " Skolem " << curr_skv << " has condition " << itk->second << std::endl; + Node curr_cond = itk->second.substitute( sf.d_vars.begin(), sf.d_vars.end(), sf.d_subs.begin(), sf.d_subs.end() ); + // the condition should have no bound variables, or skolems that are associated with conditions that have bound variables. + + // if the condition is updated, we need to update it + Node sk_for_curr_cond; + if( curr_cond!=itk->second ){ + Trace("cegqi-bv-debug") << " Skolem " << curr_skv << " has condition (after substitution) " << curr_cond << std::endl; + sk_for_curr_cond = d_inverter->getInversionSkolemFor( curr_cond, curr_skv.getType() ); + // we must replace the Skolem in the condition + sk_vars_add.push_back( curr_skv ); + sk_subs_add.push_back( sk_for_curr_cond ); + + // TODO : register this as a skolem that is eligible for instantiation + }else{ + sk_for_curr_cond = curr_skv; + } + + // we now must map the solve variable in the current condition to the final skolem + TNode solve_var = d_inverter->getSolveVariable( sk_for_curr_cond.getType() ); + curr_cond = curr_cond.substitute( solve_var, sk_for_curr_cond ); + + // curr_cond is now in terms of the finalized skolem + lemmas.push_back( curr_cond ); + Trace("cegqi-bv") << " side condition : " << curr_cond << std::endl; + } + + // add new substitutions + TermProperties term_prop_skvinv; + for( unsigned i=0; i final) skolem substitution : " << sk_vars_add[i] << " -> " << sk_subs_add[i] << std::endl; + } + + return true; +} + + diff --git a/src/theory/quantifiers/ceg_t_instantiator.h b/src/theory/quantifiers/ceg_t_instantiator.h index 457e07f7a..7328df167 100644 --- a/src/theory/quantifiers/ceg_t_instantiator.h +++ b/src/theory/quantifiers/ceg_t_instantiator.h @@ -84,6 +84,7 @@ public: class BvInverterModelQuery { public: BvInverterModelQuery(){} + ~BvInverterModelQuery(){} virtual Node getModelValue( Node n ) = 0; }; @@ -91,18 +92,12 @@ public: class BvInverterStatus { public: BvInverterStatus() : d_status(0) {} + ~BvInverterStatus(){} int d_status; + // side conditions std::vector< Node > d_conds; -}; - -// class for storing mapped data for fresh skolem constants -class BvInverterSkData { -public: - BvInverterSkData (Node sv_t, Node t, Kind op) - : d_sv_t(sv_t), d_t(t), d_op(op) {} - Node d_sv_t; - Node d_t; - Kind d_op; + // conditions regarding the skolems in d_conds + std::unordered_map< Node, Node, NodeHashFunction > d_sk_inv; }; // inverter class @@ -110,11 +105,19 @@ public: class BvInverter { private: std::map< TypeNode, Node > d_solve_var; - std::unordered_map< Node, BvInverterSkData, NodeHashFunction > d_sk_inv; Node getPathToPv( Node lit, Node pv, Node sv, std::vector< unsigned >& path, std::unordered_set< TNode, TNodeHashFunction >& visited ); + // stores the inversion skolems + std::unordered_map< Node, Node, NodeHashFunction > d_inversion_skolem_cache; public: + BvInverter(){} + ~BvInverter(){} // get dummy fresh variable of type tn, used as argument for sv Node getSolveVariable( TypeNode tn ); + // get inversion skolem for condition + // precondition : exists x. cond( x ) is a tautology in BV, + // where x is getSolveVariable( tn ). + // returns fresh skolem k, where we may assume cond( k ). + Node getInversionSkolemFor( Node cond, TypeNode tn ); // Get path to pv in lit, replace that occurrence by sv and all others by pvs. // e.g. if return value R is non-null, then: // lit.path = pv @@ -134,29 +137,31 @@ public: class BvInstantiator : public Instantiator { private: - BvInverter d_inverter; + // point to the bv inverter class + BvInverter * d_inverter; unsigned d_inst_id_counter; - std::map< Node, std::vector< unsigned > > d_var_to_inst_id; - std::map< unsigned, Node > d_inst_id_to_term; - std::map< unsigned, BvInverterStatus > d_inst_id_to_status; + 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; + // variable to current id we are processing + std::unordered_map< Node, unsigned, NodeHashFunction > d_var_to_curr_inst_id; private: void processLiteral( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ); public: - BvInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){} - virtual ~BvInstantiator(){} + BvInstantiator( QuantifiersEngine * qe, TypeNode tn ); + virtual ~BvInstantiator(); void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ); - 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 ); + 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; } std::string identify() const { return "Bv"; } }; - } } } diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index cdf2ec9bc..cb6ed687e 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -89,7 +89,11 @@ TESTS = \ cbqi-sdlx-fixpoint-3-dd.smt2 \ qbv-simp.smt2 \ psyco-001-bv.smt2 \ - bug822.smt2 + bug822.smt2 + +# FIXME: solvable with --cbqi-bv +#qbv-test-invert-mul.smt2 +#qbv-simple-2vars-vo.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine # set3.smt2 diff --git a/test/regress/regress0/quantifiers/qbv-simple-2vars-vo.smt2 b/test/regress/regress0/quantifiers/qbv-simple-2vars-vo.smt2 new file mode 100644 index 000000000..f38625fd8 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-simple-2vars-vo.smt2 @@ -0,0 +1,15 @@ +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 32)) +(declare-fun b () (_ BitVec 32)) +(declare-fun c () (_ BitVec 32)) + +(assert (not (= a #x00000000))) + +; this is sensitive to variable ordering (try changing x and y) +(assert (forall ((x (_ BitVec 32)) (y (_ BitVec 32))) (or +(not (= (bvmul x y) #x0000000A)) +(not (= (bvadd y a) #x00000010)) +))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-mul.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-mul.smt2 new file mode 100644 index 000000000..bea19a054 --- /dev/null +++ b/test/regress/regress0/quantifiers/qbv-test-invert-mul.smt2 @@ -0,0 +1,9 @@ +(set-logic BV) +(set-info :status sat) +(declare-fun a () (_ BitVec 32)) +(declare-fun b () (_ BitVec 32)) +(declare-fun c () (_ BitVec 32)) + +(assert (forall ((x (_ BitVec 32))) (not (= (bvmul x a) b)))) + +(check-sat)