diff options
Diffstat (limited to 'src/theory/uf/eq_proof.h')
| -rw-r--r-- | src/theory/uf/eq_proof.h | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/src/theory/uf/eq_proof.h b/src/theory/uf/eq_proof.h index 8bbda51ba..2a426a187 100644 --- a/src/theory/uf/eq_proof.h +++ b/src/theory/uf/eq_proof.h @@ -81,7 +81,8 @@ class EqProof */ Node addToProof( CDProof* p, - std::unordered_map<Node, Node, NodeHashFunction>& visited) const; + std::unordered_map<Node, Node, NodeHashFunction>& visited, + std::unordered_set<Node, NodeHashFunction>& assumptions) const; /** Removes all reflexivity steps, i.e. premises (= t t), from premises * * Such premisis are spurious for a trastivity steps. The reordering of @@ -90,9 +91,11 @@ class EqProof */ void cleanReflPremisesInTranstivity(std::vector<Node>& premises) const; - bool foldTransitivityChildren(Node conclusion, - std::vector<Node>& premises, - CDProof* p) const; + bool foldTransitivityChildren( + Node conclusion, + std::vector<Node>& premises, + CDProof* p, + std::unordered_set<Node, NodeHashFunction>& assumptions) const; void maybeAddSymmOrTrueIntroToProof(unsigned i, std::vector<Node>& premises, @@ -105,7 +108,8 @@ class EqProof Node conclusion, std::vector<std::vector<Node>>& children, CDProof* p, - std::unordered_map<Node, Node, NodeHashFunction>& visited) const; + std::unordered_map<Node, Node, NodeHashFunction>& visited, + std::unordered_set<Node, NodeHashFunction>& assumptions) const; }; /* class EqProof */ |