diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-03-10 17:49:13 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-03-10 17:49:13 -0600 |
commit | d0df704a60696d7f824eb01781b413d91a0e4202 (patch) | |
tree | 501058c359ff029cad024a3a715efdf33968c426 /src/smt | |
parent | 346c85d145f6938ce7dce74e7e7cb855d5a6025a (diff) |
Faster conditional rewriting for and/or beneath quantifiers. Improvements to sort inference, related to constants. Add several quantifiers options, minor refactoring.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 27 |
1 files changed, 13 insertions, 14 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 201585070..93623408e 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1809,23 +1809,22 @@ void SmtEngine::setDefaults() { if( !options::rewriteDivk.wasSetByUser()) { options::rewriteDivk.set( true ); } - } - if( options::cbqi() && d_logic.isPure(THEORY_ARITH) ){ - options::cbqiAll.set( false ); - if( !options::quantConflictFind.wasSetByUser() ){ - options::quantConflictFind.set( false ); - } - if( !options::instNoEntail.wasSetByUser() ){ - options::instNoEntail.set( false ); - } - if( !options::instWhenMode.wasSetByUser() && options::cbqiModel() ){ - //only instantiation should happen at last call when model is avaiable - if( !options::instWhenMode.wasSetByUser() ){ - options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL ); + if( d_logic.isPure(THEORY_ARITH) ){ + options::cbqiAll.set( false ); + if( !options::quantConflictFind.wasSetByUser() ){ + options::quantConflictFind.set( false ); + } + if( !options::instNoEntail.wasSetByUser() ){ + options::instNoEntail.set( false ); + } + if( !options::instWhenMode.wasSetByUser() && options::cbqiModel() ){ + //only instantiation should happen at last call when model is avaiable + if( !options::instWhenMode.wasSetByUser() ){ + options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL ); + } } } } - //implied options... if( options::qcfMode.wasSetByUser() || options::qcfTConstraint() ){ options::quantConflictFind.set( true ); |