diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-08-22 16:59:28 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-08-22 17:58:14 -0400 |
| commit | 2dbe1f150d30f0fb0c8522f891104270ce09db4c (patch) | |
| tree | 1305f3de890f4353c3b5695a93ab7e2419760617 /src/smt/options | |
| parent | 4ec2c8eb8b8a50dc743119100767e101f19305f6 (diff) | |
Unsat core infrastruture and API (SMT-LIB compliance to come).
Diffstat (limited to 'src/smt/options')
| -rw-r--r-- | src/smt/options | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/smt/options b/src/smt/options index 9c7eea12f..3ee3dbecb 100644 --- a/src/smt/options +++ b/src/smt/options @@ -37,9 +37,11 @@ option dumpProofs --dump-proofs bool :default false :link --proof output proofs after every UNSAT/VALID response option dumpInstantiations --dump-instantiations bool :default false output instantiations of quantified formulas after every UNSAT/VALID response -# this is just a placeholder for later; it doesn't show up in command-line options listings -undocumented-option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate CVC4::smt::unsatCoresEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" - turn on unsat core generation (NOT YET SUPPORTED) +option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" + turn on unsat core generation +option dumpUnsatCores --dump-unsat-cores bool :default false :link --produce-unsat-cores :link-smt produce-unsat-cores :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" + output unsat cores after every UNSAT/VALID response + option produceAssignments produce-assignments --produce-assignments bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" support the get-assignment command |