diff options
author | Tim King <taking@google.com> | 2016-01-05 17:28:38 -0800 |
---|---|---|
committer | Tim King <taking@google.com> | 2016-01-05 17:28:38 -0800 |
commit | b5f91dae58691468f6c8f2d7c6aebf639f1d017b (patch) | |
tree | e6584f75105e4a3c1fa461b988286c0d649d42d3 /src | |
parent | 5eabda0f55cee3be81aa7ae126269c32e818322f (diff) |
Moving sexpr.{cpp,h,i} from expr/ back into util/.
Diffstat (limited to 'src')
-rw-r--r-- | src/compat/cvc3_compat.cpp | 3 | ||||
-rw-r--r-- | src/cvc4.i | 23 | ||||
-rw-r--r-- | src/expr/Makefile.am | 3 | ||||
-rw-r--r-- | src/expr/statistics.h | 4 | ||||
-rw-r--r-- | src/printer/printer.h | 2 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 2 | ||||
-rw-r--r-- | src/smt_util/command.cpp | 2 | ||||
-rw-r--r-- | src/smt_util/command.h | 2 | ||||
-rw-r--r-- | src/util/Makefile.am | 3 | ||||
-rw-r--r-- | src/util/sexpr.cpp (renamed from src/expr/sexpr.cpp) | 4 | ||||
-rw-r--r-- | src/util/sexpr.h (renamed from src/expr/sexpr.h) | 0 | ||||
-rw-r--r-- | src/util/sexpr.i (renamed from src/expr/sexpr.i) | 4 |
12 files changed, 24 insertions, 28 deletions
diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index 24c4d8112..9ae394b97 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -28,7 +28,6 @@ #include "expr/expr_iomanip.h" #include "expr/kind.h" #include "expr/predicate.h" -#include "expr/sexpr.h" #include "options/base_options.h" #include "options/expr_options.h" #include "options/parser_options.h" @@ -41,9 +40,9 @@ #include "util/hash.h" #include "util/integer.h" #include "util/rational.h" +#include "util/sexpr.h" #include "util/subrange_bound.h" - using namespace std; // Matches base/cvc4_assert.h's PrettyCheckArgument. diff --git a/src/cvc4.i b/src/cvc4.i index e81276f23..601c9a878 100644 --- a/src/cvc4.i +++ b/src/cvc4.i @@ -52,12 +52,12 @@ using namespace CVC4; #include "base/modal_exception.h" #include "expr/datatype.h" #include "expr/expr.h" -#include "expr/sexpr.h" #include "expr/type.h" #include "options/option_exception.h" #include "smt_util/command.h" -#include "util/integer.h" #include "util/bitvector.h" +#include "util/integer.h" +#include "util/sexpr.h" #include "util/unsafe_interrupt_exception.h" #ifdef SWIGJAVA @@ -306,25 +306,24 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters; // At the moment, the header includes seem to need to follow a special order. // I don't know why. I am following the build order %include "base/exception.i" -%include "util/unsafe_interrupt_exception.i" -%include "util/integer.i" -%include "util/rational.i" -%include "options/language.i" -%include "util/configuration.i" -%include "util/bool.i" -%include "util/cardinality.i" %include "base/modal_exception.i" -%include "expr/sexpr.i" - -%include "util/bitvector.i" +%include "options/language.i" +%include "util/bitvector.i" +%include "util/bool.i" +%include "util/cardinality.i" +%include "util/configuration.i" %include "util/hash.i" +%include "util/integer.i" %include "util/proof.i" +%include "util/rational.i" %include "util/regexp.i" %include "util/result.i" +%include "util/sexpr.i" %include "util/subrange_bound.i" %include "util/tuple.i" +%include "util/unsafe_interrupt_exception.i" //%include "util/floatingpoint.i" %include "expr/uninterpreted_constant.i" diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index d4964f56a..5c046c282 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -54,8 +54,6 @@ libexpr_la_SOURCES = \ pickler.h \ resource_manager.cpp \ resource_manager.h \ - sexpr.cpp \ - sexpr.h \ symbol_table.cpp \ symbol_table.h \ type.cpp \ @@ -109,7 +107,6 @@ EXTRA_DIST = \ kind.i \ expr.i \ resource_manager.i \ - sexpr.i \ record.i \ predicate.i \ variable_type_map.i \ diff --git a/src/expr/statistics.h b/src/expr/statistics.h index 425404692..a0b6ed083 100644 --- a/src/expr/statistics.h +++ b/src/expr/statistics.h @@ -20,14 +20,14 @@ #ifndef __CVC4__STATISTICS_H #define __CVC4__STATISTICS_H -#include "expr/sexpr.h" - #include <iterator> #include <ostream> #include <set> #include <string> #include <utility> +#include "util/sexpr.h" + namespace CVC4 { class Stat; diff --git a/src/printer/printer.h b/src/printer/printer.h index 48787f70a..ca9aff65d 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -23,10 +23,10 @@ #include <string> #include "expr/node.h" -#include "expr/sexpr.h" #include "options/language.h" #include "smt_util/command.h" #include "smt_util/model.h" +#include "util/sexpr.h" namespace CVC4 { diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 3f049e392..531b499ac 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -28,7 +28,6 @@ #include "context/cdlist_forward.h" #include "expr/expr.h" #include "expr/expr_manager.h" -#include "expr/sexpr.h" #include "expr/statistics.h" #include "options/options.h" #include "proof/unsat_core.h" @@ -38,6 +37,7 @@ #include "util/hash.h" #include "util/proof.h" #include "util/result.h" +#include "util/sexpr.h" #include "util/unsafe_interrupt_exception.h" // In terms of abstraction, this is below (and provides services to) diff --git a/src/smt_util/command.cpp b/src/smt_util/command.cpp index 5917d71da..8cc8a421c 100644 --- a/src/smt_util/command.cpp +++ b/src/smt_util/command.cpp @@ -27,7 +27,6 @@ #include "base/output.h" #include "expr/expr_iomanip.h" #include "expr/node.h" -#include "expr/sexpr.h" #include "options/options.h" #include "options/smt_options.h" #include "printer/printer.h" @@ -35,6 +34,7 @@ #include "smt/smt_engine_scope.h" #include "smt_util/dump.h" #include "smt_util/model.h" +#include "util/sexpr.h" using namespace std; diff --git a/src/smt_util/command.h b/src/smt_util/command.h index c9b968722..d8f9789f5 100644 --- a/src/smt_util/command.h +++ b/src/smt_util/command.h @@ -30,12 +30,12 @@ #include "expr/datatype.h" #include "expr/expr.h" -#include "expr/sexpr.h" #include "expr/type.h" #include "expr/variable_type_map.h" #include "proof/unsat_core.h" #include "util/proof.h" #include "util/result.h" +#include "util/sexpr.h" namespace CVC4 { diff --git a/src/util/Makefile.am b/src/util/Makefile.am index b06666ae3..d086e3068 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -45,6 +45,8 @@ libutil_la_SOURCES = \ regexp.h \ result.cpp \ result.h \ + sexpr.cpp \ + sexpr.h \ smt2_quote_string.cpp \ smt2_quote_string.h \ subrange_bound.cpp \ @@ -92,6 +94,7 @@ EXTRA_DIST = \ rational_gmp_imp.h \ regexp.i \ result.i \ + sexpr.i \ subrange_bound.i \ tuple.i \ unsafe_interrupt_exception.i diff --git a/src/expr/sexpr.cpp b/src/util/sexpr.cpp index 69741859f..eb53e34c2 100644 --- a/src/expr/sexpr.cpp +++ b/src/util/sexpr.cpp @@ -22,18 +22,16 @@ ** handled in the SExpr class and the libexpr library. **/ -#include "expr/sexpr.h" +#include "util/sexpr.h" #include <iostream> #include <sstream> #include <vector> #include "base/cvc4_assert.h" -#include "expr/expr.h" #include "options/set_language.h" #include "util/smt2_quote_string.h" - namespace CVC4 { const int PrettySExprs::s_iosIndex = std::ios_base::xalloc(); diff --git a/src/expr/sexpr.h b/src/util/sexpr.h index 40fd9dd56..40fd9dd56 100644 --- a/src/expr/sexpr.h +++ b/src/util/sexpr.h diff --git a/src/expr/sexpr.i b/src/util/sexpr.i index f6229782e..4c89c5019 100644 --- a/src/expr/sexpr.i +++ b/src/util/sexpr.i @@ -1,5 +1,5 @@ %{ -#include "expr/sexpr.h" +#include "util/sexpr.h" %} %ignore CVC4::operator<<(std::ostream&, const SExpr&); @@ -18,4 +18,4 @@ %rename(equals) CVC4::SExpr::operator==(const SExpr&) const; %ignore CVC4::SExpr::operator!=(const SExpr&) const; -%include "expr/sexpr.h" +%include "util/sexpr.h" |