diff options
Diffstat (limited to 'src/theory/theory_model.h')
| -rw-r--r-- | src/theory/theory_model.h | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index 42392c522..b4a089767 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -328,10 +328,10 @@ public: Cardinality getCardinality(TypeNode t) const; //---------------------------- 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 */ - std::map< Node, std::vector< Node > > d_ho_uf_terms; + /** Does this model have terms for the given uninterpreted function? */ + bool hasUfTerms(Node f) const; + /** Get the terms for uninterpreted function f */ + const std::vector<Node>& getUfTerms(Node f) const; /** are function values enabled? */ bool areFunctionValuesEnabled() const; /** assign function value f to definition f_def */ @@ -423,6 +423,11 @@ public: //---------------------------- end separation logic //---------------------------- 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 */ + std::map<Node, std::vector<Node> > d_ho_uf_terms; /** whether function models are enabled */ bool d_enableFuncModels; /** map from function terms to the (lambda) definitions |