projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Eliminating static calls to rewriter in quantifiers (#7301)
[cvc5.git]
/
src
/
printer
/
2021-10-01
Aina Niemetz
Rename SmtEngine to SolverEngine. (#7282)
tree
|
commitdiff
2021-09-30
Aina Niemetz
Rename files smt_engine.(cpp|h) to solver_engine.(cpp...
tree
|
commitdiff
2021-09-30
Abdalrhman Mohamed
Print `str.is_digit` and `int.pow2` correctly. (#7276)
tree
|
commitdiff
2021-09-30
Andres Noetzli
[Printer] Only quote `set-info` value if necessary...
tree
|
commitdiff
2021-09-29
Abdalrhman Mohamed
Remove support for extended `(check-sat <term>)` comman...
tree
|
commitdiff
2021-09-29
Andrew Reynolds
Update the syntax for tuples in smt2 (#7265)
tree
|
commitdiff
2021-09-23
Abdalrhman Mohamed
Use `|` to print quoted strings in `set-info` command...
tree
|
commitdiff
2021-09-22
Mathias Preiner
Remove CVC language support (#7219)
tree
|
commitdiff
2021-09-22
Andrew Reynolds
Minimal fixing version for tuple update parsing (#7228)
tree
|
commitdiff
2021-09-18
Andrew Reynolds
Fix printer for datatype udpater (#7208)
tree
|
commitdiff
2021-09-14
Andrew Reynolds
Add get-difficulty to the API (#7194)
tree
|
commitdiff
2021-09-14
Andrew Reynolds
Support sygus version 2.1 command assume (#7081)
tree
|
commitdiff
2021-09-14
Andrew Reynolds
Utilities in preparation for print benchmark utility...
tree
|
commitdiff
2021-09-01
Andrew Reynolds
Print response to get-model using the API (#7084)
tree
|
commitdiff
2021-08-30
mudathirmahgoub
Add kind BAG_MAP and its type rule to bags (#6503)
tree
|
commitdiff
2021-08-27
Andrew Reynolds
Add missing methods to Solver API for models (#7052)
tree
|
commitdiff
2021-08-26
Gereon Kremer
Consolidate language types (#7065)
tree
|
commitdiff
2021-08-24
Andrew Reynolds
Miscellaneous changes from proof-new (#7042)
tree
|
commitdiff
2021-08-22
Andrew Reynolds
Simplify model printing modes (#7049)
tree
|
commitdiff
2021-08-04
Andrew Reynolds
Add optional debug information for dumping instantiatio...
tree
|
commitdiff
2021-08-04
Gereon Kremer
Refactor managed streams (#6934)
tree
|
commitdiff
2021-07-30
Andrew Reynolds
Simplify smt2 printer (#6954)
tree
|
commitdiff
2021-07-27
Andrew Reynolds
Miscellaneous fixes from proof-new (#6914)
tree
|
commitdiff
2021-07-14
Andrew Reynolds
Fix models for sequences of infinite element type ...
tree
|
commitdiff
2021-07-02
Andrew Reynolds
Fix rewriter for negative constant seq.nth (#6827)
tree
|
commitdiff
2021-06-28
Andrew Reynolds
Rename internal string kinds to match API (#6797)
tree
|
commitdiff
2021-06-26
yoni206
pow2 -- final changes (#6800)
tree
|
commitdiff
2021-06-09
Andrew Reynolds
Fixes related to printing tuples, define-fun commands...
tree
|
commitdiff
2021-06-07
Gereon Kremer
Remove `Options::wasSetByUser()` (#6682)
tree
|
commitdiff
2021-06-02
Andrew Reynolds
Fixes for printing define-fun-rec (#6673)
tree
|
commitdiff
2021-05-27
Andres Noetzli
Fix `str.replace_re` and `str.replace_re_all` (#6615)
tree
|
commitdiff
2021-05-27
Aina Niemetz
FP: Rename FLOATINGPOINT_PLUS to FLOATINGPOINT_ADD...
tree
|
commitdiff
2021-05-26
Andres Noetzli
More precise includes of `Node` constants (#6617)
tree
|
commitdiff
2021-05-21
Andrew Reynolds
Update to sygus standard output for check-synth respons...
tree
|
commitdiff
2021-05-21
Aina Niemetz
BV: Rename BITVECTOR_PLUS to BITVECTOR_ADD. (#6589)
tree
|
commitdiff
2021-05-18
Andrew Reynolds
Fix smt2 printing (#6558)
tree
|
commitdiff
2021-05-13
Mathias Preiner
Add std::hash overloads for Node, TNode and TypeNode...
tree
|
commitdiff
2021-05-08
Andrew Reynolds
Add support for datatype update (#6449)
tree
|
commitdiff
2021-05-07
Haniel Barbosa
Properly printing INST_PATTERN_LIST by itself (#6507)
tree
|
commitdiff
2021-04-27
Andrew Reynolds
Add internal support for datatype update (#6450)
tree
|
commitdiff
2021-04-26
Gereon Kremer
First part of options refactoring (#6428)
tree
|
commitdiff
2021-04-20
Andrew Reynolds
Add instantiation pool feature to the API (#6358)
tree
|
commitdiff
2021-04-20
Aina Niemetz
Remove support for CVC3 language. (#6369)
tree
|
commitdiff
2021-04-15
Aina Niemetz
Rename occurrences of CVC4 to CVC5. (#6351)
tree
|
commitdiff
2021-04-14
Aina Niemetz
Rename public and private headers in src/include. ...
tree
|
commitdiff
2021-04-12
Aina Niemetz
Refactor and update copyright headers. (#6316)
tree
|
commitdiff
2021-04-10
Aina Niemetz
Rename CVC4_ macros to CVC5_. (#6327)
tree
|
commitdiff
2021-04-09
Aina Niemetz
Rename CVC4__ header guards to CVC5__. (#6326)
tree
|
commitdiff
2021-04-06
Aina Niemetz
New C++ Api: Rename and move headers. (#6292)
tree
|
commitdiff
2021-04-01
Aina Niemetz
Rename namespace CVC5 to cvc5. (#6258)
tree
|
commitdiff
2021-03-31
Aina Niemetz
Rename namespace CVC4 to CVC5. (#6249)
tree
|
commitdiff
2021-03-30
Andrew Reynolds
Fix printing for double patterns (#6235)
tree
|
commitdiff
2021-03-30
Andrew Reynolds
Make SEXPR simply typed (#6160)
tree
|
commitdiff
2021-03-25
Aina Niemetz
FP: Refactor FloatingPointLiteral in preparation for...
tree
|
commitdiff
2021-03-18
Abdalrhman Mohamed
Eliminate more uses of SExpr. (#6149)
tree
|
commitdiff
2021-03-15
Andrew Reynolds
Letify quantifier bodies independently (#6112)
tree
|
commitdiff
2021-03-11
Aina Niemetz
Delete Expr layer. (#6117)
tree
|
commitdiff
2021-03-09
Gereon Kremer
Some more cleanup of includes (#6083)
tree
|
commitdiff
2021-03-09
Aina Niemetz
Update copyright headers to 2021. (#6081)
tree
|
commitdiff
2021-03-06
Mathias Preiner
Remove partial UDIV/UREM operators. (#6069)
tree
|
commitdiff
2021-03-06
Mathias Preiner
Remove SMT-LIB 2.5 and 2.0 support. (#6068)
tree
|
commitdiff
2021-03-03
Gereon Kremer
More cleanup of includes to reduce compilation times...
tree
|
commitdiff
2021-03-03
Abdalrhman Mohamed
Remove uses of SExpr class. (#6035)
tree
|
commitdiff
2021-03-03
mudathirmahgoub
Add tuple projection operator (#5904)
tree
|
commitdiff
2021-03-02
Gereon Kremer
Clean up includes to reduce compile times (#6031)
tree
|
commitdiff
2021-02-26
Andrew Reynolds
Minor improvement and fix to smt2 printer (#6009)
tree
|
commitdiff
2021-02-22
Gereon Kremer
(proof-new) Add new arithmetic kind INDEXED_ROOT_PREDIC...
tree
|
commitdiff
2021-02-08
Andrew Reynolds
Use 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 Reynolds
Further simplifications in preparation for removing...
tree
|
commitdiff
2021-01-08
mudathirmahgoub
Add bags inference generator (#5731)
tree
|
commitdiff
2021-01-05
Andrew Reynolds
Remove a few miscellaneous references to the expr layer...
tree
|
commitdiff
2020-12-16
Andrew Reynolds
Simplify synth-fun printer (#5682)
tree
|
commitdiff
2020-12-15
Andrew Reynolds
Improvements related to quantifiers printing (#5678)
tree
|
commitdiff
2020-12-08
Abdalrhman Mohamed
Fix a bug with synth-fun printer (#5512)
tree
|
commitdiff
2020-12-03
yoni206
Models as (#5581)
tree
|
commitdiff
2020-12-03
Aina Niemetz
Update copyright headers.
tree
|
commitdiff
2020-12-02
Andrew Reynolds
Remove dagification visitor (#5574)
tree
|
commitdiff
2020-12-02
Andrew Reynolds
Use new let binding for cvc printer (#5561)
tree
|
commitdiff
2020-11-30
Andrew Reynolds
Use new let binding in AST printer (#5529)
tree
|
commitdiff
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
next