return theory::quantifiers::QCF_PROP_EQ;
} else if(optarg == "partial") {
return theory::quantifiers::QCF_PARTIAL;
- } else if(optarg == "mc" ) {
- return theory::quantifiers::QCF_MC;
} else if(optarg == "help") {
puts(s_qcfModeHelp.c_str());
exit(1);
QCF_PROP_EQ,
/** use qcf for conflicts, propagations and heuristic instantiations */
QCF_PARTIAL,
- /** use qcf for model checking */
- QCF_MC,
};
enum UserPatMode {
void QuantAntiSkolem::check( Theory::Effort e, unsigned quant_e ) {
if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){
d_sqtc.clear();
- for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+ for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
if( d_quant_processed.find( q )==d_quant_processed.end() ){
d_quant_processed[q] = true;
}
}
if( d_firstTime ){
- Assert( d_qe->getTermDatabase()->d_type_map[d_match_pattern_type].empty() );
//must return something
d_firstTime = false;
return d_qe->getTermDatabase()->getModelBasisTerm( d_match_pattern_type );
};
-void OpArgIndex::addTerm( ConjectureGenerator * s, TNode n, unsigned index ){
+void OpArgIndex::addTerm( std::vector< TNode >& terms, TNode n, unsigned index ){
if( index==n.getNumChildren() ){
Assert( n.hasOperator() );
if( std::find( d_ops.begin(), d_ops.end(), n.getOperator() )==d_ops.end() ){
d_op_terms.push_back( n );
}
}else{
- d_child[s->getTermDatabase()->d_arg_reps[n][index]].addTerm( s, n, index+1 );
+ d_child[terms[index]].addTerm( terms, n, index+1 );
}
}
TNode n = (*ieqc_i);
if( getTermDatabase()->hasTermCurrent( n ) ){
if( isHandledTerm( n ) ){
- d_op_arg_index[r].addTerm( this, n );
+ d_op_arg_index[r].addTerm( getTermDatabase()->d_arg_reps[n], n );
}
}
++ieqc_i;
d_thm_index.clear();
std::vector< Node > provenConj;
quantifiers::FirstOrderModel* m = d_quantEngine->getModel();
- for( int i=0; i<m->getNumAssertedQuantifiers(); i++ ){
+ for( unsigned i=0; i<m->getNumAssertedQuantifiers(); i++ ){
Node q = m->getAssertedQuantifier( i );
Trace("thm-db-debug") << "Is " << q << " a relevant theorem?" << std::endl;
Node conjEq;
if( d_match_status_child_num==0 ){
//initial binding
TNode f = s->getTgFunc( d_typ, d_status_num );
- std::map< TNode, TermArgTrie >::iterator it = s->getTermDatabase()->d_func_map_eqc_trie[f].d_data.find( eqc );
- if( it!=s->getTermDatabase()->d_func_map_eqc_trie[f].d_data.end() ){
- d_match_children.push_back( it->second.d_data.begin() );
- d_match_children_end.push_back( it->second.d_data.end() );
+ //std::map< TNode, TermArgTrie >::iterator it = s->getTermDatabase()->d_func_map_eqc_trie[f].d_data.find( eqc );
+ Assert( !eqc.isNull() );
+ TermArgTrie * tat = s->getTermDatabase()->getTermArgTrie( eqc, f );
+ if( tat ){
+ d_match_children.push_back( tat->d_data.begin() );
+ d_match_children_end.push_back( tat->d_data.end() );
}else{
d_match_status++;
d_match_status_child_num--;
std::map< TNode, OpArgIndex > d_child;
std::vector< TNode > d_ops;
std::vector< TNode > d_op_terms;
- void addTerm( ConjectureGenerator * s, TNode n, unsigned index = 0 );
+ void addTerm( std::vector< TNode >& terms, TNode n, unsigned index = 0 );
Node getGroundTerm( ConjectureGenerator * s, std::vector< TNode >& args );
void getGroundTerms( ConjectureGenerator * s, std::vector< TNode >& terms );
};
using namespace CVC4::theory::quantifiers;
using namespace CVC4::theory::quantifiers::fmcheck;
+struct sortQuantifierRelevance {
+ FirstOrderModel * d_fm;
+ bool operator() (Node i, Node j) {
+ int wi = d_fm->getRelevanceValue( i );
+ int wj = d_fm->getRelevanceValue( j );
+ if( wi==wj ){
+ return i<j;
+ }else{
+ return wi<wj;
+ }
+ }
+};
+
FirstOrderModel::FirstOrderModel(QuantifiersEngine * qe, context::Context* c, std::string name ) :
TheoryModel( c, name, true ),
d_qe( qe ), d_forall_asserts( c ), d_isModelSet( c, false ){
-
+ d_rlv_count = 0;
}
void FirstOrderModel::assertQuantifier( Node n ){
}
}
+unsigned FirstOrderModel::getNumAssertedQuantifiers() {
+ return d_forall_asserts.size();
+}
+
+Node FirstOrderModel::getAssertedQuantifier( unsigned i, bool ordered ) {
+ if( !ordered || d_forall_rlv_assert.empty() ){
+ return d_forall_asserts[i];
+ }else{
+ Assert( d_forall_rlv_assert.size()==d_forall_asserts.size() );
+ return d_forall_rlv_assert[i];
+ }
+}
+
Node FirstOrderModel::getCurrentModelValue( Node n, bool partial ) {
std::vector< Node > children;
if( n.getNumChildren()>0 ){
processInitialize( true );
//this is called after representatives have been chosen and the equality engine has been built
//for each quantifier, collect all operators we care about
- for( int i=0; i<getNumAssertedQuantifiers(); i++ ){
+ for( unsigned i=0; i<getNumAssertedQuantifiers(); i++ ){
Node f = getAssertedQuantifier( i );
if( d_quant_var_id.find( f )==d_quant_var_id.end() ){
- for(unsigned i=0; i<f[0].getNumChildren(); i++){
- d_quant_var_id[f][f[0][i]] = i;
+ for(unsigned j=0; j<f[0].getNumChildren(); j++){
+ d_quant_var_id[f][f[0][j]] = j;
}
}
processInitializeQuantifier( f );
void FirstOrderModel::reset_round() {
d_quant_active.clear();
+
+ //order the quantified formulas
+ if( !d_forall_rlv_vec.empty() ){
+ Trace("fm-relevant") << "Build sorted relevant list..." << std::endl;
+ d_forall_rlv_assert.clear();
+ Trace("fm-relevant-debug") << "Mark asserted quantified formulas..." << std::endl;
+ std::map< Node, bool > qassert;
+ for( unsigned i=0; i<d_forall_asserts.size(); i++ ){
+ qassert[d_forall_asserts[i]] = true;
+ }
+ Trace("fm-relevant-debug") << "Sort the relevant quantified formulas..." << std::endl;
+ sortQuantifierRelevance sqr;
+ sqr.d_fm = this;
+ std::sort( d_forall_rlv_vec.begin(), d_forall_rlv_vec.end(), sqr );
+ Trace("fm-relevant-debug") << "Add relevant asserted formulas..." << std::endl;
+ for( int i=(int)(d_forall_rlv_vec.size()-1); i>=0; i-- ){
+ Node q = d_forall_rlv_vec[i];
+ if( qassert.find( q )!=qassert.end() ){
+ Trace("fm-relevant") << " " << d_forall_rlv[q] << " : " << q << std::endl;
+ d_forall_rlv_assert.push_back( q );
+ }
+ }
+ Trace("fm-relevant-debug") << "Add remaining asserted formulas..." << std::endl;
+ for( unsigned i=0; i<d_forall_asserts.size(); i++ ){
+ Node q = d_forall_asserts[i];
+ if( std::find( d_forall_rlv_assert.begin(), d_forall_rlv_assert.end(), q )==d_forall_rlv_assert.end() ){
+ d_forall_rlv_assert.push_back( q );
+ }else{
+ Trace("fm-relevant-debug") << "...already included " << q << std::endl;
+ }
+ }
+ Trace("fm-relevant-debug") << "Sizes : " << d_forall_rlv_assert.size() << " " << d_forall_asserts.size() << std::endl;
+ Assert( d_forall_rlv_assert.size()==d_forall_asserts.size() );
+ }
+}
+
+void FirstOrderModel::markRelevant( Node q ) {
+ if( q!=d_last_forall_rlv ){
+ Trace("fm-relevant") << "Mark relevant : " << q << std::endl;
+ if( std::find( d_forall_rlv_vec.begin(), d_forall_rlv_vec.end(), q )==d_forall_rlv_vec.end() ){
+ d_forall_rlv_vec.push_back( q );
+ }
+ d_forall_rlv[ q ] = d_rlv_count;
+ d_rlv_count++;
+ d_last_forall_rlv = q;
+ }
+}
+
+int FirstOrderModel::getRelevanceValue( Node q ) {
+ std::map< Node, unsigned >::iterator it = d_forall_rlv.find( q );
+ if( it==d_forall_rlv.end() ){
+ return -1;
+ }else{
+ return it->second;
+ }
}
//bool FirstOrderModel::isQuantifierAsserted( TNode q ) {
QuantifiersEngine * d_qe;
/** list of quantifiers asserted in the current context */
context::CDList<Node> d_forall_asserts;
+ /** quantified formulas marked as relevant */
+ unsigned d_rlv_count;
+ std::map< Node, unsigned > d_forall_rlv;
+ std::vector< Node > d_forall_rlv_vec;
+ Node d_last_forall_rlv;
+ std::vector< Node > d_forall_rlv_assert;
/** is model set */
context::CDO< bool > d_isModelSet;
/** get variable id */
/** assert quantifier */
void assertQuantifier( Node n );
/** get number of asserted quantifiers */
- int getNumAssertedQuantifiers() { return (int)d_forall_asserts.size(); }
+ unsigned getNumAssertedQuantifiers();
/** get asserted quantifier */
- Node getAssertedQuantifier( int i ) { return d_forall_asserts[i]; }
+ Node getAssertedQuantifier( unsigned i, bool ordered = false );
/** initialize model for term */
void initializeModelForTerm( Node n, std::map< Node, bool >& visited );
virtual void processInitializeModelForTerm( Node n ) = 0;
public:
/** reset round */
void reset_round();
- /** is quantified formula asserted */
- //bool isQuantifierAsserted( TNode q );
+ /** mark quantified formula relevant */
+ void markRelevant( Node q );
+ /** get relevance value */
+ int getRelevanceValue( Node q );
/** set quantified formula active/inactive
* a quantified formula may be set inactive if for instance:
* - it is entailed by other quantified formulas
}
//do not have to introduce terms for sorts of domains of quantified formulas if we are allowed to assume empty sorts
if( !options::fmfEmptySorts() ){
- for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+ for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
Node q = fm->getAssertedQuantifier( i );
//make sure all types are set
- for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
- preInitializeType( fm, q[0][i].getType() );
+ for( unsigned j=0; j<q[0].getNumChildren(); j++ ){
+ preInitializeType( fm, q[0][j].getType() );
}
}
}
}else{
Trace("qip-prop-debug") << it->first << " ";
}
+ }else{
+ //mark the quantified formula as relevant
+ d_qe->markRelevant( it->second.d_q );
}
}
Trace("qip-prop-debug") << std::endl;
}
unsigned InstStrategyCbqi::needsModel( Theory::Effort e ) {
- for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+ for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
return QuantifiersEngine::QEFFORT_STANDARD;
d_cbqi_set_quant_inactive = false;
d_incomplete_check = false;
//check if any cbqi lemma has not been added yet
- for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+ for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
//it is not active if it corresponds to a rewrite rule: we will process in rewrite engine
if( doCbqi( q ) ){
}
unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting();
for( int ee=0; ee<=1; ee++ ){
- for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+ for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
process( q, e, ee );
Node InstStrategyCbqi::getNextDecisionRequest(){
// all counterexample literals that are not asserted
- for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+ for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
if( hasAddedCbqiLemma( q ) ){
Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q );
}
}
//print debug
- Debug("quant-arith-debug") << std::endl;
- debugPrint( "quant-arith-debug" );
+ if( Debug.isOn("quant-arith-debug") ){
+ Debug("quant-arith-debug") << std::endl;
+ debugPrint( "quant-arith-debug" );
+ }
d_counter++;
}
bool m_point_valid = true;
int lem = 0;
//scan over all instantiation rows
- for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
+ for( unsigned i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i );
Debug("quant-arith-simplex") << "InstStrategySimplex check " << ic << ", rows = " << d_instRows[ic].size() << std::endl;
- for( int j=0; j<(int)d_instRows[ic].size(); j++ ){
+ for( unsigned j=0; j<d_instRows[ic].size(); j++ ){
ArithVar x = d_instRows[ic][j];
if( !d_ceTableaux[ic][x].empty() ){
if( Debug.isOn("quant-arith-simplex") ){
}
Debug(c) << std::endl;
- for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+ for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
Node f = d_quantEngine->getModel()->getAssertedQuantifier( i );
Debug(c) << f << std::endl;
Debug(c) << " Inst constants: ";
- for( int i=0; i<(int)d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
- if( i>0 ){
+ for( unsigned j=0; j<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){
+ if( j>0 ){
Debug( c ) << ", ";
}
Debug( c ) << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i );
}
Debug(c) << std::endl;
- for( int j=0; j<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); j++ ){
+ for( unsigned j=0; j<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); j++ ){
Node ic = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j );
Debug(c) << " Instantiation rows for " << ic << " : ";
- for( int i=0; i<(int)d_instRows[ic].size(); i++ ){
- if( i>0 ){
+ for( unsigned k=0; k<d_instRows[ic].size(); k++ ){
+ if( k>0 ){
Debug(c) << ", ";
}
- Debug(c) << d_instRows[ic][i];
+ Debug(c) << d_instRows[ic][k];
}
Debug(c) << std::endl;
}
//must register with the instantiator
//must explicitly remove ITEs so that we record dependencies
std::vector< Node > ce_vars;
- for( int i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( q ); i++ ){
+ for( unsigned i=0; i<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( q ); i++ ){
ce_vars.push_back( d_quantEngine->getTermDatabase()->getInstantiationConstant( q, i ) );
}
std::vector< Node > lems;
Trace("fs-engine") << "---Full Saturation Round, effort = " << e << "---" << std::endl;
}
int addedLemmas = 0;
- for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
- Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
+ for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+ Node q = d_quantEngine->getModel()->getAssertedQuantifier( i, true );
if( d_quantEngine->hasOwnership( q, this ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
if( process( q, fullEffort ) ){
//added lemma
if( r==0 ){
ts = rd->getRDomain( f, i )->d_terms.size();
}else{
- ts = d_quantEngine->getTermDatabase()->d_type_map[f[0][i].getType()].size();
+ ts = d_quantEngine->getTermDatabase()->getNumTypeGroundTerms( f[0][i].getType() );
}
max_zero.push_back( fullEffort && ts==0 );
ts = ( fullEffort && ts==0 ) ? 1 : ts;
}
}
if( !has_zero ){
+ std::vector< TypeNode > ftypes;
+ for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
+ ftypes.push_back( f[0][i].getType() );
+ }
+
Trace("inst-alg-rd") << "Will do " << final_max_i << " stages of instantiation." << std::endl;
unsigned max_i = 0;
bool success;
if( options::cbqi() && r==1 && !max_zero[index] ){
//skip inst constant nodes
while( nv<maxs[index] && nv<=max_i &&
- quantifiers::TermDb::hasInstConstAttr( d_quantEngine->getTermDatabase()->d_type_map[f[0][index].getType()][nv] ) ){
+ quantifiers::TermDb::hasInstConstAttr( d_quantEngine->getTermDatabase()->getTypeGroundTerm( ftypes[index], nv ) ) ){
nv++;
}
}
}else if( r==0 ){
terms.push_back( rd->getRDomain( f, i )->d_terms[childIndex[i]] );
}else{
- terms.push_back( d_quantEngine->getTermDatabase()->d_type_map[f[0][i].getType()][childIndex[i]] );
+ terms.push_back( d_quantEngine->getTermDatabase()->getTypeGroundTerm( ftypes[i], childIndex[i] ) );
}
}
if( d_quantEngine->addInstantiation( f, terms, false ) ){
//collect all active quantified formulas belonging to this
bool quantActive = false;
d_quants.clear();
- for( int i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
- Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
+ for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+ Node q = d_quantEngine->getModel()->getAssertedQuantifier( i, true );
if( d_quantEngine->hasOwnership( q, this ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
quantActive = true;
d_quants.push_back( q );
doInstantiationRound( e );
if( d_quantEngine->inConflict() ){
Assert( d_quantEngine->getNumLemmasWaiting()>lastWaiting );
- Trace("inst-engine") << "Conflict, size = " << d_quantEngine->getNumLemmasWaiting();
+ Trace("inst-engine") << "Conflict = " << d_quantEngine->getNumLemmasWaiting() << " / " << d_quantEngine->getNumLemmasAddedThisRound();
if( lastWaiting>0 ){
Trace("inst-engine") << " (prev " << lastWaiting << ")";
}
Trace("quant-check-model") << "Testing quantifier instantiations..." << std::endl;
int tests = 0;
int bad = 0;
- for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+ for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
Node f = fm->getAssertedQuantifier( i );
std::vector< Node > vars;
- for( int j=0; j<(int)f[0].getNumChildren(); j++ ){
+ for( unsigned j=0; j<f[0].getNumChildren(); j++ ){
vars.push_back( f[0][j] );
}
RepSetIterator riter( d_qe, &(fm->d_rep_set) );
while( !riter.isFinished() ){
tests++;
std::vector< Node > terms;
- for( int i=0; i<riter.getNumTerms(); i++ ){
- terms.push_back( riter.getTerm( i ) );
+ for( int k=0; k<riter.getNumTerms(); k++ ){
+ terms.push_back( riter.getTerm( k ) );
}
Node n = d_qe->getInstantiation( f, vars, terms );
Node val = fm->getValue( n );
if( optUseModel() ){
Trace("model-engine-debug") << "Initializing " << fm->getNumAssertedQuantifiers() << " quantifiers..." << std::endl;
//check if any quantifiers are un-initialized
- for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+ for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
Node f = fm->getAssertedQuantifier( i );
if( isQuantifierActive( f ) ){
int lems = initializeQuantifier( f, f );
Trace("model-engine-debug") << "Analyzing quantifiers..." << std::endl;
d_quant_sat.clear();
d_uf_prefs.clear();
- for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+ for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
Node f = fm->getAssertedQuantifier( i );
if( isQuantifierActive( f ) ){
analyzeQuantifier( fm, f );
d_numQuantNoSelForm = 0;
//now, see if we know that any exceptions via InstGen exist
Trace("model-engine-debug") << "Perform InstGen techniques for quantifiers..." << std::endl;
- for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+ for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
Node f = fm->getAssertedQuantifier( i );
if( isQuantifierActive( f ) ){
int lems = doInstGen( fm, f );
Trace("model-engine-debug") << "Check model..." << std::endl;
d_incomplete_check = false;
//print debug
- Trace("fmf-model-complete") << std::endl;
- debugPrint("fmf-model-complete");
+ if( Trace.isOn("fmf-model-complete") ){
+ Trace("fmf-model-complete") << std::endl;
+ debugPrint("fmf-model-complete");
+ }
//successfully built an acceptable model, now check it
addedLemmas += checkModel();
}else{
if( addedLemmas==0 ){
Trace("model-engine-debug") << "No lemmas added, incomplete = " << d_incomplete_check << std::endl;
//CVC4 will answer SAT or unknown
- Trace("fmf-consistent") << std::endl;
- debugPrint("fmf-consistent");
+ if( Trace.isOn("fmf-consistent") ){
+ Trace("fmf-consistent") << std::endl;
+ debugPrint("fmf-consistent");
+ }
}
}
}
d_addedLemmas = 0;
d_totalLemmas = 0;
//for statistics
- for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
- Node f = fm->getAssertedQuantifier( i );
- int totalInst = 1;
- for( size_t i=0; i<f[0].getNumChildren(); i++ ){
- TypeNode tn = f[0][i].getType();
- if( fm->d_rep_set.hasType( tn ) ){
- totalInst = totalInst * (int)fm->d_rep_set.d_type_reps[ tn ].size();
+ if( Trace.isOn("model-engine") ){
+ for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+ Node f = fm->getAssertedQuantifier( i );
+ int totalInst = 1;
+ for( unsigned j=0; j<f[0].getNumChildren(); j++ ){
+ TypeNode tn = f[0][j].getType();
+ if( fm->d_rep_set.hasType( tn ) ){
+ totalInst = totalInst * (int)fm->d_rep_set.d_type_reps[ tn ].size();
+ }
}
+ d_totalLemmas += totalInst;
}
- d_totalLemmas += totalInst;
}
Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl;
// 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++) {
- for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
- Node f = fm->getAssertedQuantifier( i );
+ for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+ Node f = fm->getAssertedQuantifier( i, true );
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( d_quantEngine->inConflict() || ( optOneQuantPerRound() && d_addedLemmas>0 ) ){
break;
}
//print debug information
if( d_quantEngine->inConflict() ){
- Trace("model-engine") << "Conflict, size = " << d_quantEngine->getNumLemmasWaiting() << std::endl;
+ Trace("model-engine") << "Conflict = " << d_quantEngine->getNumLemmasWaiting() << " / " << d_quantEngine->getNumLemmasAddedThisRound() << std::endl;
}else{
Trace("model-engine") << "Added Lemmas = " << d_addedLemmas << " / " << d_triedLemmas << " / ";
Trace("model-engine") << d_totalLemmas << std::endl;
void ModelEngine::debugPrint( const char* c ){
Trace( c ) << "Quantifiers: " << std::endl;
- for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
- Node f = d_quantEngine->getModel()->getAssertedQuantifier( i );
+ for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+ Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
Trace( c ) << " ";
- if( !d_quantEngine->getModelBuilder()->isQuantifierActive( f ) ){
+ if( !d_quantEngine->getModelBuilder()->isQuantifierActive( q ) ){
Trace( c ) << "*Inactive* ";
}else{
Trace( c ) << " ";
}
- Trace( c ) << f << std::endl;
+ Trace( c ) << q << std::endl;
}
//d_quantEngine->getModel()->debugPrint( c );
}
#include "theory/quantifiers/quant_util.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/trigger.h"
+#include "theory/quantifiers/first_order_model.h"
#include "theory/theory_engine.h"
using namespace CVC4::kind;
}
-void QuantInfo::initialize( Node q, Node qn ) {
+void QuantInfo::initialize( QuantConflictFind * p, Node q, Node qn ) {
d_q = q;
for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
d_match.push_back( TNode::null() );
Trace("qcf-invalid") << "QCF invalid : body of formula cannot be processed." << std::endl;
}
Trace("qcf-qregister-summary") << "QCF register : " << ( d_mg->isValid() ? "VALID " : "INVALID" ) << " : " << q << std::endl;
+
+ if( d_mg->isValid() ){
+ //optimization : record variable argument positions for terms that must be matched
+ std::vector< TNode > vars;
+ //TODO: revisit this, makes QCF faster, but misses conflicts due to caring about paths that may not be relevant (starExec jobs 14136/14137)
+ //if( options::qcfSkipRd() ){
+ // for( unsigned j=q[0].getNumChildren(); j<d_vars.size(); j++ ){
+ // vars.push_back( d_vars[j] );
+ // }
+ //}
+ //get all variables that are always relevant
+ std::map< TNode, bool > visited;
+ getPropagateVars( vars, q[1], false, visited );
+ for( unsigned j=0; j<vars.size(); j++ ){
+ Node v = vars[j];
+ TNode f = p->getTermDatabase()->getMatchOperator( v );
+ if( !f.isNull() ){
+ Trace("qcf-opt") << "Record variable argument positions in " << v << ", op=" << f << "..." << std::endl;
+ for( unsigned k=0; k<v.getNumChildren(); k++ ){
+ Node n = v[k];
+ std::map< TNode, int >::iterator itv = d_var_num.find( n );
+ if( itv!=d_var_num.end() ){
+ Trace("qcf-opt") << " arg " << k << " is var #" << itv->second << std::endl;
+ if( std::find( d_var_rel_dom[itv->second][f].begin(), d_var_rel_dom[itv->second][f].end(), k )==d_var_rel_dom[itv->second][f].end() ){
+ d_var_rel_dom[itv->second][f].push_back( k );
+ }
+ }
+ }
+ }
+ }
+ }
+}
+
+void QuantInfo::getPropagateVars( std::vector< TNode >& vars, TNode n, bool pol, std::map< TNode, bool >& visited ){
+ std::map< TNode, bool >::iterator itv = visited.find( n );
+ if( itv==visited.end() ){
+ visited[n] = true;
+ bool rec = true;
+ bool newPol = pol;
+ if( d_var_num.find( n )!=d_var_num.end() ){
+ Assert( std::find( vars.begin(), vars.end(), n )==vars.end() );
+ vars.push_back( n );
+ }else if( MatchGen::isHandledBoolConnective( n ) ){
+ Assert( n.getKind()!=IMPLIES );
+ QuantPhaseReq::getEntailPolarity( n, 0, true, pol, rec, newPol );
+ }
+ Trace("qcf-opt-debug") << "getPropagateVars " << n << ", pol = " << pol << ", rec = " << rec << std::endl;
+ if( rec ){
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ getPropagateVars( vars, n[i], pol, visited );
+ }
+ }
+ }
}
void QuantInfo::registerNode( Node n, bool hasPol, bool pol, bool beneathQuant ) {
return 1;
}else{
//std::map< int, TNode >::iterator itm = d_match.find( v );
-
+ bool isGroundRep = false;
if( vn!=-1 ){
Debug("qcf-match-debug") << " ...Variable bound to variable" << std::endl;
//std::map< int, TNode >::iterator itmn = d_match.find( vn );
}else{
Debug("qcf-match-debug") << " ...Variable bound to ground" << std::endl;
if( d_match[v].isNull() ){
+ //isGroundRep = true; ??
}else{
//compare ground values
Debug("qcf-match-debug") << " -> Ground value, compare " << d_match[v] << " "<< n << std::endl;
return p->areMatchEqual( d_match[v], n ) ? 0 : -1;
}
}
- if( setMatch( p, v, n ) ){
+ if( setMatch( p, v, n, isGroundRep ) ){
Debug("qcf-match-debug") << " -> success" << std::endl;
return 1;
}else{
}
}
-bool QuantInfo::setMatch( QuantConflictFind * p, int v, TNode n ) {
+bool QuantInfo::setMatch( QuantConflictFind * p, int v, TNode n, bool isGroundRep ) {
if( getCurrentCanBeEqual( p, v, n ) ){
+ if( isGroundRep ){
+ //fail if n does not exist in the relevant domain of each of the argument positions
+ std::map< int, std::map< TNode, std::vector< unsigned > > >::iterator it = d_var_rel_dom.find( v );
+ if( it!=d_var_rel_dom.end() ){
+ for( std::map< TNode, std::vector< unsigned > >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
+ for( unsigned j=0; j<it2->second.size(); j++ ){
+ Debug("qcf-match-debug2") << n << " in relevant domain " << it2->second << "." << it2->second[j] << "?" << std::endl;
+ if( !p->getTermDatabase()->inRelevantDomain( it2->first, it2->second[j], n ) ){
+ Debug("qcf-match-debug") << " -> fail, since " << n << " is not in relevant domain of " << it2->second << "." << it2->second[j] << std::endl;
+ return false;
+ }
+ }
+ }
+ }
+ }
Debug("qcf-match-debug") << "-- bind : " << v << " -> " << n << ", checked " << d_curr_var_deq[v].size() << " disequalities" << std::endl;
d_match[v] = n;
return true;
if( !z.isNull() ){
Trace("qcf-tconstraint-debug") << "...set " << d_vars[vn] << " = " << z << std::endl;
assigned.push_back( vn );
- if( !setMatch( p, vn, z ) ){
+ if( !setMatch( p, vn, z, false ) ){
success = false;
break;
}
if( !sum.isNull() ){
assigned.push_back( slv_v );
Trace("qcf-tconstraint-debug") << "...set " << d_vars[slv_v] << " = " << sum << std::endl;
- if( !setMatch( p, slv_v, sum ) ){
+ if( !setMatch( p, slv_v, sum, false ) ){
success = false;
}
p->d_tempCache.push_back( sum );
int currIndex = d_una_eqc_count[d_una_index];
d_una_eqc_count[d_una_index]++;
Trace("qcf-check-unassign") << d_unassigned[d_una_index] << "->" << p->d_eqcs[d_unassigned_tn[d_una_index]][currIndex] << std::endl;
- if( setMatch( p, d_unassigned[d_una_index], p->d_eqcs[d_unassigned_tn[d_una_index]][currIndex] ) ){
+ if( setMatch( p, d_unassigned[d_una_index], p->d_eqcs[d_unassigned_tn[d_una_index]][currIndex], true ) ){
d_match_term[d_unassigned[d_una_index]] = TNode::null();
Trace("qcf-check-unassign") << "Succeeded match " << d_una_index << std::endl;
d_una_index++;
}else{
//unassigned, set match to true/false
d_qni_bound[0] = vn;
- qi->setMatch( p, vn, d_tgt ? p->d_true : p->d_false );
+ qi->setMatch( p, vn, d_tgt ? p->d_true : p->d_false, false );
d_child_counter = 0;
}
if( d_child_counter==0 ){
d_qni_bound_cons.clear();
}
}
- /*
- if( d_type==typ_var && p->d_effort==QuantConflictFind::effort_mc && !d_matched_basis ){
- d_matched_basis = true;
- Node f = getMatchOperator( d_n );
- TNode mbo = p->getTermDatabase()->getModelBasisOpTerm( f );
- if( qi->setMatch( p, d_qni_var_num[0], mbo ) ){
- success = true;
- d_qni_bound[0] = d_qni_var_num[0];
- }
- }
- */
}
Debug("qcf-match") << " ...finished matching for " << d_n << ", success = " << success << std::endl;
d_wasSet = success;
if( it != d_qn[index]->d_data.end() ) {
d_qni.push_back( it );
//set the match
- if( it->first.getType().isComparableTo( qi->d_var_types[repVar] ) && qi->setMatch( p, d_qni_bound[index], it->first ) ){
+ if( it->first.getType().isComparableTo( qi->d_var_types[repVar] ) && qi->setMatch( p, d_qni_bound[index], it->first, true ) ){
Debug("qcf-match-debug") << " Binding variable" << std::endl;
if( d_qn.size()<d_qni_size ){
d_qn.push_back( &it->second );
d_qni[index]++;
if( d_qni[index]!=d_qn[index]->d_data.end() ){
success = true;
- if( qi->setMatch( p, itb->second, d_qni[index]->first ) ){
+ if( qi->setMatch( p, itb->second, d_qni[index]->first, true ) ){
Debug("qcf-match-debug") << " Bind next variable" << std::endl;
if( d_qn.size()<d_qni_size ){
d_qn.push_back( &d_qni[index]->second );
QuantConflictFind::QuantConflictFind( QuantifiersEngine * qe, context::Context* c ) :
QuantifiersModule( qe ),
-d_conflict( c, false ),
-d_qassert( c ) {
+d_conflict( c, false ) {
d_fid_count = 0;
d_true = NodeManager::currentNM()->mkConst<bool>(true);
d_false = NodeManager::currentNM()->mkConst<bool>(false);
Trace("qcf-qregister") << " : " << q << std::endl;
//make QcfNode structure
Trace("qcf-qregister") << "- Get relevant equality/disequality pairs, calculate flattening..." << std::endl;
- d_qinfo[q].initialize( q, q[1] );
+ d_qinfo[q].initialize( this, q, q[1] );
//debug print
Trace("qcf-qregister") << "- Flattened structure is :" << std::endl;
Trace("qcf-qregister") << std::endl;
}
}
-
+
Trace("qcf-qregister") << "Done registering quantifier." << std::endl;
}
}
short QuantConflictFind::getMaxQcfEffort() {
if( options::qcfMode()==QCF_CONFLICT_ONLY ){
return effort_conflict;
- }else if( options::qcfMode()==QCF_PROP_EQ ){
+ }else if( options::qcfMode()==QCF_PROP_EQ || options::qcfMode()==QCF_PARTIAL ){
return effort_prop_eq;
- }else if( options::qcfMode()==QCF_MC ){
- return effort_mc;
}else{
return 0;
}
//-------------------------------------------------- handling assertions / eqc
void QuantConflictFind::assertNode( Node q ) {
+ /*
if( d_quantEngine->hasOwnership( q, this ) ){
Trace("qcf-proc") << "QCF : assertQuantifier : ";
debugPrintQuant("qcf-proc", q);
Trace("qcf-proc") << std::endl;
- d_qassert.push_back( q );
- //set the eqRegistries that this depends on to true
- //for( std::map< EqRegistry *, bool >::iterator it = d_qinfo[q].d_rel_eqr.begin(); it != d_qinfo[q].d_rel_eqr.end(); ++it ){
- // it->first->d_active.set( true );
- //}
}
+ */
}
/** new node */
//determine order for quantified formulas
std::vector< Node > qorder;
- std::map< Node, bool > qassert;
- //mark which are asserted
- for( unsigned i=0; i<d_qassert.size(); i++ ){
- qassert[d_qassert[i]] = true;
- }
- //add which ones are specified in the order
- for( unsigned i=0; i<d_quant_order.size(); i++ ){
- Node n = d_quant_order[i];
- if( std::find( qorder.begin(), qorder.end(), n )==qorder.end() && qassert.find( n )!=qassert.end() ){
- qorder.push_back( n );
- }
- }
- d_quant_order.clear();
- d_quant_order.insert( d_quant_order.begin(), qorder.begin(), qorder.end() );
- //add remaining
- for( unsigned i=0; i<d_qassert.size(); i++ ){
- Node n = d_qassert[i];
- if( std::find( qorder.begin(), qorder.end(), n )==qorder.end() ){
- qorder.push_back( n );
+ for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
+ Node q = d_quantEngine->getModel()->getAssertedQuantifier( i, true );
+ if( d_quantEngine->hasOwnership( q, this ) ){
+ qorder.push_back( q );
}
}
-
if( Trace.isOn("qcf-debug") ){
Trace("qcf-debug") << std::endl;
debugPrint("qcf-debug");
Trace("qcf-inst") << std::endl;
++addedLemmas;
if( e==effort_conflict ){
- d_quant_order.insert( d_quant_order.begin(), q );
+ d_quantEngine->markRelevant( q );
++(d_statistics.d_conflict_inst);
if( options::qcfAllConflict() ){
isConflict = true;
}
break;
}else if( e==effort_prop_eq ){
+ d_quantEngine->markRelevant( q );
++(d_statistics.d_prop_inst);
}
}else{
//d_uf_terms.clear();
//d_eqc_uf_terms.clear();
d_eqcs.clear();
- d_model_basis.clear();
//d_arg_reps.clear();
//double clSet = 0;
//if( Trace.isOn("qcf-opt") ){
// clSet = double(clock())/double(CLOCKS_PER_SEC);
//}
- //long nTermst = 0;
- //long nTerms = 0;
- //long nEqc = 0;
-
- //which nodes are irrelevant for disequality matches
- std::map< TNode, bool > irrelevant_dnode;
//now, store matches
eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( getEqualityEngine() );
while( !eqcs_i.isFinished() ){
- //nEqc++;
Node r = (*eqcs_i);
if( getTermDatabase()->hasTermCurrent( r ) ){
TypeNode rtn = r.getType();
- if( options::qcfMode()==QCF_MC ){
- std::map< TypeNode, std::vector< TNode > >::iterator itt = d_eqcs.find( rtn );
- if( itt==d_eqcs.end() ){
- Node mb = getTermDatabase()->getModelBasisTerm( rtn );
- if( !getEqualityEngine()->hasTerm( mb ) ){
- Trace("qcf-warn") << "WARNING: Model basis term does not exist!" << std::endl;
- Assert( false );
- }
- Node mbr = getRepresentative( mb );
- if( mbr!=r ){
- d_eqcs[rtn].push_back( mbr );
- }
- d_eqcs[rtn].push_back( r );
- d_model_basis[rtn] = mb;
- }else{
- itt->second.push_back( r );
- }
- }else{
- if( !options::cbqi() || !TermDb::hasInstConstAttr( r ) ){
- d_eqcs[rtn].push_back( r );
- }
+ if( !options::cbqi() || !TermDb::hasInstConstAttr( r ) ){
+ d_eqcs[rtn].push_back( r );
}
}
++eqcs_i;
}
- /*
- if( Trace.isOn("qcf-opt") ){
- double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
- Trace("qcf-opt") << "Compute rel eqc : " << std::endl;
- Trace("qcf-opt") << " " << nEqc << " equivalence classes. " << std::endl;
- Trace("qcf-opt") << " " << nTerms << " / " << nTermst << " terms." << std::endl;
- Trace("qcf-opt") << " Time : " << (clSet2-clSet) << std::endl;
- }
- */
}
}
++eqc_i;
}
Trace(c) << (pr ? " " : "" ) << "}" << std::endl;
- /*
- EqcInfo * eqcn = getEqcInfo( n, false );
- if( eqcn ){
- Trace(c) << " DEQ : {";
- pr = false;
- for( NodeBoolMap::iterator it = eqcn->d_diseq.begin(); it != eqcn->d_diseq.end(); ++it ){
- if( (*it).second ){
- Trace(c) << (pr ? "," : "" ) << " " << (*it).first;
- pr = true;
- }
- }
- Trace(c) << (pr ? " " : "" ) << "}" << std::endl;
- }
- //}
- */
++eqcs_i;
}
}
int d_unassigned_nvar;
int d_una_index;
std::vector< int > d_una_eqc_count;
+ //optimization: track which arguments variables appear under UF terms in
+ std::map< int, std::map< TNode, std::vector< unsigned > > > d_var_rel_dom;
+ void getPropagateVars( std::vector< TNode >& vars, TNode n, bool pol, std::map< TNode, bool >& visited );
public:
QuantInfo();
~QuantInfo();
bool containsVarMg(int i) const { return var_mg_find(i) != var_mg_end(); }
bool matchGeneratorIsValid() const { return d_mg->isValid(); }
- bool getNextMatch( QuantConflictFind * p) {
+ bool getNextMatch( QuantConflictFind * p ) {
return d_mg->getNextMatch(p, this);
}
void reset_round( QuantConflictFind * p );
public:
//initialize
- void initialize( Node q, Node qn );
+ void initialize( QuantConflictFind * p, Node q, Node qn );
//current constraints
std::vector< TNode > d_match;
std::vector< TNode > d_match_term;
bool getCurrentCanBeEqual( QuantConflictFind * p, int v, TNode n, bool chDiseq = false );
int addConstraint( QuantConflictFind * p, int v, TNode n, bool polarity );
int addConstraint( QuantConflictFind * p, int v, TNode n, int vn, bool polarity, bool doRemove );
- bool setMatch( QuantConflictFind * p, int v, TNode n );
+ bool setMatch( QuantConflictFind * p, int v, TNode n, bool isGroundRep );
bool isMatchSpurious( QuantConflictFind * p );
bool isTConstraintSpurious( QuantConflictFind * p, std::vector< Node >& terms );
bool entailmentTest( QuantConflictFind * p, Node lit, bool chEnt = true );
typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
private:
context::CDO< bool > d_conflict;
- std::vector< Node > d_quant_order;
std::map< Kind, Node > d_zero;
//for storing nodes created during t-constraint solving (prevents memory leaks)
std::vector< Node > d_tempCache;
Node d_false;
TNode getZero( Kind k );
private:
- //currently asserted quantifiers
- NodeList d_qassert;
std::map< Node, QuantInfo > d_qinfo;
private: //for equivalence classes
// type -> list(eqc)
std::map< TypeNode, std::vector< TNode > > d_eqcs;
- std::map< TypeNode, Node > d_model_basis;
public:
enum {
effort_conflict,
effort_prop_eq,
- effort_mc,
};
short d_effort;
void setEffort( int e ) { d_effort = e; }
it2->second->reset();
}
}
- for( int i=0; i<d_model->getNumAssertedQuantifiers(); i++ ){
+ for( unsigned i=0; i<d_model->getNumAssertedQuantifiers(); i++ ){
Node q = d_model->getAssertedQuantifier( i );
Node icf = d_qe->getTermDatabase()->getInstConstantBody( q );
Trace("rel-dom-debug") << "compute relevant domain for " << icf << std::endl;
//make the quantified formula
d_qinfo_n[f] = NodeManager::currentNM()->mkNode( FORALL, qcfn_c );
Trace("rr-register") << " qcf formula is : " << d_qinfo_n[f] << std::endl;
- d_qinfo[f].initialize( d_qinfo_n[f], d_qinfo_n[f][1] );
+ d_qinfo[f].initialize( qcf, d_qinfo_n[f], d_qinfo_n[f][1] );
}
}
}
void TermArgTrie::debugPrint( const char * c, Node n, unsigned depth ) {
for( std::map< TNode, TermArgTrie >::iterator it = d_data.begin(); it != d_data.end(); ++it ){
- for( unsigned i=0; i<depth; i++ ){ Debug(c) << " "; }
- Debug(c) << it->first << std::endl;
+ for( unsigned i=0; i<depth; i++ ){ Trace(c) << " "; }
+ Trace(c) << it->first << std::endl;
it->second.debugPrint( c, n, depth+1 );
}
}
return d_op_map[f][i];
}
+unsigned TermDb::getNumTypeGroundTerms( TypeNode tn ) {
+ std::map< TypeNode, std::vector< Node > >::iterator it = d_type_map.find( tn );
+ if( it!=d_type_map.end() ){
+ return it->second.size();
+ }else{
+ return 0;
+ }
+}
+
+Node TermDb::getTypeGroundTerm( TypeNode tn, unsigned i ) {
+ Assert( i<d_type_map[tn].size() );
+ return d_type_map[tn][i];
+}
+
Node TermDb::getMatchOperator( Node n ) {
//return n.getOperator();
Kind k = n.getKind();
}
}
+bool TermDb::inRelevantDomain( TNode f, unsigned i, TNode r ) {
+ Assert( d_quantEngine->getTheoryEngine()->getMasterEqualityEngine()->getRepresentative( r )==r );
+ std::map< Node, std::map< unsigned, std::vector< Node > > >::iterator it = d_func_map_rel_dom.find( f );
+ if( it != d_func_map_rel_dom.end() ){
+ std::map< unsigned, std::vector< Node > >::iterator it2 = it->second.find( i );
+ if( it2!=it->second.end() ){
+ return std::find( it2->second.begin(), it2->second.end(), r )!=it2->second.end();
+ }else{
+ return false;
+ }
+ }else{
+ return false;
+ }
+}
+
//return a term n' equivalent to n
// maximal subterms of n' are representatives in the equality engine qy
Node TermDb::evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQuery * qy ) {
d_arg_reps.clear();
d_func_map_trie.clear();
d_func_map_eqc_trie.clear();
+ d_func_map_rel_dom.clear();
d_consistent_ee = true;
eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
}
computeArgReps( n );
- if( Trace.isOn("term-db-debug") ){
- Trace("term-db-debug") << "Adding term " << n << " with arg reps : ";
- for( unsigned i=0; i<d_arg_reps[n].size(); i++ ){
- Trace("term-db-debug") << d_arg_reps[n][i] << " ";
- }
- Trace("term-db-debug") << std::endl;
- if( ee->hasTerm( n ) ){
- Trace("term-db-debug") << " and value : " << ee->getRepresentative( n ) << std::endl;
+ Trace("term-db-debug") << "Adding term " << n << " with arg reps : ";
+ for( unsigned i=0; i<d_arg_reps[n].size(); i++ ){
+ Trace("term-db-debug") << d_arg_reps[n][i] << " ";
+ if( std::find( d_func_map_rel_dom[it->first][i].begin(),
+ d_func_map_rel_dom[it->first][i].end(), d_arg_reps[n][i] ) == d_func_map_rel_dom[it->first][i].end() ){
+ d_func_map_rel_dom[it->first][i].push_back( d_arg_reps[n][i] );
}
}
+ Trace("term-db-debug") << std::endl;
+ if( ee->hasTerm( n ) ){
+ Trace("term-db-debug") << " and value : " << ee->getRepresentative( n ) << std::endl;
+ }
Node at = d_func_map_trie[ it->first ].addOrGetTerm( n, d_arg_reps[n] );
if( at!=n && ee->areEqual( at, n ) ){
NoMatchAttribute nma;
Trace("term-db-stats") << "TermDb: Reset" << std::endl;
Trace("term-db-stats") << "Non-Congruent/Congruent/Non-Relevant = ";
Trace("term-db-stats") << nonCongruentCount << " / " << congruentCount << " (" << alreadyCongruentCount << ") / " << nonRelevantCount << std::endl;
- if( Debug.isOn("term-db") ){
- Debug("term-db") << "functions : " << std::endl;
+ if( Trace.isOn("term-db-index") ){
+ Trace("term-db-index") << "functions : " << std::endl;
for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){
if( it->second.size()>0 ){
- Debug("term-db") << "- " << it->first << std::endl;
- d_func_map_trie[ it->first ].debugPrint("term-db", it->second[0]);
+ Trace("term-db-index") << "- " << it->first << std::endl;
+ d_func_map_trie[ it->first ].debugPrint("term-db-index", it->second[0]);
}
}
}
}
/** get number of instantiation constants for q */
-int TermDb::getNumInstantiationConstants( Node q ) const {
+unsigned TermDb::getNumInstantiationConstants( Node q ) const {
std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( q );
if( it!=d_inst_constants.end() ){
- return (int)it->second.size();
+ return it->second.size();
}else{
return 0;
}
}
class TermDbSygus;
+class QuantConflictFind;
+class RelevantDomain;
+class ConjectureGenerator;
+class TermGenerator;
+class TermGenEnv;
class TermDb : public QuantifiersUtil {
friend class ::CVC4::theory::QuantifiersEngine;
+ //TODO: eliminate most of these
friend class ::CVC4::theory::inst::Trigger;
friend class ::CVC4::theory::quantifiers::fmcheck::FullModelChecker;
+ friend class ::CVC4::theory::quantifiers::QuantConflictFind;
+ friend class ::CVC4::theory::quantifiers::RelevantDomain;
+ friend class ::CVC4::theory::quantifiers::ConjectureGenerator;
+ friend class ::CVC4::theory::quantifiers::TermGenEnv;
typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap;
private:
/** reference to the quantifiers engine */
std::map< Node, std::map< TypeNode, Node > > d_par_op_map;
/** whether master equality engine is UF-inconsistent */
bool d_consistent_ee;
- /** set has term */
- void setHasTerm( Node n );
- /** evaluate term */
- Node evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQuery * qy );
- TNode getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy );
- bool isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy );
public:
TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe );
~TermDb(){}
/** constants */
Node d_zero;
Node d_one;
-
+public:
+ /** presolve (called once per user check-sat) */
+ void presolve();
+ /** reset (calculate which terms are active) */
+ bool reset( Theory::Effort effort );
+ /** identify */
+ std::string identify() const { return "TermDb"; }
+private:
/** map from operators to ground terms for that operator */
std::map< Node, std::vector< Node > > d_op_map;
/** map from type nodes to terms of that type */
/** map from operators to trie */
std::map< Node, TermArgTrie > d_func_map_trie;
std::map< Node, TermArgTrie > d_func_map_eqc_trie;
+ /** mapping from operators to their representative relevant domains */
+ std::map< Node, std::map< unsigned, std::vector< Node > > > d_func_map_rel_dom;
/** has map */
std::map< Node, bool > d_has_map;
/** map from reps to a term in eqc in d_has_map */
- std::map< Node, Node > d_term_elig_eqc;
-
+ std::map< Node, Node > d_term_elig_eqc;
+ /** set has term */
+ void setHasTerm( Node n );
+ /** evaluate term */
+ Node evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQuery * qy );
+ TNode getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy );
+ bool isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy );
public:
/** ground terms for operator */
unsigned getNumGroundTerms( Node f );
/** get ground term for operator */
Node getGroundTerm( Node f, unsigned i );
+ /** get num type terms */
+ unsigned getNumTypeGroundTerms( TypeNode tn );
+ /** get type ground term */
+ Node getTypeGroundTerm( TypeNode tn, unsigned i );
/** add a term to the database */
void addTerm( Node n, std::set< Node >& added, bool withinQuant = false, bool withinInstClosure = false );
- /** presolve (called once per user check-sat) */
- void presolve();
- /** reset (calculate which terms are active) */
- bool reset( Theory::Effort effort );
- /** identify */
- std::string identify() const { return "TermDb"; }
/** get match operator */
Node getMatchOperator( Node n );
/** get term arg index */
void computeArgReps( TNode n );
/** compute uf eqc terms */
void computeUfEqcTerms( TNode f );
+ /** in relevant domain */
+ bool inRelevantDomain( TNode f, unsigned i, TNode r );
/** evaluate a term under a substitution. Return representative in EE if possible.
* subsRep is whether subs contains only representatives
*/
/** get the i^th instantiation constant of q */
Node getInstantiationConstant( Node q, int i ) const;
/** get number of instantiation constants for q */
- int getNumInstantiationConstants( Node q ) const;
+ unsigned getNumInstantiationConstants( Node q ) const;
/** get the ce body q[e/x] */
Node getInstConstantBody( Node q );
/** get counterexample literal (for cbqi) */
d_tr_trie = new inst::TriggerTrie;
d_curr_effort_level = QEFFORT_NONE;
d_conflict = false;
+ d_num_added_lemmas_round = 0;
d_hasAddedLemma = false;
//don't add true lemma
d_lemmas_produced_c[d_term_db->d_true] = true;
}
d_conflict = false;
+ d_num_added_lemmas_round = 0;
d_hasAddedLemma = false;
bool setIncomplete = false;
if( e==Theory::EFFORT_LAST_CALL ){
}
Trace("quant-engine-debug") << " Theory engine finished : " << !d_te->needCheck() << std::endl;
Trace("quant-engine-debug") << " Needs model effort : " << needsModelE << std::endl;
- Trace("quant-engine-debug") << "Resetting all modules..." << std::endl;
}
if( Trace.isOn("quant-engine-ee-pre") ){
Trace("quant-engine-ee-pre") << "Equality engine (pre-inference): " << std::endl;
}
//reset utilities
+ Trace("quant-engine-debug") << "Resetting all utilities..." << std::endl;
for( unsigned i=0; i<d_util.size(); i++ ){
Trace("quant-engine-debug2") << "Reset " << d_util[i]->identify().c_str() << "..." << std::endl;
if( !d_util[i]->reset( e ) ){
}
//reset the model
+ Trace("quant-engine-debug") << "Reset model..." << std::endl;
d_model->reset_round();
//reset the modules
+ Trace("quant-engine-debug") << "Resetting all modules..." << std::endl;
for( unsigned i=0; i<d_modules.size(); i++ ){
Trace("quant-engine-debug2") << "Reset " << d_modules[i]->identify().c_str() << std::endl;
d_modules[i]->reset_round( e );
d_lemmas_produced_c[ lem ] = true;
d_lemmas_waiting.push_back( lem );
Trace("inst-add-debug") << "Added lemma" << std::endl;
+ d_num_added_lemmas_round++;
return true;
}else{
Trace("inst-add-debug") << "Duplicate." << std::endl;
}else{
//do not need to rewrite, will be rewritten after sending
d_lemmas_waiting.push_back( lem );
+ d_num_added_lemmas_round++;
return true;
}
}
}
}
+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::addSplit( Node n, bool reqPhase, bool reqPhasePol ){
n = Rewriter::rewrite( n );
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;
- }
+void QuantifiersEngine::markRelevant( Node q ) {
+ d_model->markRelevant( q );
}
-
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
unsigned d_curr_effort_level;
/** are we in conflict */
bool d_conflict;
+ /** number of lemmas we actually added this round (for debugging) */
+ unsigned d_num_added_lemmas_round;
/** has added lemma this round */
bool d_hasAddedLemma;
private:
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 );
+ /** mark relevant quantified formula, this will indicate it should be checked before the others */
+ void markRelevant( Node q );
/** 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 number of waiting lemmas */
+ unsigned getNumLemmasAddedThisRound() { return d_num_added_lemmas_round; }
/** get needs check */
bool getInstWhenNeedsCheck( Theory::Effort e );
/** get user pat mode */
anti-sk-simp.smt2 \
pure_dt_cbqi.smt2 \
florian-case-ax.smt2 \
- double-pattern.smt2
+ double-pattern.smt2 \
+ qcf-rel-dom-opt.smt2
# regression can be solved with --finite-model-find --fmf-inst-engine
--- /dev/null
+(set-logic UFLIA)
+(set-info :status unsat)
+(declare-fun P (Int) Bool)
+
+(assert (P 0))
+(assert (P 1))
+(assert (P 2))
+(assert (P 3))
+(assert (P 4))
+(assert (P 5))
+(assert (P 6))
+(assert (P 7))
+(assert (P 8))
+(assert (P 9))
+
+(assert (P 10))
+(assert (P 11))
+(assert (P 12))
+(assert (P 13))
+(assert (P 14))
+(assert (P 15))
+(assert (P 16))
+(assert (P 17))
+(assert (P 18))
+(assert (P 19))
+
+(assert (P 20))
+(assert (P 21))
+(assert (P 22))
+(assert (P 23))
+(assert (P 24))
+(assert (P 25))
+(assert (P 26))
+(assert (P 27))
+(assert (P 28))
+(assert (P 29))
+
+(declare-fun Q (Int Int Int Int Int) Bool)
+(assert (forall ((x Int) (y Int) (z Int) (w Int) (q Int)) (or (not (P x)) (not (P y)) (not (P z)) (not (P w)) (not (P q)) (Q x y z w q))))
+
+(declare-fun R (Int) Bool)
+(assert (R 0))
+(assert (forall ((x Int)) (not (R x))))
+
+(check-sat)
projects / cvc5.git / commitdiff