summaryrefslogtreecommitdiff
path: root/src/theory/theory_model.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/theory_model.h')
-rw-r--r--src/theory/theory_model.h4
1 files changed, 3 insertions, 1 deletions
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index 6e4f77336..833b124eb 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -36,6 +36,7 @@ class TheoryModel : public Model
protected:
/** substitution map for this model */
SubstitutionMap d_substitutions;
+ context::CDO<bool> d_modelBuilt;
public:
TheoryModel(context::Context* c, std::string name, bool enableFuncModels);
virtual ~TheoryModel() throw();
@@ -51,7 +52,6 @@ public:
/** true/false nodes */
Node d_true;
Node d_false;
- context::CDO<bool> d_modelBuilt;
mutable std::hash_map<Node, Node, NodeHashFunction> d_modelCache;
protected:
@@ -62,6 +62,8 @@ protected:
*/
Node getModelValue(TNode n, bool hasBoundVars = false, bool useDontCares = false) const;
public:
+ /** is built */
+ bool isBuilt() { return d_modelBuilt.get(); }
/**
* Get value function. This should be called only after a ModelBuilder has called buildModel(...)
* on this model.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback