From dd84403eb19b769d80b4c57ae690ba14c02df041 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 6 May 2016 17:04:52 -0500 Subject: Minor clean up, fixes related to sygus. --- src/theory/quantifiers_engine.cpp | 4 ---- 1 file changed, 4 deletions(-) (limited to 'src/theory/quantifiers_engine.cpp') diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 12edb5277..afb7aeb92 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -89,7 +89,6 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* d_tr_trie = new inst::TriggerTrie; d_curr_effort_level = QEFFORT_NONE; d_conflict = false; - d_num_added_lemmas_round = 0; d_hasAddedLemma = false; //don't add true lemma d_lemmas_produced_c[d_term_db->d_true] = true; @@ -367,7 +366,6 @@ void QuantifiersEngine::check( Theory::Effort e ){ } d_conflict = false; - d_num_added_lemmas_round = 0; d_hasAddedLemma = false; bool setIncomplete = false; if( e==Theory::EFFORT_LAST_CALL ){ @@ -969,7 +967,6 @@ bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){ d_lemmas_produced_c[ lem ] = true; d_lemmas_waiting.push_back( lem ); Trace("inst-add-debug") << "Added lemma" << std::endl; - d_num_added_lemmas_round++; return true; }else{ Trace("inst-add-debug") << "Duplicate." << std::endl; @@ -978,7 +975,6 @@ bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){ }else{ //do not need to rewrite, will be rewritten after sending d_lemmas_waiting.push_back( lem ); - d_num_added_lemmas_round++; return true; } } -- cgit v1.2.3