summaryrefslogtreecommitdiff
path: root/src/parser/smt2/smt2.cpp
AgeCommit message (Expand)Author
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
2020-11-30Eliminate uses of SExpr from the parser. (#5496)Abdalrhman Mohamed
2020-11-18Use symbol manager for get assignment (#5451)Andrew Reynolds
2020-11-16Cleaning up scopes in preparation for symbol manager (#5442)Andrew Reynolds
2020-11-09Add symbol manager (#5380)Andrew Reynolds
2020-11-05Remove mkSingleton from the API (#5366)mudathirmahgoub
2020-10-29Add mkInteger to the API (#5274)mudathirmahgoub
2020-10-27Refactor DeclareSygusVarCommand and SynthFunCommand to use the API. (#5334)Abdalrhman Mohamed
2020-10-26Add DUPICATE_REMOVAL operator to bags (#5336)mudathirmahgoub
2020-10-08reset-assertions: Remove all non-global symbols in the parser (#5229)Andres Noetzli
2020-10-07New C++ API: Rename Term::isConst() to Term::isValue(). (#5211)Aina Niemetz
2020-10-06Add operators bag.from_set, bag.to_set to the theory of bags (#5186)mudathirmahgoub
2020-10-04Remove subtyping for sets theory (#5179)mudathirmahgoub
2020-09-22Refactor Commands to use the Public API. (#5105)Abdalrhman Mohamed
2020-09-22Add skeleton for theory of bags (multisets) (#5100)mudathirmahgoub
2020-09-22Update copyright header script to support CMake and Python files (#5067)Mathias Preiner
2020-09-09Add is_singleton operator to the theory of sets (#5033)mudathirmahgoub
2020-09-01[API] Fix Python Examples (#4943)Andres Noetzli
2020-08-25Replace Expr-level datatype with Node-level DType (#4875)Andrew Reynolds
2020-08-04Modify the smt2 parser to use the Sygus grammar. (#4829)Abdalrhman Mohamed
2020-07-28Supporting seq.nth (#4723)yoni206
2020-07-14Remove sygus print callback (#4727)Andrew Reynolds
2020-07-12Add support for string/sequence update (#4725)Andrew Reynolds
2020-07-10Front end support for integer AND (#4717)Andrew Reynolds
2020-07-07Transfer ownership of internal Options from NodeManager to SmtEngine (#4682)Andrew Reynolds
2020-07-06Front end support for sequences (#4690)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback