diff options
author | Guy <katz911@gmail.com> | 2016-07-26 13:09:31 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-07-26 13:09:31 -0700 |
commit | 319bbda7ad32e6e9ee009c27003f6f1c0a8d7b20 (patch) | |
tree | 9648cdfb58b5f132d9a40a919dac792ad6da3c34 /src/proof/proof_manager.h | |
parent | cb835bd526296d97f8ceb001569493723a59f86b (diff) |
Added functionality to retrieve a lemma's "weakest implicant" in the unsat core. Currently, lemmas that are not conjunctions and their own weakest implicants; but for lemmas that *are* conjunctions, we may return only a subset of the conjuncts.
Diffstat (limited to 'src/proof/proof_manager.h')
-rw-r--r-- | src/proof/proof_manager.h | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index b1cfc54b5..23d7d1972 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -248,6 +248,7 @@ public: bool unsatCoreAvailable() const; void getLemmasInUnsatCore(theory::TheoryId theory, std::vector<Node> &lemmas); + Node getWeakestImplicantInUnsatCore(Node lemma); int nextId() { return d_nextId++; } @@ -271,6 +272,10 @@ public: ProofLetMap& letMap, std::ostream& out, std::ostringstream& paren); + +private: + void constructSatProof(); + std::set<Node> satClauseToNodeSet(prop::SatClause* clause); };/* class ProofManager */ class LFSCProof : public Proof { |