Minor cleanup of sources

diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index e3bc506e2c96bc461453890c2b85281d10318bd5..fca79aff073f906bad6359ee45e8b6b9f57c65bc 100644 (file)
--- 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 baf498968f662ba06307aa3a834259e404162bce..352868f7b80fb191a2d074900dc20f945fa1776b 100644 (file)
--- 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 01fbda51ed979ca3e455abd65ea4735064f057a5..490c8f1003950b41fded712b2670158fc3d13e5d 100644 (file)
--- 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 b41089b80324d9d53bd58d24e5daed7a4283717a..61b7209f6c317c273c5701f8ea7771323fbc759e 100644 (file)
--- 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;