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

2018-06-29	Aina Niemetz	New C++ API: Implementation of Result. (#2112)	blob \| commitdiff \| raw
2018-06-28	Andrew Reynolds	Split and document ceg theory instantiators (#2094)	blob \| commitdiff \| raw \| diff to current
2018-06-27	Andrew Reynolds	Synthesize candidate-rewrites from standard inputs...	blob \| commitdiff \| raw \| diff to current
2018-06-26	Andres Noetzli	sygusComp2018: Add evaluator (#2090)	blob \| commitdiff \| raw \| diff to current
2018-06-20	Andres Noetzli	Resolve CVC4_USE_SYMFPU in headers at config-time ...	blob \| commitdiff \| raw \| diff to current
2018-05-21	Andrew Reynolds	Refactor sygus eval unfold (#1946)	blob \| commitdiff \| raw \| diff to current
2018-05-16	yoni206	Refactor static learning preprocessing pass (#1857)	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	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-04	Mathias Preiner	Refactor bv-intro-pow2 preprocessing pass. (#1851)	blob \| commitdiff \| raw \| diff to current
2018-05-04	Haniel Barbosa	Move Lazy trie datastructure to its own file (#1871)	blob \| commitdiff \| raw \| diff to current
2018-05-03	Andres Noetzli	Remove (dummy) SMT1 printer (#1854)	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-27	Haniel Barbosa	New module for synthesizing functions in a data-driven...	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	Move candidate rewrite code to own file (#1804)	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-11	Aina Niemetz	Refactored BVGauss preprocessing pass. (#1766)	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-03	Andrew Reynolds	Make sygus unif I/O an subclass of sygus unif (#1741)	blob \| commitdiff \| raw \| diff to current
2018-04-02	Mathias Preiner	Reorganize bitblaster code. (#1695)	blob \| commitdiff \| raw \| diff to current
2018-03-30	Andrew Reynolds	Split strategy representation from SygusUnif (#1730)	blob \| commitdiff \| raw \| diff to current
2018-03-27	Andrew Reynolds	Make sygus unif utility (#1720)	blob \| commitdiff \| raw \| diff to current
2018-03-23	Andrew Reynolds	Remove unused code (#1700)	blob \| commitdiff \| raw \| diff to current
2018-03-23	Andrew Reynolds	Minor reorganization for ematching (#1701)	blob \| commitdiff \| raw \| diff to current
2018-03-20	Mathias Preiner	Add support for CaDiCaL as eager BV SAT solver. (#1675)	blob \| commitdiff \| raw \| diff to current
2018-03-02	Andrew Reynolds	Create infrastructure for sygus modules (#1632)	blob \| commitdiff \| raw \| diff to current
2018-02-14	Andrew Reynolds	Quantifiers subdirectories (#1608)	blob \| commitdiff \| raw \| diff to current
2018-02-14	Andres Noetzli	Remove unused cd_set_collection.h (#1606)	blob \| commitdiff \| raw \| diff to current
2018-02-09	Andrew Reynolds	Class to reduce printing of redundant candidate rewrite...	blob \| commitdiff \| raw \| diff to current
2018-02-06	Andrew Reynolds	Statically eliminate redundant sygus constructors ...	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-03	Andrew Reynolds	Global negate (#1466)	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-08	Andrew Reynolds	Document and clean datatypes rewriter (#1437)	blob \| commitdiff \| raw \| diff to current
2017-12-06	Andres Noetzli	Remove CDChunkList (#1414)	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-25	Andrew Reynolds	(Refactor) Instantiate utility (#1387)	blob \| commitdiff \| raw \| diff to current
2017-11-22	Andrew Reynolds	Sygus Lambda Grammars (#1390)	blob \| commitdiff \| raw \| diff to current
2017-11-21	Haniel Barbosa	Adding infrastructure for normalizing SyGuS grammars...	blob \| commitdiff \| raw \| diff to current
2017-11-19	Andrew Reynolds	Ho instantiation (#1204)	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-16	Andrew Reynolds	(Refactor) Arithmetic monomial sum (#1381)	blob \| commitdiff \| raw \| diff to current
2017-11-14	Andrew Reynolds	(Refactor) Split sygus term db (#1335)	blob \| commitdiff \| raw \| diff to current
2017-11-13	Andrew Reynolds	Implement enumerator for functions. (#1243)	blob \| commitdiff \| raw \| diff to current
2017-11-02	Andrew Reynolds	(Move-only) Split quant util (#1306)	blob \| commitdiff \| raw \| diff to current
2017-11-01	Andrew Reynolds	(Refactor) Split term util (#1303)	blob \| commitdiff \| raw \| diff to current
2017-11-01	Andrew Reynolds	(Move-only) Refactor and document theory model part...	blob \| commitdiff \| raw \| diff to current
2017-10-28	Andrew Reynolds	(Move only) Move enumerative instantiation strategy...	blob \| commitdiff \| raw \| diff to current
2017-10-28	Andrew Reynolds	Sygus process conjecture (#1286)	blob \| commitdiff \| raw \| diff to current
2017-10-27	Andres Noetzli	Modify LDFLAGS to support shared libraries for Win...	blob \| commitdiff \| raw \| diff to current
2017-10-24	Andrew Reynolds	Removing deprecated file. (#1270)	blob \| commitdiff \| raw \| diff to current
2017-10-10	Martin	Add skeleton of the FP theory solver (#1130)	blob \| commitdiff \| raw \| diff to current
2017-10-10	Andrew Reynolds	Split term database (#1206)	blob \| commitdiff \| raw \| diff to current
2017-10-03	Andrew Reynolds	Move sygus grammar utilities to separate file. (#1184)	blob \| commitdiff \| raw \| diff to current
2017-09-30	Andrew Reynolds	SyGuS streaming solution mode (#1131)	blob \| commitdiff \| raw \| diff to current
2017-09-29	Mathias Preiner	Move BvInverter class into separate file. (#1173)	blob \| commitdiff \| raw \| diff to current
2017-09-20	Martin	Add FP type enumerator and cardinality computer (#1104)	blob \| commitdiff \| raw \| diff to current
2017-08-31	Andres Noetzli	Use thread_local instead of compiler extensions (#210)	blob \| commitdiff \| raw \| diff to current
2017-08-25	Aina Niemetz	Move LFSC checker out of the CVC repository. (#222)	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-14	Aina Niemetz	Merge pull request #214 from CVC4/fix_warn_nonlinear	blob \| commitdiff \| raw \| diff to current
2017-08-14	Mark Laws	Build and test suite fixes for Windows (#186)	blob \| commitdiff \| raw \| diff to current
2017-07-10	ajreynol	Separate sygus term utilities to new file, minor cleanu...	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-08	Mathias Preiner	Merge branch 'master' of github.com:CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2017-07-07	Andres Noetzli	Remove unused stacking_vector class (#185)	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
2017-03-27	Clark Barrett	Merge pull request #137 from 4tXJ7f/throw_quals	blob \| commitdiff \| raw \| diff to current
2017-03-27	Tim King	Moving the CareGraph into its own file.	blob \| commitdiff \| raw \| diff to current
2017-03-27	Tim King	Moving the theory::Assertion struct into its own file.	blob \| commitdiff \| raw \| diff to current
2017-03-27	Tim King	Alphabetizing libcvc4_la_SOURCES.	blob \| commitdiff \| raw \| diff to current
2017-03-17	guykatzz	better support for proof production when encountering...	blob \| commitdiff \| raw \| diff to current
2017-03-02	ajreynol	Minor cleanup and reorganization related to last commit.	blob \| commitdiff \| raw \| diff to current
2016-10-27	Clark Barrett	Merge pull request #99 from 4tXJ7f/fix_dist_build3	blob \| commitdiff \| raw \| diff to current
2016-10-27	Andres Notzli	Fix typo in Makefile that makes distcheck fail	blob \| commitdiff \| raw \| diff to current
2016-10-26	Andrew Reynolds	Merge pull request #98 from 4tXJ7f/fix_dist_build	blob \| commitdiff \| raw \| diff to current
2016-10-26	ajreynol	New implementation of sets+cardinality. Merge Paul...	blob \| commitdiff \| raw \| diff to current
2016-10-13	Tim King	Revert "Merge branch 'origin' of https://github.com...	blob \| commitdiff \| raw \| diff to current
2016-10-11	Paul Meng	Merge branch 'origin' of https://github.com/CVC4/CVC4.git	blob \| commitdiff \| raw \| diff to current
2016-10-01	Tim King	Merge pull request #93 from timothy-king/clang-format	blob \| commitdiff \| raw \| diff to current
2016-09-20	ajreynol	Refactor, separate theory-specific counterexample-guide...	blob \| commitdiff \| raw \| diff to current
2016-08-24	PaulMeng	Merge remote-tracking branch 'origin/master'	blob \| commitdiff \| raw \| diff to current
2016-07-05	PaulMeng	Merge branch 'master' of https://github.com/CVC4/CVC4.git	blob \| commitdiff \| raw \| diff to current
2016-06-30	Guy	Merge branch 'master' of https://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2016-06-23	Clark Barrett	Add theory/sep/kinds to EXTRA_DIST to fix distcheck...	blob \| commitdiff \| raw \| diff to current
2016-06-20	Guy	Merge branch 'master' of https://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2016-06-17	ajreynol	Support for separation logic. Enable cbqi by default...	blob \| commitdiff \| raw \| diff to current
2016-06-06	guykatzz	Merge pull request #85 from CVC4/master_for_proof_merge	blob \| commitdiff \| raw \| diff to current
2016-06-02	Guy	Merge from proof branch	blob \| commitdiff \| raw \| diff to current
2016-06-02	Guy	Revert "Merging proof branch"	blob \| commitdiff \| raw \| diff to current
2016-06-02	Guy	Merging proof branch	blob \| commitdiff \| raw \| diff to current
2016-05-25	Liana Hadarean	Merged cryptominisat from experimental branch.	blob \| commitdiff \| raw \| diff to current
next

RSS Atom