Delete hashsmt example. (#6263)

This example does not serve the purpose of documenting how to use the
new API. It uses Command, which is not available via the API, and it's
not worth the effort to migrate it.

1 files changed, 0 insertions, 122 deletions

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_ */