* Initial infrastructure for BV instantiation via word-level inversions.
* Minor clean up.
* Change visited to unordered set.
**
** \brief Implementation of counterexample-guided quantifier instantiation
**/
-
+
#include "theory/quantifiers/ceg_instantiator.h"
#include "theory/quantifiers/ceg_t_instantiator.h"
postProcessSuccess = false;
break;
}
- }
+ }
if( postProcessSuccess ){
return doAddInstantiation( sf_tmp.d_subs, sf_tmp.d_vars );
}else{
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;
+ }
+ //}
}
}
}
}
}
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 );
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 ){
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;
}
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() );
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;
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 );
CegqiOutput * getOutput() { return d_out; }
//get quantifiers engine
QuantifiersEngine* getQuantifiersEngine() { return d_qe; }
-
+
//interface for instantiators
public:
void pushStackVariable( Node v );
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; }
};
-
// an instantiator for individual variables
// will make calls into CegInstantiator::doAddInstantiationInc
class Instantiator {
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"; }
};
**
** \brief Implementation of theory-specific counterexample-guided quantifier instantiation
**/
-
+
#include "theory/quantifiers/ceg_t_instantiator.h"
#include "options/quantifiers_options.h"
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;
}
//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;
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 );
}
}
};
-
+
bool EprInstantiator::processEqualTerms( CegInstantiator * ci, SolvedForm& sf, Node pv, std::vector< Node >& eqc, unsigned effort ) {
if( options::quantEprMatching() ){
//heuristic for best matching constant
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<lit.getNumChildren(); i++ ){
+ unsigned ii = ( i + rmod )%lit.getNumChildren();
+ Node litc = getPathToPv( lit[ii], pv, sv, path, visited );
+ if( !litc.isNull() ){
+ // path is outermost term index last
+ path.push_back( ii );
+ std::vector< Node > children;
+ if( lit.getMetaKind() == kind::metakind::PARAMETERIZED ){
+ children.push_back( lit.getOperator() );
+ }
+ for( unsigned j=0; j<lit.getNumChildren(); j++ ){
+ children.push_back( j==ii ? litc : lit[j] );
+ }
+ return NodeManager::currentNM()->mkNode( 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( index<sv_t.getNumChildren() );
+ path.pop_back();
+ Kind k = sv_t.getKind();
+ // inversions
+ if( k==BITVECTOR_PLUS ){
+ t = NodeManager::currentNM()->mkNode( 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( index<lit.getNumChildren() );
+ path.pop_back();
+ Kind k = lit.getKind();
+ if( k==NOT ){
+ Assert( index==0 );
+ return solve_bv_lit( sv, lit[index], !pol, path, m, status );
+ }else if( k==EQUAL ){
+ return solve_bv_constraint( sv, lit[index], lit[1-index], k, pol, path, m, status );
+ }else if( k==BITVECTOR_ULT || k==BITVECTOR_ULE || k==BITVECTOR_SLT || k==BITVECTOR_SLE ){
+ if( !pol ){
+ if( k==BITVECTOR_ULT ){
+ k = index==1 ? BITVECTOR_ULE : BITVECTOR_UGE;
+ }else if( k==BITVECTOR_ULE ){
+ k = index==1 ? BITVECTOR_ULT : BITVECTOR_UGT;
+ }else if( k==BITVECTOR_SLT ){
+ k = index==1 ? BITVECTOR_SLE : BITVECTOR_SGE;
+ }else{
+ Assert( k==BITVECTOR_SLE );
+ k = index==1 ? BITVECTOR_SLT : BITVECTOR_SGT;
+ }
+ }else if( index==1 ){
+ if( k==BITVECTOR_ULT ){
+ k = BITVECTOR_UGT;
+ }else if( k==BITVECTOR_ULE ){
+ k = BITVECTOR_UGE;
+ }else if( k==BITVECTOR_SLT ){
+ k = BITVECTOR_SGT;
+ }else{
+ Assert( k==BITVECTOR_SLE );
+ k = BITVECTOR_SGE;
+ }
+ }
+ return solve_bv_constraint( sv, lit[index], lit[1-index], k, true, path, m, status );
+ }else{
+ Trace("bv-invert") << "bv-invert : Unknown kind for bit-vector literal " << lit << std::endl;
+ }
+ 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();
+}
+
+class CegInstantiatorBvInverterModelQuery : public BvInverterModelQuery {
+protected:
+ CegInstantiator * d_ci;
+public:
+ CegInstantiatorBvInverterModelQuery( CegInstantiator * ci ) :
+ BvInverterModelQuery(), d_ci( ci ){}
+ Node getModelValue( Node n ) {
+ return d_ci->getModelValue( 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++ ){
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<BitVectorSize>(), 1) );
}
if( doAddInstantiationInc( pv, uval, veq_c, 0, sf, effort ) ){
}
}
*/
+}
+
+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; j<iti->second.size(); j++ ){
+ Trace("bv-inst") << "[" << j << "] : " << iti->second[j];
+ // print information about solved status TODO
+
+ Trace("bv-inst") << std::endl;
+ }
+ }
+
+ return false;
+}
#include "theory/quantifiers/ceg_instantiator.h"
+#include <unordered_set>
+
namespace CVC4 {
namespace theory {
namespace quantifiers {
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 );
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 <rk> 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"; }
};
projects / cvc5.git / commitdiff