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

2018-08-30	Andrew Reynolds	Add regular expression elimination module (#2400)	blob \| commitdiff \| raw
2018-08-29	Mathias Preiner	Refactor MipLibTrick preprocessing pass. (#2359)	blob \| commitdiff \| raw \| diff to current
2018-08-28	Andrew Reynolds	Split term canonize utility to own file and document...	blob \| commitdiff \| raw \| diff to current
2018-08-27	Andres Noetzli	Resolution proof: separate printing from proof (#1964)	blob \| commitdiff \| raw \| diff to current
2018-08-26	Andres Noetzli	Refactor unconstrained simplification pass (#2374)	blob \| commitdiff \| raw \| diff to current
2018-08-25	yoni206	Refactor quantifier macros preprocessing pass (#1840)	blob \| commitdiff \| raw \| diff to current
2018-08-25	Haniel Barbosa	Refactor nlExtPurify preprocessing pass (#1963)	blob \| commitdiff \| raw \| diff to current
2018-08-23	Aina Niemetz	Refactor ITE simplification preprocessing pass. (#2360)	blob \| commitdiff \| raw \| diff to current
2018-08-23	yoni206	global-negate preprocessing pass (#2317)	blob \| commitdiff \| raw \| diff to current
2018-08-20	Andrew Reynolds	Make sygus inference a preprocessing pass (#2334)	blob \| commitdiff \| raw \| diff to current
2018-08-17	Mathias Preiner	Refactor eager atoms preprocessing pass. (#2318)	blob \| commitdiff \| raw \| diff to current
2018-08-17	Caleb Donovick	Make quantifiers-preprocess preprocessing pass (#2322)	blob \| commitdiff \| raw \| diff to current
2018-08-17	Andres Noetzli	Refactor IteRemoval preprocessing pass (#1793)	blob \| commitdiff \| raw \| diff to current
2018-08-16	Haniel Barbosa	Refactor extended rewriter preprocessing pass (#2324)	blob \| commitdiff \| raw \| diff to current
2018-08-16	Haniel Barbosa	Refactor apply2const (#2316)	blob \| commitdiff \| raw \| diff to current
2018-08-15	Andrew Reynolds	Make sort inference a preprocessing pass (#2309)	blob \| commitdiff \| raw \| diff to current
2018-08-08	Andrew Reynolds	Document/refactor datatypes sygus simple symmetry break...	blob \| commitdiff \| raw \| diff to current
2018-08-02	Andres Noetzli	Remove Subversion build info (#2250)	blob \| commitdiff \| raw \| diff to current
2018-07-26	Tim King	Removing unused CDTrailHashmap. (#2221)	blob \| commitdiff \| raw \| diff to current
2018-07-17	yoni206	Refactor sep-pre-skolem-emp preprocessing pass	blob \| commitdiff \| raw \| diff to current
2018-07-11	Caleb Donovick	Move rewrite to pass (#2128)	blob \| commitdiff \| raw \| diff to current
2018-07-06	Andrew Reynolds	Split ext theory to own file and document (#1809)	blob \| commitdiff \| raw \| diff to current
2018-07-04	Andrew Reynolds	Reorganize candidate rewrite rule filtering (#2116)	blob \| commitdiff \| raw \| diff to current
2018-07-04	Andres Noetzli	Remove unused CDVector (#2139)	blob \| commitdiff \| raw \| diff to current
2018-07-02	Aina Niemetz	Refactor ApplySubsts preprocessing pass. (#2120)	blob \| commitdiff \| raw \| diff to current
2018-06-29	Aina Niemetz	New C++ API: Implementation of Result. (#2112)	blob \| commitdiff \| raw \| diff to current
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
next

RSS Atom