summaryrefslogtreecommitdiff
path: root/src/theory/rewriterules
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/rewriterules')
-rwxr-xr-xsrc/theory/rewriterules/efficient_e_matching.cpp3
-rw-r--r--src/theory/rewriterules/rr_candidate_generator.cpp78
-rw-r--r--src/theory/rewriterules/rr_candidate_generator.h16
-rw-r--r--src/theory/rewriterules/rr_inst_match.cpp1
-rw-r--r--src/theory/rewriterules/rr_trigger.cpp1
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"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback