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

2010-06-29	Tim King	Merging the unate-propagator branch into the trunk...	commit \| commitdiff \| tree
2010-06-24	Tim King	Added post_mortem.py a statistics collector for user...	commit \| commitdiff \| tree
2010-06-22	Tim King	Made ~Stat() virtual. Added some additional statistics...	commit \| commitdiff \| tree
2010-06-18	Tim King	Merging the statistics branch into the main trunk....	commit \| commitdiff \| tree
2010-06-16	Tim King	Added the experimental. +bool TheoryArith::AssertEquality...	commit \| commitdiff \| tree
2010-06-16	Tim King	More assorted changes to arithmetic in preparation...	commit \| commitdiff \| tree
2010-06-16	Tim King	This commit just contains miscellaneous arithmetic...	commit \| commitdiff \| tree
2010-06-15	Tim King	I made a documentation change to get() to make explicit...	commit \| commitdiff \| tree
2010-06-14	Tim King	Fix to arith to make sure it only attempts to report...	commit \| commitdiff \| tree
2010-06-06	Tim King	Some assorted fixes and local optimizations for theory...	commit \| commitdiff \| tree
2010-06-06	Tim King	Adding += and *= to Rational.	commit \| commitdiff \| tree
2010-06-04	Tim King	Changed how assignments are saved during check. These...	commit \| commitdiff \| tree
2010-06-04	Tim King	Changed several arguments to const references.	commit \| commitdiff \| tree
2010-06-03	Tim King	Fixes 2 issues with assignments. The first is constructing...	commit \| commitdiff \| tree
2010-06-03	Tim King	Adds toString to DeltaRational	commit \| commitdiff \| tree
2010-06-03	Tim King	Fixes a bug where registration occurs before preregistration.	commit \| commitdiff \| tree
2010-06-01	Tim King	This commit adds a debugTagIsOn() guard around some...	commit \| commitdiff \| tree
2010-06-01	Tim King	This commit is a fix for a bug in removeITEs(). The...	commit \| commitdiff \| tree
2010-06-01	Tim King	Fixed a bug in partial_model.cpp where the data was...	commit \| commitdiff \| tree
2010-05-29	Tim King	Adding a couple of example from fuzzsmt to regress1.	commit \| commitdiff \| tree
2010-05-29	Tim King	Couple of fixes to theory arith. pivotAndUpdate now...	commit \| commitdiff \| tree
2010-05-29	Tim King	After blasting the disjuncts, TheoryEngine rewrite...	commit \| commitdiff \| tree
2010-05-28	Tim King	This update enables TheoryArith to accept assertions...	commit \| commitdiff \| tree
2010-05-28	Tim King	Bug fixes for combining coefficients of rewritten nodes.	commit \| commitdiff \| tree
2010-05-28	Tim King	Added printModel() to src/theory/arith/partial_model...	commit \| commitdiff \| tree
2010-05-28	Tim King	A few changes to the organization of TheoryEngine rewriting...	commit \| commitdiff \| tree
2010-05-28	Tim King	Moving the ITE removal from CnfStream to TheoryEngine...	commit \| commitdiff \| tree
2010-05-27	Tim King	Reverting this file to not include any comments. (Morgan...	commit \| commitdiff \| tree
2010-05-27	Tim King	Preregistration has been turned on. Highly experimental...	commit \| commitdiff \| tree
2010-05-26	Tim King	. '+Outstanding case split in theory arith'	commit \| commitdiff \| tree
2010-05-26	Tim King	Fix for bug 131. Added some additional debugging assertions...	commit \| commitdiff \| tree
2010-05-25	Tim King	Added Rational constructors that only take a numerator...	commit \| commitdiff \| tree
2010-05-21	Tim King	Small fixes to TheoryArith. Added a hack to make Integers...	commit \| commitdiff \| tree
2010-05-20	Tim King	Added the division symbol to the parser, and minimal...	commit \| commitdiff \| tree
2010-05-19	Tim King	Significant revision to theory/arith. The new draft...	commit \| commitdiff \| tree
2010-04-28	Tim King	Merging the arithmetic theory draft (lra-init) back...	commit \| commitdiff \| tree
2010-04-28	Tim King	Added theory/arith/kind and enabled the smt parser...	commit \| commitdiff \| tree
2010-04-07	Tim King	This update contains more black-box tests as part of...	commit \| commitdiff \| tree
2010-04-02	Tim King	Fixed the 32 bit vs. 64 bit problem in the rational...	commit \| commitdiff \| tree
2010-03-28	Tim King	Improved the documentation and testing for Rational.	commit \| commitdiff \| tree
2010-03-26	Tim King	Added GMP backed Rational and Integer classes, and...	commit \| commitdiff \| tree
2010-03-23	Tim King	Fixed some memory cleanup and destruction issues with...	commit \| commitdiff \| tree
2010-03-11	Tim King	Added some hand generated UF tests. Unfortunartely...	commit \| commitdiff \| tree
2010-03-09	Tim King	Fixed non-debug build problems	commit \| commitdiff \| tree
2010-03-08	Tim King	Improved output for theory uf	commit \| commitdiff \| tree
2010-03-04	Tim King	Committing a bug fix from Dejan. This resolves an issue...	commit \| commitdiff \| tree
2010-03-01	Tim King	Added theory black box test.	commit \| commitdiff \| tree
2010-03-01	Tim King	Node builder tests that targetted properly detecting...	commit \| commitdiff \| tree
2010-03-01	Tim King	Added some documentation to theory_uf.	commit \| commitdiff \| tree
2010-02-28	Tim King	TheoryUFWhite is passing. I fixed 2 errors. Unfortunately...	commit \| commitdiff \| tree
2010-02-26	Tim King	TheoryUFWhite tests are added. There are also accompanying...	commit \| commitdiff \| tree
2010-02-26	Tim King	Fixed a bug in CDList reallocation. (Also corrected...	commit \| commitdiff \| tree
2010-02-25	Tim King	Updated uf to reflect APPLY structure after conversation...	commit \| commitdiff \| tree
2010-02-25	Tim King	Created basic node builder and kind tests. Also fixed...	commit \| commitdiff \| tree
2010-02-24	Tim King	Cleaned up and documented ecdata and theory_uf.	commit \| commitdiff \| tree
2010-02-24	Tim King	Committing small changes to attribute, and theory to...	commit \| commitdiff \| tree
2010-02-17	Tim King	Initial draft of TheoryUF. Should compile without problems...	commit \| commitdiff \| tree
2010-02-04	Tim King	Changed mapping from atoms to literals in the prop...	commit \| commitdiff \| tree
2010-02-04	Tim King	Moved regressions into various levels based on running...	commit \| commitdiff \| tree
2010-02-04	Tim King	Fixes to the cnf converter. Also a barebones utility...	commit \| commitdiff \| tree
2010-02-03	Tim King	By popular demand, I also added a printAst to Expr.	commit \| commitdiff \| tree
2010-02-03	Tim King	I hacked in a temporary way to restart minisat for...	commit \| commitdiff \| tree
2010-02-03	Tim King	Within node I added printAst(..) for general purpose...	commit \| commitdiff \| tree
2010-02-03	Tim King	Enabled more regress tests. Takes 26s on my machine...	commit \| commitdiff \| tree
2010-02-02	Tim King	Switched cnf conversion to go through CnfStream.	commit \| commitdiff \| tree
2010-02-01	Tim King	Added this test back to avoid make check problems.	commit \| commitdiff \| tree
2010-01-30	Tim King	Checking in small test fixes for node_black	commit \| commitdiff \| tree
2010-01-27	Tim King	Added additional tests to node_black.h. CVC4 currently...	commit \| commitdiff \| tree
2010-01-26	Tim King	Undoing stupid commit mistake. Rolling back to -r...	commit \| commitdiff \| tree
2010-01-26	Tim King	Added test/regress/boolean.cvc	commit \| commitdiff \| tree
2010-01-23	Tim King	Added pure PL regression tests. Mostly CNF	commit \| commitdiff \| tree
2010-01-22	Tim King	Added regression test	commit \| commitdiff \| tree
2009-12-16	Tim King	Small refactoring changes for the expr package.	commit \| commitdiff \| tree

RSS Atom