diff options
Diffstat (limited to 'src/theory/rewriterules')
-rwxr-xr-x | src/theory/rewriterules/efficient_e_matching.cpp | 3 | ||||
-rw-r--r-- | src/theory/rewriterules/rr_candidate_generator.cpp | 78 | ||||
-rw-r--r-- | src/theory/rewriterules/rr_candidate_generator.h | 16 | ||||
-rw-r--r-- | src/theory/rewriterules/rr_inst_match.cpp | 1 | ||||
-rw-r--r-- | src/theory/rewriterules/rr_trigger.cpp | 1 |
5 files changed, 17 insertions, 82 deletions
diff --git a/src/theory/rewriterules/efficient_e_matching.cpp b/src/theory/rewriterules/efficient_e_matching.cpp index 7f03bf8f8..2f39d8098 100755 --- a/src/theory/rewriterules/efficient_e_matching.cpp +++ b/src/theory/rewriterules/efficient_e_matching.cpp @@ -92,7 +92,8 @@ EfficientEMatcher::EfficientEMatcher( CVC4::theory::QuantifiersEngine* qe ) : d_ }
eq::EqualityEngine* EfficientEMatcher::getEqualityEngine(){
- return ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getEqualityEngine();
+ //return ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getEqualityEngine();
+ return d_quantEngine->getMasterEqualityEngine();
}
/** new node */
diff --git a/src/theory/rewriterules/rr_candidate_generator.cpp b/src/theory/rewriterules/rr_candidate_generator.cpp index 2957b4ddb..3f2895397 100644 --- a/src/theory/rewriterules/rr_candidate_generator.cpp +++ b/src/theory/rewriterules/rr_candidate_generator.cpp @@ -24,100 +24,44 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::rrinst; -GenericCandidateGeneratorClasses::GenericCandidateGeneratorClasses(QuantifiersEngine * qe){ - for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ - if(qe->getInstantiator(i) != NULL) - d_can_gen[i] = qe->getInstantiator(i)->getRRCanGenClasses(); - else d_can_gen[i] = NULL; - } +GenericCandidateGeneratorClasses::GenericCandidateGeneratorClasses(QuantifiersEngine * qe) : d_qe(qe){ + d_master_can_gen = new eq::rrinst::CandidateGeneratorTheoryEeClasses(d_qe->getMasterEqualityEngine()); } GenericCandidateGeneratorClasses::~GenericCandidateGeneratorClasses(){ - for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ - delete(d_can_gen[i]); - } + delete d_master_can_gen; } void GenericCandidateGeneratorClasses::resetInstantiationRound(){ - for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ - if(d_can_gen[i] != NULL) d_can_gen[i]->resetInstantiationRound(); - } - d_can_gen_id=THEORY_FIRST; + d_master_can_gen->resetInstantiationRound(); } void GenericCandidateGeneratorClasses::reset(TNode eqc){ - Assert(eqc.isNull()); - for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ - if(d_can_gen[i] != NULL) d_can_gen[i]->reset(eqc); - } - d_can_gen_id=THEORY_FIRST; - lookForNextTheory(); + d_master_can_gen->reset(eqc); } TNode GenericCandidateGeneratorClasses::getNextCandidate(){ - Assert(THEORY_FIRST <= d_can_gen_id && d_can_gen_id <= THEORY_LAST); - /** No more */ - if(d_can_gen_id == THEORY_LAST) return TNode::null(); - /** Try with this theory */ - TNode cand = d_can_gen[d_can_gen_id]->getNextCandidate(); - if( !cand.isNull() ) return cand; - lookForNextTheory(); - return getNextCandidate(); + return d_master_can_gen->getNextCandidate(); } -void GenericCandidateGeneratorClasses::lookForNextTheory(){ - do{ /* look for the next available generator */ - ++d_can_gen_id; - } while( d_can_gen_id < THEORY_LAST && d_can_gen[d_can_gen_id] == NULL); -} GenericCandidateGeneratorClass::GenericCandidateGeneratorClass(QuantifiersEngine * qe): d_qe(qe) { - for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ - if(d_qe->getInstantiator(i) != NULL) - d_can_gen[i] = d_qe->getInstantiator(i)->getRRCanGenClass(); - else d_can_gen[i] = NULL; - } + d_master_can_gen = new eq::rrinst::CandidateGeneratorTheoryEeClass(d_qe->getMasterEqualityEngine()); } GenericCandidateGeneratorClass::~GenericCandidateGeneratorClass(){ - for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ - delete(d_can_gen[i]); - } + delete d_master_can_gen; } void GenericCandidateGeneratorClass::resetInstantiationRound(){ - for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ - if(d_can_gen[i] != NULL) d_can_gen[i]->resetInstantiationRound(); - } - d_can_gen_id=THEORY_FIRST; + d_master_can_gen->resetInstantiationRound(); } void GenericCandidateGeneratorClass::reset(TNode eqc){ - for(TheoryId i = THEORY_FIRST; i < theory::THEORY_LAST; ++i){ - if(d_can_gen[i] != NULL) d_can_gen[i]->reset(eqc); - } - d_can_gen_id=THEORY_FIRST; - d_node = eqc; - lookForNextTheory(); + d_master_can_gen->reset(eqc); } TNode GenericCandidateGeneratorClass::getNextCandidate(){ - Assert(THEORY_FIRST <= d_can_gen_id && d_can_gen_id <= THEORY_LAST); - /** No more */ - if(d_can_gen_id == THEORY_LAST) return TNode::null(); - /** Try with this theory */ - TNode cand = d_can_gen[d_can_gen_id]->getNextCandidate(); - if( !cand.isNull() ) return cand; - lookForNextTheory(); - return getNextCandidate(); + return d_master_can_gen->getNextCandidate(); } -void GenericCandidateGeneratorClass::lookForNextTheory(){ - do{ /* look for the next available generator, where the element is */ - ++d_can_gen_id; - } while( - d_can_gen_id < THEORY_LAST && - (d_can_gen[d_can_gen_id] == NULL || - !d_qe->getInstantiator( d_can_gen_id )->hasTerm( d_node )) - ); -} diff --git a/src/theory/rewriterules/rr_candidate_generator.h b/src/theory/rewriterules/rr_candidate_generator.h index 8ebaae343..97c710219 100644 --- a/src/theory/rewriterules/rr_candidate_generator.h +++ b/src/theory/rewriterules/rr_candidate_generator.h @@ -166,10 +166,9 @@ public: class GenericCandidateGeneratorClasses: public rrinst::CandidateGenerator{ /** The candidate generators */ - rrinst::CandidateGenerator* d_can_gen[theory::THEORY_LAST]; - /** The current theory which candidategenerator is used */ - TheoryId d_can_gen_id; - + rrinst::CandidateGenerator* d_master_can_gen; + /** QuantifierEngine */ + QuantifiersEngine* d_qe; public: GenericCandidateGeneratorClasses(QuantifiersEngine * qe); ~GenericCandidateGeneratorClasses(); @@ -183,22 +182,15 @@ public: class GenericCandidateGeneratorClass: public rrinst::CandidateGenerator{ /** The candidate generators */ - rrinst::CandidateGenerator* d_can_gen[theory::THEORY_LAST]; - /** The current theory which candidategenerator is used */ - TheoryId d_can_gen_id; - /** current node to look for equivalence class */ - Node d_node; + rrinst::CandidateGenerator* d_master_can_gen; /** QuantifierEngine */ QuantifiersEngine* d_qe; - public: GenericCandidateGeneratorClass(QuantifiersEngine * qe); ~GenericCandidateGeneratorClass(); void resetInstantiationRound(); - void reset(TNode eqc); TNode getNextCandidate(); - void lookForNextTheory(); }; }/* CVC4::theory namespace */ diff --git a/src/theory/rewriterules/rr_inst_match.cpp b/src/theory/rewriterules/rr_inst_match.cpp index 5f10e1daa..5c3a55831 100644 --- a/src/theory/rewriterules/rr_inst_match.cpp +++ b/src/theory/rewriterules/rr_inst_match.cpp @@ -15,7 +15,6 @@ #include "theory/quantifiers/inst_match.h" #include "theory/theory_engine.h" #include "theory/quantifiers_engine.h" -#include "theory/uf/theory_uf_instantiator.h" #include "theory/uf/equality_engine.h" #include "theory/arrays/theory_arrays.h" #include "theory/datatypes/theory_datatypes.h" diff --git a/src/theory/rewriterules/rr_trigger.cpp b/src/theory/rewriterules/rr_trigger.cpp index ad77f0bcb..4f48a72ae 100644 --- a/src/theory/rewriterules/rr_trigger.cpp +++ b/src/theory/rewriterules/rr_trigger.cpp @@ -15,7 +15,6 @@ #include "theory/rewriterules/rr_trigger.h" #include "theory/theory_engine.h" #include "theory/quantifiers_engine.h" -#include "theory/uf/theory_uf_instantiator.h" #include "theory/rewriterules/rr_candidate_generator.h" #include "theory/uf/equality_engine.h" |