diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-10-03 21:28:11 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-10-03 21:28:11 +0000 |
commit | c3e9112157320111c18b2984052abd9cd17127dc (patch) | |
tree | 1fa4ff944c86630034357994dd602486f609899e /src/theory/model.h | |
parent | c33c9d3699597abe2fbeaacb6799ba05f11f8e93 (diff) |
New model code, mostly workin
Diffstat (limited to 'src/theory/model.h')
-rw-r--r-- | src/theory/model.h | 128 |
1 files changed, 115 insertions, 13 deletions
diff --git a/src/theory/model.h b/src/theory/model.h index de4d57d2e..90cd1e35a 100644 --- a/src/theory/model.h +++ b/src/theory/model.h @@ -23,13 +23,11 @@ #include "theory/uf/equality_engine.h" #include "theory/rep_set.h" #include "theory/substitutions.h" +#include "theory/type_enumerator.h" namespace CVC4 { namespace theory { -class QuantifiersEngine; -class TheoryEngineModelBuilder; - /** Theory Model class * For Model m, should call m.initialize() before using */ @@ -133,6 +131,112 @@ public: std::map< Node, Node > d_uf_models; }; +/* + * Class that encapsulates a map from types to sets of nodes + */ +class TypeSet { +public: + typedef std::hash_map<TypeNode, std::set<Node>*, TypeNodeHashFunction> TypeSetMap; + typedef std::hash_map<TypeNode, TypeEnumerator*, TypeNodeHashFunction> TypeToTypeEnumMap; + typedef TypeSetMap::iterator iterator; +private: + TypeSetMap d_typeSet; + TypeToTypeEnumMap d_teMap; + + public: + ~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 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) + { + iterator it = d_typeSet.find(t); + if (it == d_typeSet.end()) { + return NULL; + } + return (*it).second; + } + + Node nextTypeEnum(TypeNode t) + { + TypeEnumerator* te; + TypeToTypeEnumMap::iterator it = d_teMap.find(t); + if (it == d_teMap.end()) { + te = new TypeEnumerator(t); + d_teMap[t] = te; + } + else { + te = (*it).second; + } + Assert(!te->isFinished()); + + 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()) { + Assert(!te->isFinished()); + ++(*te); + n = **te; + } + s->insert(n); + ++(*te); + return n; + } + + 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; + } + +}; + /** TheoryEngineModelBuilder class * This model builder will consult all theories in a theory engine for * collectModelInfo( ... ) when building a model. @@ -142,24 +246,22 @@ class TheoryEngineModelBuilder : public ModelBuilder protected: /** pointer to theory engine */ TheoryEngine* d_te; + typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; + NodeMap d_normalizedCache; + /** process build model */ - virtual void processBuildModel( TheoryModel* m, bool fullModel ); + virtual void processBuildModel(TheoryModel* m, bool fullModel); /** choose representative for unconstrained equivalence class */ - virtual Node chooseRepresentative( TheoryModel* m, Node eqc, bool fullModel ); + virtual Node chooseRepresentative(TheoryModel* m, Node eqc, bool fullModel); /** normalize representative */ - Node normalizeRepresentative( TheoryModel* m, Node r, std::map< Node, Node >& reps, - std::map< Node, bool >& normalized, - std::map< Node, bool >& normalizing ); - Node normalizeNode( TheoryModel* m, Node r, std::map< Node, Node >& reps, - std::map< Node, bool >& normalized, - std::map< Node, bool >& normalizing ); + Node normalize(TheoryModel* m, TNode r, std::map<Node, Node>& constantReps); public: - TheoryEngineModelBuilder( TheoryEngine* te ); + TheoryEngineModelBuilder(TheoryEngine* te); virtual ~TheoryEngineModelBuilder(){} /** Build model function. * Should be called only on TheoryModels m */ - void buildModel( Model* m, bool fullModel ); + void buildModel(Model* m, bool fullModel); }; } |