summaryrefslogtreecommitdiff
path: root/src/printer/smt2/smt2_printer.cpp
AgeCommit message (Expand)Author
2020-06-05Printing FP values as binary or indexed BVs according to option (#4554)Haniel Barbosa
2020-05-19Renamed operator CHOICE to WITNESS (#4207)mudathirmahgoub
2020-05-19Update enum and option names for sygus languages (#4388)Andrew Reynolds
2020-04-28Support the SMT-LIB Unicode string standard by default (#4378)Andrew Reynolds
2020-04-08Added CHOOSE operator for sets (#4211)mudathirmahgoub
2020-04-06Cleanup deprecated quantifiers attribute features (#4215)Andrew Reynolds
2020-03-27Support unicode internal representation and escape sequences (#3852)Andrew Reynolds
2020-03-18Move node visitor class from smt_util/ to expr/ (#4110)Alex Ozdemir
2020-03-06Simplify DatatypeDeclarationCommand command (#3928)Andrew Reynolds
2020-03-05Enable -Wshadow and fix warnings. (#3909)Mathias Preiner
2020-02-29Convert more uses of string to word (#3834)Andrew Reynolds
2020-02-28Add support for str.from_code (#3829)Andres Noetzli
2020-02-27Fix -Wshadow warnings in common headers (#3826)Andres Noetzli
2020-02-26More fixes for printing sygus commands (#3812)Andrew Reynolds
2020-02-26Basic support for regular expression complement (#3437)Andrew Reynolds
2020-02-24Fix bugs related to printing Sygus commands (#3804)Abdalrhman Mohamed
2020-02-20Remove front-end support for Chain (#3767)Andrew Reynolds
2020-02-17Support dumping Sygus commands. (#3763)Abdalrhman Mohamed
2020-01-10Fix printing of models of uninterpreted sorts (#3597)Andres Noetzli
2019-12-23Initial support for string reverse (#3581)Andrew Reynolds
2019-12-16Move Datatype management to ExprManager (#3568)Andrew Reynolds
2019-12-13Add support for set comprehension (#3312)Andrew Reynolds
2019-12-02[SMT2 Printer] Quote symbols starting with digit (#3517)Andres Noetzli
2019-11-18Use -Wimplicit-fallthrough (#3464)Andres Noetzli
2019-10-30Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)Mathias Preiner
2019-09-27Support smt2 language "match" term (#3258)Andrew Reynolds
2019-09-25Fix printing of instantiation patterns (#3305)Andrew Reynolds
2019-09-24Return choice functions for approximate values in get-value (#3304)Andrew Reynolds
2019-09-11Fix constructor type printing (#3246)Andrew Reynolds
2019-09-06Remove parsing/printing of meta-info command. (#3260)Mathias Preiner
2019-09-05 Model API for domain elements (#3243)Andrew Reynolds
2019-08-03Fix printing issue related to nested quotes (#3154)Andrew Reynolds
2019-08-03Collapse @ chains in SMT2 printer (#3140)Haniel Barbosa
2019-07-19Fixes for sygus with datatypes (#3103)Andrew Reynolds
2019-07-16Add support for str.tolower and str.toupper (#3092)Andrew Reynolds
2019-05-30Quote symbol when printing empty symbol name (#3025)Andres Noetzli
2019-05-15Fix printing of bvurem (#2963)Andrew Reynolds
2019-04-29Eliminate APPLY kind (#2976)Andrew Reynolds
2019-03-26Update copyright headers.Aina Niemetz
2019-01-16Add option to print BV constants in binary (#2805)Andres Noetzli
2018-11-21Support string replace all (#2704)Andrew Reynolds
2018-10-11 Refactor printing of parameterized operators in smt2 (#2609)Andrew Reynolds
2018-09-05Remove printing support for sygus enumeration types (#2430)Andrew Reynolds
2018-08-29fix bv total ops printing (#2365)Haniel Barbosa
2018-08-01Fix issues with printing parametric datatypes in smt2 (#2213)Andrew Reynolds
2018-08-01Fix issues with bv2nat (#2219)Andrew Reynolds
2018-06-28Do not rename uninterpreted constants (#2098)Andrew Reynolds
2018-06-25Minor improvements in SMT2 and CVC printers (#2089)Andres Noetzli
2018-05-21Improvements in parsing and printing related to mixed int/real (#1879)Andrew Reynolds
2018-05-15Floating point theory solver based on SymFPU (#1895)Martin
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback