diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-24 18:34:25 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-24 18:34:25 +0200 |
| commit | d7dc7c2b3038b862af5ea55e7cf6b1fc4e1fe684 (patch) | |
| tree | d6c229a2659bfcb3cdf7c7c786414ecc1e59e61c /src/theory/quantifiers_engine.cpp | |
| parent | 1ec95c559074ed7575a0165deb16fcee45920e9f (diff) | |
Improvements to vts in cbqi, bug fix vts for non-atomic terms containing vts symbols. Move presolve for sygus to cbqi. Enable --cbqi-recurse by default, add option --cbqi-min-bound. Enable qcf for finite model finding by default.
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index d1a268950..ca16d2ab1 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -620,9 +620,9 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std //do virtual term substitution if( doVts ){ body = Rewriter::rewrite( body ); - Trace("inst-debug") << "Rewrite vts symbols in " << body << std::endl; + Trace("quant-vts-debug") << "Rewrite vts symbols in " << body << std::endl; Node body_r = d_term_db->rewriteVtsSymbols( body ); - Trace("inst-debug") << " ...result: " << body_r << std::endl; + Trace("quant-vts-debug") << " ...result: " << body_r << std::endl; body = body_r; } Trace("inst-assert") << "(assert " << body << ")" << std::endl; @@ -804,15 +804,15 @@ bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq, b bool QuantifiersEngine::addLemma( Node lem, bool doCache ){ if( doCache ){ lem = Rewriter::rewrite(lem); - Trace("inst-add-debug2") << "Adding lemma : " << lem << std::endl; + Trace("inst-add-debug") << "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 ); - Trace("inst-add-debug2") << "Added lemma" << std::endl; + Trace("inst-add-debug") << "Added lemma" << std::endl; return true; }else{ - Trace("inst-add-debug2") << "Duplicate." << std::endl; + Trace("inst-add-debug") << "Duplicate." << std::endl; return false; } }else{ |