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

2012-09-12	Morgan Deters	Adding model assertions after SAT responses.	blob \| commitdiff \| raw
2012-09-11	Tim King	Partially reverting the changes made in 4308. There...	blob \| commitdiff \| raw \| diff to current
2012-09-10	Andrew Reynolds	modified getValue to return Expr instead of Node	blob \| commitdiff \| raw \| diff to current
2012-09-06	Morgan Deters	Remove SmtEngine::getStackLevel(), which exposed implem...	blob \| commitdiff \| raw \| diff to current
2012-08-31	Andrew Reynolds	merge from fmf-devel branch. more updates to models...	blob \| commitdiff \| raw \| diff to current
2012-08-28	Morgan Deters	Improved compatibility layer, now supports quantifiers...	blob \| commitdiff \| raw \| diff to current
2012-08-27	Morgan Deters	fix a destruction-order issue that was (1) causing...	blob \| commitdiff \| raw \| diff to current
2012-08-16	Morgan Deters	The SmtEngine now ensures that setLogicInternal() is...	blob \| commitdiff \| raw \| diff to current
2012-08-08	Morgan Deters	Public interface review items:	blob \| commitdiff \| raw \| diff to current
2012-08-07	Morgan Deters	Fix SmtEngine::setInfo() handling for certain keys...	blob \| commitdiff \| raw \| diff to current
2012-08-06	Morgan Deters	Support setting :regular-output-channel and :diagnostic...	blob \| commitdiff \| raw \| diff to current
2012-08-03	Morgan Deters	fix uses of getMetaKind() from outside the expr package...	blob \| commitdiff \| raw \| diff to current
2012-07-31	Morgan Deters	fixes for portfolio	blob \| commitdiff \| raw \| diff to current
2012-07-31	Morgan Deters	Options merge. This commit:	blob \| commitdiff \| raw \| diff to current
2012-07-17	Morgan Deters	SMT-LIBv2 compliance updates:	blob \| commitdiff \| raw \| diff to current
2012-07-17	Morgan Deters	fix for --produce-models with CVC4 presentation language	blob \| commitdiff \| raw \| diff to current
2012-07-16	Morgan Deters	Support for having two SmtEngines with the same ExprMan...	blob \| commitdiff \| raw \| diff to current
2012-07-12	Andrew Reynolds	merged fmf-devel branch, includes support for SMT2...	blob \| commitdiff \| raw \| diff to current
2012-07-08	Morgan Deters	minor SMT-LIBv2 compliance issues	blob \| commitdiff \| raw \| diff to current
2012-07-08	Morgan Deters	Bugs resolved by this commit: #314, #322, #359, #364...	blob \| commitdiff \| raw \| diff to current
2012-06-18	Kshitij Bansal	bugfix, enable only QF_LRA, not other arith	blob \| commitdiff \| raw \| diff to current
2012-06-18	Kshitij Bansal	QF_LRA, Quantifiers: enable use decision for (only...	blob \| commitdiff \| raw \| diff to current
2012-06-17	Kshitij Bansal	QF_AUFLIA: enable use decision for (only for) stopping...	blob \| commitdiff \| raw \| diff to current
2012-06-17	Dejan Jovanović	enabling theoryof=term for quantifiers with sharing	blob \| commitdiff \| raw \| diff to current
2012-06-17	Clark Barrett	Removed assertion that can fail	blob \| commitdiff \| raw \| diff to current
2012-06-16	Kshitij Bansal	This is an attempt to fix the bug in the justification...	blob \| commitdiff \| raw \| diff to current
2012-06-16	Dejan Jovanović	changing theoryOf in shared mode with arrays to move...	blob \| commitdiff \| raw \| diff to current
2012-06-16	Tim King	Fixing if condition for trivial equalities in arithmeti...	blob \| commitdiff \| raw \| diff to current
2012-06-15	Clark Barrett	Fixes some assertion failures	blob \| commitdiff \| raw \| diff to current
2012-06-15	Clark Barrett	Fix for incompleteness bug with decision engine: repeat...	blob \| commitdiff \| raw \| diff to current
2012-06-15	Kshitij Bansal	one bug fixed	blob \| commitdiff \| raw \| diff to current
2012-06-14	Kshitij Bansal	WIP	blob \| commitdiff \| raw \| diff to current
2012-06-14	Kshitij Bansal	add failing regression, move error up	blob \| commitdiff \| raw \| diff to current
2012-06-14	Clark Barrett	New substitutions implementation - fixes performance...	blob \| commitdiff \| raw \| diff to current
2012-06-14	Clark Barrett	Removed an assertion, unneeded header file	blob \| commitdiff \| raw \| diff to current
2012-06-14	Morgan Deters	some changes to make CVC4 work nicely with trace execut...	blob \| commitdiff \| raw \| diff to current
2012-06-14	Morgan Deters	making --simplification=none the default for quantified...	blob \| commitdiff \| raw \| diff to current
2012-06-14	Kshitij Bansal	bug ifx, mv	blob \| commitdiff \| raw \| diff to current
2012-06-14	Kshitij Bansal	restore destruction of stuff in driver	blob \| commitdiff \| raw \| diff to current
2012-06-14	Kshitij Bansal	This commit:	blob \| commitdiff \| raw \| diff to current
2012-06-14	Tim King	Brings the tuning branch into trunk. This includes...	blob \| commitdiff \| raw \| diff to current
2012-06-12	Clark Barrett	Moved some things around in the preprocessor. Now...	blob \| commitdiff \| raw \| diff to current
2012-06-12	Kshitij Bansal	cleanup of exit mechanism when decisionEngine is on...	blob \| commitdiff \| raw \| diff to current
2012-06-12	Clark Barrett	Fixed compile error	blob \| commitdiff \| raw \| diff to current
2012-06-12	Clark Barrett	Enabling constant propagation	blob \| commitdiff \| raw \| diff to current
2012-06-12	Clark Barrett	Adding constant propagation code - needs more testing...	blob \| commitdiff \| raw \| diff to current
2012-06-09	Clark Barrett	Turning on unconstrained simp for QF_AUFBV	blob \| commitdiff \| raw \| diff to current
2012-06-08	Kshitij Bansal	Merge from decision branch (till r3663)	blob \| commitdiff \| raw \| diff to current
2012-06-07	Morgan Deters	LogicInfo locking implemented, and some initialization...	blob \| commitdiff \| raw \| diff to current
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
next

RSS Atom