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/cad_solver.h | |
| 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/cad_solver.h')
| -rw-r--r-- | src/theory/arith/nl/cad_solver.h | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/theory/arith/nl/cad_solver.h b/src/theory/arith/nl/cad_solver.h index 4d537213f..21fbbab2e 100644 --- a/src/theory/arith/nl/cad_solver.h +++ b/src/theory/arith/nl/cad_solver.h @@ -20,6 +20,7 @@ #include "expr/node.h" #include "theory/arith/inference_manager.h" #include "theory/arith/nl/cad/cdcac.h" +#include "theory/arith/nl/cad/proof_checker.h" #include "theory/arith/nl/nl_model.h" namespace CVC4 { @@ -34,7 +35,10 @@ namespace nl { class CadSolver { public: - CadSolver(InferenceManager& im, NlModel& model); + CadSolver(InferenceManager& im, + NlModel& model, + context::Context* ctx, + ProofNodeManager* pnm); ~CadSolver(); /** @@ -81,6 +85,8 @@ class CadSolver * The object implementing the actual decision procedure. */ cad::CDCAC d_CAC; + /** The proof checker for cad proofs */ + cad::CADProofRuleChecker d_proofChecker; #endif /** * Indicates whether we found satisfiability in the last call to |