Context-dependent expr attributes are now attached to a specific SmtEngine, and the...
[cvc5.git] / src / expr / node_manager.cpp
2014-10-14 Morgan DetersContext-dependent expr attributes are now attached...
2014-10-11 Morgan DetersMerge branch '1.4.x'
2014-10-11 Morgan DetersSome defensive programming at destruction time, and...
2014-10-07 Morgan DetersMerge branch '1.4.x'
2014-10-07 Morgan DetersFix a bug in tuple-record handling. Thanks to Saumya...
2014-07-10 Kshitij BansalMerge remote-tracking branch 'origin/master' into segfa...
2014-07-01 Morgan DetersUpdate copyrights.
2014-04-28 Kshitij BansalMerge remote-tracking branch 'upstream/master' into...
2014-04-28 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4
2014-04-28 Kshitij Bansalnodemanager robust skolem numbering
2014-04-28 Kshitij BansalMerge pull request #25 from kbansal/sets
2014-04-28 Kshitij BansalMerge remote-tracking branch 'upstream/master' into...
2014-04-17 Kshitij Bansalsimplify mkSkolem naming system: don't use $$
2013-12-05 Morgan DetersUpdate copyrights, add missing file-level documentation...
2013-11-26 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4
2013-11-25 Tim KingMerge remote-tracking branch 'CVC4root/master'
2013-11-25 Tim KingSubstantial Changes:
2013-11-21 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4
2013-11-21 Tim KingAdding the changes needed to delete rewriter attributes...
2013-11-11 Morgan DetersFlatten libcvc4 build structure; remove some #include...
2013-11-07 Morgan DetersFlatten libcvc4 build structure; remove some #include...
2013-04-02 Morgan DetersRegenerated copyrights: canonicalized names, no emails
2013-04-02 Morgan Detersupdate copyrights
2013-03-13 lianahpost failed attempts at getting the incremental solver...
2013-02-03 Morgan DetersMerge from mdeters/miplib branch (commit 'ce7c485182902...
2013-02-01 Morgan DetersMerge branch '1.0.x'
2013-02-01 Morgan DetersFix a tuple attribute bug that was causing model-genera...
2012-12-01 Morgan DetersFix the way abstract values are typed; fixes some compl...
2012-11-27 Morgan DetersTuples and records merge. Resolves bug 270.
2012-10-11 Morgan DetersStandardizing copyright notice. Touches **ALL** source...
2012-09-28 Morgan Detersrename Assert.h/Assert.cpp to cvc4_assert.h/cvc4_assert...
2012-09-22 Morgan DetersSeparate public-facing and internal-facing interfaces...
2012-09-19 Morgan DetersGeneral subscriber infrastructure for NodeManager,...
2012-07-31 Morgan DetersOptions merge. This commit:
2012-07-08 Morgan DetersBugs resolved by this commit: #314, #322, #359, #364...
2012-03-01 Morgan DetersPartial merge from kind-backend branch, including Minis...
2012-02-23 Morgan DetersAdded ability to set a "cvc4-specific logic" in standar...
2012-02-20 Morgan Detersportfolio merge
2011-11-16 Morgan DetersAddressed many of the concerns raised in the public...
2011-09-02 Morgan DetersMerge from my post-smtcomp branch. Includes:
2011-07-05 Dejan Jovanovićupdated preprocessing and rewriting input equalities...
2011-06-06 Morgan DetersFix for Mac OS breakage (x86 didn't crash, but probably...
2011-06-01 Morgan Deterstype ascriptions (casts) for parameterized datatypes...
2011-04-20 Morgan DetersTuesday end-of-day commit.
2011-04-18 Morgan DetersPartial merge from datatypes-merge branch:
2011-04-15 Morgan Deterspartial merge from portfolio branch, adding conversions...
2011-04-01 Morgan DetersThis commit is a merge from the "betterstats" branch...
2010-12-14 Morgan Deterscongruence closure module now supports things other...
2010-10-29 Morgan Detersminor fixes as a result of review of Chris's getType...
2010-10-28 Christopher L. ConwayChanging NodeBuilder::debugCheckType() to maybeCheckType()
2010-10-28 Christopher L. ConwayDisabling bottom-up algorithm in NodeManager::getType...
2010-10-27 Christopher L. ConwaySmall change to documentation in NodeManager::getType
2010-10-27 Christopher L. ConwaySlightly more efficient version of getType
2010-10-27 Christopher L. ConwayModifying getType to use a non-recursive algorithm...
2010-10-12 Tim KingIDENTITY has been removed.
2010-10-12 Morgan Detersfix some leaks in parser, add debug code to node manage...
2010-10-12 Morgan DetersMerge from cc-memout branch. Here are the main points
2010-10-08 Morgan Deters* (define-fun...) now has proper type checking in non...
2010-10-06 Morgan Detersdeclare-sort, define-sort working but not thoroughly...
2010-10-03 Morgan Detersfile header documentation regenerated with contributors...
2010-09-28 Morgan Detersfix TLS support for platforms (e.g. Mac OS X) where...
2010-09-27 ACSYSadd workaround for systems (i.e., Mac OS X) that don...
2010-09-21 Morgan Detersremove assertion in TNode destructor and ensure all...
2010-09-20 Dejan Jovanovićbitvector rewriting for the core theory and testcases
2010-09-13 Tim King* New normal form for arithmetic is in place.
2010-08-17 Morgan DetersMerge from "cc" branch:
2010-07-27 Christopher L. ConwayAdding optional 'check' parameter to getType() methods
2010-07-02 Morgan Deters* Added white-box TheoryEngine test that tests the...
2010-06-30 Morgan Deters* theory "tree" rewriting implemented and works
2010-06-29 Morgan Deters* Add CDMap<>::insertAtContextLevelZero(k, d) for inser...
2010-06-18 Morgan Detersbug fix (unreported on bugzilla): skolem variables...
2010-06-04 Morgan Deters** Don't fear the files-changed list, almost all change...
2010-05-28 Tim KingMoving the ITE removal from CnfStream to TheoryEngine...
2010-05-27 Morgan Detersfix bug #134: infinite deallocation loop
2010-05-27 Christopher L. ConwayAdding NodeManager::prepareToBeDestroyed() (Fixes:...
2010-05-04 Dejan JovanovićType-checking classes and hooks (not tested yet).
2010-04-14 Dejan JovanovićMarging from types 404:415, changes: Massive
2010-04-05 Christopher L. ConwayAdding black-box tests for NodeManager (Closes bug...
2010-04-05 Christopher L. ConwayTypos and renames for code review
2010-04-04 Morgan Deters* Addressed issues brought up in Chris's review of...
2010-04-01 Morgan Detersreran update-copyright.pl to get new contributors and...
2010-03-30 Morgan DetersHighlights of this commit are:
2010-03-23 Tim KingFixed some memory cleanup and destruction issues with...
2010-03-16 Morgan Deters* test/unit/Makefile.am, test/unit/expr/attribute_white.h,
2010-03-12 Morgan Deters* src/context/cdmap.h: rename orderedIterator to iterat...
2010-03-08 Morgan DetersThis fixes regressions at levels >= 1 which were failing
2010-02-25 Christopher L. ConwayAdding Node::getOperator()
2010-02-25 Morgan Deters* src/expr/node.h: add a copy constructor. Apparently...
2010-02-23 Christopher L. ConwayMinor optimizations to parser (use const string& for...
2010-02-22 Christopher L. ConwaySwitching to types-as-attributes in parser
2010-02-22 Morgan Deters* configure.ac: Remove doc/ from search path for Makefi...
2010-02-19 Morgan Deters* Attribute infrastructure -- static design. Documenta...
2010-02-12 Dejan JovanovićChanges to hashing that solve the xinetd boolean benchm...
2010-02-04 Morgan Detersremove -*- c++ -*- emacs tag from source files (it...
2010-02-04 Morgan Detersminor fix for update-copyright.pl; ran update-copyright...
2010-02-01 Morgan Detersfix node manager code (bugzilla #15, comment #2) in...
2010-01-29 Morgan Detersfixed CNF conversion, and more modular; CNF conversion...
2010-01-26 Morgan Detersfixes to build structure, util classes, lots of fixes...
2009-12-18 Morgan Detersnumerous fixes to nodes; more coming
2009-12-17 Morgan Detersupdate-copyright.pl now retrieves and incorporates...
next