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

2012-06-07	Morgan Deters	LogicInfo locking implemented, and some initialization...	blob \| commitdiff \| raw
2012-06-06	Clark Barrett	Don't ever call nonclausalSimplify if simplificationMod...	blob \| commitdiff \| raw \| diff to current
2012-06-06	Morgan Deters	removing std::cout from trunk	blob \| commitdiff \| raw \| diff to current
2012-06-04	Clark Barrett	Added preprocessing pass that propagates unconstrained...	blob \| commitdiff \| raw \| diff to current
2012-06-01	Morgan Deters	add a global user-context push/pop in smt engine, just...	blob \| commitdiff \| raw \| diff to current
2012-05-31	Clark Barrett	Fixed bug in bv: one more case where non-shared equalit...	blob \| commitdiff \| raw \| diff to current
2012-05-30	Clark Barrett	Added BitwiseEq bitvector rewrite	blob \| commitdiff \| raw \| diff to current
2012-05-15	Tim King	This commit removes the CONST_INTEGER kind from nodes...	blob \| commitdiff \| raw \| diff to current
2012-05-14	Dejan Jovanović	fixes for shared term registration. previously the...	blob \| commitdiff \| raw \| diff to current
2012-05-13	Dejan Jovanović	fixing build warnings	blob \| commitdiff \| raw \| diff to current
2012-05-11	Clark Barrett	Disabled arith-rewrite-equalities by default unless...	blob \| commitdiff \| raw \| diff to current
2012-05-11	Clark Barrett	Added some ITE rewrites,	blob \| commitdiff \| raw \| diff to current
2012-05-09	Dejan Jovanović	* simplifying equality engine interface	blob \| commitdiff \| raw \| diff to current
2012-05-09	Kshitij Bansal	Merge from decision branch (ITE support)	blob \| commitdiff \| raw \| diff to current
2012-04-30	Clark Barrett	Added map from skolem variables to new ite formulas...	blob \| commitdiff \| raw \| diff to current
2012-04-28	Morgan Deters	New LogicInfo functionality.	blob \| commitdiff \| raw \| diff to current
2012-04-23	Kshitij Bansal	Merge from decision branch -- partially working justifi...	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-17	Tim King	Merges branches/arithmetic/atom-database r2979 through...	blob \| commitdiff \| raw \| diff to current
2012-04-11	Morgan Deters	merge from arrays-clark branch	blob \| commitdiff \| raw \| diff to current
2012-04-06	Morgan Deters	* Fix ITEs and functions in CVC language printer.	blob \| commitdiff \| raw \| diff to current
2012-04-02	Kshitij Bansal	fix for cvc4_logic dump	blob \| commitdiff \| raw \| diff to current
2012-03-22	Liana Hadarean	Merged updated version of the bitvector theory:	blob \| commitdiff \| raw \| diff to current
2012-03-21	Morgan Deters	Disable nonclausal simplification for QF_SAT benchmarks...	blob \| commitdiff \| raw \| diff to current
2012-03-09	Morgan Deters	Some work on the dump infrastructure to support portfol...	blob \| commitdiff \| raw \| diff to current
2012-03-02	Dejan Jovanović	CDMap -> CDHashMap	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-28	Morgan Deters	Replace the sequence of hardcoded addTheory() calls...	blob \| commitdiff \| raw \| diff to current
2012-02-24	Dejan Jovanović	Theory interface changes:	blob \| commitdiff \| raw \| diff to current
2012-02-23	Morgan Deters	Added ability to set a "cvc4-specific logic" in standar...	blob \| commitdiff \| raw \| diff to current
2012-02-20	Morgan Deters	Added Theory::postsolve() infrastructure as Clark reque...	blob \| commitdiff \| raw \| diff to current
2012-02-20	Morgan Deters	By default, ONLY enable symmetry breaker ONLY for QF_UF...	blob \| commitdiff \| raw \| diff to current
2011-10-29	Morgan Deters	Support for SMT-LIBv2 (get-proof), CVC-style DUMP_PROOF...	blob \| commitdiff \| raw \| diff to current
2011-10-28	Liana Hadarean	merged the proofgen3 branch into trunk:	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-03	Morgan Deters	user push/pop support in minisat and simplification...	blob \| commitdiff \| raw \| diff to current
2011-09-30	Morgan Deters	fixes to incremental simplification, cnf routines,...	blob \| commitdiff \| raw \| diff to current
2011-09-29	Morgan Deters	Some base infrastructure for user push/pop; a few bugfi...	blob \| commitdiff \| raw \| diff to current
2011-09-16	Morgan Deters	dump define-funs correctly with "--dump declarations...	blob \| commitdiff \| raw \| diff to current
2011-09-15	Dejan Jovanović	additional stuff for sharing,	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-09-02	Morgan Deters	Partial merge of integers work; this is simple B&B...	blob \| commitdiff \| raw \| diff to current
2011-08-24	Dejan Jovanović	Simplification of the preregister and register throught...	blob \| commitdiff \| raw \| diff to current
2011-07-11	Morgan Deters	merge from symmetry branch	blob \| commitdiff \| raw \| diff to current
2011-07-09	Dejan Jovanović	surprize surprize	blob \| commitdiff \| raw \| diff to current
2011-07-05	Dejan Jovanović	updated preprocessing and rewriting input equalities...	blob \| commitdiff \| raw \| diff to current
2011-05-23	Morgan Deters	fixes for "make dist" and "make doc", minor cleanups	blob \| commitdiff \| raw \| diff to current
2011-05-23	Morgan Deters	Merge from arrays2 branch.	blob \| commitdiff \| raw \| diff to current
2011-05-05	Morgan Deters	Merge from nonclausal-simplification-v2 branch:	blob \| commitdiff \| raw \| diff to current
2011-05-02	Morgan Deters	fix a performance issue from last commit	blob \| commitdiff \| raw \| diff to current
2011-05-02	Morgan Deters	Minor fixes to various parts of CVC4, including the...	blob \| commitdiff \| raw \| diff to current
2011-04-25	Morgan Deters	Monday tasks:	blob \| commitdiff \| raw \| diff to current
2011-04-22	Morgan Deters	fix to last commit	blob \| commitdiff \| raw \| diff to current
2011-04-22	Morgan Deters	Fixing SmtEngine::getValue() by adding a NodeManagerSco...	blob \| commitdiff \| raw \| diff to current
2011-04-20	Morgan Deters	Minor mixed-bag commit. Expected performance impact...	blob \| commitdiff \| raw \| diff to current
2011-04-18	Morgan Deters	Partial merge from datatypes-merge branch:	blob \| commitdiff \| raw \| diff to current
2011-04-13	Morgan Deters	cache the LET rewriting (and defined-function expansion...	blob \| commitdiff \| raw \| diff to current
2011-04-04	Tim King	Merging the satliteral-before-prereg branch into trunk...	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
2011-03-15	Morgan Deters	Merge from cudd branch. This mostly just adds support...	blob \| commitdiff \| raw \| diff to current
2011-01-05	Dejan Jovanović	Commit for the theory engine and rewriter changes....	blob \| commitdiff \| raw \| diff to current
2010-11-19	Morgan Deters	Merge from ufprop branch, including:	blob \| commitdiff \| raw \| diff to current
2010-11-16	Morgan Deters	SmtEngine now fails with a ModalException if --incremen...	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-11-08	Morgan Deters	command-line flag to disable theory registration, also...	blob \| commitdiff \| raw \| diff to current
2010-11-08	Morgan Deters	cleanup, documentation, SMT-LIBv2 compliance	blob \| commitdiff \| raw \| diff to current
2010-10-31	Morgan Deters	enable dependence graphs in doxygen; fix lots of doxyge...	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-22	Morgan Deters	comment out the "interactive" check in SmtEngine::getVa...	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-12	Morgan Deters	hooked up "we are incomplete" flag after conversation...	blob \| commitdiff \| raw \| diff to current
2010-10-12	Morgan Deters	Merge from cc-memout branch. Here are the main points	blob \| commitdiff \| raw \| diff to current
2010-10-12	Morgan Deters	check last result in (get-assignment); some context...	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	support for SMT-LIBv2 :named attributes, and attributes...	blob \| commitdiff \| raw \| diff to current
2010-10-09	Morgan Deters	bug fixes to model gen	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-10-08	Morgan Deters	* (define-fun...) now has proper type checking in non...	blob \| commitdiff \| raw \| diff to current
2010-10-08	Morgan Deters	support (set-info) on status, source, category, difficu...	blob \| commitdiff \| raw \| diff to current
2010-10-07	Morgan Deters	type checking for define-fun in production builds;...	blob \| commitdiff \| raw \| diff to current
2010-10-07	Morgan Deters	SMT-LIBv2 (define-fun...) command now functional; does...	blob \| commitdiff \| raw \| diff to current
2010-10-06	Morgan Deters	declare-sort, define-sort working but not thoroughly...	blob \| commitdiff \| raw \| diff to current
2010-10-05	Morgan Deters	parser and core support for SMT-LIBv2 commands get...	blob \| commitdiff \| raw \| diff to current
2010-09-24	Dejan Jovanović	equality triggers for the equality engine	blob \| commitdiff \| raw \| diff to current
2010-08-17	Morgan Deters	Merge from "cc" branch:	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-03-16	Morgan Deters	* test/unit/Makefile.am, test/unit/expr/attribute_white.h,	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-11	Morgan Deters	naive rewriting to fix minisat invariant; rewrite ...	blob \| commitdiff \| raw \| diff to current
2010-03-08	Morgan Deters	This fixes regressions at levels >= 1 which were failing	blob \| commitdiff \| raw \| diff to current
2010-03-05	Morgan Deters	* public/private code untangled (smt/smt_engine.h no...	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-25	Morgan Deters	* src/expr/node.h: add a copy constructor. Apparently...	blob \| commitdiff \| raw \| diff to current
2010-02-23	Dejan Jovanović	cosmetic changes, comments, and renaming of Expr relate...	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-22	Dejan Jovanović	Small changes to the smt-engine, removed the assertions...	blob \| commitdiff \| raw \| diff to current
2010-02-19	Morgan Deters	* Attribute infrastructure -- static design. Documenta...	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-09	Dejan Jovanović	empty stubs for push and pop to fix the build fail	blob \| commitdiff \| raw \| diff to current
next

RSS Atom