Format

src/api/cpp/cvc5_proof_rule_template.cpp

@@ -130,7 +130,8 @@ const char* toString(ProofRule rule)
     case ProofRule::QUANT_VAR_REORDERING: return "QUANT_VAR_REORDERING";
     case ProofRule::EXISTS_STRING_LENGTH: return "EXISTS_STRING_LENGTH";
     case ProofRule::EXISTS_INV_CONDITION: return "EXISTS_INV_CONDITION";
-    case ProofRule::MACRO_EXISTS_INV_CONDITION: return "MACRO_EXISTS_INV_CONDITION";
+    case ProofRule::MACRO_EXISTS_INV_CONDITION:
+      return "MACRO_EXISTS_INV_CONDITION";
     //================================================= Sets rules
     case ProofRule::SETS_SINGLETON_INJ: return "SETS_SINGLETON_INJ";
     case ProofRule::SETS_EXT: return "SETS_EXT";

src/expr/elim_witness_converter.h

@@ -29,7 +29,7 @@ namespace cvc5::internal {
  * Node converter to eliminate all terms of kind WITNESS. Each term replaced
  * in this way is captured by a skolem that witnesses the axiom for that
  * witness.
- * 
+ *
  * Witness terms are required to track their justification as part of their
  * AST. In particular, it is required that all terms of kind WITNESS are given
  * an instantiation attribute of the form:
@@ -47,7 +47,7 @@ namespace cvc5::internal {
  * For each witness of this form, we replace the witness by its corresponding
  * skolem and collect its corresponding axiom, defining what lemma we can
  * assume about it, which can be retrieved via ::getAxioms in this class.
- * 
+ *
  * Note that we use WITNESS terms for two reasons:
  * (1) (witness x (= x t)) can naturally rewrite to t, which we wish to
  * infer when applicable by substitution + rewriting.

src/theory/arith/arith_proof_rcons.cpp

@@ -15,16 +15,16 @@
 
 #include "theory/arith/arith_proof_rcons.h"
 
+#include "expr/term_context.h"
+#include "proof/conv_proof_generator.h"
 #include "proof/proof.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/arith_subs.h"
-#include "proof/conv_proof_generator.h"
-#include "expr/term_context.h"
 
 namespace cvc5::internal {
 namespace theory {
 namespace arith {
-  
+
 /**
  * Arithmetic substitution term context.
  */
@@ -37,7 +37,7 @@ class ArithSubsTermContext : public TermContext
   /** Compute the value of the index^th child of t whose hash is tval */
   uint32_t computeValue(TNode t, uint32_t tval, size_t index) const override
   {
-    if (tval==0)
+    if (tval == 0)
     {
       // if we should not traverse, return 1
       if (!ArithSubs::shouldTraverse(t))
@@ -78,8 +78,12 @@ std::shared_ptr<ProofNode> ArithProofRCons::getProofFor(Node fact)
     ArithSubs asubs;
     std::vector<Node> assumpsNoSolve;
     ArithSubsTermContext astc;
-    TConvProofGenerator tcnv(d_env, nullptr, TConvPolicy::FIXPOINT, TConvCachePolicy::NEVER,
-                      "ArithRConsTConv", &astc);
+    TConvProofGenerator tcnv(d_env,
+                             nullptr,
+                             TConvPolicy::FIXPOINT,
+                             TConvCachePolicy::NEVER,
+                             "ArithRConsTConv",
+                             &astc);
     Node tgtAssump;
     // prove false
     for (const Node& a : assumps)
@@ -98,10 +102,10 @@ std::shared_ptr<ProofNode> ArithProofRCons::getProofFor(Node fact)
       if (asr == d_false)
       {
         Trace("arith-proof-rcons") << "...success!" << std::endl;
-        if (a!=as)
+        if (a != as)
         {
           std::shared_ptr<ProofNode> pfn = tcnv.getProofForRewriting(a);
-          Assert (pfn.getResult()[1]==as);
+          Assert(pfn.getResult()[1] == as);
           cdp.addProof(pfn);
           cdp.addStep(as, ProofRule::EQ_RESOLVE, {a, a.eqNode(as)}, {});
         }
@@ -129,14 +133,14 @@ std::shared_ptr<ProofNode> ArithProofRCons::getProofFor(Node fact)
             Trace("arith-proof-rcons")
                 << "...solved " << m.first << " = " << val << std::endl;
             Node eq = m.first.eqNode(val);
-            if (a!=as)
+            if (a != as)
             {
               std::shared_ptr<ProofNode> pfn = tcnv.getProofForRewriting(a);
-              Assert (pfn.getResult()[1]==as);
+              Assert(pfn.getResult()[1] == as);
               cdp.addProof(pfn);
               cdp.addStep(as, ProofRule::EQ_RESOLVE, {a, a.eqNode(as)}, {});
             }
-            if (as!=eq)
+            if (as != eq)
             {
               cdp.addStep(eq, ProofRule::MACRO_SR_PRED_TRANSFORM, {as}, {eq});
             }
@@ -165,14 +169,14 @@ std::shared_ptr<ProofNode> ArithProofRCons::getProofFor(Node fact)
         Node as = asubs.applyArith(a);
         Node asr = rewrite(as);
         Trace("arith-proof-rcons") << "...have " << asr << std::endl;
-        if (a!=as)
+        if (a != as)
         {
           std::shared_ptr<ProofNode> pfn = tcnv.getProofForRewriting(a);
-          Assert (pfn.getResult()[1]==as);
+          Assert(pfn.getResult()[1] == as);
           cdp.addProof(pfn);
           cdp.addStep(as, ProofRule::EQ_RESOLVE, {a, a.eqNode(as)}, {});
         }
-        if (as!=asr)
+        if (as != asr)
         {
           cdp.addStep(asr, ProofRule::MACRO_SR_PRED_TRANSFORM, {as}, {asr});
         }

src/theory/arith/arith_subs.cpp

@@ -109,11 +109,9 @@ bool ArithSubs::shouldTraverse(const Node& n, bool traverseNlMult)
 {
   Kind k = n.getKind();
   TheoryId ctid = theory::kindToTheoryId(k);
-  if ((ctid != THEORY_ARITH && ctid != THEORY_BOOL
-        && ctid != THEORY_BUILTIN)
+  if ((ctid != THEORY_ARITH && ctid != THEORY_BOOL && ctid != THEORY_BUILTIN)
       || isTranscendentalKind(k)
-      || (!traverseNlMult
-          && (k == Kind::NONLINEAR_MULT || k == Kind::IAND)))
+      || (!traverseNlMult && (k == Kind::NONLINEAR_MULT || k == Kind::IAND)))
   {
     return false;
   }

src/theory/arith/arith_subs.h

@@ -47,10 +47,10 @@ class ArithSubs : public Subs
    * @param traverseNlMult Whether to traverse applications of NONLINEAR_MULT.
    */
   Node applyArith(const Node& n, bool traverseNlMult = true) const;
-  /** 
+  /**
    * Should traverse, returns true if the above method traverses n.
    */
-  static bool shouldTraverse(const Node& n, bool traverseNlMult = true); 
+  static bool shouldTraverse(const Node& n, bool traverseNlMult = true);
 };
 
 }  // namespace arith