diff options
Diffstat (limited to 'src/theory/rr_inst_match.cpp')
-rw-r--r-- | src/theory/rr_inst_match.cpp | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/src/theory/rr_inst_match.cpp b/src/theory/rr_inst_match.cpp index 3ba0c8d32..287f7475a 100644 --- a/src/theory/rr_inst_match.cpp +++ b/src/theory/rr_inst_match.cpp @@ -15,16 +15,16 @@ **/ #include "theory/inst_match.h" -#include "theory/rr_inst_match.h" -#include "theory/rr_trigger.h" -#include "theory/rr_inst_match_impl.h" #include "theory/theory_engine.h" #include "theory/quantifiers_engine.h" #include "theory/uf/theory_uf_instantiator.h" -#include "theory/uf/theory_uf_candidate_generator.h" -#include "theory/datatypes/theory_datatypes_candidate_generator.h" #include "theory/uf/equality_engine.h" #include "theory/arrays/theory_arrays.h" +#include "theory/datatypes/theory_datatypes.h" +#include "theory/rr_inst_match.h" +#include "theory/rr_trigger.h" +#include "theory/rr_inst_match_impl.h" +#include "theory/rr_candidate_generator.h" using namespace CVC4; using namespace CVC4::kind; @@ -437,8 +437,7 @@ class OpMatcher: public Matcher{ AuxMatcher2 am2(am3,LegalOpTest(pat.getOperator())); /** Iter on the equivalence class of the given term */ uf::TheoryUF* uf = static_cast<uf::TheoryUF *>(qe->getTheoryEngine()->getTheory( theory::THEORY_UF )); - eq::EqualityEngine* ee = - static_cast<eq::EqualityEngine*>(uf->getEqualityEngine()); + eq::EqualityEngine* ee = static_cast<eq::EqualityEngine*>(uf->getEqualityEngine()); CandidateGeneratorTheoryEeClass cdtUfEq(ee); /* Create a matcher from the candidate generator */ AuxMatcher1 am1(cdtUfEq,am2); @@ -474,7 +473,7 @@ class DatatypesMatcher: public Matcher{ /* The matcher */ typedef ApplyMatcher AuxMatcher3; typedef TestMatcher< AuxMatcher3, LegalOpTest > AuxMatcher2; - typedef CandidateGeneratorMatcher< datatypes::rrinst::CandidateGeneratorTheoryClass, AuxMatcher2> AuxMatcher1; + typedef CandidateGeneratorMatcher< CandidateGeneratorTheoryEeClass, AuxMatcher2> AuxMatcher1; AuxMatcher1 d_cgm; static inline AuxMatcher1 createCgm(Node pat, QuantifiersEngine* qe){ Assert( pat.getKind() == kind::APPLY_CONSTRUCTOR, @@ -485,7 +484,8 @@ class DatatypesMatcher: public Matcher{ AuxMatcher2 am2(am3,LegalOpTest(pat.getOperator())); /** Iter on the equivalence class of the given term */ datatypes::TheoryDatatypes* dt = static_cast<datatypes::TheoryDatatypes *>(qe->getTheoryEngine()->getTheory( theory::THEORY_DATATYPES )); - datatypes::rrinst::CandidateGeneratorTheoryClass cdtDtEq(dt); + eq::EqualityEngine* ee = static_cast<eq::EqualityEngine*>(dt->getEqualityEngine()); + CandidateGeneratorTheoryEeClass cdtDtEq(ee); /* Create a matcher from the candidate generator */ AuxMatcher1 am1(cdtDtEq,am2); return am1; |