Minor clean up, fixes related to sygus.

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;