diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-04-01 13:09:49 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-04-01 13:11:13 +0200 |
commit | 3ac872f4a3f65bd1b38c1362b8ca9d351ed89333 (patch) | |
tree | c62a424af1b419155af0f59612d376fc10e7a6b6 /src/theory/quantifiers_engine.cpp | |
parent | 9350915de95c1b569eea8262c4602708dfa6c3fa (diff) |
Improvements and bug fixes related to cbqi/cegqi. Minor fix for fmf with fun-def. Add skolemization options.
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 31 |
1 files changed, 17 insertions, 14 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 888cdbce0..ba75af873 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -417,7 +417,7 @@ bool QuantifiersEngine::registerQuantifier( Node f ){ Trace("quant") << " : " << f << std::endl; ++(d_statistics.d_num_quant); Assert( f.getKind()==FORALL ); - + //check whether we should apply a reduction bool reduced = false; if( d_lte_part_inst && !f.getAttribute(LtePartialInstAttribute()) ){ @@ -567,7 +567,7 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std Trace("inst") << std::endl; Assert( terms[i].getType().isSubtypeOf( f[0][i].getType() ) ); } - if( options::cbqi() ){ + if( options::cbqi() && !options::cbqi2() ){ for( int i=0; i<(int)terms.size(); i++ ){ if( quantifiers::TermDb::hasInstConstAttr(terms[i]) ){ Debug("inst")<< "***& Bad Instantiate " << f << " with " << std::endl; @@ -589,7 +589,6 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std } setInstantiationLevelAttr( body, f[1], maxInstLevel+1 ); } - Trace("inst-debug") << "*** Lemma is " << lem << std::endl; ++(d_statistics.d_instantiations); return true; }else{ @@ -673,13 +672,17 @@ Node QuantifiersEngine::getInstantiation( Node f, std::vector< Node >& vars, std Trace("partial-inst") << "Partial instantiation : " << f << std::endl; Trace("partial-inst") << " : " << body << std::endl; }else{ - //do optimized version - Node icb = d_term_db->getInstConstantBody( f ); - body = getSubstitute( icb, terms ); - if( Debug.isOn("check-inst") ){ - Node body2 = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); - if( body!=body2 ){ - Debug("check-inst") << "Substitution is wrong : " << body << " " << body2 << std::endl; + if( options::cbqi() ){ + body = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); + }else{ + //do optimized version + Node icb = d_term_db->getInstConstantBody( f ); + body = getSubstitute( icb, terms ); + if( Debug.isOn("check-inst") ){ + Node body2 = f[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); + if( body!=body2 ){ + Debug("check-inst") << "Substitution is wrong : " << body << " " << body2 << std::endl; + } } } } @@ -722,16 +725,16 @@ bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq, b bool QuantifiersEngine::addLemma( Node lem, bool doCache ){ if( doCache ){ - Debug("inst-engine-debug") << "Adding lemma : " << lem << std::endl; lem = Rewriter::rewrite(lem); + Trace("inst-add-debug2") << "Adding lemma : " << lem << std::endl; if( d_lemmas_produced_c.find( lem )==d_lemmas_produced_c.end() ){ //d_curr_out->lemma( lem, false, true ); d_lemmas_produced_c[ lem ] = true; d_lemmas_waiting.push_back( lem ); - Debug("inst-engine-debug") << "Added lemma : " << lem << std::endl; + Trace("inst-add-debug2") << "Added lemma : " << lem << std::endl; return true; }else{ - Debug("inst-engine-debug") << "Duplicate." << std::endl; + Trace("inst-add-debug2") << "Duplicate." << std::endl; return false; } }else{ @@ -943,7 +946,7 @@ void QuantifiersEngine::printSynthSolution( std::ostream& out ) { out << "Internal error : module for synth solution not found." << std::endl; } } - + QuantifiersEngine::Statistics::Statistics(): d_num_quant("QuantifiersEngine::Num_Quantifiers", 0), d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0), |