summaryrefslogtreecommitdiff
path: root/src/theory/uf/eq_proof.cpp
AgeCommit message (Expand)Author
2021-07-27Fix eq proof conversion for constant merged parameterized ops (#6926)Andrew Reynolds
2021-07-14Generalize congruence handling for HO in eq proofs (#6883)Haniel Barbosa
2021-05-24Move proof utilities to src/proof/ (#6611)Andrew Reynolds
2021-05-13Add std::hash overloads for Node, TNode and TypeNode. (#6534)Mathias Preiner
2021-04-12Refactor and update copyright headers. (#6316)Aina Niemetz
2021-04-01Rename namespace CVC5 to cvc5. (#6258)Aina Niemetz
2021-03-31Rename namespace CVC4 to CVC5. (#6249)Aina Niemetz
2021-03-10Move ExprManager::isNAryKind to NodeManager. (#6107)Aina Niemetz
2021-03-09Update copyright headers to 2021. (#6081)Aina Niemetz
2021-03-03More cleanup of includes to reduce compilation times (#6037)Gereon Kremer
2021-03-02Clean up includes to reduce compile times (#6031)Gereon Kremer
2020-09-22Update copyright header script to support CMake and Python files (#5067)Mathias Preiner
2020-09-16[proof-new] Extending eqproof conversion to HO congruence (#5071)Haniel Barbosa
2020-09-01Removes old proof code (#4964)Haniel Barbosa
2020-08-12[proof-new] Adding support for corner case of transitivity simulating MERGED_...Haniel Barbosa
2020-08-12generalize handling MERGED_THROUGH_CONSTANST in EqProof conversion (#4878)Haniel Barbosa
2020-07-16Fix EqProof to ProofNode conversion (#4760)Haniel Barbosa
2020-07-16(proof-new) Implements the conversion between EqProof and ProofNode (#4756)Haniel Barbosa
2020-07-15(proof-new) Adding API for converting EqProof into ProofNode (#4747)Haniel Barbosa
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback