summaryrefslogtreecommitdiff
path: root/src/parser/smt2/Smt2.g
AgeCommit message (Expand)Author
2021-05-20Add more getters for api::Term (#6496)Gereon Kremer
2021-05-19Improve handling of `:named` attributes (#6549)Andres Noetzli
2021-05-07Add support for datatype update (#6449)Andrew Reynolds
2021-04-20Add instantiation pool feature to the API (#6358)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-08Initial support for parametric datatypes in sygus (#6304)Andrew Reynolds
2021-04-05New C++ Api: Rename and move headers. (#6292)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
2020-12-03Refactor handling of global declarations (#5577)Andrew Reynolds
2020-11-30Eliminate uses of SExpr from the parser. (#5496)Abdalrhman Mohamed
2020-11-19Include stddef.h (needed for size_t) in cvc4_public.h (#5476)Aina Niemetz
2020-11-19Use symbol manager for unsat cores (#5468)Andrew Reynolds
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-13Add more features to symbol manager (#5434)Andrew Reynolds
2020-11-10Add proper support for the declare-heap command for separation logic (#5405)Andrew Reynolds
2020-11-02Miscellaneous cleaning of parser (#5369)Andrew Reynolds
2020-10-29Add mkInteger to the API (#5274)mudathirmahgoub
2020-10-27Refactor DeclareSygusVarCommand and SynthFunCommand to use the API. (#5334)Abdalrhman Mohamed
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-09Parser error for wrong number of datatypes (#5049)Andrew Reynolds
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-13Debug instantiations output (#4739)Andrew Reynolds
2020-07-13Statistics on instantiations per quantified formula. (#4719)Andrew Reynolds
2020-07-06Front end support for sequences (#4690)Andrew Reynolds
2020-06-30Interpolation step 1 (#4638)Ying Sheng
2020-06-25Remove sygus1 parser (#4651)Andrew Reynolds
2020-06-18Add logic check for define-fun(s)-rec (#4577)Andres Noetzli
2020-06-16Update copyright headers.Aina Niemetz
2020-06-06Keep definitions when global-declarations enabled (#4572)Andres Noetzli
2020-06-05Smt2 parsing support for nested recursive datatypes (#4575)Andrew Reynolds
2020-06-04Add a method for retrieving base of a constant array through API (#4494)makaimann
2020-06-03New C++ Api: First batch of API guards. (#4557)Aina Niemetz
2020-06-03Do not apply unconstrained simplification when quantifiers are present (#4532)Andrew Reynolds
2020-06-02New C++ API: Keep reference to solver object in non-solver objects. (#4549)Aina Niemetz
2020-06-01Do not parse ->/lambda unless --uf-ho enabled (#4544)Andres Noetzli
2020-05-19Renamed operator CHOICE to WITNESS (#4207)mudathirmahgoub
2020-04-03New C++ API: Remove Op::getSort(). (#4208)Aina Niemetz
2020-03-31Support char smt-lib syntax (#4188)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback