Fixes

yoni206 · Sep 28, 2023 · 84a64b4 · 84a64b4
1 parent 4b38f42
commit 84a64b4
Showing 1 changed file with 9 additions and 9 deletions.
diff --git a/src/rewriter/rewrite_db_proof_cons.cpp b/src/rewriter/rewrite_db_proof_cons.cpp
@@ -139,7 +139,7 @@ DslProofRule RewriteDbProofCons::proveInternal(Node eqi)
   // Otherwise, call the get matches routine. This will call notifyMatch below
   // for each matching rewrite rule conclusion in the database
   // decrease the recursion depth
-  Assert(eqi.getKind() == EQUAL);
+  Assert(eqi.getKind() == Kind::EQUAL);
   // first, try congruence if possible, which does not count towards recursion
   // limit.
   DslProofRule retId = proveInternalViaStrategy(eqi);
@@ -149,7 +149,7 @@ DslProofRule RewriteDbProofCons::proveInternal(Node eqi)
 
 DslProofRule RewriteDbProofCons::proveInternalViaStrategy(Node eqi)
 {
-  Assert(eqi.getKind() == EQUAL);
+  Assert(eqi.getKind() == Kind::EQUAL);
   if (proveWithRule(DslProofRule::CONG, eqi, {}, {}, false, false, true))
   {
     Trace("rpc-debug2") << "...proved via congruence" << std::endl;
@@ -214,7 +214,7 @@ bool RewriteDbProofCons::notifyMatch(Node s,
                       << std::endl;
   Trace("rpc-debug2") << "notifyMatch: " << s << " from " << n << " via "
                       << vars << " -> " << subs << std::endl;
-  Assert(d_target.getKind() == EQUAL);
+  Assert(d_target.getKind() == Kind::EQUAL);
   Assert(s.getType().isComparableTo(n.getType()));
   Assert(vars.size() == subs.size());
   if (d_currFixedPointId != DslProofRule::FAIL)
@@ -273,7 +273,7 @@ bool RewriteDbProofCons::proveWithRule(DslProofRule id,
                                        bool doFixedPoint,
                                        bool doRecurse)
 {
-  Assert(!target.isNull() && target.getKind() == EQUAL);
+  Assert(!target.isNull() && target.getKind() == Kind::EQUAL);
   Trace("rpc-debug2") << "Check rule " << id << std::endl;
   std::vector<Node> vcs;
   Node transEq;
@@ -514,7 +514,7 @@ bool RewriteDbProofCons::proveWithRule(DslProofRule id,
 bool RewriteDbProofCons::proveInternalBase(Node eqi, DslProofRule& idb)
 {
   Trace("rpc-debug2") << "Prove internal base: " << eqi << std::endl;
-  Assert(eqi.getKind() == kind::EQUAL);
+  Assert(eqi.getKind() == Kind::EQUAL);
   // if we are currently trying to prove this, fail
   if (d_currProving.find(eqi) != d_currProving.end())
   {
@@ -672,7 +672,7 @@ bool RewriteDbProofCons::ensureProofInternal(CDProof* cdp, Node eqi)
     visit.pop_back();
     it = visited.find(cur);
     itd = d_pcache.find(cur);
-    Assert(cur.getKind() == kind::EQUAL);
+    Assert(cur.getKind() == Kind::EQUAL);
     if (it == visited.end())
     {
       Trace("rpc-debug") << "Ensure proof for " << cur << std::endl;
@@ -698,7 +698,7 @@ bool RewriteDbProofCons::ensureProofInternal(CDProof* cdp, Node eqi)
         {
           visited[cur] = true;
           // NOTE: this could just evaluate the equality itself
-          Assert(cur.getKind() == kind::EQUAL);
+          Assert(cur.getKind() == Kind::EQUAL);
           std::vector<Node> transc;
           for (unsigned i = 0; i < 2; i++)
           {
@@ -809,7 +809,7 @@ bool RewriteDbProofCons::ensureProofInternal(CDProof* cdp, Node eqi)
         }
         for (const Node& eq : itd->second.d_vars)
         {
-          Assert(eq.getKind() == EQUAL);
+          Assert(eq.getKind() == Kind::EQUAL);
           lhsTgtc.push_back(eq[1]);
         }
         Node lhsTgt = nm->mkNode(cur[0].getKind(), lhsTgtc);
@@ -901,7 +901,7 @@ Node RewriteDbProofCons::getRuleConclusion(const RewriteProofRule& rpr,
       {
         // currently avoid accidental loops: arbitrarily bound to 1000
         continueFixedPoint = steps.size() <= 1000;
-        Assert(d_currFixedPointConc.getKind() == EQUAL);
+        Assert(d_currFixedPointConc.getKind() == Kind::EQUAL);
         steps.push_back(d_currFixedPointConc[1]);
         stepsSubs.emplace_back(d_currFixedPointSubs.begin(),
                                d_currFixedPointSubs.end());