// Debug( c ) << std::endl;
//}
}
-
+/*
void InstMatch::makeComplete( Node f, QuantifiersEngine* qe ){
for( size_t i=0; i<f[0].getNumChildren(); i++ ){
Node ic = qe->getTermDatabase()->getInstantiationConstant( f, i );
}
}
}
-
+*/
void InstMatch::makeRepresentative( QuantifiersEngine* qe ){
for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){
- d_map[ it->first ] = qe->getEqualityQuery()->getInternalRepresentative( it->second );
- if( options::cbqi() && it->second.hasAttribute(InstConstantAttribute()) ){
- d_map[ it->first ] = qe->getTermDatabase()->getFreeVariableForInstConstant( it->first );
+ if( qe->getEqualityQuery()->getEngine()->hasTerm( it->second ) ){
+ d_map[ it->first ] = qe->getEqualityQuery()->getEngine()->getRepresentative( it->second );
}
+ //if( options::cbqi() && it->second.hasAttribute(InstConstantAttribute()) ){
+ // d_map[ it->first ] = qe->getTermDatabase()->getFreeVariableForInstConstant( it->first );
+ //}
}
}
/** is complete? */
bool isComplete( Node f ) { return d_map.size()==f[0].getNumChildren(); }
/** make complete */
- void makeComplete( Node f, QuantifiersEngine* qe );
+ //void makeComplete( Node f, QuantifiersEngine* qe );
/** make internal: ensure that no term in d_map contains instantiation constants */
- void makeInternal( QuantifiersEngine* qe );
+ //void makeInternal( QuantifiersEngine* qe );
/** make representative */
void makeRepresentative( QuantifiersEngine* qe );
/** get value */
//std::cout << "var.getType() " << var.getType() << "n.getType() " << n.getType() << std::endl ;
Assert( !var.isNull() );
Assert( n.isNull() ||// For a strange use in inst_match.cpp InstMatchGeneratorSimple::addInstantiations
- var.getType() == n.getType() );
+ //var.getType() == n.getType()
+ n.getType().isSubtypeOf( var.getType() ) );
d_map[var] = n;
}
size_t size(){ return d_map.size(); }
using namespace CVC4::theory::quantifiers;
InstantiationEngine::InstantiationEngine( QuantifiersEngine* qe, bool setIncomplete ) :
-QuantifiersModule( qe ), d_setIncomplete( setIncomplete ), d_ierCounter( 0 ){
+QuantifiersModule( qe ), d_setIncomplete( setIncomplete ), d_ierCounter( 0 ), d_performCheck( false ){
}
Debug("inst-engine-ctrl") << "IE: Instantiation Round." << std::endl;
//reset the quantifiers engine
Debug("inst-engine-ctrl") << "Reset IE" << std::endl;
- d_quantEngine->resetInstantiationRound( effort );
+ //reset the instantiators
+ for( theory::TheoryId i=theory::THEORY_FIRST; i<theory::THEORY_LAST; ++i ){
+ if( d_quantEngine->getInstantiator( i ) ){
+ d_quantEngine->getInstantiator( i )->resetInstantiationRound( effort );
+ }
+ }
//iterate over an internal effort level e
int e = 0;
int eLimit = effort==Theory::EFFORT_LAST_CALL ? 10 : 2;
}
}
-void InstantiationEngine::check( Theory::Effort e ){
+bool InstantiationEngine::needsCheck( Theory::Effort e ){
if( e==Theory::EFFORT_FULL ){
d_ierCounter++;
}
//determine if we should perform check, based on instWhenMode
- bool performCheck = false;
+ d_performCheck = false;
if( options::instWhenMode()==INST_WHEN_FULL ){
- performCheck = ( e >= Theory::EFFORT_FULL );
+ d_performCheck = ( e >= Theory::EFFORT_FULL );
}else if( options::instWhenMode()==INST_WHEN_FULL_LAST_CALL ){
- performCheck = ( ( e==Theory::EFFORT_FULL && d_ierCounter%2==0 ) || e==Theory::EFFORT_LAST_CALL );
+ d_performCheck = ( ( e==Theory::EFFORT_FULL && d_ierCounter%2==0 ) || e==Theory::EFFORT_LAST_CALL );
}else if( options::instWhenMode()==INST_WHEN_LAST_CALL ){
- performCheck = ( e >= Theory::EFFORT_LAST_CALL );
+ d_performCheck = ( e >= Theory::EFFORT_LAST_CALL );
}else{
- performCheck = true;
+ d_performCheck = true;
}
- if( performCheck ){
+ return d_performCheck;
+}
+
+void InstantiationEngine::check( Theory::Effort e ){
+ if( d_performCheck ){
Debug("inst-engine") << "IE: Check " << e << " " << d_ierCounter << std::endl;
double clSet = 0;
if( Trace.isOn("inst-engine") ){
bool d_setIncomplete;
/** inst round counter */
int d_ierCounter;
+ bool d_performCheck;
/** whether each quantifier is active */
std::map< Node, bool > d_quant_active;
/** whether we have added cbqi lemma */
InstantiationEngine( QuantifiersEngine* qe, bool setIncomplete = true );
~InstantiationEngine(){}
+ bool needsCheck( Theory::Effort e );
void check( Theory::Effort e );
void registerQuantifier( Node f );
void assertNode( Node f );
using namespace CVC4::theory;
using namespace CVC4::theory::quantifiers;
-bool TermArgBasisTrie::addTerm2( QuantifiersEngine* qe, Node n, int argIndex ){
+bool TermArgBasisTrie::addTerm2( FirstOrderModel* fm, Node n, int argIndex ){
if( argIndex<(int)n.getNumChildren() ){
Node r;
if( n[ argIndex ].getAttribute(ModelBasisAttribute()) ){
r = n[ argIndex ];
}else{
- r = qe->getEqualityQuery()->getRepresentative( n[ argIndex ] );
+ r = fm->getRepresentative( n[ argIndex ] );
}
std::map< Node, TermArgBasisTrie >::iterator it = d_data.find( r );
if( it==d_data.end() ){
- d_data[r].addTerm2( qe, n, argIndex+1 );
+ d_data[r].addTerm2( fm, n, argIndex+1 );
return true;
}else{
- return it->second.addTerm2( qe, n, argIndex+1 );
+ return it->second.addTerm2( fm, n, argIndex+1 );
}
}else{
return false;
}
}
}
+ //END FOR DEBUGGING
}else{
d_curr_model = fm;
d_addedLemmas = 0;
if( optOneQuantPerRoundInstGen() && addedLemmas>0 ){
break;
}
+ }else if( d_quant_sat.find( f )!=d_quant_sat.end() ){
+ d_numQuantSat++;
}
}
Trace("model-engine-debug") << "Quantifiers sat/ig/n-ig/null " << d_numQuantSat << " / " << d_numQuantInstGen << " / ";
if( !n.getAttribute(NoMatchAttribute()) || n.getAttribute(ModelBasisArgAttribute())==1 ){
if( !n.getAttribute(BasisNoMatchAttribute()) ){
//need to consider if it is not congruent modulo model basis
- if( !tabt.addTerm( d_qe, n ) ){
+ if( !tabt.addTerm( fm, n ) ){
BasisNoMatchAttribute bnma;
n.setAttribute(bnma,true);
}
}
bool ModelEngineBuilder::optExhInstNonInstGenQuant(){
- return true;
+ return options::fmfNewInstGen();
}
void ModelEngineBuilder::setEffort( int effort ){
namespace CVC4 {
namespace theory {
+namespace quantifiers {
/** Attribute true for nodes that should not be used when considered for inst-gen basis */
struct BasisNoMatchAttributeId {};
class TermArgBasisTrie {
private:
- bool addTerm2( QuantifiersEngine* qe, Node n, int argIndex );
+ bool addTerm2( FirstOrderModel* fm, Node n, int argIndex );
public:
/** the data */
std::map< Node, TermArgBasisTrie > d_data;
public:
- bool addTerm( QuantifiersEngine* qe, Node n ) { return addTerm2( qe, n, 0 ); }
+ bool addTerm( FirstOrderModel* fm, Node n ) { return addTerm2( fm, n, 0 ); }
};/* class TermArgBasisTrie */
-
-namespace quantifiers {
-
/** model builder class
* This class is capable of building candidate models based on the current quantified formulas
* that are asserted. Use:
FirstOrderModel* fm = d_quantEngine->getModel();
//the following will attempt to build a model and test that it satisfies all asserted universal quantifiers
int addedLemmas = 0;
- Trace("model-engine") << "---Model Engine Round---" << std::endl;
+ //quantifiers are initialized, we begin an instantiation round
+ double clSet = 0;
+ if( Trace.isOn("model-engine") ){
+ clSet = double(clock())/double(CLOCKS_PER_SEC);
+ }
+ ++(d_statistics.d_inst_rounds);
//two effort levels: first try exhaustive instantiation without axioms, then with.
int startEffort = ( !fm->isAxiomAsserted() || options::axiomInstMode()==AXIOM_INST_MODE_DEFAULT ) ? 1 : 0;
for( int effort=startEffort; effort<2; effort++ ){
// for effort = 0, we only instantiate non-axioms
// for effort = 1, we instantiate everything
if( addedLemmas==0 ){
- //quantifiers are initialized, we begin an instantiation round
- double clSet = 0;
- if( Trace.isOn("model-engine") ){
- clSet = double(clock())/double(CLOCKS_PER_SEC);
- }
- ++(d_statistics.d_inst_rounds);
- //reset the quantifiers engine
- d_quantEngine->resetInstantiationRound( e );
+ Trace("model-engine") << "---Model Engine Round---" << std::endl;
//initialize the model
Trace("model-engine-debug") << "Build model..." << std::endl;
d_builder->setEffort( effort );
//check quantifiers that inst-gen didn't apply to
addedLemmas += checkModel( check_model_no_inst_gen );
}
- if( Trace.isOn("model-engine") ){
- double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
- Trace("model-engine") << "Finished model engine, time = " << (clSet2-clSet) << std::endl;
- }
}
if( addedLemmas==0 ){
//if we have not added lemmas yet and axiomInstMode=trust, then we are done
}
}
}
+ if( Trace.isOn("model-engine") ){
+ double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
+ Trace("model-engine") << "Finished model engine, time = " << (clSet2-clSet) << std::endl;
+ }
if( addedLemmas==0 ){
Trace("model-engine-debug") << "No lemmas added, incomplete = " << d_incomplete_check << std::endl;
//CVC4 will answer SAT or unknown
#endif
}
+bool containsNN( Node n, Node nc ){
+ if( n==nc ){
+ return true;
+ }else{
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ if( containsNN( n[i], nc ) ){
+ return true;
+ }
+ }
+ return false;
+ }
+}
+
int ModelEngine::checkModel( int checkOption ){
int addedLemmas = 0;
FirstOrderModel* fm = d_quantEngine->getModel();
Trace("model-engine-debug") << it->second[i] << " ";
}
Trace("model-engine-debug") << std::endl;
+ for( size_t i=0; i<it->second.size(); i++ ){
+ std::vector< Node > eqc;
+ d_quantEngine->getEqualityQuery()->getEquivalenceClass( it->second[i], eqc );
+ Trace("model-engine-debug-eqc") << " " << it->second[i] << " : { ";
+ for( size_t j=0; j<eqc.size(); j++ ){
+ if( it->second[i]!=eqc[j] && containsNN( it->second[i], eqc[j] ) ){
+ Trace("model-engine-debug-eqc") << eqc[j] << " ";
+ }
+ }
+ Trace("model-engine-debug-eqc") << "}" << std::endl;
+ }
}
}
}
option userPatternsQuant /--ignore-user-patterns bool :default true
ignore user-provided patterns for quantifier instantiation
-option flipDecision --enable-flip-decision/ bool :default false
+option flipDecision --flip-decision/ bool :default false
turns on flip decision heuristic
+option internalReps --disable-quant-internal-reps/ bool :default true
+ disables instantiating with representatives chosen by quantifiers engine
+
option finiteModelFind --finite-model-find bool :default false
use finite model finding heuristic for quantifier instantiation
public:\r
EqualityQuery(){}\r
virtual ~EqualityQuery(){};\r
+ /** reset */\r
+ virtual void reset() = 0;\r
/** contains term */\r
virtual bool hasTerm( Node a ) = 0;\r
/** get the representative of the equivalence class of a */\r
virtual bool areEqual( Node a, Node b ) = 0;\r
/** returns true is a and b are disequal in the current context */\r
virtual bool areDisequal( Node a, Node b ) = 0;\r
- /** getInternalRepresentative gets the current best representative in the equivalence class of a, based on some criteria.\r
- If cbqi is active, this will return a term in the equivalence class of "a" that does\r
- not contain instantiation constants, if such a term exists.\r
- */\r
- virtual Node getInternalRepresentative( Node a ) = 0;\r
/** get the equality engine associated with this query */\r
virtual eq::EqualityEngine* getEngine() = 0;\r
/** get the equivalence class of a */\r
computeModelBasisArgAttribute( n );
if( !n.getAttribute(NoMatchAttribute()) ){
if( !d_func_map_trie[ it->first ].addTerm( d_quantEngine, n ) ){
- //only set no match if not a model basis argument term
NoMatchAttribute nma;
n.setAttribute(nma,true);
congruentCount++;
if( !en.getAttribute(NoMatchAttribute()) ){
Node op = en.getOperator();
if( !d_pred_map_trie[i][op].addTerm( d_quantEngine, en ) ){
- //only set no match if not a model basis argument term
NoMatchAttribute nma;
en.setAttribute(nma,true);
congruentCount++;
delete d_eq_query;
}
+EqualityQuery* QuantifiersEngine::getEqualityQuery() {
+ return d_eq_query;
+}
+
Instantiator* QuantifiersEngine::getInstantiator( theory::TheoryId id ){
return d_te->theoryOf( id )->getInstantiator();
}
void QuantifiersEngine::check( Theory::Effort e ){
CodeTimer codeTimer(d_time);
- if( e>=Theory::EFFORT_FULL ){
- Trace("quant-engine") << "Quantifiers Engine check, level = " << e << std::endl;
+ bool needsCheck = e>=Theory::EFFORT_LAST_CALL; //always need to check at or above last call
+ for( int i=0; i<(int)d_modules.size(); i++ ){
+ if( d_modules[i]->needsCheck( e ) ){
+ needsCheck = true;
+ }
}
-
- d_hasAddedLemma = false;
- if( e==Theory::EFFORT_LAST_CALL ){
- //if effort is last call, try to minimize model first
- if( options::finiteModelFind() ){
- //first, check if we can minimize the model further
- if( !((uf::TheoryUF*)getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->minimize() ){
- return;
+ if( needsCheck ){
+ Trace("quant-engine") << "Quantifiers Engine check, level = " << e << std::endl;
+ //reset relevant information
+ d_hasAddedLemma = false;
+ d_term_db->reset( e );
+ d_eq_query->reset();
+ if( e==Theory::EFFORT_LAST_CALL ){
+ //if effort is last call, try to minimize model first
+ if( options::finiteModelFind() ){
+ //first, check if we can minimize the model further
+ if( !((uf::TheoryUF*)getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->minimize() ){
+ return;
+ }
}
+ ++(d_statistics.d_instantiation_rounds_lc);
+ }else if( e==Theory::EFFORT_FULL ){
+ ++(d_statistics.d_instantiation_rounds);
}
- ++(d_statistics.d_instantiation_rounds_lc);
- }else if( e==Theory::EFFORT_FULL ){
- ++(d_statistics.d_instantiation_rounds);
- }
- for( int i=0; i<(int)d_modules.size(); i++ ){
- d_modules[i]->check( e );
- }
- //build the model if not done so already
- // this happens if no quantifiers are currently asserted and no model-building module is enabled
- if( options::produceModels() && e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma && !d_model->isModelSet() ){
- d_te->getModelBuilder()->buildModel( d_model, true );
- }
- if( e>=Theory::EFFORT_FULL ){
+ for( int i=0; i<(int)d_modules.size(); i++ ){
+ d_modules[i]->check( e );
+ }
+ //build the model if not done so already
+ // this happens if no quantifiers are currently asserted and no model-building module is enabled
+ if( options::produceModels() && e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma && !d_model->isModelSet() ){
+ d_te->getModelBuilder()->buildModel( d_model, true );
+ }
+
Trace("quant-engine") << "Finished quantifiers engine check." << std::endl;
}
}
return Node::null();
}
-void QuantifiersEngine::resetInstantiationRound( Theory::Effort level ){
- for( theory::TheoryId i=theory::THEORY_FIRST; i<theory::THEORY_LAST; ++i ){
- if( getInstantiator( i ) ){
- getInstantiator( i )->resetInstantiationRound( level );
- }
- }
- getTermDatabase()->reset( level );
-}
-
void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant ){
std::set< Node > added;
getTermDatabase()->addTerm( n, added, withinQuant );
}
bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool modEq, bool modInst, bool mkRep ){
+ Trace("inst-add") << "Add instantiation: " << m << std::endl;
//make sure there are values for each variable we are instantiating
- m.makeComplete( f, this );
- //make it representative, this is helpful for recognizing duplication
- if( mkRep ){
- m.makeRepresentative( this );
+ for( size_t i=0; i<f[0].getNumChildren(); i++ ){
+ Node ic = d_term_db->getInstantiationConstant( f, i );
+ Node val = m.getValue( ic );
+ if( val.isNull() ){
+ val = d_term_db->getFreeVariableForInstConstant( ic );
+ Trace("inst-add-debug") << "mkComplete " << val << std::endl;
+ m.set( ic, val );
+ }
+ //make it representative, this is helpful for recognizing duplication
+ if( mkRep ){
+ //pick the best possible representative for instantiation, based on past use and simplicity of term
+ Node r = d_eq_query->getInternalRepresentative( val );
+ Trace("inst-add-debug") << "mkRep " << r << " " << val << std::endl;
+ m.set( ic, r );
+ }
}
- Trace("inst-add") << "Add instantiation: " << m << std::endl;
//check for duplication modulo equality
if( !d_inst_match_trie[f].addInstMatch( this, f, m, modEq, modInst ) ){
Trace("inst-add") << " -> Already exists." << std::endl;
StatisticsRegistry::unregisterStat(&d_multi_candidates_cache_miss);
}
+void EqualityQueryQuantifiersEngine::reset(){
+ d_int_rep.clear();
+ d_reset_count++;
+}
bool EqualityQueryQuantifiersEngine::hasTerm( Node a ){
eq::EqualityEngine* ee = d_qe->getTheoryEngine()->getSharedTermsDatabase()->getEqualityEngine();
}
Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a ){
- //for( theory::TheoryId i=theory::THEORY_FIRST; i<theory::THEORY_LAST; ++i ){
- // if( d_qe->getInstantiator( i ) ){
- // if( d_qe->getInstantiator( i )->hasTerm( a ) ){
- // return d_qe->getInstantiator( i )->getInternalRepresentative( a );
- // }
- // }
- //}
- //return a;
- return d_qe->getInstantiator( THEORY_UF )->getInternalRepresentative( a );
+ if( !options::internalReps() ){
+ return d_qe->getInstantiator( THEORY_UF )->getRepresentative( a );
+ }else{
+ Node r = d_qe->getInstantiator( THEORY_UF )->getRepresentative( a );
+ if( d_int_rep.find( r )==d_int_rep.end() ){
+ std::vector< Node > eqc;
+ getEquivalenceClass( r, eqc );
+ //find best selection for representative
+ Node r_best = r;
+ int r_best_score = getRepScore( r );
+ for( size_t i=0; i<eqc.size(); i++ ){
+ int score = getRepScore( eqc[i] );
+ //score prefers earliest use of this term as a representative
+ if( score>=0 && ( r_best_score<0 || score<r_best_score ) ){
+ r_best = eqc[i];
+ r_best_score = score;
+ }
+ }
+ //now, make sure that no other member of the class is an instance
+ r_best = getInstance( r_best, eqc );
+ //store that this representative was chosen at this point
+ if( d_rep_score.find( r_best )==d_rep_score.end() ){
+ d_rep_score[ r_best ] = d_reset_count;
+ }
+ d_int_rep[r] = r_best;
+ if( r_best!=a ){
+ Trace("internal-rep-debug") << "rep( " << a << " ) = " << r << ", " << std::endl;
+ Trace("internal-rep-debug") << "int_rep( " << a << " ) = " << r_best << ", " << std::endl;
+ }
+ return r_best;
+ }else{
+ return d_int_rep[r];
+ }
+ }
}
eq::EqualityEngine* EqualityQueryQuantifiersEngine::getEngine(){
if( eqc.empty() ){
eqc.push_back( a );
}
+ //a should be in its equivalence class
+ Assert( std::find( eqc.begin(), eqc.end(), a )!=eqc.end() );
+}
+
+//helper functions
+
+Node EqualityQueryQuantifiersEngine::getInstance( Node n, std::vector< Node >& eqc ){
+ for( size_t i=0; i<n.getNumChildren(); i++ ){
+ Node nn = getInstance( n[i], eqc );
+ if( !nn.isNull() ){
+ return nn;
+ }
+ }
+ if( std::find( eqc.begin(), eqc.end(), n )!=eqc.end() ){
+ return n;
+ }else{
+ return Node::null();
+ }
+}
+
+int EqualityQueryQuantifiersEngine::getRepScore( Node n ){
+ return d_rep_score.find( n )==d_rep_score.end() ? -1 : d_rep_score[n];
}
virtual ~QuantifiersModule(){}
//get quantifiers engine
QuantifiersEngine* getQuantifiersEngine() { return d_quantEngine; }
- /* Call during check registerQuantifier has already been called */
+ /* whether this module needs to check this round */
+ virtual bool needsCheck( Theory::Effort e ) { return e>=Theory::EFFORT_LAST_CALL; }
+ /* Call during quantifier engine's check */
virtual void check( Theory::Effort e ) = 0;
/* Called for new quantifiers */
virtual void registerQuantifier( Node n ) = 0;
}/* CVC4::theory::inst */
class EfficientEMatcher;
+class EqualityQueryQuantifiersEngine;
class QuantifiersEngine {
friend class quantifiers::InstantiationEngine;
/** model engine */
quantifiers::ModelEngine* d_model_engine;
/** equality query class */
- EqualityQuery* d_eq_query;
+ EqualityQueryQuantifiersEngine* d_eq_query;
/** for computing relevance of quantifiers */
QuantRelevance d_quant_rel;
/** phase requirements for each quantifier for each instantiation literal */
TheoryEngine* getTheoryEngine() { return d_te; }
/** get equality query object for the given type. The default is the
generic one */
- EqualityQuery* getEqualityQuery() { return d_eq_query; }
+ EqualityQuery* getEqualityQuery();
/** get instantiation engine */
quantifiers::InstantiationEngine* getInstantiationEngine() { return d_inst_engine; }
/** get model engine */
void propagate( Theory::Effort level );
/** get next decision request */
Node getNextDecisionRequest();
- /** reset instantiation round */
- void resetInstantiationRound( Theory::Effort level );
private:
/** compute term vector */
void computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms );
private:
/** pointer to theory engine */
QuantifiersEngine* d_qe;
+ /** internal representatives */
+ std::map< Node, Node > d_int_rep;
+ /** rep score */
+ std::map< Node, int > d_rep_score;
+ /** reset count */
+ int d_reset_count;
+private:
+ /** node contains */
+ Node getInstance( Node n, std::vector< Node >& eqc );
+ /** get score */
+ int getRepScore( Node n );
public:
- EqualityQueryQuantifiersEngine( QuantifiersEngine* qe ) : d_qe( qe ){}
+ EqualityQueryQuantifiersEngine( QuantifiersEngine* qe ) : d_qe( qe ), d_reset_count( 0 ){}
~EqualityQueryQuantifiersEngine(){}
+ /** reset */
+ void reset();
/** general queries about equality */
bool hasTerm( Node a );
Node getRepresentative( Node a );
bool areEqual( Node a, Node b );
bool areDisequal( Node a, Node b );
- Node getInternalRepresentative( Node a );
eq::EqualityEngine* getEngine();
void getEquivalenceClass( Node a, std::vector< Node >& eqc );
+ /** getInternalRepresentative gets the current best representative in the equivalence class of a, based on some criteria.
+ If cbqi is active, this will return a term in the equivalence class of "a" that does
+ not contain instantiation constants, if such a term exists.
+ */
+ Node getInternalRepresentative( Node a );
}; /* EqualityQueryQuantifiersEngine */
}/* CVC4::theory namespace */
/**
* This is a utility function for constructing a copy of the currently shared terms
- * in a queriable form. As this is
+ * in a queriable form. As this is
*/
std::hash_set<TNode, TNodeHashFunction> currentlySharedTerms() const;
};/* class Theory */
virtual bool areEqual( Node a, Node b ) { return false; }
virtual bool areDisequal( Node a, Node b ) { return false; }
virtual Node getRepresentative( Node a ) { return a; }
- virtual Node getInternalRepresentative( Node a ) { return getRepresentative( a ); }
virtual eq::EqualityEngine* getEqualityEngine() { return NULL; }
virtual void getEquivalenceClass( Node a, std::vector< Node >& eqc ) {}
public:
}
};
-
-void InstStrategyCheckCESolved::processResetInstantiationRound( Theory::Effort effort ){
- for( std::map< Node, bool >::iterator it = d_solved.begin(); it != d_solved.end(); ++it ){
- calcSolved( it->first );
- }
-}
-
-int InstStrategyCheckCESolved::process( Node f, Theory::Effort effort, int e ){
- if( e==0 ){
- //calc solved if not done so already
- if( d_solved.find( f )==d_solved.end() ){
- calcSolved( f );
- }
- //check if f is counterexample-solved
- Debug("quant-uf-strategy") << "Try CE-solved.." << std::endl;
- if( d_solved[ f ] ){
- if( d_quantEngine->addInstantiation( f, d_th->d_baseMatch[f] ) ){
- ++(d_th->d_statistics.d_instantiations_ce_solved);
- //d_quantEngine->d_hasInstantiated[f] = true;
- }
- d_solved[f] = false;
- }
- Debug("quant-uf-strategy") << "done." << std::endl;
- }
- return STATUS_UNKNOWN;
-}
-
-void InstStrategyCheckCESolved::calcSolved( Node f ){
- d_th->d_baseMatch[f].clear();
- d_solved[ f ]= true;
- //check if instantiation constants are solved for
- for( int j = 0; j<d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); j++ ){
- Node i = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, j );
- Node rep = d_th->getInternalRepresentative( i );
- if( !rep.hasAttribute(InstConstantAttribute()) ){
- d_th->d_baseMatch[f].set(i,rep);
- }else{
- d_solved[ f ] = false;
- }
- }
-}
-
void InstStrategyUserPatterns::processResetInstantiationRound( Theory::Effort effort ){
//reset triggers
for( std::map< Node, std::vector< Trigger* > >::iterator it = d_user_gen.begin(); it != d_user_gen.end(); ++it ){
//instantiation strategies
-class InstStrategyCheckCESolved : public InstStrategy{
-private:
- /** InstantiatorTheoryUf class */
- InstantiatorTheoryUf* d_th;
- /** is solved? */
- std::map< Node, bool > d_solved;
- /** calc if f is solved */
- void calcSolved( Node f );
- /** process functions */
- void processResetInstantiationRound( Theory::Effort effort );
- int process( Node f, Theory::Effort effort, int e );
-public:
- InstStrategyCheckCESolved( InstantiatorTheoryUf* th, QuantifiersEngine* ie ) :
- InstStrategy( ie ), d_th( th ){}
- ~InstStrategyCheckCESolved(){}
- /** identify */
- std::string identify() const { return std::string("CheckCESolved"); }
-};/* class InstStrategyCheckCESolved */
-
class InstStrategyUserPatterns : public InstStrategy{
private:
/** InstantiatorTheoryUf class */
Instantiator( c, qe, th )
{
if( !options::finiteModelFind() || options::fmfInstEngine() ){
- if( options::cbqi() ){
- addInstStrategy( new InstStrategyCheckCESolved( this, qe ) );
- }
+ //if( options::cbqi() ){
+ // addInstStrategy( new InstStrategyCheckCESolved( this, qe ) );
+ //}
if( options::userPatternsQuant() ){
d_isup = new InstStrategyUserPatterns( this, qe );
addInstStrategy( d_isup );
void InstantiatorTheoryUf::processResetInstantiationRound( Theory::Effort effort ){
- d_ground_reps.clear();
+ //d_ground_reps.clear();
}
int InstantiatorTheoryUf::process( Node f, Theory::Effort effort, int e ){
return a;
}
}
-
+/*
Node InstantiatorTheoryUf::getInternalRepresentative( Node a ){
if( d_ground_reps.find( a )==d_ground_reps.end() ){
if( !hasTerm( a ) ){
}
return d_ground_reps[a];
}
-
+*/
eq::EqualityEngine* InstantiatorTheoryUf::getEqualityEngine(){
return &((TheoryUF*)d_th)->d_equalityEngine;
}
typedef context::CDChunkList<Node> NodeList;
typedef context::CDHashMap<Node, NodeList*, NodeHashFunction> NodeLists;
/** map to representatives used */
- std::map< Node, Node > d_ground_reps;
+ //std::map< Node, Node > d_ground_reps;
protected:
/** instantiation strategies */
InstStrategyUserPatterns* d_isup;
Node getRepresentative( Node a ) { return d_ith->getRepresentative( a ); }
bool areEqual( Node a, Node b ) { return d_ith->areEqual( a, b ); }
bool areDisequal( Node a, Node b ) { return d_ith->areDisequal( a, b ); }
- Node getInternalRepresentative( Node a ) { return d_ith->getInternalRepresentative( a ); }
eq::EqualityEngine* getEngine() { return d_ith->getEqualityEngine(); }
void getEquivalenceClass( Node a, std::vector< Node >& eqc ) { d_ith->getEquivalenceClass( a, eqc ); }
}; /* EqualityQueryInstantiatorTheoryUf */
//must generate new cardinality lemma term
std::stringstream ss;
ss << "_c_" << d_aloc_cardinality;
- Node var = NodeManager::currentNM()->mkSkolem( ss.str(), d_type, "is a cardinality lemma term" );
+ Node var;
+ if( d_totality_terms[0].empty() ){
+ //get arbitrary ground term
+ var = d_cardinality_term;
+ }else{
+ var = NodeManager::currentNM()->mkSkolem( ss.str(), d_type, "is a cardinality lemma term" );
+ }
d_totality_terms[0].push_back( var );
Trace("mkVar") << "allocateCardinality, mkVar : " << var << " : " << d_type << std::endl;
//must be distinct from all other cardinality terms
projects / cvc5.git / commitdiff