diff options
| author | Morgan Deters <mdeters@gmail.com> | 2011-04-18 08:59:09 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2011-04-18 08:59:09 +0000 |
| commit | b90081962840584bb9eeda368ea232a7d42a292b (patch) | |
| tree | c0f568bc787744a5d53b79a818c0f1bd819596cf /src/theory/builtin | |
| parent | 7d281fba79b1c9f3ae646d3371a0e52e2efd3bba (diff) | |
Partial merge from datatypes-merge branch:
1. Defines a new type "DatatypeType", a type-constant that holds a Datatype, describing an inductive data type.
2. CVC language parser supports datatypes.
3. CVC language printer now functional.
4. Minor other cleanups.
No performance impact is expected outside of datatypes. I'm verifying that that is the case with a cluster job this morning.
Diffstat (limited to 'src/theory/builtin')
| -rw-r--r-- | src/theory/builtin/theory_builtin_rewriter.h | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/builtin/theory_builtin_rewriter.h b/src/theory/builtin/theory_builtin_rewriter.h index d50397598..716323b8a 100644 --- a/src/theory/builtin/theory_builtin_rewriter.h +++ b/src/theory/builtin/theory_builtin_rewriter.h @@ -2,7 +2,7 @@ /*! \file theory_builtin_rewriter.h ** \verbatim ** Original author: dejan - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) @@ -36,7 +36,7 @@ class TheoryBuiltinRewriter { public: static inline RewriteResponse postRewrite(TNode node) { - if (node.getKind() == kind::EQUAL) { + if(node.getKind() == kind::EQUAL) { return Rewriter::callPostRewrite(Theory::theoryOf(node[0]), node); } return RewriteResponse(REWRITE_DONE, node); |