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

2012-06-07	Morgan Deters	LogicInfo locking implemented, and some initialization...	blob \| commitdiff \| raw
2012-04-30	Clark Barrett	Added map from skolem variables to new ite formulas...	blob \| commitdiff \| raw \| diff to current
2012-04-17	Kshitij Bansal	A dummy decision engine. Expected performance impact...	blob \| commitdiff \| raw \| diff to current
2012-04-11	Morgan Deters	merge from arrays-clark branch	blob \| commitdiff \| raw \| diff to current
2012-03-01	Morgan Deters	Partial merge from kind-backend branch, including Minis...	blob \| commitdiff \| raw \| diff to current
2012-02-25	Liana Hadarean	Refactored CnfStream to work with the bv theory Bitblaster:	blob \| commitdiff \| raw \| diff to current
2011-11-15	Morgan Deters	Bindings work (ocaml bindings are now sort of working...	blob \| commitdiff \| raw \| diff to current
2011-10-13	Morgan Deters	Interruption, time-out, and deterministic time-out...	blob \| commitdiff \| raw \| diff to current
2011-10-05	Morgan Deters	ensureLiteral() in CNF stream to support Andy's quantif...	blob \| commitdiff \| raw \| diff to current
2011-09-16	Morgan Deters	fix numerous documentation issues; doxygen complains...	blob \| commitdiff \| raw \| diff to current
2011-09-02	Morgan Deters	Merge from my post-smtcomp branch. Includes:	blob \| commitdiff \| raw \| diff to current
2011-08-17	Dejan Jovanović	new implementation of lemmas on demand	blob \| commitdiff \| raw \| diff to current
2011-07-11	Clark Barrett	Clark's work on array theory - can now solve all QF_AX...	blob \| commitdiff \| raw \| diff to current
2011-07-09	Dejan Jovanović	surprize surprize	blob \| commitdiff \| raw \| diff to current
2011-04-01	Morgan Deters	This commit is a merge from the "betterstats" branch...	blob \| commitdiff \| raw \| diff to current
2010-11-15	Tim King	Changes to Solver and PropEngine to support lemmasOnDem...	blob \| commitdiff \| raw \| diff to current
2010-11-15	Tim King	This commit merges the arith-prop-opt branch into the...	blob \| commitdiff \| raw \| diff to current
2010-11-09	Dejan Jovanović	Lemmas on demand work, push-pop, some cleanup.	blob \| commitdiff \| raw \| diff to current
2010-10-22	Christopher L. Conway	Merging main/getopt.cpp, main/usage.h, and smt/options...	blob \| commitdiff \| raw \| diff to current
2010-10-21	Christopher L. Conway	* Option --no-type-checking now disables type checks...	blob \| commitdiff \| raw \| diff to current
2010-10-10	Morgan Deters	additional model gen and SMT-LIBv2 compliance work...	blob \| commitdiff \| raw \| diff to current
2010-10-09	Morgan Deters	Model generation for arith, boolean, and uf theories via	blob \| commitdiff \| raw \| diff to current
2010-06-18	Tim King	Merging the statistics branch into the main trunk....	blob \| commitdiff \| raw \| diff to current
2010-06-04	Morgan Deters	** Don't fear the files-changed list, almost all change...	blob \| commitdiff \| raw \| diff to current
2010-05-25	Dejan Jovanović	Some initial changes to allow for lemmas on demand.	blob \| commitdiff \| raw \| diff to current
2010-05-14	Christopher L. Conway	Adding debugging code in PropEngine/CnfStream	blob \| commitdiff \| raw \| diff to current
2010-04-01	Morgan Deters	PARSER STUFF:	blob \| commitdiff \| raw \| diff to current
2010-03-12	Morgan Deters	* Added shutdown() functions to SmtEngine, TheoryEngine...	blob \| commitdiff \| raw \| diff to current
2010-03-08	Dejan Jovanović	some more sat stuff for tim: assertions now go to theory_uf	blob \| commitdiff \| raw \| diff to current
2010-03-03	Dejan Jovanović	Some SAT stuff, not doing anything special yet, just...	blob \| commitdiff \| raw \| diff to current
2010-02-26	Morgan Deters	* test/unit/context/context_black.h: Test CDList<>...	blob \| commitdiff \| raw \| diff to current
2010-02-25	Morgan Deters	* src/expr/node.h: add a copy constructor. Apparently...	blob \| commitdiff \| raw \| diff to current
2010-02-22	Morgan Deters	* configure.ac: Remove doc/ from search path for Makefi...	blob \| commitdiff \| raw \| diff to current
2010-02-09	Dejan Jovanović	Changes to the CNF conversion and the SAT solver. All...	blob \| commitdiff \| raw \| diff to current
2010-02-04	Dejan Jovanović	beautification of the prop engine	blob \| commitdiff \| raw \| diff to current
2010-02-04	Morgan Deters	remove -- c++ -- emacs tag from source files (it...	blob \| commitdiff \| raw \| diff to current
2010-02-04	Tim King	Changed mapping from atoms to literals in the prop...	blob \| commitdiff \| raw \| diff to current
2010-02-04	Morgan Deters	minor fix for update-copyright.pl; ran update-copyright...	blob \| commitdiff \| raw \| diff to current
2010-02-03	Morgan Deters	Addressed many of the concerns of bug 10 (build system...	blob \| commitdiff \| raw \| diff to current
2010-02-03	Tim King	I hacked in a temporary way to restart minisat for...	blob \| commitdiff \| raw \| diff to current
2010-02-02	Tim King	Switched cnf conversion to go through CnfStream.	blob \| commitdiff \| raw \| diff to current
2010-01-30	Morgan Deters	cnf conversion (variable-introducing), cleanups, fixes...	blob \| commitdiff \| raw \| diff to current
2009-12-17	Morgan Deters	update-copyright.pl now retrieves and incorporates...	blob \| commitdiff \| raw \| diff to current
2009-12-10	Dejan Jovanović	killing expr into node...	blob \| commitdiff \| raw \| diff to current
2009-12-08	Morgan Deters	work on propositional layer, expression builder support...	blob \| commitdiff \| raw \| diff to current
2009-11-24	Morgan Deters	various fixes and updates to use and support parser	blob \| commitdiff \| raw \| diff to current
2009-11-23	Morgan Deters	fixups, file comments	blob \| commitdiff \| raw \| diff to current
2009-11-19	Morgan Deters	testing framework, configure fixes, incorporations...	blob \| commitdiff \| raw \| diff to current
2009-11-17	Morgan Deters	from meeting	blob \| commitdiff \| raw \| diff to current

RSS Atom