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

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) Fixes https://github.com/cvc5/cvc5/issues/6654.	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
2022-02-02	Andrew Reynolds	Extend proof step buffer to optionally ensure unique...	commit \| commitdiff \| tree
2022-02-02	mudathirmahgoub	Fix parser issue with tuple_project operator (#8021)	commit \| commitdiff \| tree
2022-02-01	Andres Noetzli	[BV] Fix strategy for `RewriteExtract` (#8011)	commit \| commitdiff \| tree
2022-02-01	Andres Noetzli	[BV] Fix order of rewrites for `concat` (#8010)	commit \| commitdiff \| tree
2022-02-01	Gereon Kremer	Add new ordering utility (#8008)	commit \| commitdiff \| tree
2022-02-01	Andrew Reynolds	Add variant of get-difficulty for full effort lemmas...	commit \| commitdiff \| tree
2022-02-01	Andres Noetzli	[Arrays] Fix response for `store` chains (#8015)	commit \| commitdiff \| tree
2022-02-01	mudathirmahgoub	Add bag.filter operator (#8006)	commit \| commitdiff \| tree
2022-02-01	Gereon Kremer	Consider RANs in variable ordering (#7964)	commit \| commitdiff \| tree
2022-01-31	Gereon Kremer	Add utilities for flattening nodes (#7961)	commit \| commitdiff \| tree
2022-01-31	Andres Noetzli	Fix memory leak in quantifier info (#8005)	commit \| commitdiff \| tree
2022-01-29	Gereon Kremer	Rename docs-releases to docs (#7999) ... It now lives at https://cvc5.github.io/docs/	commit \| commitdiff \| tree
2022-01-28	Bruno Dutertre	Try a bit harder on the EQ_NCTN rewrite rule (#7998)	commit \| commitdiff \| tree
2022-01-28	Gereon Kremer	Fix docs upload once again (#7997)	commit \| commitdiff \| tree
2022-01-28	Andres Noetzli	[Rewrite Synthesis] Fix args for non-chaining ops ... Fixes https://github.com/cvc5/cvc5-projects/issues... https://github.com/cvc5/cvc5-projects/issues...	commit \| commitdiff \| tree
2022-01-27	Andrew Reynolds	Document substitute in API (#7904)	commit \| commitdiff \| tree
2022-01-27	Aina Niemetz	Update AUTHORS und copyright of docs configuration...	commit \| commitdiff \| tree
2022-01-27	Gereon Kremer	Properly recognize whether the current commit is a...	commit \| commitdiff \| tree
2022-01-26	Andrew Reynolds	Initial refactoring of conflict-based instantiation...	commit \| commitdiff \| tree
2022-01-26	mudathirmahgoub	Add Card solver to bags (#7986)	commit \| commitdiff \| tree
2022-01-26	Andrew Reynolds	More fixes and improvements for query generator (#7988)	commit \| commitdiff \| tree
2022-01-25	Andrew Reynolds	Add output -o post-asserts (#7987)	commit \| commitdiff \| tree
2022-01-25	Andres Noetzli	Send `nth(unit(...), ...)` terms to array solver (...	commit \| commitdiff \| tree
2022-01-25	Andrew Reynolds	Fixes and improvements to sygus satisfiable query generation...	commit \| commitdiff \| tree
2022-01-25	Andres Noetzli	[Strings] Avoid trivial explanation (#7982)	commit \| commitdiff \| tree
2022-01-25	Andres Noetzli	[Strings] Remove redundant call to rewriter (#7978)	commit \| commitdiff \| tree
2022-01-25	Andres Noetzli	[FP] Fix unused variable warning (#7977)	commit \| commitdiff \| tree
2022-01-24	Gereon Kremer	Disable regression if poly is not available (#7981)	commit \| commitdiff \| tree
2022-01-24	Gereon Kremer	Always compile RANs (#7979)	commit \| commitdiff \| tree
2022-01-24	Gereon Kremer	Use proper RAN nodes for nl model (#7939)	commit \| commitdiff \| tree
2022-01-24	Gereon Kremer	Refactor how arith rewriting checks for mult-by-zero...	commit \| commitdiff \| tree
2022-01-24	Abdalrhman Mohamed	Enable dump tester. (#7884)	commit \| commitdiff \| tree
2022-01-24	Gereon Kremer	Have RAN fall back to RANs (#7976)	commit \| commitdiff \| tree
2022-01-21	Andrew Reynolds	Ref count nodes in trigger trie (#7972)	commit \| commitdiff \| tree
2022-01-21	Andrew Reynolds	Fix trivial explantions in sequences array solver ...	commit \| commitdiff \| tree
2022-01-20	Andres Noetzli	Fix `Nth-Update` rule, add `Update-Bound` rule (#7968)	commit \| commitdiff \| tree
2022-01-20	Andrew Reynolds	Fix proofs for trivial cases of datatypes tester merge...	commit \| commitdiff \| tree
2022-01-20	Gereon Kremer	Refactor abs rewriting (#7935)	commit \| commitdiff \| tree
2022-01-20	Andres Noetzli	Fix CI build for macOS (#7970)	commit \| commitdiff \| tree
2022-01-19	Andres Noetzli	Add rewrites for `seq.update`/`seq.nth` (#7966)	commit \| commitdiff \| tree
2022-01-19	Gereon Kremer	Fix a subtle issue with double negations in coverings...	commit \| commitdiff \| tree
2022-01-19	Gereon Kremer	Make tracing for arithmetic rewriter more consistent...	commit \| commitdiff \| tree
2022-01-19	Gereon Kremer	Update to latest libpoly version (#7963)	commit \| commitdiff \| tree
2022-01-18	Andrew Reynolds	Distinguish purification types for strings proof reconstruct...	commit \| commitdiff \| tree
2022-01-18	Gereon Kremer	Some random documentation issues (#7921)	commit \| commitdiff \| tree
2022-01-18	Andres Noetzli	[API] Add missing arity check (#7905)	commit \| commitdiff \| tree
2022-01-18	Matthew Sotoudeh	Fix CMake script for static, auto-download, cln configuratio...	commit \| commitdiff \| tree
2022-01-18	Andrew Reynolds	Print original form for substitutions and learned literals...	commit \| commitdiff \| tree
2022-01-17	Andrew Reynolds	Refactor options related to rewriting and symmetry...	commit \| commitdiff \| tree
2022-01-17	Andres Noetzli	[Strings] Fix rewriter for `re.loop` (#7956)	commit \| commitdiff \| tree
2022-01-15	Gereon Kremer	Change how RANs are printed (#7955)	commit \| commitdiff \| tree
2022-01-15	Andrew Reynolds	Add inverse inference for update-over-concat (#7954)	commit \| commitdiff \| tree
2022-01-14	Andrew Reynolds	Improve names for sygus enumeration option (#7945)	commit \| commitdiff \| tree
2022-01-14	Andrew Reynolds	Clean enumerative instantiation options (#7947)	commit \| commitdiff \| tree
2022-01-14	Andrew Reynolds	Implement -o subs to show learned top-level substitutions...	commit \| commitdiff \| tree
2022-01-14	Alex Ozdemir	Rename python APIs (#7950)	commit \| commitdiff \| tree
next

RSS Atom