diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-11-09 21:57:06 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-11-09 21:57:06 +0000 |
commit | df5f7fe03fda041429548bcb39abb8916ca2e291 (patch) | |
tree | 46b08f3e35ee9c3d4c551d82f3e7e36582383f39 /src/util/options.h | |
parent | 1f07775e9205b3f9e172a1ad218a9015b7265b58 (diff) |
Lemmas on demand work, push-pop, some cleanup.
Diffstat (limited to 'src/util/options.h')
-rw-r--r-- | src/util/options.h | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/util/options.h b/src/util/options.h index 60c8f2a1a..1eca0d499 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -126,6 +126,9 @@ struct CVC4_PUBLIC Options { /** Whether we do typechecking at Expr creation time. */ bool earlyTypeChecking; + /** Whether incemental solving (push/pop) */ + bool incrementalSolving; + Options() : binary_name(), statistics(false), @@ -147,7 +150,8 @@ struct CVC4_PUBLIC Options { produceModels(false), produceAssignments(false), typeChecking(DO_SEMANTIC_CHECKS_BY_DEFAULT), - earlyTypeChecking(USE_EARLY_TYPE_CHECKING_BY_DEFAULT) { + earlyTypeChecking(USE_EARLY_TYPE_CHECKING_BY_DEFAULT), + incrementalSolving(false) { } /** |