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_utils.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_utils.h')
-rw-r--r-- | src/proof/proof_utils.h | 52 |
1 files changed, 52 insertions, 0 deletions
diff --git a/src/proof/proof_utils.h b/src/proof/proof_utils.h index 8c734c892..546d419fc 100644 --- a/src/proof/proof_utils.h +++ b/src/proof/proof_utils.h @@ -32,6 +32,58 @@ typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet; typedef std::pair<Node, Node> NodePair; typedef std::set<NodePair> NodePairSet; + +struct ProofLetCount { + static unsigned counter; + static void resetCounter() { counter = 0; } + static unsigned newId() { return ++counter; } + + unsigned count; + unsigned id; + ProofLetCount() + : count(0) + , id(-1) + {} + + void increment() { ++count; } + ProofLetCount(unsigned i) + : count(1) + , id(i) + {} + + ProofLetCount(const ProofLetCount& other) + : count(other.count) + , id (other.id) + {} + + bool operator==(const ProofLetCount &other) const { + return other.id == id && other.count == count; + } + + ProofLetCount& operator=(const ProofLetCount &rhs) { + if (&rhs == this) return *this; + id = rhs.id; + count = rhs.count; + return *this; + } +}; + +struct LetOrderElement { + Expr expr; + unsigned id; + LetOrderElement(Expr e, unsigned i) + : expr(e) + , id(i) + {} + + LetOrderElement() + : expr() + , id(-1) + {} +}; + +typedef std::vector<LetOrderElement> Bindings; + namespace utils { std::string toLFSCKind(Kind kind); |