projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
2022-03-29
Andrew Reynolds
Fix issue related to use of Boolean term variable for...
commit
|
commitdiff
|
tree
2022-03-29
Andres Noetzli
[API] Add `{is,get}RoundingModeValue()` (#8429)
commit
|
commitdiff
|
tree
2022-03-29
Aina Niemetz
TypeNode: Refactor get param types handling. (#8428)
commit
|
commitdiff
|
tree
2022-03-29
Clark Barrett
Fix for issue 5925: constant arrays should be nonlinear...
commit
|
commitdiff
|
tree
2022-03-29
Aina Niemetz
api: Add Sort::isInstantiated(). (#8425)
commit
|
commitdiff
|
tree
2022-03-29
Andres Noetzli
Move `RoundingMode` to `cvc5_types.h` (#8427)
commit
|
commitdiff
|
tree
2022-03-28
Andrew Reynolds
Mark more methods as experimental (#8426)
commit
|
commitdiff
|
tree
2022-03-28
Mathias Preiner
Rename get-interpol to get-interpolant. (#8424)
commit
|
commitdiff
|
tree
2022-03-28
Andres Noetzli
[API] Mark methods as experimental (#8249)
commit
|
commitdiff
|
tree
2022-03-28
Mathias Preiner
ci: Enable all language bindings for debug build. ...
commit
|
commitdiff
|
tree
2022-03-28
Aina Niemetz
api: Remove left-over Sort::getUninterpretedSortName...
commit
|
commitdiff
|
tree
2022-03-28
Lachnitt
[proofs] Alethe: Call Printer (#8408)
commit
|
commitdiff
|
tree
2022-03-28
Lachnitt
[proofs] Alethe: Add ALETHE_RULE to builtin proof check...
commit
|
commitdiff
|
tree
2022-03-28
Andrew Reynolds
Fix synth result python unit test (#8418)
commit
|
commitdiff
|
tree
2022-03-28
Mathias Preiner
Mark solve-bv-as-int as expert. (#8417)
commit
|
commitdiff
|
tree
2022-03-26
yoni206
Separating produce-interpols from the mode of interpola...
commit
|
commitdiff
|
tree
2022-03-26
Aina Niemetz
builtin: Move type rules implementation to .cpp file...
commit
|
commitdiff
|
tree
2022-03-26
Aina Niemetz
api: Rename *SortConstructor* to *UninterpretedSortCons...
commit
|
commitdiff
|
tree
2022-03-26
Andrew Reynolds
Fix spurious assertion failure (#8404)
commit
|
commitdiff
|
tree
2022-03-26
Andrew Reynolds
Throw logic exception for set.map (#8403)
commit
|
commitdiff
|
tree
2022-03-26
Andrew Reynolds
More minor cleaning of options (#8401)
commit
|
commitdiff
|
tree
2022-03-26
Andrew Reynolds
Fixes for API kind documentation (#8397)
commit
|
commitdiff
|
tree
2022-03-26
Gereon Kremer
Add API unit tests for options (#8339)
commit
|
commitdiff
|
tree
2022-03-25
Mathias Preiner
api: Unify mkOp variants. (#8369)
commit
|
commitdiff
|
tree
2022-03-25
Aina Niemetz
api: More comprehensive documentation of INTERNAL_KIND...
commit
|
commitdiff
|
tree
2022-03-25
Andres Noetzli
[Parser] Fix resolution of indexed symbols (#8383)
commit
|
commitdiff
|
tree
2022-03-25
Aina Niemetz
api: Remove Sort::isParametricDatatype(). (#8405)
commit
|
commitdiff
|
tree
2022-03-25
Haniel Barbosa
[proofs] [sat] Have SAT solver communicate whether...
commit
|
commitdiff
|
tree
2022-03-25
Aina Niemetz
api: Rename kind NULL_EXPR to NULL_TERM. (#8402)
commit
|
commitdiff
|
tree
2022-03-25
Andres Noetzli
Generate `enum` bindings for Python and Java (#8393)
commit
|
commitdiff
|
tree
2022-03-25
Andrew Reynolds
Update checkSynth and checkSynthNext to return SynthRes...
commit
|
commitdiff
|
tree
2022-03-25
Andrew Reynolds
Change output of abduction/interpolation for failed...
commit
|
commitdiff
|
tree
2022-03-25
Lachnitt
[proofs] Alethe: Bug Fix in Cong Rule (#8391)
commit
|
commitdiff
|
tree
2022-03-25
Aina Niemetz
api: Remove blocks in kinds header. (#8398)
commit
|
commitdiff
|
tree
2022-03-25
Haniel Barbosa
[proofs] [cnf] Utilities to notify and track proofs...
commit
|
commitdiff
|
tree
2022-03-25
Andrew Reynolds
Fixes related to set defaults for sygus/proofs (#8395)
commit
|
commitdiff
|
tree
2022-03-25
Andres Noetzli
Fix Python API tests (#8392)
commit
|
commitdiff
|
tree
2022-03-25
Aina Niemetz
api: Refactor kinds documentation. (#8384)
commit
|
commitdiff
|
tree
2022-03-25
Andrew Reynolds
Properly guard commands in the SyGuS API (#8390)
commit
|
commitdiff
|
tree
2022-03-25
Andrew Reynolds
Recategorize options (#8386)
commit
|
commitdiff
|
tree
2022-03-25
Andrew Reynolds
Fixes for theory reference for datatypes (#8380)
commit
|
commitdiff
|
tree
2022-03-24
Gereon Kremer
Document proof rules for coverings solver (#8376)
commit
|
commitdiff
|
tree
2022-03-24
Andrew Reynolds
Minor updates for quantifiers options (#8385)
commit
|
commitdiff
|
tree
2022-03-24
Haniel Barbosa
[proofs] [sat] Handle resolution proofs for optimized...
commit
|
commitdiff
|
tree
2022-03-24
Gereon Kremer
Document arithmetic proof rules (#8373)
commit
|
commitdiff
|
tree
2022-03-24
Andrew Reynolds
Standardize more instances of skolems (#8351)
commit
|
commitdiff
|
tree
2022-03-24
Haniel Barbosa
[sat] Add option to disable Minisat simplifications...
commit
|
commitdiff
|
tree
2022-03-24
Andrew Reynolds
Fix a couple of parse error messages for sygus (#8381)
commit
|
commitdiff
|
tree
2022-03-24
Haniel Barbosa
[unsat-cores] [sat-proof] Fix open proofs due to theory...
commit
|
commitdiff
|
tree
2022-03-23
Andrew Reynolds
Clean options (#8309)
commit
|
commitdiff
|
tree
2022-03-23
Gereon Kremer
Add API unit tests for statistics (#8341)
commit
|
commitdiff
|
tree
2022-03-23
Andrew Reynolds
Add SynthResult to the API (#8370)
commit
|
commitdiff
|
tree
2022-03-23
Gereon Kremer
Add `getOptionInfo()` and `getOptionNames()` to python...
commit
|
commitdiff
|
tree
2022-03-23
Gereon Kremer
Document proof rules for transcendentals (#8375)
commit
|
commitdiff
|
tree
2022-03-23
Andrew Reynolds
Make IDOF_MAX rewrite only apply when all children...
commit
|
commitdiff
|
tree
2022-03-23
Mathias Preiner
Only update latest tag if commit changed. (#8379)
commit
|
commitdiff
|
tree
2022-03-23
Andrew Reynolds
Add internal synth result class (#8352)
commit
|
commitdiff
|
tree
2022-03-23
Gereon Kremer
Run gen-versioninfo unconditionally (#8368)
commit
|
commitdiff
|
tree
2022-03-23
Gereon Kremer
Store latest builds in a special release (#8337)
commit
|
commitdiff
|
tree
2022-03-23
Gereon Kremer
Remove dependency on build (#8367)
commit
|
commitdiff
|
tree
2022-03-23
mudathirmahgoub
update SET_COMPREHENSION documentation (#8372)
commit
|
commitdiff
|
tree
2022-03-23
Andrew Reynolds
Initial documentation on LFSC (#8365)
commit
|
commitdiff
|
tree
2022-03-23
mudathirmahgoub
Fix cvc5-projects issue 497 (#8331)
commit
|
commitdiff
|
tree
2022-03-23
Andrew Reynolds
Fix non-termination issue in sygus enumerator (#8340)
commit
|
commitdiff
|
tree
2022-03-22
Andrew Reynolds
Change null terminator for regular expression intersect...
commit
|
commitdiff
|
tree
2022-03-22
Gereon Kremer
Refactor proof rule documentation (#8303)
commit
|
commitdiff
|
tree
2022-03-22
Andrew Reynolds
Updates for the theory reference for separation logic...
commit
|
commitdiff
|
tree
2022-03-22
Gereon Kremer
Make uncovered-api-functions.py exit with 1 if somethin...
commit
|
commitdiff
|
tree
2022-03-22
Haniel Barbosa
[proofs] Alethe: fixing formatting and adding missing...
commit
|
commitdiff
|
tree
2022-03-22
mudathirmahgoub
update sets-and-relations.rst (#8364)
commit
|
commitdiff
|
tree
2022-03-22
Abdalrhman...
Add a timeout option for verification of synthesized...
commit
|
commitdiff
|
tree
2022-03-22
Andres Noetzli
[FP] Remove `FLOATINGPOINT_TO_FP_GENERIC` kind (#8334)
commit
|
commitdiff
|
tree
2022-03-22
Andrew Reynolds
Fixes for witness terms appearing in CEGQI instantiatio...
commit
|
commitdiff
|
tree
2022-03-22
Andrew Reynolds
Refactor result class (#8313)
commit
|
commitdiff
|
tree
2022-03-22
Mathias Preiner
api: Unify mkTerm variants. (#8357)
commit
|
commitdiff
|
tree
2022-03-22
Andres Noetzli
[API] Support `Op::operator[]` in Java and Python ...
commit
|
commitdiff
|
tree
2022-03-21
Andres Noetzli
Remove `Op::getIndices()` (#8355)
commit
|
commitdiff
|
tree
2022-03-21
Andrew Reynolds
Fix return value for candidate rewrite database (#8354)
commit
|
commitdiff
|
tree
2022-03-21
Gereon Kremer
Refactor documentation (#8288)
commit
|
commitdiff
|
tree
2022-03-21
Andrew Reynolds
Fix LFSC conversion for seq unit (#8353)
commit
|
commitdiff
|
tree
2022-03-21
Gereon Kremer
Fix names of unit tests (#8338)
commit
|
commitdiff
|
tree
2022-03-21
Andrew Reynolds
Fix learned literals for top-level AND (#8336)
commit
|
commitdiff
|
tree
2022-03-20
Gereon Kremer
Add `getStatistics()` to python API (#8343)
commit
|
commitdiff
|
tree
2022-03-17
Andres Noetzli
[Parser] Simplify `Smt2::addIndexedOperator()` (#8333)
commit
|
commitdiff
|
tree
2022-03-17
Aina Niemetz
ctest: Fix labels for python unit tests. (#8328)
commit
|
commitdiff
|
tree
2022-03-17
Andrew Reynolds
Update care graph computations to use standard node...
commit
|
commitdiff
|
tree
2022-03-17
Gereon Kremer
Replace `Debug` by `Trace` (#7793)
commit
|
commitdiff
|
tree
2022-03-17
Andres Noetzli
Remove unused options handler (#8335)
commit
|
commitdiff
|
tree
2022-03-17
Andres Noetzli
[CI] Use ccache for Windows builds (#8332)
commit
|
commitdiff
|
tree
2022-03-17
Aina Niemetz
api: Fix documentation for *TO_FP* kinds. (#8329)
commit
|
commitdiff
|
tree
2022-03-17
Aina Niemetz
api: Fix documentation for UNINTERPRETED_SORT_VALUE...
commit
|
commitdiff
|
tree
2022-03-17
Gereon Kremer
don't build gtest in CI (#8323)
commit
|
commitdiff
|
tree
2022-03-17
Andres Noetzli
[CI] Strip stored binaries (#8327)
commit
|
commitdiff
|
tree
2022-03-16
Aina Niemetz
Add unit test and assertion to test and catch cvc5...
commit
|
commitdiff
|
tree
2022-03-16
Andres Noetzli
Remove unused files in `regress0` (#8325)
commit
|
commitdiff
|
tree
2022-03-16
Andres Noetzli
[CI] Build and release Win64 binaries (#8321)
commit
|
commitdiff
|
tree
2022-03-16
Gereon Kremer
Use native cancellation mechanism (#8311)
commit
|
commitdiff
|
tree
2022-03-16
Mathias Preiner
unit: Add test for api::Kind. (#8322)
commit
|
commitdiff
|
tree
2022-03-16
Aina Niemetz
First step towards refactoring regression tests. (...
commit
|
commitdiff
|
tree
2022-03-16
mudathirmahgoub
Add regression for cvc5-projects issue 490 (#8317)
commit
|
commitdiff
|
tree
next