diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-05-06 20:07:56 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-05-06 20:07:56 +0000 |
commit | 1e8c9ae990adc55570298d1ffc5d8c55fbc71237 (patch) | |
tree | 8c8c0243a44a75ee471e7a477ed2391279df419c /test | |
parent | e909abcaf122e7c426d2b078728679f43a8ca442 (diff) |
Adding bit-vector constants in SMT2
Diffstat (limited to 'test')
-rw-r--r-- | test/unit/Makefile.am | 1 | ||||
-rw-r--r-- | test/unit/parser/parser_black.h | 33 | ||||
-rw-r--r-- | test/unit/util/bitvector_black.h | 54 |
3 files changed, 80 insertions, 8 deletions
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 666d1c285..2ec5122f3 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -21,6 +21,7 @@ UNIT_TESTS = \ theory/theory_black \ theory/theory_uf_white \ util/assert_white \ + util/bitvector_black \ util/configuration_black \ util/output_black \ util/exception_black \ diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index da636353e..b4044b96f 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -174,7 +174,9 @@ const string goodSmt2Exprs[] = { "(ite a (f x) y)", "1", "0", - "1.5" + "1.5", + "#xfab09c7", + "#b0001011" }; const int numGoodSmt2Exprs = sizeof(goodSmt2Exprs) / sizeof(string); @@ -205,7 +207,11 @@ const string badSmt2Exprs[] = { "(if_then_else a (f x) y)", // no if_then_else in v2 "(a b)", // using non-function as function ".5", // rational constants must have integer prefix - "1." // rational constants must have fractional suffix + "1.", // rational constants must have fractional suffix + "#x", // hex constants must have at least one digit + "#b", // ditto binary constants + "#xg0f", + "#b9" }; const int numBadSmt2Exprs = sizeof(badSmt2Exprs) / sizeof(string); @@ -271,7 +277,7 @@ class ParserBlack : public CxxTest::TestSuite { TS_ASSERT_THROWS ( while(parser.nextCommand()); cout << "\nBad input succeeded:\n" << badInputs[i] << endl;, - ParserException ); + const ParserException& ); // Debug.off("parser"); delete input; } @@ -299,13 +305,21 @@ class ParserBlack : public CxxTest::TestSuite { TS_ASSERT( e.isNull() ); delete input; } catch (Exception& e) { - cout << "\nGood expr failed:\n" << goodBooleanExprs[i] << endl; - cout << e; + cout << endl + << "Good expr failed." << endl + << "Input: <<" << goodBooleanExprs[i] << ">>" << endl + << "Output: <<" << e << ">>" << endl; throw; } } } + /* NOTE: The check implemented here may fail if a bad expression expression string + * has a prefix that is parseable as a good expression. E.g., the bad SMT v2 expression + * "#b10@@@@@@" will actually return the bit-vector 10 and ignore the tail of the + * input. It's more trouble than it's worth to check that the whole input was + * consumed here, so just be careful to avoid valid prefixes in tests. + */ void tryBadExprs(InputLanguage d_lang, const string badBooleanExprs[], int numExprs) { //Debug.on("parser"); for(int i = 0; i < numExprs; ++i) { @@ -318,9 +332,12 @@ class ParserBlack : public CxxTest::TestSuite { setupContext(parser); TS_ASSERT( !parser.done() ); TS_ASSERT_THROWS - ( parser.nextExpression(); - cout << "\nBad expr succeeded: " << badBooleanExprs[i] << endl;, - ParserException ); + ( Expr e = parser.nextExpression(); + cout << endl + << "Bad expr succeeded." << endl + << "Input: <<" << badBooleanExprs[i] << ">>" << endl + << "Output: <<" << e << ">>" << endl;, + const ParserException& ); delete input; } //Debug.off("parser"); diff --git a/test/unit/util/bitvector_black.h b/test/unit/util/bitvector_black.h new file mode 100644 index 000000000..f35107af0 --- /dev/null +++ b/test/unit/util/bitvector_black.h @@ -0,0 +1,54 @@ +/********************* */ +/** integer_black.h + ** Original author: taking + ** Major contributors: none + ** 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) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** Black box testing of CVC4::Integer. + **/ + +#include <cxxtest/TestSuite.h> +#include <sstream> + +#include "util/bitvector.h" + +using namespace CVC4; +using namespace std; + +class BitVectorBlack : public CxxTest::TestSuite { + + +public: + + void testStringConstructor() { + BitVector b1("0101",2); + TS_ASSERT_EQUALS( 4, b1.getSize() ); + TS_ASSERT_EQUALS( "0101", b1.toString() ); + TS_ASSERT_EQUALS( "5", b1.toString(10) ); + TS_ASSERT_EQUALS( "5", b1.toString(16) ); + + BitVector b2("000001", 2); + TS_ASSERT_EQUALS( 6, b2.getSize() ); + TS_ASSERT_EQUALS( "000001", b2.toString() ); + TS_ASSERT_EQUALS( "1", b2.toString(10) ); + TS_ASSERT_EQUALS( "1", b2.toString(16) ); + + BitVector b3("7f", 16); + TS_ASSERT_EQUALS( 8, b3.getSize() ); + TS_ASSERT_EQUALS( "01111111", b3.toString() ); + TS_ASSERT_EQUALS( "127", b3.toString(10) ); + TS_ASSERT_EQUALS( "7f", b3.toString(16) ); + + BitVector b4("01a", 16); + TS_ASSERT_EQUALS( 12, b4.getSize() ); + TS_ASSERT_EQUALS( "000000011010", b4.toString() ); + TS_ASSERT_EQUALS( "26", b4.toString(10) ); + TS_ASSERT_EQUALS( "1a", b4.toString(16) ); + } +}; |