diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-05-27 16:28:58 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-27 21:28:58 +0000 |
| commit | 8b3de13131d24bf400ba5f36fc234008d950f345 (patch) | |
| tree | 0de3a60dcdad716cede78b8fe024996690399a2f /test | |
| parent | b9062490a7590708bcf158d4670a23d859fe3355 (diff) | |
Update proof namespaces (#6614)
This removes namespace theory from proof utilities, and moves MethodId to its own file in src/proof/.
Diffstat (limited to 'test')
| -rw-r--r-- | test/unit/test_smt.h | 12 |
1 files changed, 3 insertions, 9 deletions
diff --git a/test/unit/test_smt.h b/test/unit/test_smt.h index a81deabc2..672693366 100644 --- a/test/unit/test_smt.h +++ b/test/unit/test_smt.h @@ -115,10 +115,7 @@ class DummyOutputChannel : public cvc5::theory::OutputChannel void safePoint(Resource r) override {} void conflict(TNode n) override { push(CONFLICT, n); } - void trustedConflict(theory::TrustNode n) override - { - push(CONFLICT, n.getNode()); - } + void trustedConflict(TrustNode n) override { push(CONFLICT, n.getNode()); } bool propagate(TNode n) override { @@ -132,7 +129,7 @@ class DummyOutputChannel : public cvc5::theory::OutputChannel push(LEMMA, n); } - void trustedLemma(theory::TrustNode n, theory::LemmaProperty p) override + void trustedLemma(TrustNode n, theory::LemmaProperty p) override { push(LEMMA, n.getNode()); } @@ -250,10 +247,7 @@ class DummyTheory : public theory::Theory // do not assert to equality engine, since this theory does not use one return true; } - theory::TrustNode explain(TNode n) override - { - return theory::TrustNode::null(); - } + TrustNode explain(TNode n) override { return TrustNode::null(); } Node getValue(TNode n) { return Node::null(); } std::string identify() const override { return "DummyTheory" + d_id; } |