diff options
Diffstat (limited to 'src/theory/uf/proof_equality_engine.h')
| -rw-r--r-- | src/theory/uf/proof_equality_engine.h | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h index 0c093d4b2..baf155dac 100644 --- a/src/theory/uf/proof_equality_engine.h +++ b/src/theory/uf/proof_equality_engine.h @@ -23,6 +23,7 @@ #include "context/cdhashmap.h" #include "context/cdhashset.h" #include "expr/node.h" +#include "proof/assumption_proof_generator.h" #include "proof/buffered_proof_generator.h" #include "proof/eager_proof_generator.h" #include "proof/lazy_proof.h" @@ -278,6 +279,8 @@ class ProofEqEngine : public EagerProofGenerator eq::EqualityEngine& d_ee; /** The default proof generator (for simple facts) */ BufferedProofGenerator d_factPg; + /** The no-explain proof generator */ + AssumptionProofGenerator d_assumpPg; /** common nodes */ Node d_true; Node d_false; |