git.libre-soc.org Git - cvc5.git/search

2022-02-25	Andrew Reynolds	Consolidate 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 Reynolds	Ensure variables are constrained in model when equal...	commit \| commitdiff \| tree
2022-02-24	Andrew Reynolds	Make model builder robust to multiple value-like terms...	commit \| commitdiff \| tree
2022-02-24	Gereon Kremer	Improve error message for missing options include ...	commit \| commitdiff \| tree
2022-02-24	Andrew Reynolds	Make sine solver sound with respect to region boundaries...	commit \| commitdiff \| tree
2022-02-24	Andrew Reynolds	Check for free variables in several SolverEngine calls...	commit \| commitdiff \| tree
2022-02-24	Gereon Kremer	Get rid of some static objects in arithmetic theory...	commit \| commitdiff \| tree
2022-02-24	Andrew Reynolds	Make uninterpreted sort owner non-static (#8144)	commit \| commitdiff \| tree
2022-02-24	Andrew Reynolds	Add regression for some fixed array issues (#8145)	commit \| commitdiff \| tree
2022-02-23	Gereon Kremer	Add two regressions related to RAN models (#8142)	commit \| commitdiff \| tree
2022-02-23	Andrew Reynolds	Allow elimination of unevaluated terms by default ...	commit \| commitdiff \| tree
2022-02-23	Andrew Reynolds	Further relax what is considered a value in the model...	commit \| commitdiff \| tree
2022-02-23	Andrew Reynolds	Do not insist that entries for UF are constant in FMF...	commit \| commitdiff \| tree
2022-02-23	Andrew Reynolds	Eliminate match from LFSC proofs (#8090)	commit \| commitdiff \| tree
2022-02-23	Gereon Kremer	Remove long obsolete unsafe interrupt exception (#8139)	commit \| commitdiff \| tree
2022-02-23	Andrew Reynolds	Option exception when incompatible with proofs (#8064)	commit \| commitdiff \| tree
2022-02-23	Gereon Kremer	Fix creation of RAN from non-dyadic rational (#8138)	commit \| commitdiff \| tree
2022-02-23	Gereon Kremer	Fix icp candidate parsing (#8137)	commit \| commitdiff \| tree
2022-02-23	Andrew Reynolds	Properly 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 Kremer	Fix pruning of covering intervals in proofs (#8084)	commit \| commitdiff \| tree
2022-02-23	Gereon Kremer	Refactor multiplication in arithmetic rewriter (#7965)	commit \| commitdiff \| tree
2022-02-23	Andrew Reynolds	Fix issue in datatypes care graph computation involving...	commit \| commitdiff \| tree
2022-02-22	Andrew Reynolds	Support some cases of isConst for regular expressions...	commit \| commitdiff \| tree
2022-02-22	Andrew Reynolds	Remove refineConflicts option (#8129)	commit \| commitdiff \| tree
2022-02-22	Andrew Reynolds	Change inference scheme in transcendentals to rewrite...	commit \| commitdiff \| tree
2022-02-22	Andrew Reynolds	Relax 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 Reynolds	Fixes and additions for LFSC signatures (#8120)	commit \| commitdiff \| tree
2022-02-18	Andrew Reynolds	Add unit test for fixed issue with get-difficulty ...	commit \| commitdiff \| tree
2022-02-18	Andrew Reynolds	Throw option exceptions when combining input conversion...	commit \| commitdiff \| tree
2022-02-18	Andrew Reynolds	Add well formed term check to solver engine (#8056)	commit \| commitdiff \| tree
2022-02-18	Andres Noetzli	Improve `STRINGS_ARRAY_UPDATE_BOUND` inference (#8123)	commit \| commitdiff \| tree
2022-02-18	Andrew Reynolds	Make spurious assertion into warning (#8051)	commit \| commitdiff \| tree
2022-02-18	Andres Noetzli	Fix `STRINGS_ARRAY_NTH_UPDATE` inference (#8121)	commit \| commitdiff \| tree
2022-02-17	Andrew Reynolds	Introduce skolem function to make transcendental function...	commit \| commitdiff \| tree
2022-02-17	Andrew Reynolds	Missing ids for arith conflicts (#8108)	commit \| commitdiff \| tree
2022-02-17	Andrew Reynolds	Remove 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 Reynolds	Only consider relevant terms in the array-inspired...	commit \| commitdiff \| tree
2022-02-15	Abdalrhman Mohamed	Support `try` and `all` reconstruction modes. (#8098)	commit \| commitdiff \| tree
2022-02-11	Andrew Reynolds	Ensure proofs are fully disabled when incompatible...	commit \| commitdiff \| tree
2022-02-11	Andrew Reynolds	Fix for lambda-to-array constant conversion for unused...	commit \| commitdiff \| tree
2022-02-11	Andres Noetzli	Fix type check of `seq.nth` (#8093)	commit \| commitdiff \| tree
2022-02-10	Andrew Reynolds	Add assertion to require inference ids (#8091)	commit \| commitdiff \| tree
2022-02-10	Andrew Reynolds	Use witness terms to represent values for large strings...	commit \| commitdiff \| tree
2022-02-09	Mathias Preiner	bv: Add --tlimit-per support for CryptoMiniSat. (#8086)	commit \| commitdiff \| tree
2022-02-09	Mathias Preiner	bv: Add --tlimit-per support for CaDiCaL. (#8085)	commit \| commitdiff \| tree
2022-02-09	Andres Noetzli	Fix 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 Kremer	Add addition utilities for the arithmetic rewriter...	commit \| commitdiff \| tree
2022-02-08	Andrew Reynolds	Simplify formalism of introduced arithmetic skolems...	commit \| commitdiff \| tree
2022-02-08	Andrew Reynolds	Distinguish proof mode from unsat core mode (#8062)	commit \| commitdiff \| tree
2022-02-08	Andrew Reynolds	Fix LFSC node conversion for non-shared selectors ...	commit \| commitdiff \| tree
2022-02-08	Gereon Kremer	Print more commonly used murxla commands (#8046)	commit \| commitdiff \| tree
2022-02-08	Andrew Reynolds	Always produce assertions (#8041)	commit \| commitdiff \| tree
2022-02-08	Andrew Reynolds	Make witness form visited ref counted (#8081)	commit \| commitdiff \| tree
2022-02-07	Andrew Reynolds	Generalize LFSC concat unify for splitting constants...	commit \| commitdiff \| tree
2022-02-07	Gereon Kremer	Add user documentation for resource limits (#8058)	commit \| commitdiff \| tree
2022-02-07	Andrew Reynolds	Fix unsoundness in IAND solver (#8053)	commit \| commitdiff \| tree
2022-02-07	Gereon Kremer	Allow non-value model values (#8076)	commit \| commitdiff \| tree
2022-02-07	Gereon Kremer	Improve 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 Reynolds	Fix indexof_re reduction (#8065)	commit \| commitdiff \| tree
2022-02-07	Andrew V. Jones	Correct 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 Reynolds	Fix 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 Reynolds	Standardizing notifications for setting options in...	commit \| commitdiff \| tree
2022-02-04	Aina Niemetz	FP: Rename tester kinds. (#8037)	commit \| commitdiff \| tree
2022-02-04	Gereon Kremer	Use Add instead of Plus (#8043)	commit \| commitdiff \| tree
2022-02-03	Andrew Reynolds	Simplify handling of disequalities in strings (#8047)	commit \| commitdiff \| tree
2022-02-03	Gereon Kremer	Improve theory combination over real algebraic models...	commit \| commitdiff \| tree
2022-02-03	Andrew Reynolds	Eliminate even more static uses of rewrite (#8044)	commit \| commitdiff \| tree
2022-02-03	Andrew Reynolds	Test proof granularity theory-rewrite by default (...	commit \| commitdiff \| tree
2022-02-03	Gereon Kremer	Replace a some more static options (#8042)	commit \| commitdiff \| tree
2022-02-03	Andrew Reynolds	Eliminate more static uses of rewrite (#8040)	commit \| commitdiff \| tree
2022-02-03	mudathirmahgoub	Add table.product operator (#8020)	commit \| commitdiff \| tree
2022-02-03	Andrew Reynolds	Add miscellaneous missing theory definitions for LFSC...	commit \| commitdiff \| tree
2022-02-03	Gereon Kremer	Add node utils for the arithmetic rewriter (#8012)	commit \| commitdiff \| tree
2022-02-03	Andres Noetzli	Send all `nth` terms to the core array solver (#7990)	commit \| commitdiff \| tree
2022-02-03	Aina Niemetz	Rename kind PLUS -> ADD. (#8036)	commit \| commitdiff \| tree
2022-02-03	Aina Niemetz	api: Remove obsolete function declaration in Cython...	commit \| commitdiff \| tree
2022-02-03	Aina Niemetz	api: Rename kinds MINUS -> SUB and UMINUS -> NEG. ...	commit \| commitdiff \| tree
2022-02-03	Aina Niemetz	api: Add explicit guard for option produce-assertions...	commit \| commitdiff \| tree
2022-02-02	Alex Ozdemir	Change name of Python API's package from pycvc5 to...	commit \| commitdiff \| tree
2022-02-02	Andrew Reynolds	Fix rewrite for eliminating constant factors of PI...	commit \| commitdiff \| tree
2022-02-02	Aina Niemetz	Rename kinds MINUS -> SUB and UMINUS -> NEG. (#8035)	commit \| commitdiff \| tree
2022-02-02	Gereon Kremer	Use proper filename in -o subs documentation (#8030)	commit \| commitdiff \| tree
2022-02-02	Andrew Reynolds	Fix invalid rewrite involving iand (#8026)	commit \| commitdiff \| tree
2022-02-02	Aina Niemetz	api: Rename mk<Value> functions for FP for consistency...	commit \| commitdiff \| tree
2022-02-02	Andrew Reynolds	Fix printing of re.loop as an operator in LFSC (#8029)	commit \| commitdiff \| tree
2022-02-02	Andrew Reynolds	Make LFSC side condition for concat unify robust to...	commit \| commitdiff \| tree
2022-02-02	Andrew Reynolds	Add missing null terminators for regexp (#8027)	commit \| commitdiff \| tree
2022-02-02	Gereon Kremer	Add additional check to avoid cyclic substitution ...	commit \| commitdiff \| tree
2022-02-02	mudathirmahgoub	Update datatypes.rst (#8009)	commit \| commitdiff \| tree
2022-02-02	Andrew Reynolds	Remove more static calls to rewrite (#8025)	commit \| commitdiff \| tree
next

RSS Atom