From 32b0aba2c2c27ad038d34c8554a4bae76e8dd363 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 21 Nov 2014 09:42:07 +0100 Subject: Change default option to --inst-when=full-last-call (interleave instantiation and theory combination). Fix inefficiency in NNF, enable by default. Set best defaults for --mbqi=abs. --- src/smt/smt_engine.cpp | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) (limited to 'src/smt') diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 86b0faaf6..74cdee0b7 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1319,7 +1319,6 @@ void SmtEngine::setDefaults() { if( !options::quantConflictFind.wasSetByUser() ){ options::quantConflictFind.set( false ); } - //for finite model finding if( ! options::instWhenMode.wasSetByUser()){ //instantiate only on last call if( options::eMatching() ){ @@ -1327,6 +1326,14 @@ void SmtEngine::setDefaults() { options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL ); } } + if( options::mbqiMode()==quantifiers::MBQI_ABS ){ + if( !options::preSkolemQuant.wasSetByUser() ){ + options::preSkolemQuant.set( true ); + } + if( !options::fmfOneInstPerRound.wasSetByUser() ){ + options::fmfOneInstPerRound.set( true ); + } + } } //implied options... -- cgit v1.2.3