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

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
2021-06-30	Gereon Kremer	Use authored date instead of commit date. (#6815)	commit \| commitdiff \| tree
2021-06-30	yoni206	pow2: new test (#6819)	commit \| commitdiff \| tree
2021-06-30	Andrew Reynolds	Do not notify during equality engine initialization... ...an alternative fix to https://github.com/cvc5/cvc5/pull/6808.	commit \| commitdiff \| tree
2021-06-30	Andrew Reynolds	Do not apply fmfBound to standard quantifiers when...	commit \| commitdiff \| tree
2021-06-30	Andrew Reynolds	Fix pre vs. post-rewrite in proofs for theory preprocessor...	commit \| commitdiff \| tree
2021-06-30	yoni206	int-to-bv: correct model values (#6811)	commit \| commitdiff \| tree
2021-06-29	Gereon Kremer	Add new variants for the CAD projection (#6794)	commit \| commitdiff \| tree
2021-06-29	Mathias Preiner	Fix statistics in AigBitblaster. (#6810)	commit \| commitdiff \| tree
2021-06-29	Aina Niemetz	FP: Refactor, rewrite and clean up word blasting. ...	commit \| commitdiff \| tree
2021-06-28	yoni206	Rewrite POW to POW2 when the base is 2 (#6806)	commit \| commitdiff \| tree
2021-06-28	Andrew Reynolds	Rename internal string kinds to match API (#6797)	commit \| commitdiff \| tree
2021-06-28	Ouyancheng	Further fix #6453 (#6804)	commit \| commitdiff \| tree
2021-06-28	Haniel Barbosa	[proof] [dot] Make dot printer stateful (#6799)	commit \| commitdiff \| tree
2021-06-26	yoni206	pow2 -- final changes (#6800)	commit \| commitdiff \| tree
2021-06-25	yoni206	pow2: Adding monotonicity lemma (#6793)	commit \| commitdiff \| tree
2021-06-24	Aina Niemetz	api: getRealValue: Fix printing of integer values....	commit \| commitdiff \| tree
2021-06-24	Mathias Preiner	cmake: Add new code coverage targets. (#6796)	commit \| commitdiff \| tree
2021-06-24	Andrew Reynolds	Fix linear arithmetic for duplicate lemmas in incremental...	commit \| commitdiff \| tree
2021-06-24	Gereon Kremer	Add CoCoA implementation (#6733)	commit \| commitdiff \| tree
2021-06-23	Haniel Barbosa	[hol] Disable bound fmf when HOL (#6792)	commit \| commitdiff \| tree
2021-06-23	yoni206	pow2: more implementations (#6756)	commit \| commitdiff \| tree
2021-06-23	Haniel Barbosa	[regressions] Adding regression from #5371 (#6791)	commit \| commitdiff \| tree
2021-06-23	Haniel Barbosa	[proofs] [dot] Adding a counter for subproofs (#6735)	commit \| commitdiff \| tree
2021-06-23	Haniel Barbosa	[parser] [hol] Fix parser check for allowing functions...	commit \| commitdiff \| tree
2021-06-23	Aina Niemetz	docs: Add quickstart guide. (#6782)	commit \| commitdiff \| tree
2021-06-23	Aina Niemetz	FP: Remove sections guarded with undefined macro SYMFPUPROPI...	commit \| commitdiff \| tree
2021-06-23	Andres Noetzli	Remove `--tear-down-incremental` (#6745)	commit \| commitdiff \| tree
2021-06-22	Andrew Reynolds	Avoid full normalization of lambdas in getValue (#6787)	commit \| commitdiff \| tree
2021-06-22	yoni206	python api unit tests for Op (#6785) ...tests are translated from https://github.com/cvc5/cvc5/blob/master/test... ...function `[getIndices](https://github.com/cvc5/cvc5/blob/master/src... https://github.com/cvc5/cvc5/blob/90d19f7cdbaf41e389bd...	commit \| commitdiff \| tree
2021-06-22	yoni206	modular bv2int: Stubs and some implementations (#6760)	commit \| commitdiff \| tree
2021-06-22	Andrew Reynolds	Minor simplification to equality engine notifications...	commit \| commitdiff \| tree
2021-06-22	Andrew Reynolds	Always check legal eliminations in quantified logics...	commit \| commitdiff \| tree
2021-06-22	Andrew Reynolds	Fix type enumeration for non first-class sorts in FMF...	commit \| commitdiff \| tree
2021-06-22	yoni206	Python api unit tests for Result (#6763) The original cpp file is: https://github.com/cvc5/cvc5/blob/master/test...	commit \| commitdiff \| tree
2021-06-22	Andrew Reynolds	Fix cases of ITE within regular expressions (#6783)	commit \| commitdiff \| tree
2021-06-22	Andrew Reynolds	Set up fine grained equality notifications (#6734)	commit \| commitdiff \| tree
2021-06-21	Mathias Preiner	Update to CaDiCaL 1.4.1. (#6780)	commit \| commitdiff \| tree
2021-06-21	Aina Niemetz	docs: Split out and merge C++ class hierarchy. (#6781)	commit \| commitdiff \| tree
2021-06-21	Andres Noetzli	[Attributes] Remove parameter `context_dependent` ...	commit \| commitdiff \| tree
2021-06-21	Mathias Preiner	Fix model issues with --bitblast=eager. (#6753) ...relevant terms is computed in https://github.com/cvc5/cvc5/blob/master/src...	commit \| commitdiff \| tree
2021-06-21	mudathirmahgoub	Add Grammar.java to the java API (#6388)	commit \| commitdiff \| tree
2021-06-21	Mathias Preiner	Move cnfConversionTime statistic to CnfStream. (#6769)	commit \| commitdiff \| tree
2021-06-21	Mathias Preiner	Make CaDiCaL a required dependency. (#6761)	commit \| commitdiff \| tree
2021-06-21	Haniel Barbosa	[proof] Fix documentation of array rule (#6770)	commit \| commitdiff \| tree
2021-06-19	Ying Sheng	Adding python API test part 5 (#6743)	commit \| commitdiff \| tree
2021-06-19	Aina Niemetz	docs: Fix config to produce unique Sphinx section labels...	commit \| commitdiff \| tree
2021-06-19	Andres Noetzli	[CI] Build with all available cores (#6768)	commit \| commitdiff \| tree
2021-06-19	Aina Niemetz	docs: Remove 'View page source' link in right corner...	commit \| commitdiff \| tree
2021-06-18	Mathias Preiner	Make CnfStream::toCNF iterative (#6757)	commit \| commitdiff \| tree
2021-06-18	Andres Noetzli	Remove obsolete libpoly patch (#6762) https://github.com/SRI-CSL/libpoly/commit/ce7e620c54bd...	commit \| commitdiff \| tree
next

RSS Atom