diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-18 17:39:05 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-18 17:39:14 +0100 |
commit | 3a2aed30267a33ff78006aec6a5b36aad96feb09 (patch) | |
tree | fa5a61a9c0e071c0d9d438de9150e3a90b4ff583 /src/smt | |
parent | d9923e1928a158c915a71ce0addb766a1e9986ca (diff) |
Add local theory extensions instantiation strategy (incomplete). Refactor how default options are set for quantifiers. Minor improvement to datatypes. Add unsat co-datatype regression. Clean up instantiation engine. Set inst level 0 on introduced constants for types with no ground terms. Return introduced constant for variable trigger when no ground terms exist.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 57 |
1 files changed, 37 insertions, 20 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index c87753d8d..a80177429 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1268,25 +1268,22 @@ void SmtEngine::setDefaults() { options::decisionMode.set(decMode); options::decisionStopOnly.set(stoponly); } - - //for finite model finding - if( ! options::instWhenMode.wasSetByUser()){ - //instantiate only on last call - if( options::fmfInstEngine() ){ - Trace("smt") << "setting inst when mode to LAST_CALL" << endl; - options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL ); + //local theory extensions + if( options::localTheoryExt() ){ + //no E-matching? + if( !options::instMaxLevel.wasSetByUser() ){ + options::instMaxLevel.set( 0 ); } } if( d_logic.hasCardinalityConstraints() ){ //must have finite model finding on options::finiteModelFind.set( true ); } - if( options::recurseCbqi() ){ - options::cbqi.set( true ); - } if(options::fmfBoundIntLazy.wasSetByUser() && options::fmfBoundIntLazy()) { options::fmfBoundInt.set( true ); } + //now have determined whether fmfBoundInt is on/off + //apply fmfBoundInt options if( options::fmfBoundInt() ){ //must have finite model finding on options::finiteModelFind.set( true ); @@ -1301,6 +1298,35 @@ void SmtEngine::setDefaults() { if( options::ufssSymBreak() ){ options::sortInference.set( true ); } + if( options::fmfFunWellDefined() ){ + if( !options::finiteModelFind.wasSetByUser() ){ + options::finiteModelFind.set( true ); + } + } + + //now, have determined whether finite model find is on/off + //apply finite model finding options + if( options::finiteModelFind() ){ + if( !options::eMatching.wasSetByUser() ){ + options::eMatching.set( options::fmfInstEngine() ); + } + if( !options::quantConflictFind.wasSetByUser() ){ + options::quantConflictFind.set( false ); + } + //for finite model finding + if( ! options::instWhenMode.wasSetByUser()){ + //instantiate only on last call + if( options::eMatching() ){ + Trace("smt") << "setting inst when mode to LAST_CALL" << endl; + options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL ); + } + } + } + + //implied options... + if( options::recurseCbqi() ){ + options::cbqi.set( true ); + } if( options::qcfMode.wasSetByUser() || options::qcfTConstraint() ){ options::quantConflictFind.set( true ); } @@ -1342,16 +1368,7 @@ void SmtEngine::setDefaults() { options::conjectureGen.set( false ); } } - if( options::fmfFunWellDefined() ){ - if( !options::finiteModelFind.wasSetByUser() ){ - options::finiteModelFind.set( true ); - } - } - if( options::finiteModelFind() ){ - if( !options::quantConflictFind.wasSetByUser() ){ - options::quantConflictFind.set( false ); - } - } + //until bugs 371,431 are fixed if( ! options::minisatUseElim.wasSetByUser()){ if( d_logic.isQuantified() || options::produceModels() || options::produceAssignments() || options::checkModels() ){ |