cvc5.git
2022-02-11 Andrew ReynoldsFix for lambda-to-array constant conversion for unused...
2022-02-11 Andres NoetzliFix type check of `seq.nth` (#8093)
2022-02-10 Andrew ReynoldsAdd assertion to require inference ids (#8091)
2022-02-10 Andrew ReynoldsUse witness terms to represent values for large strings...
2022-02-09 Mathias Preinerbv: Add --tlimit-per support for CryptoMiniSat. (#8086)
2022-02-09 Mathias Preinerbv: Add --tlimit-per support for CaDiCaL. (#8085)
2022-02-09 Andres NoetzliFix handling of `LogicException` during solving (#8000)
2022-02-09 Andres Noetzli[Seq] Fix rewrite of `(seq.nth s n)` for large `n`...
2022-02-08 Gereon KremerAdd addition utilities for the arithmetic rewriter...
2022-02-08 Andrew ReynoldsSimplify formalism of introduced arithmetic skolems...
2022-02-08 Andrew ReynoldsDistinguish proof mode from unsat core mode (#8062)
2022-02-08 Andrew ReynoldsFix LFSC node conversion for non-shared selectors ...
2022-02-08 Gereon KremerPrint more commonly used murxla commands (#8046)
2022-02-08 Andrew ReynoldsAlways produce assertions (#8041)
2022-02-08 Andrew ReynoldsMake witness form visited ref counted (#8081)
2022-02-07 Andrew ReynoldsGeneralize LFSC concat unify for splitting constants...
2022-02-07 Gereon KremerAdd user documentation for resource limits (#8058)
2022-02-07 Andrew ReynoldsFix unsoundness in IAND solver (#8053)
2022-02-07 Gereon KremerAllow non-value model values (#8076)
2022-02-07 Gereon KremerImprove combination of NRA and transcendentals (#8075)
2022-02-07 Andres Noetzli[BV] Fix response of `RewriteConcat` (#8074)
2022-02-07 Andrew ReynoldsFix indexof_re reduction (#8065)
2022-02-07 Andrew V. JonesCorrect search location for CLN libs (#8070)
2022-02-06 Andres Noetzli[Seq] Check types for split on indices (#8066)
2022-02-05 Andrew ReynoldsFix another rewrite involving iand (#8054)
2022-02-04 Andres Noetzli[Rewriter] Always rewrite again when kind changes ...
2022-02-04 Andrew ReynoldsStandardizing notifications for setting options in...
2022-02-04 Aina NiemetzFP: Rename tester kinds. (#8037)
2022-02-04 Gereon KremerUse Add instead of Plus (#8043)
2022-02-03 Andrew ReynoldsSimplify handling of disequalities in strings (#8047)
2022-02-03 Gereon KremerImprove theory combination over real algebraic models...
2022-02-03 Andrew ReynoldsEliminate even more static uses of rewrite (#8044)
2022-02-03 Andrew ReynoldsTest proof granularity theory-rewrite by default (...
2022-02-03 Gereon KremerReplace a some more static options (#8042)
2022-02-03 Andrew ReynoldsEliminate more static uses of rewrite (#8040)
2022-02-03 mudathirmahgoubAdd table.product operator (#8020)
2022-02-03 Andrew ReynoldsAdd miscellaneous missing theory definitions for LFSC...
2022-02-03 Gereon KremerAdd node utils for the arithmetic rewriter (#8012)
2022-02-03 Andres NoetzliSend all `nth` terms to the core array solver (#7990)
2022-02-03 Aina NiemetzRename kind PLUS -> ADD. (#8036)
2022-02-03 Aina Niemetzapi: Remove obsolete function declaration in Cython...
2022-02-03 Aina Niemetzapi: Rename kinds MINUS -> SUB and UMINUS -> NEG. ...
2022-02-03 Aina Niemetzapi: Add explicit guard for option produce-assertions...
2022-02-02 Alex OzdemirChange name of Python API's package from pycvc5 to...
2022-02-02 Andrew ReynoldsFix rewrite for eliminating constant factors of PI...
2022-02-02 Aina NiemetzRename kinds MINUS -> SUB and UMINUS -> NEG. (#8035)
2022-02-02 Gereon KremerUse proper filename in -o subs documentation (#8030)
2022-02-02 Andrew ReynoldsFix invalid rewrite involving iand (#8026)
2022-02-02 Aina Niemetzapi: Rename mk<Value> functions for FP for consistency...
2022-02-02 Andrew ReynoldsFix printing of re.loop as an operator in LFSC (#8029)
2022-02-02 Andrew ReynoldsMake LFSC side condition for concat unify robust to...
2022-02-02 Andrew ReynoldsAdd missing null terminators for regexp (#8027)
2022-02-02 Gereon KremerAdd additional check to avoid cyclic substitution ...
2022-02-02 mudathirmahgoubUpdate datatypes.rst (#8009)
2022-02-02 Andrew ReynoldsRemove more static calls to rewrite (#8025)
2022-02-02 Andrew ReynoldsExtend proof step buffer to optionally ensure unique...
2022-02-02 mudathirmahgoubFix parser issue with tuple_project operator (#8021)
2022-02-01 Andres Noetzli[BV] Fix strategy for `RewriteExtract` (#8011)
2022-02-01 Andres Noetzli[BV] Fix order of rewrites for `concat` (#8010)
2022-02-01 Gereon KremerAdd new ordering utility (#8008)
2022-02-01 Andrew ReynoldsAdd variant of get-difficulty for full effort lemmas...
2022-02-01 Andres Noetzli[Arrays] Fix response for `store` chains (#8015)
2022-02-01 mudathirmahgoubAdd bag.filter operator (#8006)
2022-02-01 Gereon KremerConsider RANs in variable ordering (#7964)
2022-01-31 Gereon KremerAdd utilities for flattening nodes (#7961)
2022-01-31 Andres NoetzliFix memory leak in quantifier info (#8005)
2022-01-29 Gereon KremerRename docs-releases to docs (#7999)
2022-01-28 Mathias PreinerStart post-release for 0.0.7
2022-01-28 Mathias PreinerBump version to 0.0.7
2022-01-28 Bruno DutertreTry a bit harder on the EQ_NCTN rewrite rule (#7998)
2022-01-28 Gereon KremerFix docs upload once again (#7997)
2022-01-28 Andres Noetzli[Rewrite Synthesis] Fix args for non-chaining ops ...
2022-01-27 Andrew ReynoldsDocument substitute in API (#7904)
2022-01-27 Aina NiemetzUpdate AUTHORS und copyright of docs configuration...
2022-01-27 Gereon KremerProperly recognize whether the current commit is a...
2022-01-26 Andrew ReynoldsInitial refactoring of conflict-based instantiation...
2022-01-26 mudathirmahgoubAdd Card solver to bags (#7986)
2022-01-26 Andrew ReynoldsMore fixes and improvements for query generator (#7988)
2022-01-25 Andrew ReynoldsAdd output -o post-asserts (#7987)
2022-01-25 Mathias PreinerStart post-release for 0.0.6
2022-01-25 Mathias PreinerBump version to 0.0.6
2022-01-25 Andres NoetzliSend `nth(unit(...), ...)` terms to array solver (...
2022-01-25 Andrew ReynoldsFixes and improvements to sygus satisfiable query gener...
2022-01-25 Andres Noetzli[Strings] Avoid trivial explanation (#7982)
2022-01-25 Andres Noetzli[Strings] Remove redundant call to rewriter (#7978)
2022-01-25 Andres Noetzli[FP] Fix unused variable warning (#7977)
2022-01-24 Gereon KremerDisable regression if poly is not available (#7981)
2022-01-24 Gereon KremerAlways compile RANs (#7979)
2022-01-24 Gereon KremerUse proper RAN nodes for nl model (#7939)
2022-01-24 Gereon KremerRefactor how arith rewriting checks for mult-by-zero...
2022-01-24 Abdalrhman... Enable dump tester. (#7884)
2022-01-24 Gereon KremerHave RAN fall back to RANs (#7976)
2022-01-21 Andrew ReynoldsRef count nodes in trigger trie (#7972)
2022-01-21 Andrew ReynoldsFix trivial explantions in sequences array solver ...
2022-01-20 Andres NoetzliFix `Nth-Update` rule, add `Update-Bound` rule (#7968)
2022-01-20 Andrew ReynoldsFix proofs for trivial cases of datatypes tester merge...
2022-01-20 Gereon KremerRefactor abs rewriting (#7935)
2022-01-20 Andres NoetzliFix CI build for macOS (#7970)
2022-01-19 Andres NoetzliAdd rewrites for `seq.update`/`seq.nth` (#7966)
2022-01-19 Gereon KremerFix a subtle issue with double negations in coverings...
next