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.h | |
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.h')
-rw-r--r-- | src/theory/arith/nl/cad_solver.h | 94 |
1 files changed, 94 insertions, 0 deletions
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 <vector> + +#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<Node>& 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<NlLemma> 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<Node>& 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 */ |