diff options
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/proof_manager.cpp | 7 | ||||
-rw-r--r-- | src/proof/proof_manager.h | 1 |
2 files changed, 7 insertions, 1 deletions
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index 0f9cfa710..2d8c4178a 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -204,7 +204,7 @@ void ProofManager::addAssertion(Expr formula, bool inUnsatCore) { Debug("cores") << "assert: " << formula << std::endl; d_inputFormulas.insert(formula); d_deps[Node::fromExpr(formula)]; // empty vector of deps - if(inUnsatCore || options::dumpUnsatCores()) { + if(inUnsatCore || options::dumpUnsatCores() || options::checkUnsatCores()) { Debug("cores") << "adding to input core forms: " << formula << std::endl; d_inputCoreFormulas.insert(formula); } @@ -221,6 +221,11 @@ void ProofManager::addDependence(TNode n, TNode dep) { } } +void ProofManager::addUnsatCore(Expr formula) { + Assert (d_inputCoreFormulas.find(formula) != d_inputCoreFormulas.end()); + d_outputCoreFormulas.insert(formula); +} + void ProofManager::setLogic(const LogicInfo& logic) { d_logic = logic; } diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index 43d6723fa..ee99b0159 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -171,6 +171,7 @@ public: void addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind); // note that n depends on dep (for cores) void addDependence(TNode n, TNode dep); + void addUnsatCore(Expr formula); assertions_iterator begin_unsat_core() const { return d_outputCoreFormulas.begin(); } assertions_iterator end_unsat_core() const { return d_outputCoreFormulas.end(); } |