Merge branch 'master' into bv-core

8 files changed, 62 insertions, 40 deletions

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 9edc77e39..43679113c 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -74,11 +74,12 @@ ostream& operator<<(ostream& out, const CommandStatus* s) throw() {
 
 /* class Command */
 
-Command::Command() throw() : d_commandStatus(NULL) {
+Command::Command() throw() : d_commandStatus(NULL), d_muted(false) {
 }
 
 Command::Command(const Command& cmd) {
   d_commandStatus = (cmd.d_commandStatus == NULL) ? NULL : &cmd.d_commandStatus->clone();
+  d_muted = cmd.d_muted;
 }
 
 Command::~Command() throw() {
@@ -98,7 +99,9 @@ bool Command::fail() const throw() {
 
 void Command::invoke(SmtEngine* smtEngine, std::ostream& out) throw() {
   invoke(smtEngine);
-  printResult(out);
+  if(!(isMuted() && ok())) {
+    printResult(out);
+  }
 }
 
 std::string Command::toString() const throw() {
diff --git a/src/expr/command.h b/src/expr/command.h
index 9877044fb..8e5983403 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -193,6 +193,12 @@ protected:
    */
   const CommandStatus* d_commandStatus;
 
+  /**
+   * True if this command is "muted"---i.e., don't print "success" on
+   * successful execution.
+   */
+  bool d_muted;
+
 public:
   typedef CommandPrintSuccess printsuccess;
 
@@ -210,6 +216,16 @@ public:
   std::string toString() const throw();
 
   /**
+   * If false, instruct this Command not to print a success message.
+   */
+  void setMuted(bool muted) throw() { d_muted = muted; }
+
+  /**
+   * Determine whether this Command will print a success message.
+   */
+  bool isMuted() throw() { return d_muted; }
+
+  /**
    * Either the command hasn't run yet, or it completed successfully
    * (CommandSuccess, not CommandUnsupported or CommandFailure).
    */
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index a390cf452..387a24fe1 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -952,6 +952,7 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr]
       std::string attr_name = attr;
       attr_name.erase( attr_name.begin() );
       Command* c = new SetUserAttributeCommand( attr_name, expr );
+      c->setMuted(true);
       PARSER_STATE->preemptCommand(c);
     } else {
       PARSER_STATE->attributeNotSupported(attr);
@@ -979,6 +980,7 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr]
       // bind name to expr with define-fun
       Command* c =
         new DefineNamedFunctionCommand(name, func, std::vector<Expr>(), expr);
+      c->setMuted(true);
       PARSER_STATE->preemptCommand(c);
     }
   ;
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index e1f977890..5d104531f 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -290,7 +290,9 @@ void Smt2::checkThatLogicIsSet() {
 
       setLogic("ALL_SUPPORTED");
 
-      preemptCommand(new SetBenchmarkLogicCommand("ALL_SUPPORTED"));
+      Command* c = new SetBenchmarkLogicCommand("ALL_SUPPORTED");
+      c->setMuted(true);
+      preemptCommand(c);
     }
   }
 }
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 823b61df5..ee9ff9e1b 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -86,7 +86,7 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){
   }else if(t.isVar()){
     return rewriteVariable(t);
   }else{
-    switch(t.getKind()){
+    switch(Kind k = t.getKind()){
     case kind::MINUS:
       return rewriteMinus(t, true);
     case kind::UMINUS:
@@ -104,7 +104,7 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){
     case kind::INTS_MODULUS_TOTAL:
       return rewriteIntsDivModTotal(t,true);
     default:
-      Unreachable();
+      Unhandled(k);
     }
   }
 }
diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp
index fd6f04ca8..9bd0a3b6c 100644
--- a/src/theory/arith/normal_form.cpp
+++ b/src/theory/arith/normal_form.cpp
@@ -28,8 +28,8 @@ namespace arith {
 bool Variable::isDivMember(Node n){
   switch(n.getKind()){
   case kind::DIVISION:
-    //case kind::INTS_DIVISION:
-    //case kind::INTS_MODULUS:
+  case kind::INTS_DIVISION:
+  case kind::INTS_MODULUS:
   case kind::DIVISION_TOTAL:
   case kind::INTS_DIVISION_TOTAL:
   case kind::INTS_MODULUS_TOTAL:
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 50c21a1e6..b2713d420 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -67,8 +67,8 @@ void EqualityEngine::init() {
   // QuantifiersEngine.AddTermToDatabase that try to access to the uf
   // instantiator that currently doesn't exist.
   ScopedBool sb(d_performNotify, false);
-  addTerm(d_true);
-  addTerm(d_false);
+  addTermInternal(d_true);
+  addTermInternal(d_false);
 
   d_trueId = getNodeId(d_true);
   d_falseId = getNodeId(d_false);  
@@ -233,13 +233,6 @@ void EqualityEngine::addFunctionKind(Kind fun, bool interpreted) {
   }
 }
 
-bool isOperator(TNode node) {
-  if (node.getKind() == kind::BUILTIN) {
-    return true;
-  }
-  return false;
-}
-
 void EqualityEngine::subtermEvaluates(EqualityNodeId id)  {
   Debug("equality::evaluation") << d_name << "::eq::subtermEvaluates(" << d_nodes[id] << "): " << d_subtermsToEvaluate[id] << std::endl;
   Assert(!d_isInternal[id]);
@@ -252,13 +245,13 @@ void EqualityEngine::subtermEvaluates(EqualityNodeId id)  {
   Debug("equality::evaluation") << d_name << "::eq::subtermEvaluates(" << d_nodes[id] << "): new " << d_subtermsToEvaluate[id] << std::endl;
 }
 
-void EqualityEngine::addTerm(TNode t) {
+void EqualityEngine::addTermInternal(TNode t, bool isOperator) {
 
-  Debug("equality") << d_name << "::eq::addTerm(" << t << ")" << std::endl;
+  Debug("equality") << d_name << "::eq::addTermInternal(" << t << ")" << std::endl;
 
   // If there already, we're done
   if (hasTerm(t)) {
-    Debug("equality") << d_name << "::eq::addTerm(" << t << "): already there" << std::endl;
+    Debug("equality") << d_name << "::eq::addTermInternal(" << t << "): already there" << std::endl;
     return;
   }
 
@@ -269,23 +262,23 @@ void EqualityEngine::addTerm(TNode t) {
   EqualityNodeId result;
 
   if (t.getKind() == kind::EQUAL) {
-    addTerm(t[0]);
-    addTerm(t[1]);
+    addTermInternal(t[0]);
+    addTermInternal(t[1]);
     EqualityNodeId t0id = getNodeId(t[0]);
     EqualityNodeId t1id = getNodeId(t[1]);
     result = newApplicationNode(t, t0id, t1id, APP_EQUALITY);
     d_isInternal[result] = false;
+    d_isConstant[result] = false;
   } else if (t.getNumChildren() > 0 && d_congruenceKinds[t.getKind()]) {
     TNode tOp = t.getOperator();
     // Add the operator
-    addTerm(tOp);
+    addTermInternal(tOp, true);
     result = getNodeId(tOp);
-    d_isInternal[result] = true;
     // Add all the children and Curryfy
     bool isInterpreted = isInterpretedFunctionKind(t.getKind());
     for (unsigned i = 0; i < t.getNumChildren(); ++ i) {
       // Add the child
-      addTerm(t[i]);
+      addTermInternal(t[i]);
       EqualityNodeId tiId = getNodeId(t[i]);
       // Add the application
       result = newApplicationNode(t, result, tiId, isInterpreted ? APP_INTERPRETED : APP_UNINTERPRETED);
@@ -298,7 +291,7 @@ void EqualityEngine::addTerm(TNode t) {
       d_subtermsToEvaluate[result] = t.getNumChildren();
       for (unsigned i = 0; i < t.getNumChildren(); ++ i) {
 	if (isConstant(getNodeId(t[i]))) {
-	  Debug("equality::evaluation") << d_name << "::eq::addTerm(" << t << "): evaluatates " << t[i] << std::endl;
+	  Debug("equality::evaluation") << d_name << "::eq::addTermInternal(" << t << "): evaluatates " << t[i] << std::endl;
 	  subtermEvaluates(result);
 	}
       }
@@ -307,8 +300,8 @@ void EqualityEngine::addTerm(TNode t) {
     // Otherwise we just create the new id
     result = newNode(t);
     // Is this an operator
-    d_isInternal[result] = false;
-    d_isConstant[result] = t.isConst() && !isOperator(t);
+    d_isInternal[result] = isOperator;
+    d_isConstant[result] = !isOperator && t.isConst();
   }
 
   if (t.getType().isBoolean()) {
@@ -333,7 +326,7 @@ void EqualityEngine::addTerm(TNode t) {
 
   // If this is not an internal node, add it to the master
   if (d_masterEqualityEngine && !d_isInternal[result]) {
-    d_masterEqualityEngine->addTerm(t);
+    d_masterEqualityEngine->addTermInternal(t);
   }
 
   // Empty the queue
@@ -341,7 +334,7 @@ void EqualityEngine::addTerm(TNode t) {
 
   Assert(hasTerm(t));
   
-  Debug("equality") << d_name << "::eq::addTerm(" << t << ") => " << result << std::endl;
+  Debug("equality") << d_name << "::eq::addTermInternal(" << t << ") => " << result << std::endl;
 }
 
 bool EqualityEngine::hasTerm(TNode t) const {
@@ -380,8 +373,8 @@ void EqualityEngine::assertEqualityInternal(TNode t1, TNode t2, TNode reason) {
   }
 
   // Add the terms if they are not already in the database
-  addTerm(t1);
-  addTerm(t2);
+  addTermInternal(t1);
+  addTermInternal(t2);
 
   // Add to the queue and propagate
   EqualityNodeId t1Id = getNodeId(t1);
@@ -496,6 +489,7 @@ TNode EqualityEngine::getRepresentative(TNode t) const {
   Debug("equality::internal") << d_name << "::eq::getRepresentative(" << t << ")" << std::endl;
   Assert(hasTerm(t));
   EqualityNodeId representativeId = getEqualityNode(t).getFind();
+  Assert(!d_isInternal[representativeId]);
   Debug("equality::internal") << d_name << "::eq::getRepresentative(" << t << ") => " << d_nodes[representativeId] << std::endl;
   return d_nodes[representativeId];
 }
@@ -609,7 +603,7 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
         Debug("equality") << d_name << "::eq::merge(" << class1.getFind() << "," << class2.getFind() << "): " << d_nodes[currentId] << " in " << d_nodes[funId] << std::endl;
         const FunctionApplication& fun = d_applications[useNode.getApplicationId()].normalized;
         // If it's interpreted and we can interpret
-	if (fun.isInterpreted() && class1isConstant && !d_isInternal[class2Id]) {
+	if (fun.isInterpreted() && class1isConstant && !d_isInternal[funId]) {
 	  // Get the actual term id 
 	  TNode term = d_nodes[useNode.getApplicationId()];
 	  subtermEvaluates(getNodeId(term));
@@ -1090,8 +1084,8 @@ void EqualityEngine::addTriggerEquality(TNode eq) {
   }
 
   // Add the terms
-  addTerm(eq[0]);
-  addTerm(eq[1]);
+  addTermInternal(eq[0]);
+  addTermInternal(eq[1]);
 
   bool skipTrigger = false;
 
@@ -1110,7 +1104,7 @@ void EqualityEngine::addTriggerEquality(TNode eq) {
   }
 
   // Add the equality
-  addTerm(eq);
+  addTermInternal(eq);
 
   // Positive trigger
   addTriggerEqualityInternal(eq[0], eq[1], eq, true);
@@ -1127,7 +1121,7 @@ void EqualityEngine::addTriggerPredicate(TNode predicate) {
   }
 
   // Add the term
-  addTerm(predicate);
+  addTermInternal(predicate);
 
   bool skipTrigger = false;
 
@@ -1231,7 +1225,7 @@ void EqualityEngine::processEvaluationQueue() {
     Node nodeEvaluated = evaluateTerm(d_nodes[id]);
     Debug("equality::evaluation") << d_name << "::eq::processEvaluationQueue(): " << d_nodes[id] << " evaluates to " << nodeEvaluated << std::endl;
     Assert(nodeEvaluated.isConst());
-    addTerm(nodeEvaluated);
+    addTermInternal(nodeEvaluated);
     EqualityNodeId nodeEvaluatedId = getNodeId(nodeEvaluated);
 
     // Enqueue the semantic equality
@@ -1524,7 +1518,7 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const
 size_t EqualityEngine::getSize(TNode t)
 {
   // Add the term
-  addTerm(t);
+  addTermInternal(t);
   return getEqualityNode(getEqualityNode(t).getFind()).getSize();
 }
 
@@ -1540,7 +1534,7 @@ void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag)
   }
 
   // Add the term if it's not already there
-  addTerm(t);
+  addTermInternal(t);
 
   // Get the node id
   EqualityNodeId eqNodeId = getNodeId(t);
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 0a5d70a9c..2373c7f9a 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -702,12 +702,17 @@ private:
   /** Name of the equality engine */
   std::string d_name;
 
+  /** The internal addTerm */
+  void addTermInternal(TNode t, bool isOperator = false);
+
 public:
 
   /**
    * Adds a term to the term database.
    */
-  void addTerm(TNode t);
+  void addTerm(TNode t) {
+    addTermInternal(t, false);
+  }
 
   /**
    * Add a kind to treat as function applications.