thelibdir="$(abs_builddir)$(libdir)"; progdir="$(abs_builddir)$(bindir)"; file=cvc4; \
eval `grep '^relink_command=' $(CURRENT_BUILD)/src/main/cvc4 | sed 's:-Wl,-rpath:-Wl,-rpath -Wl,\\\\$$thelibdir -Wl,-rpath:'`; \
eval "(cd $(CURRENT_BUILD)/src/main && $$relink_command)"
- ln -sfv "$(abs_builddir)$(libdir)" $(CURRENT_BUILD)/lib
- ln -sfv "$(abs_builddir)$(bindir)" $(CURRENT_BUILD)/bin
+ test -e $(CURRENT_BUILD)/lib || ln -sfv "$(abs_builddir)$(libdir)" $(CURRENT_BUILD)/lib
+ test -e $(CURRENT_BUILD)/bin || ln -sfv "$(abs_builddir)$(bindir)" $(CURRENT_BUILD)/bin
# populate builds/bin and builds/lib
mkdir -pv ".$(bindir)" ".$(libdir)"
$(CURRENT_BUILD)/libtool --mode=install install -v $(CURRENT_BUILD)/src/libcvc4.la "`pwd`$(libdir)"
thelibdir="`pwd`$(libdir)"; progdir="`pwd`$(bindir)"; file=cvc4; \
eval `grep '^relink_command=' $(CURRENT_BUILD)/src/main/cvc4 | sed 's:-Wl,-rpath:-Wl,-rpath -Wl,\\\\$$thelibdir -Wl,-rpath:'`; \
eval "(cd $(CURRENT_BUILD)/src/main && $$relink_command)"
- ln -sfv ".$(libdir)" lib
- ln -sfv ".$(bindir)" bin
+ test -e lib || ln -sfv ".$(libdir)" lib
+ test -e bin || ln -sfv ".$(bindir)" bin
%:
(cd $(CURRENT_BUILD) && $(MAKE) $@)
echo Setting up "builds/$target/$build_type"...
rm -fv config.log config.status confdefs.h
mkdir -pv "builds/$target/$build_type"
- test -e builds/Makefile || ln -sfv "$target/$build_type/Makefile.builds" builds/Makefile
+ ln -sfv "$target/$build_type/Makefile.builds" builds/Makefile
echo Creating builds/current...
(echo "# This is the most-recently-configured CVC4 build"; \
echo "# 'make' in the top-level source directory applies to this build"; \
--- /dev/null
+#!/usr/bin/perl -w
+# DIMACS to SMT
+# Morgan Deters 2009
+
+use strict;
+
+my ($nvars, $nclauses);
+while(<>) {
+ next if /^c/;
+
+ if(/^p cnf (\d+) (\d+)/) {
+ ($nvars, $nclauses) = ($1, $2);
+ print "(benchmark b\n";
+ print ":status unknown\n";
+ print ":logic QF_UF\n";
+ for(my $i = 1; $i <= $nvars; ++$i) {
+ print ":extrapreds ((x$i))\n";
+ }
+ print ":formula (and\n";
+ next;
+ }
+
+ print "(or";
+ chomp;
+ @_ = split(/ /);
+ for(my $i = 0; $i < $#_; ++$i) {
+ if($_[$i] < 0) {
+ print " (not x" . -$_[$i] . ")";
+ } else {
+ print " x" . $_[$i];
+ }
+ }
+ print ")\n";
+}
+
+print "))\n";
public:
/** Default constructor, makes a null expression. */
- CVC4_PUBLIC Expr();
+ Expr();
- CVC4_PUBLIC Expr(const Expr&);
+ Expr(const Expr&);
/** Destructor. Decrements the reference count and, if zero,
* collects the ExprValue. */
- CVC4_PUBLIC ~Expr();
+ ~Expr();
- Expr& operator=(const Expr&) CVC4_PUBLIC;
+ bool operator==(const Expr& e) const { return d_ev == e.d_ev; }
+ bool operator!=(const Expr& e) const { return d_ev != e.d_ev; }
+ bool operator<(const Expr& e) const { return d_ev < e.d_ev; }// for map key
+
+ Expr& operator=(const Expr&);
/** Access to the encapsulated expression.
* @return the encapsulated expression. */
- ExprValue* operator->() const CVC4_PUBLIC;
+ ExprValue* operator->() const;
uint64_t hash() const;
#include "expr_builder.h"
#include "expr_manager.h"
#include "expr_value.h"
-#include "util/assert.h"
+#include "util/Assert.h"
+#include "util/output.h"
using namespace std;
// "Stream" expression constructor syntax
ExprBuilder& ExprBuilder::operator<<(const Kind& op) {
+ d_kind = op;
return *this;
}
ExprBuilder& ExprBuilder::operator<<(const Expr& child) {
+ addChild(child);
return *this;
}
void ExprBuilder::addChild(const Expr& e) {
+ Debug("expr") << "adding child E " << e << endl;
if(d_nchildren == nchild_thresh) {
+ Debug("expr") << "reached thresh " << nchild_thresh << ", copying" << endl;
vector<Expr>* v = new vector<Expr>();
v->reserve(nchild_thresh + 5);
for(ExprValue** i = d_children.u_arr; i != d_children.u_arr + nchild_thresh; ++i) {
d_children.u_vec = v;
++d_nchildren;
} else if(d_nchildren > nchild_thresh) {
+ Debug("expr") << "over thresh " << d_nchildren << " > " << nchild_thresh << endl;
d_children.u_vec->push_back(e);
++d_nchildren;
} else {
+ Debug("expr") << "under thresh " << d_nchildren << " < " << nchild_thresh << endl;
ExprValue *ev = e.d_ev;
d_children.u_arr[d_nchildren] = ev;
ev->inc();
}
void ExprBuilder::addChild(ExprValue* ev) {
+ Debug("expr") << "adding child ev " << ev << endl;
if(d_nchildren == nchild_thresh) {
+ Debug("expr") << "reached thresh " << nchild_thresh << ", copying" << endl;
vector<Expr>* v = new vector<Expr>();
v->reserve(nchild_thresh + 5);
for(ExprValue** i = d_children.u_arr; i != d_children.u_arr + nchild_thresh; ++i) {
d_children.u_vec = v;
++d_nchildren;
} else if(d_nchildren > nchild_thresh) {
+ Debug("expr") << "over thresh " << d_nchildren << " > " << nchild_thresh << endl;
d_children.u_vec->push_back(Expr(ev));
++d_nchildren;
} else {
+ Debug("expr") << "under thresh " << d_nchildren << " < " << nchild_thresh << endl;
d_children.u_arr[d_nchildren] = ev;
ev->inc();
++d_nchildren;
vector<Expr>* v = new vector<Expr>();
v->reserve(nchild_thresh + 5);
//
+ Unreachable();// unimplemented
}
return *this;
}
// For pushing sequences of children
ExprBuilder& append(const std::vector<Expr>& children) { return append(children.begin(), children.end()); }
- ExprBuilder& append(Expr child) { return append(&child, &(child)+1); }
+ ExprBuilder& append(Expr child) { return append(&child, (&child) + 1); }
template <class Iterator> ExprBuilder& append(const Iterator& begin, const Iterator& end);
operator Expr();// not const
template <class Iterator>
inline ExprBuilder& ExprBuilder::append(const Iterator& begin, const Iterator& end) {
+ for(Iterator i = begin; i != end; ++i)
+ addChild(*i);
return *this;
}
// not const
inline ExprBuilder::operator Expr() {
- uint64_t hash = d_kind;
-
- for(ev_iterator i = ev_begin(); i != ev_end(); ++i)
- hash = ((hash << 3) | ((hash & 0xE000000000000000ull) >> 61)) ^ (*i)->hash();
+ ExprValue *ev;
+ uint64_t hash;
+
+ // variables are permitted to be duplicates (from POV of the expression manager)
+ if(d_kind == VARIABLE) {
+ ev = new ExprValue;
+ hash = reinterpret_cast<uint64_t>(ev);
+ } else {
+ hash = d_kind;
+
+ if(d_nchildren <= nchild_thresh) {
+ for(ev_iterator i = ev_begin(); i != ev_end(); ++i)
+ hash = ((hash << 3) | ((hash & 0xE000000000000000ull) >> 61)) ^ (*i)->hash();
+
+ void *space = std::calloc(1, sizeof(ExprValue) + d_nchildren * sizeof(Expr));
+ ev = new (space) ExprValue;
+ size_t nc = 0;
+ for(ev_iterator i = ev_begin(); i != ev_end(); ++i)
+ ev->d_children[nc++] = Expr(*i);
+ } else {
+ for(std::vector<Expr>::iterator i = d_children.u_vec->begin(); i != d_children.u_vec->end(); ++i)
+ hash = ((hash << 3) | ((hash & 0xE000000000000000ull) >> 61)) ^ (*i)->hash();
+
+ void *space = std::calloc(1, sizeof(ExprValue) + d_nchildren * sizeof(Expr));
+ ev = new (space) ExprValue;
+ size_t nc = 0;
+ for(std::vector<Expr>::iterator i = d_children.u_vec->begin(); i != d_children.u_vec->end(); ++i)
+ ev->d_children[nc++] = Expr(*i);
+ }
+ }
- void *space = std::malloc(sizeof(ExprValue) + d_nchildren * sizeof(Expr));
- ExprValue *ev = new (space) ExprValue;
- size_t nc = 0;
- for(ev_iterator i = ev_begin(); i != ev_end(); ++i)
- ev->d_children[nc++] = Expr(*i);
ev->d_nchildren = d_nchildren;
ev->d_kind = d_kind;
- ev->d_id = ExprValue::next_id++;
+ ev->d_id = ExprValue::next_id++;// FIXME multithreading
ev->d_rc = 0;
Expr e(ev);
__thread ExprManager* ExprManager::s_current = 0;
+Expr ExprManager::lookup(uint64_t hash, const Expr& e) {
+ hash_t::iterator i = d_hash.find(hash);
+ if(i == d_hash.end()) {
+ // insert
+ std::vector<Expr> v;
+ v.push_back(e);
+ d_hash.insert(std::make_pair(hash, v));
+ return e;
+ } else {
+ for(std::vector<Expr>::iterator j = i->second.begin(); j != i->second.end(); ++j) {
+ if(e.getKind() != j->getKind())
+ continue;
+
+ if(e.numChildren() != j->numChildren())
+ continue;
+
+ Expr::iterator c1 = e.begin();
+ Expr::iterator c2 = j->begin();
+ for(; c1 != e.end() && c2 != j->end(); ++c1, ++c2) {
+ if(c1->d_ev != c2->d_ev)
+ break;
+ }
+
+ if(c1 != e.end() || c2 != j->end())
+ continue;
+
+ return *j;
+ }
+ // didn't find it, insert
+ std::vector<Expr> v;
+ v.push_back(e);
+ d_hash.insert(std::make_pair(hash, v));
+ return e;
+ }
+}
+
// general expression-builders
Expr ExprManager::mkExpr(Kind kind) {
return ExprBuilder(this, kind).append(children);
}
+Expr ExprManager::mkVar() {
+ return ExprBuilder(this, VARIABLE);
+}
+
}/* CVC4 namespace */
typedef std::map<uint64_t, std::vector<Expr> > hash_t;
hash_t d_hash;
- Expr lookup(uint64_t hash, const Expr& e) {
- hash_t::iterator i = d_hash.find(hash);
- if(i == d_hash.end()) {
- // insert
- std::vector<Expr> v;
- v.push_back(e);
- d_hash.insert(std::make_pair(hash, v));
- return e;
- } else {
- for(std::vector<Expr>::iterator j = i->second.begin(); j != i->second.end(); ++j) {
- if(e.getKind() != j->getKind())
- continue;
-
- if(e.numChildren() != j->numChildren())
- continue;
-
- Expr::iterator c1 = e.begin();
- Expr::iterator c2 = j->begin();
- while(c1 != e.end() && c2 != j->end()) {
- if(c1->d_ev != c2->d_ev)
- break;
- }
-
- if(c1 != e.end() || c2 != j->end())
- continue;
-
- return *j;
- }
- // didn't find it, insert
- std::vector<Expr> v;
- v.push_back(e);
- d_hash.insert(std::make_pair(hash, v));
- return e;
- }
- }
+ Expr lookup(uint64_t hash, const Expr& e);
public:
static ExprManager* currentEM() { return s_current; }
// N-ary version
Expr mkExpr(Kind kind, std::vector<Expr> children);
+ // variables are special, because duplicates are permitted
+ Expr mkVar();
+
// TODO: these use the current EM (but must be renamed)
/*
static Expr mkExpr(Kind kind)
namespace CVC4 {
+size_t ExprValue::next_id = 1;
+
ExprValue::ExprValue() :
d_id(0), d_rc(MAX_RC), d_kind(NULL_EXPR), d_nchildren(0) {
}
-size_t ExprValue::next_id = 1;
-
uint64_t ExprValue::hash() const {
uint64_t hash = d_kind;
return d_children - 1;
}
+void ExprValue::toString(std::ostream& out) const {
+ out << "(" << Kind(d_kind);
+ if(d_kind == VARIABLE) {
+ out << ":" << this;
+ } else {
+ for(const_iterator i = begin(); i != end(); ++i) {
+ if(i != end())
+ out << " ";
+ out << *i;
+ }
+ }
+ out << ")";
+}
+
}/* CVC4 namespace */
#ifndef __CVC4__EXPR__EXPR_VALUE_H
#define __CVC4__EXPR__EXPR_VALUE_H
+#include "cvc4_config.h"
#include <stdint.h>
+#include "kind.h"
namespace CVC4 {
const_iterator rbegin() const;
const_iterator rend() const;
- void toString(std::ostream& out) {
- out << Kind(d_kind);
- }
+ void CVC4_PUBLIC toString(std::ostream& out) const;
};
}/* CVC4::expr namespace */
};/* enum Kind */
-}/* CVC4 namespace */
-
-inline std::ostream& operator<<(std::ostream&, const CVC4::Kind&) CVC4_PUBLIC;
-inline std::ostream& operator<<(std::ostream& out, const CVC4::Kind& k) {
+inline std::ostream& operator<<(std::ostream&, CVC4::Kind) CVC4_PUBLIC;
+inline std::ostream& operator<<(std::ostream& out, CVC4::Kind k) {
using namespace CVC4;
switch(k) {
+
+ /* special cases */
case UNDEFINED_KIND: out << "UNDEFINED_KIND"; break;
case NULL_EXPR: out << "NULL"; break;
+
case EQUAL: out << "EQUAL"; break;
case ITE: out << "ITE"; break;
case SKOLEM: out << "SKOLEM"; break;
return out;
}
+}/* CVC4 namespace */
+
#endif /* __CVC4__KIND_H */
#include "util/exception.h"
#include "usage.h"
#include "about.h"
+#include "util/output.h"
using namespace std;
using namespace CVC4;
progName = x + 1;
opts->binary_name = string(progName);
- while((c = getopt_long(argc, argv, "+:hVvqL:", cmdlineOptions, NULL)) != -1) {
+ while((c = getopt_long(argc, argv, "+:hVvqL:d:", cmdlineOptions, NULL)) != -1) {
switch(c) {
case 'h':
fputs(lang_help, stdout);
exit(1);
+ case 'd':
+ Debug.on(optarg);
+
case STATS:
opts->statistics = true;
break;
#include <iostream>
#include <fstream>
#include <cstdlib>
+#include <cstring>
#include <new>
#include "config.h"
#include "expr/expr_manager.h"
#include "smt/smt_engine.h"
#include "util/command.h"
+#include "util/output.h"
using namespace std;
using namespace CVC4;
if(options.smtcomp_mode)
cout << unitbuf;
- // We only accept one input file
+ // We only accept one input file
if(argc > firstArgIndex + 1)
throw new Exception("Too many input files specified.");
// Create the expression manager
ExprManager exprMgr;
+
// Create the SmtEngine
SmtEngine smt(&exprMgr, &options);
// If no file supplied we read from standard input
bool inputFromStdin = firstArgIndex >= argc;
+ if(!inputFromStdin && options.lang == Options::LANG_AUTO) {
+ if(!strcmp(".smt", argv[firstArgIndex] + strlen(argv[firstArgIndex]) - 4))
+ options.lang = Options::LANG_SMTLIB;
+ else if(!strcmp(".cvc", argv[firstArgIndex] + strlen(argv[firstArgIndex]) - 4) ||
+ !strcmp(".cvc4", argv[firstArgIndex] + strlen(argv[firstArgIndex]) - 5))
+ options.lang = Options::LANG_CVC4;
+ }
+
+ if(options.smtcomp_mode) {
+ Debug.setStream(CVC4::null_os);
+ Trace.setStream(CVC4::null_os);
+ Notice.setStream(CVC4::null_os);
+ Chat.setStream(CVC4::null_os);
+ Warning.setStream(CVC4::null_os);
+ } else {
+ if(options.verbosity < 2)
+ Chat.setStream(CVC4::null_os);
+ if(options.verbosity < 1)
+ Notice.setStream(CVC4::null_os);
+ if(options.verbosity < 0)
+ Warning.setStream(CVC4::null_os);
+ }
+
// Create the parser
Parser* parser;
switch(options.lang) {
abort();
}
- // Parse the and execute commands until we are done
+ // Parse and execute commands until we are done
while(!parser->done()) {
// Parse the next command
Command *cmd = parser->parseNextCommand();
#include "antlr_parser.h"
#include "expr/expr_manager.h"
+#include "util/output.h"
using namespace std;
using namespace CVC4;
using namespace CVC4::parser;
-ostream& operator <<(ostream& out, AntlrParser::BenchmarkStatus status) {
+namespace CVC4 {
+namespace parser {
+
+ostream& operator<<(ostream& out, AntlrParser::BenchmarkStatus status) {
switch(status) {
case AntlrParser::SMT_SATISFIABLE:
out << "sat";
}
Expr AntlrParser::getVariable(std::string var_name) {
- return d_var_symbol_table.getObject(var_name);
+ Expr e = d_var_symbol_table.getObject(var_name);
+ Debug("parser") << "getvar " << var_name << " gives " << e << endl;
+ return e;
}
Expr AntlrParser::getTrueExpr() const {
void AntlrParser::newPredicate(std::string p_name, const std::vector<
std::string>& p_sorts) {
if(p_sorts.size() == 0)
- d_var_symbol_table.bindName(p_name, d_expr_manager->mkExpr(VARIABLE));
+ d_var_symbol_table.bindName(p_name, d_expr_manager->mkVar());
else
Unhandled("Non unary predicate not supported yet!");
}
Expr child_2 = createPrecedenceExpr(exprs, kinds, pivot + 1, end_index);
return d_expr_manager->mkExpr(kinds[pivot], child_1, child_2);
}
+
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
#include "expr/expr.h"
#include "expr/expr_manager.h"
#include "util/command.h"
-#include "util/assert.h"
+#include "util/Assert.h"
#include "parser/symbol_table.h"
namespace CVC4 {
BUILT_SOURCES = $(ANTLR_STUFF)
CLEAN_FILES = $(ANTLR_STUFF)
-AntlrCvcLexer.cpp AntlrCvcLexer.hpp: CvcLexer.g
+AntlrCvcLexer.cpp: CvcLexer.g
$(ANTLR) -o "@builddir@" "$<"
-AntlrCvcParser.cpp AntlrCvcParser.hpp: CvcParser.g
+AntlrCvcParser.cpp: CvcParser.g CvcVocabularyTokenTypes.hpp CvcVocabularyTokenTypes.txt
$(ANTLR) -o "@builddir@" "$<"
+AntlrCvcLexer.hpp CvcVocabularyTokenTypes.hpp CvcVocabularyTokenTypes.txt: AntlrCvcLexer.cpp
+AntlrCvcParser.hpp: AntlrCvcParser.cpp
#include "parser.h"
#include "util/command.h"
-#include "util/assert.h"
+#include "util/Assert.h"
#include "parser_exception.h"
#include "parser/antlr_parser.h"
#include "parser/smt/AntlrSmtParser.hpp"
BUILT_SOURCES = $(ANTLR_STUFF)
CLEAN_FILES = $(ANTLR_STUFF)
-AntlrSmtLexer.cpp AntlrSmtLexer.hpp: SmtLexer.g
+AntlrSmtLexer.cpp: SmtLexer.g
$(ANTLR) -o "@builddir@" "$<"
-AntlrSmtParser.cpp AntlrSmtParser.hpp: SmtParser.g
+AntlrSmtParser.cpp: SmtParser.g SmtVocabularyTokenTypes.hpp SmtVocabularyTokenTypes.txt
$(ANTLR) -o "@builddir@" "$<"
+AntlrSmtLexer.hpp SmtVocabularyTokenTypes.hpp SmtVocabularyTokenTypes.txt: AntlrSmtLexer.cpp
+AntlrSmtParser.hpp: AntlrSmtParser.cpp
**
**/
+#ifndef __CVC4__PARSER__SYMBOL_TABLE_H
+#define __CVC4__PARSER__SYMBOL_TABLE_H
+
#include <string>
#include <stack>
#include <ext/hash_map>
* Generic symbol table for looking up variables by name.
*/
template<typename ObjectType>
- class SymbolTable {
+class SymbolTable {
- private:
+private:
- /** The name to expression bindings */
- typedef __gnu_cxx ::hash_map<std::string, std::stack<ObjectType> >
- LookupTable;
- /** The table iterator */
- typedef typename LookupTable::iterator table_iterator;
- /** The table iterator */
- typedef typename LookupTable::const_iterator const_table_iterator;
+ /** The name to expression bindings */
+ typedef __gnu_cxx ::hash_map<std::string, std::stack<ObjectType> >
+ LookupTable;
+ /** The table iterator */
+ typedef typename LookupTable::iterator table_iterator;
+ /** The table iterator */
+ typedef typename LookupTable::const_iterator const_table_iterator;
- /** Bindings for the names */
- LookupTable d_name_bindings;
+ /** Bindings for the names */
+ LookupTable d_name_bindings;
- public:
+public:
- /**
- * Bind the name of the variable to the given expression. If the variable
- * has been bind before, this will redefine it until its undefined.
- */
- void bindName(const std::string name, const ObjectType& obj) throw () {
- d_name_bindings[name].push(obj);
- }
+ /**
+ * Bind the name of the variable to the given expression. If the variable
+ * has been bind before, this will redefine it until its undefined.
+ */
+ void bindName(const std::string name, const ObjectType& obj) throw () {
+ d_name_bindings[name].push(obj);
+ }
- /**
- * Unbinds the last binding of the name to the expression.
- */
- void unbindName(const std::string name) throw () {
- table_iterator find = d_name_bindings.find(name);
- if(find != d_name_bindings.end()) {
- find->second.pop();
- if(find->second.empty()) {
- d_name_bindings.erase(find);
- }
+ /**
+ * Unbinds the last binding of the name to the expression.
+ */
+ void unbindName(const std::string name) throw () {
+ table_iterator find = d_name_bindings.find(name);
+ if(find != d_name_bindings.end()) {
+ find->second.pop();
+ if(find->second.empty()) {
+ d_name_bindings.erase(find);
}
}
+ }
- /**
- * Returns the last binding expression of the name.
- */
- ObjectType getObject(const std::string name) throw () {
- ObjectType result;
- table_iterator find = d_name_bindings.find(name);
- if(find != d_name_bindings.end())
- result = find->second.top();
- return result;
- }
+ /**
+ * Returns the last binding expression of the name.
+ */
+ ObjectType getObject(const std::string name) throw () {
+ ObjectType result;
+ table_iterator find = d_name_bindings.find(name);
+ if(find != d_name_bindings.end())
+ result = find->second.top();
+ return result;
+ }
- /**
- * Returns true is name is bound to an expression.
- */
- bool isBound(const std::string name) const throw () {
- const_table_iterator find = d_name_bindings.find(name);
- return (find != d_name_bindings.end());
- }
- };
+ /**
+ * Returns true is name is bound to an expression.
+ */
+ bool isBound(const std::string name) const throw () {
+ const_table_iterator find = d_name_bindings.find(name);
+ return (find != d_name_bindings.end());
+ }
+};
}/* CVC4::parser namespace */
}/* CVC4 namespace */
+
+#endif /* __CVC4__PARSER__SYMBOL_TABLE_H */
// Constructor/Destructor:
namespace CVC4 {
-namespace MiniSat {
+namespace prop {
+namespace minisat {
Solver::Solver() :
}
}
-}/* CVC4::MiniSat namespace */
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
}/* CVC4 namespace */
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
**************************************************************************************************/
-#ifndef CVC4_MiniSat_Solver_h
-#define CVC4_MiniSat_Solver_h
+#ifndef __CVC4__PROP__MINISAT__SOLVER_H
+#define __CVC4__PROP__MINISAT__SOLVER_H
#include <cstdio>
+#include <cassert>
-#include "Vec.h"
-#include "Heap.h"
-#include "Alg.h"
+#include "cvc4_config.h"
+#include "../mtl/Vec.h"
+#include "../mtl/Heap.h"
+#include "../mtl/Alg.h"
#include "SolverTypes.h"
// Solver -- the main class:
namespace CVC4 {
-namespace MiniSat {
+namespace prop {
+namespace minisat {
class Solver {
public:
// Constructor/Destructor:
//
Solver();
- ~Solver();
+ CVC4_PUBLIC ~Solver();
// Problem specification:
//
bool okay () const; // FALSE means solver is in a conflicting state
// Variable mode:
- //
+ //
void setPolarity (Var v, bool b); // Declare which polarity the decision heuristic should use for a variable. Requires mode 'polarity_user'.
void setDecisionVar (Var v, bool b); // Declare if a variable should be eligible for selection in the decision heuristic.
#define reportf(format, args...) ( fflush(stdout), fprintf(stderr, format, ## args), fflush(stderr) )
+//#define reportf(format, args...) do {} while(0)
static inline void logLit(FILE* f, Lit l)
{
}
}
-}/* CVC4::MiniSat namespace */
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
}/* CVC4 namespace */
//=================================================================================================
-#endif /* CVC4_MiniSat_Solver_h */
+#endif /* __CVC4__PROP__MINISAT__SOLVER_H */
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
**************************************************************************************************/
-#ifndef CVC4_MiniSat_SolverTypes_h
-#define CVC4_MiniSat_SolverTypes_h
+#ifndef __CVC4__PROP__MINISAT__SOLVERTYPES_H
+#define __CVC4__PROP__MINISAT__SOLVERTYPES_H
#include <cassert>
#include <stdint.h>
namespace CVC4 {
-namespace MiniSat {
+namespace prop {
+namespace minisat {
//=================================================================================================
// Variables, literals, lifted booleans, clauses:
calcAbstraction();
}
-}/* CVC4::MiniSat namespace */
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
}/* CVC4 namespace */
-#endif /* CVC4_MiniSat_SolverTypes_h */
+#endif /* __CVC4__PROP__MINISAT__SOLVERTYPES_H */
#ifndef CVC4_MiniSat_Alg_h
#define CVC4_MiniSat_Alg_h
+#include <cassert>
+
namespace CVC4 {
-namespace MiniSat {
+namespace prop {
+namespace minisat {
//=================================================================================================
// Useful functions on vectors
return j < ts.size();
}
-}/* CVC4::MiniSat namespace */
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
}/* CVC4 namespace */
#endif /* CVC4_MiniSat_Alg_h */
#include "Vec.h"
namespace CVC4 {
-namespace MiniSat {
+namespace prop {
+namespace minisat {
//=================================================================================================
// A heap implementation with support for decrease/increase key.
//=================================================================================================
-}/* CVC4::MiniSat namespace */
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
}/* CVC4 namespace */
#endif /* CVC4_MiniSat_BasicHeap_h */
#include <new>
namespace CVC4 {
-namespace MiniSat {
+namespace prop {
+namespace minisat {
//=================================================================================================
// Automatically resizable arrays
x->cap = size;
return x;
}
-
+
};
Vec_t* ref;
altvec (altvec<T>& other) { assert(0); }
public:
- void clear (bool dealloc = false) {
+ void clear (bool dealloc = false) {
if (ref != NULL){
- for (int i = 0; i < ref->sz; i++)
+ for (int i = 0; i < ref->sz; i++)
(*ref).data[i].~T();
- if (dealloc) {
- free(ref); ref = NULL;
- }else
+ if (dealloc) {
+ free(ref); ref = NULL;
+ }else
ref->sz = 0;
- }
+ }
}
// Constructors:
int cap = ref != NULL ? ref->cap : 0;
if (size == cap){
cap = cap != 0 ? nextSize(cap) : init_size;
- ref = Vec_t::alloc(ref, cap);
+ ref = Vec_t::alloc(ref, cap);
}
- //new (&ref->data[size]) T(elem);
- ref->data[size] = elem;
- ref->sz = size+1;
+ //new (&ref->data[size]) T(elem);
+ ref->data[size] = elem;
+ ref->sz = size+1;
}
void push () {
int cap = ref != NULL ? ref->cap : 0;
if (size == cap){
cap = cap != 0 ? nextSize(cap) : init_size;
- ref = Vec_t::alloc(ref, cap);
+ ref = Vec_t::alloc(ref, cap);
}
- new (&ref->data[size]) T();
- ref->sz = size+1;
+ new (&ref->data[size]) T();
+ ref->sz = size+1;
}
void shrink (int nelems) { for (int i = 0; i < nelems; i++) pop(); }
};
-}/* CVC4::MiniSat namespace */
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
}/* CVC4 namespace */
#endif /* CVC4_MiniSat_BoxedVec_h */
#define CVC4_MiniSat_Heap_h
#include "Vec.h"
+#include <cassert>
namespace CVC4 {
-namespace MiniSat {
+namespace prop {
+namespace minisat {
//=================================================================================================
// A heap implementation with support for decrease/increase key.
indices[n] = heap.size();
heap.push(n);
- percolateUp(indices[n]);
+ percolateUp(indices[n]);
}
indices[x] = -1;
heap.pop();
if (heap.size() > 1) percolateDown(0);
- return x;
+ return x;
}
- void clear(bool dealloc = false)
- {
+ void clear(bool dealloc = false)
+ {
for (int i = 0; i < heap.size(); i++)
indices[heap[i]] = -1;
#ifdef NDEBUG
for (int i = 0; i < indices.size(); i++)
assert(indices[i] == -1);
#endif
- heap.clear(dealloc);
+ heap.clear(dealloc);
}
};
-}/* CVC4::MiniSat namespace */
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
}/* CVC4 namespace */
//=================================================================================================
#include "Vec.h"
namespace CVC4 {
-namespace MiniSat {
+namespace prop {
+namespace minisat {
//=================================================================================================
// Default hash/equals functions
cap = newsize;
}
-
+
public:
Map () : table(NULL), cap(0), size(0) {}
for (int i = 0; i < ps.size(); i++)
if (equals(ps[i].key, k)){
d = ps[i].data;
- return true; }
+ return true; }
return false;
}
}
};
-}/* CVC4::MiniSat namespace */
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
}/* CVC4 namespace */
#endif /* CVC4_MiniSat_Map_h */
#include "Vec.h"
namespace CVC4 {
-namespace MiniSat {
+namespace prop {
+namespace minisat {
//=================================================================================================
//=================================================================================================
-}/* CVC4::MiniSat namespace */
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
}/* CVC4 namespace */
#endif /* CVC4_MiniSat_Queue_h */
#include "Vec.h"
namespace CVC4 {
-namespace MiniSat {
+namespace prop {
+namespace minisat {
//=================================================================================================
// Some sorting algorithms for vec's
//=================================================================================================
-}/* CVC4::MiniSat namespace */
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
}/* CVC4 namespace */
#endif /* CVC4_MiniSat_Sort_h */
#include <new>
namespace CVC4 {
-namespace MiniSat {
+namespace prop {
+namespace minisat {
//=================================================================================================
// Automatically resizable arrays
sz = 0;
if (dealloc) free(data), data = NULL, cap = 0; } }
-}/* CVC4::MiniSat namespace */
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
}/* CVC4 namespace */
#endif /* CVC4_MiniSat_Vec_h */
// Constructor/Destructor:
namespace CVC4 {
-namespace MiniSat {
+namespace prop {
+namespace minisat {
SimpSolver::SimpSolver() :
grow (0)
for (int i = 0; i < qs.size(); i++){
if (var(qs[i]) != v){
for (int j = 0; j < ps.size(); j++)
- if (var(ps[j]) == var(qs[i]))
+ if (var(ps[j]) == var(qs[i])) {
if (ps[j] == ~qs[i])
return false;
else
goto next;
+ }
out_clause.push(qs[i]);
}
next:;
for (int i = 0; i < qs.size(); i++){
if (var(__qs[i]) != v){
for (int j = 0; j < ps.size(); j++)
- if (var(__ps[j]) == var(__qs[i]))
+ if (var(__ps[j]) == var(__qs[i])) {
if (__ps[j] == ~__qs[i])
return false;
else
goto next;
+ }
}
next:;
}
fprintf(stderr, "could not open file %s\n", file);
}
-}/* CVC4::MiniSat namespace */
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
}/* CVC4 namespace */
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
**************************************************************************************************/
-#ifndef CVC4_MiniSat_SimpSolver_h
-#define CVC4_MiniSat_SimpSolver_h
+#ifndef __CVC4__PROP__MINISAT__SIMP_SOLVER_H
+#define __CVC4__PROP__MINISAT__SIMP_SOLVER_H
#include <cstdio>
+#include <cassert>
-#include "Queue.h"
-#include "Solver.h"
+#include "../mtl/Queue.h"
+#include "../core/Solver.h"
namespace CVC4 {
-namespace MiniSat {
+namespace prop {
+namespace minisat {
class SimpSolver : public Solver {
public:
// Constructor/Destructor:
//
SimpSolver();
- ~SimpSolver();
+ CVC4_PUBLIC ~SimpSolver();
// Problem specification:
//
inline void SimpSolver::setFrozen (Var v, bool b) { frozen[v] = (char)b; if (b) { updateElimHeap(v); } }
inline bool SimpSolver::solve (bool do_simp, bool turn_off_simp) { vec<Lit> tmp; return solve(tmp, do_simp, turn_off_simp); }
-}/* CVC4::MiniSat namespace */
+}/* CVC4::prop::minisat namespace */
+}/* CVC4::prop namespace */
}/* CVC4 namespace */
//=================================================================================================
-#endif /* CVC4_MiniSat_SimpSolver_h */
+#endif /* __CVC4__PROP__MINISAT__SIMP_SOLVER_H */
+/********************* -*- C++ -*- */
+/** prop_engine.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.
+ **
+ **/
+
+#include "prop/prop_engine.h"
+#include "theory/theory_engine.h"
+#include "util/decision_engine.h"
+#include "prop/minisat/mtl/Vec.h"
+#include "prop/minisat/simp/SimpSolver.h"
+#include "prop/minisat/core/SolverTypes.h"
+#include "util/Assert.h"
+#include "util/output.h"
+
+#include <utility>
+#include <map>
+
+using namespace CVC4::prop::minisat;
+using namespace std;
+
+namespace CVC4 {
+
+PropEngine::PropEngine(DecisionEngine& de, TheoryEngine& te) :
+ d_de(de), d_te(te), d_sat() {
+}
+
+void PropEngine::addVars(Expr e) {
+ Debug("prop") << "adding vars to " << e << endl;
+ for(Expr::iterator i = e.begin(); i != e.end(); ++i) {
+ Debug("prop") << "expr " << *i << endl;
+ if(i->getKind() == VARIABLE) {
+ if(d_vars.find(*i) == d_vars.end()) {
+ Var v = d_sat.newVar();
+ Debug("prop") << "adding var " << *i << " <--> " << v << endl;
+ d_vars.insert(make_pair(*i, v));
+ d_varsReverse.insert(make_pair(v, *i));
+ } else Debug("prop") << "using var " << *i << " <--> " << d_vars[*i] << endl;
+ } else addVars(*i);
+ }
+}
+
+static void doAtom(SimpSolver* minisat, map<Expr, Var>* vars, Expr e, vec<Lit>* c) {
+ if(e.getKind() == VARIABLE) {
+ map<Expr, Var>::iterator v = vars->find(e);
+ Assert(v != vars->end());
+ c->push(Lit(v->second, false));
+ return;
+ }
+ if(e.getKind() == NOT) {
+ Assert(e.numChildren() == 1);
+ Expr child = *e.begin();
+ Assert(child.getKind() == VARIABLE);
+ map<Expr, Var>::iterator v = vars->find(child);
+ Assert(v != vars->end());
+ c->push(Lit(v->second, true));
+ return;
+ }
+ Unhandled();
+}
+
+static void doClause(SimpSolver* minisat, map<Expr, Var>* vars, map<Var, Expr>* varsReverse, Expr e) {
+ vec<Lit> c;
+ Debug("prop") << " " << e << endl;
+ if(e.getKind() == VARIABLE || e.getKind() == NOT) {
+ doAtom(minisat, vars, e, &c);
+ } else {
+ Assert(e.getKind() == OR);
+ for(Expr::iterator i = e.begin(); i != e.end(); ++i) {
+ Debug("prop") << " " << *i << endl;
+ doAtom(minisat, vars, *i, &c);
+ }
+ }
+ Notice() << "added clause of length " << c.size() << endl;
+ for(int i = 0; i < c.size(); ++i)
+ Notice() << " " << (sign(c[i]) ? "-" : "") << var(c[i]);
+ Notice() << " [[";
+ for(int i = 0; i < c.size(); ++i)
+ Notice() << " " << (sign(c[i]) ? "-" : "") << (*varsReverse)[var(c[i])];
+ Notice() << " ]] " << endl;
+ minisat->addClause(c);
+}
+
+void PropEngine::solve(Expr e) {
+ Debug("prop") << "SOLVING " << e << endl;
+ addVars(e);
+ if(e.getKind() == AND) {
+ Debug("prop") << "AND" << endl;
+ for(Expr::iterator i = e.begin(); i != e.end(); ++i)
+ doClause(&d_sat, &d_vars, &d_varsReverse, *i);
+ } else doClause(&d_sat, &d_vars, &d_varsReverse, e);
+
+ d_sat.verbosity = 1;
+ bool result = d_sat.solve();
+
+ Notice() << "result is " << (result ? "sat" : "unsat") << endl;
+ if(result) {
+ Notice() << "model:" << endl;
+ for(int i = 0; i < d_sat.model.size(); ++i)
+ Notice() << " " << toInt(d_sat.model[i]);
+ Notice() << endl;
+ for(int i = 0; i < d_sat.model.size(); ++i)
+ Notice() << " " << d_varsReverse[i] << " is "
+ << (d_sat.model[i] == l_False ? "FALSE" :
+ (d_sat.model[i] == l_Undef ? "UNDEF" :
+ "TRUE")) << endl;
+ } else {
+ Notice() << "conflict:" << endl;
+ for(int i = 0; i < d_sat.conflict.size(); ++i)
+ Notice() << " " << (sign(d_sat.conflict[i]) ? "-" : "") << var(d_sat.conflict[i]);
+ Notice() << " [[";
+ for(int i = 0; i < d_sat.conflict.size(); ++i)
+ Notice() << " " << (sign(d_sat.conflict[i]) ? "-" : "") << d_varsReverse[var(d_sat.conflict[i])];
+ Notice() << " ]] " << endl;
+ }
+}
+
+}/* CVC4 namespace */
**
**/
-#ifndef __CVC4__PROP__PROP_ENGINE_H
-#define __CVC4__PROP__PROP_ENGINE_H
+#ifndef __CVC4__PROP_ENGINE_H
+#define __CVC4__PROP_ENGINE_H
+#include "cvc4_config.h"
#include "expr/expr.h"
#include "util/decision_engine.h"
#include "theory/theory_engine.h"
+#include "prop/minisat/simp/SimpSolver.h"
+#include "prop/minisat/core/SolverTypes.h"
+
+#include <map>
namespace CVC4 {
-namespace prop {
// In terms of abstraction, this is below (and provides services to)
// Prover and above (and requires the services of) a specific
// propositional solver, DPLL or otherwise.
class PropEngine {
- DecisionEngine* d_de;
+ DecisionEngine &d_de;
+ TheoryEngine &d_te;
+ CVC4::prop::minisat::SimpSolver d_sat;
+ std::map<Expr, CVC4::prop::minisat::Var> d_vars;
+ std::map<CVC4::prop::minisat::Var, Expr> d_varsReverse;
+
+ void addVars(Expr);
public:
/**
* Create a PropEngine with a particular decision and theory engine.
*/
- PropEngine(DecisionEngine*, TheoryEngine*);
+ CVC4_PUBLIC PropEngine(CVC4::DecisionEngine&, CVC4::TheoryEngine&);
/**
* Converts to CNF if necessary.
};/* class PropEngine */
-}/* CVC4::prop namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__PROP__PROP_ENGINE_H */
+#endif /* __CVC4__PROP_ENGINE_H */
for(std::vector<Expr>::iterator i = d_assertions.begin();
i != d_assertions.end();
++i)
- ;//d_expr = d_expr.isNull() ? *i : d_expr.andExpr(*i);
+ d_expr = d_expr.isNull() ? *i : d_expr.andExpr(*i);
}
Result SmtEngine::check() {
processAssertionList();
+ d_prop.solve(d_expr);
return Result(Result::VALIDITY_UNKNOWN);
}
return check();
}
-Result SmtEngine::assert(Expr e) {
+Result SmtEngine::assertFormula(Expr e) {
e = preprocess(e);
addFormula(e);
return quickCheck();
#include "util/result.h"
#include "util/model.h"
#include "util/options.h"
+#include "prop/prop_engine.h"
+#include "util/decision_engine.h"
// In terms of abstraction, this is below (and provides services to)
// ValidityChecker and above (and requires the services of)
/** Expression built-up for handing off to the propagation engine */
Expr d_expr;
+ /** The decision engine */
+ DecisionEngine d_de;
+
+ /** The decision engine */
+ TheoryEngine d_te;
+
+ /** The propositional engine */
+ PropEngine d_prop;
+
/**
* Pre-process an Expr. This is expected to be highly-variable,
* with a lot of "source-level configurability" to add multiple
/*
* Construct an SmtEngine with the given expression manager and user options.
*/
- SmtEngine(ExprManager* em, Options* opts) throw() : d_em(em), d_opts(opts), d_expr(Expr::null()) {}
+ SmtEngine(ExprManager* em, Options* opts) throw() :
+ d_em(em),
+ d_opts(opts),
+ d_expr(Expr::null()),
+ d_de(),
+ d_te(),
+ d_prop(d_de, d_te) {
+ }
/**
* Execute a command.
* literals and conjunction of literals. Returns false iff
* inconsistent.
*/
- Result assert(Expr);
+ Result assertFormula(Expr);
/**
* Add a formula to the current context and call check(). Returns
**
**/
-#ifndef __CVC4__THEORY__THEORY_ENGINE_H
-#define __CVC4__THEORY__THEORY_ENGINE_H
+#ifndef __CVC4__THEORY_ENGINE_H
+#define __CVC4__THEORY_ENGINE_H
namespace CVC4 {
-namespace theory {
// In terms of abstraction, this is below (and provides services to)
// PropEngine.
public:
};/* class TheoryEngine */
-}/* CVC4::theory namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__THEORY__THEORY_ENGINE_H */
+#endif /* __CVC4__THEORY_ENGINE_H */
--- /dev/null
+/********************* -*- C++ -*- */
+/** assert.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.
+ **
+ ** Assertion utility classes, functions, and exceptions.
+ **/
+
+#ifndef __CVC4__ASSERT_H
+#define __CVC4__ASSERT_H
+
+#include <string>
+#include "util/exception.h"
+#include "cvc4_config.h"
+#include "config.h"
+
+namespace CVC4 {
+
+class CVC4_PUBLIC AssertionException : public Exception {
+public:
+ AssertionException() : Exception() {}
+ AssertionException(std::string msg) : Exception(msg) {}
+ AssertionException(const char* msg) : Exception(msg) {}
+};/* class AssertionException */
+
+class CVC4_PUBLIC UnreachableCodeException : public AssertionException {
+public:
+ UnreachableCodeException() : AssertionException() {}
+ UnreachableCodeException(std::string msg) : AssertionException(msg) {}
+ UnreachableCodeException(const char* msg) : AssertionException(msg) {}
+};/* class UnreachableCodeException */
+
+class CVC4_PUBLIC UnhandledCaseException : public UnreachableCodeException {
+public:
+ UnhandledCaseException() : UnreachableCodeException() {}
+ UnhandledCaseException(std::string msg) : UnreachableCodeException(msg) {}
+ UnhandledCaseException(const char* msg) : UnreachableCodeException(msg) {}
+};/* class UnhandledCaseException */
+
+#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(msg...) __CVC4_UNREACHABLEGLUE("Hit a section of unreachable code at " __FILE__ ":", __LINE__, ## msg)
+#define Unhandled(msg...) __CVC4_UNHANDLEDGLUE("Hit an unhandled case at " __FILE__ ":", __LINE__, ## msg)
+
+#define __CVC4_ASSERTGLUE(str1, line, str2, cond, msg...) AssertImpl(str1 #line str2, cond, ## msg)
+#define __CVC4_UNREACHABLEGLUE(str, line, msg...) UnreachableImpl(str #line, ## msg)
+#define __CVC4_UNHANDLEDGLUE(str, line, msg...) UnhandledImpl(str #line, ## msg)
+
+inline void AssertImpl(const char* info, bool cond, std::string msg) {
+ if(EXPECT_FALSE( ! cond ))
+ throw AssertionException(std::string(info) + "\n" + msg);
+}
+
+inline void AssertImpl(const char* info, bool cond, const char* msg) {
+ if(EXPECT_FALSE( ! cond ))
+ throw AssertionException(std::string(info) + "\n" + msg);
+}
+
+inline void AssertImpl(const char* info, bool cond) {
+ if(EXPECT_FALSE( ! cond ))
+ throw 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 UnreachableCodeException(std::string(info) + "\n" + msg);
+}
+
+inline void UnreachableImpl(const char* info, const char* msg) {
+ throw UnreachableCodeException(std::string(info) + "\n" + msg);
+}
+
+inline void UnreachableImpl(const char* info) {
+ throw UnreachableCodeException(info);
+}
+
+#ifdef __GNUC__
+inline void UnhandledImpl(const char* info, std::string msg) __attribute__ ((noreturn));
+inline void UnhandledImpl(const char* info, const char* msg) __attribute__ ((noreturn));
+inline void UnhandledImpl(const char* info) __attribute__ ((noreturn));
+#endif /* __GNUC__ */
+
+inline void UnhandledImpl(const char* info, std::string msg) {
+ throw UnhandledCaseException(std::string(info) + "\n" + msg);
+}
+
+inline void UnhandledImpl(const char* info, const char* msg) {
+ throw UnhandledCaseException(std::string(info) + "\n" + msg);
+}
+
+inline void UnhandledImpl(const char* info) {
+ throw UnhandledCaseException(info);
+}
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__ASSERT_H */
noinst_LTLIBRARIES = libutil.la
libutil_la_SOURCES = \
- command.cpp
+ command.cpp \
+ decision_engine.cpp \
+ output.cpp
+++ /dev/null
-/********************* -*- C++ -*- */
-/** assert.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.
- **
- ** Assertion utility classes, functions, and exceptions.
- **/
-
-#ifndef __CVC4__ASSERT_H
-#define __CVC4__ASSERT_H
-
-#include <string>
-#include "util/exception.h"
-#include "cvc4_config.h"
-#include "config.h"
-
-namespace CVC4 {
-
-class CVC4_PUBLIC AssertionException : public Exception {
-public:
- AssertionException() : Exception() {}
- AssertionException(std::string msg) : Exception(msg) {}
- AssertionException(const char* msg) : Exception(msg) {}
-};/* class AssertionException */
-
-class CVC4_PUBLIC UnreachableCodeException : public AssertionException {
-public:
- UnreachableCodeException() : AssertionException() {}
- UnreachableCodeException(std::string msg) : AssertionException(msg) {}
- UnreachableCodeException(const char* msg) : AssertionException(msg) {}
-};/* class UnreachableCodeException */
-
-class CVC4_PUBLIC UnhandledCaseException : public UnreachableCodeException {
-public:
- UnhandledCaseException() : UnreachableCodeException() {}
- UnhandledCaseException(std::string msg) : UnreachableCodeException(msg) {}
- UnhandledCaseException(const char* msg) : UnreachableCodeException(msg) {}
-};/* class UnhandledCaseException */
-
-#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(msg...) __CVC4_UNREACHABLEGLUE("Hit a section of unreachable code at " __FILE__ ":", __LINE__, ## msg)
-#define Unhandled(msg...) __CVC4_UNHANDLEDGLUE("Hit an unhandled case at " __FILE__ ":", __LINE__, ## msg)
-
-#define __CVC4_ASSERTGLUE(str1, line, str2, cond, msg...) AssertImpl(str1 #line str2, cond, ## msg)
-#define __CVC4_UNREACHABLEGLUE(str, line, msg...) UnreachableImpl(str #line, ## msg)
-#define __CVC4_UNHANDLEDGLUE(str, line, msg...) UnhandledImpl(str #line, ## msg)
-
-inline void AssertImpl(const char* info, bool cond, std::string msg) {
- if(EXPECT_FALSE( ! cond ))
- throw AssertionException(std::string(info) + "\n" + msg);
-}
-
-inline void AssertImpl(const char* info, bool cond, const char* msg) {
- if(EXPECT_FALSE( ! cond ))
- throw AssertionException(std::string(info) + "\n" + msg);
-}
-
-inline void AssertImpl(const char* info, bool cond) {
- if(EXPECT_FALSE( ! cond ))
- throw 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 UnreachableCodeException(std::string(info) + "\n" + msg);
-}
-
-inline void UnreachableImpl(const char* info, const char* msg) {
- throw UnreachableCodeException(std::string(info) + "\n" + msg);
-}
-
-inline void UnreachableImpl(const char* info) {
- throw UnreachableCodeException(info);
-}
-
-#ifdef __GNUC__
-inline void UnhandledImpl(const char* info, std::string msg) __attribute__ ((noreturn));
-inline void UnhandledImpl(const char* info, const char* msg) __attribute__ ((noreturn));
-inline void UnhandledImpl(const char* info) __attribute__ ((noreturn));
-#endif /* __GNUC__ */
-
-inline void UnhandledImpl(const char* info, std::string msg) {
- throw UnhandledCaseException(std::string(info) + "\n" + msg);
-}
-
-inline void UnhandledImpl(const char* info, const char* msg) {
- throw UnhandledCaseException(std::string(info) + "\n" + msg);
-}
-
-inline void UnhandledImpl(const char* info) {
- throw UnhandledCaseException(info);
-}
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__ASSERT_H */
}
void AssertCommand::invoke(SmtEngine* smt_engine) {
- smt_engine->assert(d_expr);
+ smt_engine->assertFormula(d_expr);
}
CheckSatCommand::CheckSatCommand() {
--- /dev/null
+/********************* -*- 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 */
#ifndef __CVC4__DECISION_ENGINE_H
#define __CVC4__DECISION_ENGINE_H
+#include "cvc4_config.h"
#include "util/literal.h"
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
namespace CVC4 {
-class Literal;
+class Literal {
+};
}/* CVC4 namespace */
--- /dev/null
+/********************* -*- 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 */
#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 */
projects / cvc5.git / commitdiff