diff options
author | Guy <katz911@gmail.com> | 2016-06-08 11:52:42 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-06-08 11:52:42 -0700 |
commit | 4b8f92d23f7a75b4148f41e039f7bdc5f165babc (patch) | |
tree | e2d8abdff6f2d6befa652a09188fff991caf1cf4 /src/proof/proof_manager.h | |
parent | 8bfab32eed06973d53ce8ae066a9a26d4ae8a489 (diff) |
Support for printing a global let map in LFSC proofs.
Added a flag to enable/disbale this feature (enabled by default).
Also, added some infrastructure for proving rewrite rules.
Diffstat (limited to 'src/proof/proof_manager.h')
-rw-r--r-- | src/proof/proof_manager.h | 41 |
1 files changed, 40 insertions, 1 deletions
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index c6454b652..14793f380 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -22,6 +22,7 @@ #include <iosfwd> #include <map> #include "proof/proof.h" +#include "proof/proof_utils.h" #include "proof/skolemization_manager.h" #include "util/proof.h" #include "expr/node.h" @@ -115,6 +116,30 @@ enum ProofRule { RULE_ARRAYS_ROW, /* arrays, read-over-write */ };/* enum ProofRules */ +class RewriteLogEntry { +public: + RewriteLogEntry(unsigned ruleId, Node original, Node result) + : d_ruleId(ruleId), d_original(original), d_result(result) { + } + + unsigned getRuleId() const { + return d_ruleId; + } + + Node getOriginal() const { + return d_original; + } + + Node getResult() const { + return d_result; + } + +private: + unsigned d_ruleId; + Node d_original; + Node d_result; +}; + class ProofManager { CoreSatProof* d_satProof; CnfProof* d_cnfProof; @@ -140,6 +165,8 @@ class ProofManager { std::map<std::string, std::string> d_rewriteFilters; + std::vector<RewriteLogEntry> d_rewriteLog; + protected: LogicInfo d_logic; @@ -231,6 +258,16 @@ public: void addRewriteFilter(const std::string &original, const std::string &substitute); void clearRewriteFilters(); + static void registerRewrite(unsigned ruleId, Node original, Node result); + static void clearRewriteLog(); + + std::vector<RewriteLogEntry> getRewriteLog(); + void dumpRewriteLog() const; + + void printGlobalLetMap(std::set<Node>& atoms, + ProofLetMap& letMap, + std::ostream& out, + std::ostringstream& paren); };/* class ProofManager */ class LFSCProof : public Proof { @@ -242,13 +279,15 @@ class LFSCProof : public Proof { // FIXME: hack until we get preprocessing void printPreprocessedAssertions(const NodeSet& assertions, std::ostream& os, - std::ostream& paren); + std::ostream& paren, + ProofLetMap& globalLetMap); public: LFSCProof(SmtEngine* smtEngine, LFSCCoreSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProofEngine* theory); virtual void toStream(std::ostream& out); + virtual void toStream(std::ostream& out, const ProofLetMap& map); virtual ~LFSCProof() {} };/* class LFSCProof */ |