diff options
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. |