projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
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
2022-03-16
Mathias Preiner
api: Print the correct string for external kinds. ...
commit
|
commitdiff
|
tree
2022-03-16
Mathias Preiner
run_regression: Make sure to strip trailing whitespaces...
commit
|
commitdiff
|
tree
2022-03-16
Mathias Preiner
api: Make mkDatatypeDecl argument const&. (#8315)
commit
|
commitdiff
|
tree
2022-03-16
Andres Noetzli
Fix shared library Windows builds with LibPoly (#8306)
commit
|
commitdiff
|
tree
2022-03-16
Andrew Reynolds
Fix getModelValue for arithmetic (#8316)
commit
|
commitdiff
|
tree
2022-03-16
Andrew Reynolds
Ensure trusted steps are given for skolem lemmas when...
commit
|
commitdiff
|
tree
2022-03-16
Andres Noetzli
Ignore `CMAKE_SYSROOT` when cross-compiling (#8318)
commit
|
commitdiff
|
tree
2022-03-15
Andrew Reynolds
Make learned literal computation more robust (#8308)
commit
|
commitdiff
|
tree
2022-03-15
Aina Niemetz
api: Remove Sort::isFirstClass(). (#8312)
commit
|
commitdiff
|
tree
2022-03-15
Andres Noetzli
[BV] Fix strategy for rewriting `bvnot` (#8297)
commit
|
commitdiff
|
tree
2022-03-15
Andrew Reynolds
Add unit test involving seq concat term (#8257)
commit
|
commitdiff
|
tree
2022-03-15
Andrew Reynolds
Fix issues involving multiple sources of model substitu...
commit
|
commitdiff
|
tree
2022-03-15
mudathirmahgoub
Add skolem lemmas for bags card terms (#7995)
commit
|
commitdiff
|
tree
2022-03-15
Andrew Reynolds
Properly guard sort instantiate (#8247)
commit
|
commitdiff
|
tree
2022-03-15
Gereon Kremer
Enable nl-cov-var-elim by default, but disable with...
commit
|
commitdiff
|
tree
2022-03-15
Andrew Reynolds
Remove unecessary separation logic options (#8269)
commit
|
commitdiff
|
tree
2022-03-15
Andres Noetzli
Simplify `Scope` (#8307)
commit
|
commitdiff
|
tree
2022-03-15
Andrew Reynolds
Fix to consider leafs of theory sets to be variables...
commit
|
commitdiff
|
tree
2022-03-15
Andrew Reynolds
Simplify reductions for set and bag choose (#8304)
commit
|
commitdiff
|
tree
2022-03-15
Aina Niemetz
Rename TO_FP operator kinds. (#8285)
commit
|
commitdiff
|
tree
2022-03-14
Andrew Reynolds
Fixes for skolem definition management (#8301)
commit
|
commitdiff
|
tree
2022-03-14
Andrew Reynolds
Remove unecessary methods from the API (#8260)
commit
|
commitdiff
|
tree
2022-03-14
Andrew Reynolds
Add rewrite for allchar beneath union + star (#8299)
commit
|
commitdiff
|
tree
2022-03-14
Andrew Reynolds
Run preprocess rewrite on equalities until fixed point...
commit
|
commitdiff
|
tree
2022-03-13
Andrew Reynolds
Minor sync from proof-new (#8293)
commit
|
commitdiff
|
tree
2022-03-12
Andrew Reynolds
Introduce new splitting inference in sets + cardinality...
commit
|
commitdiff
|
tree
2022-03-12
Andrew Reynolds
Add algorithm for finding pairs of paths in a node...
commit
|
commitdiff
|
tree
2022-03-12
Mathias Preiner
cmake: Do not require googletest if unit tests are...
commit
|
commitdiff
|
tree
2022-03-12
Andrew Reynolds
Improvements for sygus query generation (#8224)
commit
|
commitdiff
|
tree
2022-03-12
Andrew Reynolds
Document type rules (#8248)
commit
|
commitdiff
|
tree
2022-03-12
Andrew Reynolds
Always ensure literal when requiring phase via inferenc...
commit
|
commitdiff
|
tree
2022-03-11
Andres Noetzli
[API/Python] Add support for `Solver::getModel()` ...
commit
|
commitdiff
|
tree
2022-03-11
Aina Niemetz
api: Make checks header private. (#8283)
commit
|
commitdiff
|
tree
2022-03-11
Andrew Reynolds
Remove old decision justification heurstic (#8275)
commit
|
commitdiff
|
tree
2022-03-11
Andrew Reynolds
Update abduction and interpolation API to not use pass...
commit
|
commitdiff
|
tree
2022-03-11
Andrew Reynolds
Fix maximum value for pedantic proof level (#8246)
commit
|
commitdiff
|
tree
2022-03-11
Andrew Reynolds
Guard parametric datatypes instantiated by non-first...
commit
|
commitdiff
|
tree
2022-03-11
Gereon Kremer
Add first step for proofs documentation (#8193)
commit
|
commitdiff
|
tree
2022-03-11
Andrew Reynolds
Remove unecessary CEGQI options (#8281)
commit
|
commitdiff
|
tree
2022-03-11
Andrew Reynolds
Consider APPLY_CONSTRUCTOR applied to values to be...
commit
|
commitdiff
|
tree
next