From: Gereon Kremer Date: Tue, 4 Aug 2020 10:57:34 +0000 (+0200) Subject: Add CAD-based solver (#4834) X-Git-Tag: cvc5-1.0.0~3046 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4844afa3d254bdabac397556e166a2534bb6c2ac;p=cvc5.git Add CAD-based solver (#4834) Based on #4774, this PR adds a new CadSolver class that allows the NonlinearExtension to actually employ the CAD-based method. In more detail: add --nl-cad option add CadSolver class that wraps cad::CDCAC with support for checks, model construction and conflict generation add new Inference types for the NlLemma class use CadSolver in NonlinearExtension (if --nl-cad is given) --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 17c4a26f5..cd6f48178 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -310,6 +310,8 @@ libcvc4_add_sources( theory/arith/linear_equality.h theory/arith/matrix.cpp theory/arith/matrix.h + theory/arith/nl/cad_solver.cpp + theory/arith/nl/cad_solver.h theory/arith/nl/cad/cdcac.cpp theory/arith/nl/cad/cdcac.h theory/arith/nl/cad/cdcac_utils.cpp diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml index a6c967dc9..23ced4d8f 100644 --- a/src/options/arith_options.toml +++ b/src/options/arith_options.toml @@ -541,3 +541,12 @@ header = "options/arith_options.h" default = "true" read_only = true help = "whether to use simple rounding, similar to a unit-cube test, for integers" + +[[option]] + name = "nlCad" + category = "regular" + long = "nl-cad" + type = "bool" + default = "false" + help = "whether to use the cylindrical algebraic decomposition solver for non-linear arithmetic" + diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp new file mode 100644 index 000000000..783fb0187 --- /dev/null +++ b/src/theory/arith/nl/cad_solver.cpp @@ -0,0 +1,141 @@ +/********************* */ +/*! \file cad_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 Implementation of new non-linear solver + **/ + +#include "theory/arith/nl/cad_solver.h" + +#ifdef CVC4_POLY_IMP +#include +#endif + +#include "inference.h" +#include "theory/arith/nl/cad/cdcac.h" +#include "theory/arith/nl/poly_conversion.h" +#include "util/poly_util.h" + +namespace CVC4 { +namespace theory { +namespace arith { +namespace nl { + +CadSolver::CadSolver(TheoryArith& containing, NlModel& model) + : d_foundSatisfiability(false), d_containing(containing), d_model(model) +{ + d_ranVariable = + NodeManager::currentNM()->mkSkolem("__z", + NodeManager::currentNM()->realType(), + "", + NodeManager::SKOLEM_EXACT_NAME); +} + +CadSolver::~CadSolver() {} + +void CadSolver::initLastCall(const std::vector& assertions) +{ +#ifdef CVC4_POLY_IMP + if (Trace.isOn("nl-cad")) + { + Trace("nl-cad") << "CadSolver::initLastCall" << std::endl; + Trace("nl-cad") << "* Assertions: " << std::endl; + for (const Node& a : assertions) + { + Trace("nl-cad") << " " << a << std::endl; + } + } + // store or process assertions + d_CAC.reset(); + for (const Node& a : assertions) + { + d_CAC.getConstraints().addConstraint(a); + } + d_CAC.computeVariableOrdering(); +#else + Warning() << "Tried to use CadSolver but libpoly is not available. Compile " + "with --poly." + << std::endl; +#endif +} + +std::vector CadSolver::checkFull() +{ +#ifdef CVC4_POLY_IMP + std::vector lems; + auto covering = d_CAC.getUnsatCover(); + if (covering.empty()) + { + d_foundSatisfiability = true; + Trace("nl-cad") << "SAT: " << d_CAC.getModel() << std::endl; + } + else + { + d_foundSatisfiability = false; + auto mis = collectConstraints(covering); + Trace("nl-cad") << "Collected MIS: " << mis << std::endl; + auto* nm = NodeManager::currentNM(); + for (auto& n : mis) + { + n = n.negate(); + } + Assert(!mis.empty()) << "Infeasible subset can not be empty"; + if (mis.size() == 1) + { + lems.emplace_back(mis.front(), Inference::CAD_CONFLICT); + } + else + { + lems.emplace_back(nm->mkNode(Kind::OR, mis), Inference::CAD_CONFLICT); + } + Trace("nl-cad") << "UNSAT with MIS: " << lems.back().d_lemma << std::endl; + } + return lems; +#else + Warning() << "Tried to use CadSolver but libpoly is not available. Compile " + "with --poly." + << std::endl; +#endif +} + +bool CadSolver::constructModelIfAvailable(std::vector& assertions) +{ +#ifdef CVC4_POLY_IMP + if (!d_foundSatisfiability) + { + return false; + } + assertions.clear(); + for (const auto& v : d_CAC.getVariableOrdering()) + { + Node variable = d_CAC.getConstraints().varMapper()(v); + Node value = value_to_node(d_CAC.getModel().get(v), d_ranVariable); + if (value.isConst()) + { + d_model.addCheckModelSubstitution(variable, value); + } + else + { + d_model.addCheckModelWitness(variable, value); + } + Trace("nl-cad") << "-> " << v << " = " << value << std::endl; + } + return true; +#else + Warning() << "Tried to use CadSolver but libpoly is not available. Compile " + "with --poly." + << std::endl; +#endif +} + +} // namespace nl +} // namespace arith +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/arith/nl/cad_solver.h b/src/theory/arith/nl/cad_solver.h new file mode 100644 index 000000000..9fb243897 --- /dev/null +++ b/src/theory/arith/nl/cad_solver.h @@ -0,0 +1,94 @@ +/********************* */ +/*! \file cad_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 CAD-based solver based on https://arxiv.org/pdf/2003.05633.pdf. + **/ + +#ifndef CVC4__THEORY__ARITH__CAD_SOLVER_H +#define CVC4__THEORY__ARITH__CAD_SOLVER_H + +#include + +#include "expr/node.h" +#include "theory/arith/nl/cad/cdcac.h" +#include "theory/arith/nl/nl_model.h" +#include "theory/arith/theory_arith.h" + +namespace CVC4 { +namespace theory { +namespace arith { +namespace nl { + +/** + * A solver for nonlinear arithmetic that implements the CAD-based method + * described in https://arxiv.org/pdf/2003.05633.pdf. + */ +class CadSolver +{ + public: + CadSolver(TheoryArith& containing, NlModel& model); + ~CadSolver(); + + /** + * This is called at the beginning of last call effort check, where + * assertions are the set of assertions belonging to arithmetic, + * false_asserts is the subset of assertions that are false in the current + * model, and xts is the set of extended function terms that are active in + * the current context. + */ + void initLastCall(const std::vector& assertions); + + /** + * Perform a full check, returning either {} or a single lemma. + * If the result is empty, the input is satisfiable and a model is available + * for construct_model_if_available. Otherwise, the single lemma can be used + * as an infeasible subset. + */ + std::vector checkFull(); + + /** + * If a model is available (indicated by the last call to check_full() or + * check_partial()) this method puts a satisfying assignment in d_model, + * clears the list of assertions, and returns true. + * Otherwise, this method returns false. + */ + bool constructModelIfAvailable(std::vector& assertions); + + private: + /** + * The variable used to encode real algebraic numbers to nodes. + */ + Node d_ranVariable; + +#ifdef CVC4_POLY_IMP + /** + * The object implementing the actual decision procedure. + */ + cad::CDCAC d_CAC; +#endif + /** + * Indicates whether we found satisfiability in the last call to + * checkFullRefine. + */ + bool d_foundSatisfiability; + + /** The theory of arithmetic containing this extension.*/ + TheoryArith& d_containing; + /** Reference to the non-linear model object */ + NlModel& d_model; +}; /* class CadSolver */ + +} // namespace nl +} // namespace arith +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__ARITH__CAD_SOLVER_H */ diff --git a/src/theory/arith/nl/inference.h b/src/theory/arith/nl/inference.h index 99b7e681e..20c1a06a2 100644 --- a/src/theory/arith/nl/inference.h +++ b/src/theory/arith/nl/inference.h @@ -67,6 +67,11 @@ enum class Inference : uint32_t T_TANGENT, // secant refinement, the dual of the above inference T_SECANT, + //-------------------- cad solver + // conflict / infeasible subset obtained from cad + CAD_CONFLICT, + // excludes an interval for a single variable + CAD_EXCLUDED_INTERVAL, //-------------------- unknown UNKNOWN, }; diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index 4cb1c9fe6..9dbb95d93 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -42,6 +42,7 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing, d_model(containing.getSatContext()), d_trSlv(d_model), d_nlSlv(containing, d_model), + d_cadSlv(containing, d_model), d_iandSlv(containing, d_model), d_builtModel(containing.getSatContext(), false) { @@ -406,6 +407,10 @@ bool NonlinearExtension::checkModel(const std::vector& assertions, return false; } } + if (options::nlCad()) + { + d_cadSlv.constructModelIfAvailable(passertions); + } Trace("nl-ext-cm") << "-----" << std::endl; unsigned tdegree = d_trSlv.getTaylorDegree(); @@ -433,7 +438,11 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, // process lemmas that may have been generated by the transcendental solver filterLemmas(lemmas, lems); } - + if (options::nlCad()) + { + d_cadSlv.initLastCall(assertions); + } + // init last call with IAND d_iandSlv.initLastCall(assertions, false_asserts, xts); @@ -594,6 +603,15 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, filterLemmas(lemmas, wlems); } } + if (options::nlCad()) + { + lemmas = d_cadSlv.checkFull(); + if (lemmas.empty()) + { + Trace("nl-cad") << "nl-cad found SAT!" << std::endl; + } + filterLemmas(lemmas, wlems); + } // run the full refinement in the IAND solver lemmas = d_iandSlv.checkFullRefine(); filterLemmas(lemmas, wlems); diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index 6cc5c29d4..6fb8dbbfa 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -19,12 +19,14 @@ #define CVC4__THEORY__ARITH__NL__NONLINEAR_EXTENSION_H #include + #include #include #include "context/cdlist.h" #include "expr/kind.h" #include "expr/node.h" +#include "theory/arith/nl/cad_solver.h" #include "theory/arith/nl/iand_solver.h" #include "theory/arith/nl/nl_lemma_utils.h" #include "theory/arith/nl/nl_model.h" @@ -311,6 +313,8 @@ class NonlinearExtension * constraints involving nonlinear mulitplication, Cimatti et al., TACAS 2017. */ NlSolver d_nlSlv; + /** The CAD-based solver */ + CadSolver d_cadSlv; /** The integer and solver * * This is the subsolver responsible for running the procedure for