summaryrefslogtreecommitdiff
path: root/src/theory/uf
AgeCommit message (Expand)Author
2020-12-09Fixed a bunch of clang warnings. (#5637)Gereon Kremer
2020-12-03Use mkAnd where the number of children may be less than two. (#5551)Gereon Kremer
2020-12-02Update copyright headers.Aina Niemetz
2020-12-02Rename macro Message to CVC4Message. (#5576)Aina Niemetz
2020-11-23Change UF ho to ppRewrite instead of expand definition (#5499)Andrew Reynolds
2020-11-12(proof-new) Separate explanation stages in proof equality engine (#5356)Andrew Reynolds
2020-11-12(proof-new) Fix true explanations of propagations in pf equality engine (#5338)Andrew Reynolds
2020-10-23[proof-new] Fix n-ary kind handling in EqEngine explanations (#5332)Haniel Barbosa
2020-10-23Fix related to preregistering boolean term variables in strings (#5331)Andrew Reynolds
2020-10-22Remove unused equality engine types (#5319)Andrew Reynolds
2020-10-20Fix compiler warnings. (#5305)Aina Niemetz
2020-10-20(proof-new) Update add lazy step interface in LazyCDProof (#5299)Andrew Reynolds
2020-10-20Fix miscellaneous warnings (#5256)Andrew Reynolds
2020-10-12Remove uf-ss-totality option (#5251)Andrew Reynolds
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-15[proof-new] A simple proof generator for buffered proof steps (#5069)Haniel Barbosa
2020-09-15(proof-new) Make proofs mandatory in proof equality engine (#5059)Andrew Reynolds
2020-09-14Standard equality engine notify class for Theory (#5042)Andrew Reynolds
2020-09-14Standardize uses of inference manager in datatypes (#5035)Andrew Reynolds
2020-09-11Move finite model minimization to UF last call effort (#5050)Andrew Reynolds
2020-09-11(proof-new) Handle mismatched assumptions in proof equality engine during mkS...Andrew Reynolds
2020-09-11(proof-new) Use deep copy for final lemma step in proof equality engine (#5013)Andrew Reynolds
2020-09-09Use state and inference manager in UF CardinalityExtension (#5036)Andrew Reynolds
2020-09-03Add interfaces for making trust nodes in TheoryInferenceManager. (#5016)Andrew Reynolds
2020-09-02(proof-new) Add proof support in TheoryUF (#5002)Andrew Reynolds
2020-09-01Removes old proof code (#4964)Haniel Barbosa
2020-08-31Basic proof support in inference manager (#4975)Andrew Reynolds
2020-08-28Replace Theory::Set with TheoryIdSet (#4959)Andrew Reynolds
2020-08-27(proof-new) Add the proof equality engine (#4881)Andrew Reynolds
2020-08-26(new theory) Update TheoryUF to new interface (#4944)Andrew Reynolds
2020-08-24Add a few basic extensions for equality engine (#4937)Andrew Reynolds
2020-08-24Extend the standard Theory template based on equality engine (#4929)Andrew Reynolds
2020-08-21Remove spurious theory methods calls (#4931)Andrew Reynolds
2020-08-21Simplify and fix care graph for ufHo (#4924)Andrew Reynolds
2020-08-20Add TheoryState objects to each Theory (#4920)Andrew Reynolds
2020-08-19Simplify trigger notifications in equality engine (#4921)Andrew Reynolds
2020-08-17Dynamic allocation of equality engine in Theory (#4890)Andrew Reynolds
2020-08-14Simplify equality engine notifications (#4896)Andrew Reynolds
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-08-12(proof-new) Improve robustness of CONG rule (#4882)Andrew Reynolds
2020-08-12(proof-new) Improving proof-production in Equality Engine (#4871)Haniel Barbosa
2020-08-09Make valuation class more robust to null underlying TheoryEngine. (#4864)Andrew Reynolds
2020-08-09Splitting a few utility classes from EqualityEngine to their own file (#4862)Andrew Reynolds
2020-07-17Improving equality engine tracing (#4770)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
2020-07-10(proof-new) Update Theory interface for proof-new (#4648)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback