diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2020-05-15 18:39:57 -0300 |
|---|---|---|
| committer | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2020-05-15 18:39:57 -0300 |
| commit | 9dfc7947a67b39b724ccb56e2e3f4a08f28d6386 (patch) | |
| tree | 46f6312da1c36dcd505809894f096d8b555bacfa /src/theory/uf/eq_proof.h | |
| parent | 501e1776ec298772181c4fed30c5d0a413c4da0f (diff) | |
introducing search for building better transitivity proofs
Diffstat (limited to 'src/theory/uf/eq_proof.h')
| -rw-r--r-- | src/theory/uf/eq_proof.h | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/theory/uf/eq_proof.h b/src/theory/uf/eq_proof.h index 2a426a187..42783d31f 100644 --- a/src/theory/uf/eq_proof.h +++ b/src/theory/uf/eq_proof.h @@ -97,6 +97,9 @@ class EqProof CDProof* p, std::unordered_set<Node, NodeHashFunction>& assumptions) const; + bool buildTransitivityChain(Node conclusion, std::vector<Node>& premises) const; + + // returns whether it did reordering void maybeAddSymmOrTrueIntroToProof(unsigned i, std::vector<Node>& premises, bool first, |