diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-07-25 16:40:54 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-07-25 16:40:54 +0200 |
| commit | c0079b3110a81f2ff993b7f86782266380dd102e (patch) | |
| tree | c39d61ecc3857ebe5af75bd41ef7c11353e0824a /src/smt | |
| parent | 7dcb635088e73b508dbe00ae7fe08dae99968416 (diff) | |
Add option --sygus-inv-templ for synthesizing strengthening/weakening of pre/post conditions. Dump synth by default in sygus, update regressions. Set better defaults for induction. Fix bug in related to IFF and EQUAL in sygus grammar.
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/options | 2 | ||||
| -rw-r--r-- | src/smt/smt_engine.cpp | 7 |
2 files changed, 8 insertions, 1 deletions
diff --git a/src/smt/options b/src/smt/options index 077acc6e9..7c725e508 100644 --- a/src/smt/options +++ b/src/smt/options @@ -37,7 +37,7 @@ 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 -option dumpSynth --dump-synth bool :default false +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 CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" turn on unsat core generation diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 921583ed2..fa145813c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1465,6 +1465,13 @@ void SmtEngine::setDefaults() { if( !options::dtForceAssignment.wasSetByUser() ){ options::dtForceAssignment.set( true ); } + //try to remove ITEs from quantified formulas + if( !options::iteDtTesterSplitQuant.wasSetByUser() ){ + options::iteDtTesterSplitQuant.set( true ); + } + if( !options::iteLiftQuant.wasSetByUser() ){ + options::iteLiftQuant.set( quantifiers::ITE_LIFT_QUANT_MODE_ALL ); + } } if( options::intWfInduction() ){ if( !options::purifyTriggers.wasSetByUser() ){ |