projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2022-03-24 Haniel Barbosa[unsat-cores] [sat-proof] Fix open proofs due to theory... commit | commitdiff | tree
2022-03-23 Andrew ReynoldsClean options (#8309) commit | commitdiff | tree
2022-03-23 Gereon KremerAdd API unit tests for statistics (#8341) commit | commitdiff | tree
2022-03-23 Andrew ReynoldsAdd SynthResult to the API (#8370) commit | commitdiff | tree
2022-03-23 Gereon KremerAdd `getOptionInfo()` and `getOptionNames()` to python... commit | commitdiff | tree
2022-03-23 Gereon KremerDocument proof rules for transcendentals (#8375) commit | commitdiff | tree
2022-03-23 Andrew ReynoldsMake IDOF_MAX rewrite only apply when all children... commit | commitdiff | tree
2022-03-23 Mathias PreinerOnly update latest tag if commit changed. (#8379) commit | commitdiff | tree
2022-03-23 Andrew ReynoldsAdd internal synth result class (#8352) commit | commitdiff | tree
2022-03-23 Gereon KremerRun gen-versioninfo unconditionally (#8368) commit | commitdiff | tree
2022-03-23 Gereon KremerStore latest builds in a special release (#8337) commit | commitdiff | tree
2022-03-23 Gereon KremerRemove dependency on build (#8367) commit | commitdiff | tree
2022-03-23 mudathirmahgoubupdate SET_COMPREHENSION documentation (#8372) commit | commitdiff | tree
2022-03-23 Andrew ReynoldsInitial documentation on LFSC (#8365) commit | commitdiff | tree
2022-03-23 mudathirmahgoubFix cvc5-projects issue 497 (#8331) commit | commitdiff | tree
2022-03-23 Andrew ReynoldsFix non-termination issue in sygus enumerator (#8340) commit | commitdiff | tree
2022-03-22 Andrew ReynoldsChange null terminator for regular expression intersect... commit | commitdiff | tree
2022-03-22 Gereon KremerRefactor proof rule documentation (#8303) commit | commitdiff | tree
2022-03-22 Andrew ReynoldsUpdates for the theory reference for separation logic... commit | commitdiff | tree
2022-03-22 Gereon KremerMake 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 mudathirmahgoubupdate 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 ReynoldsFixes for witness terms appearing in CEGQI instantiatio... commit | commitdiff | tree
2022-03-22 Andrew ReynoldsRefactor result class (#8313) commit | commitdiff | tree
2022-03-22 Mathias Preinerapi: 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 NoetzliRemove `Op::getIndices()` (#8355) commit | commitdiff | tree
2022-03-21 Andrew ReynoldsFix return value for candidate rewrite database (#8354) commit | commitdiff | tree
2022-03-21 Gereon KremerRefactor documentation (#8288) commit | commitdiff | tree
2022-03-21 Andrew ReynoldsFix LFSC conversion for seq unit (#8353) commit | commitdiff | tree
2022-03-21 Gereon KremerFix names of unit tests (#8338) commit | commitdiff | tree
2022-03-21 Andrew ReynoldsFix learned literals for top-level AND (#8336) commit | commitdiff | tree
2022-03-20 Gereon KremerAdd `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 Niemetzctest: Fix labels for python unit tests. (#8328) commit | commitdiff | tree
2022-03-17 Andrew ReynoldsUpdate care graph computations to use standard node... commit | commitdiff | tree
2022-03-17 Gereon KremerReplace `Debug` by `Trace` (#7793) commit | commitdiff | tree
2022-03-17 Andres NoetzliRemove 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 Niemetzapi: Fix documentation for *TO_FP* kinds. (#8329) commit | commitdiff | tree
2022-03-17 Aina Niemetzapi: Fix documentation for UNINTERPRETED_SORT_VALUE... commit | commitdiff | tree
2022-03-17 Gereon Kremerdon'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 NiemetzAdd unit test and assertion to test and catch cvc5... commit | commitdiff | tree
2022-03-16 Andres NoetzliRemove 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 KremerUse native cancellation mechanism (#8311) commit | commitdiff | tree
2022-03-16 Mathias Preinerunit: Add test for api::Kind. (#8322) commit | commitdiff | tree
2022-03-16 Aina NiemetzFirst step towards refactoring regression tests. (... commit | commitdiff | tree
2022-03-16 mudathirmahgoubAdd regression for cvc5-projects issue 490 (#8317) commit | commitdiff | tree
2022-03-16 Mathias Preinerapi: Print the correct string for external kinds. ... commit | commitdiff | tree
2022-03-16 Mathias Preinerrun_regression: Make sure to strip trailing whitespaces... commit | commitdiff | tree
2022-03-16 Mathias Preinerapi: Make mkDatatypeDecl argument const&. (#8315) commit | commitdiff | tree
2022-03-16 Andres NoetzliFix shared library Windows builds with LibPoly (#8306) commit | commitdiff | tree
2022-03-16 Andrew ReynoldsFix getModelValue for arithmetic (#8316) commit | commitdiff | tree
2022-03-16 Andrew ReynoldsEnsure trusted steps are given for skolem lemmas when... commit | commitdiff | tree
2022-03-16 Andres NoetzliIgnore `CMAKE_SYSROOT` when cross-compiling (#8318) commit | commitdiff | tree
2022-03-15 Andrew ReynoldsMake learned literal computation more robust (#8308) commit | commitdiff | tree
2022-03-15 Aina Niemetzapi: 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 ReynoldsAdd unit test involving seq concat term (#8257) commit | commitdiff | tree
2022-03-15 Andrew ReynoldsFix issues involving multiple sources of model substitu... commit | commitdiff | tree
2022-03-15 mudathirmahgoubAdd skolem lemmas for bags card terms (#7995) commit | commitdiff | tree
2022-03-15 Andrew ReynoldsProperly guard sort instantiate (#8247) commit | commitdiff | tree
2022-03-15 Gereon KremerEnable nl-cov-var-elim by default, but disable with... commit | commitdiff | tree
2022-03-15 Andrew ReynoldsRemove unecessary separation logic options (#8269) commit | commitdiff | tree
2022-03-15 Andres NoetzliSimplify `Scope` (#8307) commit | commitdiff | tree
2022-03-15 Andrew ReynoldsFix to consider leafs of theory sets to be variables... commit | commitdiff | tree
2022-03-15 Andrew ReynoldsSimplify reductions for set and bag choose (#8304) commit | commitdiff | tree
2022-03-15 Aina NiemetzRename TO_FP operator kinds. (#8285) commit | commitdiff | tree
2022-03-14 Andrew ReynoldsFixes for skolem definition management (#8301) commit | commitdiff | tree
2022-03-14 Andrew ReynoldsRemove unecessary methods from the API (#8260) commit | commitdiff | tree
2022-03-14 Andrew ReynoldsAdd rewrite for allchar beneath union + star (#8299) commit | commitdiff | tree
2022-03-14 Andrew ReynoldsRun preprocess rewrite on equalities until fixed point... commit | commitdiff | tree
2022-03-13 Andrew ReynoldsMinor sync from proof-new (#8293) commit | commitdiff | tree
2022-03-12 Andrew ReynoldsIntroduce new splitting inference in sets + cardinality... commit | commitdiff | tree
2022-03-12 Andrew ReynoldsAdd algorithm for finding pairs of paths in a node... commit | commitdiff | tree
2022-03-12 Mathias Preinercmake: Do not require googletest if unit tests are... commit | commitdiff | tree
2022-03-12 Andrew ReynoldsImprovements for sygus query generation (#8224) commit | commitdiff | tree
2022-03-12 Andrew ReynoldsDocument type rules (#8248) commit | commitdiff | tree
2022-03-12 Andrew ReynoldsAlways 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 Niemetzapi: Make checks header private. (#8283) commit | commitdiff | tree
2022-03-11 Andrew ReynoldsRemove old decision justification heurstic (#8275) commit | commitdiff | tree
2022-03-11 Andrew ReynoldsUpdate abduction and interpolation API to not use pass... commit | commitdiff | tree
2022-03-11 Andrew ReynoldsFix maximum value for pedantic proof level (#8246) commit | commitdiff | tree
2022-03-11 Andrew ReynoldsGuard parametric datatypes instantiated by non-first... commit | commitdiff | tree
2022-03-11 Gereon KremerAdd first step for proofs documentation (#8193) commit | commitdiff | tree
2022-03-11 Andrew ReynoldsRemove unecessary CEGQI options (#8281) commit | commitdiff | tree
2022-03-11 Andrew ReynoldsConsider APPLY_CONSTRUCTOR applied to values to be... commit | commitdiff | tree
2022-03-11 Andrew ReynoldsFix 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 NoetzliRefactor kinds parser (#8287) commit | commitdiff | tree
2022-03-10 Andrew ReynoldsFix issue with subtyping from set membership in models... commit | commitdiff | tree
2022-03-10 Andrew ReynoldsFix theoryOf call in get equality status (#8279) commit | commitdiff | tree
2022-03-10 Andrew ReynoldsEliminate unecessary datatype options (#8280) commit | commitdiff | tree
2022-03-10 mudathirmahgoubFix cvc5-projects issue 475 (#8278) commit | commitdiff | tree
2022-03-10 Andrew ReynoldsAdd output -o pre-asserts (#8270) commit | commitdiff | tree
next