diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-06 17:04:52 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-06 17:04:52 -0500 |
commit | dd84403eb19b769d80b4c57ae690ba14c02df041 (patch) | |
tree | aa63f0f909ecd7063e38f7121c17cafb431abdf4 /src/theory | |
parent | c87ee73ad3d51c238700f236c18e425b80e8e7ac (diff) |
Minor clean up, fixes related to sygus.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/instantiation_engine.cpp | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/model_engine.cpp | 9 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 1 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.h | 4 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 2 |
7 files changed, 8 insertions, 20 deletions
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 955dc5d86..db597d031 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -137,11 +137,7 @@ void InstantiationEngine::check( Theory::Effort e, unsigned quant_e ){ doInstantiationRound( e ); if( d_quantEngine->inConflict() ){ Assert( d_quantEngine->getNumLemmasWaiting()>lastWaiting ); - Trace("inst-engine") << "Conflict = " << d_quantEngine->getNumLemmasWaiting() << " / " << d_quantEngine->getNumLemmasAddedThisRound(); - if( lastWaiting>0 ){ - Trace("inst-engine") << " (prev " << lastWaiting << ")"; - } - Trace("inst-engine") << std::endl; + Trace("inst-engine") << "Conflict, added lemmas = " << (d_quantEngine->getNumLemmasWaiting()-lastWaiting) << std::endl; }else if( d_quantEngine->hasAddedLemma() ){ Trace("inst-engine") << "Added lemmas = " << (d_quantEngine->getNumLemmasWaiting()-lastWaiting) << std::endl; } diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 0bbca88eb..3063e7a2f 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -221,11 +221,12 @@ int ModelEngine::checkModel(){ //print debug information if( d_quantEngine->inConflict() ){ - Trace("model-engine") << "Conflict = " << d_quantEngine->getNumLemmasWaiting() << " / " << d_quantEngine->getNumLemmasAddedThisRound() << std::endl; + Trace("model-engine") << "Conflict, added lemmas = "; }else{ - Trace("model-engine") << "Added Lemmas = " << d_addedLemmas << " / " << d_triedLemmas << " / "; - Trace("model-engine") << d_totalLemmas << std::endl; - } + Trace("model-engine") << "Added Lemmas = "; + } + Trace("model-engine") << d_addedLemmas << " / " << d_triedLemmas << " / "; + Trace("model-engine") << d_totalLemmas << std::endl; return d_addedLemmas; } diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 6963f7e62..e41dfc67a 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -230,7 +230,7 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) { ret = ret.negate(); status = REWRITE_AGAIN_FULL; }else if( in.getKind()==FORALL ){ - if( in[1].isConst() ){ + if( in[1].isConst() && in.getNumChildren()==2 ){ return RewriteResponse( status, in[1] ); }else{ //compute attributes diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 61c02d3ac..ae9426172 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -3111,6 +3111,7 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node > std::string name = std::string( str.begin() + found +1, str.end() ); out << name; }else{ + Trace("ajr-temp") << "[[print operator " << op << "]]" << std::endl; out << op; } if( n.getNumChildren()>0 ){ 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; } } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 60666c4a9..7522c633b 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -158,8 +158,6 @@ private: //this information is reset during check /** are we in conflict */ bool d_conflict; context::CDO< bool > d_conflict_c; - /** number of lemmas we actually added this round (for debugging) */ - unsigned d_num_added_lemmas_round; /** has added lemma this round */ bool d_hasAddedLemma; private: @@ -332,8 +330,6 @@ public: bool inConflict() { return d_conflict; } /** get number of waiting lemmas */ unsigned getNumLemmasWaiting() { return d_lemmas_waiting.size(); } - /** get number of waiting lemmas */ - unsigned getNumLemmasAddedThisRound() { return d_num_added_lemmas_round; } /** get needs check */ bool getInstWhenNeedsCheck( Theory::Effort e ); /** get user pat mode */ diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index b3e1925ae..93aedd17b 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -3275,11 +3275,9 @@ void TheoryStrings::separateByLength(std::vector< Node >& n, Assert( d_equalityEngine.getRepresentative(eqc)==eqc ); EqcInfo* ei = getOrMakeEqcInfo( eqc, false ); Node lt = ei ? ei->d_length_term : Node::null(); - Trace("ajr-temp") << "Length term for " << eqc << " is " << lt << std::endl; if( !lt.isNull() ){ lt = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt ); Node r = d_equalityEngine.getRepresentative( lt ); - Trace("ajr-temp") << "Length term rep for " << eqc << " is " << lt << std::endl; if( eqc_to_leqc.find( r )==eqc_to_leqc.end() ){ eqc_to_leqc[r] = leqc_counter; leqc_to_eqc[leqc_counter] = r; |