diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-20 14:49:02 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-20 14:49:02 -0600 |
commit | 5489ef01beb91e256e343e2fd2d734b48b42ad6e (patch) | |
tree | f6a535c768ae4f3cfbbed765b0697300f4412657 /src/expr | |
parent | 32fdf625f66b8ebf260756962a53d63eec771c12 (diff) |
Remove front-end support for Chain (#3767)
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/CMakeLists.txt | 1 | ||||
-rw-r--r-- | src/expr/chain.h | 51 | ||||
-rw-r--r-- | src/expr/chain.i | 12 |
3 files changed, 0 insertions, 64 deletions
diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index f6b48048f..8357102b0 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -7,7 +7,6 @@ libcvc4_add_sources( attribute.cpp attribute_internals.h attribute_unique_id.h - chain.h emptyset.cpp emptyset.h expr_iomanip.cpp diff --git a/src/expr/chain.h b/src/expr/chain.h deleted file mode 100644 index 9df819b4d..000000000 --- a/src/expr/chain.h +++ /dev/null @@ -1,51 +0,0 @@ -/********************* */ -/*! \file chain.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 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 - **/ - -#include "cvc4_public.h" - -#ifndef CVC4__CHAIN_H -#define CVC4__CHAIN_H - -#include "expr/kind.h" -#include <iostream> - -namespace CVC4 { - -/** A class to represent a chained, built-in operator. */ -class CVC4_PUBLIC Chain { - Kind d_kind; -public: - explicit Chain(Kind k) : d_kind(k) { } - bool operator==(const Chain& ch) const { return d_kind == ch.d_kind; } - bool operator!=(const Chain& ch) const { return d_kind != ch.d_kind; } - Kind getOperator() const { return d_kind; } -};/* class Chain */ - -inline std::ostream& operator<<(std::ostream& out, const Chain& ch) CVC4_PUBLIC; -inline std::ostream& operator<<(std::ostream& out, const Chain& ch) { - return out << ch.getOperator(); -} - -struct CVC4_PUBLIC ChainHashFunction { - size_t operator()(const Chain& ch) const { - return kind::KindHashFunction()(ch.getOperator()); - } -};/* struct ChainHashFunction */ - -}/* CVC4 namespace */ - -#endif /* CVC4__CHAIN_H */ diff --git a/src/expr/chain.i b/src/expr/chain.i deleted file mode 100644 index 8de1665ce..000000000 --- a/src/expr/chain.i +++ /dev/null @@ -1,12 +0,0 @@ -%{ -#include "expr/chain.h" -%} - -%rename(equals) CVC4::Chain::operator==(const Chain&) const; -%ignore CVC4::Chain::operator!=(const Chain&) const; - -%ignore CVC4::operator<<(std::ostream&, const Chain&); - -%rename(apply) CVC4::ChainHashFunction::operator()(const CVC4::Chain&) const; - -%include "expr/chain.h" |