From 7f10c78f572debd0ddf717bfb9f9453a42c015cb Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 17 Oct 2012 02:59:07 +0000 Subject: first working version of new inst-gen-style quantifier instantiation technique for fmf (--fmf-new-inst-gen), minor cleanup --- src/theory/quantifiers_engine.cpp | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'src/theory/quantifiers_engine.cpp') diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 9d7c8e315..4ba5c39e6 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -97,17 +97,17 @@ void QuantifiersEngine::check( Theory::Effort e ){ d_hasAddedLemma = false; if( e==Theory::EFFORT_LAST_CALL ){ + //if effort is last call, try to minimize model first + if( options::finiteModelFind() ){ + //first, check if we can minimize the model further + if( !((uf::TheoryUF*)getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->minimize() ){ + return; + } + } ++(d_statistics.d_instantiation_rounds_lc); }else if( e==Theory::EFFORT_FULL ){ ++(d_statistics.d_instantiation_rounds); } - //if effort is last call, try to minimize model first - if( e==Theory::EFFORT_LAST_CALL && options::finiteModelFind() ){ - //first, check if we can minimize the model further - if( !((uf::TheoryUF*)getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->minimize() ){ - return; - } - } for( int i=0; i<(int)d_modules.size(); i++ ){ d_modules[i]->check( e ); } -- cgit v1.2.3