More

src/api/cpp/cvc5_proof_rule_template.cpp

@@ -158,7 +158,8 @@ const char* toString(ProofRule rule)
     case ProofRule::MACRO_RE_ELIM: return "MACRO_RE_ELIM";
     //================================================= Arith rules
     case ProofRule::MACRO_ARITH_SCALE_SUM_UB: return "MACRO_ARITH_SCALE_SUM_UB";
-    case ProofRule::MACRO_ARITH_NL_COMPARISON: return "MACRO_ARITH_NL_COMPARISON";
+    case ProofRule::MACRO_ARITH_NL_COMPARISON:
+      return "MACRO_ARITH_NL_COMPARISON";
     case ProofRule::ARITH_SUM_UB: return "ARITH_SUM_UB";
     case ProofRule::ARITH_TRICHOTOMY: return "ARITH_TRICHOTOMY";
     case ProofRule::INT_TIGHT_LB: return "INT_TIGHT_LB";

src/proof/conv_proof_generator.cpp

@@ -112,13 +112,14 @@ void TConvProofGenerator::addRewriteStep(Node t,
   }
 }
 
-void TConvProofGenerator::addTrustedRewriteStep(Node t,
-                    Node s,
-                    TrustId id,
-                    const std::vector<Node>& children,
-                    const std::vector<Node>& args,
-                    bool isPre,
-                    uint32_t tctx)
+void TConvProofGenerator::addTrustedRewriteStep(
+    Node t,
+    Node s,
+    TrustId id,
+    const std::vector<Node>& children,
+    const std::vector<Node>& args,
+    bool isPre,
+    uint32_t tctx)
 {
   std::vector<Node> targs;
   targs.push_back(mkTrustId(id));

src/proof/conv_proof_generator.h

@@ -174,12 +174,12 @@ class TConvProofGenerator : protected EnvObj, public ProofGenerator
                       uint32_t tctx = 0);
   /** Same as above, but with a trusted step */
   void addTrustedRewriteStep(Node t,
-                      Node s,
-                      TrustId id,
-                      const std::vector<Node>& children,
-                      const std::vector<Node>& args,
-                      bool isPre = false,
-                      uint32_t tctx = 0);
+                             Node s,
+                             TrustId id,
+                             const std::vector<Node>& children,
+                             const std::vector<Node>& args,
+                             bool isPre = false,
+                             uint32_t tctx = 0);
   /** Has rewrite step for term t */
   bool hasRewriteStep(Node t, uint32_t tctx = 0, bool isPre = false) const;
   /**

src/proof/trust_id.cpp

@@ -38,7 +38,8 @@ const char* toString(TrustId id)
     case TrustId::ARITH_NL_COVERING_DIRECT: return "ARITH_NL_COVERING_DIRECT";
     case TrustId::ARITH_NL_COVERING_RECURSIVE:
       return "ARITH_NL_COVERING_RECURSIVE";
-    case TrustId::ARITH_NL_COMPARE_LIT_TRANSFORM: return "ARITH_NL_COMPARE_LIT_TRANSFORM";
+    case TrustId::ARITH_NL_COMPARE_LIT_TRANSFORM:
+      return "ARITH_NL_COMPARE_LIT_TRANSFORM";
     case TrustId::EXT_THEORY_REWRITE: return "EXT_THEORY_REWRITE";
     case TrustId::REWRITE_NO_ELABORATE: return "REWRITE_NO_ELABORATE";
     case TrustId::FLATTENING_REWRITE: return "FLATTENING_REWRITE";

src/smt/proof_post_processor.cpp

@@ -970,8 +970,8 @@ Node ProofPostprocessCallback::expandMacros(ProofRule id,
   else if (id == ProofRule::MACRO_ARITH_NL_COMPARISON)
   {
     Node resc = theory::arith::expandMacroNlComparison(children, args, cdp);
-    //Assert(!resc.isNull());
-    //Assert(res.isNull() || resc == res);
+    // Assert(!resc.isNull());
+    // Assert(res.isNull() || resc == res);
     return resc;
   }
   else if (id == ProofRule::MACRO_STRING_INFERENCE)

src/theory/arith/arith_proof_utilities.cpp

@@ -109,11 +109,12 @@ Node expandMacroSumUb(const std::vector<Node>& children,
 }
 
 Node expandMacroNlComparison(const std::vector<Node>& children,
-                      const std::vector<Node>& args,
-                      CDProof* cdp)
+                             const std::vector<Node>& args,
+                             CDProof* cdp)
 {
-  Trace("macro::arith") << "Comparsion prove: " << children << " => " << args[0] << std::endl;
-  //AlwaysAssert(false);
+  Trace("macro::arith") << "Comparsion prove: " << children << " => " << args[0]
+                        << std::endl;
+  // AlwaysAssert(false);
   return Node::null();
 }
 

src/theory/arith/arith_proof_utilities.h

@@ -76,8 +76,8 @@ Node expandMacroSumUb(const std::vector<Node>& children,
  * @return The conclusion of the proof rule.
  */
 Node expandMacroNlComparison(const std::vector<Node>& children,
-                      const std::vector<Node>& args,
-                      CDProof* cdp);
+                             const std::vector<Node>& args,
+                             CDProof* cdp);
 }  // namespace arith
 }  // namespace theory
 }  // namespace cvc5::internal

src/theory/arith/nl/ext/arith_nl_compare_proof_gen.cpp

@@ -15,24 +15,27 @@
 
 #include "theory/arith/nl/ext/arith_nl_compare_proof_gen.h"
 
-#include "theory/arith/arith_utilities.h"
-#include "theory/arith/nl/ext/monomial_check.h"
 #include "expr/attribute.h"
 #include "proof/proof.h"
+#include "theory/arith/arith_utilities.h"
+#include "theory/arith/nl/ext/monomial_check.h"
 
 namespace cvc5::internal {
 namespace theory {
 namespace arith {
 namespace nl {
 
-ArithNlCompareProofGenerator::ArithNlCompareProofGenerator(Env& env) : EnvObj(env) {}
+ArithNlCompareProofGenerator::ArithNlCompareProofGenerator(Env& env)
+    : EnvObj(env)
+{
+}
 ArithNlCompareProofGenerator::~ArithNlCompareProofGenerator() {}
 
 std::shared_ptr<ProofNode> ArithNlCompareProofGenerator::getProofFor(Node fact)
 {
-  Assert (fact.getKind()==Kind::IMPLIES);
+  Assert(fact.getKind() == Kind::IMPLIES);
   std::vector<Node> exp;
-  if (fact[0].getKind()==Kind::AND)
+  if (fact[0].getKind() == Kind::AND)
   {
     exp.insert(exp.end(), fact[0].begin(), fact[0].end());
   }
@@ -41,7 +44,8 @@ std::shared_ptr<ProofNode> ArithNlCompareProofGenerator::getProofFor(Node fact)
     exp.emplace_back(fact[0]);
   }
   Node conc = fact[1];
-  Trace("arith-nl-compare") << "Comparsion prove: " << exp << " => " << conc << std::endl;
+  Trace("arith-nl-compare")
+      << "Comparsion prove: " << exp << " => " << conc << std::endl;
   // get the expected form of the literals
   CDProof cdp(d_env);
   std::vector<Node> expc;
@@ -54,18 +58,19 @@ std::shared_ptr<ProofNode> ArithNlCompareProofGenerator::getProofFor(Node fact)
       continue;
     }
     expc.emplace_back(ec);
-    if (e!=ec)
+    if (e != ec)
     {
       Node eeq = e.eqNode(ec);
       cdp.addTrustedStep(eeq, TrustId::ARITH_NL_COMPARE_LIT_TRANSFORM, {}, {});
       cdp.addStep(ec, ProofRule::EQ_RESOLVE, {e, eeq}, {});
     }
   }
   Node concc = getCompareLit(conc);
-  Assert (!concc.isNull());  
-  Trace("arith-nl-compare") << "...processed prove: " << expc << " => " << concc << std::endl;
+  Assert(!concc.isNull());
+  Trace("arith-nl-compare")
+      << "...processed prove: " << expc << " => " << concc << std::endl;
   cdp.addStep(concc, ProofRule::MACRO_ARITH_NL_COMPARISON, expc, {concc});
-  if (conc!=concc)
+  if (conc != concc)
   {
     Node ceq = concc.eqNode(conc);
     cdp.addTrustedStep(ceq, TrustId::ARITH_NL_COMPARE_LIT_TRANSFORM, {}, {});
@@ -76,9 +81,13 @@ std::shared_ptr<ProofNode> ArithNlCompareProofGenerator::getProofFor(Node fact)
   return cdp.getProofFor(fact);
 }
 
-std::string ArithNlCompareProofGenerator::identify() const { return "ArithNlCompareProofGenerator"; }
+std::string ArithNlCompareProofGenerator::identify() const
+{
+  return "ArithNlCompareProofGenerator";
+}
 
-Node ArithNlCompareProofGenerator::mkLit(NodeManager* nm, Kind k, const Node& a, const Node& b, bool isAbsolute)
+Node ArithNlCompareProofGenerator::mkLit(
+    NodeManager* nm, Kind k, const Node& a, const Node& b, bool isAbsolute)
 {
   Node au = a;
   Node bu = b;
@@ -87,7 +96,7 @@ Node ArithNlCompareProofGenerator::mkLit(NodeManager* nm, Kind k, const Node& a,
     au = nm->mkNode(Kind::ABS, au);
     bu = nm->mkNode(Kind::ABS, bu);
   }
-  if (k==Kind::EQUAL)
+  if (k == Kind::EQUAL)
   {
     return mkEquality(au, bu);
   }
@@ -97,9 +106,15 @@ Node ArithNlCompareProofGenerator::mkLit(NodeManager* nm, Kind k, const Node& a,
 struct ArithNlCompareLitAttributeId
 {
 };
-using ArithNlCompareLitAttribute = expr::Attribute<ArithNlCompareLitAttributeId, Node>;
+using ArithNlCompareLitAttribute =
+    expr::Attribute<ArithNlCompareLitAttributeId, Node>;
 
-void ArithNlCompareProofGenerator::setCompareLit(NodeManager* nm, Node olit, Kind k, const Node& a, const Node& b, bool isAbsolute)
+void ArithNlCompareProofGenerator::setCompareLit(NodeManager* nm,
+                                                 Node olit,
+                                                 Kind k,
+                                                 const Node& a,
+                                                 const Node& b,
+                                                 bool isAbsolute)
 {
   Node lit = mkLit(nm, k, a, b, isAbsolute);
   ArithNlCompareLitAttribute ancla;
@@ -116,4 +131,3 @@ Node ArithNlCompareProofGenerator::getCompareLit(const Node& olit)
 }  // namespace arith
 }  // namespace theory
 }  // namespace cvc5::internal
-

src/theory/arith/nl/ext/arith_nl_compare_proof_gen.h

@@ -16,8 +16,8 @@
 #ifndef CVC5__THEORY__ARITH__NL__EXT__ARITH_NL_COMPARE_PROOF_GEN_H
 #define CVC5__THEORY__ARITH__NL__EXT__ARITH_NL_COMPARE_PROOF_GEN_H
 
-#include "smt/env_obj.h"
 #include "proof/proof_generator.h"
+#include "smt/env_obj.h"
 
 namespace cvc5::internal {
 namespace theory {
@@ -26,7 +26,7 @@ namespace nl {
 
 class ArithNlCompareProofGenerator : protected EnvObj, public ProofGenerator
 {
-public:
+ public:
   ArithNlCompareProofGenerator(Env& env);
   virtual ~ArithNlCompareProofGenerator();
   /**
@@ -35,9 +35,15 @@ class ArithNlCompareProofGenerator : protected EnvObj, public ProofGenerator
   /** identify */
   std::string identify() const override;
   /** Make literal */
-  static Node mkLit(NodeManager* nm, Kind k, const Node& a, const Node& b, bool isAbsolute);
+  static Node mkLit(
+      NodeManager* nm, Kind k, const Node& a, const Node& b, bool isAbsolute);
   /** */
-  static void setCompareLit(NodeManager* nm, Node olit, Kind k, const Node& a, const Node& b, bool isAbsolute);
+  static void setCompareLit(NodeManager* nm,
+                            Node olit,
+                            Kind k,
+                            const Node& a,
+                            const Node& b,
+                            bool isAbsolute);
   /** */
   static Node getCompareLit(const Node& olit);
 };

src/theory/arith/nl/ext/monomial_check.cpp

@@ -31,7 +31,11 @@ namespace arith {
 namespace nl {
 
 MonomialCheck::MonomialCheck(Env& env, ExtState* data)
-    : EnvObj(env), d_data(data), d_ancPfGen(env.isTheoryProofProducing() ? new ArithNlCompareProofGenerator(env) : nullptr)
+    : EnvObj(env),
+      d_data(data),
+      d_ancPfGen(env.isTheoryProofProducing()
+                     ? new ArithNlCompareProofGenerator(env)
+                     : nullptr)
 {
   d_order_points.push_back(d_data->d_neg_one);
   d_order_points.push_back(d_data->d_zero);
@@ -426,17 +430,18 @@ bool MonomialCheck::compareMonomial(
         }
       }
       Node cob = ob;
-      if (ob==d_data->d_one)
+      if (ob == d_data->d_one)
       {
         cob = mkOne(oa.getType());
       }
       Node conc = mkLit(oa, ob, status, true);
-      Node clem = nm->mkNode(
-          Kind::IMPLIES, nm->mkAnd(exp), conc);
+      Node clem = nm->mkNode(Kind::IMPLIES, nm->mkAnd(exp), conc);
       Trace("nl-ext-comp-lemma") << "comparison lemma : " << clem << std::endl;
       // use special proof generator
-      lem.emplace_back(
-          InferenceId::ARITH_NL_COMPARISON, clem, LemmaProperty::NONE, d_ancPfGen.get());
+      lem.emplace_back(InferenceId::ARITH_NL_COMPARISON,
+                       clem,
+                       LemmaProperty::NONE,
+                       d_ancPfGen.get());
       cmp_infers[status][oa][ob] = clem;
     }
     return true;
@@ -728,8 +733,8 @@ void MonomialCheck::assignOrderIds(std::vector<Node>& vars,
 
 Node MonomialCheck::mkLit(Node a, Node b, int status, bool isAbsolute) const
 {
-  NodeManager * nm = nodeManager();
-  if (status<0)
+  NodeManager* nm = nodeManager();
+  if (status < 0)
   {
     status = -status;
     Node tmp = a;
@@ -770,13 +775,13 @@ Node MonomialCheck::mkLit(Node a, Node b, int status, bool isAbsolute) const
       Node negate_b = nm->mkNode(Kind::NEG, b);
       ret = a_is_nonnegative.iteNode(
           b_is_nonnegative.iteNode(nm->mkNode(k, a, b),
-                                  nm->mkNode(k, a, negate_b)),
+                                   nm->mkNode(k, a, negate_b)),
           b_is_nonnegative.iteNode(nm->mkNode(k, negate_a, b),
-                                  nm->mkNode(k, negate_a, negate_b)));
+                                   nm->mkNode(k, negate_a, negate_b)));
     }
   }
   // if proofs are enabled, we ensure we remember what the literal represents
-  if (d_ancPfGen!=nullptr)
+  if (d_ancPfGen != nullptr)
   {
     ArithNlCompareProofGenerator::setCompareLit(nm, ret, k, a, b, isAbsolute);
   }

src/theory/arith/nl/ext/monomial_check.h

@@ -18,9 +18,9 @@
 
 #include "expr/node.h"
 #include "smt/env_obj.h"
+#include "theory/arith/nl/ext/arith_nl_compare_proof_gen.h"
 #include "theory/arith/nl/ext/monomial.h"
 #include "theory/theory_inference.h"
-#include "theory/arith/nl/ext/arith_nl_compare_proof_gen.h"
 
 namespace cvc5::internal {
 namespace theory {
@@ -77,6 +77,7 @@ class MonomialCheck : protected EnvObj
 
   /** Make literal */
   static Node mkLit(NodeManager* nm, Kind k, Node a, Node b, bool isAbsolute);
+
  private:
   /** In the following functions, status states a relationship
    * between two arithmetic terms, where:

src/theory/arith/nl/ext/proof_checker.cpp

@@ -152,7 +152,7 @@ Node ExtProofRuleChecker::checkInternal(ProofRule id,
                        nm->mkNode(Kind::GEQ, x, a),
                        nm->mkNode(sgn == -1 ? Kind::LEQ : Kind::GEQ, y, b))));
   }
-  else if (id ==ProofRule::MACRO_ARITH_NL_COMPARISON)
+  else if (id == ProofRule::MACRO_ARITH_NL_COMPARISON)
   {
     return args[0];
   }