diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-10-05 07:12:47 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-10-05 07:12:47 -0500 |
commit | f56f46f5bb5845cff0c329926f51a0377379365b (patch) | |
tree | ff22d91db4f2265b17634b3797cc724ee079f410 /src/theory/theory_model.h | |
parent | 3c5c0c2287203b61acc94bb83fac1b91ae290007 (diff) |
Ho model (#1120)
* Update model construction for higher order. If HO_APPLY terms are present for a function, we use a curried (tree) model construction to avoid exponential size model representations for function definitions.
* Update comments.
* Change terminology in comment.
* Improve comments.
Diffstat (limited to 'src/theory/theory_model.h')
-rw-r--r-- | src/theory/theory_model.h | 64 |
1 files changed, 62 insertions, 2 deletions
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index 6c9e706d4..00dd215e9 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -130,12 +130,30 @@ public: 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; - //necessary information for function models + /** 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; - std::map< Node, Node > d_uf_models; + /** 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; + /** assign function value f to definition f_def */ + void assignFunctionDefinition( Node f, Node f_def ); + /** have we assigned function f? */ + bool hasAssignedFunctionDefinition( Node f ) const { return d_uf_models.find( f )!=d_uf_models.end(); } + /** get the list of functions to assign. + * This list will contain all terms of function type that are terms in d_equalityEngine. + * If higher-order is enabled, we ensure that this list is sorted by type size. + * This allows us to assign functions T -> T before ( T x T ) -> T and before ( T -> T ) -> T, + * which is required for "dag form" model construction (see TheoryModelBuilder::assignHoFunction). + */ + std::vector< Node > getFunctionsToAssign(); };/* class TheoryModel */ /* @@ -307,6 +325,48 @@ protected: /** involves usort */ bool involvesUSort( TypeNode tn ); bool isExcludedUSortValue( std::map< TypeNode, unsigned >& eqc_usort_count, Node v, std::map< Node, bool >& visited ); +protected: + /** assign function f based on the model m. + * This construction is based on "table form". For example: + * (f 0 1) = 1 + * (f 0 2) = 2 + * (f 1 1) = 3 + * ... + * becomes: + * f = (lambda xy. (ite (and (= x 0) (= y 1)) 1 + * (ite (and (= x 0) (= y 2)) 2 + * (ite (and (= x 1) (= y 1)) 3 ...))) + */ + void assignFunction(TheoryModel* m, Node f); + /** assign function f based on the model m. + * This construction is based on "dag form". For example: + * (f 0 1) = 1 + * (f 0 2) = 2 + * (f 1 1) = 3 + * ... + * becomes: + * f = (lambda xy. (ite (= x 0) (ite (= y 1) 1 + * (ite (= y 2) 2 ...)) + * (ite (= x 1) (ite (= y 1) 3 ...) + * ...)) + * + * where the above is represented as a directed acyclic graph (dag). + * This construction is accomplished by assigning values to (f c) + * terms before f, e.g. + * (f 0) = (lambda y. (ite (= y 1) 1 + * (ite (= y 2) 2 ...)) + * (f 1) = (lambda y. (ite (= y 1) 3 ...)) + * where + * f = (lambda xy. (ite (= x 0) ((f 0) y) + * (ite (= x 1) ((f 1) y) ...)) + */ + void assignHoFunction(TheoryModel* m, Node f); + /** Assign all unassigned functions in the model m (those returned by TheoryModel::getFunctionsToAssign), + * using the two functions above. Currently: + * If ufHo is disabled, we call assignFunction for all functions. + * If ufHo is enabled, we call assignHoFunction. + */ + void assignFunctions(TheoryModel* m); public: TheoryEngineModelBuilder(TheoryEngine* te); virtual ~TheoryEngineModelBuilder(){} |