diff options
author | Gereon Kremer <gkremer@stanford.edu> | 2021-02-11 20:00:18 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-02-11 20:00:18 +0100 |
commit | f5486884229348516ac26300273e4f5458a74208 (patch) | |
tree | 8e48bd833c3e55b247adca891ec2081fc9077528 /src/theory/theory_inference.cpp | |
parent | 8fcb59d072b09bfaf8f56334182d425274842461 (diff) |
Add InferenceId member to TheoryInference, adapt all derived classes. (#5894)
This PR adds a new InferenceId member to the TheoryInference class.
All classes derived from TheoryInference are adapted accordingly.
Diffstat (limited to 'src/theory/theory_inference.cpp')
-rw-r--r-- | src/theory/theory_inference.cpp | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/src/theory/theory_inference.cpp b/src/theory/theory_inference.cpp index 8e52c8cd1..f64b88daa 100644 --- a/src/theory/theory_inference.cpp +++ b/src/theory/theory_inference.cpp @@ -21,10 +21,11 @@ using namespace CVC4::kind; namespace CVC4 { namespace theory { -SimpleTheoryLemma::SimpleTheoryLemma(Node n, +SimpleTheoryLemma::SimpleTheoryLemma(InferenceId id, + Node n, LemmaProperty p, ProofGenerator* pg) - : d_node(n), d_property(p), d_pg(pg) + : TheoryInference(id), d_node(n), d_property(p), d_pg(pg) { } @@ -36,10 +37,11 @@ bool SimpleTheoryLemma::process(TheoryInferenceManager* im, bool asLemma) return im->trustedLemma(TrustNode::mkTrustLemma(d_node, d_pg), d_property); } -SimpleTheoryInternalFact::SimpleTheoryInternalFact(Node conc, +SimpleTheoryInternalFact::SimpleTheoryInternalFact(InferenceId id, + Node conc, Node exp, ProofGenerator* pg) - : d_conc(conc), d_exp(exp), d_pg(pg) + : TheoryInference(id), d_conc(conc), d_exp(exp), d_pg(pg) { } |