Minor cleanup of sources

4 files changed, 1 insertions, 17 deletions

diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index e3bc506e2..fca79aff0 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -343,7 +343,6 @@ typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule
 typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule
 typerule SEXPR ::CVC4::theory::builtin::SExprTypeRule
 typerule LAMBDA ::CVC4::theory::builtin::LambdaTypeRule
-construle LAMBDA ::CVC4::theory::builtin::LambdaTypeRule
 typerule CHAIN ::CVC4::theory::builtin::ChainTypeRule
 
 constant SUBTYPE_TYPE \
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index baf498968..352868f7b 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -170,11 +170,6 @@ public:
     TypeNode rangeType = n[1].getType(check);
     return nodeManager->mkFunctionType(argTypes, rangeType);
   }
-
-  inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
-    Assert(n.getKind() == kind::LAMBDA);
-    return false;
-  }
 };/* class LambdaTypeRule */
 
 class ChainTypeRule {
diff --git a/src/theory/rewriterules/kinds b/src/theory/rewriterules/kinds
index 01fbda51e..490c8f100 100644
--- a/src/theory/rewriterules/kinds
+++ b/src/theory/rewriterules/kinds
@@ -23,7 +23,7 @@ sort RRHB_TYPE \
 # operators...
 
 # variables, guards, RR_REWRITE/REDUCTION_RULE/DEDUCTION_RULE
-operator REWRITE_RULE 3 "generale rewrite rule"
+operator REWRITE_RULE 3 "general rewrite rule"
 #HEAD/BODY/TRIGGER
 operator RR_REWRITE 2:3 "actual rewrite rule"
 operator RR_REDUCTION 2:3 "actual reduction rule"
diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp
index b41089b80..61b7209f6 100644
--- a/src/theory/term_registration_visitor.cpp
+++ b/src/theory/term_registration_visitor.cpp
@@ -171,9 +171,6 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const {
   TheoryId parentTheoryId  = Theory::theoryOf(parent);
 
   // Should we use the theory of the type
-#if 0
-  bool useType = current != parent && currentTheoryId != parentTheoryId;
-#else
   bool useType = false;
   TheoryId typeTheoryId = THEORY_LAST;
 
@@ -199,12 +196,10 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const {
       }
     }
   }
-#endif
 
   if (Theory::setContains(currentTheoryId, theories)) {
       if (Theory::setContains(parentTheoryId, theories)) {
         if (useType) {
-          ////TheoryId typeTheoryId = Theory::theoryOf(current.getType());
           return Theory::setContains(typeTheoryId, theories);
         } else {
           return true;
@@ -228,9 +223,6 @@ void SharedTermsVisitor::visit(TNode current, TNode parent) {
   TheoryId currentTheoryId = Theory::theoryOf(current);
   TheoryId parentTheoryId  = Theory::theoryOf(parent);
 
-#if 0
-  bool useType = current != parent && currentTheoryId != parentTheoryId;
-#else
   // Should we use the theory of the type
   bool useType = false;
   TheoryId typeTheoryId = THEORY_LAST;
@@ -257,7 +249,6 @@ void SharedTermsVisitor::visit(TNode current, TNode parent) {
       }
     }
   }
-#endif
 
   Theory::Set visitedTheories = d_visited[current];
   Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): previously registered with " << Theory::setToString(visitedTheories) << std::endl;
@@ -270,7 +261,6 @@ void SharedTermsVisitor::visit(TNode current, TNode parent) {
     Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl;
   }
   if (useType) {
-    //////TheoryId typeTheoryId = Theory::theoryOf(current.getType());
     if (!Theory::setContains(typeTheoryId, visitedTheories)) {
       visitedTheories = Theory::setInsert(typeTheoryId, visitedTheories);
       Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << typeTheoryId << std::endl;