summaryrefslogtreecommitdiff
path: root/src/theory/theory_model.h
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2016-02-08 15:49:14 -0600
committerajreynol <andrew.j.reynolds@gmail.com>2016-02-08 15:50:20 -0600
commit2dd6292b73e4e19be2e261c7fe5664bd2b0149bd (patch)
tree0f4956ec068972da8c8d1c708df7c8b2f7a07f3a /src/theory/theory_model.h
parent3c4c4420ebae4d27d53084453591363942eb4d2e (diff)
Updates related to finite model finding and (co)datatypes. Bug fix enumerator and codatatype rewriter, further simplify fmc.
Diffstat (limited to 'src/theory/theory_model.h')
-rw-r--r--src/theory/theory_model.h1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index 4b27aeacb..b0952538a 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -255,6 +255,7 @@ protected:
typedef std::hash_set<Node, NodeHashFunction> NodeSet;
/** process build model */
+ virtual void preProcessBuildModel(TheoryModel* m, bool fullModel);
virtual void processBuildModel(TheoryModel* m, bool fullModel);
/** normalize representative */
Node normalize(TheoryModel* m, TNode r, std::map<Node, Node>& constantReps, bool evalOnly);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback