From: Andrew Reynolds Date: Tue, 12 Sep 2017 23:48:27 +0000 (-0500) Subject: Initial infrastructure for BV instantiation via word-level inversions. (#1056) X-Git-Tag: cvc5-1.0.0~5646 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=51cab64a53daee8e6f2693f12911c71827013f15;p=cvc5.git Initial infrastructure for BV instantiation via word-level inversions. (#1056) * Initial infrastructure for BV instantiation via word-level inversions. * Minor clean up. * Change visited to unordered set. --- diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index 05e86c9e8..db283ccfc 100644 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -11,7 +11,7 @@ ** ** \brief Implementation of counterexample-guided quantifier instantiation **/ - + #include "theory/quantifiers/ceg_instantiator.h" #include "theory/quantifiers/ceg_t_instantiator.h" @@ -131,7 +131,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e postProcessSuccess = false; break; } - } + } if( postProcessSuccess ){ return doAddInstantiation( sf_tmp.d_subs, sf_tmp.d_vars ); }else{ @@ -294,9 +294,13 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e Node lit = ita->second[j]; if( std::find( lits.begin(), lits.end(), lit )==lits.end() ){ lits.push_back( lit ); - if( vinst->processAssertion( this, sf, pv, lit, effort ) ){ - return true; - } + //if( vinst->hasProcessAssertion( this, sf, pv, lit, effort ) ){ + // apply substitutions check if eligible and contains pv + // TODO + if( vinst->processAssertion( this, sf, pv, lit, effort ) ){ + return true; + } + //} } } } @@ -326,7 +330,7 @@ bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned e } } Trace("cbqi-inst-debug") << "[No instantiation found for " << pv << "]" << std::endl; - if( is_cv ){ + if( is_cv ){ d_stack_vars.push_back( pv ); } d_active_instantiators.erase( pv ); @@ -509,7 +513,7 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node Assert( subs[i].getType().isSubtypeOf( vars[i].getType() ) ); } } - + if( !req_coeff ){ Node nret = n.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); if( n!=nret ){ @@ -995,7 +999,7 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st Node v = lems[i][0]; d_aux_eq[rlem][v] = lems[i][1]; Trace("cbqi-debug") << " " << rlem << " implies " << v << " = " << lems[i][1] << std::endl; - } + } }*/ lems[i] = rlem; } diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h index aed1be3a4..c260486ff 100644 --- a/src/theory/quantifiers/ceg_instantiator.h +++ b/src/theory/quantifiers/ceg_instantiator.h @@ -41,14 +41,27 @@ public: class Instantiator; +//TODO: refactor pv_coeff to pv_prop throughout +//generic class that stores properties for a variable to solve for in CEGQI +class TermProperties { +public: + TermProperties() : d_type(-1) {} + int d_type; + // for arithmetic + Node d_coeff; +}; + //solved form, involves substitution with coefficients class SolvedForm { public: std::vector< Node > d_vars; std::vector< Node > d_subs; + //TODO: refactor below coeff -> prop; std::vector< Node > d_coeff; std::vector< int > d_btyp; + //std::vector< TermProperties > d_props; std::vector< Node > d_has_coeff; + //std::vector< Node > d_has_prop; Node d_theta; void copy( SolvedForm& sf ){ d_vars.insert( d_vars.end(), sf.d_vars.begin(), sf.d_vars.end() ); @@ -105,7 +118,7 @@ private: bool d_is_nested_quant; std::vector< Node > d_ce_atoms; //collect atoms - void collectCeAtoms( Node n, std::map< Node, bool >& visited ); + void collectCeAtoms( Node n, std::map< Node, bool >& visited ); private: //map from variables to their instantiators std::map< Node, Instantiator * > d_instantiator; @@ -114,7 +127,7 @@ private: std::map< Node, unsigned > d_curr_index; //stack of temporary variables we are solving (e.g. subfields of datatypes) std::vector< Node > d_stack_vars; - //used instantiators + //used instantiators std::map< Node, Instantiator * > d_active_instantiators; //register variable void registerInstantiationVariable( Node v, unsigned index ); @@ -141,7 +154,7 @@ public: CegqiOutput * getOutput() { return d_out; } //get quantifiers engine QuantifiersEngine* getQuantifiersEngine() { return d_qe; } - + //interface for instantiators public: void pushStackVariable( Node v ); @@ -157,9 +170,9 @@ public: public: unsigned getNumCEAtoms() { return d_ce_atoms.size(); } Node getCEAtom( unsigned i ) { return d_ce_atoms[i]; } - // is eligible + // is eligible bool isEligible( Node n ); - // has variable + // has variable bool hasVariable( Node n, Node pv ); bool useVtsDelta() { return d_use_vts_delta; } bool useVtsInfinity() { return d_use_vts_inf; } @@ -167,7 +180,6 @@ public: }; - // an instantiator for individual variables // will make calls into CegInstantiator::doAddInstantiationInc class Instantiator { @@ -178,29 +190,32 @@ public: Instantiator( QuantifiersEngine * qe, TypeNode tn ); virtual ~Instantiator(){} virtual void reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) {} - + //called when pv_coeff * pv = n, and n is eligible for instantiation virtual bool processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, Node pv_coeff, Node n, unsigned effort ); //eqc is the equivalence class of pv virtual bool processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort ) { return false; } - - //term_coeffs.size() = terms.size() = 2, called when term_coeff[0] * terms[0] = term_coeff[1] * terms[1], terms are eligible, and at least one of these terms contains pv + virtual bool hasProcessEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; } + //term_coeffs.size() = terms.size() = 2, called when term_coeff[0] * terms[0] = term_coeff[1] * terms[1], terms are eligible, and at least one of these terms contains pv + // returns true if an instantiation was successfully added via a recursive call virtual bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort ) { return false; } - - //called when assertion lit holds. note that lit is unsubstituted, first must substitute/solve/check eligible + virtual bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; } + virtual bool hasProcessAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) { return false; } + //called when assertion lit holds. note that lit is unsubstituted, first must substitute/solve/check eligible + // 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; } virtual bool processAssertions( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& lits, unsigned effort ) { return false; } - + //do we allow instantiation for the model value of pv virtual bool useModelValue( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; } virtual bool allowModelValue( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return d_closed_enum_type; } - + //do we need to postprocess the solved form? did we successfully postprocess virtual bool needsPostProcessInstantiation( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return false; } virtual bool postProcessInstantiation( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; } - + /** Identify this module (for debugging) */ virtual std::string identify() const { return "Default"; } }; diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp index cd541a2a6..fa7dbabab 100644 --- a/src/theory/quantifiers/ceg_t_instantiator.cpp +++ b/src/theory/quantifiers/ceg_t_instantiator.cpp @@ -11,7 +11,7 @@ ** ** \brief Implementation of theory-specific counterexample-guided quantifier instantiation **/ - + #include "theory/quantifiers/ceg_t_instantiator.h" #include "options/quantifiers_options.h" @@ -258,6 +258,13 @@ bool ArithInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, N return false; } +bool 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() ); +} + bool ArithInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) { Trace("cbqi-inst-debug2") << " look at " << lit << std::endl; Node atom = lit.getKind()==NOT ? lit[0] : lit; @@ -583,7 +590,7 @@ bool ArithInstantiator::processAssertions( CegInstantiator * ci, SolvedForm& sf, } //generally should not make it to this point FIXME: write proper assertion //Assert( ( ci->hasNestedQuantification() && !options::cbqiNestedQE() ) || options::cbqiAll() ); - + if( options::cbqiNopt() ){ //try non-optimal bounds (heuristic, may help when nested quantification) ? Trace("cbqi-bound") << "Try non-optimal bounds..." << std::endl; @@ -757,8 +764,8 @@ void EprInstantiator::reset( CegInstantiator * ci, SolvedForm& sf, Node pv, unsi bool EprInstantiator::processEqualTerm( CegInstantiator * ci, SolvedForm& sf, Node pv, Node pv_coeff, Node n, unsigned effort ) { if( options::quantEprMatching() ){ Assert( pv_coeff.isNull() ); - d_equal_terms.push_back( n ); - return false; + d_equal_terms.push_back( n ); + return false; }else{ return ci->doAddInstantiationInc( pv, n, pv_coeff, 0, sf, effort ); } @@ -814,7 +821,7 @@ struct sortEqTermsMatch { } }; - + bool EprInstantiator::processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort ) { if( options::quantEprMatching() ){ //heuristic for best matching constant @@ -835,7 +842,179 @@ bool EprInstantiator::processEqualTerms( CegInstantiator * ci, SolvedForm& sf, N return false; } -bool BvInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) { +Node BvInverter::getSolveVariable( TypeNode tn ) { + std::map< TypeNode, Node >::iterator its = d_solve_var.find( tn ); + if( its==d_solve_var.end() ){ + Node k = NodeManager::currentNM()->mkSkolem( "s", tn ); + d_solve_var[tn] = k; + return k; + }else{ + return its->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 ); + if( lit==pv ){ + return sv; + }else{ + unsigned rmod = 0; // TODO : randomize? + for( unsigned i=0; i children; + if( lit.getMetaKind() == kind::metakind::PARAMETERIZED ){ + children.push_back( lit.getOperator() ); + } + for( unsigned j=0; jmkNode( lit.getKind(), children ); + } + } + } + } + return Node::null(); +} + +Node BvInverter::getPathToPv( Node lit, Node pv, Node sv, Node pvs, std::vector< unsigned >& path ) { + std::unordered_set< TNode, TNodeHashFunction > visited; + Node slit = getPathToPv( lit, pv, sv, path, visited ); + if( !slit.isNull() ){ + // substitute pvs for the other occurrences of pv + TNode tpv = pv; + TNode tpvs = pvs; + slit = slit.substitute( tpv, tpvs ); + } + return slit; +} + +Node BvInverter::solve_bv_constraint( Node sv, Node sv_t, Node t, Kind rk, bool pol, std::vector< unsigned >& path, + BvInverterModelQuery * m, BvInverterStatus& status ) { + while( !path.empty() ){ + unsigned index = path.back(); + Assert( indexmkNode( BITVECTOR_SUB, t, sv_t[1-index] ); + }else if( k==BITVECTOR_SUB ){ + t = NodeManager::currentNM()->mkNode( BITVECTOR_PLUS, t, sv_t[1-index] ); + //}else if( k==BITVECTOR_MULT ){ + // TODO + }else if( k==BITVECTOR_NEG || k==BITVECTOR_NOT ){ + t = NodeManager::currentNM()->mkNode( k, t ); + //}else if( k==BITVECTOR_AND || k==BITVECTOR_OR ){ + // TODO + //}else if( k==BITVECTOR_CONCAT ){ + // TODO + //}else if( k==BITVECTOR_SHL || k==BITVECTOR_LSHR ){ + // TODO + //}else if( k==BITVECTOR_ASHR ){ + // TODO + }else{ + Trace("bv-invert") << "bv-invert : Unknown kind for bit-vector term " << k << ", from " << sv_t << std::endl; + return Node::null(); + } + sv_t = sv_t[index]; + } + Assert( sv_t==sv ); + // finalize based on the kind of constraint + //TODO + if( rk==EQUAL ){ + return t; + }else{ + Trace("bv-invert") << "bv-invert : Unknown relation kind for bit-vector literal " << rk << std::endl; + return Node::null(); + } +} + +Node BvInverter::solve_bv_lit( Node sv, Node lit, bool pol, std::vector< unsigned >& path, + BvInverterModelQuery * m, BvInverterStatus& status ){ + Assert( !path.empty() ); + unsigned index = path.back(); + Assert( indexgetModelValue( n ); + } +}; + +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 pvs = ci->getModelValue( pv ); + 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] ); + 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 + 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++ ){ @@ -849,7 +1028,7 @@ bool BvInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf, Nod 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], + 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, veq_c, 0, sf, effort ) ){ @@ -861,8 +1040,35 @@ bool BvInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf, Nod } } */ +} + +bool BvInstantiator::processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, std::vector< Node >& terms, unsigned effort ) { + //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 ) { + return true; +} +bool BvInstantiator::processAssertion( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ) { + //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 ); + if( iti!=d_var_to_inst_id.end() ){ + // get inst id list + Trace("bv-inst") << "bv-inst : " << iti->second.size() << " candidate instantiations for " << pv << " : " << std::endl; + 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; + } + } + + return false; +} diff --git a/src/theory/quantifiers/ceg_t_instantiator.h b/src/theory/quantifiers/ceg_t_instantiator.h index 787c2547a..dfb7921c8 100644 --- a/src/theory/quantifiers/ceg_t_instantiator.h +++ b/src/theory/quantifiers/ceg_t_instantiator.h @@ -20,6 +20,8 @@ #include "theory/quantifiers/ceg_instantiator.h" +#include + namespace CVC4 { namespace theory { namespace quantifiers { @@ -40,6 +42,7 @@ public: bool hasProcessEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; } bool processEquality( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& term_coeffs, 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 needsPostProcessInstantiation( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ); @@ -76,11 +79,67 @@ public: std::string identify() const { return "Epr"; } }; + +// virtual class for model queries +class BvInverterModelQuery { +public: + BvInverterModelQuery(){} + virtual Node getModelValue( Node n ) = 0; +}; + +// class for storing information about the solved status +class BvInverterStatus { +public: + BvInverterStatus() : d_status(0) {} + int d_status; + std::vector< Node > d_conds; +}; + +// inverter class +// TODO : move to theory/bv/ if generally useful? +class BvInverter { +private: + std::map< TypeNode, Node > d_solve_var; + Node getPathToPv( Node lit, Node pv, Node sv, std::vector< unsigned >& path, std::unordered_set< TNode, TNodeHashFunction >& visited ); +public: + // get dummy fresh variable of type tn, used as argument for sv + Node getSolveVariable( 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 + // R.path = sv + // R.path' = pvs for all lit.path' = pv, where path' != path + Node getPathToPv( Node lit, Node pv, Node sv, Node pvs, std::vector< unsigned >& path ); +public: + // solve for sv in constraint ( (pol ? _ : not) sv_t t ), where sv_t.path = sv + // status accumulates side conditions + Node solve_bv_constraint( Node sv, Node sv_t, Node t, Kind rk, bool pol, std::vector< unsigned >& path, + BvInverterModelQuery * m, BvInverterStatus& status ); + // solve for sv in lit, where lit.path = sv + // status accumulates side conditions + Node solve_bv_lit( Node sv, Node lit, bool pol, std::vector< unsigned >& path, + BvInverterModelQuery * m, BvInverterStatus& status ); +}; + class BvInstantiator : public Instantiator { +private: + 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; +private: + void processLiteral( CegInstantiator * ci, SolvedForm& sf, Node pv, Node lit, unsigned effort ); public: BvInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, 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< Node >& term_coeffs, 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 useModelValue( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; } std::string identify() const { return "Bv"; } };