diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-04-18 18:05:39 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-04-18 18:05:39 +0000 |
commit | 267858307741675cb78e829270e619f57cf21a27 (patch) | |
tree | d8b663f8b213f6d4a085b06c2f12bffccfd7de33 /test/unit | |
parent | abe849b486ea3707fd51a612c7982554f3d6581f (diff) |
mostly CVC presentation language parsing and printing
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/parser/parser_black.h | 12 | ||||
-rw-r--r-- | test/unit/util/datatype_black.h | 4 |
2 files changed, 13 insertions, 3 deletions
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index af9b7bd0f..dbc8e2281 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -2,10 +2,10 @@ /*! \file parser_black.h ** \verbatim ** Original author: cconway - ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Major contributors: mdeters + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing @@ -206,7 +206,12 @@ public: tryGoodInput("a, b : BOOLEAN;"); tryGoodInput("a, b : BOOLEAN; QUERY (a => b) AND a => b;"); tryGoodInput("T, U : TYPE; f : T -> U; x : T; y : U; CHECKSAT f(x) = y;"); + tryGoodInput("T : TYPE = BOOLEAN; x : T; CHECKSAT x;"); + tryGoodInput("a : ARRAY INT OF REAL; ASSERT (a WITH [1] := 0.0)[1] = a[0];"); + tryGoodInput("b : BITVECTOR(3); ASSERT b = 0bin101;"); + tryGoodInput("T : TYPE = BOOLEAN; x : T; CHECKSAT x;"); tryGoodInput("T : TYPE; x, y : T; a : BOOLEAN; QUERY (IF a THEN x ELSE y ENDIF) = x;"); + tryGoodInput("CHECKSAT 0bin0000 /= 0hex7;"); tryGoodInput("%% nothing but a comment"); tryGoodInput("% a comment\nASSERT TRUE; %a command\n% another comment"); } @@ -219,6 +224,7 @@ public: tryBadInput("a, b : boolean;"); // lowercase boolean isn't a type tryBadInput("0x : INT;"); // 0x isn't an identifier tryBadInput("a, b : BOOLEAN\nQUERY (a => b) AND a => b;"); // no semicolon after decl + tryBadInput("ASSERT 0bin012 /= 0hex0;"); // bad binary literal tryBadInput("a : BOOLEAN; a: BOOLEAN;"); // double decl tryBadInput("a, b: BOOLEAN; QUERY a(b);"); // non-function used as function } diff --git a/test/unit/util/datatype_black.h b/test/unit/util/datatype_black.h index d0de68e33..991d71364 100644 --- a/test/unit/util/datatype_black.h +++ b/test/unit/util/datatype_black.h @@ -54,6 +54,10 @@ public: cout << nat << std::endl; DatatypeType natType = d_em->mkDatatypeType(nat); cout << natType << std::endl; + + Expr ctor = natType.getDatatype()[1].getConstructor(); + Expr apply = d_em->mkExpr(kind::APPLY_CONSTRUCTOR, ctor); + cout << apply << std::endl; } void testTree() { |