#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"
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,
}
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) {
if(!done()) {
try {
result = d_input->parseExpr();
- if(result.isNull())
+ if(result.isNull()) {
setDone();
+ }
} catch(ParserException& e) {
setDone();
throw;
| 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
;
{ 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
;
/**
- * 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.
*/
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
#ifndef __CVC4__BITVECTOR_H_
#define __CVC4__BITVECTOR_H_
-#include <string>
#include <iostream>
+#include "util/Assert.h"
#include "util/gmp_util.h"
+#include "util/integer.h"
+
+using namespace std;
namespace CVC4 {
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:
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() {}
}
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 {
}
};
+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.
*/
theory/theory_black \
theory/theory_uf_white \
util/assert_white \
+ util/bitvector_black \
util/configuration_black \
util/output_black \
util/exception_black \
"(ite a (f x) y)",
"1",
"0",
- "1.5"
+ "1.5",
+ "#xfab09c7",
+ "#b0001011"
};
const int numGoodSmt2Exprs = sizeof(goodSmt2Exprs) / sizeof(string);
"(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);
TS_ASSERT_THROWS
( while(parser.nextCommand());
cout << "\nBad input succeeded:\n" << badInputs[i] << endl;,
- ParserException );
+ const ParserException& );
// Debug.off("parser");
delete input;
}
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) {
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");
--- /dev/null
+/********************* */
+/** 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) );
+ }
+};
projects / cvc5.git / commitdiff