diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-04-05 15:47:40 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-05 18:47:40 +0000 |
| commit | b75f48683c08e66e0d47d29c5262f32f33b36c49 (patch) | |
| tree | 0a76b276add9a8d0acd3a52167747e5664f12569 /src/theory/bags | |
| parent | ca5fd891038a93bd63b3863faa8c5e39fff88ed0 (diff) | |
[proof-new] Registering proof checkers uniformly from the SMT solver (#6275)
Each theory has its own proof checker, responsible for checking the rules pertaining to that theory. The main proof checker uses these specialized checkers. Previously the main proof checker (of the proof node manager used across the SMT solver) was connected to these theory proof checkers during initialization of the theory. This commit adds an interface to the theories for retrieving its proof checker (analogous to how one retrieves the rewriter of a theory) which is used by a new method in the theory engine to register a theory proof checker to a given proof checker according to a theory id.
This is in preparation for the new unsat cores based on proofs.
Diffstat (limited to 'src/theory/bags')
| -rw-r--r-- | src/theory/bags/theory_bags.cpp | 3 | ||||
| -rw-r--r-- | src/theory/bags/theory_bags.h | 2 |
2 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp index bea83ce40..933f1b1a1 100644 --- a/src/theory/bags/theory_bags.cpp +++ b/src/theory/bags/theory_bags.cpp @@ -14,6 +14,7 @@ #include "theory/bags/theory_bags.h" +#include "expr/proof_checker.h" #include "smt/logic_exception.h" #include "theory/bags/normal_form.h" #include "theory/rewriter.h" @@ -50,6 +51,8 @@ TheoryBags::~TheoryBags() {} TheoryRewriter* TheoryBags::getTheoryRewriter() { return &d_rewriter; } +ProofRuleChecker* TheoryBags::getProofChecker() { return nullptr; } + bool TheoryBags::needsEqualityEngine(EeSetupInfo& esi) { esi.d_notify = &d_notify; diff --git a/src/theory/bags/theory_bags.h b/src/theory/bags/theory_bags.h index 7bb6111bd..7505f43bf 100644 --- a/src/theory/bags/theory_bags.h +++ b/src/theory/bags/theory_bags.h @@ -46,6 +46,8 @@ class TheoryBags : public Theory //--------------------------------- initialization /** get the official theory rewriter of this theory */ TheoryRewriter* getTheoryRewriter() override; + /** get the proof checker of this theory */ + ProofRuleChecker* getProofChecker() override; /** * Returns true if we need an equality engine. If so, we initialize the * information regarding how it should be setup. For details, see the |