summaryrefslogtreecommitdiff
path: root/src/parser/smt2/smt2.cpp
AgeCommit message (Expand)Author
2021-11-13Add operator set.map to theory of sets (#7641)mudathirmahgoub
2021-11-12bags: Rename kinds with a more consistent naming scheme (#7611)mudathirmahgoub
2021-11-10api: Add Solver::mkRegexpAll(). (#7614)Aina Niemetz
2021-11-10Fix parsing array constants (#7617)Andrew Reynolds
2021-11-10sets: Rename set.intersection to set.inter. (#7622)Aina Niemetz
2021-11-09regex: Rename REGEXP_EMPTY and REGEXP_SIGMA to match SMT-LIB. (#7609)Aina Niemetz
2021-11-08sets: Rename kinds with a more consistent naming scheme. (#7595)Aina Niemetz
2021-11-02Improve syntax for fmf cardinality constraints (#7556)Andrew Reynolds
2021-10-21Make cardinality constraint a nullary operator (#7333)Andrew Reynolds
2021-10-20api: Add Solver::mkSepEmp(). (#7432)Aina Niemetz
2021-10-18Move check for experimental arrays features to `theory_arrays.cpp`. (#7391)Abdalrhman Mohamed
2021-10-14Improve parser for tuple select (#7364)Andrew Reynolds
2021-09-30Rename SmtEngine to SolverEngine. (#7282)Aina Niemetz
2021-09-30Simplify the syntax and representation of the separation logic empty heap con...Andrew Reynolds
2021-09-22Remove CVC language support (#7219)Mathias Preiner
2021-09-22Minimal fixing version for tuple update parsing (#7228)Andrew Reynolds
2021-09-01No longer use direct access to options in driver (#7094)Gereon Kremer
2021-08-30Add kind BAG_MAP and its type rule to bags (#6503)mudathirmahgoub
2021-08-27Handle languages as strings in driver (#7074)Gereon Kremer
2021-08-26Consolidate language types (#7065)Gereon Kremer
2021-07-07Rename operator pow2 to int.pow2. (#6849)Aina Niemetz
2021-06-25pow2 -- final changes (#6800)yoni206
2021-06-23[parser] [hol] Fix parser check for allowing functions when HOL is enabled (#...Haniel Barbosa
2021-06-15Remove public option wrappers (#6716)Gereon Kremer
2021-06-11Better support for HOL parsing and set up (#6697)Haniel Barbosa
2021-06-03Simplify automatic set-logic in smt2 parser (#6678)Andrew Reynolds
2021-06-02Move public wrapper functions out of options class (#6600)Gereon Kremer
2021-05-27Fix `str.replace_re` and `str.replace_re_all` (#6615)Andres Noetzli
2021-05-27FP: Rename FLOATINGPOINT_PLUS to FLOATINGPOINT_ADD. (#6628)Aina Niemetz
2021-05-21BV: Rename BITVECTOR_PLUS to BITVECTOR_ADD. (#6589)Aina Niemetz
2021-05-20Add more getters for api::Term (#6496)Gereon Kremer
2021-05-19Improve handling of `:named` attributes (#6549)Andres Noetzli
2021-05-14Decouple parser creation from input selection (#6533)Andres Noetzli
2021-05-07Add support for datatype update (#6449)Andrew Reynolds
2021-04-19Remove linking against gmp and cln in tests and parser (#6376)Gereon Kremer
2021-04-15Rename occurrences of CVC4 to CVC5. (#6351)Aina Niemetz
2021-04-12Refactor and update copyright headers. (#6316)Aina Niemetz
2021-04-09Rename CVC4_ macros to CVC5_. (#6327)Aina Niemetz
2021-04-01Rename namespace CVC5 to cvc5. (#6258)Aina Niemetz
2021-03-31Rename namespace CVC4 to CVC5. (#6249)Aina Niemetz
2021-03-10Use Assert instead of assert. (#6095)Mathias Preiner
2021-03-09Update copyright headers to 2021. (#6081)Aina Niemetz
2021-03-06Remove SMT-LIB 2.5 and 2.0 support. (#6068)Mathias Preiner
2021-03-03Add tuple projection operator (#5904)mudathirmahgoub
2021-02-08Remove support for inst closure (#5874)Andrew Reynolds
2021-01-21Add div, mod, abs in non-strict parsing mode (#5793)Andrew Reynolds
2021-01-20SMT2 parser: Do not add non-linear symbols for linear Int arith logics. (#5787)Aina Niemetz
2021-01-08Add bags inference generator (#5731)mudathirmahgoub
2020-12-16Use uint64 utility when parsing tuple selectors in smt2 (#5681)Andrew Reynolds
2020-12-03Refactor handling of global declarations (#5577)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback