diff options
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/CMakeLists.txt | 1 | ||||
-rw-r--r-- | src/expr/expr_stream.h | 45 | ||||
-rw-r--r-- | src/expr/expr_stream.i | 5 | ||||
-rw-r--r-- | src/expr/metakind_template.h | 14 | ||||
-rwxr-xr-x | src/expr/mkmetakind | 16 |
5 files changed, 0 insertions, 81 deletions
diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index 00bd121cb..a308e536c 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -12,7 +12,6 @@ libcvc4_add_sources( expr_iomanip.cpp expr_iomanip.h expr_manager_scope.h - expr_stream.h kind_map.h match_trie.cpp match_trie.h diff --git a/src/expr/expr_stream.h b/src/expr/expr_stream.h deleted file mode 100644 index d31e8e4fc..000000000 --- a/src/expr/expr_stream.h +++ /dev/null @@ -1,45 +0,0 @@ -/********************* */ -/*! \file expr_stream.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 A stream interface for expressions - ** - ** A stream interface for expressions. - **/ - -#include "cvc4_public.h" - -#ifndef CVC4__EXPR_STREAM_H -#define CVC4__EXPR_STREAM_H - -#include "expr/expr.h" - -namespace CVC4 { - -/** - * A pure-virtual stream interface for expressions. Can be used to - * communicate streams of expressions between different parts of CVC4. - */ -class CVC4_PUBLIC ExprStream { -public: - /** Virtual destructor; this implementation does nothing. */ - virtual ~ExprStream() {} - - /** - * Get the next expression in the stream (advancing the stream - * pointer as a side effect.) - */ - virtual Expr nextExpr() = 0; -};/* class ExprStream */ - -}/* CVC4 namespace */ - -#endif /* CVC4__EXPR_STREAM_H */ - diff --git a/src/expr/expr_stream.i b/src/expr/expr_stream.i deleted file mode 100644 index f1144623b..000000000 --- a/src/expr/expr_stream.i +++ /dev/null @@ -1,5 +0,0 @@ -%{ -#include "expr/expr_stream.h" -%} - -%include "expr/expr_stream.h" diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h index c4d35b7dc..fb1626adb 100644 --- a/src/expr/metakind_template.h +++ b/src/expr/metakind_template.h @@ -203,20 +203,6 @@ Kind operatorToKind(::CVC4::expr::NodeValue* nv); #line 205 "${template}" -namespace theory { - -static inline bool useTheoryValidate(std::string theory) { -${use_theory_validations} - return false; -} - -static const char *const useTheoryHelp = "\ -The following options are valid alternate implementations for use with\n\ -the --use-theory option:\n\ -\n\ -${theory_alternate_doc}"; - -}/* CVC4::theory namespace */ }/* CVC4 namespace */ #endif /* CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP */ diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind index fe8a152df..e2a733ec8 100755 --- a/src/expr/mkmetakind +++ b/src/expr/mkmetakind @@ -50,9 +50,6 @@ metakind_ubchildren= metakind_lbchildren= metakind_operatorKinds= -use_theory_validations= -theory_alternate_doc= - seen_theory=false seen_theory_builtin=false @@ -108,13 +105,6 @@ function alternate { theory_header="$4" theory_includes="${theory_includes}#include \"$theory_header\" " - - use_theory_validations="${use_theory_validations} - if(theory == \"$name\") { - return true; - }" - theory_alternate_doc="$theory_alternate_doc$name - alternate implementation for $theory_id\\n\\ -" } function properties { @@ -410,10 +400,6 @@ check_builtin_theory_seen nl -ba -s' ' "$template" | grep '^ *[0-9][0-9]* # *line' | awk '{OFS="";if($1+1!=$3) print "'"$template"':",$1,": warning: incorrect annotation \"#line ",$3,"\" (it should be \"#line ",($1+1),"\")"}' >&2 -if [ -z "$theory_alternate_doc" ]; then - theory_alternate_doc="[none defined]" -fi - text=$(cat "$template") for var in \ metakind_includes \ @@ -428,8 +414,6 @@ for var in \ metakind_ubchildren \ metakind_lbchildren \ metakind_operatorKinds \ - use_theory_validations \ - theory_alternate_doc \ template \ ; do eval text="\${text//\\\$\\{$var\\}/\${$var}}" |