diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-01 10:08:19 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-11-01 10:08:19 -0500 |
commit | bdcc170e1bf5bb62904c4a3ebbdc9902096799ba (patch) | |
tree | ae8e7ea4eb10d94cfdc1dac3c9d49a00e7baa0a2 /src/theory/theory_model.h | |
parent | 5b6551c529506592da7c66e39a911d9299944eb8 (diff) |
(Move-only) Refactor and document theory model part 2 (#1305)
* Move type set to its own file and document.
* Move theory engine model builder to its own class.
* Working on documentation.
* Document Theory Model.
* Minor
* Document theory model builder.
* Clang format
* Address review.
Diffstat (limited to 'src/theory/theory_model.h')
-rw-r--r-- | src/theory/theory_model.h | 339 |
1 files changed, 84 insertions, 255 deletions
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index 0d73cd72a..a8726f490 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -21,51 +21,80 @@ #include <unordered_set> #include "smt/model.h" -#include "theory/uf/equality_engine.h" #include "theory/rep_set.h" #include "theory/substitutions.h" #include "theory/type_enumerator.h" +#include "theory/type_set.h" +#include "theory/uf/equality_engine.h" namespace CVC4 { namespace theory { -/** - * Theory Model class. - * For Model m, should call m.initialize() before using. +/** Theory Model class. + * + * This class represents a model produced by the TheoryEngine. + * The data structures used to represent a model are: + * (1) d_equalityEngine : an equality engine object, which stores + * an equivalence relation over all terms that exist in + * the current set of assertions. + * (2) d_substitutions : a substitution map storing cases of + * explicitly solved terms, for instance during preprocessing. + * (3) d_reps : a map from equivalence class representatives of + * the equality engine to the (constant) representatives + * assigned to that equivalence class. + * (4) d_uf_models : a map from uninterpreted functions to their + * lambda representation. + * (5) d_rep_set : a data structure that allows interpretations + * for types to be represented as terms. This is useful for + * finite model finding. + * + * These data structures are built after a full effort check with + * no lemmas sent, within a call to: + * TheoryEngineModelBuilder::buildModel(...) + * which includes subcalls to TheoryX::collectModelInfo(...) calls. + * + * These calls may modify the model object using the interface + * functions below, including: + * - assertEquality, assertPredicate, assertRepresentative, + * assertEqualityEngine. + * - assignFunctionDefinition + * + * During and after this building process, these calls may use + * interface functions below to guide the model construction: + * - hasTerm, getRepresentative, areEqual, areDisequal + * - getEqualityEngine + * - getRepSet + * - hasAssignedFunctionDefinition, getFunctionsToAssign + * + * After this building process, the function getValue can be + * used to query the value of nodes. */ class TheoryModel : public Model { friend class TheoryEngineModelBuilder; - public: TheoryModel(context::Context* c, std::string name, bool enableFuncModels); virtual ~TheoryModel() throw(); - /** get comments */ - void getComments(std::ostream& out) const; - /** is built */ - bool isBuilt() { return d_modelBuilt; } - /** set need build */ - void setNeedsBuild() { d_modelBuilt = false; } - /** - * Get value function. This should be called only after a ModelBuilder has called buildModel(...) - * on this model. + /** reset the model */ + virtual void reset(); + /** is built + * + * Have we (attempted to) build this model since the last + * call to reset? Notice for model building techniques + * that are not guaranteed to succeed (such as + * when quantified formulas are enabled), a true return + * value does not imply that this is a model of the + * current assertions. */ - Node getValue( TNode n, bool useDontCares = false ) const; - - //---------------------------- 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 - + bool isBuilt() { return d_modelBuilt; } + //---------------------------- for building the model /** Adds a substitution from x to t. */ void addSubstitution(TNode x, TNode t, bool invalidateCache = true); - /** add term function - * addTerm( n ) will do any model-specific processing necessary for n, - * such as constraining the interpretation of uninterpreted functions, - * and adding n to the equality engine of this model + /** add term + * This will do any model-specific processing necessary for n, + * such as constraining the interpretation of uninterpreted functions, + * and adding n to the equality engine of this model. */ virtual void addTerm(TNode n); /** assert equality holds in the model */ @@ -81,6 +110,7 @@ public: * functions. */ void assertRepresentative(TNode n); + //---------------------------- end building the model // ------------------- general equality queries /** does the equality engine of this model have term a? */ @@ -95,6 +125,23 @@ public: eq::EqualityEngine* getEqualityEngine() { return d_equalityEngine; } // ------------------- end general equality queries + /** Get value function. + * This should be called only after a ModelBuilder + * has called buildModel(...) on this model. + * useDontCares is whether to return Node::null() if + * n does not occur in the equality engine. + */ + Node getValue(TNode n, bool useDontCares = false) const; + /** get comments */ + void getComments(std::ostream& out) const; + + //---------------------------- 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 + /** get the representative set object */ const RepSet* getRepSet() const { return &d_rep_set; } /** get the representative set object (FIXME: remove this, see #1199) */ @@ -145,19 +192,23 @@ public: /** 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 + /** Get model value function. + * + * This function is a helper function for getValue. + * hasBoundVars is whether n may contain bound variables + * useDontCares is whether to return Node::null() if + * n does not occur in the equality engine. */ Node getModelValue(TNode n, bool hasBoundVars = false, bool useDontCares = false) const; private: + /** cache for getModelValue */ + mutable std::unordered_map<Node, Node, NodeHashFunction> d_modelCache; + //---------------------------- separation logic /** the value of the heap */ Node d_sep_heap; @@ -170,234 +221,12 @@ public: 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. + * type that appear as terms in d_equalityEngine. */ std::map<Node, Node> d_uf_models; //---------------------------- end function values };/* class TheoryModel */ -/* - * Class that encapsulates a map from types to sets of nodes - */ -class TypeSet { -public: - typedef std::unordered_map<TypeNode, std::set<Node>*, TypeNodeHashFunction> TypeSetMap; - typedef std::unordered_map<TypeNode, TypeEnumerator*, TypeNodeHashFunction> TypeToTypeEnumMap; - typedef TypeSetMap::iterator iterator; - typedef TypeSetMap::const_iterator const_iterator; -private: - TypeSetMap d_typeSet; - TypeToTypeEnumMap d_teMap; - TypeEnumeratorProperties * d_tep; - - /* Note that recursive traversal here is over enumerated expressions - * (very low expression depth). */ - void addSubTerms(TNode n, std::map< TNode, bool >& visited, bool topLevel=true){ - if( visited.find( n )==visited.end() ){ - visited[n] = true; - if( !topLevel ){ - add(n.getType(), n); - } - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - addSubTerms( n[i], visited, false ); - } - } - } -public: - TypeSet() : d_tep(NULL) {} - ~TypeSet() { - iterator it; - for (it = d_typeSet.begin(); it != d_typeSet.end(); ++it) { - if ((*it).second != NULL) { - delete (*it).second; - } - } - TypeToTypeEnumMap::iterator it2; - for (it2 = d_teMap.begin(); it2 != d_teMap.end(); ++it2) { - if ((*it2).second != NULL) { - delete (*it2).second; - } - } - } - void setTypeEnumeratorProperties( TypeEnumeratorProperties * tep ) { d_tep = tep; } - void add(TypeNode t, TNode n) - { - iterator it = d_typeSet.find(t); - std::set<Node>* s; - if (it == d_typeSet.end()) { - s = new std::set<Node>; - d_typeSet[t] = s; - } - else { - s = (*it).second; - } - s->insert(n); - } - - std::set<Node>* getSet(TypeNode t) const - { - const_iterator it = d_typeSet.find(t); - if (it == d_typeSet.end()) { - return NULL; - } - return (*it).second; - } - - Node nextTypeEnum(TypeNode t, bool useBaseType = false) - { - TypeEnumerator* te; - TypeToTypeEnumMap::iterator it = d_teMap.find(t); - if (it == d_teMap.end()) { - te = new TypeEnumerator(t, d_tep); - d_teMap[t] = te; - } - else { - te = (*it).second; - } - if (te->isFinished()) { - return Node(); - } - - if (useBaseType) { - t = t.getBaseType(); - } - iterator itSet = d_typeSet.find(t); - std::set<Node>* s; - if (itSet == d_typeSet.end()) { - s = new std::set<Node>; - d_typeSet[t] = s; - } - else { - s = (*itSet).second; - } - Node n = **te; - while (s->find(n) != s->end()) { - ++(*te); - if (te->isFinished()) { - return Node(); - } - n = **te; - } - s->insert(n); - // add all subterms of n to this set as well - // this is necessary for parametric types whose values are constructed from other types - // to ensure that we do not enumerate subterms of other previous enumerated values - std::map< TNode, bool > visited; - addSubTerms(n, visited); - ++(*te); - return n; - } - - bool empty() - { - return d_typeSet.empty(); - } - - iterator begin() - { - return d_typeSet.begin(); - } - - iterator end() - { - return d_typeSet.end(); - } - - static TypeNode getType(iterator it) - { - return (*it).first; - } - - static std::set<Node>& getSet(iterator it) - { - return *(*it).second; - } - -};/* class TypeSet */ - -/** TheoryEngineModelBuilder class - * This model builder will consult all theories in a theory engine for - * collectModelInfo( ... ) when building a model. - */ -class TheoryEngineModelBuilder : public ModelBuilder -{ -protected: - /** pointer to theory engine */ - TheoryEngine* d_te; - typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap; - NodeMap d_normalizedCache; - typedef std::unordered_set<Node, NodeHashFunction> NodeSet; - std::map< Node, Node > d_constantReps; - - /** process build model */ - virtual bool preProcessBuildModel(TheoryModel* m); - virtual bool processBuildModel(TheoryModel* m); - virtual void debugModel( TheoryModel* m ) {} - /** normalize representative */ - Node normalize(TheoryModel* m, TNode r, bool evalOnly); - bool isAssignable(TNode n); - void checkTerms(TNode n, TheoryModel* tm, NodeSet& cache); - void assignConstantRep( TheoryModel* tm, Node eqc, Node const_rep ); - void addToTypeList( TypeNode tn, std::vector< TypeNode >& type_list, std::map< TypeNode, bool >& visiting ); - /** is v an excluded codatatype value */ - bool isExcludedCdtValue( Node v, std::set<Node>* repSet, std::map< Node, Node >& assertedReps, Node eqc ); - bool isCdtValueMatch( Node v, Node r, Node eqc, Node& eqc_m ); - /** 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(){} - /** Build model function. - * Should be called only on TheoryModels m - */ - bool buildModel(Model* m); - void debugCheckModel(Model* m); -};/* class TheoryEngineModelBuilder */ - }/* CVC4::theory namespace */ }/* CVC4 namespace */ |