diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-31 00:54:24 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-31 00:54:24 +0000 |
commit | f40d0a7cc8d6af511cc0817caf8df3296a59f380 (patch) | |
tree | a79f142c5b6fbeaec34978f8da2b2db308a33e79 /src/theory/uf | |
parent | 5b4c416608bda1df62e1ffe7131648a89882ddc7 (diff) |
cleaning up some of the equality query stuff, implemented a new representative selection strategy for quantifier instantiation
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/inst_strategy.cpp | 42 | ||||
-rw-r--r-- | src/theory/uf/inst_strategy.h | 19 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_instantiator.cpp | 12 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_instantiator.h | 3 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_strong_solver.cpp | 8 |
5 files changed, 14 insertions, 70 deletions
diff --git a/src/theory/uf/inst_strategy.cpp b/src/theory/uf/inst_strategy.cpp index eef2dac79..4fe5772de 100644 --- a/src/theory/uf/inst_strategy.cpp +++ b/src/theory/uf/inst_strategy.cpp @@ -48,48 +48,6 @@ struct sortQuantifiersForSymbol { } }; - -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 ){ diff --git a/src/theory/uf/inst_strategy.h b/src/theory/uf/inst_strategy.h index 6baa5b147..5a3b9cc3d 100644 --- a/src/theory/uf/inst_strategy.h +++ b/src/theory/uf/inst_strategy.h @@ -34,25 +34,6 @@ class InstantiatorTheoryUf; //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 */ diff --git a/src/theory/uf/theory_uf_instantiator.cpp b/src/theory/uf/theory_uf_instantiator.cpp index 0cc32d420..099eb5b5e 100644 --- a/src/theory/uf/theory_uf_instantiator.cpp +++ b/src/theory/uf/theory_uf_instantiator.cpp @@ -38,9 +38,9 @@ InstantiatorTheoryUf::InstantiatorTheoryUf(context::Context* c, CVC4::theory::Qu 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 ); @@ -88,7 +88,7 @@ void InstantiatorTheoryUf::addUserPattern( Node f, Node pat ){ void InstantiatorTheoryUf::processResetInstantiationRound( Theory::Effort effort ){ - d_ground_reps.clear(); + //d_ground_reps.clear(); } int InstantiatorTheoryUf::process( Node f, Theory::Effort effort, int e ){ @@ -132,7 +132,7 @@ Node InstantiatorTheoryUf::getRepresentative( Node a ){ return a; } } - +/* Node InstantiatorTheoryUf::getInternalRepresentative( Node a ){ if( d_ground_reps.find( a )==d_ground_reps.end() ){ if( !hasTerm( a ) ){ @@ -160,7 +160,7 @@ Node InstantiatorTheoryUf::getInternalRepresentative( Node a ){ } return d_ground_reps[a]; } - +*/ eq::EqualityEngine* InstantiatorTheoryUf::getEqualityEngine(){ return &((TheoryUF*)d_th)->d_equalityEngine; } diff --git a/src/theory/uf/theory_uf_instantiator.h b/src/theory/uf/theory_uf_instantiator.h index 324fa6386..3cb4f97cc 100644 --- a/src/theory/uf/theory_uf_instantiator.h +++ b/src/theory/uf/theory_uf_instantiator.h @@ -48,7 +48,7 @@ protected: 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; @@ -132,7 +132,6 @@ public: 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 */ diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index d037c374d..548d6f2f0 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -919,7 +919,13 @@ void StrongSolverTheoryUf::SortRepModel::allocateCardinality( OutputChannel* out //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 |