Foramt

ajreynol · Dec 20, 2024 · be2a827 · be2a827
1 parent 7d0c75b
commit be2a827
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 9 deletions.
diff --git a/src/rewriter/rewrite_db_proof_cons.cpp b/src/rewriter/rewrite_db_proof_cons.cpp
@@ -213,11 +213,11 @@ Node RewriteDbProofCons::preprocessClosureEq(CDProof* cdp,
   }
   Node eq;
   Node eqConv = ai.eqNode(bi);
-  theory::Rewriter * rr = d_env.getRewriter();
+  theory::Rewriter* rr = d_env.getRewriter();
   if (ai[0] == bi[0])
   {
-    ProofRewriteRule prid = rr->findRule(
-        ai, bi, theory::TheoryRewriteCtx::PRE_DSL);
+    ProofRewriteRule prid =
+        rr->findRule(ai, bi, theory::TheoryRewriteCtx::PRE_DSL);
     if (prid != ProofRewriteRule::NONE)
     {
       // a simple theory rewrite happens to solve it, do not continue
@@ -287,10 +287,10 @@ Node RewriteDbProofCons::preprocessClosureEq(CDProof* cdp,
   else if (ai[0].getNumChildren() > bi[0].getNumChildren())
   {
     // maybe unused variables on the left hand side
-    Node aiu =  rr->rewriteViaRule(ProofRewriteRule::QUANT_UNUSED_VARS, ai);
+    Node aiu = rr->rewriteViaRule(ProofRewriteRule::QUANT_UNUSED_VARS, ai);
     if (!aiu.isNull())
     {
-      Assert (aiu!=ai);
+      Assert(aiu != ai);
       Node eqq = ai.eqNode(aiu);
       cdp->addTheoryRewriteStep(eqq, ProofRewriteRule::QUANT_UNUSED_VARS);
       eq = aiu.eqNode(bi);

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
@@ -470,7 +470,7 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){
       case Kind::ARCSECANT:
       case Kind::ARCCOTANGENT:
       case Kind::SQRT:
-      case Kind::IAND: 
+      case Kind::IAND:
       case Kind::POW2: return postRewriteExpert(t);
       default: Unreachable();
     }
@@ -482,7 +482,7 @@ RewriteResponse ArithRewriter::postRewriteExpert(TNode t)
   {
     return RewriteResponse(REWRITE_DONE, t);
   }
-  switch(t.getKind())
+  switch (t.getKind())
   {
     case Kind::EXPONENTIAL:
     case Kind::SINE:
@@ -503,7 +503,6 @@ RewriteResponse ArithRewriter::postRewriteExpert(TNode t)
     default: Unreachable();
   }
 }
-
 
 RewriteResponse ArithRewriter::rewriteRAN(TNode t)
 {

diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h
@@ -67,7 +67,7 @@ class ArithRewriter : public TheoryRewriter
   RewriteResponse preRewriteTerm(TNode t);
   /** postRewrite for terms */
   RewriteResponse postRewriteTerm(TNode t);
-  
+
   /** Post-rewrites that are only available in expert mode */
   RewriteResponse postRewriteExpert(TNode t);