projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
[Rewrite Synthesis] Fix args for non-chaining ops (#7996)
[cvc5.git]
/
src
/
printer
/
2022-01-24
Abdalrhman Mohamed
Enable dump tester. (#7884)
tree
|
commitdiff
2022-01-15
Gereon Kremer
Change how RANs are printed (#7955)
tree
|
commitdiff
2022-01-13
Andres Noetzli
Unify abstract values and uninterpreted constants ...
tree
|
commitdiff
2022-01-04
mudathirmahgoub
Add bag.member operator to theory of bags (#7857)
tree
|
commitdiff
2021-12-22
Andrew Reynolds
Add support for incremental + interpolants (#7853)
tree
|
commitdiff
2021-12-21
Andrew Reynolds
Support get-abduct-next (#7850)
tree
|
commitdiff
2021-12-20
Andrew Reynolds
Allow SyGuS subsolver to be reused in incremental mode...
tree
|
commitdiff
2021-12-02
mudathirmahgoub
add bag.fold operator (#7718)
tree
|
commitdiff
2021-11-23
Gereon Kremer
Push output language inside the printing code (#7683)
tree
|
commitdiff
2021-11-17
Andrew Reynolds
Preparations for eliminating arithmetic subtyping ...
tree
|
commitdiff
2021-11-16
Andres Noetzli
Refactor `metakind` (#7639)
tree
|
commitdiff
2021-11-13
mudathirmahgoub
Add operator set.map to theory of sets (#7641)
tree
|
commitdiff
2021-11-12
mudathirmahgoub
bags: Rename kinds with a more consistent naming scheme...
tree
|
commitdiff
2021-11-11
Abdalrhman Mohamed
Add an API method to get the raw name of a term. (...
tree
|
commitdiff
2021-11-10
Aina Niemetz
sets: Rename set.intersection to set.inter. (#7622)
tree
|
commitdiff
2021-11-09
Aina Niemetz
regex: Rename REGEXP_EMPTY and REGEXP_SIGMA to match...
tree
|
commitdiff
2021-11-08
Aina Niemetz
sets: Rename kinds with a more consistent naming scheme...
tree
|
commitdiff
2021-11-04
Andrew Reynolds
Add -o sygus-grammar to print auto-generated SyGuS...
tree
|
commitdiff
2021-11-04
Andrew Reynolds
Replace the old dump infrastructure (#7572)
tree
|
commitdiff
2021-11-02
Abdalrhman Mohamed
Move `fmf.card` printing code. (#7559)
tree
|
commitdiff
2021-11-02
Abdalrhman Mohamed
Add printing methods for some commands. (#7557)
tree
|
commitdiff
2021-10-28
Abdalrhman Mohamed
Fix `(set-info <sexpr>)` parsing and printing bugs...
tree
|
commitdiff
2021-10-21
Andrew Reynolds
Make cardinality constraint a nullary operator (#7333)
tree
|
commitdiff
2021-10-20
Abdalrhman Mohamed
Avoid escaping `double-quotes` twice. (#7409)
tree
|
commitdiff
2021-10-06
Abdalrhman Mohamed
Avoid calling `quoteSymbol` multiple times. (#7307)
tree
|
commitdiff
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
next