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

2014-06-16	lianah	core solver fix	commit \| commitdiff \| tree
2014-06-16	lianah	fixed bv bug due to applying equisatisfiable transformations...	commit \| commitdiff \| tree
2014-06-15	lianah	fixed fuzzer assertion failures for bv	commit \| commitdiff \| tree
2014-06-15	lianah	added rewriting to bv-pow2 pass	commit \| commitdiff \| tree
2014-06-15	lianah	Evil bitvector preprocessing pass for simplifying powers...	commit \| commitdiff \| tree
2014-06-15	lianah	bv static learning and rewrites for power of 2 terms	commit \| commitdiff \| tree
2014-06-14	lianah	more bv rewrites	commit \| commitdiff \| tree
2014-06-14	lianah	fix to inequality rewrite	commit \| commitdiff \| tree
2014-06-14	lianah	fixed merge	commit \| commitdiff \| tree
2014-06-14	lianah	added bv inequality rewrite	commit \| commitdiff \| tree
2014-06-14	Liana Hadarean	added bv inequality lemmas	commit \| commitdiff \| tree
2014-06-14	Liana Hadarean	added bv inequality lemmas	commit \| commitdiff \| tree
2014-06-13	lianah	fixed BVMinisat bug due to not clearing seen properly	commit \| commitdiff \| tree
2014-06-12	lianah	Merge branch 'master' of https://github.com/CVC4/CVC4	commit \| commitdiff \| tree
2014-06-12	lianah	fixing bv inequality solver explanation bug	commit \| commitdiff \| tree
2014-06-12	lianah	added bvcomp case to bv to bool lifting	commit \| commitdiff \| tree
2014-06-12	lianah	added optionException for trying to use abc in an non...	commit \| commitdiff \| tree
2014-06-11	lianah	Merge branch 'master' of https://github.com/CVC4/CVC4	commit \| commitdiff \| tree
2014-06-11	lianah	switched bv equality order	commit \| commitdiff \| tree
2014-06-11	lianah	fixed unit tests failures	commit \| commitdiff \| tree
2014-06-11	lianah	fixing bv ackermanization cache bug	commit \| commitdiff \| tree
2014-06-10	lianah	reverting portfolio hack	commit \| commitdiff \| tree
2014-06-10	lianah	Merging CAV14 paper bit-vector work.	commit \| commitdiff \| tree
2013-12-03	lianah	fixed rewriter bug where postRewrite was not caching...	commit \| commitdiff \| tree
2013-11-06	lianah	fixed proof regression script and added a new uf test...	commit \| commitdiff \| tree
2013-11-04	lianah	Merge branch 'master' of https://github.com/CVC4/CVC4	commit \| commitdiff \| tree
2013-10-09	lianah	fixed options::proof() segfault	commit \| commitdiff \| tree
2013-10-09	lianah	cleaned up proof code	commit \| commitdiff \| tree
2013-10-09	lianah	fixed uf proof bug: now storing deleted theory lemmas	commit \| commitdiff \| tree
2013-10-08	lianah	added currying for uf proofs; still needs debugging	commit \| commitdiff \| tree
2013-10-08	lianah	fixed uf proof with holes bugs	commit \| commitdiff \| tree
2013-10-08	Liana Hadarean	fixed some bugs	commit \| commitdiff \| tree
2013-10-08	Liana Hadarean	first draft implementation of uf proofs with holes	commit \| commitdiff \| tree
2013-10-07	Liana Hadarean	merged golden	commit \| commitdiff \| tree
2013-09-30	Liana Hadarean	merged golden	commit \| commitdiff \| tree
2013-07-16	Liana Hadarean	fixed seg fault when bv equality is turned off	commit \| commitdiff \| tree
2013-07-16	Liana Hadarean	fixed bug520	commit \| commitdiff \| tree
2013-05-14	lianah	added some extra options to the bit-vector theory	commit \| commitdiff \| tree
2013-05-10	lianah	now proofs print mapping between atom and propositional...	commit \| commitdiff \| tree
2013-05-10	lianah	fixes to the proof system so it works with theory lemmas...	commit \| commitdiff \| tree
2013-05-07	lianah	added type checking rule to check for bit-vector constants...	commit \| commitdiff \| tree
2013-05-07	lianah	one more fix for rewrites	commit \| commitdiff \| tree
2013-05-07	lianah	fixed bv rewrite blow-up	commit \| commitdiff \| tree
2013-05-07	Liana Hadarean	fixed bv rewrite rule bug	commit \| commitdiff \| tree
2013-05-03	lianah	changed the shifting bit-blasting to potentially be...	commit \| commitdiff \| tree
2013-05-02	lianah	merged master	commit \| commitdiff \| tree
2013-05-02	lianah	Merge branch 'master' of https://github.com/CVC4/CVC4	commit \| commitdiff \| tree
2013-05-01	lianah	removed tracing code causing slowdown; cleaned up some...	commit \| commitdiff \| tree
2013-05-01	lianah	added back BitwiseEq rule	commit \| commitdiff \| tree
2013-04-30	lianah	fixed merge conflicts	commit \| commitdiff \| tree
2013-04-30	lianah	merged cvc4 master	commit \| commitdiff \| tree
2013-04-30	lianah	updated the author name	commit \| commitdiff \| tree
2013-04-30	lianah	added several rewrite rules (BitwiseSlicing, Ule/SleEliminat...	commit \| commitdiff \| tree
2013-04-30	lianah	added bvule, bvsle operator elimination rulesl; added...	commit \| commitdiff \| tree
2013-04-30	lianah	added some bv rewrite rules	commit \| commitdiff \| tree
2013-04-30	lianah	innd examples are solved fast, but destruction assertion...	commit \| commitdiff \| tree
2013-04-30	Liana Hadarean	fixed compile error	commit \| commitdiff \| tree
2013-04-30	lianah	uncompiling new bv to bool lifting	commit \| commitdiff \| tree
2013-04-30	lianah	finished implementing bv to bool lifting and added...	commit \| commitdiff \| tree
2013-04-30	Liana Hadarean	more work on boolean lifting	commit \| commitdiff \| tree
2013-04-30	lianah	started work on bv1 to boolean lifting	commit \| commitdiff \| tree
2013-04-30	lianah	added support for dumping the SAT problem the sat solver...	commit \| commitdiff \| tree
2013-04-30	lianah	updated the author name	commit \| commitdiff \| tree
2013-04-30	lianah	added several rewrite rules (BitwiseSlicing, Ule/SleEliminat...	commit \| commitdiff \| tree
2013-04-25	lianah	added bvule, bvsle operator elimination rulesl; added...	commit \| commitdiff \| tree
2013-04-21	lianah	added some bv rewrite rules	commit \| commitdiff \| tree
2013-04-18	lianah	Merge branch 'master' of https://github.com/CVC4/CVC4	commit \| commitdiff \| tree
2013-04-18	lianah	making sure sat context is zero when user context is...	commit \| commitdiff \| tree
2013-04-18	lianah	fixing destruction order in SmtEngine	commit \| commitdiff \| tree
2013-04-17	lianah	innd examples are solved fast, but destruction assertion...	commit \| commitdiff \| tree
2013-04-16	Liana Hadarean	fixed compile error	commit \| commitdiff \| tree
2013-04-16	lianah	uncompiling new bv to bool lifting	commit \| commitdiff \| tree
2013-04-12	lianah	finished implementing bv to bool lifting and added...	commit \| commitdiff \| tree
2013-04-11	lianah	fixed getModelValue to only query the value of leaves...	commit \| commitdiff \| tree
2013-04-10	Liana Hadarean	more work on boolean lifting	commit \| commitdiff \| tree
2013-04-10	lianah	started work on bv1 to boolean lifting	commit \| commitdiff \| tree
2013-04-08	lianah	added support for dumping the SAT problem the sat solver...	commit \| commitdiff \| tree
2013-04-03	Liana Hadarean	updated NEWS to include inequality solver	commit \| commitdiff \| tree
2013-04-01	lianah	fixed TheoryBool rewriter bug	commit \| commitdiff \| tree
2013-04-01	lianah	fixed bug 502; now the core bv solver only gives the...	commit \| commitdiff \| tree
2013-03-31	Liana Hadarean	changed option to run inequality solver by default	commit \| commitdiff \| tree
2013-03-27	lianah	reverted the core solver to do static slicing, added...	commit \| commitdiff \| tree
2013-03-27	lianah	fixed inequality checkDisequalities inefficiency	commit \| commitdiff \| tree
2013-03-27	lianah	Merge branch 'master' into bv-core	commit \| commitdiff \| tree
2013-03-27	lianah	fixed some model stuff	commit \| commitdiff \| tree
2013-03-27	lianah	fixed model generation bug; commented out attempt...	commit \| commitdiff \| tree
2013-03-27	lianah	inequality solver now only splits on disequalities...	commit \| commitdiff \| tree
2013-03-27	lianah	added model generation for bv subtheories and bv-inequality...	commit \| commitdiff \| tree
2013-03-26	lianah	core theory currently disabled	commit \| commitdiff \| tree
2013-03-26	lianah	fixed inequality bugs due to improper explanation	commit \| commitdiff \| tree
2013-03-26	lianah	cleaned up the bv subtheory interface; added check...	commit \| commitdiff \| tree
2013-03-25	lianah	getEqualityStatus now also queries the inequality solver	commit \| commitdiff \| tree
2013-03-25	Liana Hadarean	added support for disequalities in the inequality solver	commit \| commitdiff \| tree
2013-03-24	lianah	incremental inequality solver implemented	commit \| commitdiff \| tree
2013-03-23	lianah	non-incremental inequality solver seems to be bug-free...	commit \| commitdiff \| tree
2013-03-23	lianah	fixed some explanation problems for the core theory...	commit \| commitdiff \| tree
2013-03-22	lianah	Merge branch 'master' into bv-core	commit \| commitdiff \| tree
2013-03-21	lianah	Merge branch 'master' into bv-core	commit \| commitdiff \| tree
2013-03-21	lianah	fixed more equality stuff	commit \| commitdiff \| tree
2013-03-21	lianah	fixed compilation problem	commit \| commitdiff \| tree
next

RSS Atom