From 0c4a6edae95b3ffc76cb82604a3d1694d42625bb Mon Sep 17 00:00:00 2001 From: "Christopher L. Conway" Date: Tue, 27 Apr 2010 20:44:47 +0000 Subject: Adding Integer and Rational constants to SMT --- test/unit/parser/parser_white.h | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'test') diff --git a/test/unit/parser/parser_white.h b/test/unit/parser/parser_white.h index 317817e15..1d19525d6 100644 --- a/test/unit/parser/parser_white.h +++ b/test/unit/parser/parser_white.h @@ -109,7 +109,10 @@ const string goodSmtExprs[] = { "(and (iff a b) (not a))", "(iff (xor a b) (and (or a b) (not (and a b))))", "(ite a (f x) y)", - "(if_then_else a (f x) y)" + "(if_then_else a (f x) y)", + "1", + "0"// , +// "1.5" }; const int numGoodSmtExprs = sizeof(goodSmtExprs) / sizeof(string); @@ -134,7 +137,9 @@ const string badSmtExprs[] = { "(not a b)", // wrong arity "not a", // needs parens "(ite a x)", // wrong arity - "(a b)" // using non-function as function + "(a b)", // using non-function as function + ".5", // rational constants must have integer prefix + "1." // rational constants must have fractional suffix }; const int numBadSmtExprs = sizeof(badSmtExprs) / sizeof(string); -- cgit v1.2.3