diff options
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 19 |
1 files changed, 8 insertions, 11 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index cb7a4d055..2e69080e7 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -217,7 +217,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, if (options::sygus() || options::sygusInst()) { d_sygus_tdb.reset(new quantifiers::TermDbSygus(c, this)); - } + } d_util.push_back(d_instantiate.get()); @@ -580,7 +580,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ if( d_hasAddedLemma ){ return; } - + double clSet = 0; if( Trace.isOn("quant-engine") ){ clSet = double(clock())/double(CLOCKS_PER_SEC); @@ -805,7 +805,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ Trace("quant-engine") << ", added lemma = " << d_hasAddedLemma; Trace("quant-engine") << std::endl; } - + Trace("quant-engine-debug2") << "Finished quantifiers engine check." << std::endl; }else{ Trace("quant-engine-debug2") << "Quantifiers Engine does not need check." << std::endl; @@ -1035,7 +1035,7 @@ bool QuantifiersEngine::removeLemma( Node lem ) { void QuantifiersEngine::addRequirePhase( Node lit, bool req ){ d_phase_req_waiting[lit] = req; } - + void QuantifiersEngine::markRelevant( Node q ) { d_model->markRelevant( q ); } @@ -1048,9 +1048,10 @@ bool QuantifiersEngine::theoryEngineNeedsCheck() const return d_te->needCheck(); } -void QuantifiersEngine::setConflict() { - d_conflict = true; - d_conflict_c = true; +void QuantifiersEngine::setConflict() +{ + d_conflict = true; + d_conflict_c = true; } bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) { @@ -1123,10 +1124,6 @@ bool QuantifiersEngine::getUnsatCoreLemmas( std::vector< Node >& active_lemmas ) return d_instantiate->getUnsatCoreLemmas(active_lemmas); } -bool QuantifiersEngine::getUnsatCoreLemmas( std::vector< Node >& active_lemmas, std::map< Node, Node >& weak_imp ) { - return d_instantiate->getUnsatCoreLemmas(active_lemmas, weak_imp); -} - void QuantifiersEngine::getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ) { d_instantiate->getInstantiationTermVectors(q, tvecs); } |