summaryrefslogtreecommitdiff
path: root/src/parser
AgeCommit message (Expand)Author
2020-11-25Use symbol manager for printing responses get-model (#5516)Andrew Reynolds
2020-11-20Fix use of declaration sequence command in cvc parser (#5479)Andrew Reynolds
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-12Make symbol manager context dependent (#5424)Andrew Reynolds
2020-11-11Move symbol manager to src/expr/ (#5420)Andrew Reynolds
2020-11-10Add proper support for the declare-heap command for separation logic (#5405)Andrew Reynolds
2020-11-09Add symbol manager (#5380)Andrew Reynolds
2020-11-05Simplify printing with respect to expression types (#5394)Andrew Reynolds
2020-11-05Remove mkSingleton from the API (#5366)mudathirmahgoub
2020-11-02Miscellaneous cleaning of parser (#5369)Andrew Reynolds
2020-10-29Update api::Sort to use TypeNode instead of Type (#5363)Andrew Reynolds
2020-10-29Add mkInteger to the API (#5274)mudathirmahgoub
2020-10-28Convert symbol table from Expr-level to Term-level (#5355)Andrew Reynolds
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-16Dump commands in internal code using command printing functions. (#5040)Abdalrhman Mohamed
2020-09-09Parser error for wrong number of datatypes (#5049)Andrew Reynolds
2020-09-09Add is_singleton operator to the theory of sets (#5033)mudathirmahgoub
2020-09-02Drop {INCLUDE,LIBRARY,RUNTIME}_INSTALL_DIR variables in CMakeLists.txt (#4979)FabianWolff
2020-09-01[API] Fix Python Examples (#4943)Andres Noetzli
2020-08-31Fix spelling errors (#4977)FabianWolff
2020-08-25Replace Expr-level datatype with Node-level DType (#4875)Andrew Reynolds
2020-08-24Fix memory issue in AntlrInput::parseError (#4873)Gereon Kremer
2020-08-04Modify the smt2 parser to use the Sygus grammar. (#4829)Abdalrhman Mohamed
2020-08-04Add API interface for specialized constructor term (#4817)Andrew Reynolds
2020-08-03Update datatypes in cvc parser to the new API (#4826)Andrew Reynolds
2020-07-28Supporting seq.nth (#4723)yoni206
2020-07-14Remove sygus print callback (#4727)Andrew Reynolds
2020-07-13Debug instantiations output (#4739)Andrew Reynolds
2020-07-13Statistics on instantiations per quantified formula. (#4719)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
2020-06-30Interpolation step 1 (#4638)Ying Sheng
2020-06-25Remove sygus1 parser (#4651)Andrew Reynolds
2020-06-23Add support for eqrange predicate (#4562)Mathias Preiner
2020-06-18Add logic check for define-fun(s)-rec (#4577)Andres Noetzli
2020-06-16Update copyright headers.Aina Niemetz
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback