summaryrefslogtreecommitdiff
path: root/src/smt/smt_engine.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt/smt_engine.h')
-rw-r--r--src/smt/smt_engine.h9
1 files changed, 9 insertions, 0 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 11f3bdcb9..ae9caf0eb 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -197,10 +197,19 @@ class CVC4_PUBLIC SmtEngine {
* as often as you like. Should be called whenever the final options
* and logic for the problem are set (at least, those options that are
* not permitted to change after assertions and queries are made).
+ *
+ * FIXME: Above comment not true. Please don't call this more than
+ * once. (6/14/2012 -- K)
*/
void finalOptionsAreSet();
/**
+ * Create theory engine, prop engine, decision engine. Called by
+ * finalOptionsAreSet()
+ */
+ void finishInit();
+
+ /**
* This is called by the destructor, just before destroying the
* PropEngine, TheoryEngine, and DecisionEngine (in that order). It
* is important because there are destruction ordering issues
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback