Add arithmetic lemma proof reconstruction utility

src/CMakeLists.txt

@@ -387,6 +387,8 @@ libcvc5_add_sources(
   theory/arith/arith_poly_norm.h
   theory/arith/arith_preprocess.cpp
   theory/arith/arith_preprocess.h
+  theory/arith/arith_proof_rcons.cpp
+  theory/arith/arith_proof_rcons.h
   theory/arith/arith_proof_utilities.cpp
   theory/arith/arith_proof_utilities.h
   theory/arith/arith_rewriter.cpp

src/theory/arith/arith_proof_rcons.cpp

@@ -0,0 +1,167 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * A generic utility for infer proofs for arithmetic lemmas.
+ */
+
+#include "theory/arith/arith_proof_rcons.h"
+
+#include "proof/proof.h"
+#include "theory/arith/arith_msum.h"
+#include "theory/arith/arith_subs.h"
+
+namespace cvc5::internal {
+namespace theory {
+namespace arith {
+
+ArithProofRCons::ArithProofRCons(Env& env, TrustId id) : EnvObj(env), d_id(id)
+{
+  d_false = nodeManager()->mkConst(false);
+}
+
+ArithProofRCons::~ArithProofRCons() {}
+
+std::shared_ptr<ProofNode> ArithProofRCons::getProofFor(Node fact)
+{
+  Trace("arith-proof-rcons") << "ArithProofRCons: prove " << fact << std::endl;
+  CDProof cdp(d_env);
+  bool success = false;
+  // ARITH_DIO_LEMMA can typically be reconstructed via substitution+rewriting.
+  if (d_id == TrustId::ARITH_DIO_LEMMA)
+  {
+    Assert(fact.getKind() == Kind::NOT);
+    std::vector<Node> assumps;
+    if (fact[0].getKind() == Kind::AND)
+    {
+      assumps.insert(assumps.end(), fact[0].begin(), fact[0].end());
+    }
+    else
+    {
+      assumps.push_back(fact[0]);
+    }
+    ArithSubs asubs;
+    std::vector<Node> assumpsNoSolve;
+    std::vector<Node> assumpsSolve;
+    Node tgtAssump;
+    // prove false
+    for (const Node& a : assumps)
+    {
+      Trace("arith-proof-rcons") << "Assumption: " << a << std::endl;
+      if (a.getKind() != Kind::EQUAL)
+      {
+        Trace("arith-proof-rcons") << "...not solved" << std::endl;
+        assumpsNoSolve.push_back(a);
+        continue;
+      }
+      Node as = asubs.applyArith(a);
+      as = rewrite(as);
+      Trace("arith-proof-rcons")
+          << "...under subs+rewrite: " << as << std::endl;
+      if (as == d_false)
+      {
+        Trace("arith-proof-rcons") << "...success!" << std::endl;
+        std::vector<Node> pargs;
+        pargs.push_back(a);
+        pargs.insert(pargs.end(), assumpsSolve.begin(), assumpsSolve.end());
+        cdp.addStep(
+            d_false, ProofRule::MACRO_SR_PRED_TRANSFORM, pargs, {d_false});
+        success = true;
+        break;
+      }
+      // see if there is a variable to solve for
+      std::map<Node, Node> msum;
+      bool solved = false;
+      if (ArithMSum::getMonomialSumLit(as, msum))
+      {
+        for (const std::pair<const Node, Node>& m : msum)
+        {
+          if (m.first.isNull() || !m.second.isNull())
+          {
+            continue;
+          }
+          Node veq_c, val;
+          int ires = ArithMSum::isolate(m.first, msum, veq_c, val, Kind::EQUAL);
+          if (ires != 0 && veq_c.isNull())
+          {
+            solved = true;
+            Trace("arith-proof-rcons")
+                << "...solved " << m.first << " = " << val << std::endl;
+            Node eq = m.first.eqNode(val);
+            std::vector<Node> pargs;
+            pargs.push_back(a);
+            pargs.insert(pargs.end(), assumpsSolve.begin(), assumpsSolve.end());
+            cdp.addStep(eq, ProofRule::MACRO_SR_PRED_TRANSFORM, pargs, {eq});
+            assumpsSolve.push_back(eq);
+            asubs.add(m.first, val);
+            break;
+          }
+        }
+      }
+      if (!solved)
+      {
+        Trace("arith-proof-rcons") << "...not solved" << std::endl;
+        assumpsNoSolve.push_back(a);
+      }
+    }
+    if (!success)
+    {
+      Trace("arith-proof-rcons") << "Not solved by rewriting single literal" << std::endl;
+      // check if two unsolved literals rewrite to the negation of one another
+      std::vector<Node> sassumps;
+      std::map<Node, bool> pols;
+      std::map<Node, bool>::iterator itp;
+      for (const Node& a : assumpsNoSolve)
+      {
+        Node as = asubs.applyArith(a);
+        as = rewrite(as);
+        Trace("arith-proof-rcons") << "...have " << as << std::endl;
+        std::vector<Node> pargs;
+        pargs.push_back(a);
+        pargs.insert(pargs.end(), assumpsSolve.begin(), assumpsSolve.end());
+        cdp.addStep(as, ProofRule::MACRO_SR_PRED_TRANSFORM, pargs, {as});
+        bool pol = as.getKind()!=Kind::NOT;
+        Node aslit = pol ? as : as[0];
+        itp = pols.find(aslit);
+        if (itp!=pols.end())
+        {
+          if (itp->second!=pol)
+          {
+            Node asn = aslit.notNode();
+            cdp.addStep(d_false, ProofRule::CONTRA, {aslit, asn}, {});
+            success = true;
+            Trace("arith-proof-rcons") << "......contradiction" << std::endl;
+            break;
+          }
+        }
+        else
+        {
+          pols[aslit] = pol;
+        }
+      }
+    }
+    if (success)
+    {
+      cdp.addStep(fact, ProofRule::SCOPE, {d_false}, assumps);
+    }
+  }
+  if (!success)
+  {
+    cdp.addTrustedStep(fact, d_id, {}, {});
+  }
+  return cdp.getProofFor(fact);
+}
+
+std::string ArithProofRCons::identify() const { return "ArithProofRCons"; }
+
+}  // namespace arith
+}  // namespace theory
+}  // namespace cvc5::internal

src/theory/arith/arith_proof_rcons.h

@@ -0,0 +1,62 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * A generic utility for infer proofs for arithmetic lemmas.
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__THEORY__ARITH__ARITH_PROOF_RCONS_H
+#define CVC5__THEORY__ARITH__ARITH_PROOF_RCONS_H
+
+#include "expr/node.h"
+#include "proof/proof_generator.h"
+#include "proof/trust_id.h"
+#include "proof/trust_node.h"
+#include "smt/env_obj.h"
+
+namespace cvc5::internal {
+namespace theory {
+namespace arith {
+
+/**
+ * Proof generator that is used for reconstructing lemmas coming from
+ * arithmetic that do not have proof tracking. This includes:
+ * - ARITH_DIO_LEMMA, lemmas coming from the dio solver.
+ */
+class ArithProofRCons : protected EnvObj, public ProofGenerator
+{
+ public:
+  /**
+   * @param env Reference to the environment
+   * @param id The trust id to use if the proof reconstruction fails.
+   */
+  ArithProofRCons(Env& env, TrustId id);
+  virtual ~ArithProofRCons();
+  /**
+   * Get proof for an arithmetic lemma.
+   */
+  std::shared_ptr<ProofNode> getProofFor(Node fact) override;
+  /** identify */
+  std::string identify() const override;
+ private:
+  /** The trust id to use if the proof reconstruction fails. */
+  TrustId d_id;
+  /** False node */
+  Node d_false;
+};
+
+}  // namespace arith
+}  // namespace theory
+}  // namespace cvc5::internal
+
+#endif /* CVC5__THEORY__ARITH__ARITH_PROOF_RCONS_H */

src/theory/arith/linear/theory_arith_private.cpp

@@ -43,6 +43,7 @@
 #include "proof/proof_generator.h"
 #include "proof/proof_node_manager.h"
 #include "smt/logic_exception.h"
+#include "theory/arith/arith_proof_rcons.h"
 #include "theory/arith/arith_proof_utilities.h"
 #include "theory/arith/arith_rewriter.h"
 #include "theory/arith/arith_utilities.h"
@@ -3407,12 +3408,9 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel)
           {
             assump.push_back(possibleConflict);
           }
-          Node falsen = nodeManager()->mkConst(false);
-          CDProof cdp(d_env);
-          cdp.addTrustedStep(falsen, TrustId::ARITH_DIO_LEMMA, assump, {});
           Node npc = possibleConflict.notNode();
-          cdp.addStep(npc, ProofRule::SCOPE, {falsen}, assump);
-          pf = cdp.getProofFor(npc);
+          ArithProofRCons arc(d_env, TrustId::ARITH_DIO_LEMMA);
+          pf = arc.getProofFor(npc);
         }
         raiseBlackBoxConflict(possibleConflict, pf);
         outputConflicts();