projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
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 Reynolds
Use symbol manager for printing responses get-model...
tree
|
commitdiff
2020-11-25
Andrew Reynolds
Allow printing of null node in let binder (#5523)
tree
|
commitdiff
2020-11-20
Aina Niemetz
RoundingMode: Rename enum values to conform to code...
tree
|
commitdiff
2020-11-19
Andrew Reynolds
Use new let binding utility in smt2 printer (#5472)
tree
|
commitdiff
2020-11-19
Andrew Reynolds
Use symbol manager for unsat cores (#5468)
tree
|
commitdiff
2020-11-18
Andrew Reynolds
Add let binding utility (#5444)
tree
|
commitdiff
2020-11-18
Andrew Reynolds
Use symbol manager for get assignment (#5451)
tree
|
commitdiff
2020-11-18
Aina Niemetz
FloatingPoint: Clean up and document header, format...
tree
|
commitdiff
2020-11-13
yoni206
Model declarations printing options (#5432)
tree
|
commitdiff
2020-11-12
yoni206
Models standard (#5415)
tree
|
commitdiff
2020-11-10
Andrew Reynolds
Add proper support for the declare-heap command for...
tree
|
commitdiff
2020-11-09
Andrew Reynolds
Simplify handling of subtypes in smt2 printer (#5401)
tree
|
commitdiff
2020-11-06
Andrew Reynolds
Simplify printing with respect to expression types...
tree
|
commitdiff
2020-11-03
Andres Noetzli
Add support for printing `re.loop` and `re.^` (#5392)
tree
|
commitdiff
2020-10-30
Andrew Reynolds
Update api::Sort to use TypeNode instead of Type (...
tree
|
commitdiff
2020-10-29
mudathirmahgoub
Add mkInteger to the API (#5274)
tree
|
commitdiff
2020-10-28
Andrew Reynolds
Remove more uses of Expr (#5357)
tree
|
commitdiff
2020-10-20
Abdalrhman Mohamed
Remove some Commands from the API. (#5268)
tree
|
commitdiff
2020-10-16
Andrew Reynolds
Refactor SMT-level model object (#5277)
tree
|
commitdiff
2020-10-04
mudathirmahgoub
Remove subtyping for sets theory (#5179)
tree
|
commitdiff
2020-09-22
mudathirmahgoub
Add skeleton for theory of bags (multisets) (#5100)
tree
|
commitdiff
2020-09-22
Mathias Preiner
Update copyright header script to support CMake and...
tree
|
commitdiff
2020-09-16
Abdalrhman Mohamed
Dump commands in internal code using command printing...
tree
|
commitdiff
2020-09-11
Andrew Reynolds
Add witness to cvc printer. (#5057)
tree
|
commitdiff
2020-09-09
Andrew Reynolds
Fixes for regular expressions + sygus (#5044)
tree
|
commitdiff
2020-09-09
mudathirmahgoub
Add is_singleton operator to the theory of sets (#5033)
tree
|
commitdiff
2020-09-04
Abdalrhman Mohamed
Use Result::Sat instead of BenchmarkStatus in printers...
tree
|
commitdiff
2020-09-02
Abdalrhman Mohamed
Introduce an internal version of Commands. (#4988)
tree
|
commitdiff
2020-08-26
Andrew Reynolds
Replace Expr-level datatype with Node-level DType ...
tree
|
commitdiff
2020-08-18
Abdalrhman Mohamed
Refactor functions that print commands (Part 2) (#4905)
tree
|
commitdiff
2020-08-12
Abdalrhman Mohamed
Refactor functions that print commands (Part 1) (#4869)
tree
|
commitdiff
2020-08-06
Andrew Reynolds
Updates not related to creation for eliminating Expr...
tree
|
commitdiff
2020-08-06
Andrew Reynolds
Split preprocessor from SmtEngine (#4854)
tree
|
commitdiff
2020-08-04
Abdalrhman Mohamed
Modify the smt2 parser to use the Sygus grammar. (...
tree
|
commitdiff
2020-07-28
yoni206
Supporting seq.nth (#4723)
tree
|
commitdiff
2020-07-14
Andrew Reynolds
Remove sygus print callback (#4727)
tree
|
commitdiff
2020-07-14
Andres Noetzli
Use TypeNode/Node in ArrayStoreAll (#4728)
tree
|
commitdiff
2020-07-13
Andrew Reynolds
Add support for string/sequence update (#4725)
tree
|
commitdiff
2020-07-13
Andres Noetzli
Remove ExprSequence (#4724)
tree
|
commitdiff
2020-07-11
Andrew V. Jones
Add support for printing 'get-abduct' in verbose mode...
tree
|
commitdiff
2020-07-10
Andrew Reynolds
Front end support for integer AND (#4717)
tree
|
commitdiff
2020-07-06
Andrew Reynolds
Front end support for sequences (#4690)
tree
|
commitdiff
2020-06-25
Andrew Reynolds
Remove sygus1 parser (#4651)
tree
|
commitdiff
2020-06-23
Mathias Preiner
Add support for eqrange predicate (#4562)
tree
|
commitdiff
2020-06-19
Andres Noetzli
Add logic check for define-fun(s)-rec (#4577)
tree
|
commitdiff
2020-06-16
Aina Niemetz
Update copyright headers.
tree
|
commitdiff
2020-06-10
Andres Noetzli
Add support for str.replace_re/str.replace_re_all ...
tree
|
commitdiff
2020-06-05
Haniel Barbosa
Changing default language (#4561)
tree
|
commitdiff
2020-06-05
Haniel Barbosa
Printing FP values as binary or indexed BVs according...
tree
|
commitdiff
2020-05-19
mudathirmahgoub
Renamed operator CHOICE to WITNESS (#4207)
tree
|
commitdiff
2020-05-19
Andrew Reynolds
Update enum and option names for sygus languages (...
tree
|
commitdiff
2020-04-28
Andrew Reynolds
Support the SMT-LIB Unicode string standard by default...
tree
|
commitdiff
2020-04-08
mudathirmahgoub
Added CHOOSE operator for sets (#4211)
tree
|
commitdiff
2020-04-07
Andrew Reynolds
Cleanup deprecated quantifiers attribute features ...
tree
|
commitdiff
2020-03-27
Andrew Reynolds
Support unicode internal representation and escape...
tree
|
commitdiff
2020-03-18
Alex Ozdemir
Move node visitor class from smt_util/ to expr/ (#4110)
tree
|
commitdiff
2020-03-08
Ying Sheng
Explicit end marker for models printed in the CVC langu...
tree
|
commitdiff
2020-03-06
Andrew Reynolds
Simplify DatatypeDeclarationCommand command (#3928)
tree
|
commitdiff
2020-03-05
Mathias Preiner
Enable -Wshadow and fix warnings. (#3909)
tree
|
commitdiff
2020-02-29
Andrew Reynolds
Convert more uses of string to word (#3834)
tree
|
commitdiff
2020-02-29
Andres Noetzli
Add support for str.from_code (#3829)
tree
|
commitdiff
2020-02-27
Andres Noetzli
Fix -Wshadow warnings in common headers (#3826)
tree
|
commitdiff
2020-02-26
Andrew Reynolds
More fixes for printing sygus commands (#3812)
tree
|
commitdiff
2020-02-26
Andrew Reynolds
Basic support for regular expression complement (#3437)
tree
|
commitdiff
2020-02-24
Abdalrhman Mohamed
Fix bugs related to printing Sygus commands (#3804)
tree
|
commitdiff
2020-02-20
Andrew Reynolds
Remove front-end support for Chain (#3767)
tree
|
commitdiff
2020-02-17
Abdalrhman Mohamed
Support dumping Sygus commands. (#3763)
tree
|
commitdiff
2020-02-13
Andrew Reynolds
Const input for sygus print callback (#3755)
tree
|
commitdiff
2020-01-10
Andres Noetzli
Fix printing of models of uninterpreted sorts (#3597)
tree
|
commitdiff
2019-12-23
Andrew Reynolds
Initial support for string reverse (#3581)
tree
|
commitdiff
2019-12-16
Andrew Reynolds
Move Datatype management to ExprManager (#3568)
tree
|
commitdiff
2019-12-13
Andrew Reynolds
Eliminate Expr-level calls in TypeNode (#3562)
tree
|
commitdiff
2019-12-13
Andrew Reynolds
Add 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 Noetzli
Use -Wimplicit-fallthrough (#3464)
tree
|
commitdiff
2019-11-13
Andrew Reynolds
Distinguish unknown status for model printing (#3454)
tree
|
commitdiff
2019-10-30
Mathias Preiner
Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. ...
tree
|
commitdiff
2019-09-28
Andrew Reynolds
Support smt2 language "match" term (#3258)
tree
|
commitdiff
2019-09-27
Andrew Reynolds
CVC print support for recoverable failure (#3323)
tree
|
commitdiff
2019-09-25
Andrew Reynolds
Fix printing of instantiation patterns (#3305)
tree
|
commitdiff
2019-09-25
Andrew Reynolds
Return choice functions for approximate values in get...
tree
|
commitdiff
2019-09-13
Andrew Reynolds
Disallow let in sygus grammars, check for free variable...
tree
|
commitdiff
2019-09-11
Andrew Reynolds
Fix constructor type printing (#3246)
tree
|
commitdiff
2019-09-06
Mathias Preiner
Remove 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 Preiner
Fix DAGification for printer. (#3233)
tree
|
commitdiff
2019-08-03
Andrew Reynolds
Fix printing issue related to nested quotes (#3154)
tree
|
commitdiff
2019-08-03
Haniel Barbosa
Collapse @ chains in SMT2 printer (#3140)
tree
|
commitdiff
2019-07-19
Andrew Reynolds
Fixes for sygus with datatypes (#3103)
tree
|
commitdiff
2019-07-16
Andrew Reynolds
Add support for str.tolower and str.toupper (#3092)
tree
|
commitdiff
2019-07-01
Andrew Reynolds
Support sygus version 2 format (#3066)
tree
|
commitdiff
2019-06-05
Andres Noetzli
Prevent letification from shadowing variables (#3042)
tree
|
commitdiff
2019-05-30
Andres Noetzli
Quote symbol when printing empty symbol name (#3025)
tree
|
commitdiff
2019-05-15
Andrew Reynolds
Fix printing of bvurem (#2963)
tree
|
commitdiff
2019-04-30
Andrew Reynolds
Eliminate APPLY kind (#2976)
tree
|
commitdiff
2019-04-24
Mathias Preiner
Do not use __ prefix for header guards. (#2974)
tree
|
commitdiff
2019-04-17
Andrew Reynolds
More use of isClosure (#2959)
tree
|
commitdiff
2019-03-26
Aina Niemetz
Update copyright headers.
tree
|
commitdiff
2019-01-22
Andrew Reynolds
Fix tuple and record CVC printing (#2818)
tree
|
commitdiff
2019-01-17
Andres Noetzli
Add option to print BV constants in binary (#2805)
tree
|
commitdiff
next