void InstantiatorTheoryArith::assertNode( Node assertion ){
Debug("quant-arith-assert") << "InstantiatorTheoryArith::check: " << assertion << std::endl;
- d_quantEngine->addTermToDatabase( assertion );
+ //INST_ELIM_TRY//d_quantEngine->addTermToDatabase( assertion );
if( options::cbqi() ){
if( assertion.hasAttribute(InstConstantAttribute()) ){
setQuantifierActive( assertion.getAttribute(InstConstantAttribute()) );
void InstantiatorTheoryArrays::assertNode( Node assertion ){
Debug("quant-arrays-assert") << "InstantiatorTheoryArrays::assertNode: " << assertion << std::endl;
- d_quantEngine->addTermToDatabase( assertion );
+ //INST_ELIM_TRY//d_quantEngine->addTermToDatabase( assertion );
if( options::cbqi() ){
if( assertion.hasAttribute(InstConstantAttribute()) ){
setQuantifierActive( assertion.getAttribute(InstConstantAttribute()) );
void InstantiatorTheoryDatatypes::assertNode( Node assertion ){
Debug("quant-datatypes-assert") << "InstantiatorTheoryDatatypes::check: " << assertion << std::endl;
- d_quantEngine->addTermToDatabase( assertion );
+ //INST_ELIM_TRY//d_quantEngine->addTermToDatabase( assertion );
if( options::cbqi() ){
if( assertion.hasAttribute(InstConstantAttribute()) ){
setQuantifierActive( assertion.getAttribute(InstConstantAttribute()) );
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/options.h"
#include "theory/rewriterules/efficient_e_matching.h"
+#include "theory/quantifiers/theory_quantifiers.h"
using namespace std;
using namespace CVC4;
std::string identify() const { return std::string("TheoryQuantifiers"); }
bool flipDecision();
void setUserAttribute( std::string& attr, Node n );
+ eq::EqualityEngine* getMasterEqualityEngine() { return d_masterEqualityEngine; }
private:
void assertUniversal( Node n );
void assertExistential( Node n );
}else{
d_mg = new InstMatchGenerator( d_nodes, qe, matchOption );
}
- Debug("trigger") << "Trigger for " << f << ": " << std::endl;
+ Trace("trigger") << "Trigger for " << f << ": " << std::endl;
for( int i=0; i<(int)d_nodes.size(); i++ ){
- Debug("trigger") << " " << d_nodes[i] << std::endl;
+ Trace("trigger") << " " << d_nodes[i] << std::endl;
}
- Debug("trigger") << std::endl;
+ Trace("trigger") << std::endl;
if( d_nodes.size()==1 ){
if( isSimpleTrigger( d_nodes[0] ) ){
++(qe->d_statistics.d_triggers);
bool Trigger::isUsableTrigger( Node n, Node f ){
//return n.getAttribute(InstConstantAttribute())==f && n.getKind()==APPLY_UF;
- return n.getAttribute(InstConstantAttribute())==f && isAtomicTrigger( n ) && isUsable( n, f );
+ bool usable = n.getAttribute(InstConstantAttribute())==f && isAtomicTrigger( n ) && isUsable( n, f );
+ Trace("usable") << n << " usable : " << usable << std::endl;
+ return usable;
}
bool Trigger::isAtomicTrigger( Node n ){
}
bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool modEq, bool modInst, bool mkRep ){
- Trace("inst-add") << "Add instantiation: " << m << std::endl;
+ Trace("inst-add-debug") << "Add instantiation: " << m << std::endl;
//make sure there are values for each variable we are instantiating
for( size_t i=0; i<f[0].getNumChildren(); i++ ){
Node ic = d_term_db->getInstantiationConstant( f, i );
}
//check for duplication modulo equality
if( !d_inst_match_trie[f].addInstMatch( this, f, m, modEq, modInst ) ){
- Trace("inst-add") << " -> Already exists." << std::endl;
+ Trace("inst-add-debug") << " -> Already exists." << std::endl;
++(d_statistics.d_inst_duplicate);
return false;
}
bool addedInst = addInstantiation( f, d_term_db->d_vars[f], terms );
//report the result
if( addedInst ){
- Trace("inst-add") << " -> Success." << std::endl;
+ Trace("inst-add") << "Added instantiation for " << f << ": " << std::endl;
+ Trace("inst-add") << " " << m << std::endl;
+ Trace("inst-add-debug") << " -> Success." << std::endl;
return true;
}else{
- Trace("inst-add") << " -> Lemma already exists." << std::endl;
+ Trace("inst-add-debug") << " -> Lemma already exists." << std::endl;
return false;
}
}
StatisticsRegistry::unregisterStat(&d_multi_candidates_cache_miss);
}
+eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine(){
+ return ((quantifiers::TheoryQuantifiers*)getTheoryEngine()->theoryOf( THEORY_QUANTIFIERS ))->getMasterEqualityEngine();
+}
+
void EqualityQueryQuantifiersEngine::reset(){
d_int_rep.clear();
d_reset_count++;
}
bool EqualityQueryQuantifiersEngine::hasTerm( Node a ){
- eq::EqualityEngine* ee = d_qe->getTheoryEngine()->getSharedTermsDatabase()->getEqualityEngine();
- if( ee->hasTerm( a ) ){
- return true;
- }
- 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 true;
- }
- }
- }
- return false;
+ return getEngine()->hasTerm( a );
}
Node EqualityQueryQuantifiersEngine::getRepresentative( Node a ){
- eq::EqualityEngine* ee = d_qe->getTheoryEngine()->getSharedTermsDatabase()->getEqualityEngine();
+ eq::EqualityEngine* ee = getEngine();
if( ee->hasTerm( a ) ){
return ee->getRepresentative( 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 )->getRepresentative( a );
- }
- }
- }
return a;
}
if( a==b ){
return true;
}else{
- eq::EqualityEngine* ee = d_qe->getTheoryEngine()->getSharedTermsDatabase()->getEqualityEngine();
+ eq::EqualityEngine* ee = getEngine();
if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
if( ee->areEqual( a, b ) ){
return true;
}
}
- for( theory::TheoryId i=theory::THEORY_FIRST; i<theory::THEORY_LAST; ++i ){
- if( d_qe->getInstantiator( i ) ){
- if( d_qe->getInstantiator( i )->areEqual( a, b ) ){
- return true;
- }
- }
- }
- //std::cout << "Equal = " << eq_sh << " " << eq_uf << " " << eq_a << " " << eq_dt << std::endl;
return false;
}
}
bool EqualityQueryQuantifiersEngine::areDisequal( Node a, Node b ){
- eq::EqualityEngine* ee = d_qe->getTheoryEngine()->getSharedTermsDatabase()->getEqualityEngine();
+ eq::EqualityEngine* ee = getEngine();
if( ee->hasTerm( a ) && ee->hasTerm( b ) ){
if( ee->areDisequal( a, b, false ) ){
return true;
}
}
- for( theory::TheoryId i=theory::THEORY_FIRST; i<theory::THEORY_LAST; ++i ){
- if( d_qe->getInstantiator( i ) ){
- if( d_qe->getInstantiator( i )->areDisequal( a, b ) ){
- return true;
- }
- }
- }
return false;
- //std::cout << "Disequal = " << deq_sh << " " << deq_uf << " " << deq_a << " " << deq_dt << std::endl;
}
Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a ){
+ Node r = getRepresentative( a );
if( !options::internalReps() ){
- return d_qe->getInstantiator( THEORY_UF )->getRepresentative( a );
+ return r;
}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 );
}
eq::EqualityEngine* EqualityQueryQuantifiersEngine::getEngine(){
- return ((uf::TheoryUF*)d_qe->getTheoryEngine()->theoryOf( THEORY_UF ))->getEqualityEngine();
+ return d_qe->getMasterEqualityEngine();
}
void EqualityQueryQuantifiersEngine::getEquivalenceClass( Node a, std::vector< Node >& eqc ){
- eq::EqualityEngine* ee = d_qe->getTheoryEngine()->getSharedTermsDatabase()->getEqualityEngine();
+ eq::EqualityEngine* ee = getEngine();
if( ee->hasTerm( a ) ){
Node rep = ee->getRepresentative( a );
eq::EqClassIterator eqc_iter( rep, ee );
eqc.push_back( *eqc_iter );
eqc_iter++;
}
- }
- for( theory::TheoryId i=theory::THEORY_FIRST; i<theory::THEORY_LAST; ++i ){
- if( d_qe->getInstantiator( i ) ){
- d_qe->getInstantiator( i )->getEquivalenceClass( a, eqc );
- }
- }
- if( eqc.empty() ){
+ }else{
eqc.push_back( a );
}
//a should be in its equivalence class
rrinst::TriggerTrie* getRRTriggerDatabase() { return d_rr_tr_trie; }
/** add term to database */
void addTermToDatabase( Node n, bool withinQuant = false );
+ eq::EqualityEngine* getMasterEqualityEngine() ;
public:
/** statistics class */
class Statistics {
#include "theory/rewriterules/options.h"\r
#include "theory/quantifiers/term_database.h"\r
\r
+#include "theory/theory_engine.h"\r
+\r
using namespace std;\r
using namespace CVC4;\r
using namespace CVC4::kind;\r
\r
}\r
\r
+eq::EqualityEngine* EfficientEMatcher::getEqualityEngine(){\r
+ return ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getEqualityEngine();\r
+}\r
+\r
/** new node */\r
void EfficientEMatcher::newEqClass( TNode n ){\r
\r
return d_eqc_ops.find( n )==d_eqc_ops.end() ? NULL : d_eqc_ops[n];\r
}\r
EqClassInfo* EfficientEMatcher::getOrCreateEquivalenceClassInfo( Node n ){\r
- Assert( n==d_quantEngine->getEqualityQuery()->getEngine()->getRepresentative( n ) );\r
+ Assert( n==getEqualityEngine()->getRepresentative( n ) );\r
if( d_eqc_ops.find( n )==d_eqc_ops.end() ){\r
EqClassInfo* eci = new EqClassInfo( d_quantEngine->getSatContext() );\r
eci->setMember( n, d_quantEngine->getTermDatabase() );\r
itc != end; ++itc ) {\r
//The constant\r
Debug("efficient-e-match") << " Checking constant " << a << std::endl;\r
- if(d_quantEngine->getEqualityQuery()->getEngine()->getRepresentative(itc->first) != a) continue;\r
+ if(getEqualityEngine()->getRepresentative(itc->first) != a) continue;\r
SetNode s;\r
- eq::EqClassIterator eqc_iter( b, d_quantEngine->getEqualityQuery()->getEngine() );\r
+ eq::EqClassIterator eqc_iter( b, getEqualityEngine() );\r
while( !eqc_iter.isFinished() ){\r
Debug("efficient-e-match-debug") << "> look at " << (*eqc_iter)\r
<< std::endl;\r
bool EfficientEMatcher::collectParentsTermsIps( Node n, Node f, int arg, SetNode & terms, bool addRep, bool modEq ){ //modEq default true\r
bool addedTerm = false;\r
\r
- if( modEq && d_quantEngine->getEqualityQuery()->getEngine()->hasTerm( n )){\r
- Assert( d_quantEngine->getEqualityQuery()->getEngine()->getRepresentative( n )==n );\r
+ if( modEq && getEqualityEngine()->hasTerm( n )){\r
+ Assert( getEqualityEngine()->getRepresentative( n )==n );\r
//collect modulo equality\r
//DO_THIS: this should (if necessary) compute a current set of (f, arg) parents for n and cache it\r
- eq::EqClassIterator eqc_iter( n, d_quantEngine->getEqualityQuery()->getEngine() );\r
+ eq::EqClassIterator eqc_iter( n, getEqualityEngine() );\r
while( !eqc_iter.isFinished() ){\r
Debug("efficient-e-match-debug") << "> look at " << (*eqc_iter)\r
<< std::endl;\r
for( size_t i=0; i<parents.size(); ++i ){\r
TNode t = parents[i];\r
if(!CandidateGenerator::isLegalCandidate(t)) continue;\r
- if( addRep ) t = d_quantEngine->getEqualityQuery()->getEngine()->getRepresentative( t );\r
+ if( addRep ) t = getEqualityEngine()->getRepresentative( t );\r
terms.insert(t);\r
addedTerm = true;\r
}\r
} else if( pats[0].getKind() == kind::NOT && pats[0][0].getKind() == kind::EQUAL){\r
Node cst = NodeManager::currentNM()->mkConst<bool>(false);\r
TNode op = pats[0][0].getOperator();\r
- cst = d_quantEngine->getEqualityQuery()->getEngine()->getRepresentative(cst);\r
+ cst = getEqualityEngine()->getRepresentative(cst);\r
SetNode ele;\r
- eq::EqClassIterator eqc_iter( cst, d_quantEngine->getEqualityQuery()->getEngine() );\r
+ eq::EqClassIterator eqc_iter( cst, getEqualityEngine() );\r
while( !eqc_iter.isFinished() ){\r
Debug("efficient-e-match-debug") << "> look at " << (*eqc_iter)\r
<< std::endl;\r
}\r
\r
void EfficientEMatcher::outputEqClass( const char* c, Node n ){\r
- if( d_quantEngine->getEqualityQuery()->getEngine()->hasTerm( n ) ){\r
- eq::EqClassIterator eqc_iter( d_quantEngine->getEqualityQuery()->getEngine()->getRepresentative( n ),\r
- d_quantEngine->getEqualityQuery()->getEngine() );\r
+ if( getEqualityEngine()->hasTerm( n ) ){\r
+ eq::EqClassIterator eqc_iter( getEqualityEngine()->getRepresentative( n ),\r
+ getEqualityEngine() );\r
bool firstTime = true;\r
while( !eqc_iter.isFinished() ){\r
if( !firstTime ){ Debug(c) << ", "; }\r
#include "context/cdqueue.h"\r
#include "context/cdo.h"\r
\r
+#include "theory/uf/equality_engine.h"\r
+\r
namespace CVC4 {\r
namespace theory {\r
\r
delete(i->second.second);\r
}\r
}\r
+ /** get equality engine we are using */\r
+ eq::EqualityEngine* getEqualityEngine();\r
private:\r
//information for each equivalence class\r
std::map< Node, EqClassInfo* > d_eqc_ops;\r
typedef std::vector< std::pair< Node, int > > Ips;\r
typedef std::map< Node, std::vector< std::pair< Node, Ips > > > PpIpsMap;\r
typedef std::map< Node, std::vector< triple< size_t, Node, Ips > > > MultiPpIpsMap;\r
-\r
private:\r
/** Parent/Child Pairs (for efficient E-matching)\r
So, for example, if we have the pattern f( g( x ) ), then d_pc_pairs[g][f][f( g( x ) )] = { f.0 }.\r
#include "theory/uf/equality_engine.h"
+#include "theory/rewriterules/efficient_e_matching.h"
+
using namespace std;
using namespace CVC4;
void TheoryEngine::finishInit() {
if (d_logicInfo.isQuantified()) {
Assert(d_masterEqualityEngine == 0);
- d_masterEqualityEngine = new eq::EqualityEngine(getSatContext(), "theory::master");
+ d_masterEqualityEngine = new eq::EqualityEngine(d_masterEENotify,getSatContext(), "theory::master");
for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
if (d_theoryTable[theoryId]) {
}
}
+void TheoryEngine::eqNotifyNewClass(TNode t){
+ d_quantEngine->addTermToDatabase( t );
+}
+
+void TheoryEngine::eqNotifyPreMerge(TNode t1, TNode t2){
+ //TODO: add notification to efficient E-matching
+}
+
+void TheoryEngine::eqNotifyPostMerge(TNode t1, TNode t2){
+
+}
+
+void TheoryEngine::eqNotifyDisequal(TNode t1, TNode t2, TNode reason){
+
+}
+
+
TheoryEngine::TheoryEngine(context::Context* context,
context::UserContext* userContext,
RemoveITE& iteRemover,
d_logicInfo(logicInfo),
d_sharedTerms(this, context),
d_masterEqualityEngine(NULL),
+ d_masterEENotify(*this),
d_quantEngine(NULL),
d_curr_model(NULL),
d_curr_model_builder(NULL),
#include "util/cvc4_assert.h"
#include "theory/ite_simplifier.h"
#include "theory/unconstrained_simplifier.h"
+#include "theory/uf/equality_engine.h"
namespace CVC4 {
*/
theory::eq::EqualityEngine* d_masterEqualityEngine;
+ /** notify class for master equality engine */
+ class NotifyClass : public theory::eq::EqualityEngineNotify {
+ TheoryEngine& d_te;
+ public:
+ NotifyClass(TheoryEngine& te): d_te(te) {}
+ bool eqNotifyTriggerEquality(TNode equality, bool value) { return true; }
+ bool eqNotifyTriggerPredicate(TNode predicate, bool value) { return true; }
+ bool eqNotifyTriggerTermEquality(theory::TheoryId tag, TNode t1, TNode t2, bool value) { return true; }
+ void eqNotifyConstantTermMerge(TNode t1, TNode t2) {}
+ void eqNotifyNewClass(TNode t) { d_te.eqNotifyNewClass(t); }
+ void eqNotifyPreMerge(TNode t1, TNode t2) { d_te.eqNotifyPreMerge(t1, t2); }
+ void eqNotifyPostMerge(TNode t1, TNode t2) { d_te.eqNotifyPostMerge(t1, t2); }
+ void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { d_te.eqNotifyDisequal(t1, t2, reason); }
+ };/* class TheoryEngine::NotifyClass */
+ NotifyClass d_masterEENotify;
+
+ /**
+ * notification methods
+ */
+ void eqNotifyNewClass(TNode t);
+ void eqNotifyPreMerge(TNode t1, TNode t2);
+ void eqNotifyPostMerge(TNode t1, TNode t2);
+ void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
+
/**
* The quantifiers engine
*/
if( processTrigger ){
//if( d_user_gen[f][i]->isMultiTrigger() )
//Notice() << " Process (user) " << (*d_user_gen[f][i]) << " for " << f << "..." << std::endl;
- int numInst = d_user_gen[f][i]->addInstantiations( d_th->d_baseMatch[f] );
+ InstMatch baseMatch;
+ int numInst = d_user_gen[f][i]->addInstantiations( baseMatch );
//if( d_user_gen[f][i]->isMultiTrigger() )
//Notice() << " Done, numInst = " << numInst << "." << std::endl;
- d_th->d_statistics.d_instantiations_user_pattern += numInst;
+ //d_statistics.d_instantiations += numInst;
if( d_user_gen[f][i]->isMultiTrigger() ){
d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
}
options::smartTriggers() ) );
}
}
+/*
+InstStrategyUserPatterns::Statistics::Statistics():
+ d_instantiations("InstStrategyUserPatterns::Instantiations", 0)
+{
+ StatisticsRegistry::registerStat(&d_instantiations);
+}
+
+InstStrategyUserPatterns::Statistics::~Statistics(){
+ StatisticsRegistry::unregisterStat(&d_instantiations);
+}
+*/
void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort effort ){
//reset triggers
if( processTrigger ){
//if( tr->isMultiTrigger() )
Debug("quant-uf-strategy-auto-gen-triggers") << " Process " << (*tr) << "..." << std::endl;
- int numInst = tr->addInstantiations( d_th->d_baseMatch[f] );
+ InstMatch baseMatch;
+ int numInst = tr->addInstantiations( baseMatch );
//if( tr->isMultiTrigger() )
Debug("quant-uf-strategy-auto-gen-triggers") << " Done, numInst = " << numInst << "." << std::endl;
- if( d_tr_strategy==Trigger::TS_MIN_TRIGGER ){
- d_th->d_statistics.d_instantiations_auto_gen_min += numInst;
- }else{
- d_th->d_statistics.d_instantiations_auto_gen += numInst;
- }
+ //if( d_tr_strategy==Trigger::TS_MIN_TRIGGER ){
+ // d_statistics.d_instantiations_min += numInst;
+ //}else{
+ // d_statistics.d_instantiations += numInst;
+ //}
if( tr->isMultiTrigger() ){
d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
}
}
}
}
+/*
+InstStrategyAutoGenTriggers::Statistics::Statistics():
+ d_instantiations("InstStrategyAutoGenTriggers::Instantiations", 0),
+ d_instantiations_min("InstStrategyAutoGenTriggers::Instantiations_min", 0)
+{
+ StatisticsRegistry::registerStat(&d_instantiations);
+ StatisticsRegistry::registerStat(&d_instantiations_min);
+}
+
+InstStrategyAutoGenTriggers::Statistics::~Statistics(){
+ StatisticsRegistry::unregisterStat(&d_instantiations);
+ StatisticsRegistry::unregisterStat(&d_instantiations_min);
+}
+*/
void InstStrategyFreeVariable::processResetInstantiationRound( Theory::Effort effort ){
}
Debug("quant-uf-alg") << "Add guessed instantiation" << std::endl;
InstMatch m;
if( d_quantEngine->addInstantiation( f, m ) ){
- ++(d_th->d_statistics.d_instantiations_guess);
+ //++(d_statistics.d_instantiations);
//d_quantEngine->d_hasInstantiated[f] = true;
}
}
return STATUS_UNKNOWN;
}
}
+/*
+InstStrategyFreeVariable::Statistics::Statistics():
+ d_instantiations("InstStrategyGuess::Instantiations", 0)
+{
+ StatisticsRegistry::registerStat(&d_instantiations);
+}
+
+InstStrategyFreeVariable::Statistics::~Statistics(){
+ StatisticsRegistry::unregisterStat(&d_instantiations);
+}
+*/
\ No newline at end of file
inst::Trigger* getUserGenerator( Node f, int i ) { return d_user_gen[f][ i ]; }
/** identify */
std::string identify() const { return std::string("UserPatterns"); }
+public:
+ /** statistics class */
+ //class Statistics {
+ //public:
+ // IntStat d_instantiations;
+ // Statistics();
+ // ~Statistics();
+ //};
+ //Statistics d_statistics;
};/* class InstStrategyUserPatterns */
class InstStrategyAutoGenTriggers : public InstStrategy{
}
/** set generate additional */
void setGenerateAdditional( bool val ) { d_generate_additional = val; }
+public:
+ /** statistics class */
+ //class Statistics {
+ //public:
+ // IntStat d_instantiations;
+ // IntStat d_instantiations_min;
+ // Statistics();
+ // ~Statistics();
+ //};
+ //Statistics d_statistics;
};/* class InstStrategyAutoGenTriggers */
class InstStrategyFreeVariable : public InstStrategy{
~InstStrategyFreeVariable(){}
/** identify */
std::string identify() const { return std::string("FreeVariable"); }
+public:
+ /** statistics class */
+ //class Statistics {
+ //public:
+ // IntStat d_instantiations;
+ // Statistics();
+ // ~Statistics();
+ //};
+ //Statistics d_statistics;
};/* class InstStrategyFreeVariable */
}/* CVC4::theory::uf namespace */
#include "theory/uf/theory_uf_strong_solver.h"
#include "theory/model.h"
#include "theory/type_enumerator.h"
+//included since efficient e matching needs notifications from UF
+#include "theory/rewriterules/efficient_e_matching.h"
using namespace std;
using namespace CVC4;
}
// this can be called very early, during initialization
if (!getLogicInfo().isLocked() || getLogicInfo().isQuantified()) {
- ((InstantiatorTheoryUf*) getInstantiator())->newEqClass(t);
+ //getQuantifiersEngine()->addTermToDatabase( t );
}
}
void TheoryUF::eqNotifyPreMerge(TNode t1, TNode t2) {
if (getLogicInfo().isQuantified()) {
- ((InstantiatorTheoryUf*) getInstantiator())->merge(t1, t2);
+ getQuantifiersEngine()->getEfficientEMatcher()->merge( t1, t2 );
}
}
if (d_thss != NULL) {
d_thss->assertDisequal(t1, t2, reason);
}
- if (getLogicInfo().isQuantified()) {
- ((InstantiatorTheoryUf*) getInstantiator())->assertDisequal(t1, t2, reason);
- }
}
Node TheoryUF::ppRewrite(TNode node) {
//if( options::cbqi() ){
// addInstStrategy( new InstStrategyCheckCESolved( this, qe ) );
//}
+ //these are the instantiation strategies for basic E-matching
if( options::userPatternsQuant() ){
d_isup = new InstStrategyUserPatterns( this, qe );
addInstStrategy( d_isup );
{
Debug("quant-uf-assert") << "InstantiatorTheoryUf::check: " << assertion << std::endl;
//preRegisterTerm( assertion );
- d_quantEngine->addTermToDatabase( assertion );
+ //INST_ELIM_TRY//d_quantEngine->addTermToDatabase( assertion );
if( options::cbqi() ){
if( assertion.hasAttribute(InstConstantAttribute()) ){
setQuantifierActive( assertion.getAttribute(InstConstantAttribute()) );
}
}
-InstantiatorTheoryUf::Statistics::Statistics():
- //d_instantiations("InstantiatorTheoryUf::Total_Instantiations", 0),
- d_instantiations_ce_solved("InstantiatorTheoryUf::Instantiations_CE-Solved", 0),
- d_instantiations_e_induced("InstantiatorTheoryUf::Instantiations_E-Induced", 0),
- d_instantiations_user_pattern("InstantiatorTheoryUf::Instantiations_User_Pattern", 0),
- d_instantiations_guess("InstantiatorTheoryUf::Instantiations_Free_Var", 0),
- d_instantiations_auto_gen("InstantiatorTheoryUf::Instantiations_Auto_Gen", 0),
- d_instantiations_auto_gen_min("InstantiatorTheoryUf::Instantiations_Auto_Gen_Min", 0),
- d_splits("InstantiatorTheoryUf::Total_Splits", 0)
-{
- //StatisticsRegistry::registerStat(&d_instantiations);
- StatisticsRegistry::registerStat(&d_instantiations_ce_solved);
- StatisticsRegistry::registerStat(&d_instantiations_e_induced);
- StatisticsRegistry::registerStat(&d_instantiations_user_pattern );
- StatisticsRegistry::registerStat(&d_instantiations_guess );
- StatisticsRegistry::registerStat(&d_instantiations_auto_gen );
- StatisticsRegistry::registerStat(&d_instantiations_auto_gen_min );
- StatisticsRegistry::registerStat(&d_splits);
-}
-
-InstantiatorTheoryUf::Statistics::~Statistics(){
- //StatisticsRegistry::unregisterStat(&d_instantiations);
- StatisticsRegistry::unregisterStat(&d_instantiations_ce_solved);
- StatisticsRegistry::unregisterStat(&d_instantiations_e_induced);
- StatisticsRegistry::unregisterStat(&d_instantiations_user_pattern );
- StatisticsRegistry::unregisterStat(&d_instantiations_guess );
- StatisticsRegistry::unregisterStat(&d_instantiations_auto_gen );
- StatisticsRegistry::unregisterStat(&d_instantiations_auto_gen_min );
- StatisticsRegistry::unregisterStat(&d_splits);
-}
-
-/** new node */
-void InstantiatorTheoryUf::newEqClass( TNode n ){
- d_quantEngine->addTermToDatabase( n );
-}
-
-/** merge */
-void InstantiatorTheoryUf::merge( TNode a, TNode b ){
- d_quantEngine->getEfficientEMatcher()->merge( a, b );
-}
-
-/** assert terms are disequal */
-void InstantiatorTheoryUf::assertDisequal( TNode a, TNode b, TNode reason ){
-
-}
-
void InstantiatorTheoryUf::outputEqClass( const char* c, Node n ){
if( ((TheoryUF*)d_th)->d_equalityEngine.hasTerm( n ) ){
eq::EqClassIterator eqc_iter( getRepresentative( n ),
namespace uf {
class InstantiatorTheoryUf : public Instantiator{
- friend class ::CVC4::theory::inst::InstMatchGenerator;
- friend class ::CVC4::theory::quantifiers::TermDb;
-protected:
- typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap;
- typedef context::CDHashMap<Node, int, NodeHashFunction> IntMap;
- typedef context::CDChunkList<Node> NodeList;
- typedef context::CDHashMap<Node, NodeList*, NodeHashFunction> NodeLists;
- /** map to representatives used */
- //std::map< Node, Node > d_ground_reps;
protected:
/** instantiation strategies */
InstStrategyUserPatterns* d_isup;
void processResetInstantiationRound( Theory::Effort effort );
/** calculate matches for quantifier f at effort */
int process( Node f, Theory::Effort effort, int e );
-public:
- /** statistics class */
- class Statistics {
- public:
- //IntStat d_instantiations;
- IntStat d_instantiations_ce_solved;
- IntStat d_instantiations_e_induced;
- IntStat d_instantiations_user_pattern;
- IntStat d_instantiations_guess;
- IntStat d_instantiations_auto_gen;
- IntStat d_instantiations_auto_gen_min;
- IntStat d_splits;
- Statistics();
- ~Statistics();
- };
- Statistics d_statistics;
-public:
- /** the base match */
- std::map< Node, InstMatch > d_baseMatch;
public:
/** general queries about equality */
bool hasTerm( Node a );
/** general creators of candidate generators */
rrinst::CandidateGenerator* getRRCanGenClasses();
rrinst::CandidateGenerator* getRRCanGenClass();
- /** new node */
- void newEqClass( TNode n );
- /** merge */
- void merge( TNode a, TNode b );
- /** assert terms are disequal */
- void assertDisequal( TNode a, TNode b, TNode reason );
public:
/** output eq class */
void outputEqClass( const char* c, Node n );
};/* class InstantiatorTheoryUf */
-/** equality query object using instantiator theory uf */
-class EqualityQueryInstantiatorTheoryUf : public EqualityQuery
-{
-private:
- /** pointer to instantiator uf class */
- InstantiatorTheoryUf* d_ith;
-public:
- EqualityQueryInstantiatorTheoryUf( InstantiatorTheoryUf* ith ) : d_ith( ith ){}
- ~EqualityQueryInstantiatorTheoryUf(){}
- /** general queries about equality */
- bool hasTerm( Node a ) { return d_ith->hasTerm( a ); }
- 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 ); }
- eq::EqualityEngine* getEngine() { return d_ith->getEqualityEngine(); }
- void getEquivalenceClass( Node a, std::vector< Node >& eqc ) { d_ith->getEquivalenceClass( a, eqc ); }
-}; /* EqualityQueryInstantiatorTheoryUf */
+
}
}/* CVC4::theory namespace */
projects / cvc5.git / commitdiff