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

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) This PR moves https://github.com/cvc5/cvc5/blob/master/src...	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 ... This PR moves the method https://github.com/ajreynol/CVC4/blob/master...	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
2021-07-06	Ouyancheng	Add some printing functions for OptimizationObjective...	commit \| commitdiff \| tree
2021-07-06	Gereon Kremer	Add doc page about transcendentals (#6755)	commit \| commitdiff \| tree
2021-07-05	Andres Noetzli	[Strings] Fix incorrect rewrite (#6837)	commit \| commitdiff \| tree
2021-07-05	Andrew Reynolds	Make buffered inference manager more robust to backtracking...	commit \| commitdiff \| tree
2021-07-03	Andres Noetzli	Fix performance of string regression (#6832)	commit \| commitdiff \| tree
2021-07-03	Mathias Preiner	Add output tags -o, --output. (#6826)	commit \| commitdiff \| tree
2021-07-02	Mathias Preiner	Fix bv assert input reset assertions (#6820)	commit \| commitdiff \| tree
2021-07-02	Andrew Reynolds	Fix rewriter for negative constant seq.nth (#6827)	commit \| commitdiff \| tree
2021-07-02	Andres Noetzli	Fix CaDiCaL auto-download on macOS (#6828) [1] https://github.com/Kitware/CMake/blob/d60d6c269ae7ad15...	commit \| commitdiff \| tree
2021-07-02	Gereon Kremer	Refactor lexer for SMT-LIB in sphinx (#6805)	commit \| commitdiff \| tree
2021-07-02	Andres Noetzli	Add reverse iterators to `Node`/`TNode` (#6825)	commit \| commitdiff \| tree
2021-07-01	Andrew Reynolds	Add recursive function definitions to subsolver in...	commit \| commitdiff \| tree
2021-07-01	Gereon Kremer	Fix message to show that cadical and symfpu are required...	commit \| commitdiff \| tree
2021-07-01	Andrew Reynolds	Add option to limit the number of instantiation rounds...	commit \| commitdiff \| tree
2021-06-30	Mathias Preiner	Use SAT context level for --bv-assert-input instead...	commit \| commitdiff \| tree
next

RSS Atom