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.
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
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
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \file bound_inference.h
+ ** \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 Extract bounds on variables from theory atoms.
+ **/
+
+#ifndef CVC4__THEORY__ARITH__BOUND_INFERENCE_H
+#define CVC4__THEORY__ARITH__BOUND_INFERENCE_H
+
+#include <map>
+#include <utility>
+#include <vector>
+
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+ 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 BoundInference
+{
+ /** The currently strictest bounds for every variable. */
+ 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 Node& value,
+ bool strict);
+ /** Updates the upper bound for the given variable */
+ void update_upper_bound(const Node& origin,
+ const Node& variable,
+ const Node& value,
+ bool strict);
+
+ public:
+ void reset();
+
+ /**
+ * Get the current interval for v. Creates a new (full) interval if
+ * necessary.
+ */
+ Bounds& get_or_add(const Node& v);
+ /**
+ * Get the current interval for v. Returns a full interval if no interval was
+ * derived yet.
+ */
+ Bounds get(const Node& v) const;
+
+ /** Return the current variable bounds as an interval assignment. */
+ const std::map<Node, Bounds>& get() const;
+
+ /**
+ * Add a new theory atom. Return true if the theory atom induces a new
+ * variable bound.
+ */
+ bool add(const Node& n);
+};
+
+/** Print the current variable bounds. */
+std::ostream& operator<<(std::ostream& os, const BoundInference& bi);
+
+std::map<Node, std::pair<Node,Node>> getBounds(const std::vector<Node>& assertions);
+
+} // namespace arith
+} // namespace theory
+} // namespace CVC4
+
+#endif
\ No newline at end of file
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())
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
#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 {
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 */
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();
+++ /dev/null
-/********************* */
-/*! \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
+++ /dev/null
-/********************* */
-/*! \file variable_bounds.h
- ** \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 Extract bounds on variable 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>
-
-#include <map>
-#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 {
-
-/**
- * A utility class that extracts direct bounds on single variables from theory
- * atoms.
- */
-class VariableBounds
-{
- /** 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;
-
- /** Updates the lower bound for the given variable */
- void update_lower_bound(const Node& origin,
- const Node& variable,
- const poly::Value& 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,
- 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);
- /**
- * Get the current interval for v. Returns a full interval if no interval was
- * derived yet.
- */
- Interval get(const Node& v) const;
-
- /** Return the current variable bounds as an interval assignment. */
- poly::IntervalAssignment get() const;
-
- /**
- * Add a new theory atom. Return true if the theory atom induces a new
- * variable bound.
- */
- bool add(const Node& n);
-};
-
-/** Print the current variable bounds. */
-std::ostream& operator<<(std::ostream& os, const VariableBounds& vb);
-
-} // namespace icp
-} // namespace nl
-} // namespace arith
-} // namespace theory
-} // namespace CVC4
-
-#endif
-
-#endif
\ No newline at end of file
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
#include <iostream>
#include "expr/node.h"
+#include "theory/arith/bound_inference.h"
#include "util/real_algebraic_number.h"
namespace CVC4 {
*/
std::size_t bitsize(const poly::Value& v);
+poly::IntervalAssignment getBounds(VariableMapper& vm, const BoundInference& bi);
+
} // namespace nl
} // namespace arith
} // namespace theory
projects / cvc5.git / commitdiff