projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
floatingpoint: Use unique_ptr for FloatingPointLiteral pointer. (#5503)
[cvc5.git] / src / printer /
2020-11-25 Andrew ReynoldsUse symbol manager for printing responses get-model... tree | commitdiff
2020-11-25 Andrew ReynoldsAllow printing of null node in let binder (#5523) tree | commitdiff
2020-11-20 Aina NiemetzRoundingMode: Rename enum values to conform to code... tree | commitdiff
2020-11-19 Andrew ReynoldsUse new let binding utility in smt2 printer (#5472) tree | commitdiff
2020-11-19 Andrew ReynoldsUse symbol manager for unsat cores (#5468) tree | commitdiff
2020-11-18 Andrew ReynoldsAdd let binding utility (#5444) tree | commitdiff
2020-11-18 Andrew ReynoldsUse symbol manager for get assignment (#5451) tree | commitdiff
2020-11-18 Aina NiemetzFloatingPoint: Clean up and document header, format... tree | commitdiff
2020-11-13 yoni206Model declarations printing options (#5432) tree | commitdiff
2020-11-12 yoni206Models standard (#5415) tree | commitdiff
2020-11-10 Andrew ReynoldsAdd proper support for the declare-heap command for... tree | commitdiff
2020-11-09 Andrew ReynoldsSimplify handling of subtypes in smt2 printer (#5401) tree | commitdiff
2020-11-06 Andrew ReynoldsSimplify printing with respect to expression types... tree | commitdiff
2020-11-03 Andres NoetzliAdd support for printing `re.loop` and `re.^` (#5392) tree | commitdiff
2020-10-30 Andrew ReynoldsUpdate api::Sort to use TypeNode instead of Type (... tree | commitdiff
2020-10-29 mudathirmahgoubAdd mkInteger to the API (#5274) tree | commitdiff
2020-10-28 Andrew ReynoldsRemove more uses of Expr (#5357) tree | commitdiff
2020-10-20 Abdalrhman MohamedRemove some Commands from the API. (#5268) tree | commitdiff
2020-10-16 Andrew ReynoldsRefactor SMT-level model object (#5277) tree | commitdiff
2020-10-04 mudathirmahgoubRemove subtyping for sets theory (#5179) tree | commitdiff
2020-09-22 mudathirmahgoubAdd skeleton for theory of bags (multisets) (#5100) tree | commitdiff
2020-09-22 Mathias PreinerUpdate copyright header script to support CMake and... tree | commitdiff
2020-09-16 Abdalrhman MohamedDump commands in internal code using command printing... tree | commitdiff
2020-09-11 Andrew ReynoldsAdd witness to cvc printer. (#5057) tree | commitdiff
2020-09-09 Andrew ReynoldsFixes for regular expressions + sygus (#5044) tree | commitdiff
2020-09-09 mudathirmahgoubAdd is_singleton operator to the theory of sets (#5033) tree | commitdiff
2020-09-04 Abdalrhman MohamedUse Result::Sat instead of BenchmarkStatus in printers... tree | commitdiff
2020-09-02 Abdalrhman MohamedIntroduce an internal version of Commands. (#4988) tree | commitdiff
2020-08-26 Andrew ReynoldsReplace Expr-level datatype with Node-level DType ... tree | commitdiff
2020-08-18 Abdalrhman MohamedRefactor functions that print commands (Part 2) (#4905) tree | commitdiff
2020-08-12 Abdalrhman MohamedRefactor functions that print commands (Part 1) (#4869) tree | commitdiff
2020-08-06 Andrew ReynoldsUpdates not related to creation for eliminating Expr... tree | commitdiff
2020-08-06 Andrew ReynoldsSplit preprocessor from SmtEngine (#4854) tree | commitdiff
2020-08-04 Abdalrhman MohamedModify the smt2 parser to use the Sygus grammar. (... tree | commitdiff
2020-07-28 yoni206Supporting seq.nth (#4723) tree | commitdiff
2020-07-14 Andrew ReynoldsRemove sygus print callback (#4727) tree | commitdiff
2020-07-14 Andres NoetzliUse TypeNode/Node in ArrayStoreAll (#4728) tree | commitdiff
2020-07-13 Andrew ReynoldsAdd support for string/sequence update (#4725) tree | commitdiff
2020-07-13 Andres NoetzliRemove ExprSequence (#4724) tree | commitdiff
2020-07-11 Andrew V. JonesAdd support for printing 'get-abduct' in verbose mode... tree | commitdiff
2020-07-10 Andrew ReynoldsFront end support for integer AND (#4717) tree | commitdiff
2020-07-06 Andrew ReynoldsFront end support for sequences (#4690) tree | commitdiff
2020-06-25 Andrew ReynoldsRemove sygus1 parser (#4651) tree | commitdiff
2020-06-23 Mathias PreinerAdd support for eqrange predicate (#4562) tree | commitdiff
2020-06-19 Andres NoetzliAdd logic check for define-fun(s)-rec (#4577) tree | commitdiff
2020-06-16 Aina NiemetzUpdate copyright headers. tree | commitdiff
2020-06-10 Andres NoetzliAdd support for str.replace_re/str.replace_re_all ... tree | commitdiff
2020-06-05 Haniel BarbosaChanging default language (#4561) tree | commitdiff
2020-06-05 Haniel BarbosaPrinting FP values as binary or indexed BVs according... tree | commitdiff
2020-05-19 mudathirmahgoubRenamed operator CHOICE to WITNESS (#4207) tree | commitdiff
2020-05-19 Andrew ReynoldsUpdate enum and option names for sygus languages (... tree | commitdiff
2020-04-28 Andrew ReynoldsSupport the SMT-LIB Unicode string standard by default... tree | commitdiff
2020-04-08 mudathirmahgoubAdded CHOOSE operator for sets (#4211) tree | commitdiff
2020-04-07 Andrew ReynoldsCleanup deprecated quantifiers attribute features ... tree | commitdiff
2020-03-27 Andrew ReynoldsSupport unicode internal representation and escape... tree | commitdiff
2020-03-18 Alex OzdemirMove node visitor class from smt_util/ to expr/ (#4110) tree | commitdiff
2020-03-08 Ying ShengExplicit end marker for models printed in the CVC langu... tree | commitdiff
2020-03-06 Andrew ReynoldsSimplify DatatypeDeclarationCommand command (#3928) tree | commitdiff
2020-03-05 Mathias PreinerEnable -Wshadow and fix warnings. (#3909) tree | commitdiff
2020-02-29 Andrew ReynoldsConvert more uses of string to word (#3834) tree | commitdiff
2020-02-29 Andres NoetzliAdd support for str.from_code (#3829) tree | commitdiff
2020-02-27 Andres NoetzliFix -Wshadow warnings in common headers (#3826) tree | commitdiff
2020-02-26 Andrew ReynoldsMore fixes for printing sygus commands (#3812) tree | commitdiff
2020-02-26 Andrew ReynoldsBasic support for regular expression complement (#3437) tree | commitdiff
2020-02-24 Abdalrhman MohamedFix bugs related to printing Sygus commands (#3804) tree | commitdiff
2020-02-20 Andrew ReynoldsRemove front-end support for Chain (#3767) tree | commitdiff
2020-02-17 Abdalrhman MohamedSupport dumping Sygus commands. (#3763) tree | commitdiff
2020-02-13 Andrew ReynoldsConst input for sygus print callback (#3755) tree | commitdiff
2020-01-10 Andres NoetzliFix printing of models of uninterpreted sorts (#3597) tree | commitdiff
2019-12-23 Andrew ReynoldsInitial support for string reverse (#3581) tree | commitdiff
2019-12-16 Andrew ReynoldsMove Datatype management to ExprManager (#3568) tree | commitdiff
2019-12-13 Andrew ReynoldsEliminate Expr-level calls in TypeNode (#3562) tree | commitdiff
2019-12-13 Andrew ReynoldsAdd support for set comprehension (#3312) tree | commitdiff
2019-12-02 Andres Noetzli[SMT2 Printer] Quote symbols starting with digit (... tree | commitdiff
2019-11-18 Andres NoetzliUse -Wimplicit-fallthrough (#3464) tree | commitdiff
2019-11-13 Andrew ReynoldsDistinguish unknown status for model printing (#3454) tree | commitdiff
2019-10-30 Mathias PreinerUnify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. ... tree | commitdiff
2019-09-28 Andrew ReynoldsSupport smt2 language "match" term (#3258) tree | commitdiff
2019-09-27 Andrew ReynoldsCVC print support for recoverable failure (#3323) tree | commitdiff
2019-09-25 Andrew ReynoldsFix printing of instantiation patterns (#3305) tree | commitdiff
2019-09-25 Andrew ReynoldsReturn choice functions for approximate values in get... tree | commitdiff
2019-09-13 Andrew ReynoldsDisallow let in sygus grammars, check for free variable... tree | commitdiff
2019-09-11 Andrew ReynoldsFix constructor type printing (#3246) tree | commitdiff
2019-09-06 Mathias PreinerRemove parsing/printing of meta-info command. (#3260) tree | commitdiff
2019-09-06 Andrew Reynolds Model API for domain elements (#3243) tree | commitdiff
2019-09-04 Mathias PreinerFix DAGification for printer. (#3233) tree | commitdiff
2019-08-03 Andrew ReynoldsFix printing issue related to nested quotes (#3154) tree | commitdiff
2019-08-03 Haniel BarbosaCollapse @ chains in SMT2 printer (#3140) tree | commitdiff
2019-07-19 Andrew ReynoldsFixes for sygus with datatypes (#3103) tree | commitdiff
2019-07-16 Andrew ReynoldsAdd support for str.tolower and str.toupper (#3092) tree | commitdiff
2019-07-01 Andrew ReynoldsSupport sygus version 2 format (#3066) tree | commitdiff
2019-06-05 Andres NoetzliPrevent letification from shadowing variables (#3042) tree | commitdiff
2019-05-30 Andres NoetzliQuote symbol when printing empty symbol name (#3025) tree | commitdiff
2019-05-15 Andrew ReynoldsFix printing of bvurem (#2963) tree | commitdiff
2019-04-30 Andrew ReynoldsEliminate APPLY kind (#2976) tree | commitdiff
2019-04-24 Mathias PreinerDo not use __ prefix for header guards. (#2974) tree | commitdiff
2019-04-17 Andrew ReynoldsMore use of isClosure (#2959) tree | commitdiff
2019-03-26 Aina NiemetzUpdate copyright headers. tree | commitdiff
2019-01-22 Andrew Reynolds Fix tuple and record CVC printing (#2818) tree | commitdiff
2019-01-17 Andres NoetzliAdd option to print BV constants in binary (#2805) tree | commitdiff
next