2013-09-09 |
Morgan Deters | Support empty (and 1-ary) tuples and records. |
blob | commitdiff | raw |
2013-09-05 |
Morgan Deters | Fix declare-fun/define-fun in dumps; resolves bugs... |
blob | commitdiff | raw | diff to current |
2013-08-26 |
Kshitij Bansal | Merge branch '1.2.x' |
blob | commitdiff | raw | diff to current |
2013-07-11 |
Morgan Deters | Support for TPTP's TFF0 (with arithmetic) |
blob | commitdiff | raw | diff to current |
2013-04-02 |
Morgan Deters | Regenerated copyrights: canonicalized names, no emails |
blob | commitdiff | raw | diff to current |
2013-04-02 |
Morgan Deters | update copyrights |
blob | commitdiff | raw | diff to current |
2012-12-01 |
Morgan Deters | Fix the way abstract values are typed; fixes some compl... |
blob | commitdiff | raw | diff to current |
2012-11-29 |
Kshitij Bansal | Hack to support global variables for CVC language exten... |
blob | commitdiff | raw | diff to current |
2012-11-27 |
Morgan Deters | First chunk of boolean-terms support. |
blob | commitdiff | raw | diff to current |
2012-11-27 |
Morgan Deters | Tuples and records merge. Resolves bug 270. |
blob | commitdiff | raw | diff to current |
2012-10-11 |
Morgan Deters | Standardizing copyright notice. Touches **ALL** source... |
blob | commitdiff | raw | diff to current |
2012-10-11 |
Morgan Deters | Fix wording on GPL in legal notices; also remove an... |
blob | commitdiff | raw | diff to current |
2012-09-26 |
Morgan Deters | The Tuesday Afternoon Catch-All Commit (TACAC): |
blob | commitdiff | raw | diff to current |
2012-09-24 |
Dejan Jovanović | some api changes |
blob | commitdiff | raw | diff to current |
2012-09-19 |
Morgan Deters | General subscriber infrastructure for NodeManager,... |
blob | commitdiff | raw | diff to current |
2012-08-24 |
Morgan Deters | * disallow internal uses of mkVar() (you have to mkSkol... |
blob | commitdiff | raw | diff to current |
2012-08-24 |
Morgan Deters | fix get-value output in a couple ways; this fixes bug... |
blob | commitdiff | raw | diff to current |
2012-08-13 |
Morgan Deters | Minor cleanup. No performance difference expected. |
blob | commitdiff | raw | diff to current |
2012-08-07 |
Morgan Deters | Some items from the CVC4 public interface review: |
blob | commitdiff | raw | diff to current |
2012-08-03 |
Morgan Deters | fix uses of getMetaKind() from outside the expr package... |
blob | commitdiff | raw | diff to current |
2012-07-31 |
Morgan Deters | Options merge. This commit: |
blob | commitdiff | raw | diff to current |
2012-07-16 |
Morgan Deters | Support for having two SmtEngines with the same ExprMan... |
blob | commitdiff | raw | diff to current |
2012-07-07 |
Morgan Deters | Various fixes to documentation---typos, some incomplete... |
blob | commitdiff | raw | diff to current |
2012-06-12 |
Morgan Deters | minor cleanup, and replace a "private:" in equality... |
blob | commitdiff | raw | diff to current |
2012-06-11 |
Morgan Deters | Merge from quantifiers2-trunkmerge branch. |
blob | commitdiff | raw | diff to current |
2012-05-18 |
Tim King | This commit adds TypeNode::leastCommonTypeNode(). ... |
blob | commitdiff | raw | diff to current |
2012-05-18 |
Tim King | This commit removes the dead psuedoboolean code. |
blob | commitdiff | raw | diff to current |
2012-05-11 |
Morgan Deters | output a warning message when a function type (or datat... |
blob | commitdiff | raw | diff to current |
2012-04-18 |
Dejan Jovanović | disabling the problematic pragma in node_manager.h... |
blob | commitdiff | raw | diff to current |
2012-04-17 |
Dejan Jovanović | Fix for thos annoying "array index" warnings in product... |
blob | commitdiff | raw | diff to current |
2012-03-01 |
Morgan Deters | Partial merge from kind-backend branch, including Minis... |
blob | commitdiff | raw | diff to current |
2012-02-23 |
Morgan Deters | Added ability to set a "cvc4-specific logic" in standar... |
blob | commitdiff | raw | diff to current |
2012-02-20 |
Morgan Deters | portfolio merge |
blob | commitdiff | raw | diff to current |
2011-11-16 |
Morgan Deters | Addressed many of the concerns raised in the public... |
blob | commitdiff | raw | diff to current |
2011-11-04 |
Morgan Deters | STRING_TYPE and CONST_STRING and associate type infrast... |
blob | commitdiff | raw | diff to current |
2011-10-13 |
Morgan Deters | Interruption, time-out, and deterministic time-out... |
blob | commitdiff | raw | diff to current |
2011-09-02 |
Morgan Deters | Merge from my post-smtcomp branch. Includes: |
blob | commitdiff | raw | diff to current |
2011-09-02 |
Morgan Deters | Partial merge of integers work; this is simple B&B... |
blob | commitdiff | raw | diff to current |
2011-06-30 |
Morgan Deters | only use theory registration if (1) a theory requests... |
blob | commitdiff | raw | diff to current |
2011-06-06 |
Morgan Deters | Fix for Mac OS breakage (x86 didn't crash, but probably... |
blob | commitdiff | raw | diff to current |
2011-05-14 |
Morgan Deters | reverting node manager change from 1881; also part... |
blob | commitdiff | raw | diff to current |
2011-05-13 |
Andrew Reynolds | added support for parametric datatypes, updated cvc... |
blob | commitdiff | raw | diff to current |
2011-04-20 |
Morgan Deters | Tuesday end-of-day commit. |
blob | commitdiff | raw | diff to current |
2011-04-18 |
Morgan Deters | mostly CVC presentation language parsing and printing |
blob | commitdiff | raw | diff to current |
2011-04-18 |
Morgan Deters | Partial merge from datatypes-merge branch: |
blob | commitdiff | raw | diff to current |
2011-04-15 |
Morgan Deters | partial merge from portfolio branch, adding conversions... |
blob | commitdiff | raw | diff to current |
2011-04-01 |
Morgan Deters | This commit is a merge from the "betterstats" branch... |
blob | commitdiff | raw | diff to current |
2011-03-25 |
Morgan Deters | This is a merge from the "theoryfixes+cdattrhash" branc... |
blob | commitdiff | raw | diff to current |
2011-01-05 |
Dejan Jovanović | Commit for the theory engine and rewriter changes.... |
blob | commitdiff | raw | diff to current |
2010-12-14 |
Morgan Deters | congruence closure module now supports things other... |
blob | commitdiff | raw | diff to current |
2010-10-28 |
Christopher L. Conway | Changing NodeBuilder::debugCheckType() to maybeCheckType() |
blob | commitdiff | raw | diff to current |
2010-10-27 |
Christopher L. Conway | Modifying getType to use a non-recursive algorithm... |
blob | commitdiff | raw | diff to current |
2010-10-24 |
Morgan Deters | add a CVC4_UNDEFINED keyword, for intentionally undefin... |
blob | commitdiff | raw | diff to current |
2010-10-22 |
Morgan Deters | comment out the "interactive" check in SmtEngine::getVa... |
blob | commitdiff | raw | diff to current |
2010-10-08 |
Morgan Deters | * (define-fun...) now has proper type checking in non... |
blob | commitdiff | raw | diff to current |
2010-10-07 |
Morgan Deters | type checking for define-fun in production builds;... |
blob | commitdiff | raw | diff to current |
2010-10-06 |
Morgan Deters | declare-sort, define-sort working but not thoroughly... |
blob | commitdiff | raw | diff to current |
2010-10-05 |
Morgan Deters | parser and core support for SMT-LIBv2 commands get... |
blob | commitdiff | raw | diff to current |
2010-10-03 |
Morgan Deters | file header documentation regenerated with contributors... |
blob | commitdiff | raw | diff to current |
2010-09-28 |
Morgan Deters | fix TLS support for platforms (e.g. Mac OS X) where... |
blob | commitdiff | raw | diff to current |
2010-09-27 |
ACSYS | add workaround for systems (i.e., Mac OS X) that don... |
blob | commitdiff | raw | diff to current |
2010-09-21 |
Morgan Deters | remove assertion in TNode destructor and ensure all... |
blob | commitdiff | raw | diff to current |
2010-09-21 |
Christopher L. Conway | Moving automatic type check to NodeBuilder (Fixes:... |
blob | commitdiff | raw | diff to current |
2010-09-20 |
Dejan Jovanović | bitvector rewriting for the core theory and testcases |
blob | commitdiff | raw | diff to current |
2010-08-17 |
Morgan Deters | Merge from "cc" branch: |
blob | commitdiff | raw | diff to current |
2010-07-29 |
Christopher L. Conway | Adding configuration_private.h to allow inlining of... |
blob | commitdiff | raw | diff to current |
2010-07-28 |
Christopher L. Conway | Forcing a type check on Node construction in debug... |
blob | commitdiff | raw | diff to current |
2010-07-27 |
Christopher L. Conway | Adding optional 'check' parameter to getType() methods |
blob | commitdiff | raw | diff to current |
2010-07-06 |
Morgan Deters | Don't eagerly collect zombies. This should speed up... |
blob | commitdiff | raw | diff to current |
2010-07-02 |
Morgan Deters | * Added white-box TheoryEngine test that tests the... |
blob | commitdiff | raw | diff to current |
2010-06-30 |
Morgan Deters | * theory "tree" rewriting implemented and works |
blob | commitdiff | raw | diff to current |
2010-06-16 |
Tim King | This commit just contains miscellaneous arithmetic... |
blob | commitdiff | raw | diff to current |
2010-06-04 |
Morgan Deters | ** Don't fear the files-changed list, almost all change... |
blob | commitdiff | raw | diff to current |
2010-05-31 |
Christopher L. Conway | First draft implementation of mkAssociative |
blob | commitdiff | raw | diff to current |
2010-05-27 |
Morgan Deters | fix bug #134: infinite deallocation loop |
blob | commitdiff | raw | diff to current |
2010-05-27 |
Morgan Deters | Remove isAtomic() as per 4/27/2010 meeting. Add commen... |
blob | commitdiff | raw | diff to current |
2010-05-27 |
Christopher L. Conway | Adding NodeManager::prepareToBeDestroyed() (Fixes:... |
blob | commitdiff | raw | diff to current |
2010-05-13 |
Christopher L. Conway | Minor refactorings and corrections to comments |
blob | commitdiff | raw | diff to current |
2010-05-04 |
Dejan Jovanović | Type-checking classes and hooks (not tested yet). |
blob | commitdiff | raw | diff to current |
2010-05-02 |
Dejan Jovanović | smt parser for bit-vectors |
blob | commitdiff | raw | diff to current |
2010-05-01 |
Dejan Jovanović | Fix for the last night's build errors (type that broke... |
blob | commitdiff | raw | diff to current |
2010-04-30 |
Dejan Jovanović | Fix for bug 115, mapping was going in the wrong direction. |
blob | commitdiff | raw | diff to current |
2010-04-29 |
Dejan Jovanović | Added the capability to construct expressions by passin... |
blob | commitdiff | raw | diff to current |
2010-04-26 |
Dejan Jovanović | Some cleanup. Also added the integer and real types. |
blob | commitdiff | raw | diff to current |
2010-04-26 |
Dejan Jovanović | Adding the intermediary TypeNode to represent (and... |
blob | commitdiff | raw | diff to current |
2010-04-15 |
Christopher L. Conway | Enhancements to NodeManager tests, taking advantage... |
blob | commitdiff | raw | diff to current |
2010-04-14 |
Dejan Jovanović | Marging from types 404:415, changes: Massive |
blob | commitdiff | raw | diff to current |
2010-04-13 |
Christopher L. Conway | Doxygen fixes |
blob | commitdiff | raw | diff to current |
2010-04-06 |
Morgan Deters | * Add some protected ContextObj accessors for ContextOb... |
blob | commitdiff | raw | diff to current |
2010-04-05 |
Christopher L. Conway | Adding black-box tests for NodeManager (Closes bug... |
blob | commitdiff | raw | diff to current |
2010-04-05 |
Christopher L. Conway | Minor refactorings, in response to code review (Bug... |
blob | commitdiff | raw | diff to current |
2010-04-05 |
Christopher L. Conway | Typos and renames for code review |
blob | commitdiff | raw | diff to current |
2010-04-04 |
Morgan Deters | * Addressed issues brought up in Chris's review of... |
blob | commitdiff | raw | diff to current |
2010-04-04 |
Morgan Deters | * Node::isAtomic() now looks at an "atomic" attribute... |
blob | commitdiff | raw | diff to current |
2010-04-01 |
Morgan Deters | reran update-copyright.pl to get new contributors and... |
blob | commitdiff | raw | diff to current |
2010-04-01 |
Morgan Deters | PARSER STUFF: |
blob | commitdiff | raw | diff to current |
2010-03-31 |
Christopher L. Conway | Finishing parser cleanup. Code is now review-ready. |
blob | commitdiff | raw | diff to current |
2010-03-30 |
Morgan Deters | I think this finishes off the CDMap<>/Attribute leaks |
blob | commitdiff | raw | diff to current |
2010-03-30 |
Morgan Deters | Highlights of this commit are: |
blob | commitdiff | raw | diff to current |
2010-03-25 |
Christopher L. Conway | Adding comments to NodeManager |
blob | commitdiff | raw | diff to current |
next |