diff options
author | Morgan Deters <mdeters@gmail.com> | 2009-12-08 10:10:20 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2009-12-08 10:10:20 +0000 |
commit | 2163539a8b839acf98bda0e1a65f1fcca5232fb2 (patch) | |
tree | 207a09896626f678172ec774459defa6690b0200 /src/util | |
parent | abe5fb451ae66a4bedc88d870e99f76de4eb323c (diff) |
work on propositional layer, expression builder support for large expressions, output classes, and minisat
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/Assert.h (renamed from src/util/assert.h) | 0 | ||||
-rw-r--r-- | src/util/Makefile.am | 4 | ||||
-rw-r--r-- | src/util/command.cpp | 2 | ||||
-rw-r--r-- | src/util/decision_engine.cpp | 29 | ||||
-rw-r--r-- | src/util/decision_engine.h | 10 | ||||
-rw-r--r-- | src/util/literal.h | 3 | ||||
-rw-r--r-- | src/util/output.cpp | 29 | ||||
-rw-r--r-- | src/util/output.h | 161 |
8 files changed, 172 insertions, 66 deletions
diff --git a/src/util/assert.h b/src/util/Assert.h index 8fd970c6c..8fd970c6c 100644 --- a/src/util/assert.h +++ b/src/util/Assert.h diff --git a/src/util/Makefile.am b/src/util/Makefile.am index c70553c3e..8baf872d2 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -5,4 +5,6 @@ AM_CPPFLAGS = -D__BUILDING_CVC4LIB noinst_LTLIBRARIES = libutil.la libutil_la_SOURCES = \ - command.cpp + command.cpp \ + decision_engine.cpp \ + output.cpp diff --git a/src/util/command.cpp b/src/util/command.cpp index 190f794da..c78fbc089 100644 --- a/src/util/command.cpp +++ b/src/util/command.cpp @@ -31,7 +31,7 @@ AssertCommand::AssertCommand(const Expr& e) : } void AssertCommand::invoke(SmtEngine* smt_engine) { - smt_engine->assert(d_expr); + smt_engine->assertFormula(d_expr); } CheckSatCommand::CheckSatCommand() { diff --git a/src/util/decision_engine.cpp b/src/util/decision_engine.cpp new file mode 100644 index 000000000..ae79f920d --- /dev/null +++ b/src/util/decision_engine.cpp @@ -0,0 +1,29 @@ +/********************* -*- C++ -*- */ +/** decision_engine.cpp + ** 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. + ** + **/ + +#include "util/decision_engine.h" +#include "util/Assert.h" +#include "util/literal.h" + +namespace CVC4 { + +DecisionEngine::~DecisionEngine() { +} + +/** + * Only here to permit compilation and linkage. This may be pure + * virtual in the final design (?) + */ +Literal DecisionEngine::nextDecision() { + Unreachable(); +} + +}/* CVC4 namespace */ diff --git a/src/util/decision_engine.h b/src/util/decision_engine.h index a6f8596dd..3a093211c 100644 --- a/src/util/decision_engine.h +++ b/src/util/decision_engine.h @@ -12,6 +12,7 @@ #ifndef __CVC4__DECISION_ENGINE_H #define __CVC4__DECISION_ENGINE_H +#include "cvc4_config.h" #include "util/literal.h" namespace CVC4 { @@ -22,12 +23,17 @@ namespace CVC4 { /** * A decision mechanism for the next decision. */ -class DecisionEngine { +class CVC4_PUBLIC DecisionEngine { public: /** + * Destructor. + */ + virtual ~DecisionEngine(); + + /** * Get the next decision. */ - virtual Literal nextDecision() = 0; + virtual Literal nextDecision();// = 0 // TODO: design decision: decision engine should be notified of // propagated lits, and also why(?) (so that it can make decisions diff --git a/src/util/literal.h b/src/util/literal.h index 7af9826bb..3ec216a6a 100644 --- a/src/util/literal.h +++ b/src/util/literal.h @@ -14,7 +14,8 @@ namespace CVC4 { -class Literal; +class Literal { +}; }/* CVC4 namespace */ diff --git a/src/util/output.cpp b/src/util/output.cpp new file mode 100644 index 000000000..e07f32a66 --- /dev/null +++ b/src/util/output.cpp @@ -0,0 +1,29 @@ +/********************* -*- C++ -*- */ +/** output.cpp + ** 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. + **/ + +#include "cvc4_config.h" + +#include <iostream> +#include "util/output.h" + +namespace CVC4 { + +null_streambuf null_sb; +std::ostream null_os(&null_sb); + +DebugC Debug (&std::cout); +WarningC Warning(&std::cerr); +NoticeC Notice (&std::cout); +ChatC Chat (&std::cout); +TraceC Trace (&std::cout); + +}/* CVC4 namespace */ diff --git a/src/util/output.h b/src/util/output.h index 21b7b6e4c..b6532b93a 100644 --- a/src/util/output.h +++ b/src/util/output.h @@ -13,125 +13,164 @@ #ifndef __CVC4__OUTPUT_H #define __CVC4__OUTPUT_H +#include "cvc4_config.h" + #include <iostream> #include <string> +#include <cstdio> +#include <cstdarg> #include <set> + #include "util/exception.h" namespace CVC4 { -class Debug { +class null_streambuf : public std::streambuf { +public: + int overflow(int c) { return c; } +};/* class null_streambuf */ + +extern null_streambuf null_sb; +extern std::ostream null_os CVC4_PUBLIC; + +class CVC4_PUBLIC DebugC { std::set<std::string> d_tags; - std::ostream &d_out; + 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 operator()(const char*);// Yeting option - static void operator()(std::string);// Yeting option + DebugC(std::ostream* os) : d_os(os) {} + + void operator()(const char* tag, const char*); + void operator()(const char* tag, std::string); + void operator()(std::string tag, const char*); + void operator()(std::string tag, std::string); + //void operator()(const char*);// Yeting option + //void operator()(std::string);// Yeting option 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))); // Yeting option not possible here - static std::ostream& operator()(const char* tag); - static std::ostream& operator()(std::string tag); - static std::ostream& operator()();// Yeting option + std::ostream& operator()(const char* tag) { + if(d_tags.find(tag) != d_tags.end()) + return *d_os; + else return null_os; + } + std::ostream& operator()(std::string tag) { + if(d_tags.find(tag) != d_tags.end()) + return *d_os; + else return null_os; + } + std::ostream& operator()();// Yeting option - 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); } + void on (const char* tag) { d_tags.insert(std::string(tag)); } + void on (std::string tag) { d_tags.insert(tag); } + void off(const char* tag) { d_tags.erase (std::string(tag)); } + void off(std::string tag) { d_tags.erase (tag); } - static void setStream(std::ostream& os) { d_out = os; } + void setStream(std::ostream& os) { d_os = &os; } };/* class Debug */ +extern DebugC Debug CVC4_PUBLIC; -class Warning { - std::ostream &d_out; +class CVC4_PUBLIC WarningC { + std::ostream *d_os; public: - static void operator()(const char*); - static void operator()(std::string); + WarningC(std::ostream* os) : d_os(os) {} - static void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3))); - static void printf(std::string fmt, ...) __attribute__ ((format(printf, 2, 3))); + void operator()(const char* s) { *d_os << s; } + void operator()(std::string s) { *d_os << s; } - static std::ostream& operator()(); + void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3))); - static void setStream(std::ostream& os) { d_out = os; } + std::ostream& operator()() { return *d_os; } + + void setStream(std::ostream& os) { d_os = &os; } };/* class Warning */ +extern WarningC Warning CVC4_PUBLIC; -class Notice { - std::ostream &d_os; +class CVC4_PUBLIC NoticeC { + std::ostream *d_os; public: - static void operator()(const char*); - static void operator()(std::string); + NoticeC(std::ostream* os) : d_os(os) {} + + void operator()(const char*); + 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))); + void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3))); - static std::ostream& operator()(); + std::ostream& operator()() { return *d_os; } - static void setStream(std::ostream& os) { d_out = os; } + void setStream(std::ostream& os) { d_os = &os; } };/* class Notice */ +extern NoticeC Notice CVC4_PUBLIC; -class Chat { - std::ostream &d_os; +class CVC4_PUBLIC ChatC { + std::ostream *d_os; public: - static void operator()(const char*); - static void operator()(std::string); + ChatC(std::ostream* os) : d_os(os) {} - static void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3))); - static void printf(std::string fmt, ...) __attribute__ ((format(printf, 2, 3))); + void operator()(const char*); + void operator()(std::string); - static std::ostream& operator()(); + void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3))); - static void setStream(std::ostream& os) { d_out = os; } + std::ostream& operator()() { return *d_os; } + + void setStream(std::ostream& os) { d_os = &os; } };/* class Chat */ +extern ChatC Chat CVC4_PUBLIC; -class Trace { - std::ostream &d_os; +class CVC4_PUBLIC TraceC { + std::ostream *d_os; + std::set<std::string> d_tags; 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); + TraceC(std::ostream* os) : d_os(os) {} - static void printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 2, 3))) { + void operator()(const char* tag, const char*); + void operator()(const char* tag, std::string); + void operator()(std::string tag, const char*); + void operator()(std::string tag, std::string); + + void printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4))) { + char buf[1024]; va_list vl; va_start(vl, fmt); - vfprintf(buf, 1024, fmt, vl); + vsnprintf(buf, sizeof(buf), fmt, vl); va_end(vl); + *d_os << buf; } - 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))) { + void printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4))) { } - static void printf(std::string tag, std::string fmt, ...) __attribute__ ((format(printf, 2, 3))) { + + std::ostream& operator()(const char* tag) { + if(d_tags.find(tag) != d_tags.end()) + return *d_os; + else return null_os; } - static std::ostream& operator()(const char* tag); - static std::ostream& operator()(std::string tag); + std::ostream& operator()(std::string tag) { + if(d_tags.find(tag) != d_tags.end()) + return *d_os; + else return null_os; + } - 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); }; + void on (const char* tag) { d_tags.insert(std::string(tag)); }; + void on (std::string tag) { d_tags.insert(tag); }; + void off(const char* tag) { d_tags.erase (std::string(tag)); }; + void off(std::string tag) { d_tags.erase (tag); }; - static void setStream(std::ostream& os) { d_out = os; } + void setStream(std::ostream& os) { d_os = &os; } };/* class Trace */ +extern TraceC Trace CVC4_PUBLIC; }/* CVC4 namespace */ |