Add new arithmetic BoundInference class (#5148)

This PR adds a new utility class that extracts bounds on single variables from theory atoms like x > 0 or y <= 17. It does not perform further reasoning (like recognizing x > y with y > 3 as a bound).
Note that the functionality was introduced in arith/nl/icp/variable_bounds.h, but is now available using Node only.
This PR also replaces the VariableBounds by BoundInference in the icp solver which allowed for checking the code.

8 files changed, 219 insertions, 197 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index db274ebfb..717378b27 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -290,6 +290,8 @@ libcvc4_add_sources(
   theory/arith/attempt_solution_simplex.cpp
   theory/arith/attempt_solution_simplex.h
   theory/arith/bound_counts.h
+  theory/arith/bound_inference.cpp
+  theory/arith/bound_inference.h
   theory/arith/callbacks.cpp
   theory/arith/callbacks.h
   theory/arith/congruence_manager.cpp
@@ -343,8 +345,6 @@ libcvc4_add_sources(
   theory/arith/nl/icp/icp_solver.h
   theory/arith/nl/icp/intersection.cpp
   theory/arith/nl/icp/intersection.h
-  theory/arith/nl/icp/variable_bounds.cpp
-  theory/arith/nl/icp/variable_bounds.h
   theory/arith/nl/nl_constraint.cpp
   theory/arith/nl/nl_constraint.h
   theory/arith/nl/nl_lemma_utils.cpp
diff --git a/src/theory/arith/bound_inference.cpp b/src/theory/arith/bound_inference.cpp
new file mode 100644
index 000000000..5a1c30966
--- /dev/null
+++ b/src/theory/arith/bound_inference.cpp
@@ -0,0 +1,158 @@
+/*********************                                                        */
+/*! \file bound_inference.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Gereon Kremer
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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.\endverbatim
+ **
+ ** \brief
+ **/
+
+#include "theory/arith/bound_inference.h"
+
+#include "theory/arith/normal_form.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+std::ostream& operator<<(std::ostream& os, const Bounds& b) {
+
+  return os << (b.lower_strict ? '(' : '[') << b.lower << " .. " << b.upper
+            << (b.upper_strict ? ')' : ']');
+
+}
+
+void BoundInference::update_lower_bound(const Node& origin,
+                                        const Node& variable,
+                                        const Node& value,
+                                        bool strict)
+{
+  // variable > or >= value because of origin
+  Trace("nl-icp") << "\tNew bound " << variable << (strict ? ">" : ">=")
+                  << value << " due to " << origin << std::endl;
+  Bounds& b = get_or_add(variable);
+  if (b.lower.isNull() || b.lower.getConst<Rational>() < value.getConst<Rational>())
+  {
+    b.lower = value;
+    b.lower_strict = strict;
+    b.lower_origin = origin;
+  }
+  else if (strict && b.lower == value)
+  {
+    b.lower_strict = strict;
+    b.lower_origin = origin;
+  }
+}
+void BoundInference::update_upper_bound(const Node& origin,
+                                        const Node& variable,
+                                        const Node& value,
+                                        bool strict)
+{
+  // variable < or <= value because of origin
+  Trace("nl-icp") << "\tNew bound " << variable << (strict ? "<" : "<=")
+                  << value << " due to " << origin << std::endl;
+  Bounds& b = get_or_add(variable);
+  if (b.upper.isNull() || b.upper.getConst<Rational>() > value.getConst<Rational>())
+  {
+    b.upper = value;
+    b.upper_strict = strict;
+    b.upper_origin = origin;
+  }
+  else if (strict && b.upper == value)
+  {
+    b.upper_strict = strict;
+    b.upper_origin = origin;
+  }
+}
+
+void BoundInference::reset() { d_bounds.clear(); }
+
+Bounds& BoundInference::get_or_add(const Node& v)
+{
+  auto it = d_bounds.find(v);
+  if (it == d_bounds.end())
+  {
+    it = d_bounds.emplace(v, Bounds()).first;
+  }
+  return it->second;
+}
+Bounds BoundInference::get(const Node& v) const
+{
+  auto it = d_bounds.find(v);
+  if (it == d_bounds.end())
+  {
+    return Bounds{};
+  }
+  return it->second;
+}
+
+const std::map<Node, Bounds>& BoundInference::get() const { return d_bounds; }
+bool BoundInference::add(const Node& n)
+{
+  // Parse the node as a comparison
+  auto comp = Comparison::parseNormalForm(n);
+  auto dec = comp.decompose(true);
+  if (std::get<0>(dec).isVariable())
+  {
+    Variable v = std::get<0>(dec).getVariable();
+    Kind relation = std::get<1>(dec);
+    if (relation == Kind::DISTINCT) return false;
+    Constant bound = std::get<2>(dec);
+    // has the form  v  ~relation~  bound
+
+    switch (relation)
+    {
+      case Kind::LEQ:
+        update_upper_bound(n, v.getNode(), bound.getNode(), false);
+        break;
+      case Kind::LT:
+        update_upper_bound(n, v.getNode(), bound.getNode(), true);
+        break;
+      case Kind::EQUAL:
+        update_lower_bound(n, v.getNode(), bound.getNode(), false);
+        update_upper_bound(n, v.getNode(), bound.getNode(), false);
+        break;
+      case Kind::GT:
+        update_lower_bound(n, v.getNode(), bound.getNode(), true);
+        break;
+      case Kind::GEQ:
+        update_lower_bound(n, v.getNode(), bound.getNode(), false);
+        break;
+      default: Assert(false);
+    }
+    return true;
+  }
+  return false;
+}
+
+std::ostream& operator<<(std::ostream& os, const BoundInference& bi)
+{
+  os << "Bounds:" << std::endl;
+  for (const auto& vb : bi.get())
+  {
+    os << "\t" << vb.first << " -> " << vb.second.lower << ".."
+       << vb.second.upper << std::endl;
+  }
+  return os;
+}
+
+std::map<Node, std::pair<Node,Node>> getBounds(const std::vector<Node>& assertions) {
+  BoundInference bi;
+  for (const auto& a: assertions) {
+    bi.add(a);
+  }
+  std::map<Node, std::pair<Node,Node>> res;
+  for (const auto& vb: bi.get()) {
+    res.emplace(vb.first, std::make_pair(vb.second.lower, vb.second.upper));
+  }
+  return res;
+}
+
+}  // namespace arith
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/arith/nl/icp/variable_bounds.h b/src/theory/arith/bound_inference.h
index 256054538..b360ad421 100644
--- a/src/theory/arith/nl/icp/variable_bounds.h
+++ b/src/theory/arith/bound_inference.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file variable_bounds.h
+/*! \file bound_inference.h
  ** \verbatim
  ** Top contributors (to current version):
  **   Gereon Kremer
@@ -9,71 +9,77 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Extract bounds on variable from theory atoms.
+ ** \brief Extract bounds on variables from theory atoms.
  **/
 
-#ifndef CVC4__THEORY__ARITH__ICP__VARIABLE_BOUNDS_H
-#define CVC4__THEORY__ARITH__ICP__VARIABLE_BOUNDS_H
-
-#include "util/real_algebraic_number.h"
-
-#ifdef CVC4_POLY_IMP
-#include <poly/polyxx.h>
+#ifndef CVC4__THEORY__ARITH__BOUND_INFERENCE_H
+#define CVC4__THEORY__ARITH__BOUND_INFERENCE_H
 
 #include <map>
+#include <utility>
 #include <vector>
 
 #include "expr/node.h"
-#include "theory/arith/nl/icp/interval.h"
-#include "theory/arith/nl/poly_conversion.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
-namespace nl {
-namespace icp {
+
+  struct Bounds
+  {
+    /** The lower bound */
+    Node lower;
+    /** Whether the lower bound is strict or weak */
+    bool lower_strict = true;
+    /** The origin of the lower bound */
+    Node lower_origin;
+    /** The upper bound */
+    Node upper;
+    /** Whether the upper bound is strict or weak */
+    bool upper_strict = true;
+    /** The origin of the upper bound */
+    Node upper_origin;
+  };
+
+/** Print the current variable bounds. */
+std::ostream& operator<<(std::ostream& os, const Bounds& b);
 
 /**
  * A utility class that extracts direct bounds on single variables from theory
  * atoms.
  */
-class VariableBounds
+class BoundInference
 {
-  /** A reference to a mapper from cvc nodes to poly variables. */
-  VariableMapper& d_mapper;
   /** The currently strictest bounds for every variable. */
-  std::map<Node, Interval> d_intervals;
+  std::map<Node, Bounds> d_bounds;
 
   /** Updates the lower bound for the given variable */
   void update_lower_bound(const Node& origin,
                           const Node& variable,
-                          const poly::Value& value,
+                          const Node& value,
                           bool strict);
   /** Updates the upper bound for the given variable */
   void update_upper_bound(const Node& origin,
                           const Node& variable,
-                          const poly::Value& value,
+                          const Node& value,
                           bool strict);
 
  public:
-  VariableBounds(VariableMapper& mapper) : d_mapper(mapper) {}
-  const VariableMapper& getMapper() const { return d_mapper; }
-  /** Reset the bounds */
   void reset();
 
   /**
    * Get the current interval for v. Creates a new (full) interval if
    * necessary.
    */
-  Interval& get(const Node& v);
+  Bounds& get_or_add(const Node& v);
   /**
    * Get the current interval for v. Returns a full interval if no interval was
    * derived yet.
    */
-  Interval get(const Node& v) const;
+  Bounds get(const Node& v) const;
 
   /** Return the current variable bounds as an interval assignment. */
-  poly::IntervalAssignment get() const;
+  const std::map<Node, Bounds>& get() const;
 
   /**
    * Add a new theory atom. Return true if the theory atom induces a new
@@ -83,14 +89,12 @@ class VariableBounds
 };
 
 /** Print the current variable bounds. */
-std::ostream& operator<<(std::ostream& os, const VariableBounds& vb);
+std::ostream& operator<<(std::ostream& os, const BoundInference& bi);
+
+std::map<Node, std::pair<Node,Node>> getBounds(const std::vector<Node>& assertions);
 
-}  // namespace icp
-}  // namespace nl
 }  // namespace arith
 }  // namespace theory
 }  // namespace CVC4
 
-#endif
-
 #endif
\ No newline at end of file
diff --git a/src/theory/arith/nl/icp/icp_solver.cpp b/src/theory/arith/nl/icp/icp_solver.cpp
index ea9fc8f41..43905d802 100644
--- a/src/theory/arith/nl/icp/icp_solver.cpp
+++ b/src/theory/arith/nl/icp/icp_solver.cpp
@@ -180,9 +180,9 @@ void ICPSolver::addCandidate(const Node& n)
 
 void ICPSolver::initOrigins()
 {
-  for (const auto& vars : d_mapper.mVarCVCpoly)
+  for (const auto& vars : d_state.d_bounds.get())
   {
-    auto& i = d_state.d_bounds.get(vars.first);
+    const Bounds& i = vars.second;
     Trace("nl-icp") << "Adding initial " << vars.first << " -> " << i
                     << std::endl;
     if (!i.lower_origin.isNull())
@@ -320,7 +320,7 @@ void ICPSolver::reset(const std::vector<Node>& assertions)
 void ICPSolver::check()
 {
   initOrigins();
-  d_state.d_assignment = d_state.d_bounds.get();
+  d_state.d_assignment = getBounds(d_mapper, d_state.d_bounds);
   bool did_progress = false;
   bool progress = false;
   do
diff --git a/src/theory/arith/nl/icp/icp_solver.h b/src/theory/arith/nl/icp/icp_solver.h
index 61429b5a2..ca2aef10a 100644
--- a/src/theory/arith/nl/icp/icp_solver.h
+++ b/src/theory/arith/nl/icp/icp_solver.h
@@ -22,11 +22,11 @@
 #endif /* CVC4_POLY_IMP */
 
 #include "expr/node.h"
+#include "theory/arith/bound_inference.h"
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/icp/candidate.h"
 #include "theory/arith/nl/icp/contraction_origins.h"
 #include "theory/arith/nl/icp/intersection.h"
-#include "theory/arith/nl/icp/variable_bounds.h"
 #include "theory/arith/nl/poly_conversion.h"
 
 namespace CVC4 {
@@ -60,7 +60,7 @@ class ICPSolver
   struct ICPState
   {
     /** The variable bounds extracted from the input assertions */
-    VariableBounds d_bounds;
+    BoundInference d_bounds;
     /** The contraction candidates generated from the theory atoms */
     std::vector<Candidate> d_candidates;
     /** The current assignment */
@@ -71,12 +71,12 @@ class ICPSolver
     Node d_conflict;
 
     /** Initialized the variable bounds with a variable mapper */
-    ICPState(VariableMapper& vm) : d_bounds(vm) {}
+    ICPState(VariableMapper& vm) {}
 
     /** Reset this state */
     void reset()
     {
-      d_bounds.reset();
+      d_bounds = BoundInference();
       d_candidates.clear();
       d_assignment.clear();
       d_origins = ContractionOriginManager();
diff --git a/src/theory/arith/nl/icp/variable_bounds.cpp b/src/theory/arith/nl/icp/variable_bounds.cpp
deleted file mode 100644
index 14007971a..000000000
--- a/src/theory/arith/nl/icp/variable_bounds.cpp
+++ /dev/null
@@ -1,158 +0,0 @@
-/*********************                                                        */
-/*! \file variable_bounds.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Gereon Kremer
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 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.\endverbatim
- **
- ** \brief
- **/
-
-#include "theory/arith/nl/icp/variable_bounds.h"
-
-#ifdef CVC4_POLY_IMP
-
-#include "theory/arith/normal_form.h"
-#include "util/poly_util.h"
-
-namespace CVC4 {
-namespace theory {
-namespace arith {
-namespace nl {
-namespace icp {
-
-void VariableBounds::update_lower_bound(const Node& origin,
-                                        const Node& variable,
-                                        const poly::Value& value,
-                                        bool strict)
-{
-  // variable > or >= value because of origin
-  Trace("nl-icp") << "\tNew bound " << variable << (strict ? ">" : ">=")
-                  << value << " due to " << origin << std::endl;
-  Interval& i = get(variable);
-  if (poly::is_none(i.lower) || i.lower < value)
-  {
-    i.lower = value;
-    i.lower_strict = strict;
-    i.lower_origin = origin;
-  }
-  else if (strict && i.lower == value)
-  {
-    i.lower_strict = strict;
-    i.lower_origin = origin;
-  }
-}
-void VariableBounds::update_upper_bound(const Node& origin,
-                                        const Node& variable,
-                                        const poly::Value& value,
-                                        bool strict)
-{
-  // variable < or <= value because of origin
-  Trace("nl-icp") << "\tNew bound " << variable << (strict ? "<" : "<=")
-                  << value << " due to " << origin << std::endl;
-  Interval& i = get(variable);
-  if (poly::is_none(i.upper) || i.upper > value)
-  {
-    i.upper = value;
-    i.upper_strict = strict;
-    i.upper_origin = origin;
-  }
-  else if (strict && i.upper == value)
-  {
-    i.upper_strict = strict;
-    i.upper_origin = origin;
-  }
-}
-
-void VariableBounds::reset() { d_intervals.clear(); }
-
-Interval& VariableBounds::get(const Node& v)
-{
-  auto it = d_intervals.find(v);
-  if (it == d_intervals.end())
-  {
-    it = d_intervals.emplace(v, Interval()).first;
-  }
-  return it->second;
-}
-Interval VariableBounds::get(const Node& v) const
-{
-  auto it = d_intervals.find(v);
-  if (it == d_intervals.end())
-  {
-    return Interval{};
-  }
-  return it->second;
-}
-
-poly::IntervalAssignment VariableBounds::get() const
-{
-  poly::IntervalAssignment res;
-  for (const auto& vi : d_intervals)
-  {
-    poly::Variable v = d_mapper(vi.first);
-    poly::Interval i(vi.second.lower,
-                     vi.second.lower_strict,
-                     vi.second.upper,
-                     vi.second.upper_strict);
-    res.set(v, i);
-  }
-  return res;
-}
-bool VariableBounds::add(const Node& n)
-{
-  // Parse the node as a comparison
-  auto comp = Comparison::parseNormalForm(n);
-  auto dec = comp.decompose(true);
-  if (std::get<0>(dec).isVariable())
-  {
-    Variable v = std::get<0>(dec).getVariable();
-    Kind relation = std::get<1>(dec);
-    if (relation == Kind::DISTINCT) return false;
-    Constant bound = std::get<2>(dec);
-    // has the form  v  ~relation~  bound
-
-    poly::Value val = node_to_value(bound.getNode(), v.getNode());
-    poly::Interval newi = poly::Interval::full();
-
-    Maybe<Node> res;
-    switch (relation)
-    {
-      case Kind::LEQ: update_upper_bound(n, v.getNode(), val, false); break;
-      case Kind::LT: update_upper_bound(n, v.getNode(), val, true); break;
-      case Kind::EQUAL:
-        update_lower_bound(n, v.getNode(), val, false);
-        update_upper_bound(n, v.getNode(), val, false);
-        break;
-      case Kind::GT: update_lower_bound(n, v.getNode(), val, true); break;
-      case Kind::GEQ: update_lower_bound(n, v.getNode(), val, false); break;
-      default: Assert(false);
-    }
-    d_mapper(v.getNode());
-    return true;
-  }
-  return false;
-}
-
-std::ostream& operator<<(std::ostream& os, const VariableBounds& vb)
-{
-  os << "Bounds:" << std::endl;
-  for (const auto& var : vb.getMapper().mVarCVCpoly)
-  {
-    os << "\t" << var.first << " -> " << vb.get(var.first) << std::endl;
-    ;
-  }
-  return os;
-}
-
-}  // namespace icp
-}  // namespace nl
-}  // namespace arith
-}  // namespace theory
-}  // namespace CVC4
-
-#endif
diff --git a/src/theory/arith/nl/poly_conversion.cpp b/src/theory/arith/nl/poly_conversion.cpp
index c35b07a40..1280f9c8e 100644
--- a/src/theory/arith/nl/poly_conversion.cpp
+++ b/src/theory/arith/nl/poly_conversion.cpp
@@ -715,6 +715,21 @@ std::size_t bitsize(const poly::Value& v)
   return 0;
 }
 
+poly::IntervalAssignment getBounds(VariableMapper& vm, const BoundInference& bi) {
+  poly::IntervalAssignment res;
+  for (const auto& vb: bi.get()) {
+    poly::Variable v = vm(vb.first);
+    poly::Value l = vb.second.lower.isNull() ? poly::Value::minus_infty() : node_to_value(vb.second.lower, vb.first);
+    poly::Value u = vb.second.upper.isNull() ? poly::Value::plus_infty() : node_to_value(vb.second.upper, vb.first);
+    poly::Interval i(l,
+                     vb.second.lower_strict,
+                     u,
+                     vb.second.upper_strict);
+    res.set(v, i);
+  }
+  return res;
+}
+
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
diff --git a/src/theory/arith/nl/poly_conversion.h b/src/theory/arith/nl/poly_conversion.h
index fee20e71f..b4d44c39d 100644
--- a/src/theory/arith/nl/poly_conversion.h
+++ b/src/theory/arith/nl/poly_conversion.h
@@ -26,6 +26,7 @@
 #include <iostream>
 
 #include "expr/node.h"
+#include "theory/arith/bound_inference.h"
 #include "util/real_algebraic_number.h"
 
 namespace CVC4 {
@@ -143,6 +144,8 @@ poly::Value node_to_value(const Node& n, const Node& ran_variable);
  */
 std::size_t bitsize(const poly::Value& v);
 
+poly::IntervalAssignment getBounds(VariableMapper& vm, const BoundInference& bi);
+
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory