summaryrefslogtreecommitdiff
path: root/src/expr/node.cpp
AgeCommit message (Expand)Author
2018-04-08Check free variables in assertions (#1737)Andrew Reynolds
2018-04-02Do not call toString() on malformed node when throwing TypeCheckingExceptionP...yoni206
2018-01-09Cleaning up throw specifiers on Exception and subclasses. (#1475)Tim King
2017-10-20Make Sygus conjectures higher-order (#1244)Andrew Reynolds
2017-10-09Split term database (#1206)Andrew Reynolds
2017-07-10Separate sygus term utilities to new file, minor cleanup from last commit.ajreynol
2017-07-10Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes ...ajreynol
2017-07-07Update copyright headers.Mathias Preiner
2016-04-20update from the masterPaulMeng
2016-01-05Adding a new class LastExceptionBuffer for the purpose of owning the memory f...Tim King
2015-12-14Refactoring Options Handler & Library Cycle BreakingTim King
2014-07-01Update copyrights.Morgan Deters
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback