diff options
author | guykatzz <katz911@gmail.com> | 2017-03-17 14:11:41 -0700 |
---|---|---|
committer | guykatzz <katz911@gmail.com> | 2017-03-17 14:12:04 -0700 |
commit | 768534c0973788cab0097c6485e5113da1d406da (patch) | |
tree | 32e8eda1c7882f05b16c4bbec4e4095efbec34d3 /src/proof/proof_manager.h | |
parent | afe84522b87b6fc0ad5d0e9a396b61f7b523f674 (diff) |
better support for proof production when encountering bool terms: handle the new proof constructs generated by the equality engine.
proof production for bool-array.smt2 passes
Diffstat (limited to 'src/proof/proof_manager.h')
-rw-r--r-- | src/proof/proof_manager.h | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index fa7224d72..19215589f 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -206,6 +206,8 @@ public: return d_inputFormulas.find(assertion) != d_inputFormulas.end(); } + void ensureLiteral(Node node); + //---from Morgan--- Node mkOp(TNode n); Node lookupOp(TNode n) const; @@ -230,6 +232,7 @@ public: static std::string getAtomName(TNode atom, const std::string& prefix = ""); static std::string getLitName(prop::SatLiteral lit, const std::string& prefix = ""); static std::string getLitName(TNode lit, const std::string& prefix = ""); + static bool hasLitName(TNode lit); // for SMT variable names that have spaces and other things static std::string sanitize(TNode var); @@ -265,6 +268,7 @@ public: void addRewriteFilter(const std::string &original, const std::string &substitute); void clearRewriteFilters(); + bool haveRewriteFilter(TNode lit); void addAssertionFilter(const Node& node, const std::string& rewritten); |