diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-02-24 16:04:59 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-24 16:04:59 +0100 |
| commit | 6478f414ad7d6dcbf597db037e81d97175757605 (patch) | |
| tree | 976de5c11f2cf0b32005fe85b90f6b2d586c2213 /src/theory/arith/nl/nonlinear_extension.cpp | |
| parent | 6d45b6fb6f797eb9dc51ea70b20ec875d1dfe49d (diff) | |
(proof-new) Add proofs for CAD solver (#5981)
This PR adds proofs for the CAD solver, based on the proof generator from the previous PR.
Note that the level of detail of these CAD proofs is significantly higher than for other proofs. Making these proofs more fine-grained and maybe at some point accessible to proof checkers is probably still quite a bit of work.
Thus, the CAD proof rules are both trusted rules for now.
Diffstat (limited to 'src/theory/arith/nl/nonlinear_extension.cpp')
| -rw-r--r-- | src/theory/arith/nl/nonlinear_extension.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index 4d29f1955..c46781e76 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -54,7 +54,7 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing, d_monomialSlv(&d_extState), d_splitZeroSlv(&d_extState), d_tangentPlaneSlv(&d_extState), - d_cadSlv(d_im, d_model), + d_cadSlv(d_im, d_model, state.getUserContext(), pnm), d_icpSlv(d_im), d_iandSlv(d_im, state, d_model), d_builtModel(containing.getSatContext(), false) |