diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-03 15:36:38 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-11-03 15:36:38 -0500 |
| commit | 5cafed748989602263b8ad1a27ac6b9bd159a441 (patch) | |
| tree | b0e474f47251d480dce48637e73f663aba0dd179 /src/options/smt_options | |
| parent | 3f2c2c745ae2f13441c1cabd363e6539c9bdaeb9 (diff) | |
Sygus clean main (#1297)
* Remove front end hack for sygus.
* Remove other hack, add sygus solution output mode.
* Clang format
* Minor
* Fix
* Minor
* Remove unused field.
Diffstat (limited to 'src/options/smt_options')
| -rw-r--r-- | src/options/smt_options | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/options/smt_options b/src/options/smt_options index 00424e103..c701d5c20 100644 --- a/src/options/smt_options +++ b/src/options/smt_options @@ -39,6 +39,8 @@ option dumpProofs --dump-proofs bool :default false :link --proof :link-smt prod output proofs after every UNSAT/VALID response option dumpInstantiations --dump-instantiations bool :default false output instantiations of quantified formulas after every UNSAT/VALID response +option sygusOut --sygus-out=MODE SygusSolutionOutMode :default SYGUS_SOL_OUT_STATUS_AND_DEF :include "options/sygus_out_mode.h" :handler stringToSygusSolutionOutMode :read-write + output mode for sygus option dumpSynth --dump-synth bool :read-write :default false output solution for synthesis conjectures after every UNSAT/VALID response option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate proofEnabledBuild :notify :notify notifyBeforeSearch |