diff options
63 files changed, 659 insertions, 494 deletions
diff --git a/contrib/test_install_headers.sh b/contrib/test_install_headers.sh new file mode 100755 index 000000000..6f6855e31 --- /dev/null +++ b/contrib/test_install_headers.sh @@ -0,0 +1,36 @@ +#!/bin/bash +# contrib/test_install_headers.sh +# Tim King <taking@google.com> for the CVC4 project, 24 December 2015 +# +# ./contrib/test_install_headers.sh <INSTALL> +# +# This files tests the completeness of the public headers for CVC4. +# Any header marked by #include "cvc4_public.h" in either the builds/ +# or src/ directory is installed into the path INSTALL/include/cvc4 where +# INSTALL is set using the --prefix=INSTALL flag at configure time. +# This test uses find to attempt to include all of the headers in +# INSTALL/include/cvc4 and compiles a simple cpp file. + +INSTALLATION=$1 +CXX=g++ +LDFLAGS=-lcln +CXXFILE=test_cvc4_header_install.cpp +OUTFILE=test_cvc4_header_install + +echo $INSTALLATION + +echo "Generating $CXXFILE" +find $INSTALLATION/include/cvc4/ -name *.h -printf '%P\n' | \ + awk '{ print "#include <cvc4/" $0 ">"}' > $CXXFILE +echo "int main() { return 0; }" >> $CXXFILE + +echo "Compiling $CXXFILE into $OUTFILE" +echo "$CXX -I$INSTALLATION/include -L$INSTALLATION/lib $LDFLAGS -o $OUTFILE $CXXFILE" +$CXX -I$INSTALLATION/include -L$INSTALLATION/lib $LDFLAGS -o $OUTFILE $CXXFILE + +read -p "Do you want to delete $CXXFILE and $OUTFILE? [y/n]" yn +case $yn in + [Nn]* ) exit;; + [Yy]* ) rm "$OUTFILE" "$CXXFILE";; + * ) echo "Did not get a yes or no answer. Exiting."; exit;; +esac diff --git a/examples/hashsmt/sha1_collision.cpp b/examples/hashsmt/sha1_collision.cpp index 9ed4424ba..984cbde13 100644 --- a/examples/hashsmt/sha1_collision.cpp +++ b/examples/hashsmt/sha1_collision.cpp @@ -28,6 +28,7 @@ #include <sstream> #include <string> +#include "expr/expr_iomanip.h" #include "options/language.h" #include "options/set_language.h" #include "sha1.hpp" diff --git a/examples/hashsmt/sha1_inversion.cpp b/examples/hashsmt/sha1_inversion.cpp index 15c7d8728..9aac7bbe0 100644 --- a/examples/hashsmt/sha1_inversion.cpp +++ b/examples/hashsmt/sha1_inversion.cpp @@ -28,6 +28,7 @@ #include <sstream> #include <string> +#include "expr/expr_iomanip.h" #include "options/language.h" #include "options/set_language.h" #include "sha1.hpp" diff --git a/examples/hashsmt/word.cpp b/examples/hashsmt/word.cpp index 2e638f64f..7aa37e91b 100644 --- a/examples/hashsmt/word.cpp +++ b/examples/hashsmt/word.cpp @@ -26,6 +26,12 @@ #include <vector> +#include "expr/expr.h" +#include "expr/expr_iomanip.h" +#include "options/base_options.h" +#include "options/language.h" +#include "options/options.h" + using namespace std; using namespace hashsmt; using namespace CVC4; @@ -66,7 +72,7 @@ Word Word::concat(const Word words[], unsigned size) { } void Word::print(ostream& out) const { - out << CVC4::Expr::setdepth(-1) << d_expr; + out << CVC4::expr::ExprSetDepth(-1) << d_expr; } Word::Word(unsigned newSize, unsigned value) { diff --git a/examples/nra-translate/normalize.cpp b/examples/nra-translate/normalize.cpp index db76390a7..56f326216 100644 --- a/examples/nra-translate/normalize.cpp +++ b/examples/nra-translate/normalize.cpp @@ -23,7 +23,9 @@ #include <vector> #include "expr/expr.h" +#include "expr/expr_iomanip.h" #include "options/language.h" +#include "options/base_options.h" #include "options/options.h" #include "options/set_language.h" #include "parser/parser.h" @@ -49,7 +51,7 @@ int main(int argc, char* argv[]) ExprManager exprManager(options); cout << language::SetLanguage(language::output::LANG_SMTLIB_V2) - << Expr::setdepth(-1); + << expr::ExprSetDepth(-1); // Create the parser ParserBuilder parserBuilder(&exprManager, input, options); diff --git a/examples/nra-translate/smt2info.cpp b/examples/nra-translate/smt2info.cpp index d59f9f4c4..c541a23fe 100644 --- a/examples/nra-translate/smt2info.cpp +++ b/examples/nra-translate/smt2info.cpp @@ -22,6 +22,7 @@ #include <vector> #include "expr/expr.h" +#include "options/base_options.h" #include "options/options.h" #include "parser/parser.h" #include "parser/parser_builder.h" diff --git a/examples/nra-translate/smt2todreal.cpp b/examples/nra-translate/smt2todreal.cpp index 97c5c5d04..56f323812 100644 --- a/examples/nra-translate/smt2todreal.cpp +++ b/examples/nra-translate/smt2todreal.cpp @@ -23,6 +23,8 @@ #include <vector> #include "expr/expr.h" +#include "expr/expr_iomanip.h" +#include "options/base_options.h" #include "options/options.h" #include "parser/parser.h" #include "parser/parser_builder.h" @@ -46,7 +48,7 @@ int main(int argc, char* argv[]) options.set(outputLanguage, language::output::LANG_SMTLIB_V2); ExprManager exprManager(options); - cout << Expr::dag(0) << Expr::setdepth(-1); + cout << expr::ExprDag(0) << expr::ExprSetDepth(-1); // Create the parser ParserBuilder parserBuilder(&exprManager, input, options); diff --git a/examples/nra-translate/smt2toisat.cpp b/examples/nra-translate/smt2toisat.cpp index 9c94cdd43..8eb46dd2f 100644 --- a/examples/nra-translate/smt2toisat.cpp +++ b/examples/nra-translate/smt2toisat.cpp @@ -23,6 +23,7 @@ #include <vector> #include "expr/expr.h" +#include "options/base_options.h" #include "options/options.h" #include "parser/parser.h" #include "parser/parser_builder.h" diff --git a/examples/nra-translate/smt2tomathematica.cpp b/examples/nra-translate/smt2tomathematica.cpp index 86aaf786f..0ad5bbab5 100644 --- a/examples/nra-translate/smt2tomathematica.cpp +++ b/examples/nra-translate/smt2tomathematica.cpp @@ -23,6 +23,7 @@ #include <vector> #include "expr/expr.h" +#include "options/base_options.h" #include "options/options.h" #include "parser/parser.h" #include "parser/parser_builder.h" diff --git a/examples/nra-translate/smt2toqepcad.cpp b/examples/nra-translate/smt2toqepcad.cpp index 058fa8e0d..c74b0a110 100644 --- a/examples/nra-translate/smt2toqepcad.cpp +++ b/examples/nra-translate/smt2toqepcad.cpp @@ -23,6 +23,7 @@ #include <vector> #include "expr/expr.h" +#include "options/base_options.h" #include "options/options.h" #include "parser/parser.h" #include "parser/parser_builder.h" diff --git a/examples/nra-translate/smt2toredlog.cpp b/examples/nra-translate/smt2toredlog.cpp index 1ebd6ea59..7a6f87122 100644 --- a/examples/nra-translate/smt2toredlog.cpp +++ b/examples/nra-translate/smt2toredlog.cpp @@ -23,6 +23,7 @@ #include <vector> #include "expr/expr.h" +#include "options/base_options.h" #include "options/options.h" #include "parser/parser.h" #include "parser/parser_builder.h" diff --git a/examples/sets-translate/sets_translate.cpp b/examples/sets-translate/sets_translate.cpp index 7e17e68f4..aef3843f8 100644 --- a/examples/sets-translate/sets_translate.cpp +++ b/examples/sets-translate/sets_translate.cpp @@ -24,6 +24,7 @@ #include "expr/expr.h" #include "options/language.h" +#include "options/base_options.h" #include "options/options.h" #include "options/set_language.h" #include "parser/parser.h" diff --git a/examples/translator.cpp b/examples/translator.cpp index 7d5e912e7..248dadd5f 100644 --- a/examples/translator.cpp +++ b/examples/translator.cpp @@ -23,6 +23,8 @@ #include <iostream> #include "expr/expr.h" +#include "expr/expr_iomanip.h" +#include "options/base_options.h" #include "options/language.h" #include "options/set_language.h" #include "parser/parser.h" @@ -211,7 +213,7 @@ int main(int argc, char* argv[]) { switch(c) { case 1: ++files; - *out << Expr::dag(dag_thresh); + *out << expr::ExprDag(dag_thresh); readFile(optarg, (!strcmp(optarg, "-") && fromLang == input::LANG_AUTO) ? input::LANG_CVC4 : fromLang, toLang, expand_definitions, combine_assertions, out); break; case INPUT_LANG: @@ -276,7 +278,7 @@ int main(int argc, char* argv[]) { } if(files == 0) { - *out << Expr::dag(dag_thresh); + *out << expr::ExprDag(dag_thresh); readFile("-", fromLang == input::LANG_AUTO ? input::LANG_CVC4 : fromLang, toLang, expand_definitions, combine_assertions, out); exit(0); } diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index 3fa790f3e..24c4d8112 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -25,9 +25,11 @@ #include "base/exception.h" #include "base/output.h" +#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" #include "options/set_language.h" @@ -1560,8 +1562,8 @@ void ValidityChecker::printExpr(const Expr& e) { } void ValidityChecker::printExpr(const Expr& e, std::ostream& os) { - Expr::setdepth::Scope sd(os, -1); - Expr::printtypes::Scope pt(os, false); + CVC4::expr::ExprSetDepth::Scope sd(os, -1); + CVC4::expr::ExprPrintTypes::Scope pt(os, false); CVC4::language::SetLanguage::Scope sl(os, d_em->getOptions()[CVC4::options::outputLanguage]); os << e; } diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index dc6ad5833..63f31ed67 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -32,6 +32,8 @@ libexpr_la_SOURCES = \ chain.h \ emptyset.cpp \ emptyset.h \ + expr_iomanip.cpp \ + expr_iomanip.h \ expr_manager_scope.h \ expr_stream.h \ kind_map.h \ diff --git a/src/expr/expr_iomanip.cpp b/src/expr/expr_iomanip.cpp new file mode 100644 index 000000000..4c7ab3c8b --- /dev/null +++ b/src/expr/expr_iomanip.cpp @@ -0,0 +1,160 @@ +/********************* */ +/*! \file expr_iomanip.cpp + ** \verbatim + ** Original author: Tim King + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2015 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Expr IO manipulation classes. + ** + ** Expr IO manipulation classes. + **/ + +#include "expr/expr_iomanip.h" + +#include <iomanip> +#include <iostream> + +#include "options/options.h" +#include "options/expr_options.h" + +namespace CVC4 { +namespace expr { + +const int ExprSetDepth::s_iosIndex = std::ios_base::xalloc(); +const int ExprPrintTypes::s_iosIndex = std::ios_base::xalloc(); +const int ExprDag::s_iosIndex = std::ios_base::xalloc(); + + + +ExprSetDepth::ExprSetDepth(long depth) : d_depth(depth) {} + +void ExprSetDepth::applyDepth(std::ostream& out) { + out.iword(s_iosIndex) = d_depth; +} + +long ExprSetDepth::getDepth(std::ostream& out) { + long& l = out.iword(s_iosIndex); + if(l == 0) { + // set the default print depth on this ostream + if(not Options::isCurrentNull()) { + l = options::defaultExprDepth(); + } + if(l == 0) { + // if called from outside the library, we may not have options + // available to us at this point (or perhaps the output language + // is not set in Options). Default to something reasonable, but + // don't set "l" since that would make it "sticky" for this + // stream. + return s_defaultPrintDepth; + } + } + return l; +} + +void ExprSetDepth::setDepth(std::ostream& out, long depth) { + out.iword(s_iosIndex) = depth; +} + + +ExprSetDepth::Scope::Scope(std::ostream& out, long depth) + : d_out(out), d_oldDepth(ExprSetDepth::getDepth(out)) +{ + ExprSetDepth::setDepth(out, depth); +} + +ExprSetDepth::Scope::~Scope() { + ExprSetDepth::setDepth(d_out, d_oldDepth); +} + + +ExprPrintTypes::ExprPrintTypes(bool printTypes) : d_printTypes(printTypes) {} + +void ExprPrintTypes::applyPrintTypes(std::ostream& out) { + out.iword(s_iosIndex) = d_printTypes; +} + +bool ExprPrintTypes::getPrintTypes(std::ostream& out) { + return out.iword(s_iosIndex); +} + +void ExprPrintTypes::setPrintTypes(std::ostream& out, bool printTypes) { + out.iword(s_iosIndex) = printTypes; +} + +ExprPrintTypes::Scope::Scope(std::ostream& out, bool printTypes) + : d_out(out), + d_oldPrintTypes(ExprPrintTypes::getPrintTypes(out)) { + ExprPrintTypes::setPrintTypes(out, printTypes); +} + +ExprPrintTypes::Scope::~Scope() { + ExprPrintTypes::setPrintTypes(d_out, d_oldPrintTypes); +} + +ExprDag::ExprDag(bool dag) : d_dag(dag ? 1 : 0) {} + +ExprDag::ExprDag(int dag) : d_dag(dag < 0 ? 0 : dag) {} + +void ExprDag::applyDag(std::ostream& out) { + // (offset by one to detect whether default has been set yet) + out.iword(s_iosIndex) = static_cast<long>(d_dag) + 1; +} + +size_t ExprDag::getDag(std::ostream& out) { + long& l = out.iword(s_iosIndex); + if(l == 0) { + // set the default dag setting on this ostream + // (offset by one to detect whether default has been set yet) + if(not Options::isCurrentNull()) { + l = options::defaultDagThresh() + 1; + } + if(l == 0) { + // if called from outside the library, we may not have options + // available to us at this point (or perhaps the output language + // is not set in Options). Default to something reasonable, but + // don't set "l" since that would make it "sticky" for this + // stream. + return s_defaultDag + 1; + } + } + return static_cast<size_t>(l - 1); +} + +void ExprDag::setDag(std::ostream& out, size_t dag) { + // (offset by one to detect whether default has been set yet) + out.iword(s_iosIndex) = static_cast<long>(dag) + 1; +} + +ExprDag::Scope::Scope(std::ostream& out, size_t dag) + : d_out(out), + d_oldDag(ExprDag::getDag(out)) { + ExprDag::setDag(out, dag); +} + +ExprDag::Scope::~Scope() { + ExprDag::setDag(d_out, d_oldDag); +} + +std::ostream& operator<<(std::ostream& out, ExprDag d) { + d.applyDag(out); + return out; +} + +std::ostream& operator<<(std::ostream& out, ExprPrintTypes pt) { + pt.applyPrintTypes(out); + return out; +} + +std::ostream& operator<<(std::ostream& out, ExprSetDepth sd) { + sd.applyDepth(out); + return out; +} + + +}/* namespace CVC4::expr */ +}/* namespace CVC4 */ diff --git a/src/expr/expr_iomanip.h b/src/expr/expr_iomanip.h new file mode 100644 index 000000000..b3370e75a --- /dev/null +++ b/src/expr/expr_iomanip.h @@ -0,0 +1,239 @@ +/********************* */ +/*! \file expr_iomanip.h + ** \verbatim + ** Original author: Tim King + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2015 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Expr IO manipulation classes. + ** + ** Expr IO manipulation classes. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__EXPR__EXPR_IOMANIP_H +#define __CVC4__EXPR__EXPR_IOMANIP_H + +#include <iosfwd> + +namespace CVC4 { +namespace expr { + +/** + * IOStream manipulator to set the maximum depth of Exprs when + * pretty-printing. -1 means print to any depth. E.g.: + * + * // let a, b, c, and d be VARIABLEs + * Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d))) + * out << setdepth(3) << e; + * + * gives "(OR a b (AND c (NOT d)))", but + * + * out << setdepth(1) << [same expr as above] + * + * gives "(OR a b (...))". + * + * The implementation of this class serves two purposes; it holds + * information about the depth setting (such as the index of the + * allocated word in ios_base), and serves also as the manipulator + * itself (as above). + */ +class CVC4_PUBLIC ExprSetDepth { +public: + + /** + * Construct a ExprSetDepth with the given depth. + */ + ExprSetDepth(long depth); + + void applyDepth(std::ostream& out); + + static long getDepth(std::ostream& out); + + static void setDepth(std::ostream& out, long depth); + + /** + * Set the expression depth on the output stream for the current + * stack scope. This makes sure the old depth is reset on the stream + * after normal OR exceptional exit from the scope, using the RAII + * C++ idiom. + */ + class Scope { + public: + Scope(std::ostream& out, long depth); + ~Scope(); + + private: + std::ostream& d_out; + long d_oldDepth; + };/* class ExprSetDepth::Scope */ + + private: + /** + * The allocated index in ios_base for our depth setting. + */ + static const int s_iosIndex; + + /** + * The default depth to print, for ostreams that haven't yet had a + * setdepth() applied to them. + */ + static const int s_defaultPrintDepth = -1; + + /** + * When this manipulator is used, the depth is stored here. + */ + long d_depth; +};/* class ExprSetDepth */ + +/** + * IOStream manipulator to print type ascriptions or not. + * + * // let a, b, c, and d be variables of sort U + * Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d))) + * out << e; + * + * gives "(OR a:U b:U (AND c:U (NOT d:U)))", but + */ +class CVC4_PUBLIC ExprPrintTypes { +public: + /** + * Construct a ExprPrintTypes with the given setting. + */ + ExprPrintTypes(bool printTypes); + + void applyPrintTypes(std::ostream& out); + + static bool getPrintTypes(std::ostream& out); + + static void setPrintTypes(std::ostream& out, bool printTypes); + + /** + * Set the print-types state on the output stream for the current + * stack scope. This makes sure the old state is reset on the + * stream after normal OR exceptional exit from the scope, using the + * RAII C++ idiom. + */ + class Scope { + public: + Scope(std::ostream& out, bool printTypes); + ~Scope(); + + private: + std::ostream& d_out; + bool d_oldPrintTypes; + };/* class ExprPrintTypes::Scope */ + + private: + /** + * The allocated index in ios_base for our setting. + */ + static const int s_iosIndex; + + /** + * When this manipulator is used, the setting is stored here. + */ + bool d_printTypes; +};/* class ExprPrintTypes */ + +/** + * IOStream manipulator to print expressions as a dag (or not). + */ +class CVC4_PUBLIC ExprDag { +public: + /** + * Construct a ExprDag with the given setting (dagification on or off). + */ + explicit ExprDag(bool dag); + + /** + * Construct a ExprDag with the given setting (letify only common + * subexpressions that appear more than 'dag' times). dag <= 0 means + * don't dagify. + */ + explicit ExprDag(int dag); + + void applyDag(std::ostream& out); + + static size_t getDag(std::ostream& out); + + static void setDag(std::ostream& out, size_t dag); + + /** + * Set the dag state on the output stream for the current + * stack scope. This makes sure the old state is reset on the + * stream after normal OR exceptional exit from the scope, using the + * RAII C++ idiom. + */ + class Scope { + public: + Scope(std::ostream& out, size_t dag); + ~Scope(); + + private: + std::ostream& d_out; + size_t d_oldDag; + };/* class ExprDag::Scope */ + + private: + /** + * The allocated index in ios_base for our setting. + */ + static const int s_iosIndex; + + /** + * The default setting, for ostreams that haven't yet had a + * dag() applied to them. + */ + static const size_t s_defaultDag = 1; + + /** + * When this manipulator is used, the setting is stored here. + */ + size_t d_dag; +};/* class ExprDag */ + +/** + * Sets the default dag setting when pretty-printing a Expr to an ostream. + * Use like this: + * + * // let out be an ostream, e an Expr + * out << Expr::dag(true) << e << endl; + * + * The setting stays permanently (until set again) with the stream. + */ +std::ostream& operator<<(std::ostream& out, ExprDag d) CVC4_PUBLIC; + + +/** + * Sets the default print-types setting when pretty-printing an Expr + * to an ostream. Use like this: + * + * // let out be an ostream, e an Expr + * out << Expr::printtypes(true) << e << endl; + * + * The setting stays permanently (until set again) with the stream. + */ +std::ostream& operator<<(std::ostream& out, ExprPrintTypes pt) CVC4_PUBLIC; + +/** + * Sets the default depth when pretty-printing a Expr to an ostream. + * Use like this: + * + * // let out be an ostream, e an Expr + * out << Expr::setdepth(n) << e << endl; + * + * The depth stays permanently (until set again) with the stream. + */ +std::ostream& operator<<(std::ostream& out, ExprSetDepth sd) CVC4_PUBLIC; + +}/* namespace CVC4::expr */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__EXPR__EXPR_IOMANIP_H */ diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index dfbe179be..a6cdedd00 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -40,14 +40,6 @@ namespace CVC4 { class ExprManager; -namespace expr { - -const int ExprSetDepth::s_iosIndex = std::ios_base::xalloc(); -const int ExprPrintTypes::s_iosIndex = std::ios_base::xalloc(); -const int ExprDag::s_iosIndex = std::ios_base::xalloc(); - -}/* CVC4::expr namespace */ - std::ostream& operator<<(std::ostream& out, const TypeCheckingException& e) { return out << e.getMessage() << ": " << e.getExpression(); } diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 2e2f17742..7d82cb222 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -33,7 +33,6 @@ ${includes} #include <string> #include "base/exception.h" -#include "options/expr_options.h" #include "options/language.h" #include "util/hash.h" @@ -77,10 +76,6 @@ namespace smt { }/* CVC4::smt namespace */ namespace expr { - class CVC4_PUBLIC ExprSetDepth; - class CVC4_PUBLIC ExprPrintTypes; - class CVC4_PUBLIC ExprDag; - class ExportPrivate; }/* CVC4::expr namespace */ @@ -513,42 +508,6 @@ public: Expr exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap, uint32_t flags = 0) const; /** - * IOStream manipulator to set the maximum depth of Exprs when - * pretty-printing. -1 means print to any depth. E.g.: - * - * // let a, b, c, and d be VARIABLEs - * Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d))) - * out << setdepth(3) << e; - * - * gives "(OR a b (AND c (NOT d)))", but - * - * out << setdepth(1) << [same expr as above] - * - * gives "(OR a b (...))" - */ - typedef expr::ExprSetDepth setdepth; - - /** - * IOStream manipulator to print type ascriptions or not. - * - * // let a, b, c, and d be variables of sort U - * Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d))) - * out << printtypes(true) << e; - * - * gives "(OR a:U b:U (AND c:U (NOT d:U)))", but - * - * out << printtypes(false) << [same expr as above] - * - * gives "(OR a b (AND c (NOT d)))" - */ - typedef expr::ExprPrintTypes printtypes; - - /** - * IOStream manipulator to print expressions as a DAG (or not). - */ - typedef expr::ExprDag dag; - - /** * Very basic pretty printer for Expr. * This is equivalent to calling e.getNode().printAst(...) * @param out output stream to print to. @@ -592,307 +551,10 @@ private: };/* class Expr */ -namespace expr { - -/** - * IOStream manipulator to set the maximum depth of Exprs when - * pretty-printing. -1 means print to any depth. E.g.: - * - * // let a, b, c, and d be VARIABLEs - * Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d))) - * out << setdepth(3) << e; - * - * gives "(OR a b (AND c (NOT d)))", but - * - * out << setdepth(1) << [same expr as above] - * - * gives "(OR a b (...))". - * - * The implementation of this class serves two purposes; it holds - * information about the depth setting (such as the index of the - * allocated word in ios_base), and serves also as the manipulator - * itself (as above). - */ -class CVC4_PUBLIC ExprSetDepth { - /** - * The allocated index in ios_base for our depth setting. - */ - static const int s_iosIndex; - - /** - * The default depth to print, for ostreams that haven't yet had a - * setdepth() applied to them. - */ - static const int s_defaultPrintDepth = -1; - - /** - * When this manipulator is used, the depth is stored here. - */ - long d_depth; - -public: - /** - * Construct a ExprSetDepth with the given depth. - */ - ExprSetDepth(long depth) : d_depth(depth) {} - - inline void applyDepth(std::ostream& out) { - out.iword(s_iosIndex) = d_depth; - } - - static inline long getDepth(std::ostream& out) { - long& l = out.iword(s_iosIndex); - if(l == 0) { - // set the default print depth on this ostream - if(not Options::isCurrentNull()) { - l = options::defaultExprDepth(); - } - if(l == 0) { - // if called from outside the library, we may not have options - // available to us at this point (or perhaps the output language - // is not set in Options). Default to something reasonable, but - // don't set "l" since that would make it "sticky" for this - // stream. - return s_defaultPrintDepth; - } - } - return l; - } - - static inline void setDepth(std::ostream& out, long depth) { - out.iword(s_iosIndex) = depth; - } - - /** - * Set the expression depth on the output stream for the current - * stack scope. This makes sure the old depth is reset on the stream - * after normal OR exceptional exit from the scope, using the RAII - * C++ idiom. - */ - class Scope { - std::ostream& d_out; - long d_oldDepth; - - public: - - inline Scope(std::ostream& out, long depth) : - d_out(out), - d_oldDepth(ExprSetDepth::getDepth(out)) { - ExprSetDepth::setDepth(out, depth); - } - - inline ~Scope() { - ExprSetDepth::setDepth(d_out, d_oldDepth); - } - - };/* class ExprSetDepth::Scope */ - -};/* class ExprSetDepth */ - -/** - * IOStream manipulator to print type ascriptions or not. - * - * // let a, b, c, and d be variables of sort U - * Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d))) - * out << e; - * - * gives "(OR a:U b:U (AND c:U (NOT d:U)))", but - */ -class CVC4_PUBLIC ExprPrintTypes { - /** - * The allocated index in ios_base for our setting. - */ - static const int s_iosIndex; - - /** - * When this manipulator is used, the setting is stored here. - */ - bool d_printTypes; - -public: - /** - * Construct a ExprPrintTypes with the given setting. - */ - ExprPrintTypes(bool printTypes) : d_printTypes(printTypes) {} - - inline void applyPrintTypes(std::ostream& out) { - out.iword(s_iosIndex) = d_printTypes; - } - - static inline bool getPrintTypes(std::ostream& out) { - return out.iword(s_iosIndex); - } - - static inline void setPrintTypes(std::ostream& out, bool printTypes) { - out.iword(s_iosIndex) = printTypes; - } - - /** - * Set the print-types state on the output stream for the current - * stack scope. This makes sure the old state is reset on the - * stream after normal OR exceptional exit from the scope, using the - * RAII C++ idiom. - */ - class Scope { - std::ostream& d_out; - bool d_oldPrintTypes; - - public: - - inline Scope(std::ostream& out, bool printTypes) : - d_out(out), - d_oldPrintTypes(ExprPrintTypes::getPrintTypes(out)) { - ExprPrintTypes::setPrintTypes(out, printTypes); - } - - inline ~Scope() { - ExprPrintTypes::setPrintTypes(d_out, d_oldPrintTypes); - } - - };/* class ExprPrintTypes::Scope */ - -};/* class ExprPrintTypes */ - -/** - * IOStream manipulator to print expressions as a dag (or not). - */ -class CVC4_PUBLIC ExprDag { - /** - * The allocated index in ios_base for our setting. - */ - static const int s_iosIndex; - - /** - * The default setting, for ostreams that haven't yet had a - * dag() applied to them. - */ - static const size_t s_defaultDag = 1; - - /** - * When this manipulator is used, the setting is stored here. - */ - size_t d_dag; - -public: - /** - * Construct a ExprDag with the given setting (dagification on or off). - */ - explicit ExprDag(bool dag) : d_dag(dag ? 1 : 0) {} - - /** - * Construct a ExprDag with the given setting (letify only common - * subexpressions that appear more than 'dag' times). dag <= 0 means - * don't dagify. - */ - explicit ExprDag(int dag) : d_dag(dag < 0 ? 0 : dag) {} - - inline void applyDag(std::ostream& out) { - // (offset by one to detect whether default has been set yet) - out.iword(s_iosIndex) = static_cast<long>(d_dag) + 1; - } - - static inline size_t getDag(std::ostream& out) { - long& l = out.iword(s_iosIndex); - if(l == 0) { - // set the default dag setting on this ostream - // (offset by one to detect whether default has been set yet) - if(not Options::isCurrentNull()) { - l = options::defaultDagThresh() + 1; - } - if(l == 0) { - // if called from outside the library, we may not have options - // available to us at this point (or perhaps the output language - // is not set in Options). Default to something reasonable, but - // don't set "l" since that would make it "sticky" for this - // stream. - return s_defaultDag + 1; - } - } - return static_cast<size_t>(l - 1); - } - - static inline void setDag(std::ostream& out, size_t dag) { - // (offset by one to detect whether default has been set yet) - out.iword(s_iosIndex) = static_cast<long>(dag) + 1; - } - - /** - * Set the dag state on the output stream for the current - * stack scope. This makes sure the old state is reset on the - * stream after normal OR exceptional exit from the scope, using the - * RAII C++ idiom. - */ - class Scope { - std::ostream& d_out; - size_t d_oldDag; - - public: - - inline Scope(std::ostream& out, size_t dag) : - d_out(out), - d_oldDag(ExprDag::getDag(out)) { - ExprDag::setDag(out, dag); - } - - inline ~Scope() { - ExprDag::setDag(d_out, d_oldDag); - } - - };/* class ExprDag::Scope */ - -};/* class ExprDag */ -}/* CVC4::expr namespace */ - ${getConst_instantiations} #line 939 "${template}" -namespace expr { - -/** - * Sets the default depth when pretty-printing a Expr to an ostream. - * Use like this: - * - * // let out be an ostream, e an Expr - * out << Expr::setdepth(n) << e << endl; - * - * The depth stays permanently (until set again) with the stream. - */ -inline std::ostream& operator<<(std::ostream& out, ExprSetDepth sd) { - sd.applyDepth(out); - return out; -} - -/** - * Sets the default print-types setting when pretty-printing an Expr - * to an ostream. Use like this: - * - * // let out be an ostream, e an Expr - * out << Expr::printtypes(true) << e << endl; - * - * The setting stays permanently (until set again) with the stream. - */ -inline std::ostream& operator<<(std::ostream& out, ExprPrintTypes pt) { - pt.applyPrintTypes(out); - return out; -} - -/** - * Sets the default dag setting when pretty-printing a Expr to an ostream. - * Use like this: - * - * // let out be an ostream, e an Expr - * out << Expr::dag(true) << e << endl; - * - * The setting stays permanently (until set again) with the stream. - */ -inline std::ostream& operator<<(std::ostream& out, ExprDag d) { - d.applyDag(out); - return out; -} - -}/* CVC4::expr namespace */ - inline size_t ExprHashFunction::operator()(CVC4::Expr e) const { return (size_t) e.getId(); } diff --git a/src/expr/node.h b/src/expr/node.h index f345ba552..c0e2a5542 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -37,6 +37,7 @@ #include "expr/kind.h" #include "expr/metakind.h" #include "expr/expr.h" +#include "expr/expr_iomanip.h" #include "options/language.h" #include "options/set_language.h" #include "util/configuration.h" diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index dbe7d09eb..ab18973cb 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -24,6 +24,7 @@ #include "expr/kind.h" #include "expr/metakind.h" #include "expr/node.h" +#include "options/base_options.h" #include "options/language.h" #include "options/options.h" #include "printer/printer.h" diff --git a/src/expr/statistics_registry.cpp b/src/expr/statistics_registry.cpp index bf36236f7..3f9124a2f 100644 --- a/src/expr/statistics_registry.cpp +++ b/src/expr/statistics_registry.cpp @@ -21,10 +21,8 @@ #include "expr/expr_manager.h" #include "lib/clock_gettime.h" #include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" -#ifndef __BUILDING_STATISTICS_FOR_EXPORT -# include "smt/smt_engine_scope.h" -#endif /* ! __BUILDING_STATISTICS_FOR_EXPORT */ #ifdef CVC4_STATISTICS_ON # define __CVC4_USE_STATISTICS true @@ -65,8 +63,6 @@ inline StatisticsRegistry* getStatisticsRegistry(ExprManager* em) { }/* CVC4::stats namespace */ -#ifndef __BUILDING_STATISTICS_FOR_EXPORT - StatisticsRegistry* StatisticsRegistry::current() { return stats::getStatisticsRegistry(smt::currentSmtEngine()); } @@ -91,8 +87,6 @@ void StatisticsRegistry::unregisterStat(Stat* s) throw(CVC4::IllegalArgumentExce #endif /* CVC4_STATISTICS_ON */ }/* StatisticsRegistry::unregisterStat() */ -#endif /* ! __BUILDING_STATISTICS_FOR_EXPORT */ - void StatisticsRegistry::registerStat_(Stat* s) throw(CVC4::IllegalArgumentException) { #ifdef CVC4_STATISTICS_ON PrettyCheckArgument(d_stats.find(s) == d_stats.end(), s); diff --git a/src/expr/statistics_registry.h b/src/expr/statistics_registry.h index 4793f1301..3feb0d5d7 100644 --- a/src/expr/statistics_registry.h +++ b/src/expr/statistics_registry.h @@ -32,7 +32,6 @@ #include "base/exception.h" #include "expr/statistics.h" -#include "lib/clock_gettime.h" namespace CVC4 { @@ -617,10 +616,10 @@ public: d_prefix = d_name = name; } -#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) && !defined(__BUILDING_STATISTICS_FOR_EXPORT) +#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) /** Get a pointer to the current statistics registry */ static StatisticsRegistry* current(); -#endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST) && ! __BUILDING_STATISTICS_FOR_EXPORT */ +#endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST) */ /** Overridden to avoid the name being printed */ void flushStat(std::ostream &out) const; @@ -638,13 +637,13 @@ public: return SExpr(v); } -#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) && !defined(__BUILDING_STATISTICS_FOR_EXPORT) +#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) /** Register a new statistic, making it active. */ static void registerStat(Stat* s) throw(CVC4::IllegalArgumentException); /** Unregister an active statistic, making it inactive. */ static void unregisterStat(Stat* s) throw(CVC4::IllegalArgumentException); -#endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB) && ! __BUILDING_STATISTICS_FOR_EXPORT */ +#endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB) */ /** Register a new statistic */ void registerStat_(Stat* s) throw(CVC4::IllegalArgumentException); @@ -887,7 +886,7 @@ class RegisterStatistic { public: -#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) && ! defined(__BUILDING_STATISTICS_FOR_EXPORT) +#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) RegisterStatistic(Stat* stat) : d_reg(StatisticsRegistry::current()), d_stat(stat) { @@ -896,7 +895,7 @@ public: } StatisticsRegistry::registerStat(d_stat); } -#endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST) && ! __BUILDING_STATISTICS_FOR_EXPORT */ +#endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST) */ RegisterStatistic(StatisticsRegistry* reg, Stat* stat) : d_reg(reg), diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 659e80550..ea185f98b 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -13,12 +13,14 @@ ** ** Reference-counted encapsulation of a pointer to node information. **/ +#include "expr/type_node.h" #include <vector> #include "expr/node_manager_attributes.h" -#include "expr/type_node.h" #include "expr/type_properties.h" +#include "options/base_options.h" +#include "options/expr_options.h" using namespace std; @@ -564,4 +566,12 @@ bool TypeNode::isSortConstructor() const { return getKind() == kind::SORT_TYPE && hasAttribute(expr::SortArityAttr()); } +std::string TypeNode::toString() const { + std::stringstream ss; + OutputLanguage outlang = (this == &s_null) ? language::output::LANG_AUTO : options::outputLanguage(); + d_nv->toStream(ss, -1, false, 0, outlang); + return ss.str(); +} + + }/* CVC4 namespace */ diff --git a/src/expr/type_node.h b/src/expr/type_node.h index ce006a4f1..59f602f09 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -372,12 +372,7 @@ public: * * @return the string representation of this type. */ - inline std::string toString() const { - std::stringstream ss; - OutputLanguage outlang = (this == &s_null) ? language::output::LANG_AUTO : options::outputLanguage(); - d_nv->toStream(ss, -1, false, 0, outlang); - return ss.str(); - } + std::string toString() const; /** * Converts this node into a string representation and sends it to the diff --git a/src/lib/clock_gettime.h b/src/lib/clock_gettime.h index e065466f2..daae9aabf 100644 --- a/src/lib/clock_gettime.h +++ b/src/lib/clock_gettime.h @@ -14,7 +14,7 @@ ** Replacement for clock_gettime() for systems without it (like Mac OS X). **/ -#include "cvc4_public.h" +#include "cvc4_private.h" #ifndef __CVC4__LIB__CLOCK_GETTIME_H #define __CVC4__LIB__CLOCK_GETTIME_H diff --git a/src/lib/ffs.h b/src/lib/ffs.h index 2dc51d0e9..44fb40674 100644 --- a/src/lib/ffs.h +++ b/src/lib/ffs.h @@ -14,11 +14,14 @@ ** Replacement for ffs() for systems without it (like Win32). **/ -#include "cvc4_public.h" +#include "cvc4_private.h" #ifndef __CVC4__LIB__FFS_H #define __CVC4__LIB__FFS_H +//We include this for HAVE_FFS +#include "cvc4autoconfig.h" + #ifdef HAVE_FFS // available in strings.h diff --git a/src/lib/strtok_r.h b/src/lib/strtok_r.h index 644ff7a31..cc737043b 100644 --- a/src/lib/strtok_r.h +++ b/src/lib/strtok_r.h @@ -14,7 +14,7 @@ ** Replacement for strtok_r() for systems without it (like Win32). **/ -#include "cvc4_public.h" +#include "cvc4_private.h" #ifndef __CVC4__LIB__STRTOK_R_H #define __CVC4__LIB__STRTOK_R_H diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index 0b53c3cbe..aa43cff0f 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -22,6 +22,7 @@ #include <string> #include "main/main.h" +#include "options/base_options.h" #include "options/main_options.h" #include "options/printer_options.h" #include "options/smt_options.h" diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp index a1f737d1d..c471ae585 100644 --- a/src/main/command_executor_portfolio.cpp +++ b/src/main/command_executor_portfolio.cpp @@ -31,6 +31,7 @@ #include "expr/pickler.h" #include "main/main.h" #include "main/portfolio.h" +#include "options/base_options.h" #include "options/main_options.h" #include "options/options.h" #include "options/printer_options.h" diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 7e82e1bd1..3ad26c6a2 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -22,8 +22,11 @@ #include <iostream> #include <new> -#include "base/output.h" +// This must come before PORTFOLIO_BUILD. #include "cvc4autoconfig.h" + +#include "base/output.h" +#include "expr/expr_iomanip.h" #include "expr/expr_manager.h" #include "expr/result.h" #include "expr/statistics_registry.h" @@ -35,6 +38,7 @@ #include "main/interactive_shell.h" #include "main/main.h" +#include "options/base_options.h" #include "options/main_options.h" #include "options/options.h" #include "options/quantifiers_options.h" @@ -284,7 +288,8 @@ int runCvc4(int argc, char* argv[], Options& opts) { opts.set(options::replayStream, new Parser::ExprStream(replayParser)); } if( opts[options::replayLog] != NULL ) { - *opts[options::replayLog] << language::SetLanguage(opts[options::outputLanguage]) << Expr::setdepth(-1); + *opts[options::replayLog] << language::SetLanguage(opts[options::outputLanguage]) + << expr::ExprSetDepth(-1); } int returnValue = 0; diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index 7b146b3b0..6888d3af5 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -40,6 +40,7 @@ #include "base/output.h" #include "options/language.h" +#include "options/base_options.h" #include "options/main_options.h" #include "options/options.h" #include "options/smt_options.h" diff --git a/src/main/main.cpp b/src/main/main.cpp index 36a339d94..3f0842cc5 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -28,6 +28,7 @@ #include "expr/statistics.h" #include "main/command_executor.h" #include "main/interactive_shell.h" +#include "options/base_options.h" #include "options/language.h" #include "options/main_options.h" #include "parser/parser.h" diff --git a/src/main/portfolio_util.cpp b/src/main/portfolio_util.cpp index 6b5fe4723..1ec0b961c 100644 --- a/src/main/portfolio_util.cpp +++ b/src/main/portfolio_util.cpp @@ -12,11 +12,14 @@ ** \brief Code relevant only for portfolio builds **/ +#include "main/portfolio_util.h" + #include <unistd.h> #include <cassert> #include <vector> +#include "options/base_options.h" #include "options/main_options.h" #include "options/options.h" #include "options/prop_options.h" @@ -96,4 +99,48 @@ vector<Options> parseThreadSpecificOptions(Options opts) return threadOptions; } +void PortfolioLemmaOutputChannel::notifyNewLemma(Expr lemma) { + if(int(lemma.getNumChildren()) > options::sharingFilterByLength()) { + return; + } + ++cnt; + Trace("sharing") << d_tag << ": " << lemma << std::endl; + expr::pickle::Pickle pkl; + try { + d_pickler.toPickle(lemma, pkl); + d_sharedChannel->push(pkl); + if(Trace.isOn("showSharing") && options::thread_id() == 0) { + *options::out() << "thread #0: notifyNewLemma: " << lemma + << std::endl; + } + } catch(expr::pickle::PicklingException& p){ + Trace("sharing::blocked") << lemma << std::endl; + } +} + + +PortfolioLemmaInputChannel::PortfolioLemmaInputChannel(std::string tag, + SharedChannel<ChannelFormat>* c, + ExprManager* em, + VarMap& to, + VarMap& from) + : d_tag(tag), d_sharedChannel(c), d_pickler(em, to, from) +{} + +bool PortfolioLemmaInputChannel::hasNewLemma(){ + Debug("lemmaInputChannel") << d_tag << ": " << "hasNewLemma" << std::endl; + return !d_sharedChannel->empty(); +} + +Expr PortfolioLemmaInputChannel::getNewLemma() { + Debug("lemmaInputChannel") << d_tag << ": " << "getNewLemma" << std::endl; + expr::pickle::Pickle pkl = d_sharedChannel->pop(); + + Expr e = d_pickler.fromPickle(pkl); + if(Trace.isOn("showSharing") && options::thread_id() == 0) { + *options::out() << "thread #0: getNewLemma: " << e << std::endl; + } + return e; +} + }/*CVC4 namespace */ diff --git a/src/main/portfolio_util.h b/src/main/portfolio_util.h index d6d6a2d02..2b1e22754 100644 --- a/src/main/portfolio_util.h +++ b/src/main/portfolio_util.h @@ -20,6 +20,7 @@ #include "base/output.h" #include "expr/pickler.h" #include "options/main_options.h" +#include "smt/smt_engine.h" #include "smt_util/lemma_input_channel.h" #include "smt_util/lemma_output_channel.h" #include "util/channel.h" @@ -49,25 +50,7 @@ public: ~PortfolioLemmaOutputChannel() throw() { } - void notifyNewLemma(Expr lemma) { - if(int(lemma.getNumChildren()) > options::sharingFilterByLength()) { - return; - } - ++cnt; - Trace("sharing") << d_tag << ": " << lemma << std::endl; - expr::pickle::Pickle pkl; - try { - d_pickler.toPickle(lemma, pkl); - d_sharedChannel->push(pkl); - if(Trace.isOn("showSharing") && options::thread_id() == 0) { - *options::out() << "thread #0: notifyNewLemma: " << lemma - << std::endl; - } - } catch(expr::pickle::PicklingException& p){ - Trace("sharing::blocked") << lemma << std::endl; - } - } - + void notifyNewLemma(Expr lemma); };/* class PortfolioLemmaOutputChannel */ class PortfolioLemmaInputChannel : public LemmaInputChannel { @@ -81,29 +64,12 @@ public: SharedChannel<ChannelFormat>* c, ExprManager* em, VarMap& to, - VarMap& from) : - d_tag(tag), - d_sharedChannel(c), - d_pickler(em, to, from){ - } + VarMap& from); ~PortfolioLemmaInputChannel() throw() { } - bool hasNewLemma(){ - Debug("lemmaInputChannel") << d_tag << ": " << "hasNewLemma" << std::endl; - return !d_sharedChannel->empty(); - } - - Expr getNewLemma() { - Debug("lemmaInputChannel") << d_tag << ": " << "getNewLemma" << std::endl; - expr::pickle::Pickle pkl = d_sharedChannel->pop(); - - Expr e = d_pickler.fromPickle(pkl); - if(Trace.isOn("showSharing") && options::thread_id() == 0) { - *options::out() << "thread #0: getNewLemma: " << e << std::endl; - } - return e; - } + bool hasNewLemma(); + Expr getNewLemma(); };/* class PortfolioLemmaInputChannel */ diff --git a/src/main/util.cpp b/src/main/util.cpp index 86272ee53..ce4e4509d 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -34,6 +34,7 @@ #include "expr/statistics.h" #include "main/command_executor.h" #include "main/main.h" +#include "options/base_options.h" #include "options/options.h" #include "smt/smt_engine.h" diff --git a/src/options/base_options_template.h b/src/options/base_options_template.h index e43d2848e..c8c02ecaa 100644 --- a/src/options/base_options_template.h +++ b/src/options/base_options_template.h @@ -14,7 +14,7 @@ ** Contains code for handling command-line options **/ -#include "cvc4_public.h" +#include "cvc4_private.h" #ifndef __CVC4__OPTIONS__${module_id}_H #define __CVC4__OPTIONS__${module_id}_H diff --git a/src/options/boolean_term_conversion_mode.h b/src/options/boolean_term_conversion_mode.h index 65cc7a8a5..81a0c661a 100644 --- a/src/options/boolean_term_conversion_mode.h +++ b/src/options/boolean_term_conversion_mode.h @@ -26,7 +26,7 @@ namespace CVC4 { namespace theory { namespace booleans { -typedef enum { +enum BooleanTermConversionMode { /** * Convert Boolean terms to bitvectors of size 1. */ @@ -41,7 +41,7 @@ typedef enum { */ BOOLEAN_TERM_CONVERT_NATIVE -} BooleanTermConversionMode; +}; }/* CVC4::theory::booleans namespace */ }/* CVC4::theory namespace */ diff --git a/src/options/bv_bitblast_mode.h b/src/options/bv_bitblast_mode.h index 08a6e4077..f36021478 100644 --- a/src/options/bv_bitblast_mode.h +++ b/src/options/bv_bitblast_mode.h @@ -64,8 +64,8 @@ enum BvSlicerMode { }/* CVC4::theory::bv namespace */ }/* CVC4::theory namespace */ -std::ostream& operator<<(std::ostream& out, theory::bv::BitblastMode mode) CVC4_PUBLIC; -std::ostream& operator<<(std::ostream& out, theory::bv::BvSlicerMode mode) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, theory::bv::BitblastMode mode); +std::ostream& operator<<(std::ostream& out, theory::bv::BvSlicerMode mode); }/* CVC4 namespace */ diff --git a/src/options/decision_mode.cpp b/src/options/decision_mode.cpp index 168637e64..0aeae1baa 100644 --- a/src/options/decision_mode.cpp +++ b/src/options/decision_mode.cpp @@ -17,6 +17,8 @@ #include "options/decision_mode.h" +#include <iostream> + namespace CVC4 { std::ostream& operator<<(std::ostream& out, decision::DecisionMode mode) { diff --git a/src/options/decision_mode.h b/src/options/decision_mode.h index fb01c587b..420d00b4c 100644 --- a/src/options/decision_mode.h +++ b/src/options/decision_mode.h @@ -20,7 +20,7 @@ #ifndef __CVC4__SMT__DECISION_MODE_H #define __CVC4__SMT__DECISION_MODE_H -#include <iostream> +#include <iosfwd> namespace CVC4 { namespace decision { @@ -57,7 +57,7 @@ enum DecisionWeightInternal { }/* CVC4::decision namespace */ -std::ostream& operator<<(std::ostream& out, decision::DecisionMode mode) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, decision::DecisionMode mode); }/* CVC4 namespace */ diff --git a/src/options/decision_weight.h b/src/options/decision_weight.h index 42f1d5b6d..89ebe8a21 100644 --- a/src/options/decision_weight.h +++ b/src/options/decision_weight.h @@ -21,7 +21,9 @@ namespace CVC4 { namespace decision { + typedef uint64_t DecisionWeight; + }/* CVC4::decision namespace */ }/* CVC4 namespace */ diff --git a/src/options/options.h b/src/options/options.h index fc3bf40ac..a83de9acb 100644 --- a/src/options/options.h +++ b/src/options/options.h @@ -164,6 +164,4 @@ public: }/* CVC4 namespace */ -#include "options/base_options.h" - #endif /* __CVC4__OPTIONS__OPTIONS_H */ diff --git a/src/options/set_language.cpp b/src/options/set_language.cpp index db0275e04..f68adbb45 100644 --- a/src/options/set_language.cpp +++ b/src/options/set_language.cpp @@ -18,6 +18,7 @@ #include <iosfwd> #include <iomanip> +#include "options/base_options.h" #include "options/language.h" #include "options/options.h" diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 0e8a9e241..120f63987 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -26,6 +26,7 @@ #include "base/output.h" #include "expr/expr.h" +#include "expr/expr_iomanip.h" #include "expr/kind.h" #include "expr/resource_manager.h" #include "expr/type.h" @@ -331,7 +332,7 @@ Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) { j != j_end; ++j) { const DatatypeConstructor& ctor = *j; - Expr::printtypes::Scope pts(Debug("parser-idt"), true); + expr::ExprPrintTypes::Scope pts(Debug("parser-idt"), true); Expr constructor = ctor.getConstructor(); Debug("parser-idt") << "+ define " << constructor << std::endl; string constructorName = ctor.getName(); diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index 08e0232aa..f473ae178 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -18,6 +18,7 @@ #include <string> #include "expr/expr_manager.h" +#include "options/base_options.h" #include "options/parser_options.h" #include "options/smt_options.h" #include "parser/input.h" diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index 75d625edc..d4b99536e 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -17,6 +17,7 @@ #include <string> +#include "options/base_options.h" #include "options/language.h" #include "printer/ast/ast_printer.h" #include "printer/cvc/cvc_printer.h" @@ -87,4 +88,29 @@ void Printer::toStream(std::ostream& out, const UnsatCore& core, const std::map< } }/* Printer::toStream(UnsatCore, std::map<Expr, std::string>) */ +Printer* Printer::getPrinter(OutputLanguage lang) throw() { + if(lang == language::output::LANG_AUTO) { + // Infer the language to use for output. + // + // Options can be null in certain circumstances (e.g., when printing + // the singleton "null" expr. So we guard against segfault + if(not Options::isCurrentNull()) { + if(options::outputLanguage.wasSetByUser()) { + lang = options::outputLanguage(); + } + if(lang == language::output::LANG_AUTO && options::inputLanguage.wasSetByUser()) { + lang = language::toOutputLanguage(options::inputLanguage()); + } + } + if(lang == language::output::LANG_AUTO) { + lang = language::output::LANG_CVC4; // default + } + } + if(d_printers[lang] == NULL) { + d_printers[lang] = makePrinter(lang); + } + return d_printers[lang]; +} + + }/* CVC4 namespace */ diff --git a/src/printer/printer.h b/src/printer/printer.h index 30d33d46b..48787f70a 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -56,29 +56,7 @@ protected: public: /** Get the Printer for a given OutputLanguage */ - static Printer* getPrinter(OutputLanguage lang) throw() { - if(lang == language::output::LANG_AUTO) { - // Infer the language to use for output. - // - // Options can be null in certain circumstances (e.g., when printing - // the singleton "null" expr. So we guard against segfault - if(not Options::isCurrentNull()) { - if(options::outputLanguage.wasSetByUser()) { - lang = options::outputLanguage(); - } - if(lang == language::output::LANG_AUTO && options::inputLanguage.wasSetByUser()) { - lang = language::toOutputLanguage(options::inputLanguage()); - } - } - if(lang == language::output::LANG_AUTO) { - lang = language::output::LANG_CVC4; // default - } - } - if(d_printers[lang] == NULL) { - d_printers[lang] = makePrinter(lang); - } - return d_printers[lang]; - } + static Printer* getPrinter(OutputLanguage lang) throw(); /** Write a Node out to a stream with this Printer. */ virtual void toStream(std::ostream& out, TNode n, diff --git a/src/proof/unsat_core.cpp b/src/proof/unsat_core.cpp index 4a4d13977..37cc62aa0 100644 --- a/src/proof/unsat_core.cpp +++ b/src/proof/unsat_core.cpp @@ -16,6 +16,8 @@ #include "proof/unsat_core.h" +#include "expr/expr_iomanip.h" +#include "options/base_options.h" #include "printer/printer.h" #include "smt/smt_engine_scope.h" #include "smt_util/command.h" @@ -36,13 +38,13 @@ UnsatCore::const_iterator UnsatCore::end() const { void UnsatCore::toStream(std::ostream& out) const { smt::SmtScope smts(d_smt); - Expr::dag::Scope scope(out, false); + expr::ExprDag::Scope scope(out, false); Printer::getPrinter(options::outputLanguage())->toStream(out, *this); } void UnsatCore::toStream(std::ostream& out, const std::map<Expr, std::string>& names) const { smt::SmtScope smts(d_smt); - Expr::dag::Scope scope(out, false); + expr::ExprDag::Scope scope(out, false); Printer::getPrinter(options::outputLanguage())->toStream(out, *this, names); } diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index 23a740a26..d9b8bb4f8 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -18,6 +18,7 @@ #include "prop/minisat/minisat.h" +#include "options/base_options.h" #include "options/decision_options.h" #include "options/prop_options.h" #include "options/smt_options.h" diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 499cf1b56..2a1b05619 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -26,6 +26,7 @@ #include "expr/expr.h" #include "expr/resource_manager.h" #include "expr/result.h" +#include "options/base_options.h" #include "options/decision_options.h" #include "options/main_options.h" #include "options/options.h" diff --git a/src/prop/sat_solver_factory.h b/src/prop/sat_solver_factory.h index 34776c245..e0446eb4a 100644 --- a/src/prop/sat_solver_factory.h +++ b/src/prop/sat_solver_factory.h @@ -14,12 +14,13 @@ ** SAT Solver creation facility **/ -#pragma once +#include "cvc4_private.h" -#include "cvc4_public.h" +#pragma once #include <string> #include <vector> + #include "prop/sat_solver.h" namespace CVC4 { diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index f2c45eab9..c1d49d8c8 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -26,11 +26,8 @@ #include <utility> #include <vector> -#include "options/boolean_term_conversion_mode.h" -#include "options/decision_mode.h" #include "base/exception.h" #include "base/modal_exception.h" -#include "options/option_exception.h" #include "base/output.h" #include "context/cdhashset.h" #include "context/cdlist.h" @@ -46,12 +43,16 @@ #include "expr/resource_manager.h" #include "options/arith_options.h" #include "options/arrays_options.h" +#include "options/base_options.h" +#include "options/boolean_term_conversion_mode.h" #include "options/booleans_options.h" #include "options/booleans_options.h" #include "options/bv_options.h" #include "options/datatypes_options.h" +#include "options/decision_mode.h" #include "options/decision_options.h" #include "options/main_options.h" +#include "options/option_exception.h" #include "options/options_handler_interface.h" #include "options/printer_options.h" #include "options/prop_options.h" @@ -65,8 +66,8 @@ #include "proof/proof.h" #include "proof/proof_manager.h" #include "proof/proof_manager.h" -#include "proof/unsat_core.h" #include "proof/theory_proof.h" +#include "proof/unsat_core.h" #include "prop/prop_engine.h" #include "smt/boolean_terms.h" #include "smt/command_list.h" @@ -74,8 +75,8 @@ #include "smt/model_postprocessor.h" #include "smt/smt_engine_scope.h" #include "smt/smt_options_handler.h" -#include "smt_util/command.h" #include "smt_util/boolean_simplification.h" +#include "smt_util/command.h" #include "smt_util/ite_removal.h" #include "smt_util/nary_builder.h" #include "smt_util/node_visitor.h" diff --git a/src/smt/smt_options_handler.cpp b/src/smt/smt_options_handler.cpp index 371cdcddd..e1a19d48b 100644 --- a/src/smt/smt_options_handler.cpp +++ b/src/smt/smt_options_handler.cpp @@ -25,6 +25,7 @@ #include "base/modal_exception.h" #include "base/output.h" #include "cvc4autoconfig.h" +#include "expr/expr_iomanip.h" #include "expr/metakind.h" #include "expr/node_manager.h" #include "expr/resource_manager.h" @@ -32,6 +33,7 @@ #include "options/arith_heuristic_pivot_rule.h" #include "options/arith_propagation_mode.h" #include "options/arith_unate_lemma_mode.h" +#include "options/base_options.h" #include "options/boolean_term_conversion_mode.h" #include "options/bv_bitblast_mode.h" #include "options/bv_options.h" @@ -1219,9 +1221,9 @@ void SmtOptionsHandler::proofEnabledBuild(std::string option, bool value) throw( bool printtypesSetting = expr::ExprPrintTypes::getPrintTypes(__channel_get); \ OutputLanguage languageSetting = language::SetLanguage::getLanguage(__channel_get); \ __channel_set; \ - __channel_get << Expr::dag(dagSetting); \ - __channel_get << Expr::setdepth(exprDepthSetting); \ - __channel_get << Expr::printtypes(printtypesSetting); \ + __channel_get << expr::ExprDag(dagSetting); \ + __channel_get << expr::ExprSetDepth(exprDepthSetting); \ + __channel_get << expr::ExprPrintTypes(printtypesSetting); \ __channel_get << language::SetLanguage(languageSetting); \ } @@ -1418,12 +1420,12 @@ void SmtOptionsHandler::setDefaultExprDepth(std::string option, int depth) { throw OptionException("--default-expr-depth requires a positive argument, or -1."); } - Debug.getStream() << Expr::setdepth(depth); - Trace.getStream() << Expr::setdepth(depth); - Notice.getStream() << Expr::setdepth(depth); - Chat.getStream() << Expr::setdepth(depth); - Message.getStream() << Expr::setdepth(depth); - Warning.getStream() << Expr::setdepth(depth); + Debug.getStream() << expr::ExprSetDepth(depth); + Trace.getStream() << expr::ExprSetDepth(depth); + Notice.getStream() << expr::ExprSetDepth(depth); + Chat.getStream() << expr::ExprSetDepth(depth); + Message.getStream() << expr::ExprSetDepth(depth); + Warning.getStream() << expr::ExprSetDepth(depth); // intentionally exclude Dump stream from this list } @@ -1432,22 +1434,22 @@ void SmtOptionsHandler::setDefaultDagThresh(std::string option, int dag) { throw OptionException("--default-dag-thresh requires a nonnegative argument."); } - Debug.getStream() << Expr::dag(dag); - Trace.getStream() << Expr::dag(dag); - Notice.getStream() << Expr::dag(dag); - Chat.getStream() << Expr::dag(dag); - Message.getStream() << Expr::dag(dag); - Warning.getStream() << Expr::dag(dag); - Dump.getStream() << Expr::dag(dag); + Debug.getStream() << expr::ExprDag(dag); + Trace.getStream() << expr::ExprDag(dag); + Notice.getStream() << expr::ExprDag(dag); + Chat.getStream() << expr::ExprDag(dag); + Message.getStream() << expr::ExprDag(dag); + Warning.getStream() << expr::ExprDag(dag); + Dump.getStream() << expr::ExprDag(dag); } void SmtOptionsHandler::setPrintExprTypes(std::string option) { - Debug.getStream() << Expr::printtypes(true); - Trace.getStream() << Expr::printtypes(true); - Notice.getStream() << Expr::printtypes(true); - Chat.getStream() << Expr::printtypes(true); - Message.getStream() << Expr::printtypes(true); - Warning.getStream() << Expr::printtypes(true); + Debug.getStream() << expr::ExprPrintTypes(true); + Trace.getStream() << expr::ExprPrintTypes(true); + Notice.getStream() << expr::ExprPrintTypes(true); + Chat.getStream() << expr::ExprPrintTypes(true); + Message.getStream() << expr::ExprPrintTypes(true); + Warning.getStream() << expr::ExprPrintTypes(true); // intentionally exclude Dump stream from this list } diff --git a/src/smt_util/command.cpp b/src/smt_util/command.cpp index ae4e1f1f0..5917d71da 100644 --- a/src/smt_util/command.cpp +++ b/src/smt_util/command.cpp @@ -25,6 +25,7 @@ #include "base/cvc4_assert.h" #include "base/output.h" +#include "expr/expr_iomanip.h" #include "expr/node.h" #include "expr/sexpr.h" #include "options/options.h" @@ -984,7 +985,7 @@ void GetValueCommand::printResult(std::ostream& out, uint32_t verbosity) const t if(! ok()) { this->Command::printResult(out, verbosity); } else { - Expr::dag::Scope scope(out, false); + expr::ExprDag::Scope scope(out, false); out << d_result << endl; } } diff --git a/src/smt_util/model.cpp b/src/smt_util/model.cpp index 3f0423f49..ddac7e263 100644 --- a/src/smt_util/model.cpp +++ b/src/smt_util/model.cpp @@ -16,10 +16,12 @@ #include <vector> -#include "smt_util/command.h" -#include "smt/smt_engine_scope.h" -#include "smt/command_list.h" +#include "expr/expr_iomanip.h" +#include "options/base_options.h" #include "printer/printer.h" +#include "smt/command_list.h" +#include "smt/smt_engine_scope.h" +#include "smt_util/command.h" using namespace std; @@ -27,7 +29,7 @@ namespace CVC4 { std::ostream& operator<<(std::ostream& out, const Model& m) { smt::SmtScope smts(&m.d_smt); - Expr::dag::Scope scope(out, false); + expr::ExprDag::Scope scope(out, false); Printer::getPrinter(options::outputLanguage())->toStream(out, m); return out; } diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 36b24c51b..56f966426 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/term_database.h" #include "expr/datatype.h" +#include "options/base_options.h" #include "options/quantifiers_options.h" #include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/ce_guided_instantiation.h" diff --git a/src/util/floatingpoint.h b/src/util/floatingpoint.h index 132d67b1c..d8a3a65d9 100644 --- a/src/util/floatingpoint.h +++ b/src/util/floatingpoint.h @@ -62,11 +62,11 @@ namespace CVC4 { }; /* class FloatingPointSize */ - - -#define ROLL(X,N) (((X) << (N)) | ((X) >> (8*sizeof((X)) - (N)) )) - struct CVC4_PUBLIC FloatingPointSizeHashFunction { + static inline size_t ROLL(size_t X, size_t N) { + return (((X) << (N)) | ((X) >> (8*sizeof((X)) - (N)) )); + } + inline size_t operator() (const FloatingPointSize& fpt) const { return size_t(ROLL(fpt.exponent(), 4*sizeof(unsigned)) | fpt.significand()); diff --git a/test/system/ouroborous.cpp b/test/system/ouroborous.cpp index dd6cbccb8..d27ebd9b3 100644 --- a/test/system/ouroborous.cpp +++ b/test/system/ouroborous.cpp @@ -29,6 +29,7 @@ #include <string> #include "expr/expr.h" +#include "expr/expr_iomanip.h" #include "options/set_language.h" #include "parser/parser.h" #include "parser/parser_builder.h" @@ -70,7 +71,7 @@ string translate(string in, InputLanguage inlang, OutputLanguage outlang) { psr->setInput(Input::newStringInput(inlang, in, "internal-buffer")); Expr e = psr->nextExpression(); stringstream ss; - ss << language::SetLanguage(outlang) << Expr::setdepth(-1) << e; + ss << language::SetLanguage(outlang) << expr::ExprSetDepth(-1) << e; assert(psr->nextExpression().isNull());// next expr should be null assert(psr->done());// parser should be done string s = ss.str(); @@ -122,7 +123,7 @@ int runTest() { assert(psr->done());// parser should be done - cout << Expr::setdepth(-1); + cout << expr::ExprSetDepth(-1); runTestString("(= (f (f y)) x)"); runTestString("~BVPLUS(3, 0bin00, 0bin11)[2:1] = 0bin10", input::LANG_CVC4); diff --git a/test/system/smt2_compliance.cpp b/test/system/smt2_compliance.cpp index 99b4c625c..b202bcccc 100644 --- a/test/system/smt2_compliance.cpp +++ b/test/system/smt2_compliance.cpp @@ -19,6 +19,7 @@ #include <sstream> #include "expr/expr_manager.h" +#include "options/base_options.h" #include "options/set_language.h" #include "options/smt_options.h" #include "parser/parser.h" diff --git a/test/unit/main/interactive_shell_black.h b/test/unit/main/interactive_shell_black.h index 6c3e73d2c..b351f5c3e 100644 --- a/test/unit/main/interactive_shell_black.h +++ b/test/unit/main/interactive_shell_black.h @@ -22,6 +22,7 @@ #include "expr/expr_manager.h" #include "main/interactive_shell.h" +#include "options/base_options.h" #include "options/language.h" #include "options/options.h" #include "parser/parser_builder.h" diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index 9b700eda6..6ecc76c2b 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -22,6 +22,7 @@ #include "base/output.h" #include "expr/expr.h" #include "expr/expr_manager.h" +#include "options/base_options.h" #include "options/language.h" #include "options/options.h" #include "parser/parser.h" diff --git a/test/unit/util/boolean_simplification_black.h b/test/unit/util/boolean_simplification_black.h index 355d4ff37..4c0eb81cc 100644 --- a/test/unit/util/boolean_simplification_black.h +++ b/test/unit/util/boolean_simplification_black.h @@ -18,6 +18,7 @@ #include <set> #include <vector> +#include "expr/expr_iomanip.h" #include "expr/kind.h" #include "expr/node.h" #include "expr/node_manager.h" @@ -102,7 +103,7 @@ public: TS_ASSERT_LESS_THAN_EQUALS(10u, BooleanSimplification::DUPLICATE_REMOVAL_THRESHOLD); - cout << Expr::setdepth(-1) + cout << expr::ExprSetDepth(-1) << language::SetLanguage(language::output::LANG_CVC4); } |