Internally remove redundant assertions and infer equalities in NonLinearExtension (#1633)

1 files changed, 16 insertions, 2 deletions

diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h
index a37ef97f8..96d37cbc2 100644
--- a/src/theory/arith/nonlinear_extension.h
+++ b/src/theory/arith/nonlinear_extension.h
@@ -245,6 +245,17 @@ class NonlinearExtension {
   void assignOrderIds(std::vector<Node>& vars, NodeMultiset& d_order,
                       unsigned orderType);
 
+  /** get assertions
+   *
+   * Let M be the set of assertions known by THEORY_ARITH. This function adds a
+   * set of literals M' to assertions such that M' and M are equivalent.
+   *
+   * Examples of how M' differs with M:
+   * (1) M' may not include t < c (in M) if t < c' is in M' for c' < c, where
+   * c and c' are constants,
+   * (2) M' may contain t = c if both t >= c and t <= c are in M.
+   */
+  void getAssertions(std::vector<Node>& assertions);
   /** check model
    *
    * Returns the subset of assertions whose concrete values we cannot show are
@@ -700,7 +711,9 @@ private:
   *      that occur in the current context.
   */
   std::vector<Node> checkMonomialInferBounds(
-      std::vector<Node>& nt_lemmas, const std::vector<Node>& false_asserts);
+      std::vector<Node>& nt_lemmas,
+      const std::vector<Node>& asserts,
+      const std::vector<Node>& false_asserts);
 
   /** check factoring
   *
@@ -714,7 +727,8 @@ private:
   *   ...where k is fresh and x*z + y*z > t is a
   *      constraint that occurs in the current context.
   */
-  std::vector<Node> checkFactoring(const std::vector<Node>& false_asserts);
+  std::vector<Node> checkFactoring(const std::vector<Node>& asserts,
+                                   const std::vector<Node>& false_asserts);
 
   /** check monomial infer resolution bounds
   *