diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-26 17:15:02 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-02-26 17:15:02 -0600 |
| commit | 19392f3e588287b2f0838f90b7e1a6adcf690063 (patch) | |
| tree | f5b989f2c5398122b7e7098360be5542ba7e5c69 /src/theory/arith/nonlinear_extension.cpp | |
| parent | 8e476f1efeb7f8b3188ea1795ccd27f98f41e4d2 (diff) | |
Infrastructure for tautological literals in nonlinear solver (#3795)
Work towards CVC4/cvc4-projects#113 and #3783.
This PR adds the ability to mark certain literals as being tautological, since they can be assumed to hold in all models. This is important for internally generated literals whose purpose is to guide models generated by the linear solver but should not hinder our ability to answer "sat".
This PR is required for further refactoring of check-model for transcendental functions.
Diffstat (limited to 'src/theory/arith/nonlinear_extension.cpp')
| -rw-r--r-- | src/theory/arith/nonlinear_extension.cpp | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp index bcf7cae14..94c925131 100644 --- a/src/theory/arith/nonlinear_extension.cpp +++ b/src/theory/arith/nonlinear_extension.cpp @@ -559,6 +559,8 @@ void NonlinearExtension::sendLemmas(const std::vector<Node>& out, { d_lemmas.insert(lem); } + // also indicate this is a tautology + d_model.addTautology(lem); } } |