- Adding a script contrib/test_install_headers.h that tests whether one can include all cvc4_public headers. CVC4 can pass this test after this commit.
- Making lib/{clock_gettime.h,ffs.h,strtok_r.h} cvc4_private.
- Making prop/sat_solver_factory.h cvc4_private.
- Moving the expr iostream manipulators into their own files: expr_iomanip.{h,cpp}.
- Setting the generated *_options.h files back to being cvc4_private.
-- Removing the usage of options/expr_options.h from expr.h.
-- Removing the include of base_options.h from options.h.
- Cleaning up CPP macros in cvc4_public headers.
-- Changing the ROLL macro in floatingpoint.h into an inline function.
-- Removing the now unused flag -D__BUILDING_STATISTICS_FOR_EXPORT.
--- /dev/null
+#!/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
#include <sstream>
#include <string>
+#include "expr/expr_iomanip.h"
#include "options/language.h"
#include "options/set_language.h"
#include "sha1.hpp"
#include <sstream>
#include <string>
+#include "expr/expr_iomanip.h"
#include "options/language.h"
#include "options/set_language.h"
#include "sha1.hpp"
#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;
}
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) {
#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"
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);
#include <vector>
#include "expr/expr.h"
+#include "options/base_options.h"
#include "options/options.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
#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"
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);
#include <vector>
#include "expr/expr.h"
+#include "options/base_options.h"
#include "options/options.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
#include <vector>
#include "expr/expr.h"
+#include "options/base_options.h"
#include "options/options.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
#include <vector>
#include "expr/expr.h"
+#include "options/base_options.h"
#include "options/options.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
#include <vector>
#include "expr/expr.h"
+#include "options/base_options.h"
#include "options/options.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
#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"
#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"
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:
}
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);
}
#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"
}
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;
}
chain.h \
emptyset.cpp \
emptyset.h \
+ expr_iomanip.cpp \
+ expr_iomanip.h \
expr_manager_scope.h \
expr_stream.h \
kind_map.h \
--- /dev/null
+/********************* */
+/*! \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 */
--- /dev/null
+/********************* */
+/*! \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 */
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();
}
#include <string>
#include "base/exception.h"
-#include "options/expr_options.h"
#include "options/language.h"
#include "util/hash.h"
}/* CVC4::smt namespace */
namespace expr {
- class CVC4_PUBLIC ExprSetDepth;
- class CVC4_PUBLIC ExprPrintTypes;
- class CVC4_PUBLIC ExprDag;
-
class ExportPrivate;
}/* CVC4::expr namespace */
*/
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(...)
};/* 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();
}
#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"
#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"
#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
}/* CVC4::stats namespace */
-#ifndef __BUILDING_STATISTICS_FOR_EXPORT
-
StatisticsRegistry* StatisticsRegistry::current() {
return stats::getStatisticsRegistry(smt::currentSmtEngine());
}
#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);
#include "base/exception.h"
#include "expr/statistics.h"
-#include "lib/clock_gettime.h"
namespace CVC4 {
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;
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);
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) {
}
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),
**
** 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;
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 */
*
* @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
** 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
** 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
** 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
#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"
#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"
#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"
#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"
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;
#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"
#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"
** \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"
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 */
#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"
~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 {
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 */
#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"
** 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
namespace theory {
namespace booleans {
-typedef enum {
+enum BooleanTermConversionMode {
/**
* Convert Boolean terms to bitvectors of size 1.
*/
*/
BOOLEAN_TERM_CONVERT_NATIVE
-} BooleanTermConversionMode;
+};
}/* CVC4::theory::booleans namespace */
}/* CVC4::theory namespace */
}/* 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 */
#include "options/decision_mode.h"
+#include <iostream>
+
namespace CVC4 {
std::ostream& operator<<(std::ostream& out, decision::DecisionMode mode) {
#ifndef __CVC4__SMT__DECISION_MODE_H
#define __CVC4__SMT__DECISION_MODE_H
-#include <iostream>
+#include <iosfwd>
namespace CVC4 {
namespace decision {
}/* 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 */
namespace CVC4 {
namespace decision {
+
typedef uint64_t DecisionWeight;
+
}/* CVC4::decision namespace */
}/* CVC4 namespace */
}/* CVC4 namespace */
-#include "options/base_options.h"
-
#endif /* __CVC4__OPTIONS__OPTIONS_H */
#include <iosfwd>
#include <iomanip>
+#include "options/base_options.h"
#include "options/language.h"
#include "options/options.h"
#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"
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();
#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"
#include <string>
+#include "options/base_options.h"
#include "options/language.h"
#include "printer/ast/ast_printer.h"
#include "printer/cvc/cvc_printer.h"
}
}/* 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 */
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,
#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"
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);
}
#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"
#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"
** 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 {
#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"
#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"
#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"
#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"
#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"
#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"
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); \
}
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
}
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
}
#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"
if(! ok()) {
this->Command::printResult(out, verbosity);
} else {
- Expr::dag::Scope scope(out, false);
+ expr::ExprDag::Scope scope(out, false);
out << d_result << endl;
}
}
#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;
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;
}
#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"
}; /* 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());
#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"
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();
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);
#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"
#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"
#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"
#include <set>
#include <vector>
+#include "expr/expr_iomanip.h"
#include "expr/kind.h"
#include "expr/node.h"
#include "expr/node_manager.h"
TS_ASSERT_LESS_THAN_EQUALS(10u,
BooleanSimplification::DUPLICATE_REMOVAL_THRESHOLD);
- cout << Expr::setdepth(-1)
+ cout << expr::ExprSetDepth(-1)
<< language::SetLanguage(language::output::LANG_CVC4);
}
projects / cvc5.git / commitdiff