diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-24 09:37:13 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-24 09:37:32 -0500 |
commit | 67ea40d24cbbcd3f490248754a6abc1989bacc7b (patch) | |
tree | f74d7a52a5046e346035b1c5b5abec1f17004033 /src/theory/theory_model.h | |
parent | 2c1e5b35ba688c0df297b0510058454c54bab54d (diff) |
Refactor model building for quantifiers to be a single pass, simplification. Modify datatypes collect model info to include dt equivalence classes. Further work on sygus. Other minor fixes.
Diffstat (limited to 'src/theory/theory_model.h')
-rw-r--r-- | src/theory/theory_model.h | 19 |
1 files changed, 12 insertions, 7 deletions
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index c30d1eabc..82341c377 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -36,7 +36,7 @@ class TheoryModel : public Model protected: /** substitution map for this model */ SubstitutionMap d_substitutions; - context::CDO<bool> d_modelBuilt; + bool d_modelBuilt; public: TheoryModel(context::Context* c, std::string name, bool enableFuncModels); virtual ~TheoryModel() throw(); @@ -74,7 +74,9 @@ protected: Node getModelValue(TNode n, bool hasBoundVars = false, bool useDontCares = false) const; public: /** is built */ - bool isBuilt() { return d_modelBuilt.get(); } + 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. @@ -266,15 +268,17 @@ protected: typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; NodeMap d_normalizedCache; typedef std::hash_set<Node, NodeHashFunction> NodeSet; + std::map< Node, Node > d_constantReps; /** process build model */ - virtual void preProcessBuildModel(TheoryModel* m, bool fullModel); - virtual void processBuildModel(TheoryModel* m, bool fullModel); + virtual bool preProcessBuildModel(TheoryModel* m); + virtual bool processBuildModel(TheoryModel* m); + virtual void debugModel( TheoryModel* m ) {} /** normalize representative */ - Node normalize(TheoryModel* m, TNode r, std::map<Node, Node>& constantReps, bool evalOnly); + Node normalize(TheoryModel* m, TNode r, bool evalOnly); bool isAssignable(TNode n); void checkTerms(TNode n, TheoryModel* tm, NodeSet& cache); - void assignConstantRep( TheoryModel* tm, std::map<Node, Node>& constantReps, Node eqc, Node const_rep, bool fullModel ); + void assignConstantRep( TheoryModel* tm, Node eqc, Node const_rep ); /** 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 ); @@ -287,7 +291,8 @@ public: /** Build model function. * Should be called only on TheoryModels m */ - void buildModel(Model* m, bool fullModel); + bool buildModel(Model* m); + void debugCheckModel(Model* m); };/* class TheoryEngineModelBuilder */ }/* CVC4::theory namespace */ |