diff options
Diffstat (limited to 'src/theory/theory_model.h')
| -rw-r--r-- | src/theory/theory_model.h | 125 |
1 files changed, 73 insertions, 52 deletions
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index 00dd215e9..0d73cd72a 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -36,46 +36,13 @@ namespace theory { class TheoryModel : public Model { friend class TheoryEngineModelBuilder; -protected: - /** substitution map for this model */ - SubstitutionMap d_substitutions; - bool d_modelBuilt; + public: TheoryModel(context::Context* c, std::string name, bool enableFuncModels); virtual ~TheoryModel() throw(); - /** special local context for our equalityEngine so we can clear it independently of search context */ - context::Context* d_eeContext; - /** equality engine containing all known equalities/disequalities */ - eq::EqualityEngine* d_equalityEngine; - /** map of representatives of equality engine to used representatives in representative set */ - std::map< Node, Node > d_reps; - /** stores set of representatives for each type */ - RepSet d_rep_set; - /** true/false nodes */ - Node d_true; - Node d_false; - mutable std::unordered_map<Node, Node, NodeHashFunction> d_modelCache; -public: - /** comment stream to include in printing */ - std::stringstream d_comment_str; /** get comments */ void getComments(std::ostream& out) const; -private: - /** information for separation logic */ - Node d_sep_heap; - Node d_sep_nil_eq; -public: - void setHeapModel( Node h, Node neq ); - bool getHeapModel( Expr& h, Expr& neq ) const; -protected: - /** reset the model */ - virtual void reset(); - /** - * Get model value function. This function is called by getValue - */ - Node getModelValue(TNode n, bool hasBoundVars = false, bool useDontCares = false) const; -public: /** is built */ bool isBuilt() { return d_modelBuilt; } /** set need build */ @@ -86,11 +53,13 @@ public: */ Node getValue( TNode n, bool useDontCares = false ) const; - /** get existing domain value, with possible exclusions - * This function returns a term in d_rep_set.d_type_reps[tn] but not in exclude - */ - Node getDomainValue( TypeNode tn, std::vector< Node >& exclude ); -public: + //---------------------------- separation logic + /** set the heap and value sep.nil is equal to */ + void setHeapModel(Node h, Node neq); + /** get the heap and value sep.nil is equal to */ + bool getHeapModel(Expr& h, Expr& neq) const; + //---------------------------- end separation logic + /** Adds a substitution from x to t. */ void addSubstitution(TNode x, TNode t, bool invalidateCache = true); /** add term function @@ -112,33 +81,36 @@ public: * functions. */ void assertRepresentative(TNode n); -public: - /** general queries */ + + // ------------------- general equality queries + /** does the equality engine of this model have term a? */ bool hasTerm(TNode a); + /** get the representative of a in the equality engine of this model */ Node getRepresentative(TNode a); + /** are a and b equal in the equality engine of this model? */ bool areEqual(TNode a, TNode b); + /** are a and b disequal in the equality engine of this model? */ bool areDisequal(TNode a, TNode b); -public: + /** get the equality engine for this model */ + eq::EqualityEngine* getEqualityEngine() { return d_equalityEngine; } + // ------------------- end general equality queries + + /** get the representative set object */ + const RepSet* getRepSet() const { return &d_rep_set; } + /** get the representative set object (FIXME: remove this, see #1199) */ + RepSet* getRepSetPtr() { return &d_rep_set; } /** return whether this node is a don't-care */ bool isDontCare(Expr expr) const; /** get value function for Exprs. */ Expr getValue( Expr expr ) const; /** get cardinality for sort */ Cardinality getCardinality( Type t ) const; -public: /** print representative debug function */ void printRepresentativeDebug( const char* c, Node r ); /** print representative function */ void printRepresentative( std::ostream& out, Node r ); -private: - /** map from function terms to the (lambda) definitions - * After the model is built, the domain of this map is all terms of function type - * that appear as terms in d_equalityEngine. - */ - std::map< Node, Node > d_uf_models; -public: - /** whether function models are enabled */ - bool d_enableFuncModels; + + //---------------------------- function values /** a map from functions f to a list of all APPLY_UF terms with operator f */ std::map< Node, std::vector< Node > > d_uf_terms; /** a map from functions f to a list of all HO_APPLY terms with first argument f */ @@ -154,6 +126,55 @@ public: * which is required for "dag form" model construction (see TheoryModelBuilder::assignHoFunction). */ std::vector< Node > getFunctionsToAssign(); + //---------------------------- end function values + protected: + /** substitution map for this model */ + SubstitutionMap d_substitutions; + /** whether this model has been built */ + bool d_modelBuilt; + /** special local context for our equalityEngine so we can clear it + * independently of search context */ + context::Context* d_eeContext; + /** equality engine containing all known equalities/disequalities */ + eq::EqualityEngine* d_equalityEngine; + /** map of representatives of equality engine to used representatives in + * representative set */ + std::map<Node, Node> d_reps; + /** stores set of representatives for each type */ + RepSet d_rep_set; + /** true/false nodes */ + Node d_true; + Node d_false; + mutable std::unordered_map<Node, Node, NodeHashFunction> d_modelCache; + /** comment stream to include in printing */ + std::stringstream d_comment_str; + /** reset the model */ + virtual void reset(); + /** + * Get model value function. This function is called by getValue + */ + Node getModelValue(TNode n, + bool hasBoundVars = false, + bool useDontCares = false) const; + + private: + //---------------------------- separation logic + /** the value of the heap */ + Node d_sep_heap; + /** the value of the nil element */ + Node d_sep_nil_eq; + //---------------------------- end separation logic + + //---------------------------- function values + /** whether function models are enabled */ + bool d_enableFuncModels; + /** map from function terms to the (lambda) definitions + * After the model is built, the domain of this map is all terms of function + * type + * that appear as terms in d_equalityEngine. + */ + std::map<Node, Node> d_uf_models; + //---------------------------- end function values };/* class TheoryModel */ /* |