This PR adds a new icp-based solver to be integrated into the nonlinear extension.
It is not meant to be used as a stand-alone ICP solver. It does not implement splits (only propagations) and implements a rather aggressive budget mechanism that aims to quickly stop propagation to allow other solvers to take over. Additionally, it enforces a maximum bit size to avoid divergence.
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
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"
+
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,
};
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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
--- /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
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)
{
}
}
+ 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
d_builtModel = true;
}
filterLemmas(lemmas, mlems);
- if (!mlems.empty())
+ if (!mlems.empty() || d_im.hasPendingLemma())
{
return true;
}
#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"
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
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,
* 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
}
}
+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);
/** 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
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 */
d_pnm(pnm),
d_keep(t.getSatContext()),
d_lemmasSent(t.getUserContext()),
+ d_numConflicts(0),
d_numCurrentLemmas(0),
d_numCurrentFacts(0)
{
void TheoryInferenceManager::reset()
{
+ d_numConflicts = 0;
d_numCurrentLemmas = 0;
d_numCurrentFacts = 0;
}
{
d_theoryState.notifyInConflict();
d_out.conflict(conf);
+ ++d_numConflicts;
}
}
* 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. */
projects / cvc5.git / commitdiff