summaryrefslogtreecommitdiff
path: root/src/expr/expr_template.cpp
AgeCommit message (Expand)Author
2012-10-11Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it'sMorgan Deters
2012-10-05BoolExpr removed and replaced with ExprDejan Jovanović
2012-09-28Some fixes to portfolioKshitij Bansal
2012-09-28rename Assert.h/Assert.cpp to cvc4_assert.h/cvc4_assert.cpp -- we need to mak...Morgan Deters
2012-09-24some api changesDejan Jovanović
2012-09-19General subscriber infrastructure for NodeManager, as discussed in theMorgan Deters
2012-09-08Some minor changes after reviewing the portfolio "unified driver" commit.Morgan Deters
2012-09-08Single driver for both sequential and portfolioKshitij Bansal
2012-08-29* Numerous documentation fixes (fix doxygen warnings, add missing documentati...Morgan Deters
2012-08-28Improved compatibility layer, now supports quantifiers. Also incorporatesMorgan Deters
2012-08-24fix get-value output in a couple ways; this fixes bug #378Morgan Deters
2012-08-03fix uses of getMetaKind() from outside the expr package. (they now use isCon...Morgan Deters
2012-06-09Dagification of output expressions.Morgan Deters
2012-03-01Partial merge from kind-backend branch, including Minisat and CNF work toMorgan Deters
2012-02-20portfolio mergeMorgan Deters
2011-12-14minor fixes to printing and parsing of CVC-language defined functions and lam...Morgan Deters
2011-11-22More language bindings work:Morgan Deters
2011-09-02Merge from my post-smtcomp branch. Includes:Morgan Deters
2011-06-03datatypes workMorgan Deters
2011-05-02Minor fixes to various parts of CVC4, including the removal of the uintptr_t ...Morgan Deters
2011-04-23* reviewed BooleanSimplification, added documentation & unit testMorgan Deters
2011-04-20Minor mixed-bag commit. Expected performance impact negligible.Morgan Deters
2011-04-20Tuesday end-of-day commit.Morgan Deters
2011-03-25This is a merge from the "theoryfixes+cdattrhash" branch. The changesMorgan Deters
2010-10-08* (define-fun...) now has proper type checking in non-debug buildsMorgan Deters
2010-10-07SMT-LIBv2 (define-fun...) command now functional; does eager expansion at pre...Morgan Deters
2010-10-06declare-sort, define-sort working but not thoroughly tested; define-fun half ...Morgan Deters
2010-10-05parser and core support for SMT-LIBv2 commands get-info, set-option, get-opti...Morgan Deters
2010-10-04remove/shuffle some #include dependencies; fix some documentation; apply codi...Morgan Deters
2010-07-27Adding optional 'check' parameter to getType() methodsChristopher L. Conway
2010-07-10add >, <=, and >= comparisons for Exprs and NodesMorgan Deters
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-04** Don't fear the files-changed list, almost all changes are in the **Morgan Deters
2010-05-31First draft implementation of mkAssociativeChristopher L. Conway
2010-05-27Remove isAtomic() as per 4/27/2010 meeting. Add comments about its potential...Morgan Deters
2010-05-05bug fixes for types, old unit tests for types work nowDejan Jovanović
2010-05-04Type-checking classes and hooks (not tested yet).Dejan Jovanović
2010-04-14Marging from types 404:415, changes: MassiveDejan Jovanović
2010-04-04Recommit revision 365 (undoing revision 375, which reverted revision 365).Morgan Deters
2010-04-03Reverting r365Christopher L. Conway
2010-04-01Removing Expr::operator=(uintptr_t n), as it's no longer used by the parser.Christopher L. Conway
2010-04-01reran update-copyright.pl to get new contributors and add new header comments...Morgan Deters
2010-04-01* Minor code formatting stuff in src/expr/type.{h,cpp}. ConcludedMorgan Deters
2010-04-01PARSER STUFF:Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback