summaryrefslogtreecommitdiff
path: root/test/unit
AgeCommit message (Expand)Author
2012-06-06Changes to the combination mechanism, lots of details. Not done yet, there ar...Dejan Jovanović
2012-05-22This commit merges in the branch arithmetic/cprop.Tim King
2012-05-17Fixing an issue with LogicInfo::isPure() that turned off simplification in QF...Morgan Deters
2012-05-15Implement TypeNode::isComparableTo() and add a unit test for it.Morgan Deters
2012-05-15This commit removes the CONST_INTEGER kind from nodes. This code comes from t...Tim King
2012-05-15renamed bv_sat.h, bv_sat.cpp to bitblaster.h, bitblaster.cpp respectivelyLiana Hadarean
2012-05-09* simplifying equality engine interfaceDejan Jovanović
2012-05-08Merging in bvprop branch, with proper bit-vector propagation. Liana Hadarean
2012-05-03Some cleanup starting off from trying to understand the sharing code. Changes...Dejan Jovanović
2012-04-28New LogicInfo functionality.Morgan Deters
2012-04-17Merges branches/arithmetic/atom-database r2979 through 3247 into trunk. Belo...Tim King
2012-04-02Fix for broken unit tests from the previous commit.Tim King
2012-04-02- Merged in the branch cdlist-cleanup.Tim King
2012-03-26More cleaning up.Dejan Jovanović
2012-03-26forgot to commit this one, fixing build errorsDejan Jovanović
2012-03-08Removing QUICK_CHECK, and other unused ones, from the Theory::Effort.Dejan Jovanović
2012-03-02CDMap -> CDHashMapDejan Jovanović
2012-03-01Partial merge from kind-backend branch, including Minisat and CNF work toMorgan Deters
2012-02-25Refactored CnfStream to work with the bv theory Bitblaster:Liana Hadarean
2012-02-22Added OutputChannel::propagateAsDecision() functionality, allowing a theoryMorgan Deters
2012-02-06Fixing a bug in the integer unit tests when configured for GMP with assertion...Tim King
2011-12-06LemmaStatus changes, as agreed to during 12/2 meeting.Morgan Deters
2011-11-16Addressed many of the concerns raised in the public interface review of CVC4 ...Morgan Deters
2011-11-15Bindings work (ocaml bindings are now sort of working); also minor cleanupMorgan Deters
2011-11-14public tests need to be linked against gmp/cln explicitly---looks like a subt...Morgan Deters
2011-10-23Implement changes from yesterday morning's meeting (10/21/2011):Morgan Deters
2011-10-21some printing and parser fixes for problems recently uncoveredMorgan Deters
2011-10-17Sharing workDejan Jovanović
2011-10-13Interruption, time-out, and deterministic time-out ("resource-out") features.Morgan Deters
2011-10-07Some new Datatype public functionality, as per Chris Conway's suggestions on ...Morgan Deters
2011-10-05ensureLiteral() in CNF stream to support Andy's quantifiers work; an update t...Morgan Deters
2011-09-29Some base infrastructure for user push/pop; a few bugfixes to user push/pop a...Morgan Deters
2011-09-15additional stuff for sharing, Dejan Jovanović
2011-09-02Merge from my post-smtcomp branch. Includes:Morgan Deters
2011-08-25Fixing the broken unit testsDejan Jovanović
2011-08-17new implementation of lemmas on demandDejan Jovanović
2011-07-09minor fixupsMorgan Deters
2011-06-30some things I had laying around in a directory but never got committed; minor...Morgan Deters
2011-06-02minor fix to build system for system testsMorgan Deters
2011-06-02added (temporary) support for ensuring that all ambiguously typed constructor...Andrew Reynolds
2011-05-13* fix for Mac OS (includes some ThreadLocal stuff copied in from portfolioMorgan Deters
2011-05-04Stronger support for zero-performance-penalty output, and fixes andMorgan Deters
2011-05-02more minor fixes related to last few commitsMorgan Deters
2011-05-01minor fixes, plus experimental readline support in InteractiveShellMorgan Deters
2011-04-25Monday tasks:Morgan Deters
2011-04-25small unit test fix; was broken only in non-assertion, non-CLN buildsMorgan Deters
2011-04-25Weekend work. The main points:Morgan Deters
2011-04-23fix for parser/tests for ANTLR 3.2 (it was working fine on 3.3)Morgan Deters
2011-04-23* reviewed BooleanSimplification, added documentation & unit testMorgan Deters
2011-04-20numerous bugfixesMorgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback