diff options
author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-08-04 12:57:34 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-04 05:57:34 -0500 |
commit | 4844afa3d254bdabac397556e166a2534bb6c2ac (patch) | |
tree | 1da4a957cf073c25c6cfc9a7393afe29a1b14b3b /src/theory/arith/nl/cad_solver.cpp | |
parent | c84db77ecdaa7107a33824484bf9c649f8fcbbff (diff) |
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)
Diffstat (limited to 'src/theory/arith/nl/cad_solver.cpp')
-rw-r--r-- | src/theory/arith/nl/cad_solver.cpp | 141 |
1 files changed, 141 insertions, 0 deletions
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 <poly/polyxx.h> +#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<Node>& 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<NlLemma> CadSolver::checkFull() +{ +#ifdef CVC4_POLY_IMP + std::vector<NlLemma> 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<Node>& 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 |