diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-08-19 23:06:57 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-19 16:06:57 -0500 |
| commit | 6710b082bc6fa8c7f67203a4013657e069479119 (patch) | |
| tree | 3f3ba1065e1100e86526a0b13ab26c759e77f1c2 /src/theory/arith/nl/cad_solver.h | |
| parent | 31717bf7c014bf1971cabcc9b871de5818278126 (diff) | |
(cad solver) Add a partial check method. (#4904)
This PR extends the CAD-based solver to enable partial checks. Essentially, we only collect the first interval that is excluded for the first variable and return that one as a lemma. This does not leave a lot of choice on "how partial" the check should be, but it is fairly easy to implement and does not add additional overhead.
It also fixes some confusion in excluding_interval_to_lemma...
Diffstat (limited to 'src/theory/arith/nl/cad_solver.h')
| -rw-r--r-- | src/theory/arith/nl/cad_solver.h | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/theory/arith/nl/cad_solver.h b/src/theory/arith/nl/cad_solver.h index 9fb243897..6f6c0d43c 100644 --- a/src/theory/arith/nl/cad_solver.h +++ b/src/theory/arith/nl/cad_solver.h @@ -55,6 +55,14 @@ class CadSolver std::vector<NlLemma> checkFull(); /** + * Perform a partial check, returning either {} or a list of lemmas. + * If the result is empty, the input is satisfiable and a model is available + * for construct_model_if_available. Otherwise, the lemmas exclude some part + * of the search space. + */ + std::vector<NlLemma> checkPartial(); + + /** * 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. |