diff options
-rw-r--r-- | examples/CMakeLists.txt | 1 | ||||
-rw-r--r-- | examples/hashsmt/CMakeLists.txt | 21 | ||||
-rw-r--r-- | examples/hashsmt/sha1.hpp | 229 | ||||
-rw-r--r-- | examples/hashsmt/sha1_collision.cpp | 109 | ||||
-rw-r--r-- | examples/hashsmt/sha1_inversion.cpp | 112 | ||||
-rw-r--r-- | examples/hashsmt/word.cpp | 174 | ||||
-rw-r--r-- | examples/hashsmt/word.h | 122 |
7 files changed, 0 insertions, 768 deletions
diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt index 4f7f1332f..03cbe1b2c 100644 --- a/examples/CMakeLists.txt +++ b/examples/CMakeLists.txt @@ -75,7 +75,6 @@ cvc4_add_example(simple_vc_quant_cxx "" "") add_subdirectory(api) # TODO(project issue $206): Port example to new API -# add_subdirectory(hashsmt) # add_subdirectory(nra-translate) # add_subdirectory(sets-translate) diff --git a/examples/hashsmt/CMakeLists.txt b/examples/hashsmt/CMakeLists.txt deleted file mode 100644 index c436f5e56..000000000 --- a/examples/hashsmt/CMakeLists.txt +++ /dev/null @@ -1,21 +0,0 @@ -##################### -## CMakeLists.txt -## Top contributors (to current version): -## Mathias Preiner, Aina Niemetz -## This file is part of the CVC4 project. -## Copyright (c) 2009-2021 by the authors listed in the file AUTHORS -## in the top-level source directory and their institutional affiliations. -## All rights reserved. See the file COPYING in the top-level source -## directory for licensing information. -## -if(Boost_FOUND) - cvc4_add_example(sha1_inversion - "sha1_inversion.cpp word.cpp" "hashsmt" - # arguments to binary (for testing) - "a" "sha1_inversion.outfile") -endif() - -cvc4_add_example(sha1_collision - "sha1_collision.cpp word.cpp" "hashsmt" - # arguments to binary (for testing) - "1" "1" "sha1_collision.outfile") diff --git a/examples/hashsmt/sha1.hpp b/examples/hashsmt/sha1.hpp deleted file mode 100644 index 98c33d47e..000000000 --- a/examples/hashsmt/sha1.hpp +++ /dev/null @@ -1,229 +0,0 @@ -/********************* */ -/*! \file sha1.hpp - ** \verbatim - ** Top contributors (to current version): - ** Dejan Jovanovic, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -// boost/uuid/sha1.hpp header file ----------------------------------------------// - -// Copyright 2007 Andy Tompkins. -// Distributed under the Boost Software License, Version 1.0. (See -// accompanying file LICENSE_1_0.txt or copy at -// http://www.boost.org/LICENSE_1_0.txt) - -// Revision History -// 29 May 2007 - Initial Revision -// 25 Feb 2008 - moved to namespace boost::uuids::detail - -// This is a byte oriented implementation -// Note: this implementation does not handle message longer than -// 2^32 bytes. - -#ifndef __CVC4__EXAMPLES__HASHSMT__SHA1_H -#define __CVC4__EXAMPLES__HASHSMT__SHA1_H - -#include <cstddef> - -#include "word.h" - -#ifdef BOOST_NO_STDC_NAMESPACE -namespace std { - using ::size_t; -} // namespace std -#endif - -namespace hashsmt { - -static_assert(sizeof(unsigned char)*8 == 8, - "Unexpected size for unsigned char"); -static_assert(sizeof(unsigned int)*8 == 32, - "Unexpected size for unsigned int"); - -inline cvc4_uint32 left_rotate(cvc4_uint32 x, std::size_t n) -{ - return (x<<n) ^ (x>> (32-n)); -} - -class sha1 -{ -public: - typedef cvc4_uint32(&digest_type)[5]; -public: - sha1(unsigned rounds = 80); - - void reset(); - - void process_byte(cvc4_uchar8 byte); - void process_block(void const* bytes_begin, void const* bytes_end); - void process_bytes(void const* buffer, std::size_t byte_count); - - void get_digest(digest_type digest); - -private: - void process_block(); - -private: - cvc4_uint32 h_[5]; - - cvc4_uchar8 block_[64]; - - std::size_t block_byte_index_; - std::size_t byte_count_; - - unsigned rounds_; -}; - -inline sha1::sha1(unsigned rounds) -: rounds_(rounds) -{ - reset(); -} - -inline void sha1::reset() -{ - h_[0] = 0x67452301; - h_[1] = 0xEFCDAB89; - h_[2] = 0x98BADCFE; - h_[3] = 0x10325476; - h_[4] = 0xC3D2E1F0; - - block_byte_index_ = 0; - byte_count_ = 0; -} - -inline void sha1::process_byte(cvc4_uchar8 byte) -{ - block_[block_byte_index_++] = byte; - ++byte_count_; - if (block_byte_index_ == 64) { - block_byte_index_ = 0; - process_block(); - } -} - -inline void sha1::process_block(void const* bytes_begin, void const* bytes_end) -{ - cvc4_uchar8 const* begin = static_cast<cvc4_uchar8 const*>(bytes_begin); - cvc4_uchar8 const* end = static_cast<cvc4_uchar8 const*>(bytes_end); - for(; begin != end; ++begin) { - process_byte(*begin); - } -} - -inline void sha1::process_bytes(void const* buffer, std::size_t byte_count) -{ - cvc4_uchar8 const* b = static_cast<cvc4_uchar8 const*>(buffer); - process_block(b, b+byte_count); -} - -inline void sha1::process_block() -{ - cvc4_uint32 w[80]; - for (std::size_t i=0; i<16; ++i) { - w[i] = (block_[i*4 + 0] << 24); - w[i] |= (block_[i*4 + 1] << 16); - w[i] |= (block_[i*4 + 2] << 8); - w[i] |= (block_[i*4 + 3]); - } - for (std::size_t i=16; i<80; ++i) { - w[i] = left_rotate((w[i-3] ^ w[i-8] ^ w[i-14] ^ w[i-16]), 1); - } - - cvc4_uint32 a = h_[0]; - cvc4_uint32 b = h_[1]; - cvc4_uint32 c = h_[2]; - cvc4_uint32 d = h_[3]; - cvc4_uint32 e = h_[4]; - - for (std::size_t i=0; i<rounds_; ++i) { - cvc4_uint32 f; - cvc4_uint32 k; - - if (i<20) { - f = (b & c) | (~b & d); - k = 0x5A827999; - } else if (i<40) { - f = b ^ c ^ d; - k = 0x6ED9EBA1; - } else if (i<60) { - f = (b & c) | (b & d) | (c & d); - k = 0x8F1BBCDC; - } else { - f = b ^ c ^ d; - k = 0xCA62C1D6; - } - - cvc4_uint32 temp = left_rotate(a, 5) + f + e + k + w[i]; - e = d; - d = c; - c = left_rotate(b, 30); - b = a; - a = temp; - } - - h_[0] += a; - h_[1] += b; - h_[2] += c; - h_[3] += d; - h_[4] += e; -} - -inline void sha1::get_digest(digest_type digest) -{ - std::size_t bit_count = byte_count_*8; - - // append the bit '1' to the message - process_byte(0x80); - - // append k bits '0', where k is the minimum number >= 0 - // such that the resulting message length is congruent to 56 (mod 64) - // check if there is enough space for padding and bit_count - if (block_byte_index_ > 56) { - // finish this block - while (block_byte_index_ != 0) { - process_byte(0); - } - - // one more block - while (block_byte_index_ < 56) { - process_byte(0); - } - } else { - while (block_byte_index_ < 56) { - process_byte(0); - } - } - - // append length of message (before pre-processing) - // as a 64-bit big-endian integer - process_byte(0); - process_byte(0); - process_byte(0); - process_byte(0); - process_byte( static_cast<unsigned char>((bit_count>>24) & 0xFF)); - process_byte( static_cast<unsigned char>((bit_count>>16) & 0xFF)); - process_byte( static_cast<unsigned char>((bit_count>>8 ) & 0xFF)); - process_byte( static_cast<unsigned char>((bit_count) & 0xFF)); - - // get final digest - digest[0] = h_[0]; - digest[1] = h_[1]; - digest[2] = h_[2]; - digest[3] = h_[3]; - digest[4] = h_[4]; -} - -} // namespace hashsmt - -#endif /* __CVC4__EXAMPLES__HASHSMT__SHA1_H */ diff --git a/examples/hashsmt/sha1_collision.cpp b/examples/hashsmt/sha1_collision.cpp deleted file mode 100644 index 0545ce048..000000000 --- a/examples/hashsmt/sha1_collision.cpp +++ /dev/null @@ -1,109 +0,0 @@ -/********************* */ -/*! \file sha1_collision.cpp - ** \verbatim - ** Top contributors (to current version): - ** Dejan Jovanovic, Aina Niemetz, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -/* - * sha1smt.cpp - * - * Created on: Jul 13, 2012 - * Author: dejan - */ - -#include <fstream> -#include <iostream> -#include <sstream> -#include <string> - -#include <cvc4/cvc4.h> -#include <cvc4/expr/expr_iomanip.h> -#include <cvc4/options/set_language.h> -#include "sha1.hpp" -#include "word.h" - -using namespace std; -using namespace cvc5; - -hashsmt::cvc4_uchar8 *createInput(unsigned size, std::string prefix, std::ostream& output) { - hashsmt::cvc4_uchar8 *input = new hashsmt::cvc4_uchar8[size]; - for(unsigned i = 0; i < size; ++i) { - stringstream ss; - ss << prefix << i; - input[i] = hashsmt::cvc4_uchar8(ss.str()); - output << DeclareFunctionCommand(ss.str(), input[i].getExpr(), input[i].getExpr().getType()) << endl; - } - return input; -} - -int main(int argc, char* argv[]) { - - try { - - // Check the arguments - if (argc != 4) { - cerr << "usage: sha1smt size rounds (1..80) output-file" << std::endl; - return 1; - } - - // Get the input size to encode - unsigned msgSize; - istringstream msgSize_is(argv[1]); - msgSize_is >> msgSize; - - // Get the number of rounds to use - unsigned rounds; - istringstream rounds_is(argv[2]); - rounds_is >> rounds; - - // The output - ofstream output(argv[3]); - output << expr::ExprSetDepth(-1) << language::SetLanguage(language::output::LANG_SMTLIB_V2); - output << SetBenchmarkLogicCommand("QF_BV") << endl; - output << SetBenchmarkStatusCommand(SMT_UNSATISFIABLE) << endl; - - // Make the variables the size of the string - hashsmt::cvc4_uchar8 *cvc4input1 = createInput(msgSize, "x", output); - hashsmt::cvc4_uchar8 *cvc4input2 = createInput(msgSize, "y", output); - - // Do the cvc4 encoding for first message - hashsmt::sha1 cvc4encoder1(rounds); - cvc4encoder1.process_bytes(cvc4input1, msgSize); - hashsmt::cvc4_uint32 cvc4digest1[5]; - cvc4encoder1.get_digest(cvc4digest1); - - // Do the cvc4 encoding for second message - hashsmt::sha1 cvc4encoder2(rounds); - cvc4encoder2.process_bytes(cvc4input2, msgSize); - hashsmt::cvc4_uint32 cvc4digest2[5]; - cvc4encoder2.get_digest(cvc4digest2); - - // Create the assertion - Expr inputEqual = (hashsmt::Word::concat(cvc4input1, msgSize) == hashsmt::Word::concat(cvc4input2, msgSize)); - Expr digestEqual = (hashsmt::Word::concat(cvc4digest1, 5) == hashsmt::Word::concat(cvc4digest2, 5)); - Expr assertion = inputEqual.notExpr().andExpr(digestEqual); - - output << AssertCommand(assertion) << endl; - - // Checksat command - output << CheckSatCommand() << endl; - - delete[] cvc4input1; - delete[] cvc4input2; - } - catch (cvc5::Exception& e) - { - cerr << e << endl; - } -} diff --git a/examples/hashsmt/sha1_inversion.cpp b/examples/hashsmt/sha1_inversion.cpp deleted file mode 100644 index a4acfc3c6..000000000 --- a/examples/hashsmt/sha1_inversion.cpp +++ /dev/null @@ -1,112 +0,0 @@ -/********************* */ -/*! \file sha1_inversion.cpp - ** \verbatim - ** Top contributors (to current version): - ** Dejan Jovanovic, Aina Niemetz, Andres Noetzli - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -/* - * sha1smt.cpp - * - * Created on: Jul 13, 2012 - * Author: dejan - */ - -#include <boost/version.hpp> -#if BOOST_VERSION > 106700 -#include <boost/uuid/detail/sha1.hpp> -#else -#include <boost/uuid/sha1.hpp> -#endif - -#include <fstream> -#include <iostream> -#include <sstream> -#include <string> -#include <vector> - -#include <cvc4/cvc4.h> -#include <cvc4/expr/expr_iomanip.h> -#include <cvc4/options/set_language.h> - -#include "sha1.hpp" -#include "word.h" - -using namespace std; -using namespace cvc5; - -int main(int argc, char* argv[]) { - - try { - - // Check the arguments - if (argc != 3) { - cerr << "usage: sha1smt message output-file" << std::endl; - return 1; - } - - // Get the message to encode and the output file - string msg = argv[1]; - unsigned msgSize = msg.size(); - ofstream output(argv[2]); - output << expr::ExprSetDepth(-1) << language::SetLanguage(language::output::LANG_SMTLIB_V2); - output << SetBenchmarkLogicCommand("QF_BV") << endl; - output << SetBenchmarkStatusCommand(SMT_SATISFIABLE) << endl; - - // Make the variables the size of the string - std::vector<hashsmt::cvc4_uchar8> cvc4input(msgSize); - for (unsigned i = 0; i < msgSize; ++ i) { - stringstream ss; - ss << "x" << i; - cvc4input[i] = hashsmt::cvc4_uchar8(ss.str()); - output << DeclareFunctionCommand(ss.str(), cvc4input[i].getExpr(), cvc4input[i].getExpr().getType()) << endl; - - // Ouput the solution also - Expr solution = (cvc4input[i] == hashsmt::cvc4_uchar8(msg.c_str()[i])); - output << "; " << AssertCommand(solution) << endl; - } - - // Do the cvc4 encoding - hashsmt::sha1 cvc4encoder; - cvc4encoder.process_bytes(cvc4input.data(), msgSize); - - // Get the digest as bitvectors - hashsmt::cvc4_uint32 cvc4digest[5]; - cvc4encoder.get_digest(cvc4digest); - - // Do the actual sha1 encoding - boost::uuids::detail::sha1 sha1encoder; - sha1encoder.process_bytes(msg.c_str(), msgSize); - unsigned sha1digest[5]; - sha1encoder.get_digest(sha1digest); - - // Create the assertion - Expr assertion; - for (unsigned i = 0; i < 5; ++ i) { - Expr conjunct = (cvc4digest[i] == hashsmt::cvc4_uint32(sha1digest[i])); - if (i > 0) { - assertion = assertion.andExpr(conjunct); - } else { - assertion = conjunct; - } - } - output << AssertCommand(assertion) << endl; - - // Checksat command - output << CheckSatCommand() << endl; - } - catch (cvc5::Exception& e) - { - cerr << e << endl; - } -} diff --git a/examples/hashsmt/word.cpp b/examples/hashsmt/word.cpp deleted file mode 100644 index 79b868d1c..000000000 --- a/examples/hashsmt/word.cpp +++ /dev/null @@ -1,174 +0,0 @@ -/********************* */ -/*! \file word.cpp - ** \verbatim - ** Top contributors (to current version): - ** Dejan Jovanovic, Tim King, Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -/* - * word.cpp - * - * Created on: Jul 13, 2012 - * Author: dejan - */ - -#include "word.h" - -#include <vector> - -#include <cvc4/cvc4.h> -#include <cvc4/expr/expr_iomanip.h> -#include <cvc4/options/language.h> -#include <cvc4/options/options.h> - -using namespace std; -using namespace hashsmt; -using namespace cvc5; -using namespace cvc5::options; - -Expr Word::extendToSize(unsigned newSize) const { - if (newSize <= size()) { - return d_expr; - } else { - // 0-extend to size - Expr extendOp = em()->mkConst(BitVectorZeroExtend(newSize - size())); - return em()->mkExpr(extendOp, d_expr); - } -} - -ExprManager* Word::s_manager = 0; - -ExprManager* Word::em() { - if (s_manager == 0) { - cvc5::Options options; - options.setInputLanguage(language::input::LANG_SMTLIB_V2); - options.setOutputLanguage(language::output::LANG_SMTLIB_V2); - s_manager = new cvc5::ExprManager(options); - } - return s_manager; -} - -Expr Word::operator == (const Word& b) const { - return em()->mkExpr(kind::EQUAL, d_expr, b.getExpr()); -} - -Word Word::concat(const Word words[], unsigned size) { - Expr concat = words[0].d_expr; - for(unsigned i = 1; i < size; ++i) { - concat = em()->mkExpr(kind::BITVECTOR_CONCAT, concat, words[i].d_expr); - } - return Word(concat); -} - -void Word::print(ostream& out) const { - out << cvc5::expr::ExprSetDepth(-1) << d_expr; -} - -Word::Word(unsigned newSize, unsigned value) { - d_expr = em()->mkConst(BitVector(newSize, value)); -}; - -Word::Word(unsigned newSize, string name) { - d_expr = em()->mkVar(name, em()->mkBitVectorType(newSize)); -}; - -Word& Word::operator = (const Word& b) { - d_expr = b.d_expr; - return *this; -} - -Word Word::operator + (const Word& b) const { - unsigned newSize = std::max(size(), b.size()); - Expr lhs = extendToSize(newSize); - Expr rhs = b.extendToSize(newSize); - return em()->mkExpr(kind::BITVECTOR_PLUS, lhs, rhs); -} - -Word& Word::operator += (const Word& b) { - (*this) = (*this) + b; - return (*this); -} - -Word Word::operator ~ () const { - return em()->mkExpr(kind::BITVECTOR_NOT, d_expr); -} - -Word Word::operator & (const Word& b) const { - unsigned newSize = std::max(size(), b.size()); - Expr lhs = extendToSize(newSize); - Expr rhs = b.extendToSize(newSize); - return em()->mkExpr(kind::BITVECTOR_AND, lhs, rhs); -} - -Word Word::operator | (const Word& b) const { - unsigned newSize = std::max(size(), b.size()); - Expr lhs = extendToSize(newSize); - Expr rhs = b.extendToSize(newSize); - return em()->mkExpr(kind::BITVECTOR_OR, lhs, rhs); -} - -Word& Word::operator |= (const Word& b) { - (*this) = (*this) | b; - return (*this); -} - -Word Word::operator ^ (const Word& b) const { - unsigned newSize = std::max(size(), b.size()); - Expr lhs = extendToSize(newSize); - Expr rhs = b.extendToSize(newSize); - return em()->mkExpr(kind::BITVECTOR_XOR, lhs, rhs); -} - -Word Word::operator << (unsigned amount) const { - // Instead of shifting we just add zeroes, to ensure that ((char)x << 24) return 32 bits - Word padding(amount, 0); - return em()->mkExpr(kind::BITVECTOR_CONCAT, d_expr, padding.d_expr); -} - -Word Word::operator >> (unsigned amount) const { - Word shiftAmount(size(), amount); - return em()->mkExpr(kind::BITVECTOR_LSHR, d_expr, shiftAmount.d_expr); -} - -unsigned Word::size() const { - BitVectorType type = d_expr.getType(); - return type.getSize(); -} - -cvc4_uint32::cvc4_uint32(const Word& b) { - if (b.size() > 32) { - // Extract the first 32 bits - Expr extractOp = em()->mkConst(BitVectorExtract(31, 0)); - d_expr = em()->mkExpr(extractOp, b.getExpr()); - } else if (b.size() < 32) { - // 0-extend to 32 bits - Expr extendOp = em()->mkConst(BitVectorZeroExtend(32 - b.size())); - d_expr = em()->mkExpr(extendOp, b.getExpr()); - } else { - d_expr = b.getExpr(); - } -} - -cvc4_uchar8::cvc4_uchar8(const Word& b) { - if (b.size() > 8) { - // Extract the first 8 bits - Expr extractOp = em()->mkConst(BitVectorExtract(7, 0)); - d_expr = em()->mkExpr(extractOp, b.getExpr()); - } else if (b.size() < 8) { - // 0-extend to 8 bits - Expr extendOp = em()->mkConst(BitVectorZeroExtend(8 - b.size())); - d_expr = em()->mkExpr(extendOp, b.getExpr()); - } else { - d_expr = b.getExpr(); - } -} diff --git a/examples/hashsmt/word.h b/examples/hashsmt/word.h deleted file mode 100644 index f5b95ba32..000000000 --- a/examples/hashsmt/word.h +++ /dev/null @@ -1,122 +0,0 @@ -/********************* */ -/*! \file word.h - ** \verbatim - ** Top contributors (to current version): - ** Dejan Jovanovic - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -/* - * word.h - * - * Created on: Jul 13, 2012 - * Author: dejan - */ - -#ifndef WORD_H_ -#define WORD_H_ - -#include <string> -#include <iostream> - -#include <cvc4/cvc4.h> - -namespace hashsmt { - -class Word { - - /** Expression managaer we're using for all word expressions */ - static cvc5::ExprManager* s_manager; - - protected: - - /** The expression of this word */ - cvc5::Expr d_expr; - - /** Get the expression manager words are using */ - static cvc5::ExprManager* em(); - - Word(cvc5::Expr expr = cvc5::Expr()) : d_expr(expr) {} - - /** Extend the representing expression to the given size >= size() */ - cvc5::Expr extendToSize(unsigned size) const; - - public: - - Word(unsigned size, unsigned value = 0); - Word(unsigned size, std::string name); - - Word& operator = (const Word& b); - Word operator + (const Word& b) const; - Word& operator += (const Word& b); - Word operator ~ () const; - Word operator & (const Word& b) const; - Word operator | (const Word& b) const; - Word& operator |= (const Word& b); - Word operator ^ (const Word& b) const; - Word operator << (unsigned amount) const; - Word operator >> (unsigned amount) const; - - unsigned size() const; - - void print(std::ostream& out) const; - - cvc5::Expr getExpr() const { return d_expr; } - - /** Returns the comparison expression */ - cvc5::Expr operator==(const Word& b) const; - - /** Concatenate the given words */ - static Word concat(const Word words[], unsigned size); -}; - -inline std::ostream& operator << (std::ostream& out, const Word& word) { - word.print(out); - return out; -} - -/** Symbolic 32-bit unsigned integer as a CVC4 bitvector expression */ -class cvc4_uint32 : public Word { -public: - - /** Construction from constants of the right size */ - cvc4_uint32(unsigned value = 0) - : Word(32, value) {} - - /** Construction of variables of the right size */ - cvc4_uint32(std::string name) - : Word(32, name) {} - - /** Automatic extend/cut to uint32 */ - cvc4_uint32(const Word& word); -}; - -/** Symbolic 8-bit unsigned char as a CVC4 bitvector expression */ -class cvc4_uchar8 : public Word { -public: - - /** Construction from constants of the right size */ - cvc4_uchar8(unsigned value = 0) - : Word(8, value) {} - - /** Construction of variables of the right size */ - cvc4_uchar8(std::string name) - : Word(8, name) {} - - /** Automatic extend/cut to uchar8 */ - cvc4_uchar8(const Word& word); -}; - - -} - -#endif /* WORD_H_ */ |