diff options
Diffstat (limited to 'src/theory/theory_model.h')
| -rw-r--r-- | src/theory/theory_model.h | 50 |
1 files changed, 50 insertions, 0 deletions
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index b6d1288ae..cee39b542 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -161,6 +161,50 @@ public: * construction process. */ void recordApproximation(TNode n, TNode pred); + /** set unevaluate/semi-evaluated kind + * + * This informs this model how it should interpret applications of terms with + * kind k in getModelValue. We distinguish four categories of kinds: + * + * [1] "Evaluated" + * This includes (standard) interpreted symbols like NOT, PLUS, UNION, etc. + * These operators can be characterized by the invariant that they are + * "evaluatable". That is, if they are applied to only constants, the rewriter + * is guaranteed to rewrite the application to a constant. When getting + * the model value of <k>( t1...tn ) where k is a kind of this category, we + * compute the (constant) value of t1...tn, say this returns c1...cn, we + * return the (constant) result of rewriting <k>( c1...cn ). + * + * [2] "Unevaluated" + * This includes interpreted symbols like FORALL, EXISTS, + * CARDINALITY_CONSTRAINT, that are not evaluatable. When getting a model + * value for a term <k>( t1...tn ) where k is a kind of this category, we + * check whether <k>( t1...tn ) exists in the equality engine of this model. + * If it does, we return its representative, otherwise we return the term + * itself. + * + * [3] "Semi-evaluated" + * This includes kinds like BITVECTOR_ACKERMANNIZE_UDIV and others, typically + * those that correspond to abstractions. Like unevaluated kinds, these + * kinds do not have an evaluator. In contrast to unevaluated kinds, we + * interpret a term <k>( t1...tn ) not appearing in the equality engine as an + * arbitrary value instead of the term itself. + * + * [4] APPLY_UF, where getting the model value depends on an internally + * constructed representation of a lambda model value (d_uf_models). + * It is optional whether this kind is "evaluated" or "semi-evaluated". + * In the case that it is "evaluated", get model rewrites the application + * of the lambda model value of its operator to its evaluated arguments. + * + * By default, all kinds are considered "evaluated". The following methods + * change the interpretation of various (non-APPLY_UF) kinds to one of the + * above categories and should be called by the theories that own the kind + * during Theory::finishInit. We set APPLY_UF to be semi-interpreted when + * this model does not enabled function values (this is the case for the model + * of TheoryEngine when the option assignFunctionValues is set to false). + */ + void setUnevaluatedKind(Kind k); + void setSemiEvaluatedKind(Kind k); //---------------------------- end building the model // ------------------- general equality queries @@ -217,6 +261,8 @@ public: 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; + /** are function values enabled? */ + bool areFunctionValuesEnabled() const; /** assign function value f to definition f_def */ void assignFunctionDefinition( Node f, Node f_def ); /** have we assigned function f? */ @@ -245,6 +291,10 @@ public: std::map<Node, Node> d_approximations; /** list of all approximations */ std::vector<std::pair<Node, Node> > d_approx_list; + /** a set of kinds that are not evaluated */ + std::unordered_set<Kind, kind::KindHashFunction> d_not_evaluated_kinds; + /** a set of kinds that are semi-evaluated */ + std::unordered_set<Kind, kind::KindHashFunction> d_semi_evaluated_kinds; /** map of representatives of equality engine to used representatives in * representative set */ std::map<Node, Node> d_reps; |