summaryrefslogtreecommitdiff
path: root/src/theory/sets
AgeCommit message (Expand)Author
2021-11-12Remove `ConstantMap<Rational>` (#7635)Andres Noetzli
2021-11-10sets: Rename set.intersection to set.inter. (#7622)Aina Niemetz
2021-11-08expand bag.choose operator (#7481)mudathirmahgoub
2021-11-08sets: Rename kinds with a more consistent naming scheme. (#7595)Aina Niemetz
2021-11-05Remove many static calls to rewrite (#7580)Andrew Reynolds
2021-11-03Refactor skolem construction (#7561)Andrew Reynolds
2021-11-01Eliminate calls to Rewriter::rewrite and options:: in sets and bags (#7550)Andrew Reynolds
2021-11-01Fix upwards closure for relations (#7515)Andrew Reynolds
2021-10-27Fix model unsoundness for relation join (#7511)Andrew Reynolds
2021-10-22Refactor theory inference manager constructor (#7457)Andrew Reynolds
2021-10-20api: Improve documentation for special cases with nullary ops. (#7433)Aina Niemetz
2021-10-04Move isFiniteType from theory engine to Env (#7287)Andrew Reynolds
2021-09-13Remove context getters from `TheoryState` (#7174)Andres Noetzli
2021-09-07Use `EnvObj` methods instead of `Theory` methods (#7144)Andres Noetzli
2021-09-03EnvObj: Add options(), context(), userContext(). (#7137)Aina Niemetz
2021-08-16Push Env class into TheoryState (#7012)Gereon Kremer
2021-08-16Make Theory class use Env (#7011)Gereon Kremer
2021-08-04Add missing inference identifiers (#6962)Andrew Reynolds
2021-07-26Enable default equality proofs for sets (#6931)Andrew Reynolds
2021-07-22Miscellaneous changes in preparation for central equality engine (#6900)Andrew Reynolds
2021-07-09Fix sets cardinality inference involving equivalent parents (#6855)Andrew Reynolds
2021-06-22Set up fine grained equality notifications (#6734)Andrew Reynolds
2021-05-26 More precise includes of `Node` constants (#6617)Andres Noetzli
2021-05-24Move proof utilities to src/proof/ (#6611)Andrew Reynolds
2021-05-19Add more missing inference ids (#6313)Andrew Reynolds
2021-05-13Add std::hash overloads for Node, TNode and TypeNode. (#6534)Mathias Preiner
2021-04-23(proof-new) Proofs for sets purification lemmas (#6416)Andrew Reynolds
2021-04-22Move expand definition from Theory to TheoryRewriter (#6408)Andrew Reynolds
2021-04-21Goodbye CVC4, hello cvc5! (#6371)Mathias Preiner
2021-04-21Sets: Move implementation of type rules to cpp. (#6401)Aina Niemetz
2021-04-15Rename occurrences of CVC4 to CVC5. (#6351)Aina Niemetz
2021-04-14Fix type rule for relations join image (#6349)Andrew Reynolds
2021-04-14Refactor / reimplement statistics (#6162)Gereon Kremer
2021-04-14Rename public and private headers in src/include. (#6352)Aina Niemetz
2021-04-12Fix computation of whether a type is finite (#6312)Andrew Reynolds
2021-04-12Refactor and update copyright headers. (#6316)Aina Niemetz
2021-04-09Rename CVC4__ header guards to CVC5__. (#6326)Aina Niemetz
2021-04-08Add identifiers for sources of incompleteness (#6311)Andrew Reynolds
2021-04-07Replace calls to NodeManager::mkSkolem with SkolemManager::mkDummySkolem (#6291)Andrew Reynolds
2021-04-06Remove template argument from `NodeBuilder` (#6290)Andres Noetzli
2021-04-06Fix issue with lemma during equality engine iterator in sets (#6289)Andrew Reynolds
2021-04-05[proof-new] Registering proof checkers uniformly from the SMT solver (#6275)Haniel Barbosa
2021-04-05Fix subtyping for sets care graph (#6278)Andrew Reynolds
2021-04-01Rename namespace CVC5 to cvc5. (#6258)Aina Niemetz
2021-03-31Rename namespace CVC4 to CVC5. (#6249)Aina Niemetz
2021-03-31Add missing inference ids (#6242)Andrew Reynolds
2021-03-16cmake: Generate cvc4_export.h and set visibility to hidden. (#6139)Mathias Preiner
2021-03-11Delete Expr layer. (#6117)Aina Niemetz
2021-03-11(proof-new) Clean up uses of witness with skolem lemmas (#6109)Andrew Reynolds
2021-03-10(proof-new) Update ppRewrite to use skolem lemmas (#6102)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback