cvc5.git
2022-03-22 mudathirmahgoubupdate sets-and-relations.rst (#8364)
2022-03-22 Abdalrhman... Add a timeout option for verification of synthesized...
2022-03-22 Andres Noetzli[FP] Remove `FLOATINGPOINT_TO_FP_GENERIC` kind (#8334)
2022-03-22 Andrew ReynoldsFixes for witness terms appearing in CEGQI instantiatio...
2022-03-22 Andrew ReynoldsRefactor result class (#8313)
2022-03-22 Mathias Preinerapi: Unify mkTerm variants. (#8357)
2022-03-22 Andres Noetzli[API] Support `Op::operator[]` in Java and Python ...
2022-03-21 Andres NoetzliRemove `Op::getIndices()` (#8355)
2022-03-21 Andrew ReynoldsFix return value for candidate rewrite database (#8354)
2022-03-21 Gereon KremerRefactor documentation (#8288)
2022-03-21 Andrew ReynoldsFix LFSC conversion for seq unit (#8353)
2022-03-21 Gereon KremerFix names of unit tests (#8338)
2022-03-21 Andrew ReynoldsFix learned literals for top-level AND (#8336)
2022-03-20 Gereon KremerAdd `getStatistics()` to python API (#8343)
2022-03-17 Andres Noetzli[Parser] Simplify `Smt2::addIndexedOperator()` (#8333)
2022-03-17 Aina Niemetzctest: Fix labels for python unit tests. (#8328)
2022-03-17 Andrew ReynoldsUpdate care graph computations to use standard node...
2022-03-17 Gereon KremerReplace `Debug` by `Trace` (#7793)
2022-03-17 Andres NoetzliRemove unused options handler (#8335)
2022-03-17 Andres Noetzli[CI] Use ccache for Windows builds (#8332)
2022-03-17 Aina Niemetzapi: Fix documentation for *TO_FP* kinds. (#8329)
2022-03-17 Aina Niemetzapi: Fix documentation for UNINTERPRETED_SORT_VALUE...
2022-03-17 Gereon Kremerdon't build gtest in CI (#8323)
2022-03-17 Andres Noetzli[CI] Strip stored binaries (#8327)
2022-03-16 Aina NiemetzAdd unit test and assertion to test and catch cvc5...
2022-03-16 Andres NoetzliRemove unused files in `regress0` (#8325)
2022-03-16 Andres Noetzli[CI] Build and release Win64 binaries (#8321)
2022-03-16 Gereon KremerUse native cancellation mechanism (#8311)
2022-03-16 Mathias Preinerunit: Add test for api::Kind. (#8322)
2022-03-16 Aina NiemetzFirst step towards refactoring regression tests. (...
2022-03-16 mudathirmahgoubAdd regression for cvc5-projects issue 490 (#8317)
2022-03-16 Mathias Preinerapi: Print the correct string for external kinds. ...
2022-03-16 Mathias Preinerrun_regression: Make sure to strip trailing whitespaces...
2022-03-16 Mathias Preinerapi: Make mkDatatypeDecl argument const&. (#8315)
2022-03-16 Andres NoetzliFix shared library Windows builds with LibPoly (#8306)
2022-03-16 Andrew ReynoldsFix getModelValue for arithmetic (#8316)
2022-03-16 Andrew ReynoldsEnsure trusted steps are given for skolem lemmas when...
2022-03-16 Andres NoetzliIgnore `CMAKE_SYSROOT` when cross-compiling (#8318)
2022-03-15 Andrew ReynoldsMake learned literal computation more robust (#8308)
2022-03-15 Aina Niemetzapi: Remove Sort::isFirstClass(). (#8312)
2022-03-15 Andres Noetzli[BV] Fix strategy for rewriting `bvnot` (#8297)
2022-03-15 Andrew ReynoldsAdd unit test involving seq concat term (#8257)
2022-03-15 Andrew ReynoldsFix issues involving multiple sources of model substitu...
2022-03-15 mudathirmahgoubAdd skolem lemmas for bags card terms (#7995)
2022-03-15 Andrew ReynoldsProperly guard sort instantiate (#8247)
2022-03-15 Gereon KremerEnable nl-cov-var-elim by default, but disable with...
2022-03-15 Andrew ReynoldsRemove unecessary separation logic options (#8269)
2022-03-15 Andres NoetzliSimplify `Scope` (#8307)
2022-03-15 Andrew ReynoldsFix to consider leafs of theory sets to be variables...
2022-03-15 Andrew ReynoldsSimplify reductions for set and bag choose (#8304)
2022-03-15 Aina NiemetzRename TO_FP operator kinds. (#8285)
2022-03-14 Andrew ReynoldsFixes for skolem definition management (#8301)
2022-03-14 Andrew ReynoldsRemove unecessary methods from the API (#8260)
2022-03-14 Andrew ReynoldsAdd rewrite for allchar beneath union + star (#8299)
2022-03-14 Andrew ReynoldsRun preprocess rewrite on equalities until fixed point...
2022-03-13 Andrew ReynoldsMinor sync from proof-new (#8293)
2022-03-12 Andrew ReynoldsIntroduce new splitting inference in sets + cardinality...
2022-03-12 Andrew ReynoldsAdd algorithm for finding pairs of paths in a node...
2022-03-12 Mathias Preinercmake: Do not require googletest if unit tests are...
2022-03-12 Andrew ReynoldsImprovements for sygus query generation (#8224)
2022-03-12 Andrew ReynoldsDocument type rules (#8248)
2022-03-12 Andrew ReynoldsAlways ensure literal when requiring phase via inferenc...
2022-03-11 Andres Noetzli[API/Python] Add support for `Solver::getModel()` ...
2022-03-11 Aina Niemetzapi: Make checks header private. (#8283)
2022-03-11 Andrew ReynoldsRemove old decision justification heurstic (#8275)
2022-03-11 Andrew ReynoldsUpdate abduction and interpolation API to not use pass...
2022-03-11 Andrew ReynoldsFix maximum value for pedantic proof level (#8246)
2022-03-11 Andrew ReynoldsGuard parametric datatypes instantiated by non-first...
2022-03-11 Gereon KremerAdd first step for proofs documentation (#8193)
2022-03-11 Andrew ReynoldsRemove unecessary CEGQI options (#8281)
2022-03-11 Andrew ReynoldsConsider APPLY_CONSTRUCTOR applied to values to be...
2022-03-11 Andrew ReynoldsFix reduction for arc trig functions (#8289)
2022-03-11 Andres Noetzli[CI] Make building static/shared configurable (#8272)
2022-03-11 Andres NoetzliRefactor kinds parser (#8287)
2022-03-10 Andrew ReynoldsFix issue with subtyping from set membership in models...
2022-03-10 Andrew ReynoldsFix theoryOf call in get equality status (#8279)
2022-03-10 Andrew ReynoldsEliminate unecessary datatype options (#8280)
2022-03-10 mudathirmahgoubFix cvc5-projects issue 475 (#8278)
2022-03-10 Andrew ReynoldsAdd output -o pre-asserts (#8270)
2022-03-10 Andrew ReynoldsDisable timing out regressions (#8273)
2022-03-10 Mathias PreinerFix regression errors for arm64 nightlies. (#8268)
2022-03-09 Gereon KremerRename expert statistics to internal, add documentation...
2022-03-09 Gereon KremerClear obsolete pending lemmas in arithmetic (#8236)
2022-03-09 Andrew ReynoldsChange interface for printing instantiations in the...
2022-03-09 Andrew ReynoldsUse expression mining independent of whether sygus...
2022-03-09 Andrew ReynoldsAdd REGEXP_ALL kind to API (#8264)
2022-03-09 Andrew ReynoldsAdd regression for fixed issue 6700 (#8265)
2022-03-09 Andrew ReynoldsEliminate the APPLY_SELECTOR_TOTAL kind (#8266)
2022-03-08 Gereon KremerProduce intermediate json output for coverage (#8252)
2022-03-08 Andrew ReynoldsDo not expand APPLY_SELECTOR (#8174)
2022-03-08 Andres Noetzli[API/Python] Add support for `Solver::getProof()` ...
2022-03-08 Andrew ReynoldsGuard another case of non-termination in quantifiers...
2022-03-08 Gereon KremerMake one CI job not use libpoly (#8261)
2022-03-08 Andrew ReynoldsFixes and additions to LFSC signature (#8205)
2022-03-08 Andrew ReynoldsEliminate shadowing in the quantifiers rewriter (#8244)
2022-03-08 Andrew ReynoldsAdd unit for fixed project issue (#8253)
2022-03-08 Gereon KremerScript to list not covered API functions (#8254)
2022-03-08 Gereon KremerRerun failed tests in CI (#8258)
2022-03-08 Gereon KremerDon't run the pypi packaging job on forks (#8256)
2022-03-07 Andres NoetzliUpdate documentation of `Solver::getUnsatCore()` (...
next