projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
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
2022-03-10 Andrew ReynoldsDisable timing out regressions (#8273) commit | commitdiff | tree
2022-03-10 Mathias PreinerFix regression errors for arm64 nightlies. (#8268) commit | commitdiff | tree
2022-03-09 Gereon KremerRename expert statistics to internal, add documentation... commit | commitdiff | tree
2022-03-09 Gereon KremerClear obsolete pending lemmas in arithmetic (#8236) commit | commitdiff | tree
2022-03-09 Andrew ReynoldsChange interface for printing instantiations in the... commit | commitdiff | tree
2022-03-09 Andrew ReynoldsUse expression mining independent of whether sygus... commit | commitdiff | tree
2022-03-09 Andrew ReynoldsAdd REGEXP_ALL kind to API (#8264) commit | commitdiff | tree
2022-03-09 Andrew ReynoldsAdd regression for fixed issue 6700 (#8265) commit | commitdiff | tree
2022-03-09 Andrew ReynoldsEliminate the APPLY_SELECTOR_TOTAL kind (#8266) commit | commitdiff | tree
2022-03-08 Gereon KremerProduce intermediate json output for coverage (#8252) commit | commitdiff | tree
2022-03-08 Andrew ReynoldsDo 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 ReynoldsGuard another case of non-termination in quantifiers... commit | commitdiff | tree
2022-03-08 Gereon KremerMake one CI job not use libpoly (#8261) commit | commitdiff | tree
2022-03-08 Andrew ReynoldsFixes and additions to LFSC signature (#8205) commit | commitdiff | tree
2022-03-08 Andrew ReynoldsEliminate shadowing in the quantifiers rewriter (#8244) commit | commitdiff | tree
2022-03-08 Andrew ReynoldsAdd unit for fixed project issue (#8253) commit | commitdiff | tree
2022-03-08 Gereon KremerScript to list not covered API functions (#8254) commit | commitdiff | tree
2022-03-08 Gereon KremerRerun failed tests in CI (#8258) commit | commitdiff | tree
2022-03-08 Gereon KremerDon't run the pypi packaging job on forks (#8256) commit | commitdiff | tree
2022-03-07 Andres NoetzliUpdate documentation of `Solver::getUnsatCore()` (... commit | commitdiff | tree
2022-03-07 Gereon KremerFix docs warnings (#8019) commit | commitdiff | tree
2022-03-07 Andrew ReynoldsProper error message for non-first-class sets (#8245) commit | commitdiff | tree
2022-03-07 Gereon KremerTry harder to show that a RAN is rational (#8230) commit | commitdiff | tree
2022-03-06 Andres NoetzliDisallow models with `--arrays-weak-equiv` (#8217) commit | commitdiff | tree
2022-03-05 Andrew ReynoldsUnit tests for fixed projects issues (#8229) commit | commitdiff | tree
2022-03-05 Andrew ReynoldsMake 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 KremerAdd regressions for fixed issue (#8237) commit | commitdiff | tree
2022-03-05 Andrew ReynoldsEnable NL tangent planes by default (#8233) commit | commitdiff | tree
2022-03-04 mudathirmahgoubFix bag.map upwards inferences (#8232) commit | commitdiff | tree
2022-03-04 Gereon KremerAdd unit test for fixed issue (#8235) commit | commitdiff | tree
2022-03-04 Gereon KremerRemove spurious assertion in linear solver (#8231) commit | commitdiff | tree
2022-03-04 Gereon KremerGuard recursion into terms during substitution in arith... commit | commitdiff | tree
2022-03-04 Andrew ReynoldsFix rewrite rule synthesis for 0-ary operators (#8221) commit | commitdiff | tree
2022-03-04 Andrew ReynoldsLogic exception when using solution filtering for non... commit | commitdiff | tree
2022-03-04 Gereon KremerOnly build wheels nightly and for releases (#8223) commit | commitdiff | tree
2022-03-04 Andrew ReynoldsAdd regressions for fixed projects issues (#8228) commit | commitdiff | tree
2022-03-04 Andrew ReynoldsAdd support for get learned literals in the API (#8099) commit | commitdiff | tree
2022-03-03 Andrew ReynoldsFix datatype declaration printing in LFSC printer ... commit | commitdiff | tree
2022-03-03 Gereon KremerBuild python wheels in our CI (#8087) commit | commitdiff | tree
2022-03-03 Andrew ReynoldsGeneralize LFSC string signature to sequences (#8220) commit | commitdiff | tree
2022-03-03 Lachnitt[proofs] Alethe: Removed Steps that are Double-Printed... commit | commitdiff | tree
2022-03-03 Andrew ReynoldsThrow logic exception if a transcendental function... commit | commitdiff | tree
2022-03-03 Andrew ReynoldsAdd regression for fixed issue (#8213) commit | commitdiff | tree
2022-03-03 Andrew ReynoldsImprove error for higher-order logic (#8207) commit | commitdiff | tree
2022-03-03 Mathias Preinercmake: Fix murxla setup. (#8215) commit | commitdiff | tree
2022-03-03 Gereon KremerIntegrate pythonic api (#8131) commit | commitdiff | tree
2022-03-03 Gereon KremerFix rewriting of mixed-integer atoms (#8214) commit | commitdiff | tree
2022-03-02 Andrew ReynoldsFix issue with dropping non-reduced sine terms (#8211) commit | commitdiff | tree
2022-03-02 Andrew ReynoldsFix models involving cardinality of sets of finite... commit | commitdiff | tree
2022-03-02 Andrew ReynoldsAlways purify universe from set minus (#8201) commit | commitdiff | tree
2022-03-02 Andrew ReynoldsEliminate CDHashMap::insertAtContextLevelZero (#8173) commit | commitdiff | tree
2022-03-02 Andrew ReynoldsFix incorrect assertion in prop engine proofs (#8204) commit | commitdiff | tree
2022-03-02 Andrew ReynoldsClean usage of options in regressions (#8190) commit | commitdiff | tree
2022-03-02 Andrew ReynoldsImprove error message when not using strings-exp (... commit | commitdiff | tree
2022-03-02 Gereon KremerMove libpoly <-> CoCoA conversion to new utility (... commit | commitdiff | tree
2022-03-02 Gereon KremerRefactor rewriting of arithmetic division (#8195) commit | commitdiff | tree
2022-03-02 Andrew ReynoldsAdd utility to access how to print floating point ... commit | commitdiff | tree
2022-03-02 Andrew ReynoldsMake blockModelValues robust to non-closed enumerable... commit | commitdiff | tree
2022-03-02 Andrew ReynoldsAdd regressions for fixed issues (#8202) commit | commitdiff | tree
2022-03-02 Gereon KremerPrune spurious roots in lazard evaluation of coverings... commit | commitdiff | tree
2022-03-02 Gereon KremerAdd standard theories to documentation (#8192) commit | commitdiff | tree
2022-03-01 Andrew ReynoldsFix issue involving dropped purification lemmas for... commit | commitdiff | tree
2022-03-01 Andrew ReynoldsDo not use sygus evaluation functions in sygus-inst... commit | commitdiff | tree
2022-03-01 Andrew ReynoldsDisable regression (#8191) commit | commitdiff | tree
2022-03-01 Andres Noetzli[BV] Fix rewriter policy for `bvneg` (#8196) commit | commitdiff | tree
2022-03-01 Andrew ReynoldsFix lambda lifting + proofs (#8152) commit | commitdiff | tree
2022-03-01 Andres NoetzliRemove unused data members from `TheoryArrays` (#8197) commit | commitdiff | tree
next