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

2021-07-29	Gereon Kremer	Integrate installation instructions into documentation...	commit \| commitdiff \| tree
2021-07-29	Aina Niemetz	quickstart: Add python example to docs. (#6949)	commit \| commitdiff \| tree
2021-07-29	Haniel Barbosa	[proofs] Set BV solver to better proof-producing one...	commit \| commitdiff \| tree
2021-07-29	yoni206	Python quick start example (#6939)	commit \| commitdiff \| tree
2021-07-29	Andrew Reynolds	Integrate central equality engine approach into theory...	commit \| commitdiff \| tree
2021-07-29	Andrew Reynolds	Minor updates to shared terms database for central...	commit \| commitdiff \| tree
2021-07-28	makaimann	Fixes for building python wheels on manylinux2014 ...	commit \| commitdiff \| tree
2021-07-28	Andrew Reynolds	Minor changes to arrays in preparation for central...	commit \| commitdiff \| tree
2021-07-28	Gereon Kremer	Only use libedit on tty inputs (#6946)	commit \| commitdiff \| tree
2021-07-28	Andres Noetzli	Print link to docs preview (#6922)	commit \| commitdiff \| tree
2021-07-28	Andrew Reynolds	Make extended rewriter methods const (#6948)	commit \| commitdiff \| tree
2021-07-27	Mathias Preiner	bv: Refactor getEqualityStatus and use for both bitblasting...	commit \| commitdiff \| tree
2021-07-27	Mathias Preiner	proof: Add eqrange expansion rule. (#6936)	commit \| commitdiff \| tree
2021-07-27	Andrew Reynolds	Track instantiation reasons in proofs (#6935)	commit \| commitdiff \| tree
2021-07-27	Andrew Reynolds	Add basic LFSC utilities (#6879)	commit \| commitdiff \| tree
2021-07-27	Andrew Reynolds	Move enum value generator to own file (#6941)	commit \| commitdiff \| tree
2021-07-27	Andrew Reynolds	Minor fix for term database + central equality engine...	commit \| commitdiff \| tree
2021-07-27	Andrew Reynolds	Revert change to regression (#6940)	commit \| commitdiff \| tree
2021-07-27	Andrew Reynolds	Make all dependencies in the fast enumerator optional...	commit \| commitdiff \| tree
2021-07-27	Andrew Reynolds	Add print expression utility (#6880)	commit \| commitdiff \| tree
2021-07-27	Andres Noetzli	Add regression for fixed `str.indexof_re` issue (#6938)	commit \| commitdiff \| tree
2021-07-27	Andrew Reynolds	Minor changes from proof-new (#6937)	commit \| commitdiff \| tree
2021-07-27	Andrew Reynolds	Miscellaneous fixes from proof-new (#6914)	commit \| commitdiff \| tree
2021-07-27	Andrew Reynolds	Add proof letify utility (#6881)	commit \| commitdiff \| tree
2021-07-27	Andrew Reynolds	Fix eq proof conversion for constant merged parameterized...	commit \| commitdiff \| tree
2021-07-27	Andrew Reynolds	Default equality proofs for bags and separation logic...	commit \| commitdiff \| tree
2021-07-27	Andrew Reynolds	Add sygus enumerator callback (#6923)	commit \| commitdiff \| tree
2021-07-26	Gereon Kremer	Move public options functions to separate file (#6671)	commit \| commitdiff \| tree
2021-07-26	Andrew Reynolds	Enable default equality proofs for sets (#6931)	commit \| commitdiff \| tree
2021-07-26	Andrew Reynolds	More updates to arithmetic in preparation for central...	commit \| commitdiff \| tree
2021-07-25	Andrew Reynolds	Changes to datatypes in preparation for central equality...	commit \| commitdiff \| tree
2021-07-25	Andrew Reynolds	Refactor equality engine setup for arithmetic congruence...	commit \| commitdiff \| tree
2021-07-24	Andres Noetzli	Fix CLN build (#6920)	commit \| commitdiff \| tree
2021-07-23	Andres Noetzli	Configuration: Indicate dependencies being built (...	commit \| commitdiff \| tree
2021-07-23	Andres Noetzli	Fix CoCoA build for newer compilers (#6919)	commit \| commitdiff \| tree
2021-07-23	Aina Niemetz	FP: Add option to word-blast more lazily. (#6904)	commit \| commitdiff \| tree
2021-07-22	Andrew Reynolds	Simplify computation of relevant terms in datatypes...	commit \| commitdiff \| tree
2021-07-22	Andrew Reynolds	Add the central equality engine manager (#6893)	commit \| commitdiff \| tree
2021-07-22	Andrew Reynolds	Miscellaneous changes in preparation for central equality...	commit \| commitdiff \| tree
2021-07-22	Andres Noetzli	Add support for minimal unsat cores (#4605)	commit \| commitdiff \| tree
2021-07-22	Andrew Reynolds	Preparation for carry the rewrite rule database in...	commit \| commitdiff \| tree
2021-07-22	mudathirmahgoub	Add std::vector<Term> Op:: getIndices() and operator...	commit \| commitdiff \| tree
2021-07-20	Haniel Barbosa	[AUTHORS] Add CVC4 as part of CVC series (#6907)	commit \| commitdiff \| tree
2021-07-20	Andres Noetzli	ANTLR3: Install into `CMAKE_INSTALL_LIBDIR` (#6912)	commit \| commitdiff \| tree
2021-07-19	Andrew V. Jones	'CryptoMiniSat_LIBRARIES' should respect lib/lib64...	commit \| commitdiff \| tree
2021-07-19	Andrew V. Jones	'ANTLR3_RUNTIME' should respect lib/lib64 (#6906)	commit \| commitdiff \| tree
2021-07-18	Andrew Reynolds	Add n-ary term utilities (#6896)	commit \| commitdiff \| tree
2021-07-16	Andrew Reynolds	Do not exhaustive instantiation when FMF is disabled...	commit \| commitdiff \| tree
2021-07-16	Andres Noetzli	[Unit Tests] Avoid linking against external libs (...	commit \| commitdiff \| tree
2021-07-16	Andres Noetzli	[Unit Tests] Reenable `top_scope_context_obj` (#6892)	commit \| commitdiff \| tree
2021-07-15	Andrew Reynolds	Fix context for proofs of instantiations (#6890)	commit \| commitdiff \| tree
2021-07-15	Andrew Reynolds	Distinguish quantifiers preprocess as its own proof...	commit \| commitdiff \| tree
2021-07-15	Andrew Reynolds	Connect the equality solver to theory arith (#6894)	commit \| commitdiff \| tree
2021-07-15	Andrew Reynolds	Arithmetic equality solver (#6876)	commit \| commitdiff \| tree
2021-07-15	Andrew Reynolds	Move master equality engine notification to own file...	commit \| commitdiff \| tree
2021-07-15	Andrew Reynolds	Add node converter utility (#6878)	commit \| commitdiff \| tree
2021-07-15	Mathias Preiner	bv: Disable bv-assert-input if proofs are enabled....	commit \| commitdiff \| tree
2021-07-15	Mathias Preiner	bv: Rename BBSimple to NodeBitblaster. (#6891)	commit \| commitdiff \| tree
2021-07-15	Mathias Preiner	bv: Rename lazy solver to layered solver. (#6889)	commit \| commitdiff \| tree
2021-07-15	Mathias Preiner	bv: Rename simple solver to bitblast-internal. (#6888)	commit \| commitdiff \| tree
2021-07-14	Haniel Barbosa	[proof] Fix open proof issues in SAT proof (#6887)	commit \| commitdiff \| tree
2021-07-14	Haniel Barbosa	Add option that exercises the previously buggy behavior...	commit \| commitdiff \| tree
2021-07-14	Haniel Barbosa	Generalize congruence handling for HO in eq proofs...	commit \| commitdiff \| tree
2021-07-14	Andrew Reynolds	Fix for context on input proof generator (#6873)	commit \| commitdiff \| tree
2021-07-14	Andrew Reynolds	Move synthesis verification check to own file (#6882)	commit \| commitdiff \| tree
2021-07-14	Andrew Reynolds	Refactor setup of proof equality engine for central...	commit \| commitdiff \| tree
2021-07-14	Andrew Reynolds	Fix models for sequences of infinite element type ...	commit \| commitdiff \| tree
2021-07-14	Gereon Kremer	Clean up option usage in command executor (#6844)	commit \| commitdiff \| tree
2021-07-14	Mathias Preiner	Add missing space for check macro error messages. ...	commit \| commitdiff \| tree
2021-07-14	Mathias Preiner	bv: Add missing BV_EAGER_ATOM proof rule. (#6874)	commit \| commitdiff \| tree
2021-07-13	Mathias Preiner	bv: Simplify BV_BITBLAST_* proof rules. (#6871)	commit \| commitdiff \| tree
2021-07-13	Haniel Barbosa	[rewriter] Add rewrite to order IFF (equality for Booleans...	commit \| commitdiff \| tree
2021-07-13	Mathias Preiner	bv: Do not rewrite below BV leafs in BBProof's TConvProofGen...	commit \| commitdiff \| tree
2021-07-13	Andrew Reynolds	Add branch and bound lemma if linear arithmetic generates...	commit \| commitdiff \| tree
2021-07-13	Mathias Preiner	bv: Expand bitblast proof steps in the proof post processor...	commit \| commitdiff \| tree
2021-07-12	Andrew Reynolds	Add branch and bound (#6865)	commit \| commitdiff \| tree
2021-07-12	Andrew Reynolds	Fix for learned rewrite pass, add regression (#6850)	commit \| commitdiff \| tree
2021-07-12	Andres Noetzli	Fix ANTLR build on CMake <3.11 (#6864)	commit \| commitdiff \| tree
2021-07-12	Andrew Reynolds	Add arithmetic preprocess rewrite equality module ...	commit \| commitdiff \| tree
2021-07-12	Andrew Reynolds	Add trace for combination splits (#6862)	commit \| commitdiff \| tree
2021-07-12	Andres Noetzli	Use default visibility for `cvc5::Exception` (#6856)	commit \| commitdiff \| tree
2021-07-12	Andrew Reynolds	Improvements to debug check model (#6861)	commit \| commitdiff \| tree
2021-07-09	Haniel Barbosa	test also with default cores (#6858)	commit \| commitdiff \| tree
2021-07-09	Andres Noetzli	Make regression test `issue4971-0` more robust (#6857)	commit \| commitdiff \| tree
2021-07-09	Andres Noetzli	Use newer config.sub to fix build on Apple M1 (#6854)	commit \| commitdiff \| tree
2021-07-09	Andrew Reynolds	Fix sets cardinality inference involving equivalent...	commit \| commitdiff \| tree
2021-07-09	Andrew Reynolds	Implement stop-only for new justification heuristic...	commit \| commitdiff \| tree
2021-07-08	Andrew Reynolds	Disable ordering heuristic for justification by default...	commit \| commitdiff \| tree
2021-07-08	makaimann	Add script to build wheel for pycvc5 (#6839)	commit \| commitdiff \| tree
2021-07-08	Haniel Barbosa	[proof] [dot] Print let map (of terms in proof) as...	commit \| commitdiff \| tree
2021-07-07	Haniel Barbosa	[unsat cores] Adding regressions from #4971 (#6852)	commit \| commitdiff \| tree
2021-07-07	Aina Niemetz	pow2: Update NEWS. (#6851)	commit \| commitdiff \| tree
2021-07-07	Aina Niemetz	Rename operator pow2 to int.pow2. (#6849)	commit \| commitdiff \| tree
2021-07-07	Andrew Reynolds	Fix regressions for competition build (#6846)	commit \| commitdiff \| tree
2021-07-07	Andrew Reynolds	Standard output for trigger selection (#6841)	commit \| commitdiff \| tree
2021-07-06	Gereon Kremer	Integrate Lazard into CAD module (#6812)	commit \| commitdiff \| tree
2021-07-06	Andrew Reynolds	Integrate learned rewrite preprocessing pass (#6840)	commit \| commitdiff \| tree
2021-07-06	Andrew Reynolds	Add implementation of learned rewrite pass (#6843)	commit \| commitdiff \| tree
2021-07-06	Andrew Reynolds	Add learned rewrite preprocessing pass (#6842)	commit \| commitdiff \| tree
2021-07-06	Haniel Barbosa	Porting C++ API examples to SMT-LIB examples (#6789)	commit \| commitdiff \| tree
next

RSS Atom