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.h8
1 files changed, 2 insertions, 6 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index fbd92bcf2..f5abda1b0 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -203,6 +203,8 @@ class CVC4_PUBLIC SmtEngine
* --sygus-abduct.
*/
void setIsInternalSubsolver();
+ /** Is this an internal subsolver? */
+ bool isInternalSubsolver() const;
/** set the input name */
void setFilename(std::string filename);
@@ -939,12 +941,6 @@ class CVC4_PUBLIC SmtEngine
void finalOptionsAreSet();
/**
- * Apply heuristics settings and other defaults. Done once, at
- * finishInit() time.
- */
- void setDefaults();
-
- /**
* Sets that the problem has been extended. This sets the smt mode of the
* solver to SMT_MODE_ASSERT, and clears the list of assumptions from the
* previous call to checkSatisfiability.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback