diff options
author | Guy <katz911@gmail.com> | 2016-06-20 14:20:15 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-06-20 14:20:15 -0700 |
commit | a592e0137504c5788084cb8e150f46f109f566d7 (patch) | |
tree | 0816b285c639e0121a1d0a63033ad29bf25b5e35 /src/proof/theory_proof.h | |
parent | 4b8972fec229012812bb7edc9e315c2e54f7c059 (diff) |
Addressed a bug that occurs when proof production is triggered via text flags in the input.
Separated some initialization into two phases:
1. Those that can be done when the proof compiliation flag is set
2. Those that can be done only when the --proof option is set.
For #2, deferred their execution until the text flags in the input have been processed
Diffstat (limited to 'src/proof/theory_proof.h')
-rw-r--r-- | src/proof/theory_proof.h | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h index f6f00fa11..5907f9bd5 100644 --- a/src/proof/theory_proof.h +++ b/src/proof/theory_proof.h @@ -130,10 +130,19 @@ public: /** * Ensures that a theory proof class for the given theory is created. + * This method can be invoked regardless of whether the "proof" option + * has been set. * * @param theory */ void registerTheory(theory::Theory* theory); + /** + * Additional configuration of the theory proof class for the given theory. + * This method should only be invoked when the "proof" option has been set. + * + * @param theory + */ + void finishRegisterTheory(theory::Theory* theory); theory::TheoryId getTheoryForLemma(const prop::SatClause* clause); TheoryProof* getTheoryProof(theory::TheoryId id); |