diff options
author | François Bobot <francois@bobot.eu> | 2012-07-27 13:36:32 +0000 |
---|---|---|
committer | François Bobot <francois@bobot.eu> | 2012-07-27 13:36:32 +0000 |
commit | 4bfa927dac67bbcadf219f70e61f1d123e33944b (patch) | |
tree | f295343430799748de8b9a823f1a3c641c096905 /src/theory/arrays | |
parent | 988c97d92fa617c5dccaeb1ef33121bfa6459afc (diff) |
Merge quantifiers2-trunk:
- new syntax for rewrite rules
- better rewrite rules theory
- remove the rewriting with rewrite rules during ppRewrite temporarily
- theory can define their own candidate generator
- define a general candidate generator (inefficient ask to every theory)
- split inst_match between the pattern matching used for quantifiers (inst_match.*) and
the one used for rewrite rules (rr_inst_match.*):
- the pattern matching is less exhaustive for quantifiers,
- the one for rewrite rules can use efficient-e-matching.
Diffstat (limited to 'src/theory/arrays')
-rw-r--r-- | src/theory/arrays/theory_arrays_instantiator.cpp | 14 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays_instantiator.h | 6 |
2 files changed, 19 insertions, 1 deletions
diff --git a/src/theory/arrays/theory_arrays_instantiator.cpp b/src/theory/arrays/theory_arrays_instantiator.cpp index 2e446c57f..ca9001fe5 100644 --- a/src/theory/arrays/theory_arrays_instantiator.cpp +++ b/src/theory/arrays/theory_arrays_instantiator.cpp @@ -17,6 +17,7 @@ #include "theory/theory_engine.h" #include "theory/arrays/theory_arrays_instantiator.h" #include "theory/arrays/theory_arrays.h" +#include "theory/uf/theory_uf_candidate_generator.h" using namespace std; using namespace CVC4; @@ -83,3 +84,16 @@ Node InstantiatorTheoryArrays::getRepresentative( Node a ){ } } +rrinst::CandidateGenerator* InstantiatorTheoryArrays::getRRCanGenClasses(){ + arrays::TheoryArrays* ar = static_cast<arrays::TheoryArrays *>(getTheory()); + eq::EqualityEngine* ee = + static_cast<eq::EqualityEngine*>(ar->getEqualityEngine()); + return new eq::rrinst::CandidateGeneratorTheoryEeClasses(ee); +} + +rrinst::CandidateGenerator* InstantiatorTheoryArrays::getRRCanGenClass(){ + arrays::TheoryArrays* ar = static_cast<arrays::TheoryArrays *>(getTheory()); + eq::EqualityEngine* ee = + static_cast<eq::EqualityEngine*>(ar->getEqualityEngine()); + return new eq::rrinst::CandidateGeneratorTheoryEeClass(ee); +} diff --git a/src/theory/arrays/theory_arrays_instantiator.h b/src/theory/arrays/theory_arrays_instantiator.h index ade43fdb0..f711229b2 100644 --- a/src/theory/arrays/theory_arrays_instantiator.h +++ b/src/theory/arrays/theory_arrays_instantiator.h @@ -21,6 +21,7 @@ #define __CVC4__INSTANTIATOR_THEORY_ARRAYS_H #include "theory/quantifiers_engine.h" +#include "theory/uf/equality_engine.h" namespace CVC4 { namespace theory { @@ -48,10 +49,13 @@ public: bool areEqual( Node a, Node b ); bool areDisequal( Node a, Node b ); Node getRepresentative( Node a ); + /** general creators of candidate generators */ + rrinst::CandidateGenerator* getRRCanGenClasses(); + rrinst::CandidateGenerator* getRRCanGenClass(); };/* class Instantiatior */ } } } -#endif
\ No newline at end of file +#endif |