diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-22 14:25:59 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-11-22 14:25:59 -0600 |
commit | 20704741e4609055d61e010b6981c6916d28019a (patch) | |
tree | a8e8beec06083b91c2336e3013538e86eb177a29 /src/options/smt_options | |
parent | 047b8f69db1ab46ad68a2693565066f2a8d40b29 (diff) |
Sygus Lambda Grammars (#1390)
Diffstat (limited to 'src/options/smt_options')
-rw-r--r-- | src/options/smt_options | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/options/smt_options b/src/options/smt_options index c701d5c20..fa6c3ae4e 100644 --- a/src/options/smt_options +++ b/src/options/smt_options @@ -40,7 +40,9 @@ option dumpProofs --dump-proofs bool :default false :link --proof :link-smt prod 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 + output mode for sygus +option sygusPrintCallbacks --sygus-print-callbacks bool :default true + use sygus print callbacks to print sygus terms in the user-provided form (disable for debugging) 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 |