summaryrefslogtreecommitdiff
path: root/src/expr/node_manager.cpp
AgeCommit message (Expand)Author
2012-11-27Tuples and records merge. Resolves bug 270.Morgan Deters
2012-10-11Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it'sMorgan Deters
2012-09-28rename Assert.h/Assert.cpp to cvc4_assert.h/cvc4_assert.cpp -- we need to mak...Morgan Deters
2012-09-22Separate public-facing and internal-facing interfaces to Statistics.Morgan Deters
2012-09-19General subscriber infrastructure for NodeManager, as discussed in theMorgan Deters
2012-07-31Options merge. This commit:Morgan Deters
2012-07-08Bugs resolved by this commit: #314, #322, #359, #364, #365.Morgan Deters
2012-03-01Partial merge from kind-backend branch, including Minisat and CNF work toMorgan Deters
2012-02-23Added ability to set a "cvc4-specific logic" in standards-compliantMorgan Deters
2012-02-20portfolio mergeMorgan Deters
2011-11-16Addressed many of the concerns raised in the public interface review of CVC4 ...Morgan Deters
2011-09-02Merge from my post-smtcomp branch. Includes:Morgan Deters
2011-07-05updated preprocessing and rewriting input equalities into inequalities for LRADejan Jovanović
2011-06-06Fix for Mac OS breakage (x86 didn't crash, but probably would, eventually, on...Morgan Deters
2011-06-01type ascriptions (casts) for parameterized datatypes, e.g. "nil :: list[INT]Morgan Deters
2011-04-20Tuesday end-of-day commit.Morgan Deters
2011-04-18Partial merge from datatypes-merge branch:Morgan Deters
2011-04-15partial merge from portfolio branch, adding conversions (library-internal-onl...Morgan Deters
2011-04-01This commit is a merge from the "betterstats" branch, which:Morgan Deters
2010-12-14congruence closure module now supports things other than APPLY_UF; ported fro...Morgan Deters
2010-10-29minor fixes as a result of review of Chris's getType() rewrite; also fix some...Morgan Deters
2010-10-28Changing NodeBuilder::debugCheckType() to maybeCheckType()Christopher L. Conway
2010-10-28Disabling bottom-up algorithm in NodeManager::getType() when type checkingChristopher L. Conway
2010-10-27Small change to documentation in NodeManager::getTypeChristopher L. Conway
2010-10-27Slightly more efficient version of getTypeChristopher L. Conway
2010-10-27Modifying getType to use a non-recursive algorithm (Fixes: #228)Christopher L. Conway
2010-10-12IDENTITY has been removed.Tim King
2010-10-12fix some leaks in parser, add debug code to node manager to find moreMorgan Deters
2010-10-12Merge from cc-memout branch. Here are the main pointsMorgan Deters
2010-10-08* (define-fun...) now has proper type checking in non-debug buildsMorgan Deters
2010-10-06declare-sort, define-sort working but not thoroughly tested; define-fun half ...Morgan Deters
2010-10-03file header documentation regenerated with contributors names; no code modifi...Morgan Deters
2010-09-28fix TLS support for platforms (e.g. Mac OS X) where __thread storage class do...Morgan Deters
2010-09-27add workaround for systems (i.e., Mac OS X) that don't support __thread; also...ACSYS
2010-09-21remove assertion in TNode destructor and ensure all TNode methods check rc > ...Morgan Deters
2010-09-20bitvector rewriting for the core theory and testcasesDejan Jovanović
2010-09-13* New normal form for arithmetic is in place.Tim King
2010-08-17Merge from "cc" branch:Morgan Deters
2010-07-27Adding optional 'check' parameter to getType() methodsChristopher L. Conway
2010-07-02* Added white-box TheoryEngine test that tests the rewriterMorgan Deters
2010-06-30* theory "tree" rewriting implemented and worksMorgan Deters
2010-06-29* Add CDMap<>::insertAtContextLevelZero(k, d) for inserting "initializing"Morgan Deters
2010-06-18bug fix (unreported on bugzilla): skolem variables failing removal from poolMorgan Deters
2010-06-04** Don't fear the files-changed list, almost all changes are in the **Morgan Deters
2010-05-28Moving the ITE removal from CnfStream to TheoryEngine, which is a bit closer ...Tim King
2010-05-27fix bug #134: infinite deallocation loopMorgan Deters
2010-05-27Adding NodeManager::prepareToBeDestroyed() (Fixes: #128)Christopher L. Conway
2010-05-04Type-checking classes and hooks (not tested yet).Dejan Jovanović
2010-04-14Marging from types 404:415, changes: MassiveDejan Jovanović
2010-04-05Adding black-box tests for NodeManager (Closes bug #65)Christopher L. Conway
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback