diff options
author | lianah <lianahady@gmail.com> | 2013-10-08 19:22:19 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-10-08 19:22:19 -0400 |
commit | 000f574406c29df4c60947169ef527ee5316beb7 (patch) | |
tree | e2bc0426627689ccd59d63976c9497cb9f0dc335 /src/smt/smt_engine.cpp | |
parent | 3361081acd11178d0eb580ce91279a2ecaa7aa65 (diff) |
added currying for uf proofs; still needs debugging
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index be6acd09c..5a3334d64 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -38,6 +38,7 @@ #include "expr/node.h" #include "expr/node_self_iterator.h" #include "prop/prop_engine.h" +#include "proof/theory_proof.h" #include "smt/modal_exception.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" @@ -46,6 +47,7 @@ #include "theory/bv/theory_bv_rewriter.h" #include "proof/proof_manager.h" #include "util/proof.h" +#include "proof/proof.h" #include "util/boolean_simplification.h" #include "util/node_visitor.h" #include "util/configuration.h" @@ -3103,6 +3105,11 @@ void SmtEngine::ensureBoolean(const Expr& e) throw(TypeCheckingException) { Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalException, LogicException) { Assert(ex.isNull() || ex.getExprManager() == d_exprManager); + // PROOF ( + ProofManager* pm = ProofManager::currentPM(); + TheoryProof* pf = pm->getTheoryProof(); + pf->assertFormula(ex); + // ); SmtScope smts(this); finalOptionsAreSet(); doPendingPops(); @@ -3246,6 +3253,8 @@ Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalExcept Result SmtEngine::assertFormula(const Expr& ex) throw(TypeCheckingException, LogicException) { Assert(ex.getExprManager() == d_exprManager); + //PROOF ( + ProofManager::currentPM()->getTheoryProof()->assertFormula(ex); //); SmtScope smts(this); finalOptionsAreSet(); doPendingPops(); |