success = true;
}
}
- }while( !success && index<32 );
+ }while( !qe->inConflict() && !success && index<32 );
//mark if we are incomplete
osuccess = osuccess && success;
}
namespace CVC4 {
-bool CegqiOutputSingleInv::addInstantiation( std::vector< Node >& subs ) {
- return d_out->addInstantiation( subs );
+bool CegqiOutputSingleInv::doAddInstantiation( std::vector< Node >& subs ) {
+ return d_out->doAddInstantiation( subs );
}
bool CegqiOutputSingleInv::isEligibleForInstantiation( Node n ) {
}
d_cosi = new CegqiOutputSingleInv( this );
// third and fourth arguments set to (false,false) until we have solution reconstruction for delta and infinity
- d_cinst = new CegInstantiator( d_qe, d_cosi, false, false );
+ d_cinst = new CegInstantiator( d_qe, d_cosi, false, false );
d_sol = new CegConjectureSingleInvSol( qe );
d_sip = new SingleInvocationPartition;
-
+
if( options::cegqiSingleInvPartial() ){
d_ei = new CegEntailmentInfer( qe, d_sip );
}else{
if( d_cinst ){
delete d_cinst;
}
- d_cinst = new CegInstantiator( d_qe, d_cosi, false, false );
+ d_cinst = new CegInstantiator( d_qe, d_cosi, false, false );
d_cinst->registerCounterexampleLemma( lems, d_single_inv_sk );
}
}
if( d_single_inv.isNull() ){
if( d_ei->getEntailedConjecture( d_single_inv, d_single_inv_exp ) ){
Trace("cegqi-nsi") << "NSI : got : " << d_single_inv << std::endl;
- Trace("cegqi-nsi") << "NSI : exp : " << d_single_inv_exp << std::endl;
+ Trace("cegqi-nsi") << "NSI : exp : " << d_single_inv_exp << std::endl;
}else{
Trace("cegqi-nsi") << "NSI : failed to construct next conjecture." << std::endl;
Notice() << "Incomplete due to --cegqi-si-partial." << std::endl;
Trace("cegqi-nsi") << "NSI : have : " << d_single_inv << std::endl;
Assert( d_single_inv_exp.isNull() );
}
-
+
d_si_guard = Node::null();
d_ns_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "GS", NodeManager::currentNM()->booleanType() ) );
d_ns_guard = d_qe->getValuation().ensureLiteral( d_ns_guard );
Trace("cegqi-nsi") << "NSI : conjecture is " << d_single_inv << std::endl;
}
-bool CegConjectureSingleInv::addInstantiation( std::vector< Node >& subs ){
+bool CegConjectureSingleInv::doAddInstantiation( std::vector< Node >& subs ){
std::stringstream siss;
if( Trace.isOn("cegqi-si-inst-debug") || Trace.isOn("cegqi-engine") ){
siss << " * single invocation: " << std::endl;
std::vector< TypeNode > typs;
std::map< Node, bool > visited;
if( inferArgTypes( n, typs, visited ) ){
- return init( typs, n );
+ return init( typs, n );
}else{
Trace("si-prt") << "Could not infer argument types." << std::endl;
return false;
CegqiOutputSingleInv( CegConjectureSingleInv * out ) : d_out( out ){}
~CegqiOutputSingleInv() {}
CegConjectureSingleInv * d_out;
- bool addInstantiation( std::vector< Node >& subs );
+ bool doAddInstantiation( std::vector< Node >& subs );
bool isEligibleForInstantiation( Node n );
bool addLemma( Node lem );
};
private:
std::vector< Node > d_curr_lemmas;
//add instantiation
- bool addInstantiation( std::vector< Node >& subs );
+ bool doAddInstantiation( std::vector< Node >& subs );
//is eligible for instantiation
bool isEligibleForInstantiation( Node n );
// add lemma
}
}
-bool CegInstantiator::addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars,
- std::vector< int >& btyp, Node theta, unsigned i, unsigned effort,
- std::map< Node, Node >& cons, std::vector< Node >& curr_var ){
+bool CegInstantiator::doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars,
+ std::vector< int >& btyp, Node theta, unsigned i, unsigned effort,
+ std::map< Node, Node >& cons, std::vector< Node >& curr_var ){
if( i==d_vars.size() ){
//solved for all variables, now construct instantiation
if( !sf.d_has_coeff.empty() ){
//use symbolic solved forms
SolvedForm csf;
csf.copy( ssf );
- return addInstantiationCoeff( csf, vars, btyp, 0, cons );
+ return doAddInstantiationCoeff( csf, vars, btyp, 0, cons );
}else{
- return addInstantiationCoeff( sf, vars, btyp, 0, cons );
+ return doAddInstantiationCoeff( sf, vars, btyp, 0, cons );
}
}else{
- return addInstantiation( sf.d_subs, vars, cons );
+ return doAddInstantiation( sf.d_subs, vars, cons );
}
}else{
std::map< Node, std::map< Node, bool > > subs_proc;
if( proc ){
//try the substitution
subs_proc[ns][pv_coeff] = true;
- if( addInstantiationInc( ns, pv, pv_coeff, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
+ if( doAddInstantiationInc( ns, pv, pv_coeff, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
return true;
}
}
for( unsigned j=0; j<dt[cindex].getNumArgs(); j++ ){
curr_var.push_back( NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex][j].getSelector() ), pv ) );
}
- if( addInstantiation( sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
+ if( doAddInstantiation( sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
return true;
}else{
//cleanup
Node val = veq[1];
if( subs_proc[val].find( veq_c )==subs_proc[val].end() ){
subs_proc[val][veq_c] = true;
- if( addInstantiationInc( val, pv, veq_c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
+ if( doAddInstantiationInc( val, pv, veq_c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
return true;
}
}
if( success ){
if( subs_proc[val].find( veq_c )==subs_proc[val].end() ){
subs_proc[val][veq_c] = true;
- if( addInstantiationInc( val, pv, veq_c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
+ if( doAddInstantiationInc( val, pv, veq_c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
return true;
}
}
//try this bound
if( subs_proc[uval].find( veq_c )==subs_proc[uval].end() ){
subs_proc[uval][veq_c] = true;
- if( addInstantiationInc( uval, pv, veq_c, uires>0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
+ if( doAddInstantiationInc( uval, pv, veq_c, uires>0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
return true;
}
}
val = NodeManager::currentNM()->mkNode( UMINUS, val );
val = Rewriter::rewrite( val );
}
- if( addInstantiationInc( val, pv, Node::null(), 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
+ if( doAddInstantiationInc( val, pv, Node::null(), 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
return true;
}
}
if( !val.isNull() ){
if( subs_proc[val].find( mbp_coeff[rr][best] )==subs_proc[val].end() ){
subs_proc[val][mbp_coeff[rr][best]] = true;
- if( addInstantiationInc( val, pv, mbp_coeff[rr][best], rr==0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
+ if( doAddInstantiationInc( val, pv, mbp_coeff[rr][best], rr==0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
return true;
}
}
if( !val.isNull() ){
if( subs_proc[val].find( c )==subs_proc[val].end() ){
subs_proc[val][c] = true;
- if( addInstantiationInc( val, pv, c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
+ if( doAddInstantiationInc( val, pv, c, 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
return true;
}
}
if( !val.isNull() ){
if( subs_proc[val].find( Node::null() )==subs_proc[val].end() ){
subs_proc[val][Node::null()] = true;
- if( addInstantiationInc( val, pv, Node::null(), 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
+ if( doAddInstantiationInc( val, pv, Node::null(), 0, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
return true;
}
}
if( !val.isNull() ){
if( subs_proc[val].find( mbp_coeff[rr][j] )==subs_proc[val].end() ){
subs_proc[val][mbp_coeff[rr][j]] = true;
- if( addInstantiationInc( val, pv, mbp_coeff[rr][j], rr==0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
+ if( doAddInstantiationInc( val, pv, mbp_coeff[rr][j], rr==0 ? 1 : -1, sf, ssf, vars, btyp, theta, i, effort, cons, curr_var ) ){
return true;
}
}
//we only resort to values in the case of booleans
Assert( ( pvtn.isInteger() ? !options::cbqiUseInfInt() : !options::cbqiUseInfReal() ) || pvtn.isBoolean() );
#endif
- if( addInstantiationInc( mv, pv, pv_coeff_m, 0, sf, ssf, vars, btyp, theta, i, new_effort, cons, curr_var ) ){
+ if( doAddInstantiationInc( mv, pv, pv_coeff_m, 0, sf, ssf, vars, btyp, theta, i, new_effort, cons, curr_var ) ){
return true;
}
}
}
-bool CegInstantiator::addInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars,
- std::vector< int >& btyp, Node theta, unsigned i, unsigned effort,
- std::map< Node, Node >& cons, std::vector< Node >& curr_var ) {
+bool CegInstantiator::doAddInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars,
+ std::vector< int >& btyp, Node theta, unsigned i, unsigned effort,
+ std::map< Node, Node >& cons, std::vector< Node >& curr_var ) {
if( Trace.isOn("cbqi-inst") ){
for( unsigned j=0; j<sf.d_subs.size(); j++ ){
Trace("cbqi-inst") << " ";
curr_var.pop_back();
is_cv = true;
}
- success = addInstantiation( sf, ssf, vars, btyp, new_theta, curr_var.empty() ? i+1 : i, effort, cons, curr_var );
+ success = doAddInstantiation( sf, ssf, vars, btyp, new_theta, curr_var.empty() ? i+1 : i, effort, cons, curr_var );
if( !success ){
if( is_cv ){
curr_var.push_back( pv );
}
}
-bool CegInstantiator::addInstantiationCoeff( SolvedForm& sf, std::vector< Node >& vars, std::vector< int >& btyp,
+bool CegInstantiator::doAddInstantiationCoeff( SolvedForm& sf, std::vector< Node >& vars, std::vector< int >& btyp,
unsigned j, std::map< Node, Node >& cons ) {
if( j==sf.d_has_coeff.size() ){
- return addInstantiation( sf.d_subs, vars, cons );
+ return doAddInstantiation( sf.d_subs, vars, cons );
}else{
Assert( std::find( vars.begin(), vars.end(), sf.d_has_coeff[j] )!=vars.end() );
unsigned index = std::find( vars.begin(), vars.end(), sf.d_has_coeff[j] )-vars.begin();
}
}
}
- if( addInstantiationCoeff( sf, vars, btyp, j+1, cons ) ){
+ if( doAddInstantiationCoeff( sf, vars, btyp, j+1, cons ) ){
return true;
}
}
}
}
-bool CegInstantiator::addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::map< Node, Node >& cons ) {
+bool CegInstantiator::doAddInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::map< Node, Node >& cons ) {
if( vars.size()>d_vars.size() ){
Trace("cbqi-inst-debug") << "Reconstructing instantiations...." << std::endl;
std::map< Node, Node > subs_map;
subs.push_back( subs_orig[d_var_order_index[i]] );
}
}
- bool ret = d_out->addInstantiation( subs );
+ bool ret = d_out->doAddInstantiation( subs );
#ifdef MBP_STRICT_ASSERTIONS
Assert( ret );
#endif
std::map< Node, Node > cons;
std::vector< Node > curr_var;
//try to add an instantiation
- if( addInstantiation( sf, ssf, vars, btyp, theta, 0, r==0 ? 0 : 2, cons, curr_var ) ){
+ if( doAddInstantiation( sf, ssf, vars, btyp, theta, 0, r==0 ? 0 : 2, cons, curr_var ) ){
return true;
}
}
}
}
-//this isolates the atom into solved form
+//this isolates the atom into solved form
// veq_c * pv <> val + vts_coeff_delta * delta + vts_coeff_inf * inf
// ensures val is Int if pv is Int, and val does not contain vts symbols
int CegInstantiator::solve_arith( Node pv, Node atom, Node& veq_c, Node& val, Node& vts_coeff_inf, Node& vts_coeff_delta ) {
class CegqiOutput {
public:
virtual ~CegqiOutput() {}
- virtual bool addInstantiation( std::vector< Node >& subs ) = 0;
+ virtual bool doAddInstantiation( std::vector< Node >& subs ) = 0;
virtual bool isEligibleForInstantiation( Node n ) = 0;
virtual bool addLemma( Node lem ) = 0;
};
};
*/
// effort=0 : do not use model value, 1: use model value, 2: one must use model value
- bool addInstantiation( SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars,
+ bool doAddInstantiation( SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars,
std::vector< int >& btyp, Node theta, unsigned i, unsigned effort,
std::map< Node, Node >& cons, std::vector< Node >& curr_var );
- bool addInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars,
+ bool doAddInstantiationInc( Node n, Node pv, Node pv_coeff, int bt, SolvedForm& sf, SolvedForm& ssf, std::vector< Node >& vars,
std::vector< int >& btyp, Node theta, unsigned i, unsigned effort,
std::map< Node, Node >& cons, std::vector< Node >& curr_var );
- bool addInstantiationCoeff( SolvedForm& sf,
+ bool doAddInstantiationCoeff( SolvedForm& sf,
std::vector< Node >& vars, std::vector< int >& btyp,
unsigned j, std::map< Node, Node >& cons );
- bool addInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::map< Node, Node >& cons );
+ bool doAddInstantiation( std::vector< Node >& subs, std::vector< Node >& vars, std::map< Node, Node >& cons );
Node constructInstantiation( Node n, std::map< Node, Node >& subs_map, std::map< Node, Node >& cons );
Node applySubstitution( TypeNode tn, Node n, SolvedForm& sf, std::vector< Node >& vars, Node& pv_coeff, bool try_coeff = true ) {
return applySubstitution( tn, n, sf.d_subs, sf.d_coeff, sf.d_has_coeff, vars, pv_coeff, try_coeff );
bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) {
Trace("fmc") << "Full model check " << f << ", effort = " << effort << "..." << std::endl;
+ Assert( !d_qe->inConflict() );
if( optUseModel() ){
FirstOrderModelFmc * fmfmc = fm->asFirstOrderModelFmc();
if (effort==0) {
if( d_qe->addInstantiation( f, inst ) ){
Trace("fmc-debug-inst") << "** Added instantiation." << std::endl;
d_addedLemmas++;
- if( options::fmfOneInstPerRound() ){
+ if( d_qe->inConflict() || options::fmfOneInstPerRound() ){
break;
}
}else{
if( d_qe->addInstantiation( f, inst ) ){
Trace("fmc-exh-debug") << " ...success.";
addedLemmas++;
- if( options::fmfOneInstPerRound() ){
+ if( d_qe->inConflict() || options::fmfOneInstPerRound() ){
break;
}
}else{
return ret;
}
}
- /*
- //check if m is an instance of another instantiation if modInst is true
- if( modInst ){
- if( !n.isNull() ){
- Node nl;
- std::map< Node, InstMatchTrie >::iterator itm = d_data.find( nl );
- if( itm!=d_data.end() ){
- if( !itm->second.addInstMatch( qe, f, m, modEq, modInst, imtio, true, index+1 ) ){
- return false;
- }
- }
- }
- }
- */
if( modEq ){
//check modulo equality if any other instantiation match exists
if( !n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){
}
}
+bool InstMatchTrie::removeInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, ImtIndexOrder* imtio, int index ) {
+ Assert( index<(int)q[0].getNumChildren() );
+ Assert( !imtio || index<(int)imtio->d_order.size() );
+ int i_index = imtio ? imtio->d_order[index] : index;
+ Node n = m[i_index];
+ std::map< Node, InstMatchTrie >::iterator it = d_data.find( n );
+ if( it!=d_data.end() ){
+ if( (index+1)==(int)q[0].getNumChildren() || ( imtio && (index+1)==(int)imtio->d_order.size() ) ){
+ d_data.erase( n );
+ return true;
+ }else{
+ return it->second.removeInstMatch( qe, q, m, imtio, index+1 );
+ }
+ }else{
+ return false;
+ }
+}
+
void InstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& terms ) const {
if( terms.size()==q[0].getNumChildren() ){
out << " ( ";
return reset || ret;
}
}
- //check if m is an instance of another instantiation if modInst is true
- /*
- if( modInst ){
- if( !n.isNull() ){
- Node nl;
- std::map< Node, CDInstMatchTrie* >::iterator itm = d_data.find( nl );
- if( itm!=d_data.end() ){
- if( !itm->second->addInstMatch( qe, f, m, c, modEq, modInst, index+1, true ) ){
- return false;
- }
- }
- }
- }
- */
if( modEq ){
//check modulo equality if any other instantiation match exists
if( !n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){
}
}
+bool CDInstMatchTrie::removeInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, int index ) {
+ if( index==(int)q[0].getNumChildren() ){
+ if( d_valid.get() ){
+ d_valid.set( false );
+ return true;
+ }else{
+ return false;
+ }
+ }else{
+ Node n = m[index];
+ std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n );
+ if( it!=d_data.end() ){
+ return it->second->removeInstMatch( qe, q, m, index+1 );
+ }else{
+ return false;
+ }
+ }
+}
+
void CDInstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& terms ) const{
if( d_valid.get() ){
if( terms.size()==q[0].getNumChildren() ){
}
bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false,
bool modInst = false, ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 );
+ bool removeInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, ImtIndexOrder* imtio = NULL, int index = 0 );
void print( std::ostream& out, Node q ) const{
std::vector< TNode > terms;
print( out, q, terms );
modEq is if we check modulo equality
modInst is if we return true if m is an instance of a match that exists
*/
- bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, context::Context* c, bool modEq = false,
+ bool existsInstMatch( QuantifiersEngine* qe, Node q, InstMatch& m, context::Context* c, bool modEq = false,
bool modInst = false, int index = 0 ) {
- return !addInstMatch( qe, f, m, c, modEq, modInst, index, true );
+ return !addInstMatch( qe, q, m, c, modEq, modInst, index, true );
}
- bool existsInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, context::Context* c, bool modEq = false,
+ bool existsInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, context::Context* c, bool modEq = false,
bool modInst = false, int index = 0 ) {
- return !addInstMatch( qe, f, m, c, modEq, modInst, index, true );
+ return !addInstMatch( qe, q, m, c, modEq, modInst, index, true );
}
/** add match m for quantifier f, take into account equalities if modEq = true,
if imtio is non-null, this is the order to add to trie
return true if successful
*/
- bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, context::Context* c, bool modEq = false,
+ bool addInstMatch( QuantifiersEngine* qe, Node q, InstMatch& m, context::Context* c, bool modEq = false,
bool modInst = false, int index = 0, bool onlyExist = false ) {
- return addInstMatch( qe, f, m.d_vals, c, modEq, modInst, index, onlyExist );
+ return addInstMatch( qe, q, m.d_vals, c, modEq, modInst, index, onlyExist );
}
- bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, context::Context* c, bool modEq = false,
+ bool addInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, context::Context* c, bool modEq = false,
bool modInst = false, int index = 0, bool onlyExist = false );
+ bool removeInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, int index = 0 );
void print( std::ostream& out, Node q ) const{
std::vector< TNode > terms;
print( out, q, terms );
if( d_pattern.getKind()==NOT && ( d_pattern[0].getKind()==IFF || d_pattern[0].getKind()==EQUAL ) ){
((inst::CandidateGeneratorQE*)d_cg)->excludeEqc( d_eq_class_rel );
d_eq_class_rel = Node::null();
- }
+ }
}else if( d_match_pattern.getKind()==INST_CONSTANT ){
if( d_pattern.getKind()==APPLY_SELECTOR_TOTAL ){
Expr selectorExpr = qe->getTermDatabase()->getMatchOperator( d_pattern ).toExpr();
}else{
d_cg = new CandidateGeneratorQEAll( qe, d_match_pattern );
}
- }else if( ( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ) &&
+ }else if( ( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ) &&
d_match_pattern[0].getKind()==INST_CONSTANT && d_match_pattern[1].getKind()==INST_CONSTANT ){
//we will be producing candidates via literal matching heuristics
if( d_pattern.getKind()!=NOT ){
}
bool InstMatchGenerator::getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ){
+ if( qe->inConflict() ){
+ return false;
+ }
if( d_needsReset ){
Trace("matching") << "Reset not done yet, must do the reset..." << std::endl;
reset( d_eq_class, qe );
m.setValue( v, t);
addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) );
m.setValue( v, prev);
+ if( qe->inConflict() ){
+ break;
+ }
}
}
return;
}
}
- Node r = qe->getEqualityQuery()->getRepresentative( d_match_pattern[argIndex] );
- std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.find( r );
- if( it!=tat->d_data.end() ){
- addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) );
+ if( !qe->inConflict() ){
+ Node r = qe->getEqualityQuery()->getRepresentative( d_match_pattern[argIndex] );
+ std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.find( r );
+ if( it!=tat->d_data.end() ){
+ addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) );
+ }
}
}
}
-/********************* */\r
-/*! \file inst_propagator.cpp\r
- ** \verbatim\r
- ** Top contributors (to current version):\r
- ** Andrew Reynolds\r
- ** This file is part of the CVC4 project.\r
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS\r
- ** in the top-level source directory) and their institutional affiliations.\r
- ** All rights reserved. See the file COPYING in the top-level source\r
- ** directory for licensing information.\endverbatim\r
- **\r
- ** Propagate mechanism for instantiations\r
- **/\r
-\r
-#include <vector>\r
-\r
-#include "theory/quantifiers/inst_propagator.h"\r
-#include "theory/rewriter.h"\r
-#include "theory/quantifiers/term_database.h"\r
-\r
-using namespace CVC4;\r
-using namespace std;\r
-using namespace CVC4::theory;\r
-using namespace CVC4::theory::quantifiers;\r
-using namespace CVC4::kind;\r
-\r
-\r
-EqualityQueryInstProp::EqualityQueryInstProp( QuantifiersEngine* qe ) : d_qe( qe ){\r
- d_true = NodeManager::currentNM()->mkConst( true );\r
- d_false = NodeManager::currentNM()->mkConst( false );\r
-}\r
-\r
-bool EqualityQueryInstProp::reset( Theory::Effort e ) {\r
- d_uf.clear();\r
- d_uf_exp.clear();\r
- d_diseq_list.clear();\r
- return true;\r
-}\r
-\r
-/** contains term */\r
-bool EqualityQueryInstProp::hasTerm( Node a ) {\r
- if( getEngine()->hasTerm( a ) ){\r
- return true;\r
- }else{\r
- std::vector< Node > exp;\r
- Node ar = getUfRepresentative( a, exp );\r
- return !ar.isNull() && getEngine()->hasTerm( ar );\r
- }\r
-}\r
-\r
-/** get the representative of the equivalence class of a */\r
-Node EqualityQueryInstProp::getRepresentative( Node a ) {\r
- if( getEngine()->hasTerm( a ) ){\r
- a = getEngine()->getRepresentative( a );\r
- }\r
- std::vector< Node > exp;\r
- Node ar = getUfRepresentative( a, exp );\r
- return ar.isNull() ? a : ar;\r
-}\r
-\r
-/** returns true if a and b are equal in the current context */\r
-bool EqualityQueryInstProp::areEqual( Node a, Node b ) {\r
- if( a==b ){\r
- return true;\r
- }else{\r
- eq::EqualityEngine* ee = getEngine();\r
- if( ee->hasTerm( a ) && ee->hasTerm( b ) ){\r
- if( ee->areEqual( a, b ) ){\r
- return true;\r
- }\r
- }\r
- return false;\r
- }\r
-}\r
-\r
-/** returns true is a and b are disequal in the current context */\r
-bool EqualityQueryInstProp::areDisequal( Node a, Node b ) {\r
- if( a==b ){\r
- return true;\r
- }else{\r
- eq::EqualityEngine* ee = getEngine();\r
- if( ee->hasTerm( a ) && ee->hasTerm( b ) ){\r
- if( ee->areDisequal( a, b, false ) ){\r
- return true;\r
- }\r
- }\r
- return false;\r
- }\r
-}\r
-\r
-/** get the equality engine associated with this query */\r
-eq::EqualityEngine* EqualityQueryInstProp::getEngine() {\r
- return d_qe->getMasterEqualityEngine();\r
-}\r
-\r
-/** get the equivalence class of a */\r
-void EqualityQueryInstProp::getEquivalenceClass( Node a, std::vector< Node >& eqc ) {\r
- //TODO?\r
-}\r
-\r
-TNode EqualityQueryInstProp::getCongruentTerm( Node f, std::vector< TNode >& args ) {\r
- TNode t = d_qe->getTermDatabase()->getCongruentTerm( f, args );\r
- if( !t.isNull() ){\r
- return t;\r
- }else{\r
- //TODO?\r
- return TNode::null();\r
- }\r
-}\r
-\r
-Node EqualityQueryInstProp::getRepresentativeExp( Node a, std::vector< Node >& exp ) {\r
- bool engine_has_a = getEngine()->hasTerm( a );\r
- if( engine_has_a ){\r
- a = getEngine()->getRepresentative( a );\r
- }\r
- //get union find representative, if this occurs in the equality engine, return it\r
- unsigned prev_size = exp.size();\r
- Node ar = getUfRepresentative( a, exp );\r
- if( !ar.isNull() ){\r
- if( engine_has_a || getEngine()->hasTerm( ar ) ){\r
- Assert( getEngine()->hasTerm( ar ) );\r
- Assert( getEngine()->getRepresentative( ar )==ar );\r
- return ar;\r
- }\r
- }else{\r
- if( engine_has_a ){\r
- return a;\r
- }\r
- }\r
- //retract explanation\r
- while( exp.size()>prev_size ){\r
- exp.pop_back();\r
- }\r
- return Node::null();\r
-}\r
-\r
-bool EqualityQueryInstProp::areEqualExp( Node a, Node b, std::vector< Node >& exp ) {\r
- if( areEqual( a, b ) ){\r
- return true;\r
- }else{\r
- std::vector< Node > exp_a;\r
- Node ar = getUfRepresentative( a, exp_a );\r
- if( !ar.isNull() ){\r
- std::vector< Node > exp_b;\r
- if( ar==getUfRepresentative( b, exp_b ) ){\r
- merge_exp( exp, exp_a );\r
- merge_exp( exp, exp_b );\r
- return true;\r
- }\r
- }\r
- return false;\r
- }\r
-}\r
-\r
-bool EqualityQueryInstProp::areDisequalExp( Node a, Node b, std::vector< Node >& exp ) {\r
- if( areDisequal( a, b ) ){\r
- return true;\r
- }else{\r
- //TODO?\r
- return false;\r
- }\r
-}\r
-\r
-Node EqualityQueryInstProp::getUfRepresentative( Node a, std::vector< Node >& exp ) {\r
- Assert( exp.empty() );\r
- std::map< Node, Node >::iterator it = d_uf.find( a );\r
- if( it!=d_uf.end() ){\r
- if( it->second==a ){\r
- Assert( d_uf_exp[ a ].empty() );\r
- return it->second;\r
- }else{\r
- Node m = getUfRepresentative( it->second, exp );\r
- Assert( !m.isNull() );\r
- if( m!=it->second ){\r
- //update union find\r
- d_uf[ a ] = m;\r
- //update explanation : merge the explanation of the parent\r
- merge_exp( d_uf_exp[ a ], exp );\r
- Trace("qip-eq") << "EqualityQueryInstProp::getUfRepresentative : merge " << a << " -> " << m << ", exp size=" << d_uf_exp[ a ].size() << std::endl;\r
- }\r
- //add current explanation to exp: note that exp is a subset of d_uf_exp[ a ], reset\r
- exp.clear();\r
- exp.insert( exp.end(), d_uf_exp[ a ].begin(), d_uf_exp[ a ].end() );\r
- return m;\r
- }\r
- }else{\r
- return Node::null();\r
- }\r
-}\r
-\r
-// set a == b with reason, return status, modify a and b to representatives pre-merge\r
-int EqualityQueryInstProp::setEqual( Node& a, Node& b, std::vector< Node >& reason ) {\r
- int status = STATUS_MERGED_UNKNOWN;\r
- Trace("qip-eq") << "EqualityQueryInstProp::setEqual " << a << ", " << b << ", reason size = " << reason.size() << std::endl;\r
- //get the representative for a\r
- std::vector< Node > exp_a;\r
- Node ar = getUfRepresentative( a, exp_a );\r
- if( ar.isNull() ){\r
- Assert( exp_a.empty() );\r
- ar = a;\r
- }\r
- if( ar==b ){\r
- Trace("qip-eq") << "EqualityQueryInstProp::setEqual : already equal" << std::endl;\r
- return STATUS_NONE;\r
- }\r
- bool swap = false;\r
- //get the representative for b\r
- std::vector< Node > exp_b;\r
- Node br = getUfRepresentative( b, exp_b );\r
- if( br.isNull() ){\r
- Assert( exp_b.empty() );\r
- br = b;\r
- if( !getEngine()->hasTerm( br ) ){\r
- if( ar!=a ){\r
- swap = true;\r
- }\r
- }else{\r
- if( getEngine()->hasTerm( ar ) ){\r
- status = STATUS_MERGED_KNOWN;\r
- }\r
- }\r
- }else{\r
- if( ar==br ){\r
- Trace("qip-eq") << "EqualityQueryInstProp::setEqual : already equal" << std::endl;\r
- return STATUS_NONE;\r
- }else if( getEngine()->hasTerm( ar ) ){\r
- if( getEngine()->hasTerm( br ) ){\r
- status = STATUS_MERGED_KNOWN;\r
- }else{\r
- swap = true;\r
- }\r
- }\r
- }\r
- if( swap ){\r
- //swap\r
- Node temp_r = ar;\r
- ar = br;\r
- br = temp_r;\r
- }\r
-\r
- Assert( ar!=br );\r
- Assert( !getEngine()->hasTerm( ar ) || getEngine()->hasTerm( br ) );\r
-\r
- //update the union find\r
- Assert( d_uf_exp[ar].empty() );\r
- Assert( d_uf_exp[br].empty() );\r
-\r
- d_uf[ar] = br;\r
- merge_exp( d_uf_exp[ar], exp_a );\r
- merge_exp( d_uf_exp[ar], exp_b );\r
- merge_exp( d_uf_exp[ar], reason );\r
-\r
- d_uf[br] = br;\r
- d_uf_exp[br].clear();\r
-\r
- Trace("qip-eq") << "EqualityQueryInstProp::setEqual : merge " << ar << " -> " << br << ", exp size = " << d_uf_exp[ar].size() << ", status = " << status << std::endl;\r
- a = ar;\r
- b = br;\r
- return status;\r
-}\r
-\r
-\r
-void EqualityQueryInstProp::addArgument( std::vector< TNode >& args, std::vector< TNode >& props, Node n, bool is_prop, bool pol ) {\r
- if( is_prop ){\r
- if( isLiteral( n ) ){\r
- props.push_back( pol ? n : n.negate() );\r
- return;\r
- }\r
- }\r
- args.push_back( n );\r
-}\r
-\r
-bool EqualityQueryInstProp::isLiteral( Node n ) {\r
- Kind ak = n.getKind()==NOT ? n[0].getKind() : n.getKind();\r
- Assert( ak!=NOT );\r
- return ak!=AND && ak!=OR && ak!=IFF && ak!=ITE;\r
-}\r
-\r
-//this is identical to TermDb::evaluateTerm2, but tracks more information\r
-Node EqualityQueryInstProp::evaluateTermExp( TNode n, std::vector< Node >& exp, std::map< TNode, Node >& visited, bool hasPol, bool pol,\r
- std::map< Node, bool >& watch_list_out, std::vector< TNode >& props ) {\r
- std::map< TNode, Node >::iterator itv = visited.find( n );\r
- if( itv != visited.end() ){\r
- return itv->second;\r
- }else{\r
- Trace("term-db-eval") << "evaluate term : " << n << std::endl;\r
- std::vector< Node > exp_n;\r
- Node ret = getRepresentativeExp( n, exp_n );\r
- if( ret.isNull() ){\r
- //term is not known to be equal to a representative in equality engine, evaluate it\r
- Kind k = n.getKind();\r
- if( k==FORALL ){\r
- ret = Node::null();\r
- }else{\r
- std::map< Node, bool > watch_list_out_curr;\r
- TNode f = d_qe->getTermDatabase()->getMatchOperator( n );\r
- std::vector< TNode > args;\r
- bool ret_set = false;\r
- bool childChanged = false;\r
- int abort_i = -1;\r
- //get the child entailed polarity\r
- Assert( n.getKind()!=IMPLIES );\r
- bool newHasPol, newPol;\r
- QuantPhaseReq::getEntailPolarity( n, 0, hasPol, pol, newHasPol, newPol );\r
- //for each child\r
- for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
- TNode c = evaluateTermExp( n[i], exp, visited, newHasPol, newPol, watch_list_out_curr, props );\r
- if( c.isNull() ){\r
- ret = Node::null();\r
- ret_set = true;\r
- break;\r
- }else if( c==d_true || c==d_false ){\r
- //short-circuiting\r
- if( k==kind::AND || k==kind::OR ){\r
- if( (k==kind::AND)==(c==d_false) ){\r
- ret = c;\r
- ret_set = true;\r
- break;\r
- }else{\r
- //redundant\r
- c = Node::null();\r
- childChanged = true;\r
- }\r
- }else if( k==kind::ITE && i==0 ){\r
- Assert( watch_list_out_curr.empty() );\r
- ret = evaluateTermExp( n[ c==d_true ? 1 : 2], exp, visited, hasPol, pol, watch_list_out_curr, props );\r
- ret_set = true;\r
- break;\r
- }else if( k==kind::NOT ){\r
- ret = c==d_true ? d_false : d_true;\r
- ret_set = true;\r
- break;\r
- }\r
- }\r
- if( !c.isNull() ){\r
- childChanged = childChanged || n[i]!=c;\r
- if( !f.isNull() && !watch_list_out_curr.empty() ){\r
- // we are done if this is an UF application and an argument is unevaluated\r
- args.push_back( c );\r
- abort_i = i;\r
- break;\r
- }else if( ( k==kind::AND || k==kind::OR ) ){\r
- if( c.getKind()==k ){\r
- //flatten\r
- for( unsigned j=0; j<c.getNumChildren(); j++ ){\r
- addArgument( args, props, c[j], newHasPol, newPol );\r
- }\r
- }else{\r
- addArgument( args, props, c, newHasPol, newPol );\r
- }\r
- //if we are in a branching position\r
- if( hasPol && !newHasPol && args.size()>=2 ){\r
- //we are done if at least two args are unevaluated\r
- abort_i = i;\r
- break;\r
- }\r
- }else if( k==kind::ITE ){\r
- //we are done if we are ITE and condition is unevaluated\r
- Assert( i==0 );\r
- args.push_back( c );\r
- abort_i = i;\r
- break;\r
- }else{\r
- args.push_back( c );\r
- }\r
- }\r
- }\r
- //add remaining children if we aborted\r
- if( abort_i!=-1 ){\r
- for( int i=(abort_i+1); i<(int)n.getNumChildren(); i++ ){\r
- args.push_back( n[i] );\r
- }\r
- }\r
- //copy over the watch list\r
- for( std::map< Node, bool >::iterator itc = watch_list_out_curr.begin(); itc != watch_list_out_curr.end(); ++itc ){\r
- watch_list_out[itc->first] = itc->second;\r
- }\r
-\r
- //if we have not short-circuited evaluation\r
- if( !ret_set ){\r
- //if it is an indexed term, return the congruent term\r
- if( !f.isNull() && watch_list_out.empty() ){\r
- Assert( args.size()==n.getNumChildren() );\r
- //args contains terms known by the equality engine\r
- TNode nn = getCongruentTerm( f, args );\r
- Trace("term-db-eval") << " got congruent term " << nn << " from DB for " << n << std::endl;\r
- if( !nn.isNull() ){\r
- //successfully constructed representative in EE\r
- Assert( exp_n.empty() );\r
- ret = getRepresentativeExp( nn, exp_n );\r
- Trace("term-db-eval") << "return rep, exp size = " << exp_n.size() << std::endl;\r
- merge_exp( exp, exp_n );\r
- ret_set = true;\r
- Assert( !ret.isNull() );\r
- }\r
- }\r
- if( !ret_set ){\r
- if( childChanged ){\r
- Trace("term-db-eval") << "return rewrite" << std::endl;\r
- if( ( k==kind::AND || k==kind::OR ) ){\r
- if( args.empty() ){\r
- ret = k==kind::AND ? d_true : d_false;\r
- ret_set = true;\r
- }else if( args.size()==1 ){\r
- ret = args[0];\r
- ret_set = true;\r
- }\r
- }\r
- if( !ret_set ){\r
- Assert( args.size()==n.getNumChildren() );\r
- if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){\r
- args.insert( args.begin(), n.getOperator() );\r
- }\r
- ret = NodeManager::currentNM()->mkNode( k, args );\r
- ret = Rewriter::rewrite( ret );\r
- watch_list_out[ret] = true;\r
- }\r
- }else{\r
- ret = n;\r
- watch_list_out[ret] = true;\r
- }\r
- }\r
- }\r
- }\r
- }else{\r
- Trace("term-db-eval") << "...exists in ee, return rep, exp size = " << exp_n.size() << std::endl;\r
- merge_exp( exp, exp_n );\r
- }\r
- Trace("term-db-eval") << "evaluated term : " << n << ", got : " << ret << ", exp size = " << exp.size() << std::endl;\r
- visited[n] = ret;\r
- return ret;\r
- }\r
-}\r
-\r
-void EqualityQueryInstProp::merge_exp( std::vector< Node >& v, std::vector< Node >& v_to_merge, int up_to_size ) {\r
- //TODO : optimize\r
- if( v.empty() ){\r
- Assert( up_to_size==-1 || up_to_size==(int)v_to_merge.size() );\r
- v.insert( v.end(), v_to_merge.begin(), v_to_merge.end() );\r
- }else{\r
- //std::vector< Node >::iterator v_end = v.end();\r
- up_to_size = up_to_size==-1 ? (int)v_to_merge.size() : up_to_size;\r
- for( int j=0; j<up_to_size; j++ ){\r
- if( std::find( v.begin(), v.end(), v_to_merge[j] )==v.end() ){\r
- v.push_back( v_to_merge[j] );\r
- }\r
- }\r
- }\r
-}\r
-\r
-\r
-void InstPropagator::InstInfo::init( Node q, Node lem, std::vector< Node >& terms, Node body ) {\r
- d_active = true;\r
- //information about the instance\r
- d_q = q;\r
- d_lem = lem;\r
- Assert( d_terms.empty() );\r
- d_terms.insert( d_terms.end(), terms.begin(), terms.end() );\r
- //the current lemma\r
- d_curr = body;\r
- d_curr_exp.push_back( body );\r
-}\r
-\r
-InstPropagator::InstPropagator( QuantifiersEngine* qe ) :\r
-d_qe( qe ), d_notify(*this), d_qy( qe ){\r
-}\r
-\r
-bool InstPropagator::reset( Theory::Effort e ) {\r
- d_icount = 0;\r
- d_ii.clear();\r
- for( unsigned i=0; i<2; i++ ){\r
- d_conc_to_id[i].clear();\r
- }\r
- d_conflict = false;\r
- d_watch_list.clear();\r
- d_relevant_inst.clear();\r
- return d_qy.reset( e );\r
-}\r
-\r
-void InstPropagator::notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) {\r
- if( !d_conflict ){\r
- if( Trace.isOn("qip-prop") ){\r
- Trace("qip-prop") << "InstPropagator:: Notify instantiation " << q << " : " << std::endl;\r
- for( unsigned i=0; i<terms.size(); i++ ){\r
- Trace("qip-prop") << " " << terms[i] << std::endl;\r
- }\r
- }\r
- unsigned id = d_icount;\r
- d_icount++;\r
- Trace("qip-prop") << "...assign id=" << id << std::endl;\r
- d_ii[id].init( q, lem, terms, body );\r
- //initialize the information\r
- if( cacheConclusion( id, body ) ){\r
- Assert( d_update_list.empty() );\r
- d_update_list.push_back( id );\r
- bool firstTime = true;\r
- //update infos in the update list until empty \r
- do {\r
- unsigned uid = d_update_list.back();\r
- d_update_list.pop_back();\r
- if( d_ii[uid].d_active ){\r
- update( uid, d_ii[uid], firstTime );\r
- }\r
- firstTime = false;\r
- }while( !d_update_list.empty() );\r
- }else{\r
- d_ii[id].d_active = false;\r
- Trace("qip-prop") << "...duplicate." << std::endl;\r
- }\r
- }\r
-}\r
-\r
-bool InstPropagator::update( unsigned id, InstInfo& ii, bool firstTime ) {\r
- Assert( !d_conflict );\r
- Assert( ii.d_active );\r
- Trace("qip-prop-debug") << "Update info [" << id << "]..." << std::endl;\r
- //update the evaluation of the current lemma\r
- std::map< TNode, Node > visited;\r
- std::map< Node, bool > watch_list;\r
- std::vector< TNode > props;\r
- Node eval = d_qy.evaluateTermExp( ii.d_curr, ii.d_curr_exp, visited, true, true, watch_list, props );\r
- if( eval.isNull() ){\r
- ii.d_active = false;\r
- }else if( firstTime || eval!=ii.d_curr ){\r
- if( EqualityQueryInstProp::isLiteral( eval ) ){\r
- props.push_back( eval );\r
- eval = d_qy.d_true;\r
- watch_list.clear();\r
- }\r
- if( Trace.isOn("qip-prop") ){\r
- Trace("qip-prop") << "Update info [" << id << "]..." << std::endl;\r
- Trace("qip-prop") << "...updated lemma " << ii.d_curr << " -> " << eval << ", exp = ";\r
- debugPrintExplanation( ii.d_curr_exp, "qip-prop" );\r
- Trace("qip-prop") << std::endl;\r
- Trace("qip-prop") << "...watch list: " << std::endl;\r
- for( std::map< Node, bool >::iterator itw = watch_list.begin(); itw!=watch_list.end(); ++itw ){\r
- Trace("qip-prop") << " " << itw->first << std::endl;\r
- }\r
- Trace("qip-prop") << "...new propagations: " << std::endl;\r
- for( unsigned i=0; i<props.size(); i++ ){\r
- Trace("qip-prop") << " " << props[i] << std::endl;\r
- }\r
- Trace("qip-prop") << std::endl;\r
- }\r
- //determine the status of eval\r
- if( eval==d_qy.d_false ){\r
- Assert( props.empty() );\r
- //we have inferred a conflict\r
- conflict( ii.d_curr_exp );\r
- return false;\r
- }else{\r
- for( unsigned i=0; i<props.size(); i++ ){\r
- //if we haven't propagated this literal yet\r
- if( cacheConclusion( id, props[i], 1 ) ){\r
- Node lit = props[i].getKind()==NOT ? props[i][0] : props[i];\r
- bool pol = props[i].getKind()!=NOT;\r
- if( lit.getKind()==EQUAL ){\r
- propagate( lit[0], lit[1], pol, ii.d_curr_exp );\r
- }else{\r
- propagate( lit, pol ? d_qy.d_true : d_qy.d_false, true, ii.d_curr_exp );\r
- }\r
- if( d_conflict ){\r
- return false;\r
- }\r
- }\r
- }\r
- //if we have not inferred this conclusion yet\r
- if( cacheConclusion( id, eval ) ){\r
- ii.d_curr = eval;\r
- //update the watch list\r
- Trace("qip-prop-debug") << "...updating watch list for [" << id << "], curr is " << ii.d_curr << std::endl;\r
- //Here, we need to be notified of enough terms such that if we are not notified, then update( ii ) will return no propagations.\r
- // Similar to two-watched literals, but since we are in UF, we need to watch all terms on a complete path of two terms.\r
- for( std::map< Node, bool >::iterator itw = watch_list.begin(); itw != watch_list.end(); ++itw ){\r
- d_watch_list[ itw->first ][ id ] = true;\r
- }\r
- }else{\r
- Trace("qip-prop-debug") << "...conclusion is duplicate." << std::endl;\r
- ii.d_active = false;\r
- }\r
- }\r
- }else{\r
- Trace("qip-prop-debug") << "...did not update." << std::endl;\r
- }\r
- Assert( !d_conflict );\r
- return true;\r
-}\r
-\r
-void InstPropagator::propagate( Node a, Node b, bool pol, std::vector< Node >& exp ) {\r
- if( Trace.isOn("qip-propagate") ){\r
- Trace("qip-propagate") << "* Propagate " << a << ( pol ? " == " : " != " ) << b << ", exp = ";\r
- debugPrintExplanation( exp, "qip-propagate" );\r
- Trace("qip-propagate") << "..." << std::endl;\r
- }\r
- if( pol ){\r
- std::vector< Node > exp_d;\r
- if( d_qy.areDisequalExp( a, b, exp_d ) ){\r
- Trace("qip-prop-debug") << "...conflict." << std::endl;\r
- EqualityQueryInstProp::merge_exp( exp, exp_d );\r
- conflict( exp );\r
- }else{\r
- //set equal\r
- int status = d_qy.setEqual( a, b, exp );\r
- if( status==EqualityQueryInstProp::STATUS_NONE ){\r
- Trace("qip-prop-debug") << "...already equal." << std::endl;\r
- return;\r
- }else if( status==EqualityQueryInstProp::STATUS_MERGED_KNOWN ){\r
- Assert( d_qy.getEngine()->hasTerm( a ) );\r
- Assert( d_qy.getEngine()->hasTerm( b ) );\r
- Trace("qip-prop-debug") << "...equality between known terms." << std::endl;\r
- addRelevantInstances( exp, "qip-propagate" );\r
- }\r
- Trace("qip-prop-debug") << "...merging " << a << " and " << b << std::endl;\r
- for( unsigned i=0; i<2; i++ ){\r
- //update terms from watched lists\r
- Node c = i==0 ? a : b;\r
- std::map< Node, std::map< unsigned, bool > >::iterator it = d_watch_list.find( c );\r
- if( it!=d_watch_list.end() ){\r
- Trace("qip-prop-debug") << "...update ids from watch list of " << c << ", size=" << it->second.size() << "..." << std::endl;\r
- for( std::map< unsigned, bool >::iterator itw = it->second.begin(); itw != it->second.end(); ++itw ){\r
- unsigned idw = itw->first;\r
- if( std::find( d_update_list.begin(), d_update_list.end(), idw )==d_update_list.end() ){\r
- Trace("qip-prop-debug") << "...will update " << idw << std::endl;\r
- d_update_list.push_back( idw );\r
- }\r
- }\r
- d_watch_list.erase( c );\r
- }\r
- }\r
- }\r
- }else{\r
- std::vector< Node > exp_e;\r
- if( d_qy.areEqualExp( a, b, exp_e ) ){\r
- EqualityQueryInstProp::merge_exp( exp, exp_e );\r
- conflict( exp );\r
- }else{\r
- //TODO?\r
- }\r
- }\r
-}\r
-\r
-void InstPropagator::conflict( std::vector< Node >& exp ) {\r
- Trace("qip-propagate") << "Conflict, exp size =" << exp.size() << std::endl;\r
- d_conflict = true;\r
- d_relevant_inst.clear();\r
- addRelevantInstances( exp, "qip-propagate" );\r
-}\r
-\r
-bool InstPropagator::cacheConclusion( unsigned id, Node body, int prop_index ) {\r
- Assert( prop_index==0 || prop_index==1 );\r
- //check if the conclusion is non-redundant\r
- if( d_conc_to_id[prop_index].find( body )==d_conc_to_id[prop_index].end() ){\r
- d_conc_to_id[prop_index][body] = id;\r
- return true;\r
- }else{\r
- return false;\r
- }\r
-}\r
-\r
-void InstPropagator::addRelevantInstances( std::vector< Node >& exp, const char * c ) {\r
- for( unsigned i=0; i<exp.size(); i++ ){\r
- Assert( d_conc_to_id[0].find( exp[i] )!=d_conc_to_id[0].end() );\r
- Trace(c) << " relevant instance id : " << d_conc_to_id[0][ exp[i] ] << std::endl;\r
- d_relevant_inst[ d_conc_to_id[0][ exp[i] ] ] = true;\r
- }\r
-}\r
-\r
-void InstPropagator::debugPrintExplanation( std::vector< Node >& exp, const char * c ) {\r
- for( unsigned i=0; i<exp.size(); i++ ){\r
- Assert( d_conc_to_id[0].find( exp[i] )!=d_conc_to_id[0].end() );\r
- Trace(c) << d_conc_to_id[0][ exp[i] ] << " ";\r
- }\r
-}\r
-\r
+/********************* */
+/*! \file inst_propagator.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** Propagate mechanism for instantiations
+ **/
+
+#include <vector>
+
+#include "theory/quantifiers/inst_propagator.h"
+#include "theory/rewriter.h"
+#include "theory/quantifiers/term_database.h"
+
+using namespace CVC4;
+using namespace std;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+using namespace CVC4::kind;
+
+
+EqualityQueryInstProp::EqualityQueryInstProp( QuantifiersEngine* qe ) : d_qe( qe ){
+ d_true = NodeManager::currentNM()->mkConst( true );
+ d_false = NodeManager::currentNM()->mkConst( false );
+}
+
+bool EqualityQueryInstProp::reset( Theory::Effort e ) {
+ d_uf.clear();
+ d_uf_exp.clear();
+ d_diseq_list.clear();
+ return true;
+}
+
+/** contains term */
+bool EqualityQueryInstProp::hasTerm( Node a ) {
+ if( getEngine()->hasTerm( a ) ){
+ return true;
+ }else{
+ std::vector< Node > exp;
+ Node ar = getUfRepresentative( a, exp );
+ return !ar.isNull() && getEngine()->hasTerm( ar );
+ }
+}
+
+/** get the representative of the equivalence class of a */
+Node EqualityQueryInstProp::getRepresentative( Node a ) {
+ if( getEngine()->hasTerm( a ) ){
+ a = getEngine()->getRepresentative( a );
+ }
+ std::vector< Node > exp;
+ Node ar = getUfRepresentative( a, exp );
+ return ar.isNull() ? a : ar;
+}
+
+/** returns true if a and b are equal in the current context */
+bool EqualityQueryInstProp::areEqual( Node a, Node b ) {
+ if( a==b ){
+ return true;
+ }else{
+ eq::EqualityEngine* ee = getEngine();
+ if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
+ if( ee->areEqual( a, b ) ){
+ return true;
+ }
+ }
+ return false;
+ }
+}
+
+/** returns true is a and b are disequal in the current context */
+bool EqualityQueryInstProp::areDisequal( Node a, Node b ) {
+ if( a==b ){
+ return false;
+ }else{
+ eq::EqualityEngine* ee = getEngine();
+ if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
+ if( ee->areDisequal( a, b, false ) ){
+ return true;
+ }
+ }
+ return false;
+ }
+}
+
+/** get the equality engine associated with this query */
+eq::EqualityEngine* EqualityQueryInstProp::getEngine() {
+ return d_qe->getMasterEqualityEngine();
+}
+
+/** get the equivalence class of a */
+void EqualityQueryInstProp::getEquivalenceClass( Node a, std::vector< Node >& eqc ) {
+ //TODO?
+}
+
+TNode EqualityQueryInstProp::getCongruentTerm( Node f, std::vector< TNode >& args ) {
+ TNode t = d_qe->getTermDatabase()->getCongruentTerm( f, args );
+ if( !t.isNull() ){
+ return t;
+ }else{
+ //TODO?
+ return TNode::null();
+ }
+}
+
+Node EqualityQueryInstProp::getRepresentativeExp( Node a, std::vector< Node >& exp ) {
+ bool engine_has_a = getEngine()->hasTerm( a );
+ if( engine_has_a ){
+ a = getEngine()->getRepresentative( a );
+ }
+ //get union find representative, if this occurs in the equality engine, return it
+ unsigned prev_size = exp.size();
+ Node ar = getUfRepresentative( a, exp );
+ if( !ar.isNull() ){
+ if( engine_has_a || getEngine()->hasTerm( ar ) ){
+ Assert( getEngine()->hasTerm( ar ) );
+ Assert( getEngine()->getRepresentative( ar )==ar );
+ return ar;
+ }
+ }else{
+ if( engine_has_a ){
+ return a;
+ }
+ }
+ //retract explanation
+ while( exp.size()>prev_size ){
+ exp.pop_back();
+ }
+ return Node::null();
+}
+
+bool EqualityQueryInstProp::areEqualExp( Node a, Node b, std::vector< Node >& exp ) {
+ if( areEqual( a, b ) ){
+ return true;
+ }else{
+ std::vector< Node > exp_a;
+ Node ar = getUfRepresentative( a, exp_a );
+ if( !ar.isNull() ){
+ std::vector< Node > exp_b;
+ if( ar==getUfRepresentative( b, exp_b ) ){
+ merge_exp( exp, exp_a );
+ merge_exp( exp, exp_b );
+ return true;
+ }
+ }
+ return false;
+ }
+}
+
+bool EqualityQueryInstProp::areDisequalExp( Node a, Node b, std::vector< Node >& exp ) {
+ if( areDisequal( a, b ) ){
+ return true;
+ }else{
+ //TODO?
+ return false;
+ }
+}
+
+Node EqualityQueryInstProp::getUfRepresentative( Node a, std::vector< Node >& exp ) {
+ Assert( exp.empty() );
+ std::map< Node, Node >::iterator it = d_uf.find( a );
+ if( it!=d_uf.end() ){
+ if( it->second==a ){
+ Assert( d_uf_exp[ a ].empty() );
+ return it->second;
+ }else{
+ Node m = getUfRepresentative( it->second, exp );
+ Assert( !m.isNull() );
+ if( m!=it->second ){
+ //update union find
+ d_uf[ a ] = m;
+ //update explanation : merge the explanation of the parent
+ merge_exp( d_uf_exp[ a ], exp );
+ Trace("qip-eq") << "EqualityQueryInstProp::getUfRepresentative : merge " << a << " -> " << m << ", exp size=" << d_uf_exp[ a ].size() << std::endl;
+ }
+ //add current explanation to exp: note that exp is a subset of d_uf_exp[ a ], reset
+ exp.clear();
+ exp.insert( exp.end(), d_uf_exp[ a ].begin(), d_uf_exp[ a ].end() );
+ return m;
+ }
+ }else{
+ return Node::null();
+ }
+}
+
+// set a == b with reason, return status, modify a and b to representatives pre-merge
+int EqualityQueryInstProp::setEqual( Node& a, Node& b, bool pol, std::vector< Node >& reason ) {
+ if( a==b ){
+ return pol ? STATUS_NONE : STATUS_CONFLICT;
+ }
+ int status = pol ? STATUS_MERGED_UNKNOWN : STATUS_NONE;
+ Trace("qip-eq") << "EqualityQueryInstProp::setEqual " << a << ", " << b << ", pol = " << pol << ", reason size = " << reason.size() << std::endl;
+ //get the representative for a
+ std::vector< Node > exp_a;
+ Node ar = getUfRepresentative( a, exp_a );
+ if( ar.isNull() ){
+ Assert( exp_a.empty() );
+ ar = a;
+ }
+ if( ar==b ){
+ Trace("qip-eq") << "EqualityQueryInstProp::setEqual : already equal" << std::endl;
+ if( pol ){
+ return STATUS_NONE;
+ }else{
+ merge_exp( reason, exp_a );
+ return STATUS_CONFLICT;
+ }
+ }
+ bool swap = false;
+ //get the representative for b
+ std::vector< Node > exp_b;
+ Node br = getUfRepresentative( b, exp_b );
+ if( br.isNull() ){
+ Assert( exp_b.empty() );
+ br = b;
+ if( !getEngine()->hasTerm( br ) ){
+ if( ar!=a || getEngine()->hasTerm( ar ) ){
+ swap = true;
+ }
+ }else{
+ if( getEngine()->hasTerm( ar ) ){
+ status = STATUS_MERGED_KNOWN;
+ }
+ }
+ }else{
+ if( ar==br ){
+ Trace("qip-eq") << "EqualityQueryInstProp::setEqual : already equal" << std::endl;
+ if( pol ){
+ return STATUS_NONE;
+ }else{
+ merge_exp( reason, exp_a );
+ merge_exp( reason, exp_b );
+ return STATUS_CONFLICT;
+ }
+ }else if( getEngine()->hasTerm( ar ) ){
+ if( getEngine()->hasTerm( br ) ){
+ status = STATUS_MERGED_KNOWN;
+ }else{
+ swap = true;
+ }
+ }
+ }
+
+ if( swap ){
+ //swap
+ Node temp_r = ar;
+ ar = br;
+ br = temp_r;
+ }
+
+ Assert( !getEngine()->hasTerm( ar ) || getEngine()->hasTerm( br ) );
+ Assert( ar!=br );
+
+ std::vector< Node > exp_d;
+ if( areDisequalExp( ar, br, exp_d ) ){
+ if( pol ){
+ merge_exp( reason, exp_b );
+ merge_exp( reason, exp_b );
+ merge_exp( reason, exp_d );
+ return STATUS_CONFLICT;
+ }else{
+ return STATUS_NONE;
+ }
+ }else{
+ if( pol ){
+ //update the union find
+ Assert( d_uf_exp[ar].empty() );
+ Assert( d_uf_exp[br].empty() );
+
+ d_uf[ar] = br;
+ merge_exp( d_uf_exp[ar], exp_a );
+ merge_exp( d_uf_exp[ar], exp_b );
+ merge_exp( d_uf_exp[ar], reason );
+
+ d_uf[br] = br;
+ d_uf_exp[br].clear();
+
+ Trace("qip-eq") << "EqualityQueryInstProp::setEqual : merge " << ar << " -> " << br << ", exp size = " << d_uf_exp[ar].size() << ", status = " << status << std::endl;
+ a = ar;
+ b = br;
+ return status;
+ }else{
+ //TODO?
+ return STATUS_NONE;
+ }
+ }
+}
+
+void EqualityQueryInstProp::addArgument( std::vector< Node >& args, std::vector< Node >& props, Node n, bool is_prop, bool pol ) {
+ if( is_prop ){
+ if( isLiteral( n ) ){
+ props.push_back( pol ? n : n.negate() );
+ return;
+ }
+ }
+ args.push_back( n );
+}
+
+bool EqualityQueryInstProp::isLiteral( Node n ) {
+ Kind ak = n.getKind()==NOT ? n[0].getKind() : n.getKind();
+ Assert( ak!=NOT );
+ return ak!=AND && ak!=OR && ak!=IFF && ak!=ITE;
+}
+
+//this is identical to TermDb::evaluateTerm2, but tracks more information
+Node EqualityQueryInstProp::evaluateTermExp( Node n, std::vector< Node >& exp, std::map< Node, Node >& visited, bool hasPol, bool pol,
+ std::map< Node, bool >& watch_list_out, std::vector< Node >& props ) {
+ std::map< Node, Node >::iterator itv = visited.find( n );
+ if( itv != visited.end() ){
+ return itv->second;
+ }else{
+ visited[n] = n;
+ Trace("qip-eval") << "evaluate term : " << n << std::endl;
+ std::vector< Node > exp_n;
+ Node ret = getRepresentativeExp( n, exp_n );
+ if( ret.isNull() ){
+ //term is not known to be equal to a representative in equality engine, evaluate it
+ Kind k = n.getKind();
+ if( k==FORALL ){
+ ret = Node::null();
+ }else{
+ std::map< Node, bool > watch_list_out_curr;
+ TNode f = d_qe->getTermDatabase()->getMatchOperator( n );
+ std::vector< Node > args;
+ bool ret_set = false;
+ bool childChanged = false;
+ int abort_i = -1;
+ //get the child entailed polarity
+ Assert( n.getKind()!=IMPLIES );
+ bool newHasPol, newPol;
+ QuantPhaseReq::getEntailPolarity( n, 0, hasPol, pol, newHasPol, newPol );
+ //for each child
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ Node c = evaluateTermExp( n[i], exp, visited, newHasPol, newPol, watch_list_out_curr, props );
+ if( c.isNull() ){
+ ret = Node::null();
+ ret_set = true;
+ break;
+ }else if( c==d_true || c==d_false ){
+ //short-circuiting
+ if( k==kind::AND || k==kind::OR ){
+ if( (k==kind::AND)==(c==d_false) ){
+ ret = c;
+ ret_set = true;
+ break;
+ }else{
+ //redundant
+ c = Node::null();
+ childChanged = true;
+ }
+ }else if( k==kind::ITE && i==0 ){
+ Assert( watch_list_out_curr.empty() );
+ ret = evaluateTermExp( n[ c==d_true ? 1 : 2], exp, visited, hasPol, pol, watch_list_out_curr, props );
+ ret_set = true;
+ break;
+ }else if( k==kind::NOT ){
+ ret = c==d_true ? d_false : d_true;
+ ret_set = true;
+ break;
+ }
+ }
+ if( !c.isNull() ){
+ childChanged = childChanged || n[i]!=c;
+ if( !f.isNull() && !watch_list_out_curr.empty() ){
+ // we are done if this is an UF application and an argument is unevaluated
+ args.push_back( c );
+ abort_i = i;
+ break;
+ }else if( ( k==kind::AND || k==kind::OR ) ){
+ if( c.getKind()==k ){
+ //flatten
+ for( unsigned j=0; j<c.getNumChildren(); j++ ){
+ addArgument( args, props, c[j], newHasPol, newPol );
+ }
+ }else{
+ addArgument( args, props, c, newHasPol, newPol );
+ }
+ //if we are in a branching position
+ if( hasPol && !newHasPol && args.size()>=2 ){
+ //we are done if at least two args are unevaluated
+ abort_i = i;
+ break;
+ }
+ }else if( k==kind::ITE ){
+ //we are done if we are ITE and condition is unevaluated
+ Assert( i==0 );
+ args.push_back( c );
+ abort_i = i;
+ break;
+ }else{
+ args.push_back( c );
+ }
+ }
+ }
+ //add remaining children if we aborted
+ if( abort_i!=-1 ){
+ for( int i=(abort_i+1); i<(int)n.getNumChildren(); i++ ){
+ args.push_back( n[i] );
+ }
+ }
+ //copy over the watch list
+ for( std::map< Node, bool >::iterator itc = watch_list_out_curr.begin(); itc != watch_list_out_curr.end(); ++itc ){
+ watch_list_out[itc->first] = itc->second;
+ }
+
+ //if we have not short-circuited evaluation
+ if( !ret_set ){
+ //if it is an indexed term, return the congruent term
+ if( !f.isNull() && watch_list_out.empty() ){
+ std::vector< TNode > t_args;
+ for( unsigned i=0; i<args.size(); i++ ) {
+ t_args.push_back( args[i] );
+ }
+ Assert( args.size()==n.getNumChildren() );
+ //args contains terms known by the equality engine
+ TNode nn = getCongruentTerm( f, t_args );
+ Trace("qip-eval") << " got congruent term " << nn << " from DB for " << n << std::endl;
+ if( !nn.isNull() ){
+ //successfully constructed representative in EE
+ Assert( exp_n.empty() );
+ ret = getRepresentativeExp( nn, exp_n );
+ Trace("qip-eval") << "return rep, exp size = " << exp_n.size() << std::endl;
+ merge_exp( exp, exp_n );
+ ret_set = true;
+ Assert( !ret.isNull() );
+ }
+ }
+ if( !ret_set ){
+ if( childChanged ){
+ Trace("qip-eval") << "return rewrite" << std::endl;
+ if( ( k==kind::AND || k==kind::OR ) ){
+ if( args.empty() ){
+ ret = k==kind::AND ? d_true : d_false;
+ ret_set = true;
+ }else if( args.size()==1 ){
+ ret = args[0];
+ ret_set = true;
+ }
+ }else{
+ Assert( args.size()==n.getNumChildren() );
+ }
+ if( !ret_set ){
+ if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
+ args.insert( args.begin(), n.getOperator() );
+ }
+ ret = NodeManager::currentNM()->mkNode( k, args );
+ ret = Rewriter::rewrite( ret );
+ //re-evaluate
+ Node ret_eval = getRepresentativeExp( ret, exp_n );
+ if( !ret_eval.isNull() ){
+ ret = ret_eval;
+ watch_list_out.clear();
+ }else{
+ watch_list_out[ret] = true;
+ }
+ }
+ }else{
+ ret = n;
+ watch_list_out[ret] = true;
+ }
+ }
+ }
+ }
+ }else{
+ Trace("qip-eval") << "...exists in ee, return rep, exp size = " << exp_n.size() << std::endl;
+ merge_exp( exp, exp_n );
+ }
+ Trace("qip-eval") << "evaluated term : " << n << ", got : " << ret << ", exp size = " << exp.size() << std::endl;
+ visited[n] = ret;
+ return ret;
+ }
+}
+
+void EqualityQueryInstProp::merge_exp( std::vector< Node >& v, std::vector< Node >& v_to_merge, int up_to_size ) {
+ //TODO : optimize
+ if( v.empty() ){
+ Assert( up_to_size==-1 || up_to_size==(int)v_to_merge.size() );
+ v.insert( v.end(), v_to_merge.begin(), v_to_merge.end() );
+ }else{
+ //std::vector< Node >::iterator v_end = v.end();
+ up_to_size = up_to_size==-1 ? (int)v_to_merge.size() : up_to_size;
+ for( int j=0; j<up_to_size; j++ ){
+ if( std::find( v.begin(), v.end(), v_to_merge[j] )==v.end() ){
+ v.push_back( v_to_merge[j] );
+ }
+ }
+ }
+}
+
+
+void InstPropagator::InstInfo::init( Node q, Node lem, std::vector< Node >& terms, Node body ) {
+ d_active = true;
+ //information about the instance
+ d_q = q;
+ d_lem = lem;
+ Assert( d_terms.empty() );
+ d_terms.insert( d_terms.end(), terms.begin(), terms.end() );
+ //the current lemma
+ d_curr = body;
+ d_curr_exp.push_back( body );
+}
+
+InstPropagator::InstPropagator( QuantifiersEngine* qe ) :
+d_qe( qe ), d_notify(*this), d_qy( qe ){
+}
+
+bool InstPropagator::reset( Theory::Effort e ) {
+ d_icount = 1;
+ d_ii.clear();
+ for( unsigned i=0; i<2; i++ ){
+ d_conc_to_id[i].clear();
+ d_conc_to_id[i][d_qy.d_true] = 0;
+ }
+ d_conflict = false;
+ d_watch_list.clear();
+ d_update_list.clear();
+ d_relevant_inst.clear();
+ return d_qy.reset( e );
+}
+
+bool InstPropagator::notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) {
+ if( !d_conflict ){
+ if( Trace.isOn("qip-prop") ){
+ Trace("qip-prop") << "InstPropagator:: Notify instantiation " << q << " : " << std::endl;
+ for( unsigned i=0; i<terms.size(); i++ ){
+ Trace("qip-prop") << " " << terms[i] << std::endl;
+ }
+ }
+ unsigned id = d_icount;
+ d_icount++;
+ Trace("qip-prop") << "...assign id=" << id << std::endl;
+ d_ii[id].init( q, lem, terms, body );
+ //initialize the information
+ if( cacheConclusion( id, body ) ){
+ Assert( d_update_list.empty() );
+ d_update_list.push_back( id );
+ bool firstTime = true;
+ //update infos in the update list until empty
+ do {
+ unsigned uid = d_update_list.back();
+ d_update_list.pop_back();
+ if( d_ii[uid].d_active ){
+ update( uid, d_ii[uid], firstTime );
+ }
+ firstTime = false;
+ }while( !d_conflict && !d_update_list.empty() );
+ }else{
+ d_ii[id].d_active = false;
+ Trace("qip-prop") << "...duplicate." << std::endl;
+ }
+ Trace("qip-prop") << "...finished notify instantiation." << std::endl;
+ return !d_conflict;
+ }else{
+ return true;
+ }
+}
+
+bool InstPropagator::update( unsigned id, InstInfo& ii, bool firstTime ) {
+ Assert( !d_conflict );
+ Assert( ii.d_active );
+ Trace("qip-prop-debug") << "Update info [" << id << "]..." << std::endl;
+ //update the evaluation of the current lemma
+ std::map< Node, Node > visited;
+ std::map< Node, bool > watch_list;
+ std::vector< Node > props;
+ Node eval = d_qy.evaluateTermExp( ii.d_curr, ii.d_curr_exp, visited, true, true, watch_list, props );
+ if( eval.isNull() ){
+ ii.d_active = false;
+ }else if( firstTime || eval!=ii.d_curr ){
+ if( EqualityQueryInstProp::isLiteral( eval ) ){
+ props.push_back( eval );
+ eval = d_qy.d_true;
+ watch_list.clear();
+ }
+ if( Trace.isOn("qip-prop") ){
+ Trace("qip-prop") << "Update info [" << id << "]..." << std::endl;
+ Trace("qip-prop") << "...updated lemma " << ii.d_curr << " -> " << eval << ", exp = ";
+ debugPrintExplanation( ii.d_curr_exp, "qip-prop" );
+ Trace("qip-prop") << std::endl;
+ Trace("qip-prop") << "...watch list: " << std::endl;
+ for( std::map< Node, bool >::iterator itw = watch_list.begin(); itw!=watch_list.end(); ++itw ){
+ Trace("qip-prop") << " " << itw->first << std::endl;
+ }
+ Trace("qip-prop") << "...new propagations: " << std::endl;
+ for( unsigned i=0; i<props.size(); i++ ){
+ Trace("qip-prop") << " " << props[i] << std::endl;
+ }
+ Trace("qip-prop") << std::endl;
+ }
+ //determine the status of eval
+ if( eval==d_qy.d_false ){
+ Assert( props.empty() );
+ //we have inferred a conflict
+ conflict( ii.d_curr_exp );
+ return false;
+ }else{
+ for( unsigned i=0; i<props.size(); i++ ){
+ Trace("qip-prop-debug2") << "Process propagation " << props[i] << std::endl;
+ //if we haven't propagated this literal yet
+ if( cacheConclusion( id, props[i], 1 ) ){
+ Node lit = props[i].getKind()==NOT ? props[i][0] : props[i];
+ bool pol = props[i].getKind()!=NOT;
+ if( lit.getKind()==EQUAL ){
+ propagate( lit[0], lit[1], pol, ii.d_curr_exp );
+ }else{
+ propagate( lit, pol ? d_qy.d_true : d_qy.d_false, true, ii.d_curr_exp );
+ }
+ if( d_conflict ){
+ return false;
+ }
+ }
+ Trace("qip-prop-debug2") << "Done process propagation " << props[i] << std::endl;
+ }
+ //if we have not inferred this conclusion yet
+ if( cacheConclusion( id, eval ) ){
+ ii.d_curr = eval;
+ //update the watch list
+ Trace("qip-prop-debug") << "...updating watch list for [" << id << "], curr is " << ii.d_curr << std::endl;
+ //Here, we need to be notified of enough terms such that if we are not notified, then update( ii ) will return no propagations.
+ // Similar to two-watched literals, but since we are in UF, we need to watch all terms on a complete path of two terms.
+ for( std::map< Node, bool >::iterator itw = watch_list.begin(); itw != watch_list.end(); ++itw ){
+ d_watch_list[ itw->first ][ id ] = true;
+ }
+ }else{
+ Trace("qip-prop-debug") << "...conclusion " << eval << " is duplicate." << std::endl;
+ ii.d_active = false;
+ }
+ }
+ }else{
+ Trace("qip-prop-debug") << "...did not update." << std::endl;
+ }
+ Assert( !d_conflict );
+ return true;
+}
+
+void InstPropagator::propagate( Node a, Node b, bool pol, std::vector< Node >& exp ) {
+ if( Trace.isOn("qip-propagate") ){
+ Trace("qip-propagate") << "* Propagate " << a << ( pol ? " == " : " != " ) << b << ", exp = ";
+ debugPrintExplanation( exp, "qip-propagate" );
+ Trace("qip-propagate") << "..." << std::endl;
+ }
+ //set equal
+ int status = d_qy.setEqual( a, b, pol, exp );
+ if( status==EqualityQueryInstProp::STATUS_NONE ){
+ Trace("qip-prop-debug") << "...already equal/no conflict." << std::endl;
+ return;
+ }else if( status==EqualityQueryInstProp::STATUS_CONFLICT ){
+ Trace("qip-prop-debug") << "...conflict." << std::endl;
+ conflict( exp );
+ return;
+ }
+ if( pol ){
+ if( status==EqualityQueryInstProp::STATUS_MERGED_KNOWN ){
+ Assert( d_qy.getEngine()->hasTerm( a ) );
+ Assert( d_qy.getEngine()->hasTerm( b ) );
+ Trace("qip-prop-debug") << "...equality between known terms." << std::endl;
+ addRelevantInstances( exp, "qip-propagate" );
+ }
+ Trace("qip-prop-debug") << "...merged representatives " << a << " and " << b << std::endl;
+ for( unsigned i=0; i<2; i++ ){
+ //update terms from watched lists
+ Node c = i==0 ? a : b;
+ std::map< Node, std::map< unsigned, bool > >::iterator it = d_watch_list.find( c );
+ if( it!=d_watch_list.end() ){
+ Trace("qip-prop-debug") << "...update ids from watch list of " << c << ", size=" << it->second.size() << "..." << std::endl;
+ for( std::map< unsigned, bool >::iterator itw = it->second.begin(); itw != it->second.end(); ++itw ){
+ unsigned idw = itw->first;
+ if( std::find( d_update_list.begin(), d_update_list.end(), idw )==d_update_list.end() ){
+ Trace("qip-prop-debug") << "...will update " << idw << std::endl;
+ d_update_list.push_back( idw );
+ }
+ }
+ d_watch_list.erase( c );
+ }
+ }
+ }
+}
+
+void InstPropagator::conflict( std::vector< Node >& exp ) {
+ Trace("qip-propagate") << "Conflict, exp size =" << exp.size() << std::endl;
+ d_conflict = true;
+ d_relevant_inst.clear();
+ addRelevantInstances( exp, "qip-propagate" );
+
+ //now, inform quantifiers engine which instances should be retracted
+ for( std::map< unsigned, InstInfo >::iterator it = d_ii.begin(); it != d_ii.end(); ++it ){
+ if( d_relevant_inst.find( it->first )==d_relevant_inst.end() ){
+ if( !d_qe->removeInstantiation( it->second.d_q, it->second.d_lem, it->second.d_terms ) ){
+ Trace("qip-warn") << "WARNING : did not remove instantiation id " << it->first << std::endl;
+ Assert( false );
+ }
+ }
+ }
+ //will interupt the quantifiers engine
+ Trace("quant-engine-conflict") << "-----> InstPropagator::conflict with " << exp.size() << " instances." << std::endl;
+}
+
+bool InstPropagator::cacheConclusion( unsigned id, Node body, int prop_index ) {
+ Assert( prop_index==0 || prop_index==1 );
+ //check if the conclusion is non-redundant
+ if( d_conc_to_id[prop_index].find( body )==d_conc_to_id[prop_index].end() ){
+ d_conc_to_id[prop_index][body] = id;
+ return true;
+ }else{
+ return false;
+ }
+}
+
+void InstPropagator::addRelevantInstances( std::vector< Node >& exp, const char * c ) {
+ for( unsigned i=0; i<exp.size(); i++ ){
+ Assert( d_conc_to_id[0].find( exp[i] )!=d_conc_to_id[0].end() );
+ Trace(c) << " relevant instance id : " << d_conc_to_id[0][ exp[i] ] << std::endl;
+ d_relevant_inst[ d_conc_to_id[0][ exp[i] ] ] = true;
+ }
+}
+
+void InstPropagator::debugPrintExplanation( std::vector< Node >& exp, const char * c ) {
+ for( unsigned i=0; i<exp.size(); i++ ){
+ Assert( d_conc_to_id[0].find( exp[i] )!=d_conc_to_id[0].end() );
+ Trace(c) << d_conc_to_id[0][ exp[i] ] << " ";
+ }
+}
+
-/********************* */\r
-/*! \file inst_propagator.h\r
- ** \verbatim\r
- ** Top contributors (to current version):\r
- ** Andrew Reynolds\r
- ** This file is part of the CVC4 project.\r
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS\r
- ** in the top-level source directory) and their institutional affiliations.\r
- ** All rights reserved. See the file COPYING in the top-level source\r
- ** directory for licensing information.\endverbatim\r
- **\r
- ** \brief Propagate mechanism for instantiations\r
- **/\r
-\r
-#include "cvc4_private.h"\r
-\r
-#ifndef __CVC4__QUANTIFIERS_INST_PROPAGATOR_H\r
-#define __CVC4__QUANTIFIERS_INST_PROPAGATOR_H\r
-\r
-#include <iostream>\r
-#include <string>\r
-#include <vector>\r
-#include <map>\r
-#include "expr/node.h"\r
-#include "expr/type_node.h"\r
-#include "theory/quantifiers_engine.h"\r
-#include "theory/quantifiers/term_database.h"\r
-\r
-namespace CVC4 {\r
-namespace theory {\r
-namespace quantifiers {\r
-\r
-class EqualityQueryInstProp : public EqualityQuery {\r
-private:\r
- /** pointer to quantifiers engine */\r
- QuantifiersEngine* d_qe;\r
-public:\r
- EqualityQueryInstProp( QuantifiersEngine* qe );\r
- ~EqualityQueryInstProp(){};\r
- /** reset */\r
- bool reset( Theory::Effort e );\r
- /** identify */\r
- std::string identify() const { return "EqualityQueryInstProp"; }\r
- /** extends engine */\r
- bool extendsEngine() { return true; }\r
- /** contains term */\r
- bool hasTerm( Node a );\r
- /** get the representative of the equivalence class of a */\r
- Node getRepresentative( Node a );\r
- /** returns true if a and b are equal in the current context */\r
- bool areEqual( Node a, Node b );\r
- /** returns true is a and b are disequal in the current context */\r
- bool areDisequal( Node a, Node b );\r
- /** get the equality engine associated with this query */\r
- eq::EqualityEngine* getEngine();\r
- /** get the equivalence class of a */\r
- void getEquivalenceClass( Node a, std::vector< Node >& eqc );\r
- /** get congruent term */\r
- TNode getCongruentTerm( Node f, std::vector< TNode >& args );\r
-public:\r
- /** get the representative of the equivalence class of a, with explanation */\r
- Node getRepresentativeExp( Node a, std::vector< Node >& exp );\r
- /** returns true if a and b are equal in the current context */\r
- bool areEqualExp( Node a, Node b, std::vector< Node >& exp );\r
- /** returns true is a and b are disequal in the current context */\r
- bool areDisequalExp( Node a, Node b, std::vector< Node >& exp );\r
-private:\r
- /** term index */\r
- std::map< Node, TermArgTrie > d_func_map_trie;\r
- /** union find for terms beyond what is stored in equality engine */\r
- std::map< Node, Node > d_uf;\r
- std::map< Node, std::vector< Node > > d_uf_exp;\r
- Node getUfRepresentative( Node a, std::vector< Node >& exp );\r
- /** disequality list, stores explanations */\r
- std::map< Node, std::map< Node, Node > > d_diseq_list;\r
- /** add arg */\r
- void addArgument( std::vector< TNode >& args, std::vector< TNode >& props, Node n, bool is_prop, bool pol );\r
-public:\r
- enum {\r
- STATUS_MERGED_KNOWN,\r
- STATUS_MERGED_UNKNOWN,\r
- STATUS_NONE,\r
- };\r
- /** set equal */\r
- int setEqual( Node& a, Node& b, std::vector< Node >& reason );\r
- Node d_true;\r
- Node d_false;\r
-public:\r
- //for explanations\r
- static void merge_exp( std::vector< Node >& v, std::vector< Node >& v_to_merge, int up_to_size = -1 );\r
-\r
- Node evaluateTermExp( TNode n, std::vector< Node >& exp, std::map< TNode, Node >& visited, bool hasPol, bool pol,\r
- std::map< Node, bool >& watch_list_out, std::vector< TNode >& props );\r
- static bool isLiteral( Node n );\r
-};\r
-\r
-class InstPropagator : public QuantifiersUtil {\r
-private:\r
- /** pointer to quantifiers engine */\r
- QuantifiersEngine* d_qe;\r
- /** notify class */\r
- class InstantiationNotifyInstPropagator : public InstantiationNotify {\r
- InstPropagator& d_ip;\r
- public:\r
- InstantiationNotifyInstPropagator(InstPropagator& ip): d_ip(ip) {}\r
- virtual void notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) { d_ip.notifyInstantiation( quant_e, q, lem, terms, body ); }\r
- };\r
- InstantiationNotifyInstPropagator d_notify;\r
- /** notify instantiation method */\r
- void notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body );\r
- /** equality query */\r
- EqualityQueryInstProp d_qy;\r
- class InstInfo {\r
- public:\r
- bool d_active;\r
- Node d_q;\r
- Node d_lem;\r
- std::vector< Node > d_terms;\r
- // the current entailed body\r
- Node d_curr;\r
- //explanation for current entailed body\r
- std::vector< Node > d_curr_exp;\r
- void init( Node q, Node lem, std::vector< Node >& terms, Node body );\r
- };\r
- /** instantiation count/info */\r
- unsigned d_icount;\r
- std::map< unsigned, InstInfo > d_ii;\r
- std::map< TNode, unsigned > d_conc_to_id[2];\r
- /** are we in conflict */\r
- bool d_conflict;\r
- /** watch list */\r
- std::map< Node, std::map< unsigned, bool > > d_watch_list;\r
- /** update list */\r
- std::vector< unsigned > d_update_list;\r
- /** relevant instances */\r
- std::map< unsigned, bool > d_relevant_inst;\r
-private:\r
- bool update( unsigned id, InstInfo& i, bool firstTime = false );\r
- void propagate( Node a, Node b, bool pol, std::vector< Node >& exp );\r
- void conflict( std::vector< Node >& exp );\r
- bool cacheConclusion( unsigned id, Node body, int prop_index = 0 );\r
- void addRelevantInstances( std::vector< Node >& exp, const char * c );\r
-\r
- void debugPrintExplanation( std::vector< Node >& exp, const char * c );\r
-public:\r
- InstPropagator( QuantifiersEngine* qe );\r
- ~InstPropagator(){}\r
- /** reset */\r
- bool reset( Theory::Effort e );\r
- /** identify */\r
- std::string identify() const { return "InstPropagator"; }\r
- /** get the notify mechanism */\r
- InstantiationNotify* getInstantiationNotify() { return &d_notify; }\r
-};\r
-\r
-}\r
-}\r
-}\r
-\r
-#endif\r
+/********************* */
+/*! \file inst_propagator.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Propagate mechanism for instantiations
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__QUANTIFIERS_INST_PROPAGATOR_H
+#define __CVC4__QUANTIFIERS_INST_PROPAGATOR_H
+
+#include <iostream>
+#include <string>
+#include <vector>
+#include <map>
+#include "expr/node.h"
+#include "expr/type_node.h"
+#include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/term_database.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class EqualityQueryInstProp : public EqualityQuery {
+private:
+ /** pointer to quantifiers engine */
+ QuantifiersEngine* d_qe;
+public:
+ EqualityQueryInstProp( QuantifiersEngine* qe );
+ ~EqualityQueryInstProp(){};
+ /** reset */
+ bool reset( Theory::Effort e );
+ /** identify */
+ std::string identify() const { return "EqualityQueryInstProp"; }
+ /** extends engine */
+ bool extendsEngine() { return true; }
+ /** contains term */
+ bool hasTerm( Node a );
+ /** get the representative of the equivalence class of a */
+ Node getRepresentative( Node a );
+ /** returns true if a and b are equal in the current context */
+ bool areEqual( Node a, Node b );
+ /** returns true is a and b are disequal in the current context */
+ bool areDisequal( Node a, Node b );
+ /** get the equality engine associated with this query */
+ eq::EqualityEngine* getEngine();
+ /** get the equivalence class of a */
+ void getEquivalenceClass( Node a, std::vector< Node >& eqc );
+ /** get congruent term */
+ TNode getCongruentTerm( Node f, std::vector< TNode >& args );
+public:
+ /** get the representative of the equivalence class of a, with explanation */
+ Node getRepresentativeExp( Node a, std::vector< Node >& exp );
+ /** returns true if a and b are equal in the current context */
+ bool areEqualExp( Node a, Node b, std::vector< Node >& exp );
+ /** returns true is a and b are disequal in the current context */
+ bool areDisequalExp( Node a, Node b, std::vector< Node >& exp );
+private:
+ /** term index */
+ std::map< Node, TermArgTrie > d_func_map_trie;
+ /** union find for terms beyond what is stored in equality engine */
+ std::map< Node, Node > d_uf;
+ std::map< Node, std::vector< Node > > d_uf_exp;
+ Node getUfRepresentative( Node a, std::vector< Node >& exp );
+ /** disequality list, stores explanations */
+ std::map< Node, std::map< Node, Node > > d_diseq_list;
+ /** add arg */
+ void addArgument( std::vector< Node >& args, std::vector< Node >& props, Node n, bool is_prop, bool pol );
+public:
+ enum {
+ STATUS_CONFLICT,
+ STATUS_MERGED_KNOWN,
+ STATUS_MERGED_UNKNOWN,
+ STATUS_NONE,
+ };
+ /** set equal */
+ int setEqual( Node& a, Node& b, bool pol, std::vector< Node >& reason );
+ Node d_true;
+ Node d_false;
+public:
+ //for explanations
+ static void merge_exp( std::vector< Node >& v, std::vector< Node >& v_to_merge, int up_to_size = -1 );
+
+ Node evaluateTermExp( Node n, std::vector< Node >& exp, std::map< Node, Node >& visited, bool hasPol, bool pol,
+ std::map< Node, bool >& watch_list_out, std::vector< Node >& props );
+ static bool isLiteral( Node n );
+};
+
+class InstPropagator : public QuantifiersUtil {
+private:
+ /** pointer to quantifiers engine */
+ QuantifiersEngine* d_qe;
+ /** notify class */
+ class InstantiationNotifyInstPropagator : public InstantiationNotify {
+ InstPropagator& d_ip;
+ public:
+ InstantiationNotifyInstPropagator(InstPropagator& ip): d_ip(ip) {}
+ virtual bool notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) {
+ return d_ip.notifyInstantiation( quant_e, q, lem, terms, body );
+ }
+ };
+ InstantiationNotifyInstPropagator d_notify;
+ /** notify instantiation method */
+ bool notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body );
+ /** equality query */
+ EqualityQueryInstProp d_qy;
+ class InstInfo {
+ public:
+ bool d_active;
+ Node d_q;
+ Node d_lem;
+ std::vector< Node > d_terms;
+ // the current entailed body
+ Node d_curr;
+ //explanation for current entailed body
+ std::vector< Node > d_curr_exp;
+ void init( Node q, Node lem, std::vector< Node >& terms, Node body );
+ };
+ /** instantiation count/info */
+ unsigned d_icount;
+ std::map< unsigned, InstInfo > d_ii;
+ std::map< Node, unsigned > d_conc_to_id[2];
+ /** are we in conflict */
+ bool d_conflict;
+ /** watch list */
+ std::map< Node, std::map< unsigned, bool > > d_watch_list;
+ /** update list */
+ std::vector< unsigned > d_update_list;
+ /** relevant instances */
+ std::map< unsigned, bool > d_relevant_inst;
+private:
+ bool update( unsigned id, InstInfo& i, bool firstTime = false );
+ void propagate( Node a, Node b, bool pol, std::vector< Node >& exp );
+ void conflict( std::vector< Node >& exp );
+ bool cacheConclusion( unsigned id, Node body, int prop_index = 0 );
+ void addRelevantInstances( std::vector< Node >& exp, const char * c );
+
+ void debugPrintExplanation( std::vector< Node >& exp, const char * c );
+public:
+ InstPropagator( QuantifiersEngine* qe );
+ ~InstPropagator(){}
+ /** reset */
+ bool reset( Theory::Effort e );
+ /** identify */
+ std::string identify() const { return "InstPropagator"; }
+ /** get the notify mechanism */
+ InstantiationNotify* getInstantiationNotify() { return &d_notify; }
+};
+
+}
+}
+}
+
+#endif
void InstStrategyCbqi::check( Theory::Effort e, unsigned quant_e ) {
if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){
+ Assert( !d_quantEngine->inConflict() );
double clSet = 0;
if( Trace.isOn("cbqi-engine") ){
clSet = double(clock())/double(CLOCKS_PER_SEC);
Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
process( q, e, ee );
+ if( d_quantEngine->inConflict() ){
+ break;
+ }
}
}
- if( d_quantEngine->getNumLemmasWaiting()>lastWaiting ){
+ if( d_quantEngine->inConflict() || d_quantEngine->getNumLemmasWaiting()>lastWaiting ){
break;
}
}
//new implementation
-bool CegqiOutputInstStrategy::addInstantiation( std::vector< Node >& subs ) {
- return d_out->addInstantiation( subs );
+bool CegqiOutputInstStrategy::doAddInstantiation( std::vector< Node >& subs ) {
+ return d_out->doAddInstantiation( subs );
}
bool CegqiOutputInstStrategy::isEligibleForInstantiation( Node n ) {
}
}
-bool InstStrategyCegqi::addInstantiation( std::vector< Node >& subs ) {
+bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) {
Assert( !d_curr_quant.isNull() );
//if doing partial quantifier elimination, record the instantiation and set the incomplete flag instead of sending instantiation lemma
if( d_quantEngine->getTermDatabase()->isQAttrQuantElimPartial( d_curr_quant ) ){
d_cbqi_set_quant_inactive = true;
d_incomplete_check = true;
- d_quantEngine->recordInstantiationInternal( d_curr_quant, subs, false, false );
+ d_quantEngine->recordInstantiationInternal( d_curr_quant, subs, false, false, true );
return true;
}else{
//check if we need virtual term substitution (if used delta or infinity)
public:
CegqiOutputInstStrategy( InstStrategyCegqi * out ) : d_out( out ){}
InstStrategyCegqi * d_out;
- bool addInstantiation( std::vector< Node >& subs );
+ bool doAddInstantiation( std::vector< Node >& subs );
bool isEligibleForInstantiation( Node n );
bool addLemma( Node lem );
};
InstStrategyCegqi( QuantifiersEngine * qe );
~InstStrategyCegqi() throw();
- bool addInstantiation( std::vector< Node >& subs );
+ bool doAddInstantiation( std::vector< Node >& subs );
bool isEligibleForInstantiation( Node n );
bool addLemma( Node lem );
/** identify */
if( d_user_gen[f][i]->isMultiTrigger() ){
d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
}
- //d_quantEngine->d_hasInstantiated[f] = true;
+ if( d_quantEngine->inConflict() ){
+ break;
+ }
}
}
}
if( r==1 ){
d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
}
- //d_quantEngine->d_hasInstantiated[f] = true;
+ if( d_quantEngine->inConflict() ){
+ break;
+ }
}
}
}
- if( hasInst && options::multiTriggerPriority() ){
+ if( d_quantEngine->inConflict() || ( hasInst && options::multiTriggerPriority() ) ){
break;
}
}
if( process( q, fullEffort ) ){
//added lemma
addedLemmas++;
+ if( d_quantEngine->inConflict() ){
+ break;
+ }
}
}
}
}
}
-bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
+void InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting();
//iterate over an internal effort level e
int e = 0;
InstStrategy* is = d_instStrategies[j];
Trace("inst-engine-debug") << "Do " << is->identify() << " " << e_use << std::endl;
int quantStatus = is->process( q, effort, e_use );
- Trace("inst-engine-debug") << " -> status is " << quantStatus << std::endl;
- if( quantStatus==InstStrategy::STATUS_UNFINISHED ){
+ Trace("inst-engine-debug") << " -> status is " << quantStatus << ", conflict=" << d_quantEngine->inConflict() << std::endl;
+ if( d_quantEngine->inConflict() ){
+ return;
+ }else if( quantStatus==InstStrategy::STATUS_UNFINISHED ){
finished = false;
}
}
}
e++;
}
- //Notice() << "All instantiators finished, # added lemmas = " << (int)d_lemmas_waiting.size() << std::endl;
- if( !d_quantEngine->hasAddedLemma() ){
- return false;
- }else{
- Trace("inst-engine") << "Added lemmas = " << (int)(d_quantEngine->getNumLemmasWaiting()-lastWaiting) << std::endl;
- return true;
- }
}
bool InstantiationEngine::needsCheck( Theory::Effort e ){
Trace("inst-engine-debug") << "InstEngine: check: # asserted quantifiers " << d_quants.size() << "/";
Trace("inst-engine-debug") << d_quantEngine->getModel()->getNumAssertedQuantifiers() << " " << quantActive << std::endl;
if( quantActive ){
- bool addedLemmas = doInstantiationRound( e );
- Trace("inst-engine-debug") << "Add lemmas = " << addedLemmas << std::endl;
+ unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting();
+ doInstantiationRound( e );
+ if( d_quantEngine->inConflict() ){
+ Assert( d_quantEngine->getNumLemmasWaiting()>lastWaiting );
+ Trace("inst-engine") << "Conflict, size = " << d_quantEngine->getNumLemmasWaiting();
+ if( lastWaiting>0 ){
+ Trace("inst-engine") << " (prev " << lastWaiting << ")";
+ }
+ Trace("inst-engine") << std::endl;
+ }else if( d_quantEngine->hasAddedLemma() ){
+ Trace("inst-engine") << "Added lemmas = " << (d_quantEngine->getNumLemmasWaiting()-lastWaiting) << std::endl;
+ }
}else{
d_quants.clear();
}
/** is the engine incomplete for this quantifier */
bool isIncomplete( Node q );
/** do instantiation round */
- bool doInstantiationRound( Theory::Effort effort );
+ void doInstantiationRound( Theory::Effort effort );
public:
InstantiationEngine( QuantifiersEngine* qe );
~InstantiationEngine();
int lems = initializeQuantifier( f, f );
d_statistics.d_init_inst_gen_lemmas += lems;
d_addedLemmas += lems;
+ if( d_qe->inConflict() ){
+ break;
+ }
}
}
if( d_addedLemmas>0 ){
Trace("model-engine") << "Initialize, Added Lemmas = " << d_addedLemmas << std::endl;
}else{
+ Assert( !d_qe->inConflict() );
//initialize model
fm->initialize();
//analyze the functions
}else{
d_numQuantNoSelForm++;
}
- if( options::fmfInstGenOneQuantPerRound() && lems>0 ){
+ if( d_qe->inConflict() || ( options::fmfInstGenOneQuantPerRound() && lems>0 ) ){
break;
}
}else if( d_quant_sat.find( f )!=d_quant_sat.end() ){
//add as instantiation
if( d_qe->addInstantiation( f, m ) ){
d_addedLemmas++;
+ if( d_qe->inConflict() ){
+ break;
+ }
//if the instantiation is show to be false, and we wish to skip multiple instantiations at once
if( eval==-1 ){
riter.increment2( depIndex );
void ModelEngine::check( Theory::Effort e, unsigned quant_e ){
if( quant_e==QuantifiersEngine::QEFFORT_MODEL ){
+ Assert( !d_quantEngine->inConflict() );
int addedLemmas = 0;
FirstOrderModel* fm = d_quantEngine->getModel();
//CVC4 will answer SAT or unknown
Trace("fmf-consistent") << std::endl;
debugPrint("fmf-consistent");
- }else{
- //otherwise, the search will continue
}
}
}
// FMC uses two sub-effort levels
int e_max = options::mbqiMode()==MBQI_FMC || options::mbqiMode()==MBQI_FMC_INTERVAL ? 2 : ( options::mbqiMode()==MBQI_TRUST ? 0 : 1 );
for( int e=0; e<e_max; e++) {
- if (d_addedLemmas==0) {
- for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
- Node f = fm->getAssertedQuantifier( i );
- Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << f << ", effort = " << e << "..." << std::endl;
- //determine if we should check this quantifier
- if( considerQuantifiedFormula( f ) ){
- exhaustiveInstantiate( f, e );
- if( Trace.isOn("model-engine-warn") ){
- if( d_addedLemmas>10000 ){
- Debug("fmf-exit") << std::endl;
- debugPrint("fmf-exit");
- exit( 0 );
- }
- }
- if( optOneQuantPerRound() && d_addedLemmas>0 ){
- break;
+ for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+ Node f = fm->getAssertedQuantifier( i );
+ Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << f << ", effort = " << e << "..." << std::endl;
+ //determine if we should check this quantifier
+ if( considerQuantifiedFormula( f ) ){
+ exhaustiveInstantiate( f, e );
+ if( Trace.isOn("model-engine-warn") ){
+ if( d_addedLemmas>10000 ){
+ Debug("fmf-exit") << std::endl;
+ debugPrint("fmf-exit");
+ exit( 0 );
}
- }else{
- Trace("fmf-exh-inst") << "-> Inactive : " << f << std::endl;
}
+ if( d_quantEngine->inConflict() || ( optOneQuantPerRound() && d_addedLemmas>0 ) ){
+ break;
+ }
+ }else{
+ Trace("fmf-exh-inst") << "-> Inactive : " << f << std::endl;
}
}
+ if( d_addedLemmas>0 ){
+ break;
+ }else{
+ Assert( !d_quantEngine->inConflict() );
+ }
}
//print debug information
- Trace("model-engine") << "Added Lemmas = " << d_addedLemmas << " / " << d_triedLemmas << " / ";
- Trace("model-engine") << d_totalLemmas << std::endl;
+ if( d_quantEngine->inConflict() ){
+ Trace("model-engine") << "Conflict, size = " << d_quantEngine->getNumLemmasWaiting() << std::endl;
+ }else{
+ Trace("model-engine") << "Added Lemmas = " << d_addedLemmas << " / " << d_triedLemmas << " / ";
+ Trace("model-engine") << d_totalLemmas << std::endl;
+ }
return d_addedLemmas;
}
d_incomplete_check = d_incomplete_check || mb->d_incomplete_check;
d_statistics.d_mbqi_inst_lemmas += mb->d_addedLemmas;
}else{
- Trace("fmf-exh-inst-debug") << " Instantiation Constants: ";
- for( size_t i=0; i<f[0].getNumChildren(); i++ ){
- Trace("fmf-exh-inst-debug") << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) << " ";
+ if( Trace.isOn("fmf-exh-inst-debug") ){
+ Trace("fmf-exh-inst-debug") << " Instantiation Constants: ";
+ for( size_t i=0; i<f[0].getNumChildren(); i++ ){
+ Trace("fmf-exh-inst-debug") << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) << " ";
+ }
+ Trace("fmf-exh-inst-debug") << std::endl;
}
- Trace("fmf-exh-inst-debug") << std::endl;
//create a rep set iterator and iterate over the (relevant) domain of the quantifier
RepSetIterator riter( d_quantEngine, &(d_quantEngine->getModel()->d_rep_set) );
if( riter.setQuantifier( f ) ){
//add as instantiation
if( d_quantEngine->addInstantiation( f, m ) ){
addedLemmas++;
+ if( d_quantEngine->inConflict() ){
+ break;
+ }
}else{
Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl;
}
void RewriteEngine::check( Theory::Effort e, unsigned quant_e ) {
if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){
- //if( e==Theory::EFFORT_FULL ){
+ Assert( !d_quantEngine->inConflict() );
Trace("rewrite-engine") << "---Rewrite Engine Round, effort = " << e << "---" << std::endl;
//if( e==Theory::EFFORT_LAST_CALL ){
// if( !d_quantEngine->getModel()->isModelSet() ){
//per priority level
int index = 0;
bool success = true;
- while( success && index<(int)d_priority_order.size() ) {
+ while( !d_quantEngine->inConflict() && success && index<(int)d_priority_order.size() ) {
addedLemmas += checkRewriteRule( d_priority_order[index], e );
index++;
if( index<(int)d_priority_order.size() ){
}
Trace("rewrite-engine") << "Finished rewrite engine, added " << addedLemmas << " lemmas." << std::endl;
- if (addedLemmas==0) {
-
- }else{
- //otherwise, the search will continue
- }
}
}
Trace("rewrite-engine-inst-debug") << " Reset round..." << std::endl;
qi->reset_round( qcf );
Trace("rewrite-engine-inst-debug") << " Get matches..." << std::endl;
- while( qi->getNextMatch( qcf ) &&
+ while( !d_quantEngine->inConflict() && qi->getNextMatch( qcf ) &&
( addedLemmas==0 || !options::rrOneInstPerRound() ) ){
Trace("rewrite-engine-inst-debug") << " Got match to complete..." << std::endl;
qi->debugPrintMatch( "rewrite-engine-inst-debug" );
bool doContinue = false;
bool success = true;
int tempAddedLemmas = 0;
- while( tempAddedLemmas==0 && success && ( addedLemmas==0 || !options::rrOneInstPerRound() ) ){
+ while( !d_quantEngine->inConflict() && tempAddedLemmas==0 && success && ( addedLemmas==0 || !options::rrOneInstPerRound() ) ){
success = qi->completeMatch( qcf, assigned, doContinue );
doContinue = true;
if( success ){
QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te):
d_te( te ),
+ //d_quants(u),
+ //d_quants_red(u),
d_lemmas_produced_c(u),
d_skolemized(u),
d_ierCounter_c(c),
//utilities
d_eq_query = new EqualityQueryQuantifiersEngine( c, this );
d_util.push_back( d_eq_query );
-
+
d_term_db = new quantifiers::TermDb( c, u, this );
d_util.push_back( d_term_db );
-
+
if( options::instPropagate() ){
d_inst_prop = new quantifiers::InstPropagator( this );
d_util.push_back( d_inst_prop );
}
d_tr_trie = new inst::TriggerTrie;
+ d_curr_effort_level = QEFFORT_NONE;
+ d_conflict = false;
d_hasAddedLemma = false;
//don't add true lemma
d_lemmas_produced_c[d_term_db->d_true] = true;
d_rel_dom = NULL;
d_builder = NULL;
- d_curr_effort_level = QEFFORT_NONE;
d_total_inst_count_debug = 0;
//allow theory combination to go first, once initially
d_ierCounter = options::instWhenTcFirst() ? 0 : 1;
d_lte_part_inst = new quantifiers::LtePartialInst( this, c );
d_modules.push_back( d_lte_part_inst );
}
- if( ( options::finiteModelFind() && options::quantDynamicSplit()!=quantifiers::QUANT_DSPLIT_MODE_NONE ) ||
+ if( ( options::finiteModelFind() && options::quantDynamicSplit()!=quantifiers::QUANT_DSPLIT_MODE_NONE ) ||
options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_AGG ){
d_qsplit = new quantifiers::QuantDSplit( this, c );
d_modules.push_back( d_qsplit );
}
}
+ d_conflict = false;
d_hasAddedLemma = false;
bool setIncomplete = false;
if( e==Theory::EFFORT_LAST_CALL ){
if( d_hasAddedLemma ){
return;
}
-
+
if( Trace.isOn("quant-engine-debug") ){
Trace("quant-engine-debug") << "Quantifiers Engine check, level = " << e << std::endl;
Trace("quant-engine-debug") << " depth : " << d_ierCounter_c << std::endl;
Trace("quant-engine-assert") << "Assertions : " << std::endl;
getTheoryEngine()->printAssertions("quant-engine-assert");
}
-
+
//reset utilities
for( unsigned i=0; i<d_util.size(); i++ ){
Trace("quant-engine-debug2") << "Reset " << d_util[i]->identify().c_str() << "..." << std::endl;
//reset the model
d_model->reset_round();
-
+
//reset the modules
for( unsigned i=0; i<d_modules.size(); i++ ){
Trace("quant-engine-debug2") << "Reset " << d_modules[i]->identify().c_str() << std::endl;
flushLemmas();
if( d_hasAddedLemma ){
return;
+
}
if( e==Theory::EFFORT_LAST_CALL ){
for( unsigned i=0; i<qm.size(); i++ ){
Trace("quant-engine-debug") << "Check " << qm[i]->identify().c_str() << " at effort " << quant_e << "..." << std::endl;
qm[i]->check( e, quant_e );
+ if( d_conflict ){
+ Trace("quant-engine-debug") << "...conflict!" << std::endl;
+ break;
+ }
}
}
//flush all current lemmas
if( d_hasAddedLemma ){
break;
}else{
+ Assert( !d_conflict );
if( quant_e==QEFFORT_CONFLICT ){
if( e==Theory::EFFORT_FULL ){
//increment if a last call happened, we are not strictly enforcing interleaving, or already were in phase
d_quants_red[q] = false;
return false;
}else{
- return it->second;
+ return (*it).second;
}
}
return true;
}
}else{
- return it->second;
+ return (*it).second;
}
}
}
-bool QuantifiersEngine::recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq, bool modInst ) {
+bool QuantifiersEngine::recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq, bool modInst, bool addedLem ) {
+ if( !addedLem ){
+ //record the instantiation for deletion later
+ //TODO
+ }
if( options::incrementalSolving() ){
Trace("inst-add-debug") << "Adding into context-dependent inst trie, modEq = " << modEq << ", modInst = " << modInst << std::endl;
inst::CDInstMatchTrie* imt;
}
}
+bool QuantifiersEngine::removeInstantiationInternal( Node q, std::vector< Node >& terms ) {
+ if( options::incrementalSolving() ){
+ std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.find( q );
+ if( it!=d_c_inst_match_trie.end() ){
+ return it->second->removeInstMatch( this, q, terms );
+ }else{
+ return false;
+ }
+ }else{
+ return d_inst_match_trie[q].removeInstMatch( this, q, terms );
+ }
+}
+
void QuantifiersEngine::setInstantiationLevelAttr( Node n, Node qn, uint64_t level ){
Trace("inst-level-debug2") << "IL : " << n << " " << qn << " " << level << std::endl;
//if not from the vector of terms we instantiatied
lem = Rewriter::rewrite(lem);
}
Trace("inst-add-debug") << "Adding lemma : " << lem << std::endl;
- if( d_lemmas_produced_c.find( lem )==d_lemmas_produced_c.end() ){
+ BoolMap::const_iterator itp = d_lemmas_produced_c.find( lem );
+ if( itp==d_lemmas_produced_c.end() || !(*itp).second ){
//d_curr_out->lemma( lem, false, true );
d_lemmas_produced_c[ lem ] = true;
d_lemmas_waiting.push_back( lem );
}
}
+bool QuantifiersEngine::removeLemma( Node lem ) {
+ std::vector< Node >::iterator it = std::find( d_lemmas_waiting.begin(), d_lemmas_waiting.end(), lem );
+ if( it!=d_lemmas_waiting.end() ){
+ d_lemmas_waiting.erase( it, it + 1 );
+ d_lemmas_produced_c[ lem ] = false;
+ return true;
+ }else{
+ return false;
+ }
+}
+
void QuantifiersEngine::addRequirePhase( Node lit, bool req ){
d_phase_req_waiting[lit] = req;
}
bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bool mkRep, bool modEq, bool modInst, bool doVts ) {
// For resource-limiting (also does a time check).
getOutputChannel().safePoint(options::quantifierStep());
-
+ Assert( !d_conflict );
Assert( terms.size()==q[0].getNumChildren() );
Trace("inst-add-debug") << "For quantified formula " << q << ", add instantiation: " << std::endl;
for( unsigned i=0; i<terms.size(); i++ ){
}
Trace("inst-add-debug") << " -> " << terms[i] << std::endl;
if( terms[i].isNull() ){
- Trace("inst-add-debug") << " -> Failed to make term vector, due to term/type restrictions." << std::endl;
+ Trace("inst-add-debug") << " --> Failed to make term vector, due to term/type restrictions." << std::endl;
return false;
}
#ifdef CVC4_ASSERTIONS
bad_inst = true;
}else{
bad_inst = quantifiers::TermDb::containsTerms( terms[i], d_term_db->d_inst_constants[q] );
- }
+ }
}
}
//this assertion is critical to soundness
Trace("inst") << " " << terms[j] << std::endl;
}
Assert( false );
- }
+ }
#endif
}
}
}
}
-
+
//check for positive entailment
if( options::instNoEntail() ){
//TODO: check consistency of equality engine (if not aborting on utility's reset)
subs[q[0][i]] = terms[i];
}
if( d_term_db->isEntailed( q[1], subs, false, true ) ){
- Trace("inst-add-debug") << " -> Currently entailed." << std::endl;
+ Trace("inst-add-debug") << " --> Currently entailed." << std::endl;
return false;
}
//Node eval = d_term_db->evaluateTerm( q[1], subs, false, true );
//check for term vector duplication
bool alreadyExists = !recordInstantiationInternal( q, terms, modEq, modInst );
if( alreadyExists ){
- Trace("inst-add-debug") << " -> Already exists." << std::endl;
+ Trace("inst-add-debug") << " --> Already exists." << std::endl;
++(d_statistics.d_inst_duplicate_eq);
return false;
}
body = quantifiers::QuantifiersRewriter::preprocess( body, true );
Trace("inst-debug") << "...preprocess to " << body << std::endl;
- //construct the lemma
+ //construct the lemma
Trace("inst-assert") << "(assert " << body << ")" << std::endl;
body = Rewriter::rewrite(body);
Node lem = NodeManager::currentNM()->mkNode( kind::OR, q.negate(), body );
}
setInstantiationLevelAttr( body, q[1], maxInstLevel+1 );
}
- if( d_curr_effort_level>QEFFORT_CONFLICT ){
+ if( d_curr_effort_level>QEFFORT_CONFLICT && d_curr_effort_level<QEFFORT_NONE ){
//notify listeners
for( unsigned j=0; j<d_inst_notify.size(); j++ ){
- d_inst_notify[j]->notifyInstantiation( d_curr_effort_level, q, lem, terms, body );
+ if( !d_inst_notify[j]->notifyInstantiation( d_curr_effort_level, q, lem, terms, body ) ){
+ Trace("inst-add-debug") << "...we are in conflict." << std::endl;
+ d_conflict = true;
+ Assert( !d_lemmas_waiting.empty() );
+ }
}
}
- Trace("inst-add-debug") << " -> Success." << std::endl;
+ Trace("inst-add-debug") << " --> Success." << std::endl;
++(d_statistics.d_instantiations);
return true;
}else{
- Trace("inst-add-debug") << " -> Lemma already exists." << std::endl;
+ Trace("inst-add-debug") << " --> Lemma already exists." << std::endl;
++(d_statistics.d_inst_duplicate);
return false;
}
return addSplit( fm );
}
+bool QuantifiersEngine::removeInstantiation( Node q, Node lem, std::vector< Node >& terms ) {
+ //lem must occur in d_waiting_lemmas
+ if( removeLemma( lem ) ){
+ return removeInstantiationInternal( q, terms );
+ }else{
+ return false;
+ }
+}
+
+
bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) {
Trace("quant-engine-debug2") << "Get inst when needs check, counts=" << d_ierCounter << ", " << d_ierCounter_lc << std::endl;
//determine if we should perform check, based on instWhenMode
class InstantiationNotify {
public:
InstantiationNotify(){}
- virtual void notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) = 0;
+ virtual bool notifyInstantiation( unsigned quant_e, Node q, Node lem, std::vector< Node >& terms, Node body ) = 0;
};
namespace quantifiers {
//none
QEFFORT_NONE,
};
-private:
+private: //this information is reset during check
/** current effort level */
unsigned d_curr_effort_level;
+ /** are we in conflict */
+ bool d_conflict;
+ /** has added lemma this round */
+ bool d_hasAddedLemma;
+private:
/** list of all quantifiers seen */
std::map< Node, bool > d_quants;
/** quantifiers reduced */
std::vector< Node > d_lemmas_waiting;
/** phase requirements waiting */
std::map< Node, bool > d_phase_req_waiting;
- /** has added lemma this round */
- bool d_hasAddedLemma;
/** list of all instantiations produced for each quantifier */
std::map< Node, inst::InstMatchTrie > d_inst_match_trie;
std::map< Node, inst::CDInstMatchTrie* > d_c_inst_match_trie;
/** compute term vector */
void computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms );
/** record instantiation, return true if it was non-duplicate */
- bool recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq = false, bool modInst = false );
+ bool recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq = false, bool modInst = false, bool addedLem = true );
+ /** remove instantiation */
+ bool removeInstantiationInternal( Node q, std::vector< Node >& terms );
/** set instantiation level attr */
static void setInstantiationLevelAttr( Node n, Node qn, uint64_t level );
/** flush lemmas */
Node getSubstitute( Node n, std::vector< Node >& terms );
/** add lemma lem */
bool addLemma( Node lem, bool doCache = true, bool doRewrite = true );
+ /** remove pending lemma */
+ bool removeLemma( Node lem );
/** add require phase */
void addRequirePhase( Node lit, bool req );
/** do instantiation specified by m */
bool addInstantiation( Node q, InstMatch& m, bool mkRep = true, bool modEq = false, bool modInst = false, bool doVts = false );
/** add instantiation */
bool addInstantiation( Node q, std::vector< Node >& terms, bool mkRep = true, bool modEq = false, bool modInst = false, bool doVts = false );
+ /** remove pending instantiation */
+ bool removeInstantiation( Node q, Node lem, std::vector< Node >& terms );
/** split on node n */
bool addSplit( Node n, bool reqPhase = false, bool reqPhasePol = true );
/** add split equality */
bool addSplitEquality( Node n1, Node n2, bool reqPhase = false, bool reqPhasePol = true );
/** has added lemma */
bool hasAddedLemma() { return !d_lemmas_waiting.empty() || d_hasAddedLemma; }
+ /** is in conflict */
+ bool inConflict() { return d_conflict; }
/** get number of waiting lemmas */
unsigned getNumLemmasWaiting() { return d_lemmas_waiting.size(); }
/** get needs check */
/** get trigger database */
inst::TriggerTrie* getTriggerDatabase() { return d_tr_trie; }
/** add term to database */
- void addTermToDatabase( Node n, bool withinQuant = false, bool withinInstClosure = false );
+ void addTermToDatabase( Node n, bool withinQuant = false, bool withinInstClosure = false );
/** notification when master equality engine is updated */
void eqNotifyNewClass(TNode t);
void eqNotifyPreMerge(TNode t1, TNode t2);
lst-no-self-rev-exp.smt2 \
fib-core.smt2 \
fore19-exp2-core.smt2 \
- with-ind-104-core.smt2 \
syn002-si-real-int.smt2 \
krs-sat.smt2 \
forall_unit_data2.smt2 \
projects / cvc5.git / commitdiff