diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-18 10:06:49 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-18 10:06:49 -0500 |
commit | 2e02c1c2fb999f2f1cdefe867f843c2c46ad0ef0 (patch) | |
tree | e9234dd807818316a9029cab5badc62b6874fa67 /src/smt | |
parent | 8768c1079798599bbe27b29bc49087d45857a112 (diff) |
Refactor modes for sygus+single invocation. Add option --inst-rlv-cond. Minor fixes for inst max level.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 14 |
1 files changed, 10 insertions, 4 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 54deba78c..62afbf987 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1737,6 +1737,10 @@ void SmtEngine::setDefaults() { options::instMaxLevel.set( 0 ); } } + if( options::instMaxLevel()!=-1 ){ + Notice() << "SmtEngine: turning off cbqi to support instMaxLevel" << endl; + options::cbqi.set(false); + } if(options::fmfBoundIntLazy.wasSetByUser() && options::fmfBoundIntLazy()) { options::fmfBoundInt.set( true ); @@ -1797,13 +1801,15 @@ void SmtEngine::setDefaults() { } //apply counterexample guided instantiation options - if( options::cegqiSingleInv() ){ - options::ceGuidedInst.set( true ); + if( options::cegqiSingleInvMode()!=quantifiers::CEGQI_SI_MODE_NONE ){ + if( !options::ceGuidedInst.wasSetByUser() ){ + options::ceGuidedInst.set( true ); + } } if( options::ceGuidedInst() ){ //counterexample-guided instantiation for sygus - if( !options::cegqiSingleInv.wasSetByUser() ){ - options::cegqiSingleInv.set( true ); + if( !options::cegqiSingleInvMode.wasSetByUser() ){ + options::cegqiSingleInvMode.set( quantifiers::CEGQI_SI_MODE_USE ); } if( !options::quantConflictFind.wasSetByUser() ){ options::quantConflictFind.set( false ); |