summaryrefslogtreecommitdiff
path: root/src/expr/node.cpp
AgeCommit message (Expand)Author
2014-03-07Remove --ite-remove-quant; support pulling ground ITEs out of quantifier bodi...Morgan Deters
2013-12-05Update copyrights, add missing file-level documentation; fix perms.Morgan Deters
2013-11-25Substantial Changes:Tim King
2013-11-10Flatten libcvc4 build structure; remove some #include interdependencesMorgan Deters
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2012-12-01fix memory corruption issue in debug builds that led to unhelpful outputMorgan Deters
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-10-10Abstract values for SMT-LIB.Morgan Deters
2012-03-01Partial merge from kind-backend branch, including Minisat and CNF work toMorgan Deters
2011-11-22More language bindings work:Morgan Deters
2011-04-20Minor mixed-bag commit. Expected performance impact negligible.Morgan Deters
2011-03-25This is a merge from the "theoryfixes+cdattrhash" branch. The changesMorgan Deters
2010-10-31enable dependence graphs in doxygen; fix lots of doxygen warnings, fix some d...Morgan Deters
2010-10-06declare-sort, define-sort working but not thoroughly tested; define-fun half ...Morgan Deters
2010-06-30* theory "tree" rewriting implemented and worksMorgan Deters
2010-06-04** Don't fear the files-changed list, almost all changes are in the **Morgan Deters
2010-05-04Type-checking classes and hooks (not tested yet).Dejan Jovanović
2010-03-30Highlights of this commit are:Morgan Deters
2010-02-26TheoryUFWhite tests are added. There are also accompanying bug fixes. These c...Tim King
2010-02-25* src/expr/node_builder.h: fixed some overly-aggressive refcount decrementing.Morgan Deters
2010-02-22finally worksDejan Jovanović
2010-02-22Merging from branch branches/Liana r241Dejan Jovanović
2010-02-22Switching to types-as-attributes in parserChristopher L. Conway
2010-02-22* configure.ac: Remove doc/ from search path for Makefile.amsMorgan Deters
2010-02-22Re-committing revision 232 properly:Morgan Deters
2010-02-22undoing improperly-committed revision 232; will re-commit to get "svn blame" ...Morgan Deters
2010-02-22* Add virtual destructors to CnfStream, Theory, OutputChannel, andCesare Tinelli
2010-02-22fix bug 22 (remove tracing from non-trace builds; remove all outputMorgan Deters
2010-02-12Changes to hashing that solve the xinetd boolean benchmark in 14s (from ~25mi...Dejan Jovanović
2010-02-04beautification of the prop engineDejan Jovanović
2010-02-04remove -*- c++ -*- emacs tag from source files (it overrides cvc4-c++-editing...Morgan Deters
2010-02-04minor fix for update-copyright.pl; ran update-copyright.pl on all sources; re...Morgan Deters
2010-02-04Fixes to the cnf converter. Also a barebones utility for printing out a satis...Tim King
2010-02-03simple ITE parsingDejan Jovanović
2010-02-03Within node I added printAst(..) for general purpose debugging use throughout...Tim King
2009-12-18numerous fixes to nodes; more comingMorgan Deters
2009-12-17update-copyright.pl now retrieves and incorporates author information from re...Morgan Deters
2009-12-17+ test infrastructure fixesMorgan Deters
2009-12-16+ refactoring fixes for expr package based on code review (see bug #4)Morgan Deters
2009-12-16Small refactoring changes for the expr package.Tim King
2009-12-16Fixes to the build system:Morgan Deters
2009-12-11Extracted the public Expr and ExprManager interface to encapsulate the optimi...Dejan Jovanović
2009-12-10killing expr into node...Dejan Jovanović
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback