diff options
22 files changed, 1709 insertions, 2 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index a72a5f6bb..a868a6ab5 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -323,6 +323,16 @@ libcvc4_add_sources( theory/arith/nl/ext_theory_callback.h theory/arith/nl/iand_solver.cpp theory/arith/nl/iand_solver.h + theory/arith/nl/icp/candidate.cpp + theory/arith/nl/icp/candidate.h + theory/arith/nl/icp/contraction_origins.cpp + theory/arith/nl/icp/contraction_origins.h + theory/arith/nl/icp/icp_solver.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 diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml index ab33f123c..fde48d3f7 100644 --- a/src/options/arith_options.toml +++ b/src/options/arith_options.toml @@ -568,3 +568,11 @@ header = "options/arith_options.h" default = "false" help = "whether to use the cylindrical algebraic decomposition solver for non-linear arithmetic" +[[option]] + name = "nlICP" + category = "regular" + long = "nl-icp" + type = "bool" + default = "false" + help = "whether to use ICP-style propagations for non-linear arithmetic" + diff --git a/src/theory/arith/inference_id.h b/src/theory/arith/inference_id.h index 56aeb3d24..fa330313d 100644 --- a/src/theory/arith/inference_id.h +++ b/src/theory/arith/inference_id.h @@ -76,6 +76,11 @@ enum class InferenceId : uint32_t NL_CAD_CONFLICT, // excludes an interval for a single variable NL_CAD_EXCLUDED_INTERVAL, + //-------------------- icp solver + // conflict obtained from icp + NL_ICP_CONFLICT, + // propagation / contraction of variable bounds from icp + NL_ICP_PROPAGATION, //-------------------- unknown UNKNOWN, }; diff --git a/src/theory/arith/nl/icp/candidate.cpp b/src/theory/arith/nl/icp/candidate.cpp new file mode 100644 index 000000000..df8e18818 --- /dev/null +++ b/src/theory/arith/nl/icp/candidate.cpp @@ -0,0 +1,120 @@ +/********************* */ +/*! \file candidate.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/candidate.h" + +#ifdef CVC4_POLY_IMP + +#include <iostream> + +#include "base/check.h" +#include "base/output.h" +#include "theory/arith/nl/icp/intersection.h" +#include "theory/arith/nl/poly_conversion.h" + +namespace CVC4 { +namespace theory { +namespace arith { +namespace nl { +namespace icp { + +PropagationResult Candidate::propagate(poly::IntervalAssignment& ia, + std::size_t size_threshold) const +{ + // Evaluate the right hand side + auto res = poly::evaluate(rhs, ia) * poly::Interval(poly::Value(rhsmult)); + if (get_lower(res) == poly::Value::minus_infty() + && get_upper(res) == poly::Value::plus_infty()) + { + return PropagationResult::NOT_CHANGED; + } + Trace("nl-icp") << "Prop: " << *this << " -> " << res << std::endl; + // Remove bounds based on the sign condition + switch (rel) + { + case poly::SignCondition::LT: + res.set_lower(poly::Value::minus_infty(), true); + res.set_upper(get_upper(res), true); + break; + case poly::SignCondition::LE: + res.set_lower(poly::Value::minus_infty(), true); + break; + case poly::SignCondition::EQ: break; + case poly::SignCondition::NE: Assert(false); break; + case poly::SignCondition::GT: + res.set_lower(get_lower(res), true); + res.set_upper(poly::Value::plus_infty(), true); + break; + case poly::SignCondition::GE: + res.set_upper(poly::Value::plus_infty(), true); + break; + } + // Get the current interval for lhs + auto cur = ia.get(lhs); + + // Update the current interval + PropagationResult result = intersect_interval_with(cur, res, size_threshold); + // Check for strong propagations + switch (result) + { + case PropagationResult::CONTRACTED: + case PropagationResult::CONTRACTED_WITHOUT_CURRENT: + { + Trace("nl-icp") << *this << " contracted " << lhs << " -> " << cur + << std::endl; + auto old = ia.get(lhs); + bool strong = false; + strong = strong + || (is_minus_infinity(get_lower(old)) + && !is_minus_infinity(get_lower(cur))); + strong = strong + || (is_plus_infinity(get_upper(old)) + && !is_plus_infinity(get_upper(cur))); + ia.set(lhs, cur); + if (strong) + { + if (result == PropagationResult::CONTRACTED) + { + result = PropagationResult::CONTRACTED_STRONGLY; + } + else if (result == PropagationResult::CONTRACTED_WITHOUT_CURRENT) + { + result = PropagationResult::CONTRACTED_STRONGLY_WITHOUT_CURRENT; + } + } + break; + } + case PropagationResult::CONTRACTED_STRONGLY: + case PropagationResult::CONTRACTED_STRONGLY_WITHOUT_CURRENT: + Assert(false) << "This method should not return strong flags."; + break; + default: break; + } + return result; +} + +std::ostream& operator<<(std::ostream& os, const Candidate& c) +{ + os << c.lhs << " " << c.rel << " "; + if (c.rhsmult != poly::Rational(1)) os << c.rhsmult << " * "; + return os << c.rhs; +} + +} // namespace icp +} // namespace nl +} // namespace arith +} // namespace theory +} // namespace CVC4 + +#endif diff --git a/src/theory/arith/nl/icp/candidate.h b/src/theory/arith/nl/icp/candidate.h new file mode 100644 index 000000000..7980e5c97 --- /dev/null +++ b/src/theory/arith/nl/icp/candidate.h @@ -0,0 +1,85 @@ +/********************* */ +/*! \file candidate.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 Represents a contraction candidate for ICP-style propagation. + **/ + +#ifndef CVC4__THEORY__ARITH__ICP__CANDIDATE_H +#define CVC4__THEORY__ARITH__ICP__CANDIDATE_H + +#include "util/real_algebraic_number.h" + +#ifdef CVC4_POLY_IMP +#include <poly/polyxx.h> + +#include "expr/node.h" +#include "theory/arith/nl/icp/intersection.h" + +namespace CVC4 { +namespace theory { +namespace arith { +namespace nl { +namespace icp { + +/** + * A contraction candidate for ICP-style propagation with the following + * semantics: + * + * lhs ~rel~ rhsmult*rhs + * + * where lhs is the variable whose interval we aim to contract, rel is a + * relation symbol (other than disequality), rhsmult is a fractional constant + * and rhs a polynomial. As poly::Polynomial only holds integer polynomials, + * rhsmult is necessary to encode polynomials with rational coefficients. + * + * Additionally, we store the origin of this constraints (a single theory + * constraint) and the variables contained in rhs. + * + * A candidate is evaluated (or propagated) by evaluating the rhsmult*rhs over + * an interval assignment and then updating the interval assignment for lhs with + * the result of this evaluation, properly considering the relation. + */ +struct Candidate +{ + /** The target variable */ + poly::Variable lhs; + /** The relation symbol */ + poly::SignCondition rel; + /** The (integer) polynomial on the right hand side */ + poly::Polynomial rhs; + /** The rational multiplier */ + poly::Rational rhsmult; + /** The origin of this candidate */ + Node origin; + /** The variable within rhs */ + std::vector<Node> rhsVariables; + + /** + * Contract the interval assignment based on this candidate. + * Only contract if the new interval is below the given threshold, see + * intersect_interval_with(). + */ + PropagationResult propagate(poly::IntervalAssignment& ia, + std::size_t size_threshold) const; +}; + +/** Print a candidate. */ +std::ostream& operator<<(std::ostream& os, const Candidate& c); + +} // namespace icp +} // namespace nl +} // namespace arith +} // namespace theory +} // namespace CVC4 + +#endif + +#endif diff --git a/src/theory/arith/nl/icp/contraction_origins.cpp b/src/theory/arith/nl/icp/contraction_origins.cpp new file mode 100644 index 000000000..1e8f0769a --- /dev/null +++ b/src/theory/arith/nl/icp/contraction_origins.cpp @@ -0,0 +1,124 @@ +/********************* */ +/*! \file contraction_origins.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/contraction_origins.h" + +namespace CVC4 { +namespace theory { +namespace arith { +namespace nl { +namespace icp { + +void ContractionOriginManager::getOrigins(ContractionOrigin const* const origin, + std::set<Node>& res) const +{ + if (!origin->candidate.isNull()) + { + res.insert(origin->candidate); + } + for (const auto& co : origin->origins) + { + getOrigins(co, res); + } +} + +const std::map<Node, ContractionOriginManager::ContractionOrigin*>& +ContractionOriginManager::currentOrigins() const +{ + return d_currentOrigins; +} + +void ContractionOriginManager::add(const Node& targetVariable, + const Node& candidate, + const std::vector<Node>& originVariables, + bool addTarget) +{ + Trace("nl-icp") << "Adding contraction for " << targetVariable << std::endl; + std::vector<ContractionOrigin*> origins; + if (addTarget) + { + auto it = d_currentOrigins.find(targetVariable); + if (it != d_currentOrigins.end()) + { + origins.emplace_back(it->second); + } + } + for (const auto& v : originVariables) + { + auto it = d_currentOrigins.find(v); + if (it != d_currentOrigins.end()) + { + origins.emplace_back(it->second); + } + } + d_allocations.emplace_back( + new ContractionOrigin{candidate, std::move(origins)}); + d_currentOrigins[targetVariable] = d_allocations.back().get(); +} + +Node ContractionOriginManager::getOrigins(const Node& variable) const +{ + Trace("nl-icp") << "Obtaining origins for " << variable << std::endl; + std::set<Node> origins; + Assert(d_currentOrigins.find(variable) != d_currentOrigins.end()) + << "Using variable as origin that is unknown yet."; + getOrigins(d_currentOrigins.at(variable), origins); + Assert(!origins.empty()) << "There should be at least one origin"; + if (origins.size() == 1) + { + return *origins.begin(); + } + return NodeManager::currentNM()->mkNode( + Kind::AND, std::vector<Node>(origins.begin(), origins.end())); +} + +bool ContractionOriginManager::isInOrigins(const Node& variable, + const Node& c) const +{ + std::set<Node> origins; + Assert(d_currentOrigins.find(variable) != d_currentOrigins.end()) + << "Using variable as origin that is unknown yet."; + getOrigins(d_currentOrigins.at(variable), origins); + return origins.find(c) != origins.end(); +} + +void print(std::ostream& os, + const std::string& indent, + const ContractionOriginManager::ContractionOrigin* co) +{ + os << indent << co->candidate << std::endl; + for (const auto& o : co->origins) + { + print(os, indent + "\t", o); + } +} + +inline std::ostream& operator<<(std::ostream& os, + const ContractionOriginManager& com) +{ + os << "ContractionOrigins:" << std::endl; + const auto& origins = com.currentOrigins(); + for (const auto& vars : origins) + { + os << vars.first << ":" << std::endl; + print(os, "\t", vars.second); + } + return os; +} + +} // namespace icp +} // namespace nl +} // namespace arith +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/arith/nl/icp/contraction_origins.h b/src/theory/arith/nl/icp/contraction_origins.h new file mode 100644 index 000000000..d8e56759d --- /dev/null +++ b/src/theory/arith/nl/icp/contraction_origins.h @@ -0,0 +1,104 @@ +/********************* */ +/*! \file contraction_origins.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 Implements a way to track the origins of ICP-style contractions. + **/ + +#ifndef CVC4__THEORY__ARITH__ICP__CONTRACTION_ORIGINS_H +#define CVC4__THEORY__ARITH__ICP__CONTRACTION_ORIGINS_H + +#include <memory> +#include <vector> + +#include "expr/node.h" + +namespace CVC4 { +namespace theory { +namespace arith { +namespace nl { +namespace icp { + +/** + * This class tracks origins of ICP-style contractions of variable intervals. + * For every variable, it holds one origin object that may recursively depend on + * previous contraction origins. Initially, a immediate bound on a variable + * (like x>0) yields an origin for this variable. For every contraction, we then + * add a new origin that recursively holds the old origins, usually those of all + * variables involved in the contraction. When generating a conflict or a lemma, + * a recursive walk through this structure allow to retrieve all input theory + * atoms that contributed to the new fact or the conflict. + */ +class ContractionOriginManager +{ + public: + /** + * Origin of one particular contraction step. + * Usually, this is either a direct bound or the application of a contraction + * candidate. The direct bound is stored in the candidate while origins + * remains empty. The contraction candidate is stored in the candidate while + * origins hold the origins of all variables used in the contraction. + */ + struct ContractionOrigin + { + /** The theory atom used to do this contraction. */ + Node candidate; + /** All origins required for this contraction. */ + std::vector<ContractionOrigin*> origins; + }; + + private: + /** + * Recursively walks through the data structure, collecting all theory atoms. + */ + void getOrigins(ContractionOrigin const* const origin, + std::set<Node>& res) const; + + public: + /** Return the current origins for all variables. */ + const std::map<Node, ContractionOrigin*>& currentOrigins() const; + /** + * Add a new contraction for the targetVariable. + * Adds a new origin with the given candidate and origins. + * If addTarget is set to true, we also add the current origin of the + * targetVariable to origins. This corresponds to whether we intersected the + * new interval with the previous interval, or whether the new interval was a + * subset of the previous one in the first place. + */ + void add(const Node& targetVariable, + const Node& candidate, + const std::vector<Node>& originVariables, + bool addTarget = true); + + /** + * Collect all theory atoms from the origins of the given variable. + */ + Node getOrigins(const Node& variable) const; + + /** Check whether a node c is among the origins of a variable. */ + bool isInOrigins(const Node& variable, const Node& c) const; + + private: + /** The current origins for every variable. */ + std::map<Node, ContractionOrigin*> d_currentOrigins; + /** All allocated origins to allow for proper deallocation. */ + std::vector<std::unique_ptr<ContractionOrigin>> d_allocations; +}; + +/** Stream the constration origins to an ostream. */ +std::ostream& operator<<(std::ostream& os, const ContractionOriginManager& com); + +} // namespace icp +} // namespace nl +} // namespace arith +} // namespace theory +} // namespace CVC4 + +#endif diff --git a/src/theory/arith/nl/icp/icp_solver.cpp b/src/theory/arith/nl/icp/icp_solver.cpp new file mode 100644 index 000000000..128841527 --- /dev/null +++ b/src/theory/arith/nl/icp/icp_solver.cpp @@ -0,0 +1,364 @@ +/********************* */ +/*! \file icp_solver.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 Implements a ICP-based solver for nonlinear arithmetic. + **/ + +#include "theory/arith/nl/icp/icp_solver.h" + +#ifdef CVC4_POLY_IMP + +#include <iostream> + +#include "base/check.h" +#include "base/output.h" +#include "expr/node_algorithm.h" +#include "theory/arith/arith_msum.h" +#include "theory/arith/nl/poly_conversion.h" +#include "theory/arith/normal_form.h" +#include "theory/rewriter.h" +#include "util/poly_util.h" + +namespace CVC4 { +namespace theory { +namespace arith { +namespace nl { +namespace icp { + +namespace { +/** A simple wrapper to nicely print an interval assignment. */ +struct IAWrapper +{ + const poly::IntervalAssignment& ia; + const VariableMapper& vm; +}; +inline std::ostream& operator<<(std::ostream& os, const IAWrapper& iaw) +{ + os << "{ "; + bool first = true; + for (const auto& v : iaw.vm.mVarpolyCVC) + { + if (iaw.ia.has(v.first)) + { + if (first) + { + first = false; + } + else + { + os << ", "; + } + os << v.first << " -> " << iaw.ia.get(v.first); + } + } + return os << " }"; +} +} // namespace + +std::vector<Node> ICPSolver::collectVariables(const Node& n) const +{ + std::unordered_set<TNode, TNodeHashFunction> tmp; + expr::getVariables(n, tmp); + std::vector<Node> res; + for (const auto& t : tmp) + { + res.emplace_back(t); + } + return res; +} + +std::vector<Candidate> ICPSolver::constructCandidates(const Node& n) +{ + auto comp = Comparison::parseNormalForm(n).decompose(false); + Kind k = std::get<1>(comp); + if (k == Kind::DISTINCT) + { + return {}; + } + auto poly = std::get<0>(comp); + + std::vector<Candidate> result; + std::unordered_set<TNode, TNodeHashFunction> vars; + expr::getVariables(n, vars); + for (const auto& v : vars) + { + Trace("nl-icp") << "\tChecking " << n << " for " << v << std::endl; + + std::map<Node, Node> msum; + ArithMSum::getMonomialSum(poly.getNode(), msum); + + Node veq_c; + Node val; + + int isolated = ArithMSum::isolate(v, msum, veq_c, val, k); + if (isolated == 1) + { + poly::Variable lhs = d_mapper(v); + poly::SignCondition rel; + switch (k) + { + case Kind::LT: rel = poly::SignCondition::LT; break; + case Kind::LEQ: rel = poly::SignCondition::LE; break; + case Kind::EQUAL: rel = poly::SignCondition::EQ; break; + case Kind::DISTINCT: rel = poly::SignCondition::NE; break; + case Kind::GT: rel = poly::SignCondition::GT; break; + case Kind::GEQ: rel = poly::SignCondition::GE; break; + default: Assert(false) << "Unexpected kind: " << k; + } + poly::Rational rhsmult; + poly::Polynomial rhs = as_poly_polynomial(val, d_mapper, rhsmult); + rhsmult = poly::Rational(1) / rhsmult; + // only correct up to a constant (denominator is thrown away!) + if (!veq_c.isNull()) + { + rhsmult = poly_utils::toRational(veq_c.getConst<Rational>()); + } + Candidate res{lhs, rel, rhs, rhsmult, n, collectVariables(val)}; + Trace("nl-icp") << "\tAdded " << res << " from " << n << std::endl; + result.emplace_back(res); + } + else if (isolated == -1) + { + poly::Variable lhs = d_mapper(v); + poly::SignCondition rel; + switch (k) + { + case Kind::LT: rel = poly::SignCondition::GT; break; + case Kind::LEQ: rel = poly::SignCondition::GE; break; + case Kind::EQUAL: rel = poly::SignCondition::EQ; break; + case Kind::DISTINCT: rel = poly::SignCondition::NE; break; + case Kind::GT: rel = poly::SignCondition::LT; break; + case Kind::GEQ: rel = poly::SignCondition::LE; break; + default: Assert(false) << "Unexpected kind: " << k; + } + poly::Rational rhsmult; + poly::Polynomial rhs = as_poly_polynomial(val, d_mapper, rhsmult); + rhsmult = poly::Rational(1) / rhsmult; + if (!veq_c.isNull()) + { + rhsmult = poly_utils::toRational(veq_c.getConst<Rational>()); + } + Candidate res{lhs, rel, rhs, rhsmult, n, collectVariables(val)}; + Trace("nl-icp") << "\tAdded " << res << " from " << n << std::endl; + result.emplace_back(res); + } + } + return result; +} + +void ICPSolver::addCandidate(const Node& n) +{ + auto it = d_candidateCache.find(n); + if (it != d_candidateCache.end()) + { + for (const auto& c : it->second) + { + d_state.d_candidates.emplace_back(c); + } + } + else + { + auto cands = constructCandidates(n); + d_candidateCache.emplace(n, cands); + for (const auto& c : cands) + { + d_state.d_candidates.emplace_back(c); + Trace("nl-icp") << "Bumping budget because of the new candidate" + << std::endl; + d_budget += d_budgetIncrement; + } + } +} + +void ICPSolver::initOrigins() +{ + for (const auto& vars : d_mapper.mVarCVCpoly) + { + auto& i = d_state.d_bounds.get(vars.first); + Trace("nl-icp") << "Adding initial " << vars.first << " -> " << i + << std::endl; + if (!i.lower_origin.isNull()) + { + Trace("nl-icp") << "\tAdding lower " << i.lower_origin << std::endl; + d_state.d_origins.add(vars.first, i.lower_origin, {}); + } + if (!i.upper_origin.isNull()) + { + Trace("nl-icp") << "\tAdding upper " << i.upper_origin << std::endl; + d_state.d_origins.add(vars.first, i.upper_origin, {}); + } + } +} + +PropagationResult ICPSolver::doPropagationRound() +{ + if (d_budget <= 0) + { + Trace("nl-icp") << "ICP budget exceeded" << std::endl; + return PropagationResult::NOT_CHANGED; + } + d_state.d_conflict = Node(); + Trace("nl-icp") << "Starting propagation with " + << IAWrapper{d_state.d_assignment, d_mapper} << std::endl; + Trace("nl-icp") << "Current budget: " << d_budget << std::endl; + PropagationResult res = PropagationResult::NOT_CHANGED; + for (const auto& c : d_state.d_candidates) + { + --d_budget; + PropagationResult cres = c.propagate(d_state.d_assignment, 100); + switch (cres) + { + case PropagationResult::NOT_CHANGED: break; + case PropagationResult::CONTRACTED: + case PropagationResult::CONTRACTED_STRONGLY: + d_state.d_origins.add(d_mapper(c.lhs), c.origin, c.rhsVariables); + res = PropagationResult::CONTRACTED; + break; + case PropagationResult::CONTRACTED_WITHOUT_CURRENT: + case PropagationResult::CONTRACTED_STRONGLY_WITHOUT_CURRENT: + d_state.d_origins.add(d_mapper(c.lhs), c.origin, c.rhsVariables, false); + res = PropagationResult::CONTRACTED; + break; + case PropagationResult::CONFLICT: + d_state.d_origins.add(d_mapper(c.lhs), c.origin, c.rhsVariables); + d_state.d_conflict = d_state.d_origins.getOrigins(d_mapper(c.lhs)); + return PropagationResult::CONFLICT; + } + switch (cres) + { + case PropagationResult::CONTRACTED_STRONGLY: + case PropagationResult::CONTRACTED_STRONGLY_WITHOUT_CURRENT: + Trace("nl-icp") << "Bumping budget because of a strong contraction" + << std::endl; + d_budget += d_budgetIncrement; + break; + default: break; + } + } + return res; +} + +std::vector<Node> ICPSolver::generateLemmas() const +{ + auto nm = NodeManager::currentNM(); + std::vector<Node> lemmas; + + for (const auto& vars : d_mapper.mVarCVCpoly) + { + if (!d_state.d_assignment.has(vars.second)) continue; + Node v = vars.first; + poly::Interval i = d_state.d_assignment.get(vars.second); + if (!is_minus_infinity(get_lower(i))) + { + Kind rel = get_lower_open(i) ? Kind::GT : Kind::GEQ; + Node c = nm->mkNode(rel, v, value_to_node(get_lower(i), v)); + if (!d_state.d_origins.isInOrigins(v, c)) + { + Node premise = d_state.d_origins.getOrigins(v); + Trace("nl-icp") << premise << " => " << c << std::endl; + Node lemma = Rewriter::rewrite(nm->mkNode(Kind::IMPLIES, premise, c)); + if (lemma.isConst()) + { + Assert(lemma == nm->mkConst<bool>(true)); + } + else + { + Trace("nl-icp") << "Adding lemma " << lemma << std::endl; + lemmas.emplace_back(lemma); + } + } + } + if (!is_plus_infinity(get_upper(i))) + { + Kind rel = get_upper_open(i) ? Kind::LT : Kind::LEQ; + Node c = nm->mkNode(rel, v, value_to_node(get_upper(i), v)); + if (!d_state.d_origins.isInOrigins(v, c)) + { + Node premise = d_state.d_origins.getOrigins(v); + Trace("nl-icp") << premise << " => " << c << std::endl; + Node lemma = Rewriter::rewrite(nm->mkNode(Kind::IMPLIES, premise, c)); + if (lemma.isConst()) + { + Assert(lemma == nm->mkConst<bool>(true)); + } + else + { + Trace("nl-icp") << "Adding lemma " << lemma << std::endl; + lemmas.emplace_back(lemma); + } + } + } + } + return lemmas; +} + +void ICPSolver::reset(const std::vector<Node>& assertions) +{ + d_state.reset(); + for (const auto& n : assertions) + { + Node tmp = Rewriter::rewrite(n); + Trace("nl-icp") << "Adding " << tmp << std::endl; + if (tmp.getKind() != Kind::CONST_BOOLEAN) + { + if (!d_state.d_bounds.add(tmp)) + { + addCandidate(tmp); + } + } + } +} + +void ICPSolver::check() +{ + initOrigins(); + d_state.d_assignment = d_state.d_bounds.get(); + bool did_progress = false; + bool progress = false; + do + { + switch (doPropagationRound()) + { + case icp::PropagationResult::NOT_CHANGED: progress = false; break; + case icp::PropagationResult::CONTRACTED: + case icp::PropagationResult::CONTRACTED_STRONGLY: + case icp::PropagationResult::CONTRACTED_WITHOUT_CURRENT: + case icp::PropagationResult::CONTRACTED_STRONGLY_WITHOUT_CURRENT: + did_progress = true; + progress = true; + break; + case icp::PropagationResult::CONFLICT: + Trace("nl-icp") << "Found a conflict: " << d_state.d_conflict + << std::endl; + + d_im.addConflict(d_state.d_conflict, InferenceId::NL_ICP_CONFLICT); + did_progress = true; + progress = false; + break; + } + } while (progress); + if (did_progress) + { + std::vector<Node> lemmas = generateLemmas(); + for (const auto& l : lemmas) + { + d_im.addPendingArithLemma(l, InferenceId::NL_ICP_PROPAGATION); + } + } +} + +} // namespace icp +} // namespace nl +} // namespace arith +} // namespace theory +} // namespace CVC4 + +#endif diff --git a/src/theory/arith/nl/icp/icp_solver.h b/src/theory/arith/nl/icp/icp_solver.h new file mode 100644 index 000000000..5fcd45fc6 --- /dev/null +++ b/src/theory/arith/nl/icp/icp_solver.h @@ -0,0 +1,142 @@ +/********************* */ +/*! \file icp_solver.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 Implements a ICP-based solver for nonlinear arithmetic. + **/ + +#ifndef CVC4__THEORY__ARITH__ICP__ICP_SOLVER_H +#define CVC4__THEORY__ARITH__ICP__ICP_SOLVER_H + +#include "util/real_algebraic_number.h" + +#ifdef CVC4_POLY_IMP +#include <poly/polyxx.h> + +#include "expr/node.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 { +namespace theory { +namespace arith { +namespace nl { +namespace icp { + +/** + * This class implements an ICP-based solver. As it is intended to be used in + * conjunction with other solvers, it only performs contractions, but does not + * issue splits. + * + * In essence, interval constraint propagation has candidates (like x = y^2-z), + * evaluates their right hand side over the current (interval) assignment and + * uses the resulting interval to make the interval of the left-hand side + * variable smaller (contract it). + * + * These contractions can yield to a conflict (if the interval of some variable + * becomes empty) or shrink the search space for a variable. + */ +class ICPSolver +{ + /** + * This encapsulates the state of the ICP solver that is local to a single + * theory call. It contains the variable bounds and candidates derived from + * the assertions, the origins manager and the last conflict. + */ + struct ICPState + { + /** The variable bounds extracted from the input assertions */ + VariableBounds d_bounds; + /** The contraction candidates generated from the theory atoms */ + std::vector<Candidate> d_candidates; + /** The current assignment */ + poly::IntervalAssignment d_assignment; + /** The origins for the current assignment */ + ContractionOriginManager d_origins; + /** The conflict, if any way found. Initially the null node */ + Node d_conflict; + + /** Initialized the variable bounds with a variable mapper */ + ICPState(VariableMapper& vm) : d_bounds(vm) {} + + /** Reset this state */ + void reset() + { + d_bounds.reset(); + d_candidates.clear(); + d_assignment.clear(); + d_origins = ContractionOriginManager(); + d_conflict = Node(); + } + }; + + /** Maps Node (variables) to poly::Variable */ + VariableMapper d_mapper; + /** The inference manager */ + InferenceManager& d_im; + /** Cache candidates to avoid reconstruction for every theory call */ + std::map<Node, std::vector<Candidate>> d_candidateCache; + /** The current state */ + ICPState d_state; + + /** The remaining budget */ + std::int64_t d_budget = 0; + /** The budget increment for new candidates and strong contractions */ + static constexpr std::int64_t d_budgetIncrement = 10; + + /** Collect all variables from a node */ + std::vector<Node> collectVariables(const Node& n) const; + /** Construct all possible candidates from a given theory atom */ + std::vector<Candidate> constructCandidates(const Node& n); + /** Add the given node as candidate */ + void addCandidate(const Node& n); + /** Initialize the origin manager from the variable bounds */ + void initOrigins(); + + /** + * Perform one contraction with every candidate. + * If any candidate yields a conflict stops immediately and returns + * PropagationResult::CONFLICT. If any candidate yields a contraction returns + * PropagationResult::CONTRACTED. Otherwise returns + * PropagationResult::NOT_CHANGED. + */ + PropagationResult doPropagationRound(); + + /** + * Construct lemmas for all bounds that have been improved. + * For every improved bound, all origins are collected and a lemma of the form + * (and origins) ==> (new bound) + * is constructed. + */ + std::vector<Node> generateLemmas() const; + + public: + ICPSolver(InferenceManager& im) : d_im(im), d_state(d_mapper) {} + /** Reset this solver for the next theory call */ + void reset(const std::vector<Node>& assertions); + + /** + * Performs a full ICP check. + */ + void check(); +}; + +} // 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/intersection.cpp b/src/theory/arith/nl/icp/intersection.cpp new file mode 100644 index 000000000..148059db0 --- /dev/null +++ b/src/theory/arith/nl/icp/intersection.cpp @@ -0,0 +1,224 @@ +/********************* */ +/*! \file intersection.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/intersection.h" + +#ifdef CVC4_POLY_IMP + +#include <iostream> + +#include "base/check.h" +#include "base/output.h" +#include "theory/arith/nl/poly_conversion.h" + +namespace CVC4 { +namespace theory { +namespace arith { +namespace nl { +namespace icp { + +PropagationResult intersect_interval_with(poly::Interval& cur, + const poly::Interval& res, + std::size_t size_threshold) +{ + Trace("nl-icp") << cur << " := " << cur << " intersected with " << res + << std::endl; + + if (bitsize(get_lower(res)) > size_threshold + || bitsize(get_upper(res)) > size_threshold) + { + Trace("nl-icp") << "Reached bitsize threshold" << std::endl; + return PropagationResult::NOT_CHANGED; + } + + // Basic idea to organize this function: + // The bounds for res have 5 positions: + // 1 < 2 (lower(cur)) < 3 < 4 (upper(cur)) < 5 + + if (get_upper(res) < get_lower(cur)) + { + // upper(res) at 1 + Trace("nl-icp") << "res < cur -> conflict" << std::endl; + return PropagationResult::CONFLICT; + } + if (get_upper(res) == get_lower(cur)) + { + // upper(res) at 2 + if (get_upper_open(res) || get_lower_open(cur)) + { + Trace("nl-icp") << "meet at lower, but one is open -> conflict" + << std::endl; + return PropagationResult::CONFLICT; + } + if (!is_point(cur)) + { + Trace("nl-icp") << "contracts to point interval at lower" << std::endl; + cur = poly::Interval(get_upper(res)); + return PropagationResult::CONTRACTED; + } + return PropagationResult::NOT_CHANGED; + } + Assert(get_upper(res) > get_lower(cur)) + << "Comparison operator does weird stuff."; + if (get_upper(res) < get_upper(cur)) + { + // upper(res) at 3 + if (get_lower(res) < get_lower(cur)) + { + // lower(res) at 1 + Trace("nl-icp") << "lower(cur) .. upper(res)" << std::endl; + cur.set_upper(get_upper(res), get_upper_open(res)); + return PropagationResult::CONTRACTED; + } + if (get_lower(res) == get_lower(cur)) + { + // lower(res) at 2 + Trace("nl-icp") << "meet at lower, lower(cur) .. upper(res)" << std::endl; + cur = poly::Interval(get_lower(cur), + get_lower_open(cur) || get_lower_open(res), + get_upper(res), + get_upper_open(res)); + if (get_lower_open(cur) && !get_lower_open(res)) + { + return PropagationResult::CONTRACTED; + } + return PropagationResult::CONTRACTED_WITHOUT_CURRENT; + } + Assert(get_lower(res) > get_lower(cur)) + << "Comparison operator does weird stuff."; + // lower(res) at 3 + Trace("nl-icp") << "cur covers res" << std::endl; + cur = res; + return PropagationResult::CONTRACTED_WITHOUT_CURRENT; + } + if (get_upper(res) == get_upper(cur)) + { + // upper(res) at 4 + if (get_lower(res) < get_lower(cur)) + { + // lower(res) at 1 + Trace("nl-icp") << "res covers cur but meet at upper" << std::endl; + if (get_upper_open(res) && !get_upper_open(cur)) + { + cur.set_upper(get_upper(cur), true); + return PropagationResult::CONTRACTED; + } + return PropagationResult::NOT_CHANGED; + } + if (get_lower(res) == get_lower(cur)) + { + // lower(res) at 2 + Trace("nl-icp") << "same bounds but check openness" << std::endl; + bool changed = false; + if (get_lower_open(res) && !get_lower_open(cur)) + { + changed = true; + cur.set_lower(get_lower(cur), true); + } + if (get_upper_open(res) && !get_upper_open(cur)) + { + changed = true; + cur.set_upper(get_upper(cur), true); + } + if (changed) + { + if ((get_lower_open(res) || !get_upper_open(cur)) + && (get_upper_open(res) || !get_upper_open(cur))) + { + return PropagationResult::CONTRACTED_WITHOUT_CURRENT; + } + return PropagationResult::CONTRACTED; + } + return PropagationResult::NOT_CHANGED; + } + Assert(get_lower(res) > get_lower(cur)) + << "Comparison operator does weird stuff."; + // lower(res) at 3 + Trace("nl-icp") << "cur covers res but meet at upper" << std::endl; + cur = poly::Interval(get_lower(res), + get_lower_open(res), + get_upper(res), + get_upper_open(cur) || get_upper_open(res)); + if (get_upper_open(cur) && !get_upper_open(res)) + { + return PropagationResult::CONTRACTED; + } + return PropagationResult::CONTRACTED_WITHOUT_CURRENT; + } + + Assert(get_upper(res) > get_upper(cur)) + << "Comparison operator does weird stuff."; + // upper(res) at 5 + + if (get_lower(res) < get_lower(cur)) + { + // lower(res) at 1 + Trace("nl-icp") << "res covers cur" << std::endl; + return PropagationResult::NOT_CHANGED; + } + if (get_lower(res) == get_lower(cur)) + { + // lower(res) at 2 + Trace("nl-icp") << "res covers cur but meet at lower" << std::endl; + if (get_lower_open(res) && is_point(cur)) + { + return PropagationResult::CONFLICT; + } + else if (get_lower_open(res) && !get_lower_open(cur)) + { + cur.set_lower(get_lower(cur), true); + return PropagationResult::CONTRACTED; + } + return PropagationResult::NOT_CHANGED; + } + Assert(get_lower(res) > get_lower(cur)) + << "Comparison operator does weird stuff."; + if (get_lower(res) < get_upper(cur)) + { + // lower(res) at 3 + Trace("nl-icp") << "lower(res) .. upper(cur)" << std::endl; + cur.set_lower(get_lower(res), get_lower_open(res)); + return PropagationResult::CONTRACTED; + } + if (get_lower(res) == get_upper(cur)) + { + // lower(res) at 4 + if (get_lower_open(res) || get_upper_open(cur)) + { + Trace("nl-icp") << "meet at upper, but one is open -> conflict" + << std::endl; + return PropagationResult::CONFLICT; + } + if (!is_point(cur)) + { + Trace("nl-icp") << "contracts to point interval at upper" << std::endl; + cur = poly::Interval(get_lower(res)); + return PropagationResult::CONTRACTED; + } + return PropagationResult::NOT_CHANGED; + } + + Assert(get_lower(res) > get_upper(cur)); + // lower(res) at 5 + Trace("nl-icp") << "res > cur -> conflict" << std::endl; + return PropagationResult::CONFLICT; +} + +} // namespace icp +} // namespace nl +} // namespace arith +} // namespace theory +} // namespace CVC4 + +#endif diff --git a/src/theory/arith/nl/icp/intersection.h b/src/theory/arith/nl/icp/intersection.h new file mode 100644 index 000000000..8d772cb7a --- /dev/null +++ b/src/theory/arith/nl/icp/intersection.h @@ -0,0 +1,79 @@ +/********************* */ +/*! \file intersection.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 Implement intersection of intervals for propagation. + **/ + +#ifndef CVC4__THEORY__ARITH__ICP__INTERSECTION_H +#define CVC4__THEORY__ARITH__ICP__INTERSECTION_H + +#include "util/real_algebraic_number.h" + +#ifdef CVC4_POLY_IMP +#include <poly/polyxx.h> + +namespace CVC4 { +namespace theory { +namespace arith { +namespace nl { +namespace icp { + +/** + * Represents the possible results of a single propagation step. + * A propagation tries to refine a current interval with a new interval by + * intersecting them. + */ +enum class PropagationResult +{ + /** The propagation did not change the current interval. */ + NOT_CHANGED, + /** The propagation contracted the current interval. */ + CONTRACTED, + /** + * The propagation contracted the current interval made at least one bound + * finite. + */ + CONTRACTED_STRONGLY, + /** + * The propagation only used the new interval (as it was a subset of the + * current interval). + */ + CONTRACTED_WITHOUT_CURRENT, + /** + * The propagation only used the new interval (as it was a subset of the + * current interval) and made at least one bound finite. + */ + CONTRACTED_STRONGLY_WITHOUT_CURRENT, + /** + * The propagation found a conflict as the two intervals did not intersect. + */ + CONFLICT +}; + +/** + * Update the current interval by intersection with the new interval and return + * the appropriate result. If the size of any of the bounds, as computed by + * bitsize(), would grow beyond the given threshold, no intersection is + * performed and PropagationResult::NOT_CHANGED is returned. + */ +PropagationResult intersect_interval_with(poly::Interval& cur, + const poly::Interval& res, + std::size_t size_threshold); + +} // namespace icp +} // namespace nl +} // namespace arith +} // namespace theory +} // namespace CVC4 + +#endif + +#endif diff --git a/src/theory/arith/nl/icp/interval.h b/src/theory/arith/nl/icp/interval.h new file mode 100644 index 000000000..374067961 --- /dev/null +++ b/src/theory/arith/nl/icp/interval.h @@ -0,0 +1,65 @@ +/********************* */ +/*! \file interval.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 + **/ + +#ifndef CVC4__THEORY__ARITH__ICP__INTERVAL_H +#define CVC4__THEORY__ARITH__ICP__INTERVAL_H + +#include "util/real_algebraic_number.h" + +#ifdef CVC4_POLY_IMP +#include <poly/polyxx.h> + +#include "expr/node.h" + +namespace CVC4 { +namespace theory { +namespace arith { +namespace nl { +namespace icp { + +/** + * Represents an interval with poly::Value bounds and origins for these bounds. + */ +struct Interval +{ + /** The lower bound */ + poly::Value lower = poly::Value::minus_infty(); + /** Whether the lower bound is strict or weak */ + bool lower_strict = true; + /** The origin of the lower bound */ + Node lower_origin; + /** The upper bound */ + poly::Value upper = poly::Value::plus_infty(); + /** Whether the upper bound is strict or weak */ + bool upper_strict = true; + /** The origin of the upper bound */ + Node upper_origin; +}; + +/** Print an interval */ +inline std::ostream& operator<<(std::ostream& os, const Interval& i) +{ + return os << (i.lower_strict ? '(' : '[') << i.lower << " .. " << i.upper + << (i.upper_strict ? ')' : ']'); +} + +} // namespace icp +} // namespace nl +} // namespace arith +} // namespace theory +} // namespace CVC4 + +#endif + +#endif diff --git a/src/theory/arith/nl/icp/variable_bounds.cpp b/src/theory/arith/nl/icp/variable_bounds.cpp new file mode 100644 index 000000000..14007971a --- /dev/null +++ b/src/theory/arith/nl/icp/variable_bounds.cpp @@ -0,0 +1,158 @@ +/********************* */ +/*! \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/icp/variable_bounds.h b/src/theory/arith/nl/icp/variable_bounds.h new file mode 100644 index 000000000..256054538 --- /dev/null +++ b/src/theory/arith/nl/icp/variable_bounds.h @@ -0,0 +1,96 @@ +/********************* */ +/*! \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 diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index df3a304be..05442a566 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -47,6 +47,7 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing, d_trSlv(d_im, d_model), d_nlSlv(containing, d_model), d_cadSlv(d_im, d_model), + d_icpSlv(d_im), d_iandSlv(containing, d_model), d_builtModel(containing.getSatContext(), false) { @@ -381,6 +382,21 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions, } } + if (options::nlICP()) + { + d_icpSlv.reset(assertions); + d_icpSlv.check(); + + if (d_im.hasUsed()) + { + Trace("nl-ext") << " ...finished with " + << d_im.numPendingLemmas() + d_im.numSentLemmas() + << " new lemmas from ICP." << std::endl; + return d_im.numPendingLemmas() + d_im.numSentLemmas(); + } + Trace("nl-ext") << "Done with ICP" << std::endl; + } + if (options::nlExt()) { // initialize the non-linear solver @@ -758,7 +774,7 @@ bool NonlinearExtension::modelBasedRefinement(std::vector<NlLemma>& mlems) d_builtModel = true; } filterLemmas(lemmas, mlems); - if (!mlems.empty()) + if (!mlems.empty() || d_im.hasPendingLemma()) { return true; } diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index b62b81e9c..8bd281b5f 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -30,6 +30,7 @@ #include "theory/arith/nl/cad_solver.h" #include "theory/arith/nl/ext_theory_callback.h" #include "theory/arith/nl/iand_solver.h" +#include "theory/arith/nl/icp/icp_solver.h" #include "theory/arith/nl/nl_lemma_utils.h" #include "theory/arith/nl/nl_model.h" #include "theory/arith/nl/nl_solver.h" @@ -281,6 +282,8 @@ class NonlinearExtension NlSolver d_nlSlv; /** The CAD-based solver */ CadSolver d_cadSlv; + /** The ICP-based solver */ + icp::ICPSolver d_icpSlv; /** The integer and solver * * This is the subsolver responsible for running the procedure for diff --git a/src/theory/arith/nl/poly_conversion.cpp b/src/theory/arith/nl/poly_conversion.cpp index d8dc2270d..20e39dd8b 100644 --- a/src/theory/arith/nl/poly_conversion.cpp +++ b/src/theory/arith/nl/poly_conversion.cpp @@ -201,6 +201,15 @@ poly::Polynomial as_poly_polynomial(const CVC4::Node& n, VariableMapper& vm) poly::Integer denom; return as_poly_polynomial_impl(n, denom, vm); } +poly::Polynomial as_poly_polynomial(const CVC4::Node& n, + VariableMapper& vm, + poly::Rational& denominator) +{ + poly::Integer denom; + auto res = as_poly_polynomial_impl(n, denom, vm); + denominator = poly::Rational(denom); + return res; +} poly::SignCondition normalize_kind(CVC4::Kind kind, bool negated, diff --git a/src/theory/arith/nl/poly_conversion.h b/src/theory/arith/nl/poly_conversion.h index d83bc1b2e..a60b7ac41 100644 --- a/src/theory/arith/nl/poly_conversion.h +++ b/src/theory/arith/nl/poly_conversion.h @@ -61,10 +61,17 @@ poly::UPolynomial as_poly_upolynomial(const CVC4::Node& n, * While a Node may contain rationals, a Polynomial does not. * We therefore also store the denominator of the returned polynomial and * use it to construct the integer polynomial recursively. - * Once the polynomial has been fully constructed, we can ignore the + * Once the polynomial has been fully constructed, we can oftentimes ignore the * denominator (except for its sign, which is always positive, though). + * This is the case if we are solely interested in the roots of the polynomials + * (like in the context of CAD). If we need the actual polynomial (for example + * in the context of ICP) the second overload provides the denominator in the + * third argument. */ poly::Polynomial as_poly_polynomial(const CVC4::Node& n, VariableMapper& vm); +poly::Polynomial as_poly_polynomial(const CVC4::Node& n, + VariableMapper& vm, + poly::Rational& denominator); /** * Constructs a constraints (a polynomial and a sign condition) from the given diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp index f964f1628..c91f8d400 100644 --- a/src/theory/arith/normal_form.cpp +++ b/src/theory/arith/normal_form.cpp @@ -816,6 +816,64 @@ DeltaRational Comparison::normalizedDeltaRational() const { } } +std::tuple<Polynomial, Kind, Constant> Comparison::decompose( + bool split_constant) const +{ + Kind rel = getNode().getKind(); + if (rel == Kind::NOT) + { + switch (getNode()[0].getKind()) + { + case kind::LEQ: rel = Kind::GT; break; + case kind::LT: rel = Kind::GEQ; break; + case kind::EQUAL: rel = Kind::DISTINCT; break; + case kind::DISTINCT: rel = Kind::EQUAL; break; + case kind::GEQ: rel = Kind::LT; break; + case kind::GT: rel = Kind::LEQ; break; + default: + Assert(false) << "Unsupported relation: " << getNode()[0].getKind(); + } + } + + Polynomial poly = getLeft() - getRight(); + + if (!split_constant) + { + return std::tuple<Polynomial, Kind, Constant>{ + poly, rel, Constant::mkZero()}; + } + + Constant right = Constant::mkZero(); + if (poly.containsConstant()) + { + right = -poly.getHead().getConstant(); + poly = poly + Polynomial::mkPolynomial(right); + } + + Constant lcoeff = poly.getHead().getConstant(); + if (!lcoeff.isOne()) + { + Constant invlcoeff = lcoeff.inverse(); + if (lcoeff.isNegative()) + { + switch (rel) + { + case kind::LEQ: rel = Kind::GEQ; break; + case kind::LT: rel = Kind::GT; break; + case kind::EQUAL: break; + case kind::DISTINCT: break; + case kind::GEQ: rel = Kind::LEQ; break; + case kind::GT: rel = Kind::LT; break; + default: Assert(false) << "Unsupported relation: " << rel; + } + } + poly = poly * invlcoeff; + right = right * invlcoeff; + } + + return std::tuple<Polynomial, Kind, Constant>{poly, rel, right}; +} + Comparison Comparison::parseNormalForm(TNode n) { Debug("polynomial") << "Comparison::parseNormalForm(" << n << ")"; Comparison result(n); diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h index 484bdbf44..773a43e15 100644 --- a/src/theory/arith/normal_form.h +++ b/src/theory/arith/normal_form.h @@ -946,6 +946,18 @@ public: /** Returns true if the polynomial contains a non-linear monomial.*/ bool isNonlinear() const; + /** Check whether this polynomial is only a single variable. */ + bool isVariable() const + { + return singleton() && getHead().getVarList().singleton() + && getHead().coefficientIsOne(); + } + /** Return the variable, given that isVariable() holds. */ + Variable getVariable() const + { + Assert(isVariable()); + return getHead().getVarList().getHead(); + } /** * Selects a minimal monomial in the polynomial by the absolute value of @@ -1377,6 +1389,19 @@ public: Polynomial normalizedVariablePart() const; DeltaRational normalizedDeltaRational() const; + /** + * Transforms a Comparison object into a stronger normal form: + * Polynomial ~Kind~ Constant + * + * From the comparison, this method resolved a negation (if present) and + * moves everything to the left side. + * If split_constant is false, the constant is always zero. + * If split_constant is true, the polynomial has no constant term and is + * normalized to have leading coefficient one. + */ + std::tuple<Polynomial, Kind, Constant> decompose( + bool split_constant = false) const; + };/* class Comparison */ }/* CVC4::theory::arith namespace */ diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp index 980763040..122284e8a 100644 --- a/src/theory/theory_inference_manager.cpp +++ b/src/theory/theory_inference_manager.cpp @@ -32,6 +32,7 @@ TheoryInferenceManager::TheoryInferenceManager(Theory& t, d_pnm(pnm), d_keep(t.getSatContext()), d_lemmasSent(t.getUserContext()), + d_numConflicts(0), d_numCurrentLemmas(0), d_numCurrentFacts(0) { @@ -54,6 +55,7 @@ bool TheoryInferenceManager::isProofEnabled() const { return d_pnm != nullptr; } void TheoryInferenceManager::reset() { + d_numConflicts = 0; d_numCurrentLemmas = 0; d_numCurrentFacts = 0; } @@ -85,6 +87,7 @@ void TheoryInferenceManager::conflict(TNode conf) { d_theoryState.notifyInConflict(); d_out.conflict(conf); + ++d_numConflicts; } } diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h index e63d55366..4d2573501 100644 --- a/src/theory/theory_inference_manager.h +++ b/src/theory/theory_inference_manager.h @@ -416,6 +416,8 @@ class TheoryInferenceManager * nodes. Notice that this cache does not depedent on lemma property. */ NodeSet d_lemmasSent; + /** The number of conflicts sent since the last call to reset. */ + uint32_t d_numConflicts; /** The number of lemmas sent since the last call to reset. */ uint32_t d_numCurrentLemmas; /** The number of internal facts added since the last call to reset. */ |