summaryrefslogtreecommitdiff
path: root/src/expr
AgeCommit message (Expand)Author
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-24Better formalization of regular expression unfolding skolems (#6602)Andrew Reynolds
2021-05-21Formalize shared selectors as skolem functions (#6591)Andrew Reynolds
2021-05-21(proof-new) Minor documentation sync (#6592)Andrew Reynolds
2021-05-21Add utility to get all types occurring in a term (#6588)Andrew Reynolds
2021-05-21Update to sygus standard output for check-synth responses (#6521)Andrew Reynolds
2021-05-21Support braced-init-lists with `mkNode()` (#6580)Andres Noetzli
2021-05-21BV: Rename BITVECTOR_PLUS to BITVECTOR_ADD. (#6589)Aina Niemetz
2021-05-20Expand arith's farkas lemma rule as a macro (#6577)Alex Ozdemir
2021-05-19Remove unused methods from `NodeManager` (#6578)Andres Noetzli
2021-05-19Improve handling of `:named` attributes (#6549)Andres Noetzli
2021-05-13Add std::hash overloads for Node, TNode and TypeNode. (#6534)Mathias Preiner
2021-05-12Ensure sequences of Booleans generate Boolean term variable skolems when appl...Andrew Reynolds
2021-05-07Add support for datatype update (#6449)Andrew Reynolds
2021-05-06[proof-new] Updating documentation for Subs/Rw ids (#6502)Haniel Barbosa
2021-04-27Add internal support for datatype update (#6450)Andrew Reynolds
2021-04-27Fix refutational soundness bug in quantifier prenexing (#6448)Andrew Reynolds
2021-04-27Simplify making function types (#6447)Andrew Reynolds
2021-04-27Use std::hash for API types (#6432)Gereon Kremer
2021-04-23Add assumption-based unsat cores. (#6427)Mathias Preiner
2021-04-23Add new substitution apply methods fixpoint, sequential, simultaneous (#6429)Andrew Reynolds
2021-04-23BV: Add proof logging for bit-blasting. (#6373)Aina Niemetz
2021-04-21Datatypes: Move implementation of type rules to cpp. (#6418)Aina Niemetz
2021-04-21Goodbye CVC4, hello cvc5! (#6371)Mathias Preiner
2021-04-20Add guards to disable clang-format around placeholders in templates. (#6375)Aina Niemetz
2021-04-16Fix ONCE for post-rewrite (#6372)Andrew Reynolds
2021-04-15Rename occurrences of CVC4 to CVC5. (#6351)Aina Niemetz
2021-04-15Fix printing of stats when aborted. (#6362)Gereon Kremer
2021-04-14Refactor / reimplement statistics (#6162)Gereon Kremer
2021-04-14Rename public and private headers in src/include. (#6352)Aina Niemetz
2021-04-14[proof-new] Fix explanation of literals in SAT proof manager (#6346)Haniel Barbosa
2021-04-13Formalize more skolems (#6307)Andrew Reynolds
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_ macros to CVC5_. (#6327)Aina Niemetz
2021-04-09Rename CVC4__ header guards to CVC5__. (#6326)Aina Niemetz
2021-04-09[proof-new] Optimizing sat proof (#6324)Haniel Barbosa
2021-04-08Use exceptions when constructing malformed datatypes (#6303)Andrew Reynolds
2021-04-08Initial support for parametric datatypes in sygus (#6304)Andrew Reynolds
2021-04-07[proof-new] Fixing SMT post-processor's handling of assumptions (#6277)Haniel Barbosa
2021-04-07(proof-new) Proper implementation of proof node cloning (#6285)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-05New C++ Api: Rename and move headers. (#6292)Aina Niemetz
2021-04-05Add interface for skolem functions in SkolemManager (#6256)Andrew Reynolds
2021-04-01Rename namespace CVC5 to cvc5. (#6258)Aina Niemetz
2021-03-31Rename namespace CVC4 to CVC5. (#6249)Aina Niemetz
2021-03-30Make SEXPR simply typed (#6160)Andrew Reynolds
2021-03-25Add missing includes. (#6207)Gereon Kremer
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback