diff options
Diffstat (limited to 'src/theory/theory.h')
-rw-r--r-- | src/theory/theory.h | 57 |
1 files changed, 57 insertions, 0 deletions
diff --git a/src/theory/theory.h b/src/theory/theory.h index b5a5d4e6d..ede06fd2d 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -48,6 +48,7 @@ namespace theory { class QuantifiersEngine; class TheoryModel; class SubstitutionMap; +class ExtTheory; class EntailmentCheckParameters; class EntailmentCheckSideEffects; @@ -201,6 +202,9 @@ private: protected: + /** extended theory */ + ExtTheory * d_extt; + // === STATISTICS === /** time spent in check calls */ TimerStat d_checkTime; @@ -881,6 +885,16 @@ public: */ virtual std::pair<bool, Node> entailmentCheck(TNode lit, const EntailmentCheckParameters* params = NULL, EntailmentCheckSideEffects* out = NULL); + /* equality engine */ + virtual eq::EqualityEngine * getEqualityEngine() { return NULL; } + + /* get current substitution at an effort + * input : vars + * output : subs, exp + * where ( exp[vars[i]] => vars[i] = subs[i] ) holds for all i + */ + virtual bool getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ) { return false; } + /** * Turn on proof-production mode. */ @@ -950,6 +964,49 @@ public: virtual ~EntailmentCheckSideEffects(); };/* class EntailmentCheckSideEffects */ + +class ExtTheory { + friend class Theory; + typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap; +protected: + Theory * d_parent; + //extended string terms, map to whether they are active + NodeBoolMap d_ext_func_terms; + //any non-reduced extended functions exist + context::CDO< bool > d_has_extf; + //extf kind + std::map< Kind, bool > d_extf_kind; + //information for extf + class ExtfInfo { + public: + //all variables in this term + std::vector< Node > d_vars; + }; + std::map< Node, ExtfInfo > d_extf_info; + //collect variables + void collectVars( Node n, std::vector< Node >& vars, std::map< Node, bool >& visited ); +public: + ExtTheory( Theory * p ); + virtual ~ExtTheory(){} + //add extf kind + void addFunctionKind( Kind k ) { d_extf_kind[k] = true; } + //do inferences + // input : effort + // output : terms, sterms, exp, where ( exp[i] => terms[i] = sterms[i] ) for all i + void getInferences( int effort, std::vector< Node >& terms, std::vector< Node >& sterms, std::vector< std::vector< Node > >& exp ); + //register term + void registerTerm( Node n ); + //mark reduced + void markReduced( Node n ); + //mark congruent + void markCongruent( Node a, Node b ); + //is active + bool isActive( Node n ); + //get active + void getActive( std::vector< Node >& active ); + void getActive( std::vector< Node >& active, Kind k ); +}; + }/* CVC4::theory namespace */ }/* CVC4 namespace */ |