diff options
Diffstat (limited to 'src/util/options.h')
-rw-r--r-- | src/util/options.h | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/src/util/options.h b/src/util/options.h index 4bf8b5b75..c7fbcd896 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -156,7 +156,7 @@ struct CVC4_PUBLIC Options { /** Whether we produce proofs. */ bool proof; - + /** Whether we support SmtEngine::getAssignment() for this run. */ bool produceAssignments; @@ -195,7 +195,7 @@ struct CVC4_PUBLIC Options { /** Variable activity decay factor for Minisat */ double satVarDecay; - + /** Clause activity decay factor for Minisat */ double satClauseDecay; @@ -238,6 +238,12 @@ struct CVC4_PUBLIC Options { */ bool dioSolver; + /** + * Whether to split (= x y) into (and (<= x y) (>= x y)) in + * arithmetic preprocessing. + */ + bool arithRewriteEq; + /** The output channel to receive notfication events for new lemmas */ LemmaOutputChannel* lemmaOutputChannel; LemmaInputChannel* lemmaInputChannel; @@ -251,7 +257,7 @@ struct CVC4_PUBLIC Options { /** Thread ID, for internal use in case of multi-threaded run */ int thread_id; - /** + /** * In multi-threaded setting print output of each thread at the * end of run, separated by a divider ("----"). **/ |