(proof-new) proofs for arith-constraint explanations (#5224)

Threads proofs through arith::Constraint's machinery for explaining
constraints. Changes, by function:

externalExplainByAssertions:
introduce scope to prove the implication
externalExplainForPropagation:
introduce scope to prove the implication
externalExplainConflict:
use other machinery to prove conflicting constraints
use the CONTRA rule
introduce scope to close the conflict proof
Future commits will pick up these proofs in theory_arith_private.cpp.
Future commits will prove the "split" lemmas produced in constraint.cpp

1 files changed, 12 insertions, 13 deletions

diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index 05845ec76..02bc3c988 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -553,9 +553,7 @@ class Constraint {
    * This is the minimum fringe of the implication tree s.t.
    * every constraint is assertedToTheTheory() or hasEqualityEngineProof().
    */
-  Node externalExplainByAssertions() const {
-    return externalExplain(AssertionOrderSentinel);
-  }
+  TrustNode externalExplainByAssertions() const;
 
   /**
    * Writes an explanation of a constraint into the node builder.
@@ -598,22 +596,19 @@ class Constraint {
    * The constraint must have a proof.
    * The constraint cannot be an assumption.
    *
-   * This is the minimum fringe of the implication tree (excluding the constraint itself)
-   * s.t. every constraint is assertedToTheTheory() or hasEqualityEngineProof().
+   * This is the minimum fringe of the implication tree (excluding the
+   * constraint itself) s.t. every constraint is assertedToTheTheory() or
+   * hasEqualityEngineProof().
+   *
+   * All return conjuncts were asserted before this constraint.
    */
-  Node externalExplainForPropagation() const {
-    Assert(hasProof());
-    Assert(!isAssumption());
-    Assert(!isInternalAssumption());
-    return externalExplain(d_assertionOrder);
-  }
+  TrustNode externalExplainForPropagation() const;
 
   /**
    * Explain the constraint and its negation in terms of assertions.
    * The constraint must be in conflict.
    */
-  Node externalExplainConflict() const;
-
+  TrustNode externalExplainConflict() const;
 
   /** The constraint is known to be true. */
   inline bool hasProof() const {
@@ -1155,7 +1150,11 @@ private:
   bool variableDatabaseIsSetup(ArithVar v) const;
   void removeVariable(ArithVar v);
 
+  /** Get an explanation and proof for this constraint from the equality engine
+   */
   TrustNode eeExplain(ConstraintCP c) const;
+  /** Get an explanation for this constraint from the equality engine */
+  void eeExplain(ConstraintCP c, NodeBuilder<>& nb) const;
 
   /**
    * Returns a constraint with the variable v, the constraint type t, and a value