diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-07-27 19:27:45 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-07-27 19:27:45 +0000 |
commit | 9a994c449d65e64d574a423ad9caad519f8c2148 (patch) | |
tree | 3c4571098d1771f8d277406c9f6e9c5b09dcd1da /src/theory/theory.h | |
parent | 4bfa927dac67bbcadf219f70e61f1d123e33944b (diff) |
merging fmf-devel branch, includes refactored datatype theory, updates to model.h/cpp to prepare for release, and major refactoring of quantifiers/finite model finding. Note that new datatype theory does not insist upon any interpretation for selectors applied to incorrect constructors and consequently some answers may differ with previous version
Diffstat (limited to 'src/theory/theory.h')
-rw-r--r-- | src/theory/theory.h | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/theory/theory.h b/src/theory/theory.h index 0cf7a8774..24551637b 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -777,6 +777,10 @@ public: std::ostream& operator<<(std::ostream& os, Theory::Effort level); +namespace eq{ + class EqualityEngine; +} + class Instantiator { friend class QuantifiersEngine; protected: @@ -838,6 +842,8 @@ public: virtual bool areDisequal( Node a, Node b ) { return false; } virtual Node getRepresentative( Node a ) { return a; } virtual Node getInternalRepresentative( Node a ) { return getRepresentative( a ); } + virtual eq::EqualityEngine* getEqualityEngine() { return NULL; } + virtual void getEquivalenceClass( Node a, std::vector< Node >& eqc ) {} public: /** A Creator of CandidateGenerator for classes (one element in each equivalence class) and class (every element of one equivalence |