projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
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
2022-03-11
Andrew Reynolds
Fix reduction for arc trig functions (#8289)
commit
|
commitdiff
|
tree
2022-03-11
Andres Noetzli
[CI] Make building static/shared configurable (#8272)
commit
|
commitdiff
|
tree
2022-03-11
Andres Noetzli
Refactor kinds parser (#8287)
commit
|
commitdiff
|
tree
2022-03-10
Andrew Reynolds
Fix issue with subtyping from set membership in models...
commit
|
commitdiff
|
tree
2022-03-10
Andrew Reynolds
Fix theoryOf call in get equality status (#8279)
commit
|
commitdiff
|
tree
2022-03-10
Andrew Reynolds
Eliminate unecessary datatype options (#8280)
commit
|
commitdiff
|
tree
2022-03-10
mudathirmahgoub
Fix cvc5-projects issue 475 (#8278)
commit
|
commitdiff
|
tree
2022-03-10
Andrew Reynolds
Add output -o pre-asserts (#8270)
commit
|
commitdiff
|
tree
2022-03-10
Andrew Reynolds
Disable timing out regressions (#8273)
commit
|
commitdiff
|
tree
2022-03-10
Mathias Preiner
Fix regression errors for arm64 nightlies. (#8268)
commit
|
commitdiff
|
tree
2022-03-09
Gereon Kremer
Rename expert statistics to internal, add documentation...
commit
|
commitdiff
|
tree
2022-03-09
Gereon Kremer
Clear obsolete pending lemmas in arithmetic (#8236)
commit
|
commitdiff
|
tree
2022-03-09
Andrew Reynolds
Change interface for printing instantiations in the...
commit
|
commitdiff
|
tree
2022-03-09
Andrew Reynolds
Use expression mining independent of whether sygus...
commit
|
commitdiff
|
tree
2022-03-09
Andrew Reynolds
Add REGEXP_ALL kind to API (#8264)
commit
|
commitdiff
|
tree
2022-03-09
Andrew Reynolds
Add regression for fixed issue 6700 (#8265)
commit
|
commitdiff
|
tree
2022-03-09
Andrew Reynolds
Eliminate the APPLY_SELECTOR_TOTAL kind (#8266)
commit
|
commitdiff
|
tree
2022-03-08
Gereon Kremer
Produce intermediate json output for coverage (#8252)
commit
|
commitdiff
|
tree
2022-03-08
Andrew Reynolds
Do not expand APPLY_SELECTOR (#8174)
commit
|
commitdiff
|
tree
2022-03-08
Andres Noetzli
[API/Python] Add support for `Solver::getProof()` ...
commit
|
commitdiff
|
tree
2022-03-08
Andrew Reynolds
Guard another case of non-termination in quantifiers...
commit
|
commitdiff
|
tree
2022-03-08
Gereon Kremer
Make one CI job not use libpoly (#8261)
commit
|
commitdiff
|
tree
2022-03-08
Andrew Reynolds
Fixes and additions to LFSC signature (#8205)
commit
|
commitdiff
|
tree
2022-03-08
Andrew Reynolds
Eliminate shadowing in the quantifiers rewriter (#8244)
commit
|
commitdiff
|
tree
2022-03-08
Andrew Reynolds
Add unit for fixed project issue (#8253)
commit
|
commitdiff
|
tree
2022-03-08
Gereon Kremer
Script to list not covered API functions (#8254)
commit
|
commitdiff
|
tree
2022-03-08
Gereon Kremer
Rerun failed tests in CI (#8258)
commit
|
commitdiff
|
tree
2022-03-08
Gereon Kremer
Don't run the pypi packaging job on forks (#8256)
commit
|
commitdiff
|
tree
2022-03-07
Andres Noetzli
Update documentation of `Solver::getUnsatCore()` (...
commit
|
commitdiff
|
tree
2022-03-07
Gereon Kremer
Fix docs warnings (#8019)
commit
|
commitdiff
|
tree
2022-03-07
Andrew Reynolds
Proper error message for non-first-class sets (#8245)
commit
|
commitdiff
|
tree
2022-03-07
Gereon Kremer
Try harder to show that a RAN is rational (#8230)
commit
|
commitdiff
|
tree
2022-03-06
Andres Noetzli
Disallow models with `--arrays-weak-equiv` (#8217)
commit
|
commitdiff
|
tree
2022-03-05
Andrew Reynolds
Unit tests for fixed projects issues (#8229)
commit
|
commitdiff
|
tree
2022-03-05
Andrew Reynolds
Make seq.unit robust wrt subtyping (#8209)
commit
|
commitdiff
|
tree
2022-03-05
Andres Noetzli
[Docs] Add missing requirement (#8238)
commit
|
commitdiff
|
tree
2022-03-05
Gereon Kremer
Add regressions for fixed issue (#8237)
commit
|
commitdiff
|
tree
2022-03-05
Andrew Reynolds
Enable NL tangent planes by default (#8233)
commit
|
commitdiff
|
tree
2022-03-04
mudathirmahgoub
Fix bag.map upwards inferences (#8232)
commit
|
commitdiff
|
tree
2022-03-04
Gereon Kremer
Add unit test for fixed issue (#8235)
commit
|
commitdiff
|
tree
2022-03-04
Gereon Kremer
Remove spurious assertion in linear solver (#8231)
commit
|
commitdiff
|
tree
next