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

2018-05-22	Andrew Reynolds	Make sygus infer find function definitions (#1951)	blob \| commitdiff \| raw
2018-05-16	yoni206	Refactor static learning preprocessing pass (#1857)	blob \| commitdiff \| raw \| diff to current
2018-05-15	Andrew Reynolds	Minor improvements to --nl-ext-purify (#1896)	blob \| commitdiff \| raw \| diff to current
2018-05-11	Aina Niemetz	Fix ackermannize preprocessing pass. (#1904)	blob \| commitdiff \| raw \| diff to current
2018-05-10	Andrew Reynolds	Sygus repair constants (#1812)	blob \| commitdiff \| raw \| diff to current
2018-05-10	Aina Niemetz	Refactored BVAckermann preprocessing pass. (#1889)	blob \| commitdiff \| raw \| diff to current
2018-05-09	Andrew Reynolds	Better option names for PBE (#1891)	blob \| commitdiff \| raw \| diff to current
2018-05-09	Andrew Reynolds	Make symmetry-breaker-exp into a preprocessing pass...	blob \| commitdiff \| raw \| diff to current
2018-05-09	PaulMeng	Add the symmetry breaker module (#1847)	blob \| commitdiff \| raw \| diff to current
2018-05-08	Mathias Preiner	Refactor bv-abstraction preprocessing pass. (#1860)	blob \| commitdiff \| raw \| diff to current
2018-05-08	Andrew Reynolds	Infrastructure for approximations in model output ...	blob \| commitdiff \| raw \| diff to current
2018-05-08	Aina Niemetz	Fix order of preprocessing pass registration. (#1887)	blob \| commitdiff \| raw \| diff to current
2018-05-04	Mathias Preiner	Refactor bv-intro-pow2 preprocessing pass. (#1851)	blob \| commitdiff \| raw \| diff to current
2018-05-03	Mathias Preiner	Fix redundant internalPush calls. (#1865)	blob \| commitdiff \| raw \| diff to current
2018-05-03	Andrew Reynolds	Option to interleave tangent plane inferences (#1833)	blob \| commitdiff \| raw \| diff to current
2018-05-03	Andrew Reynolds	Initial support for string standard in smt lib 2.6...	blob \| commitdiff \| raw \| diff to current
2018-04-30	Haniel Barbosa	Refactor real2int (#1813)	blob \| commitdiff \| raw \| diff to current
2018-04-30	Andrew Reynolds	Remove subsort symmetry breaking (#1807)	blob \| commitdiff \| raw \| diff to current
2018-04-25	yoni206	Refactor bv-to-bool and bool-to-bv preprocessing passes...	blob \| commitdiff \| raw \| diff to current
2018-04-25	Andrew Reynolds	Add benchmark requiring subgoal generation with inducti...	blob \| commitdiff \| raw \| diff to current
2018-04-20	yoni206	Enforcing --no-bv-eq, --no-bv-algebraic and --no-bv...	blob \| commitdiff \| raw \| diff to current
2018-04-20	PaulMeng	Symmetry detection module (#1749)	blob \| commitdiff \| raw \| diff to current
2018-04-19	Andres Noetzli	Refactor pbRewrites preprocessing pass (#1767)	blob \| commitdiff \| raw \| diff to current
2018-04-14	yoni206	allowing --bool-to-bv without quantifiers (#1771)	blob \| commitdiff \| raw \| diff to current
2018-04-11	Aina Niemetz	Refactored BVGauss preprocessing pass. (#1766)	blob \| commitdiff \| raw \| diff to current
2018-04-10	Andrew Reynolds	Improve accuracy of stats for sygus sampler (#1755)	blob \| commitdiff \| raw \| diff to current
2018-04-10	Aina Niemetz	Fix dumping of benchmark in SmtEngine::checkSatisfiabil...	blob \| commitdiff \| raw \| diff to current
2018-04-05	Mathias Preiner	Add more general SignExtendUltConst rewriting. (#1385)	blob \| commitdiff \| raw \| diff to current
2018-04-04	Andres Noetzli	Refactor IntToBV preprocessing pass (#1716)	blob \| commitdiff \| raw \| diff to current
2018-04-04	Andrew Reynolds	Option to turn arbitrary input into sygus (#1704)	blob \| commitdiff \| raw \| diff to current
2018-04-02	Clark Barrett	Remove references to nyu (#1721)	blob \| commitdiff \| raw \| diff to current
2018-03-26	Andrew Reynolds	Check model only when sat (#1694)	blob \| commitdiff \| raw \| diff to current
2018-03-09	Aina Niemetz	Add support for SMT-LIB v2.5 command get-unsat-assumpti...	blob \| commitdiff \| raw \| diff to current
2018-03-07	Mathias Preiner	Make statistics output consistent. (#1647)	blob \| commitdiff \| raw \| diff to current
2018-03-05	Mathias Preiner	Enable -Wsuggest-override by default. (#1643)	blob \| commitdiff \| raw \| diff to current
2018-03-05	Aina Niemetz	Add support for check-sat-assuming. (#1637)	blob \| commitdiff \| raw \| diff to current
2018-02-28	Aina Niemetz	SmtEngine::getAssignment now returns a vector of assign...	blob \| commitdiff \| raw \| diff to current
2018-02-14	Andrew Reynolds	Quantifiers subdirectories (#1608)	blob \| commitdiff \| raw \| diff to current
2018-02-13	Andrew Reynolds	Option to use extended rewriter as a preprocessing...	blob \| commitdiff \| raw \| diff to current
2018-02-08	Andrew Reynolds	Minor improvements to sygus sampling. (#1577)	blob \| commitdiff \| raw \| diff to current
2018-02-02	Haniel Barbosa	Option to check solutions produced by SyGuS solver...	blob \| commitdiff \| raw \| diff to current
2018-02-01	Andrew Reynolds	Use sygus to synthesize/verify rewrite rules (#1547)	blob \| commitdiff \| raw \| diff to current
2018-01-25	Tim King	Commenting out throw specifiers on SmtEngine. These...	blob \| commitdiff \| raw \| diff to current
2018-01-22	Andrew Reynolds	Only push/pop around check-sat if it is associated...	blob \| commitdiff \| raw \| diff to current
2018-01-09	Aina Niemetz	Reorganized bitvector.h. (#1505)	blob \| commitdiff \| raw \| diff to current
2018-01-03	Andrew Reynolds	Global negate (#1466)	blob \| commitdiff \| raw \| diff to current
2017-12-27	Andrew Reynolds	Disable sygus PBE when sygus stream is enabled (#1451)	blob \| commitdiff \| raw \| diff to current
2017-12-21	Andrew Reynolds	Fixes for cbqi-bv (#1449)	blob \| commitdiff \| raw \| diff to current
2017-12-11	justinxu421	Add new infrastructure for preprocessing passes (#1053)	blob \| commitdiff \| raw \| diff to current
2017-12-07	Andrew Reynolds	Fixes related to SyGuS + real arithmetic (#1432)	blob \| commitdiff \| raw \| diff to current
2017-12-07	Andrew Reynolds	Add command for define-fun-rec and add to API (#1412)	blob \| commitdiff \| raw \| diff to current
2017-12-01	Andres Noetzli	Fix reset-assertions (#1413)	blob \| commitdiff \| raw \| diff to current
2017-11-30	Aina Niemetz	Add Gaussian Elimination as a preprocessing pass for...	blob \| commitdiff \| raw \| diff to current
2017-11-30	Andrew Reynolds	Minor improvements and changes to defaults for cbqi...	blob \| commitdiff \| raw \| diff to current
2017-11-28	Andrew Reynolds	Fix models for --solve-real-as-int. (#1371)	blob \| commitdiff \| raw \| diff to current
2017-11-17	Andrew Reynolds	(Refactor) Document and clean single invocation partiti...	blob \| commitdiff \| raw \| diff to current
2017-11-17	Aina Niemetz	Add random number generator. (#1370)	blob \| commitdiff \| raw \| diff to current
2017-11-16	Andrew Reynolds	(Refactor) Arithmetic monomial sum (#1381)	blob \| commitdiff \| raw \| diff to current
2017-11-15	Tim King	Adding garbage collection for Proof objects. (#1294)	blob \| commitdiff \| raw \| diff to current
2017-11-13	Andrew Reynolds	Disable sygus qe preprocessing by default (#1353)	blob \| commitdiff \| raw \| diff to current
2017-11-09	Andrew Reynolds	Higher-order prep (#1338)	blob \| commitdiff \| raw \| diff to current
2017-11-07	Andrew Reynolds	Allow FORALL in quantifier elimination command (#1322)	blob \| commitdiff \| raw \| diff to current
2017-11-03	Andrew Reynolds	Sygus clean main (#1297)	blob \| commitdiff \| raw \| diff to current
2017-10-28	Andres Noetzli	Change bvudiv semantics based on input language (#1292)	blob \| commitdiff \| raw \| diff to current
2017-10-24	Aina Niemetz	CBQI BV: Add ULT/SLT inverse handling. (#1268)	blob \| commitdiff \| raw \| diff to current
2017-10-20	Andrew Reynolds	Make Sygus conjectures higher-order (#1244)	blob \| commitdiff \| raw \| diff to current
2017-10-17	Clark Barrett	Fix for issue 1247 (#1257)	blob \| commitdiff \| raw \| diff to current
2017-10-11	Andrew Reynolds	Ho Lambda Lifting (#1116)	blob \| commitdiff \| raw \| diff to current
2017-10-11	Andrew Reynolds	Move unsat core names to smt engine (#1192)	blob \| commitdiff \| raw \| diff to current
2017-10-10	Andrew Reynolds	Split term database (#1206)	blob \| commitdiff \| raw \| diff to current
2017-09-19	Andres Noetzli	Fix issue #1074, improve non-fatal error handling ...	blob \| commitdiff \| raw \| diff to current
2017-09-14	Tim King	Simplifying the throw specifier of SmtEngine::checkSat...	blob \| commitdiff \| raw \| diff to current
2017-09-14	Martin	Floating point symfpu support (#1093)	blob \| commitdiff \| raw \| diff to current
2017-09-10	Andrew Reynolds	Ensure that expand definitions is called on all non...	blob \| commitdiff \| raw \| diff to current
2017-08-24	Andrew Reynolds	Merge pull request #191 from timothy-king/cleanup-regexp	blob \| commitdiff \| raw \| diff to current
2017-08-24	Andres Noetzli	Fix typos	blob \| commitdiff \| raw \| diff to current
2017-08-07	ajreynol	Make quantifier elimination more robust to preprocessing.	blob \| commitdiff \| raw \| diff to current
2017-07-21	Tim King	Merge branch 'master' into cleanup-regexp	blob \| commitdiff \| raw \| diff to current
2017-07-21	Tim King	Moving from the gnu extensions for hash maps to the...	blob \| commitdiff \| raw \| diff to current
2017-07-20	Tim King	Removing the unused CDAttribute. This makes CDHashMap...	blob \| commitdiff \| raw \| diff to current
2017-07-13	Aina Niemetz	Merge pull request #188 from aniemetz/cx11	blob \| commitdiff \| raw \| diff to current
2017-07-12	ajreynol	Make type rules more strict for operators whose type...	blob \| commitdiff \| raw \| diff to current
2017-07-10	ajreynol	Do not exit when value/model/unsat-core/proof is reques...	blob \| commitdiff \| raw \| diff to current
2017-07-10	ajreynol	Merge datatype shared selectors/sygus comp 2017 branch...	blob \| commitdiff \| raw \| diff to current
2017-07-07	Mathias Preiner	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2017-05-31	ajreynol	Fix model construction for BV with cbqi. Minor change...	blob \| commitdiff \| raw \| diff to current
2017-05-31	ajreynol	Minor change to defaults, update smt comp script, minor...	blob \| commitdiff \| raw \| diff to current
2017-05-12	Andres Notzli	Make signal handlers safer	blob \| commitdiff \| raw \| diff to current
2017-05-05	ajreynol	Do not eliminate extended arithmetic symbols when finit...	blob \| commitdiff \| raw \| diff to current
2017-05-04	guykatzz	fixing bug 790: track dependencies when the unsatCores...	blob \| commitdiff \| raw \| diff to current
2017-04-22	Clark Barrett	Merge pull request #151 from 4tXJ7f/fix_debug	blob \| commitdiff \| raw \| diff to current
2017-04-21	Andres Noetzli	Move assertion out of loop for better performance	blob \| commitdiff \| raw \| diff to current
2017-04-20	Andrew Reynolds	Merge pull request #149 from PaulMeng/master	blob \| commitdiff \| raw \| diff to current
2017-04-20	ajreynol	Minor fixes.	blob \| commitdiff \| raw \| diff to current
2017-04-14	ajreynol	Fix for fmf-fun when the option is set by user command.	blob \| commitdiff \| raw \| diff to current
2017-04-12	ajreynol	Add nullary operator metakind.	blob \| commitdiff \| raw \| diff to current
2017-04-07	ajreynol	Change option names for nl.	blob \| commitdiff \| raw \| diff to current
2017-04-04	Clark Barrett	Merge pull request #141 from 4tXJ7f/remove_def	blob \| commitdiff \| raw \| diff to current
2017-04-03	Andrew Reynolds	Merge pull request #142 from timothy-king/nlAlgMerge	blob \| commitdiff \| raw \| diff to current
2017-04-03	Tim King	Adding a model based axiom instantiation scheme for...	blob \| commitdiff \| raw \| diff to current
next

RSS Atom