projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Cleanup in transcendental solver, add ApproximationBounds struct. (#5945)
[cvc5.git] / src / printer /
2021-02-08 Andrew ReynoldsUse quantifiers inference manager for lemma management... tree | commitdiff
2021-01-24 Andrew Reynolds(proof-new) Instantiation list utility (#5768) tree | commitdiff
2021-01-11 Andrew ReynoldsFurther simplifications in preparation for removing... tree | commitdiff
2021-01-08 mudathirmahgoubAdd bags inference generator (#5731) tree | commitdiff
2021-01-05 Andrew ReynoldsRemove a few miscellaneous references to the expr layer... tree | commitdiff
2020-12-16 Andrew ReynoldsSimplify synth-fun printer (#5682) tree | commitdiff
2020-12-15 Andrew ReynoldsImprovements related to quantifiers printing (#5678) tree | commitdiff
2020-12-08 Abdalrhman MohamedFix a bug with synth-fun printer (#5512) tree | commitdiff
2020-12-03 yoni206Models as (#5581) tree | commitdiff
2020-12-03 Aina NiemetzUpdate copyright headers. tree | commitdiff
2020-12-02 Andrew ReynoldsRemove dagification visitor (#5574) tree | commitdiff
2020-12-02 Andrew ReynoldsUse new let binding for cvc printer (#5561) tree | commitdiff
2020-11-30 Andrew ReynoldsUse new let binding in AST printer (#5529) tree | commitdiff
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
next