Merge branch 'main' of https://github.com/cvc5/cvc5 into pfTrustId

include/cvc5/cvc5_proof_rule.h

@@ -1892,13 +1892,23 @@ enum ENUM(ProofRule)
   EVALUE(ARITH_TRICHOTOMY),
   /**
    * \verbatim embed:rst:leading-asterisk
-   * **Arithmetic -- Operator elimination**
+   * **Arithmetic -- Reduction**
    *
    * .. math::
-   *   \inferrule{- \mid t}{\texttt{arith::OperatorElim::getAxiomFor(t)}}
+   *   \inferrule{- \mid t}{F}
+   * 
+   * where :math:`t` is an application of an extended arithmetic operator (e.g.
+   * division, modulus, cosine, sqrt, is_int, to_int) and :math:`F` is the
+   * reduction predicate for :math:`t`. In other words, :math:`F` is a
+   * predicate that is used to reduce reasoning about :math:`t` to reasoning
+   * about the core operators of arithmetic.
+   *
+   * In detail, :math:`F` is implemented by
+   * :math:`\texttt{arith::OperatorElim::getAxiomFor(t)}`, see
+   * :cvc5src:`theory/arith/operator_elim.h`.
    * \endverbatim
    */
-  EVALUE(ARITH_OP_ELIM_AXIOM),
+  EVALUE(ARITH_REDUCTION),
   /**
    * \verbatim embed:rst:leading-asterisk
    * **Arithmetic -- Polynomial normalization**

src/api/cpp/cvc5_proof_rule_template.cpp

@@ -167,7 +167,7 @@ const char* toString(ProofRule rule)
     case ProofRule::ARITH_MULT_POS: return "ARITH_MULT_POS";
     case ProofRule::ARITH_MULT_NEG: return "ARITH_MULT_NEG";
     case ProofRule::ARITH_MULT_TANGENT: return "ARITH_MULT_TANGENT";
-    case ProofRule::ARITH_OP_ELIM_AXIOM: return "ARITH_OP_ELIM_AXIOM";
+    case ProofRule::ARITH_REDUCTION: return "ARITH_REDUCTION";
     case ProofRule::ARITH_POLY_NORM: return "ARITH_POLY_NORM";
     case ProofRule::ARITH_POLY_NORM_REL: return "ARITH_POLY_NORM_REL";
     case ProofRule::ARITH_TRANS_PI: return "ARITH_TRANS_PI";

src/options/arith_options.toml

@@ -336,14 +336,6 @@ name   = "Arithmetic Theory"
   default    = "2"
   help       = "threshold for substituting an equality in ppAssert"
 
-[[option]]
-  name       = "arithNoPartialFun"
-  category   = "expert"
-  long       = "arith-no-partial-fun"
-  type       = "bool"
-  default    = "false"
-  help       = "do not use partial function semantics for arithmetic (not SMT LIB compliant)"
-
 [[option]]
   name       = "pbRewrites"
   category   = "expert"

src/theory/arith/operator_elim.cpp

@@ -28,6 +28,7 @@
 #include "theory/arith/nl/poly_conversion.h"
 #include "theory/rewriter.h"
 #include "theory/theory.h"
+#include "proof/proof.h"
 
 using namespace cvc5::internal::kind;
 
@@ -81,11 +82,13 @@ TrustNode OperatorElim::eliminate(Node n,
   Assert(klems.size() <= 1);
   for (std::pair<Node, Node>& p : klems)
   {
+    // each skolem lemma can be justified by this class
     lems.emplace_back(mkSkolemLemma(p.first, p.second, n));
   }
   if (nn != n)
   {
-    return TrustNode::mkTrustRewrite(n, nn, nullptr);
+    // we can provide a proof for the rewrite as well
+    return TrustNode::mkTrustRewrite(n, nn, this);
   }
   return TrustNode::null();
 }
@@ -441,11 +444,22 @@ Node OperatorElim::getAxiomFor(NodeManager* nm, const Node& n)
   std::vector<std::pair<Node, Node>> klems;
   bool wasNonLinear = false;
   Node nn = eliminateOperators(nm, n, klems, false, wasNonLinear);
-  if (klems.size() == 1)
+  if (nn==n)
   {
-    return klems[0].first;
+    return Node::null();
   }
-  return Node::null();
+  Node eqLem = n.eqNode(nn);
+  std::vector<Node> lemmas;
+  for (const std::pair<Node, Node>& kl : klems)
+  {
+    lemmas.emplace_back(kl.first);
+  }
+  if (!lemmas.empty())
+  {
+    Node axiom = nm->mkAnd(lemmas);
+    return nm->mkNode(Kind::AND, eqLem, axiom);
+  }
+  return eqLem;
 }
 
 Node OperatorElim::getArithSkolemApp(NodeManager* nm, Node n, SkolemId id)
@@ -482,16 +496,61 @@ SkolemLemma OperatorElim::mkSkolemLemma(const Node& lem,
 
 std::shared_ptr<ProofNode> OperatorElim::getProofFor(Node f)
 {
+  // This class provides proofs for two things:
+  // (1) rewrites n --> nn during preprocessing,
+  // (2) the axioms A added when rewriting n ---> nn.
+  // The proof rule ARITH_REDUCTION proves things of the form:
+  //    (and (= n nn) A)
+  // where A may be omitted. We first determine which case we are in (whether
+  // being asked for a proof of a preprocessing rewrite or an axiom) and store
+  // the target term (n above) into tgt.
   context::CDHashMap<Node, Node>::iterator it = d_lemmaMap.find(f);
+  Node tgt;
   if (it == d_lemmaMap.end())
   {
-    Assert(false) << "arith::OperatorElim could not prove " << f;
+    if (f.getKind()!=Kind::EQUAL)
+    {
+      Assert(false) << "arith::OperatorElim could not prove " << f;
+      return nullptr;
+    }
+    // target is the left hand side.
+    tgt = f[0];
+  }
+  else
+  {
+    // target was stored in d_lemmaMap for an axiom.
+    tgt = it->second;
+  }
+  CDProof cdp(d_env);
+  Node res = getAxiomFor(nodeManager(), tgt);
+  cdp.addStep(res, ProofRule::ARITH_REDUCTION, {}, {tgt});
+  bool success = false;
+  // If the axiom was an AND, then the fact in question should be one of the
+  // conjuncts, in which case we do an AND_ELIM step.
+  if (res.getKind()==Kind::AND)
+  {
+    Assert (res.getNumChildren()==2);
+    for (size_t i=0; i<2; i++)
+    {
+      if (res[i]==f)
+      {
+        Node ni = nodeManager()->mkConstInt(i);
+        cdp.addStep(f, ProofRule::AND_ELIM, {res}, {ni});
+        success = true;
+        break;
+      }
+    }
+  }
+  else
+  {
+    success = (res==f);
+  }
+  Assert(success) << "arith::OperatorElim could not prove " << f;
+  if (!success)
+  {
     return nullptr;
   }
-  ProofNodeManager* pnm = d_env.getProofNodeManager();
-  std::shared_ptr<ProofNode> pfn =
-      pnm->mkNode(ProofRule::ARITH_OP_ELIM_AXIOM, {}, {it->second}, f);
-  return pfn;
+  return cdp.getProofFor(f);
 }
 
 std::string OperatorElim::identify() const { return "arith::OperatorElim"; }

src/theory/arith/operator_elim.h

@@ -61,7 +61,7 @@ class OperatorElim : protected EnvObj, public ProofGenerator
   static Node getAxiomFor(NodeManager* nm, const Node& n);
   /**
    * Get proof for formula f, which should have been generated as a lemma
-   * via eliminate above.
+   * via eliminate above, or as a rewrite performed by eliminate.
    */
   std::shared_ptr<ProofNode> getProofFor(Node f) override;
   /** Identify this, for proof generator interface */
@@ -104,7 +104,12 @@ class OperatorElim : protected EnvObj, public ProofGenerator
    *
    * This method is called both during expandDefinition and during ppRewrite.
    *
+   * @param nm Pointer to the node manager
    * @param n The node to eliminate operators from.
+   * @param lems The lemmas storing (L, k) where L is the lemma and k is the 
+   * attached skolem it is associated with.
+   * @param partialOnly Whether we are only eliminating partial operators.
+   * @param wasNonLinear Set to true if n requires a non-linear logic.
    * @return The (single step) eliminated form of n.
    */
   static Node eliminateOperators(NodeManager* nm,
@@ -127,9 +132,6 @@ class OperatorElim : protected EnvObj, public ProofGenerator
    *
    * By default, this returns the term f( n ), where f is the Skolem function
    * for the identifier asi.
-   *
-   * If the option arithNoPartialFun is enabled, this returns f, where f is
-   * the Skolem constant for the identifier asi.
    */
   static Node getArithSkolemApp(NodeManager* nm, Node n, SkolemId asi);
 };

src/theory/arith/proof_checker.cpp

@@ -49,7 +49,7 @@ void ArithProofRuleChecker::registerTo(ProofChecker* pc)
   pc->registerChecker(ProofRule::ARITH_TRICHOTOMY, this);
   pc->registerChecker(ProofRule::INT_TIGHT_UB, this);
   pc->registerChecker(ProofRule::INT_TIGHT_LB, this);
-  pc->registerChecker(ProofRule::ARITH_OP_ELIM_AXIOM, this);
+  pc->registerChecker(ProofRule::ARITH_REDUCTION, this);
   pc->registerChecker(ProofRule::ARITH_MULT_POS, this);
   pc->registerChecker(ProofRule::ARITH_MULT_NEG, this);
   pc->registerChecker(ProofRule::ARITH_POLY_NORM, this);
@@ -389,7 +389,7 @@ Node ArithProofRuleChecker::checkInternal(ProofRule id,
       }
       // Check that all have the same constant:
     }
-    case ProofRule::ARITH_OP_ELIM_AXIOM:
+    case ProofRule::ARITH_REDUCTION:
     {
       Assert(children.empty());
       Assert(args.size() == 1);

test/regress/cli/regress1/nl/arctan2-expdef.smt2

@@ -1,6 +1,5 @@
 (set-logic QF_NRAT)
 (set-info :status unsat)
-(set-option :arith-no-partial-fun true)
 (declare-fun lat1 () Real)
 (declare-fun lat2 () Real)
 

test/regress/cli/regress1/nl/issue7924-sqrt-partial.smt2

@@ -1,4 +1,4 @@
-; COMMAND-LINE: --arith-no-partial-fun -q
+; COMMAND-LINE: -q
 ; EXPECT: sat
 (set-logic ALL)
 (assert (exists ((V Real)) (distinct (sqrt 1.0) (sqrt 0.0))))