projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2022-02-28 Andrew ReynoldsTrack names for witness terms in model (#8184) commit | commitdiff | tree
2022-02-28 Andrew ReynoldsAdd two reduction schemas for sin terms (#8171) commit | commitdiff | tree
2022-02-28 Andres NoetzliRemove broken/unused `--mmap` option (#8178) commit | commitdiff | tree
2022-02-28 Gereon KremerAdd scripts to build python wheels (#8132) commit | commitdiff | tree
2022-02-28 Gereon KremerRefactor rewriting of arithmetic leafs (#8177) commit | commitdiff | tree
2022-02-28 Gereon KremerRefactor rewriting of arithmetic addition (#8180) commit | commitdiff | tree
2022-02-25 Andrew ReynoldsConsider PI to be a model value (#8176) commit | commitdiff | tree
2022-02-25 Andrew ReynoldsSyntax fixes for LFSC signature (#8172) commit | commitdiff | tree
2022-02-25 Gereon KremerAdd utilities to rewrite atoms for the arithmetic rewri... commit | commitdiff | tree
2022-02-25 Gereon KremerRefactor rewriting of arithmetic negation and subtracti... commit | commitdiff | tree
2022-02-25 Gereon KremerSlightly refactor arithmetic rewriting for extended... commit | commitdiff | tree
2022-02-25 Andrew ReynoldsFix non-termination in quantifiers rewriter (#8165) commit | commitdiff | tree
2022-02-25 Andrew ReynoldsSimplify and fix how purified terms are managed in... commit | commitdiff | tree
2022-02-25 Andrew ReynoldsFix dropped bounds on PI (#8164) commit | commitdiff | tree
2022-02-25 Andrew ReynoldsRemove approximations infrastructure from model (#8166) commit | commitdiff | tree
2022-02-25 Andrew ReynoldsRemove spurious assertion involving constants for argum... commit | commitdiff | tree
2022-02-25 Andrew ReynoldsMake quantifiers terminate if it detects a (duplicate... commit | commitdiff | tree
2022-02-25 Andrew ReynoldsAdd regression for fixed transcendental regression... commit | commitdiff | tree
2022-02-25 Andrew ReynoldsConsolidate extended rewrite preprocessing modes (... commit | commitdiff | tree
2022-02-25 Andres Noetzli[Python API] Add support for blocking models (#8134) commit | commitdiff | tree
2022-02-24 Andrew ReynoldsEnsure variables are constrained in model when equal... commit | commitdiff | tree
2022-02-24 Andrew ReynoldsMake model builder robust to multiple value-like terms... commit | commitdiff | tree
2022-02-24 Gereon KremerImprove error message for missing options include ... commit | commitdiff | tree
2022-02-24 Andrew ReynoldsMake sine solver sound with respect to region boundarie... commit | commitdiff | tree
2022-02-24 Andrew ReynoldsCheck for free variables in several SolverEngine calls... commit | commitdiff | tree
2022-02-24 Gereon KremerGet rid of some static objects in arithmetic theory... commit | commitdiff | tree
2022-02-24 Andrew ReynoldsMake uninterpreted sort owner non-static (#8144) commit | commitdiff | tree
2022-02-24 Andrew ReynoldsAdd regression for some fixed array issues (#8145) commit | commitdiff | tree
2022-02-23 Gereon KremerAdd two regressions related to RAN models (#8142) commit | commitdiff | tree
2022-02-23 Andrew ReynoldsAllow elimination of unevaluated terms by default ... commit | commitdiff | tree
2022-02-23 Andrew ReynoldsFurther relax what is considered a value in the model... commit | commitdiff | tree
2022-02-23 Andrew ReynoldsDo not insist that entries for UF are constant in FMF... commit | commitdiff | tree
2022-02-23 Andrew ReynoldsEliminate match from LFSC proofs (#8090) commit | commitdiff | tree
2022-02-23 Gereon KremerRemove long obsolete unsafe interrupt exception (#8139) commit | commitdiff | tree
2022-02-23 Andrew ReynoldsOption exception when incompatible with proofs (#8064) commit | commitdiff | tree
2022-02-23 Gereon KremerFix creation of RAN from non-dyadic rational (#8138) commit | commitdiff | tree
2022-02-23 Gereon KremerFix icp candidate parsing (#8137) commit | commitdiff | tree
2022-02-23 Andrew ReynoldsProperly sanatize user names in LFSC (#8080) commit | commitdiff | tree
2022-02-23 Andres Noetzli[Rewriter] Do not attempt to rewrite constants (#8061) commit | commitdiff | tree
2022-02-23 Gereon KremerFix pruning of covering intervals in proofs (#8084) commit | commitdiff | tree
2022-02-23 Gereon KremerRefactor multiplication in arithmetic rewriter (#7965) commit | commitdiff | tree
2022-02-23 Andrew ReynoldsFix issue in datatypes care graph computation involving... commit | commitdiff | tree
2022-02-22 Andrew ReynoldsSupport some cases of isConst for regular expressions... commit | commitdiff | tree
2022-02-22 Andrew ReynoldsRemove refineConflicts option (#8129) commit | commitdiff | tree
2022-02-22 Andrew ReynoldsChange inference scheme in transcendentals to rewrite... commit | commitdiff | tree
2022-02-22 Andrew ReynoldsRelax what is generated in the model from NL (#8113) commit | commitdiff | tree
2022-02-22 vinciusb[proofs] [dot] Enable DAG and tree printing with dot... commit | commitdiff | tree
2022-02-21 Andrew ReynoldsFixes and additions for LFSC signatures (#8120) commit | commitdiff | tree
2022-02-18 Andrew ReynoldsAdd unit test for fixed issue with get-difficulty ... commit | commitdiff | tree
2022-02-18 Andrew ReynoldsThrow option exceptions when combining input conversion... commit | commitdiff | tree
2022-02-18 Andrew ReynoldsAdd well formed term check to solver engine (#8056) commit | commitdiff | tree
2022-02-18 Andres NoetzliImprove `STRINGS_ARRAY_UPDATE_BOUND` inference (#8123) commit | commitdiff | tree
2022-02-18 Andrew ReynoldsMake spurious assertion into warning (#8051) commit | commitdiff | tree
2022-02-18 Andres NoetzliFix `STRINGS_ARRAY_NTH_UPDATE` inference (#8121) commit | commitdiff | tree
2022-02-17 Andrew ReynoldsIntroduce skolem function to make transcendental functi... commit | commitdiff | tree
2022-02-17 Andrew ReynoldsMissing ids for arith conflicts (#8108) commit | commitdiff | tree
2022-02-17 Andrew ReynoldsRemove some irrelevant node kinds from the model (... commit | commitdiff | tree
2022-02-17 Lachnitt[proofs] [alethe] Introduce all_simplify and replace... commit | commitdiff | tree
2022-02-17 Andrew Reynolds[proofs] Consolidate multiple substitutions to single... commit | commitdiff | tree
2022-02-16 Andrew Reynolds[proofs] Make cache (optionally) persistent in lazy... commit | commitdiff | tree
2022-02-16 Andrew ReynoldsOnly consider relevant terms in the array-inspired... commit | commitdiff | tree
2022-02-15 Abdalrhman... Support `try` and `all` reconstruction modes. (#8098) commit | commitdiff | tree
2022-02-11 Andrew ReynoldsEnsure proofs are fully disabled when incompatible... commit | commitdiff | tree
2022-02-11 Andrew ReynoldsFix for lambda-to-array constant conversion for unused... commit | commitdiff | tree
2022-02-11 Andres NoetzliFix type check of `seq.nth` (#8093) commit | commitdiff | tree
2022-02-10 Andrew ReynoldsAdd assertion to require inference ids (#8091) commit | commitdiff | tree
2022-02-10 Andrew ReynoldsUse witness terms to represent values for large strings... commit | commitdiff | tree
2022-02-09 Mathias Preinerbv: Add --tlimit-per support for CryptoMiniSat. (#8086) commit | commitdiff | tree
2022-02-09 Mathias Preinerbv: Add --tlimit-per support for CaDiCaL. (#8085) commit | commitdiff | tree
2022-02-09 Andres NoetzliFix handling of `LogicException` during solving (#8000) commit | commitdiff | tree
2022-02-09 Andres Noetzli[Seq] Fix rewrite of `(seq.nth s n)` for large `n`... commit | commitdiff | tree
2022-02-08 Gereon KremerAdd addition utilities for the arithmetic rewriter... commit | commitdiff | tree
2022-02-08 Andrew ReynoldsSimplify formalism of introduced arithmetic skolems... commit | commitdiff | tree
2022-02-08 Andrew ReynoldsDistinguish proof mode from unsat core mode (#8062) commit | commitdiff | tree
2022-02-08 Andrew ReynoldsFix LFSC node conversion for non-shared selectors ... commit | commitdiff | tree
2022-02-08 Gereon KremerPrint more commonly used murxla commands (#8046) commit | commitdiff | tree
2022-02-08 Andrew ReynoldsAlways produce assertions (#8041) commit | commitdiff | tree
2022-02-08 Andrew ReynoldsMake witness form visited ref counted (#8081) commit | commitdiff | tree
2022-02-07 Andrew ReynoldsGeneralize LFSC concat unify for splitting constants... commit | commitdiff | tree
2022-02-07 Gereon KremerAdd user documentation for resource limits (#8058) commit | commitdiff | tree
2022-02-07 Andrew ReynoldsFix unsoundness in IAND solver (#8053) commit | commitdiff | tree
2022-02-07 Gereon KremerAllow non-value model values (#8076) commit | commitdiff | tree
2022-02-07 Gereon KremerImprove combination of NRA and transcendentals (#8075) commit | commitdiff | tree
2022-02-07 Andres Noetzli[BV] Fix response of `RewriteConcat` (#8074) commit | commitdiff | tree
2022-02-07 Andrew ReynoldsFix indexof_re reduction (#8065) commit | commitdiff | tree
2022-02-07 Andrew V. JonesCorrect search location for CLN libs (#8070) commit | commitdiff | tree
2022-02-06 Andres Noetzli[Seq] Check types for split on indices (#8066) commit | commitdiff | tree
2022-02-05 Andrew ReynoldsFix another rewrite involving iand (#8054) commit | commitdiff | tree
2022-02-04 Andres Noetzli[Rewriter] Always rewrite again when kind changes ... commit | commitdiff | tree
2022-02-04 Andrew ReynoldsStandardizing notifications for setting options in... commit | commitdiff | tree
2022-02-04 Aina NiemetzFP: Rename tester kinds. (#8037) commit | commitdiff | tree
2022-02-04 Gereon KremerUse Add instead of Plus (#8043) commit | commitdiff | tree
2022-02-03 Andrew ReynoldsSimplify handling of disequalities in strings (#8047) commit | commitdiff | tree
2022-02-03 Gereon KremerImprove theory combination over real algebraic models... commit | commitdiff | tree
2022-02-03 Andrew ReynoldsEliminate even more static uses of rewrite (#8044) commit | commitdiff | tree
2022-02-03 Andrew ReynoldsTest proof granularity theory-rewrite by default (... commit | commitdiff | tree
2022-02-03 Gereon KremerReplace a some more static options (#8042) commit | commitdiff | tree
2022-02-03 Andrew ReynoldsEliminate more static uses of rewrite (#8040) commit | commitdiff | tree
2022-02-03 mudathirmahgoubAdd table.product operator (#8020) commit | commitdiff | tree
2022-02-03 Andrew ReynoldsAdd miscellaneous missing theory definitions for LFSC... commit | commitdiff | tree
next