summaryrefslogtreecommitdiff
path: root/src/theory/uf
AgeCommit message (Expand)Author
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
2020-06-16Update copyright headers.Aina Niemetz
2020-06-03(proof-new) Adding rules and proof checker for EUF (#4559)Haniel Barbosa
2020-04-18Improving EqProof printing (#4329)Haniel Barbosa
2020-04-14Remove mergePredicates from EqualityEngine interface (#4305)Andrew Reynolds
2020-04-08Perform theory widening eagerly (#4044)Andres Noetzli
2020-04-03Update theory rewriter ownership, add stats to strings (#4202)Andres Noetzli
2020-04-01Initialize theory rewriters in theories (#4197)Andres Noetzli
2020-03-20Guard cases of sort inference in quantifier free logics in uf cardinality (#4...Andrew Reynolds
2020-03-16Create master equality engine at context level 0 (#4081)Andres Noetzli
2020-03-11Fix double notify in equality engine (#4036)Andrew Reynolds
2020-03-05Enable -Wshadow and fix warnings. (#3909)Mathias Preiner
2020-02-26Initial work towards -Wshadow (#3817)Andrew Reynolds
2020-02-25remove redundant includes (#3815)yoni206
2020-02-19resource manager: Add statistic for every resource. (#3772)Mathias Preiner
2019-12-17Generate code for options with modes. (#3561)Mathias Preiner
2019-12-09Make theory rewriters non-static (#3547)Andres Noetzli
2019-11-18Use -Wimplicit-fallthrough (#3464)Andres Noetzli
2019-11-04Fix ho extensionality in collect model info (#3435)Andrew Reynolds
2019-10-31Fix Unimplemented() macros missed in #3366. (#3424)Mathias Preiner
2019-10-30Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)Mathias Preiner
2019-10-27Fix collect model info for higher-order (#3409)Andrew Reynolds
2019-09-19Support context-(in)dependent decision strategies. (#3281)Andrew Reynolds
2019-09-13Move higher-order matching predicate (#3280)Andrew Reynolds
2019-09-12 Rename UF with cardinality extension (#3241)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback