From 2117152db35fe1e8cee1632303789dceda311d1a Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Mon, 28 Sep 2020 13:48:26 +0200 Subject: [PATCH] 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. --- src/CMakeLists.txt | 4 +- src/theory/arith/bound_inference.cpp | 158 ++++++++++++++++++ .../variable_bounds.h => bound_inference.h} | 64 +++---- src/theory/arith/nl/icp/icp_solver.cpp | 6 +- src/theory/arith/nl/icp/icp_solver.h | 8 +- src/theory/arith/nl/icp/variable_bounds.cpp | 158 ------------------ src/theory/arith/nl/poly_conversion.cpp | 15 ++ src/theory/arith/nl/poly_conversion.h | 3 + 8 files changed, 219 insertions(+), 197 deletions(-) create mode 100644 src/theory/arith/bound_inference.cpp rename src/theory/arith/{nl/icp/variable_bounds.h => bound_inference.h} (59%) delete mode 100644 src/theory/arith/nl/icp/variable_bounds.cpp 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() < value.getConst()) + { + 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() > value.getConst()) + { + 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& 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> getBounds(const std::vector& assertions) { + BoundInference bi; + for (const auto& a: assertions) { + bi.add(a); + } + std::map> 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 similarity index 59% rename from src/theory/arith/nl/icp/variable_bounds.h rename to 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 +#ifndef CVC4__THEORY__ARITH__BOUND_INFERENCE_H +#define CVC4__THEORY__ARITH__BOUND_INFERENCE_H #include +#include #include #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 d_intervals; + std::map 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& 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> getBounds(const std::vector& 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& 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 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 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 #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 -- 2.30.2