diff options
author | Morgan Deters <mdeters@gmail.com> | 2009-11-24 21:03:35 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2009-11-24 21:03:35 +0000 |
commit | 811158832b74e3b101af2c7473f4e11a41377dd4 (patch) | |
tree | 07c55ab126dd7eb24239b615c987a490b182c8a6 /src | |
parent | f6968899de4d27c5bc986c3ac89972fbbe35c361 (diff) |
configure option adjustments as per 11/24 meeting; various fixes and improvements
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/expr.cpp | 2 | ||||
-rw-r--r-- | src/expr/expr.h | 103 | ||||
-rw-r--r-- | src/expr/expr_attribute.h | 2 | ||||
-rw-r--r-- | src/expr/expr_builder.cpp | 85 | ||||
-rw-r--r-- | src/expr/expr_builder.h | 8 | ||||
-rw-r--r-- | src/expr/expr_manager.h | 2 | ||||
-rw-r--r-- | src/expr/expr_value.h | 2 | ||||
-rw-r--r-- | src/expr/kind.h | 4 | ||||
-rw-r--r-- | src/include/cvc4_config.h | 3 | ||||
-rw-r--r-- | src/include/cvc4_expr.h | 4 | ||||
-rw-r--r-- | src/main/about.h | 1 | ||||
-rw-r--r-- | src/main/getopt.cpp | 5 | ||||
-rw-r--r-- | src/main/main.cpp | 5 | ||||
-rw-r--r-- | src/main/usage.h | 1 | ||||
-rw-r--r-- | src/main/util.cpp | 4 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 116 | ||||
-rw-r--r-- | src/theory/theory.h | 2 | ||||
-rw-r--r-- | src/util/assert.h | 76 | ||||
-rw-r--r-- | src/util/options.h | 8 | ||||
-rw-r--r-- | src/util/output.h | 135 |
20 files changed, 530 insertions, 38 deletions
diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp index f1b334ff8..e25cf8595 100644 --- a/src/expr/expr.cpp +++ b/src/expr/expr.cpp @@ -10,7 +10,7 @@ ** Reference-counted encapsulation of a pointer to an expression. **/ -#include "cvc4_expr.h" +#include "expr/expr.h" #include "expr_value.h" #include "expr_builder.h" diff --git a/src/expr/expr.h b/src/expr/expr.h new file mode 100644 index 000000000..d99708991 --- /dev/null +++ b/src/expr/expr.h @@ -0,0 +1,103 @@ +/********************* -*- C++ -*- */ +/** cvc4_expr.h + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** Reference-counted encapsulation of a pointer to an expression. + **/ + +#ifndef __CVC4_EXPR_H +#define __CVC4_EXPR_H + +#include <vector> +#include <stdint.h> + +#include "cvc4_config.h" +#include "expr/kind.h" + +namespace CVC4 { + +namespace expr { + class ExprValue; +}/* CVC4::expr namespace */ + +using CVC4::expr::ExprValue; + +/** + * Encapsulation of an ExprValue pointer. The reference count is + * maintained in the ExprValue. + */ +class CVC4_PUBLIC Expr { + /** A convenient null-valued encapsulated pointer */ + static Expr s_null; + + /** The referenced ExprValue */ + ExprValue* d_ev; + + /** This constructor is reserved for use by the Expr package; one + * must construct an Expr using one of the build mechanisms of the + * Expr package. + * + * Increments the reference count. */ + explicit Expr(ExprValue*); + + typedef Expr* iterator; + typedef Expr const* const_iterator; + + friend class ExprBuilder; + +public: + CVC4_PUBLIC Expr(const Expr&); + + /** Destructor. Decrements the reference count and, if zero, + * collects the ExprValue. */ + CVC4_PUBLIC ~Expr(); + + Expr& operator=(const Expr&) CVC4_PUBLIC; + + /** Access to the encapsulated expression. + * @return the encapsulated expression. */ + ExprValue* operator->() const CVC4_PUBLIC; + + uint64_t hash() const; + + Expr eqExpr(const Expr& right) const; + Expr notExpr() const; + Expr negate() const; // avoid double-negatives + Expr andExpr(const Expr& right) const; + Expr orExpr(const Expr& right) const; + Expr iteExpr(const Expr& thenpart, const Expr& elsepart) const; + Expr iffExpr(const Expr& right) const; + Expr impExpr(const Expr& right) const; + Expr xorExpr(const Expr& right) const; + Expr skolemExpr(int i) const; + Expr substExpr(const std::vector<Expr>& oldTerms, + const std::vector<Expr>& newTerms) const; + + Expr plusExpr(const Expr& right) const; + Expr uMinusExpr() const; + Expr multExpr(const Expr& right) const; + + inline Kind getKind() const; + + static Expr null() { return s_null; } + +};/* class Expr */ + +}/* CVC4 namespace */ + +#include "expr/expr_value.h" + +namespace CVC4 { + +inline Kind Expr::getKind() const { + return Kind(d_ev->d_kind); +} + +}/* CVC4 namespace */ + +#endif /* __CVC4_EXPR_H */ diff --git a/src/expr/expr_attribute.h b/src/expr/expr_attribute.h index b44c9af6f..03140c4eb 100644 --- a/src/expr/expr_attribute.h +++ b/src/expr/expr_attribute.h @@ -17,7 +17,7 @@ #include <stdint.h> #include "config.h" #include "context/context.h" -#include "cvc4_expr.h" +#include "expr/expr.h" namespace CVC4 { namespace expr { diff --git a/src/expr/expr_builder.cpp b/src/expr/expr_builder.cpp index c5f366654..bf572cfbc 100644 --- a/src/expr/expr_builder.cpp +++ b/src/expr/expr_builder.cpp @@ -38,7 +38,7 @@ ExprBuilder& ExprBuilder::reset(const ExprValue* ev) { } ExprBuilder::ExprBuilder(const ExprBuilder& eb) : d_em(eb.d_em), d_kind(eb.d_kind), d_used(eb.d_used), d_nchildren(eb.d_nchildren) { - cvc4assert(!d_used); + Assert( !d_used ); if(d_nchildren > nchild_thresh) { d_children.u_vec = new vector<Expr>(); @@ -74,59 +74,104 @@ ExprBuilder::~ExprBuilder() { // Compound expression constructors ExprBuilder& ExprBuilder::eqExpr(const Expr& right) { - if(d_kind != UNDEFINED_KIND && d_kind != EQUAL) + Assert( d_kind != UNDEFINED_KIND ); + if(EXPECT_TRUE( d_kind != EQUAL )) { collapse(); - d_kind = EQUAL; + d_kind = EQUAL; + } + addChild(right); return *this; } ExprBuilder& ExprBuilder::notExpr() { - if(d_kind != UNDEFINED_KIND) - collapse(); + Assert( d_kind != UNDEFINED_KIND ); + collapse(); d_kind = NOT; return *this; } // avoid double-negatives ExprBuilder& ExprBuilder::negate() { - if(d_kind == NOT) + if(EXPECT_FALSE( d_kind == NOT )) return reset(d_children.u_arr[0]); - if(d_kind != UNDEFINED_KIND) - collapse(); + Assert( d_kind != UNDEFINED_KIND ); + collapse(); d_kind = NOT; return *this; } ExprBuilder& ExprBuilder::andExpr(const Expr& right) { + Assert( d_kind != UNDEFINED_KIND ); + if(d_kind != AND) { + collapse(); + d_kind = AND; + } + addChild(right); + return *this; } ExprBuilder& ExprBuilder::orExpr(const Expr& right) { + Assert( d_kind != UNDEFINED_KIND ); + if(EXPECT_TRUE( d_kind != OR )) { + collapse(); + d_kind = OR; + } + addChild(right); + return *this; } ExprBuilder& ExprBuilder::iteExpr(const Expr& thenpart, const Expr& elsepart) { + Assert( d_kind != UNDEFINED_KIND ); + collapse(); + d_kind = ITE; + addChild(thenpart); + addChild(elsepart); + return *this; } ExprBuilder& ExprBuilder::iffExpr(const Expr& right) { + Assert( d_kind != UNDEFINED_KIND ); + if(EXPECT_TRUE( d_kind != IFF )) { + collapse(); + d_kind = IFF; + } + addChild(right); + return *this; } ExprBuilder& ExprBuilder::impExpr(const Expr& right) { + Assert( d_kind != UNDEFINED_KIND ); + collapse(); + d_kind = IMPLIES; + addChild(right); + return *this; } ExprBuilder& ExprBuilder::xorExpr(const Expr& right) { + Assert( d_kind != UNDEFINED_KIND ); + if(EXPECT_TRUE( d_kind != XOR )) { + collapse(); + d_kind = XOR; + } + addChild(right); + return *this; } ExprBuilder& ExprBuilder::skolemExpr(int i) { -} - -ExprBuilder& ExprBuilder::substExpr(const std::vector<Expr>& oldTerms, - const std::vector<Expr>& newTerms) { + Assert( d_kind != UNDEFINED_KIND ); + collapse(); + d_kind = SKOLEM; + //addChild(i);//FIXME: int constant + return *this; } // "Stream" expression constructor syntax ExprBuilder& ExprBuilder::operator<<(const Kind& op) { + return *this; } ExprBuilder& ExprBuilder::operator<<(const Expr& child) { + return *this; } void ExprBuilder::addChild(const Expr& e) { @@ -182,21 +227,27 @@ void ExprBuilder::collapse() { // not const ExprBuilder::operator Expr() { + // FIXME } -AndExprBuilder ExprBuilder::operator&&(Expr) { +AndExprBuilder ExprBuilder::operator&&(Expr e) { + return AndExprBuilder(*this) && e; } -OrExprBuilder ExprBuilder::operator||(Expr) { +OrExprBuilder ExprBuilder::operator||(Expr e) { + return OrExprBuilder(*this) || e; } -PlusExprBuilder ExprBuilder::operator+ (Expr) { +PlusExprBuilder ExprBuilder::operator+ (Expr e) { + return PlusExprBuilder(*this) + e; } -PlusExprBuilder ExprBuilder::operator- (Expr) { +PlusExprBuilder ExprBuilder::operator- (Expr e) { + return PlusExprBuilder(*this) - e; } -MultExprBuilder ExprBuilder::operator* (Expr) { +MultExprBuilder ExprBuilder::operator* (Expr e) { + return MultExprBuilder(*this) * e; } }/* CVC4 namespace */ diff --git a/src/expr/expr_builder.h b/src/expr/expr_builder.h index 07d069a9e..97f18ca6d 100644 --- a/src/expr/expr_builder.h +++ b/src/expr/expr_builder.h @@ -109,6 +109,8 @@ class AndExprBuilder { public: + AndExprBuilder(const ExprBuilder&); + AndExprBuilder& operator&&(Expr); OrExprBuilder operator||(Expr); @@ -121,6 +123,8 @@ class OrExprBuilder { public: + OrExprBuilder(const ExprBuilder&); + AndExprBuilder operator&&(Expr); OrExprBuilder& operator||(Expr); @@ -133,6 +137,8 @@ class PlusExprBuilder { public: + PlusExprBuilder(const ExprBuilder&); + PlusExprBuilder& operator+(Expr); PlusExprBuilder& operator-(Expr); MultExprBuilder operator*(Expr); @@ -146,6 +152,8 @@ class MultExprBuilder { public: + MultExprBuilder(const ExprBuilder&); + PlusExprBuilder operator+(Expr); PlusExprBuilder operator-(Expr); MultExprBuilder& operator*(Expr); diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h index 802cfe9c0..e3fbd91bf 100644 --- a/src/expr/expr_manager.h +++ b/src/expr/expr_manager.h @@ -13,7 +13,7 @@ #define __CVC4__EXPR_MANAGER_H #include <vector> -#include "cvc4_expr.h" +#include "expr/expr.h" #include "kind.h" namespace CVC4 { diff --git a/src/expr/expr_value.h b/src/expr/expr_value.h index e0451f7a6..0b97dfdae 100644 --- a/src/expr/expr_value.h +++ b/src/expr/expr_value.h @@ -16,7 +16,7 @@ /* this must be above the check for __CVC4__EXPR__EXPR_VALUE_H */ /* to resolve a circular dependency */ -#include "cvc4_expr.h" +#include "expr/expr.h" #ifndef __CVC4__EXPR__EXPR_VALUE_H #define __CVC4__EXPR__EXPR_VALUE_H diff --git a/src/expr/kind.h b/src/expr/kind.h index 98cc7e2e3..db25d914e 100644 --- a/src/expr/kind.h +++ b/src/expr/kind.h @@ -36,12 +36,14 @@ enum Kind { AND, IFF, + IMPLIES, OR, XOR, /* from arith */ PLUS, - MINUS + MINUS, + MULT };/* enum Kind */ diff --git a/src/include/cvc4_config.h b/src/include/cvc4_config.h index e571f5969..ccc07b40a 100644 --- a/src/include/cvc4_config.h +++ b/src/include/cvc4_config.h @@ -39,3 +39,6 @@ # define CVC4_PUBLIC #endif /* __BUILDING_CVC4LIB */ + +#define EXPECT_TRUE(x) __builtin_expect( (x), true) +#define EXPECT_FALSE(x) __builtin_expect( (x), false) diff --git a/src/include/cvc4_expr.h b/src/include/cvc4_expr.h index 36d771647..d99708991 100644 --- a/src/include/cvc4_expr.h +++ b/src/include/cvc4_expr.h @@ -78,6 +78,10 @@ public: Expr substExpr(const std::vector<Expr>& oldTerms, const std::vector<Expr>& newTerms) const; + Expr plusExpr(const Expr& right) const; + Expr uMinusExpr() const; + Expr multExpr(const Expr& right) const; + inline Kind getKind() const; static Expr null() { return s_null; } diff --git a/src/main/about.h b/src/main/about.h index 458716842..e81e04288 100644 --- a/src/main/about.h +++ b/src/main/about.h @@ -10,6 +10,7 @@ ** [[ Add file-specific comments here ]] **/ +#ifndef __CVC4__MAIN__ABOUT_H #define __CVC4__MAIN__ABOUT_H namespace CVC4 { diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp index f1fe375b6..dcb23c303 100644 --- a/src/main/getopt.cpp +++ b/src/main/getopt.cpp @@ -10,6 +10,7 @@ ** [[ Add file-specific comments here ]] **/ +#include <cstdio> #include <cstdlib> #include <new> #include <unistd.h> @@ -29,7 +30,7 @@ using namespace std; using namespace CVC4; namespace CVC4 { -namespace Main { +namespace main { static const char lang_help[] = "\ Languages currently supported to the -L / --lang option:\n\ @@ -135,5 +136,5 @@ int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(Exception*) { return optind; } -}/* CVC4::Main namespace */ +}/* CVC4::main namespace */ }/* CVC4 namespace */ diff --git a/src/main/main.cpp b/src/main/main.cpp index 44543a75f..8529f2ca2 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -10,6 +10,7 @@ ** [[ Add file-specific comments here ]] **/ +#include <cstdio> #include <cstdlib> #include <cerrno> #include <new> @@ -25,7 +26,7 @@ using namespace std; using namespace CVC4; -using namespace CVC4::Main; +using namespace CVC4::main; int main(int argc, char *argv[]) { struct Options opts; @@ -57,7 +58,7 @@ int main(int argc, char *argv[]) { // delete cmd; // } } - } catch(CVC4::Main::OptionException* e) { + } catch(CVC4::main::OptionException* e) { if(opts.smtcomp_mode) { printf("unknown"); fflush(stdout); diff --git a/src/main/usage.h b/src/main/usage.h index 3326108ac..0b503cdb2 100644 --- a/src/main/usage.h +++ b/src/main/usage.h @@ -10,6 +10,7 @@ ** [[ Add file-specific comments here ]] **/ +#ifndef __CVC4__MAIN__USAGE_H #define __CVC4__MAIN__USAGE_H namespace CVC4 { diff --git a/src/main/util.cpp b/src/main/util.cpp index 572aea00f..e2333b417 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -23,7 +23,7 @@ using CVC4::Exception; using namespace std; namespace CVC4 { -namespace Main { +namespace main { void sigint_handler(int sig, siginfo_t* info, void*) { fprintf(stderr, "CVC4 interrupted by user.\n"); @@ -51,5 +51,5 @@ void cvc4_init() throw() { throw new Exception(string("sigaction(SIGSEGV) failure: ") + strerror(errno)); } -}/* CVC4::Main namespace */ +}/* CVC4::main namespace */ }/* CVC4 namespace */ diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h new file mode 100644 index 000000000..078bf9cde --- /dev/null +++ b/src/smt/smt_engine.h @@ -0,0 +1,116 @@ +/********************* -*- C++ -*- */ +/** prover.h + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + **/ + +#ifndef __CVC4__SMT__SMT_ENGINE_H +#define __CVC4__SMT__SMT_ENGINE_H + +#include <vector> +#include "core/cvc4_expr.h" +#include "core/result.h" +#include "core/model.h" + +// In terms of abstraction, this is below (and provides services to) +// ValidityChecker and above (and requires the services of) +// PropEngine. + +namespace CVC4 { +namespace smt { + +// TODO: SAT layer (esp. CNF- versus non-clausal solvers under the +// hood): use a type parameter and have check() delegate, or subclass +// SmtEngine and override check()? +// +// Probably better than that is to have a configuration object that +// indicates which passes are desired. The configuration occurs +// elsewhere (and can even occur at runtime). A simple "pass manager" +// of sorts determines check()'s behavior. +// +// The CNF conversion can go on in PropEngine. + +class SmtEngine { + /** Current set of assertions. */ + // TODO: make context-aware to handle user-level push/pop. + std::vector<Expr> d_assertList; + +private: + /** + * Pre-process an Expr. This is expected to be highly-variable, + * with a lot of "source-level configurability" to add multiple + * passes over the Expr. TODO: may need to specify a LEVEL of + * preprocessing (certain contexts need more/less ?). + */ + void preprocess(Expr); + + /** + * Adds a formula to the current context. + */ + void addFormula(Expr); + + /** + * Full check of consistency in current context. Returns true iff + * consistent. + */ + Result check(); + + /** + * Quick check of consistency in current context: calls + * processAssertionList() then look for inconsistency (based only on + * that). + */ + Result quickCheck(); + + /** + * Process the assertion list: for literals and conjunctions of + * literals, assert to T-solver. + */ + void processAssertionList(); + +public: + /** + * Add a formula to the current context: preprocess, do per-theory + * setup, use processAssertionList(), asserting to T-solver for + * literals and conjunction of literals. Returns false iff + * inconsistent. + */ + Result assert(Expr); + + /** + * Add a formula to the current context and call check(). Returns + * true iff consistent. + */ + Result query(Expr); + + /** + * Simplify a formula without doing "much" work. Requires assist + * from the SAT Engine. + */ + Expr simplify(Expr); + + /** + * Get a (counter)model (only if preceded by a SAT or INVALID query. + */ + Model getModel(); + + /** + * Push a user-level context. + */ + void push(); + + /** + * Pop a user-level context. Throws an exception if nothing to pop. + */ + void pop(); +};/* class SmtEngine */ + +}/* CVC4::smt namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__SMT__SMT_ENGINE_H */ diff --git a/src/theory/theory.h b/src/theory/theory.h index 1369d5f0b..5e5f053a6 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -12,7 +12,7 @@ #ifndef __CVC4__THEORY__THEORY_H #define __CVC4__THEORY__THEORY_H -#include "cvc4_expr.h" +#include "expr/expr.h" #include "util/literal.h" namespace CVC4 { diff --git a/src/util/assert.h b/src/util/assert.h index 24e3a4cdf..6691c1b04 100644 --- a/src/util/assert.h +++ b/src/util/assert.h @@ -7,20 +7,78 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** Assertion utility classes, functions, and exceptions. **/ #ifndef __CVC4__ASSERT_H #define __CVC4__ASSERT_H -#include <cassert> +#include <string> +#include "util/exception.h" +#include "cvc4_config.h" +#include "config.h" -#ifdef DEBUG -// the __builtin_expect() helps us if assert is built-in or a macro -# define cvc4assert(x) assert(__builtin_expect((x), 1)) -#else -// TODO: use a compiler annotation when assertions are off ? -// (to improve optimization) -# define cvc4assert(x) -#endif /* DEBUG */ +namespace CVC4 { + +class AssertionException : public Exception { +public: + AssertionException() : Exception() {} + AssertionException(std::string msg) : Exception(msg) {} + AssertionException(const char* msg) : Exception(msg) {} +};/* class AssertionException */ + +class UnreachableCodeException : public AssertionException { +public: + UnreachableCodeException() : AssertionException() {} + UnreachableCodeException(std::string msg) : AssertionException(msg) {} + UnreachableCodeException(const char* msg) : AssertionException(msg) {} +};/* class UnreachableCodeException */ + +#ifdef CVC4_ASSERTIONS +# define Assert(cond, msg...) __CVC4_ASSERTGLUE("Assertion failure at " __FILE__ ":", __LINE__, ": " #cond, __builtin_expect((cond), 1), ## msg) +#else /* ! CVC4_ASSERTIONS */ +# define Assert(cond, msg...) /*EXPECT_TRUE( cond )*/ +#endif /* CVC4_ASSERTIONS */ + +#define AlwaysAssert(cond, msg...) __CVC4_ASSERTGLUE("Assertion failure at " __FILE__ ":", __LINE__, ": " #cond, __builtin_expect((cond), 1), ## msg) +#define Unreachable(cond, msg...) __CVC4_UNREACHABLEGLUE("Hit a section of unreachable code at " __FILE__ ":", __LINE__, __builtin_expect((cond), 1), ## msg) + +#define __CVC4_ASSERTGLUE(str1, line, str2, cond, msg...) AssertImpl(str1 #line str2, cond, ## msg) +#define __CVC4_UNREACHABLEGLUE(str, line, cond, msg...) AssertImpl(str #line, cond, ## msg) + +inline void AssertImpl(const char* info, bool cond, std::string msg) { + if(EXPECT_FALSE( ! cond )) + throw new AssertionException(std::string(info) + "\n" + msg); +} + +inline void AssertImpl(const char* info, bool cond, const char* msg) { + if(EXPECT_FALSE( ! cond )) + throw new AssertionException(std::string(info) + "\n" + msg); +} + +inline void AssertImpl(const char* info, bool cond) { + if(EXPECT_FALSE( ! cond )) + throw new AssertionException(info); +} + +#ifdef __GNUC__ +inline void UnreachableImpl(const char* info, std::string msg) __attribute__ ((noreturn)); +inline void UnreachableImpl(const char* info, const char* msg) __attribute__ ((noreturn)); +inline void UnreachableImpl(const char* info) __attribute__ ((noreturn)); +#endif /* __GNUC__ */ + +inline void UnreachableImpl(const char* info, std::string msg) { + throw new UnreachableCodeException(std::string(info) + "\n" + msg); +} + +inline void UnreachableImpl(const char* info, const char* msg) { + throw new UnreachableCodeException(std::string(info) + "\n" + msg); +} + +inline void UnreachableImpl(const char* info) { + throw new UnreachableCodeException(info); +} + +}/* CVC4 namespace */ #endif /* __CVC4__ASSERT_H */ diff --git a/src/util/options.h b/src/util/options.h index 490cd607b..54b4e2f9b 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -10,6 +10,9 @@ ** [[ Add file-specific comments here ]] **/ +#include <iostream> + +#ifndef __CVC4__OPTIONS_H #define __CVC4__OPTIONS_H namespace CVC4 { @@ -20,6 +23,9 @@ struct Options { bool smtcomp_mode; bool statistics; + std::ostream *out; + std::ostream *err; + /* -1 means no output */ /* 0 is normal (and default) -- warnings only */ /* 1 is warnings + notices so the user doesn't get too bored */ @@ -32,6 +38,8 @@ struct Options { Options() : binary_name(), smtcomp_mode(false), statistics(false), + out(0), + err(0), verbosity(0), lang() {} diff --git a/src/util/output.h b/src/util/output.h new file mode 100644 index 000000000..4d3752849 --- /dev/null +++ b/src/util/output.h @@ -0,0 +1,135 @@ +/********************* -*- C++ -*- */ +/** output.h + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** Output utility classes and functions. + **/ + +#ifndef __CVC4__OUTPUT_H +#define __CVC4__OUTPUT_H + +#include <iostream> +#include <string> +#include <set> +#include "util/exception.h" + +namespace CVC4 { + + +class Debug { + std::set<std::string> d_tags; + std::ostream &d_out; + +public: + static void operator()(const char* tag, const char*); + static void operator()(const char* tag, std::string); + static void operator()(string tag, const char*); + static void operator()(string tag, std::string); + + static void printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 2, 3))); + static void printf(const char* tag, std::string fmt, ...) __attribute__ ((format(printf, 2, 3))); + static void printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 2, 3))); + static void printf(std::string tag, std::string fmt, ...) __attribute__ ((format(printf, 2, 3))); + + static std::ostream& operator()(const char* tag); + static std::ostream& operator()(std::string tag); + + static void on (const char* tag) { d_tags.insert(std::string(tag)); }; + static void on (std::string tag) { d_tags.insert(tag); }; + static void off(const char* tag) { d_tags.erase (std::string(tag)); }; + static void off(std::string tag) { d_tags.erase (tag); }; + + static void setStream(std::ostream& os) { d_out = os; } +};/* class Debug */ + + +class Warning { + std::ostream &d_out; + +public: + static void operator()(const char*); + static void operator()(std::string); + + static void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3))); + static void printf(std::string fmt, ...) __attribute__ ((format(printf, 2, 3))); + + static std::ostream& operator()(); + + static void setStream(std::ostream& os) { d_out = os; } +};/* class Warning */ + + +class Notice { + std::ostream &d_os; + +public: + static void operator()(const char*); + static void operator()(std::string); + + static void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3))); + static void printf(std::string fmt, ...) __attribute__ ((format(printf, 2, 3))); + + static std::ostream& operator()(); + + static void setStream(std::ostream& os) { d_out = os; } +};/* class Notice */ + + +class Chat { + std::ostream &d_os; + +public: + static void operator()(const char*); + static void operator()(std::string); + + static void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3))); + static void printf(std::string fmt, ...) __attribute__ ((format(printf, 2, 3))); + + static std::ostream& operator()(); + + static void setStream(std::ostream& os) { d_out = os; } +};/* class Chat */ + + +class Trace { + std::ostream &d_os; + +public: + static void operator()(const char* tag, const char*); + static void operator()(const char* tag, std::string); + static void operator()(string tag, const char*); + static void operator()(string tag, std::string); + + static void printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 2, 3))) { + va_list vl; + va_start(vl, fmt); + vfprintf(buf, 1024, fmt, vl); + va_end(vl); + } + static void printf(const char* tag, std::string fmt, ...) __attribute__ ((format(printf, 2, 3))) { + } + static void printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 2, 3))) { + } + static void printf(std::string tag, std::string fmt, ...) __attribute__ ((format(printf, 2, 3))) { + } + + static std::ostream& operator()(const char* tag); + static std::ostream& operator()(std::string tag); + + static void on (const char* tag) { d_tags.insert(std::string(tag)); }; + static void on (std::string tag) { d_tags.insert(tag); }; + static void off(const char* tag) { d_tags.erase (std::string(tag)); }; + static void off(std::string tag) { d_tags.erase (tag); }; + + static void setStream(std::ostream& os) { d_out = os; } +};/* class Trace */ + + +}/* CVC4 namespace */ + +#endif /* __CVC4__OUTPUT_H */ |