From: Christopher L. Conway Date: Thu, 6 May 2010 20:07:56 +0000 (+0000) Subject: Adding bit-vector constants in SMT2 X-Git-Tag: cvc5-1.0.0~9073 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1e8c9ae990adc55570298d1ffc5d8c55fbc71237;p=cvc5.git Adding bit-vector constants in SMT2 --- diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h index f52467ad9..38fe1bce8 100644 --- a/src/parser/antlr_input.h +++ b/src/parser/antlr_input.h @@ -29,6 +29,7 @@ #include "expr/expr.h" #include "expr/expr_manager.h" #include "util/Assert.h" +#include "util/bitvector.h" #include "util/integer.h" #include "util/rational.h" @@ -148,8 +149,6 @@ public: static Integer tokenToInteger( pANTLR3_COMMON_TOKEN token ); /** Retrieve a Rational from the text of a token */ static Rational tokenToRational(pANTLR3_COMMON_TOKEN token); - /** Retrive a Bitvector from the text of a token */ -// static Bitvector tokenToBitvector(pANTLR3_COMMON_TOKEN token, int base); protected: /** Create an input. This input takes ownership of the given input stream, @@ -201,8 +200,7 @@ inline unsigned AntlrInput::tokenToUnsigned(pANTLR3_COMMON_TOKEN token) { } inline Integer AntlrInput::tokenToInteger(pANTLR3_COMMON_TOKEN token) { - Integer i( tokenText(token) ); - return i; + return Integer( tokenText(token) ); } inline Rational AntlrInput::tokenToRational(pANTLR3_COMMON_TOKEN token) { diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 01cc99c3d..d788a2c3f 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -241,8 +241,9 @@ Expr Parser::nextExpression() throw(ParserException) { if(!done()) { try { result = d_input->parseExpr(); - if(result.isNull()) + if(result.isNull()) { setDone(); + } } catch(ParserException& e) { setDone(); throw; diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 19997cdd0..4f65fa5e7 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -259,6 +259,14 @@ term[CVC4::Expr& expr] | RATIONAL { // FIXME: This doesn't work because an SMT rational is not a valid GMP rational string expr = MK_CONST( AntlrInput::tokenToRational($RATIONAL) ); } + | HEX_LITERAL + { std::string hexString = AntlrInput::tokenText($HEX_LITERAL); + AlwaysAssert( hexString.find("#x") == 0 ); + expr = MK_CONST( BitVector(hexString.erase(0,2), 16) ); } + | BINARY_LITERAL + { std::string binString = AntlrInput::tokenText($BINARY_LITERAL); + AlwaysAssert( binString.find("#b") == 0 ); + expr = MK_CONST( BitVector(binString.erase(0,2), 2) ); } // NOTE: Theory constants go here ; @@ -351,15 +359,6 @@ sortSymbol[CVC4::Type& t] { t = EXPR_MANAGER->booleanType(); } ; -/** - * Matches the status of the benchmark, one of 'sat', 'unsat' or 'unknown'. - */ -benchmarkStatus[ CVC4::BenchmarkStatus& status ] - : SAT_TOK { $status = SMT_SATISFIABLE; } - | UNSAT_TOK { $status = SMT_UNSATISFIABLE; } - | UNKNOWN_TOK { $status = SMT_UNKNOWN; } - ; - /** * Matches an symbol and sets the string reference parameter id. * @param id string to hold the symbol @@ -459,16 +458,37 @@ WHITESPACE ; /** - * Matches a numeral from the input (non-empty sequence of digits). + * Matches an integer constant from the input (non-empty sequence of digits). + * This is a bit looser than what the standard allows, because it accepts + * leading zeroes. */ NUMERAL : DIGIT+ ; +/** + * Matches a rational constant from the input. This is a bit looser + * than what the standard allows, because it accepts leading zeroes. + */ RATIONAL : DIGIT+ '.' DIGIT+ ; +/** + * Matches a hexadecimal constant. + */ + HEX_LITERAL + : '#x' HEX_DIGIT+ + ; + +/** + * Matches a binary constant. + */ + BINARY_LITERAL + : '#b' ('0' | '1')+ + ; + + /** * Matches a double quoted string literal. Escaping is supported, and escape * character '\' has to be escaped. @@ -499,6 +519,8 @@ ALPHA */ fragment DIGIT : '0'..'9'; +fragment HEX_DIGIT : DIGIT | 'a'..'f' | 'A'..'F'; + /** Matches the characters that may appear in a "symbol" (i.e., an identifier) */ fragment SYMBOL_CHAR diff --git a/src/util/bitvector.h b/src/util/bitvector.h index 2d01189c5..4f6038a81 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -8,9 +8,12 @@ #ifndef __CVC4__BITVECTOR_H_ #define __CVC4__BITVECTOR_H_ -#include #include +#include "util/Assert.h" #include "util/gmp_util.h" +#include "util/integer.h" + +using namespace std; namespace CVC4 { @@ -19,9 +22,9 @@ class BitVector { private: unsigned d_size; - mpz_class d_value; + Integer d_value; - BitVector(unsigned size, const mpz_class& val) : d_size(size), d_value(val) {} + BitVector(unsigned size, const Integer& val) : d_size(size), d_value(val) {} public: @@ -37,8 +40,7 @@ public: BitVector(unsigned size, const BitVector& q) : d_size(size), d_value(q.d_value) {} - BitVector(const std::string& num, unsigned base = 2) - : d_size(1), d_value(0) {} + BitVector(const std::string& num, unsigned base = 2); ~BitVector() {} @@ -80,11 +82,20 @@ public: } size_t hash() const { - return gmpz_hash(d_value.get_mpz_t()); + return d_value.hash(); } std::string toString(unsigned int base = 2) const { - return d_value.get_str(base); + std::string str = d_value.toString(base); + if( base == 2 && d_size > str.size() ) { + std::string zeroes; + for( unsigned int i=0; i < d_size - str.size(); ++i ) { + zeroes.append("0"); + } + return zeroes + str; + } else { + return str; + } } unsigned getSize() const { @@ -92,6 +103,38 @@ public: } }; +inline BitVector::BitVector(const std::string& num, unsigned base) { + AlwaysAssert( base == 2 || base == 16 ); + + if( base == 2 ) { + d_size = num.size(); +// d_value = Integer(num,2); +/* + for( string::const_iterator it = num.begin(); it != num.end(); ++it ) { + if( *it != '0' || *it != '1' ) { + IllegalArgument(num, "BitVector argument is not a binary string."); + } + z = (Integer(2) * z) + (*it == '1'); + d_value = mpz_class(z.get_mpz()); + } +*/ + } else if( base == 16 ) { + d_size = num.size() * 4; +// // Use a stream to decode the hex string +// stringstream ss; +// ss.setf(ios::hex, ios::basefield); +// ss << num; +// ss >> z; +// d_value = mpz_class(z); +// break; + } else { + Unreachable("Unsupported base in BitVector(std::string&, unsigned int)."); + } + + d_value = Integer(num,base); +} + + /** * Hash function for the BitVector constants. */ 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 +#include + +#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) ); + } +};