summaryrefslogtreecommitdiff
path: root/src/theory/model.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/model.h')
-rw-r--r--src/theory/model.h2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/model.h b/src/theory/model.h
index 5581ce777..229d1f25e 100644
--- a/src/theory/model.h
+++ b/src/theory/model.h
@@ -247,12 +247,14 @@ protected:
TheoryEngine* d_te;
typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
NodeMap d_normalizedCache;
+ typedef std::hash_set<Node, NodeHashFunction> NodeSet;
/** process build model */
virtual void processBuildModel(TheoryModel* m, bool fullModel);
/** normalize representative */
Node normalize(TheoryModel* m, TNode r, std::map<Node, Node>& constantReps, bool evalOnly);
bool isAssignable(TNode n);
+ void checkTerms(TNode n, TheoryModel* tm, NodeSet& cache);
public:
TheoryEngineModelBuilder(TheoryEngine* te);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback