projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Relax what is generated in the model from NL (#8113)
[cvc5.git] / src /
2022-02-22 Andrew ReynoldsRelax what is generated in the model from NL (#8113) tree | commitdiff
2022-02-22 vinciusb[proofs] [dot] Enable DAG and tree printing with dot... tree | commitdiff
2022-02-18 Andrew ReynoldsThrow option exceptions when combining input conversion... tree | commitdiff
2022-02-18 Andrew ReynoldsAdd well formed term check to solver engine (#8056) tree | commitdiff
2022-02-18 Andres NoetzliImprove `STRINGS_ARRAY_UPDATE_BOUND` inference (#8123) tree | commitdiff
2022-02-18 Andrew ReynoldsMake spurious assertion into warning (#8051) tree | commitdiff
2022-02-18 Andres NoetzliFix `STRINGS_ARRAY_NTH_UPDATE` inference (#8121) tree | commitdiff
2022-02-17 Andrew ReynoldsIntroduce skolem function to make transcendental functi... tree | commitdiff
2022-02-17 Andrew ReynoldsMissing ids for arith conflicts (#8108) tree | commitdiff
2022-02-17 Andrew ReynoldsRemove some irrelevant node kinds from the model (... tree | commitdiff
2022-02-17 Lachnitt[proofs] [alethe] Introduce all_simplify and replace... tree | commitdiff
2022-02-17 Andrew Reynolds[proofs] Consolidate multiple substitutions to single... tree | commitdiff
2022-02-16 Andrew Reynolds[proofs] Make cache (optionally) persistent in lazy... tree | commitdiff
2022-02-16 Andrew ReynoldsOnly consider relevant terms in the array-inspired... tree | commitdiff
2022-02-15 Abdalrhman MohamedSupport `try` and `all` reconstruction modes. (#8098) tree | commitdiff
2022-02-11 Andrew ReynoldsEnsure proofs are fully disabled when incompatible... tree | commitdiff
2022-02-11 Andrew ReynoldsFix for lambda-to-array constant conversion for unused... tree | commitdiff
2022-02-11 Andres NoetzliFix type check of `seq.nth` (#8093) tree | commitdiff
2022-02-10 Andrew ReynoldsAdd assertion to require inference ids (#8091) tree | commitdiff
2022-02-10 Andrew ReynoldsUse witness terms to represent values for large strings... tree | commitdiff
2022-02-09 Mathias Preinerbv: Add --tlimit-per support for CryptoMiniSat. (#8086) tree | commitdiff
2022-02-09 Mathias Preinerbv: Add --tlimit-per support for CaDiCaL. (#8085) tree | commitdiff
2022-02-09 Andres NoetzliFix handling of `LogicException` during solving (#8000) tree | commitdiff
2022-02-09 Andres Noetzli[Seq] Fix rewrite of `(seq.nth s n)` for large `n`... tree | commitdiff
2022-02-08 Gereon KremerAdd addition utilities for the arithmetic rewriter... tree | commitdiff
2022-02-08 Andrew ReynoldsSimplify formalism of introduced arithmetic skolems... tree | commitdiff
2022-02-08 Andrew ReynoldsDistinguish proof mode from unsat core mode (#8062) tree | commitdiff
2022-02-08 Andrew ReynoldsFix LFSC node conversion for non-shared selectors ... tree | commitdiff
2022-02-08 Andrew ReynoldsAlways produce assertions (#8041) tree | commitdiff
2022-02-08 Andrew ReynoldsMake witness form visited ref counted (#8081) tree | commitdiff
2022-02-07 Gereon KremerAdd user documentation for resource limits (#8058) tree | commitdiff
2022-02-07 Andrew ReynoldsFix unsoundness in IAND solver (#8053) tree | commitdiff
2022-02-07 Gereon KremerAllow non-value model values (#8076) tree | commitdiff
2022-02-07 Gereon KremerImprove combination of NRA and transcendentals (#8075) tree | commitdiff
2022-02-07 Andres Noetzli[BV] Fix response of `RewriteConcat` (#8074) tree | commitdiff
2022-02-07 Andrew ReynoldsFix indexof_re reduction (#8065) tree | commitdiff
2022-02-06 Andres Noetzli[Seq] Check types for split on indices (#8066) tree | commitdiff
2022-02-05 Andrew ReynoldsFix another rewrite involving iand (#8054) tree | commitdiff
2022-02-04 Andres Noetzli[Rewriter] Always rewrite again when kind changes ... tree | commitdiff
2022-02-04 Andrew ReynoldsStandardizing notifications for setting options in... tree | commitdiff
2022-02-04 Aina NiemetzFP: Rename tester kinds. (#8037) tree | commitdiff
2022-02-03 Andrew ReynoldsSimplify handling of disequalities in strings (#8047) tree | commitdiff
2022-02-03 Gereon KremerImprove theory combination over real algebraic models... tree | commitdiff
2022-02-03 Andrew ReynoldsEliminate even more static uses of rewrite (#8044) tree | commitdiff
2022-02-03 Gereon KremerReplace a some more static options (#8042) tree | commitdiff
2022-02-03 Andrew ReynoldsEliminate more static uses of rewrite (#8040) tree | commitdiff
2022-02-03 mudathirmahgoubAdd table.product operator (#8020) tree | commitdiff
2022-02-03 Gereon KremerAdd node utils for the arithmetic rewriter (#8012) tree | commitdiff
2022-02-03 Andres NoetzliSend all `nth` terms to the core array solver (#7990) tree | commitdiff
2022-02-03 Aina NiemetzRename kind PLUS -> ADD. (#8036) tree | commitdiff
2022-02-03 Aina Niemetzapi: Remove obsolete function declaration in Cython... tree | commitdiff
2022-02-03 Aina Niemetzapi: Rename kinds MINUS -> SUB and UMINUS -> NEG. ... tree | commitdiff
2022-02-03 Aina Niemetzapi: Add explicit guard for option produce-assertions... tree | commitdiff
2022-02-02 Alex OzdemirChange name of Python API's package from pycvc5 to... tree | commitdiff
2022-02-02 Andrew ReynoldsFix rewrite for eliminating constant factors of PI... tree | commitdiff
2022-02-02 Aina NiemetzRename kinds MINUS -> SUB and UMINUS -> NEG. (#8035) tree | commitdiff
2022-02-02 Gereon KremerUse proper filename in -o subs documentation (#8030) tree | commitdiff
2022-02-02 Andrew ReynoldsFix invalid rewrite involving iand (#8026) tree | commitdiff
2022-02-02 Aina Niemetzapi: Rename mk<Value> functions for FP for consistency... tree | commitdiff
2022-02-02 Andrew ReynoldsFix printing of re.loop as an operator in LFSC (#8029) tree | commitdiff
2022-02-02 Andrew ReynoldsAdd missing null terminators for regexp (#8027) tree | commitdiff
2022-02-02 Gereon KremerAdd additional check to avoid cyclic substitution ... tree | commitdiff
2022-02-02 mudathirmahgoubUpdate datatypes.rst (#8009) tree | commitdiff
2022-02-02 Andrew ReynoldsRemove more static calls to rewrite (#8025) tree | commitdiff
2022-02-02 Andrew ReynoldsExtend proof step buffer to optionally ensure unique... tree | commitdiff
2022-02-02 mudathirmahgoubFix parser issue with tuple_project operator (#8021) tree | commitdiff
2022-02-01 Andres Noetzli[BV] Fix strategy for `RewriteExtract` (#8011) tree | commitdiff
2022-02-01 Andres Noetzli[BV] Fix order of rewrites for `concat` (#8010) tree | commitdiff
2022-02-01 Gereon KremerAdd new ordering utility (#8008) tree | commitdiff
2022-02-01 Andrew ReynoldsAdd variant of get-difficulty for full effort lemmas... tree | commitdiff
2022-02-01 Andres Noetzli[Arrays] Fix response for `store` chains (#8015) tree | commitdiff
2022-02-01 mudathirmahgoubAdd bag.filter operator (#8006) tree | commitdiff
2022-02-01 Gereon KremerConsider RANs in variable ordering (#7964) tree | commitdiff
2022-01-31 Gereon KremerAdd utilities for flattening nodes (#7961) tree | commitdiff
2022-01-31 Andres NoetzliFix memory leak in quantifier info (#8005) tree | commitdiff
2022-01-28 Bruno DutertreTry a bit harder on the EQ_NCTN rewrite rule (#7998) tree | commitdiff
2022-01-28 Andres Noetzli[Rewrite Synthesis] Fix args for non-chaining ops ... tree | commitdiff
2022-01-27 Andrew ReynoldsDocument substitute in API (#7904) tree | commitdiff
2022-01-26 Andrew ReynoldsInitial refactoring of conflict-based instantiation... tree | commitdiff
2022-01-26 mudathirmahgoubAdd Card solver to bags (#7986) tree | commitdiff
2022-01-26 Andrew ReynoldsMore fixes and improvements for query generator (#7988) tree | commitdiff
2022-01-25 Andrew ReynoldsAdd output -o post-asserts (#7987) tree | commitdiff
2022-01-25 Andres NoetzliSend `nth(unit(...), ...)` terms to array solver (... tree | commitdiff
2022-01-25 Andrew ReynoldsFixes and improvements to sygus satisfiable query gener... tree | commitdiff
2022-01-25 Andres Noetzli[Strings] Avoid trivial explanation (#7982) tree | commitdiff
2022-01-25 Andres Noetzli[Strings] Remove redundant call to rewriter (#7978) tree | commitdiff
2022-01-25 Andres Noetzli[FP] Fix unused variable warning (#7977) tree | commitdiff
2022-01-24 Gereon KremerAlways compile RANs (#7979) tree | commitdiff
2022-01-24 Gereon KremerUse proper RAN nodes for nl model (#7939) tree | commitdiff
2022-01-24 Gereon KremerRefactor how arith rewriting checks for mult-by-zero... tree | commitdiff
2022-01-24 Abdalrhman MohamedEnable dump tester. (#7884) tree | commitdiff
2022-01-24 Gereon KremerHave RAN fall back to RANs (#7976) tree | commitdiff
2022-01-21 Andrew ReynoldsRef count nodes in trigger trie (#7972) tree | commitdiff
2022-01-21 Andrew ReynoldsFix trivial explantions in sequences array solver ... tree | commitdiff
2022-01-20 Andres NoetzliFix `Nth-Update` rule, add `Update-Bound` rule (#7968) tree | commitdiff
2022-01-20 Andrew ReynoldsFix proofs for trivial cases of datatypes tester merge... tree | commitdiff
2022-01-20 Gereon KremerRefactor abs rewriting (#7935) tree | commitdiff
2022-01-19 Andres NoetzliAdd rewrites for `seq.update`/`seq.nth` (#7966) tree | commitdiff
2022-01-19 Gereon KremerFix a subtle issue with double negations in coverings... tree | commitdiff
2022-01-19 Gereon KremerMake tracing for arithmetic rewriter more consistent... tree | commitdiff
next