diff options
45 files changed, 712 insertions, 273 deletions
diff --git a/Makefile.builds.in b/Makefile.builds.in index f6e17b4ca..0955518bf 100644 --- a/Makefile.builds.in +++ b/Makefile.builds.in @@ -23,8 +23,8 @@ all: 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)" @@ -32,8 +32,8 @@ all: 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) $@) diff --git a/configure.ac b/configure.ac index 8f844f75d..f8e789ab8 100644 --- a/configure.ac +++ b/configure.ac @@ -101,7 +101,7 @@ elif test -e src/include/cvc4_config.h; then 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"; \ diff --git a/contrib/dimacs_to_smt.pl b/contrib/dimacs_to_smt.pl new file mode 100755 index 000000000..305db1d8e --- /dev/null +++ b/contrib/dimacs_to_smt.pl @@ -0,0 +1,36 @@ +#!/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"; diff --git a/src/expr/expr.h b/src/expr/expr.h index a16ffee13..013888baa 100644 --- a/src/expr/expr.h +++ b/src/expr/expr.h @@ -60,19 +60,23 @@ class CVC4_PUBLIC Expr { 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; diff --git a/src/expr/expr_builder.cpp b/src/expr/expr_builder.cpp index be9c60199..4de22f987 100644 --- a/src/expr/expr_builder.cpp +++ b/src/expr/expr_builder.cpp @@ -12,7 +12,8 @@ #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; @@ -159,15 +160,19 @@ ExprBuilder& ExprBuilder::xorExpr(const Expr& right) { // "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) { @@ -178,9 +183,11 @@ void ExprBuilder::addChild(const Expr& e) { 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(); @@ -189,7 +196,9 @@ void ExprBuilder::addChild(const Expr& e) { } 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) { @@ -200,9 +209,11 @@ void ExprBuilder::addChild(ExprValue* ev) { 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; @@ -214,6 +225,7 @@ ExprBuilder& ExprBuilder::collapse() { vector<Expr>* v = new vector<Expr>(); v->reserve(nchild_thresh + 5); // + Unreachable();// unimplemented } return *this; } diff --git a/src/expr/expr_builder.h b/src/expr/expr_builder.h index 5c6019de1..d70acb1fb 100644 --- a/src/expr/expr_builder.h +++ b/src/expr/expr_builder.h @@ -96,7 +96,7 @@ public: // 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 @@ -193,24 +193,47 @@ public: 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); diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp index 3aeab8049..9b7697e4f 100644 --- a/src/expr/expr_manager.cpp +++ b/src/expr/expr_manager.cpp @@ -18,6 +18,42 @@ namespace CVC4 { __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) { @@ -49,4 +85,8 @@ Expr ExprManager::mkExpr(Kind kind, std::vector<Expr> children) { return ExprBuilder(this, kind).append(children); } +Expr ExprManager::mkVar() { + return ExprBuilder(this, VARIABLE); +} + }/* CVC4 namespace */ diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h index ee18ddc01..d311445f3 100644 --- a/src/expr/expr_manager.h +++ b/src/expr/expr_manager.h @@ -32,41 +32,7 @@ class CVC4_PUBLIC ExprManager { 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; } @@ -81,6 +47,9 @@ public: // 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) diff --git a/src/expr/expr_value.cpp b/src/expr/expr_value.cpp index c511c580a..250803281 100644 --- a/src/expr/expr_value.cpp +++ b/src/expr/expr_value.cpp @@ -18,12 +18,12 @@ 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; @@ -82,4 +82,18 @@ ExprValue::const_iterator ExprValue::rend() const { 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 */ diff --git a/src/expr/expr_value.h b/src/expr/expr_value.h index 6df7ad76f..18ad84073 100644 --- a/src/expr/expr_value.h +++ b/src/expr/expr_value.h @@ -21,7 +21,9 @@ #ifndef __CVC4__EXPR__EXPR_VALUE_H #define __CVC4__EXPR__EXPR_VALUE_H +#include "cvc4_config.h" #include <stdint.h> +#include "kind.h" namespace CVC4 { @@ -92,9 +94,7 @@ public: 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 */ diff --git a/src/expr/kind.h b/src/expr/kind.h index 49321b47f..5ac02ca7c 100644 --- a/src/expr/kind.h +++ b/src/expr/kind.h @@ -51,15 +51,16 @@ enum Kind { };/* 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; @@ -88,4 +89,6 @@ inline std::ostream& operator<<(std::ostream& out, const CVC4::Kind& k) { return out; } +}/* CVC4 namespace */ + #endif /* __CVC4__KIND_H */ diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp index 2daead11b..7f515c58b 100644 --- a/src/main/getopt.cpp +++ b/src/main/getopt.cpp @@ -25,6 +25,7 @@ #include "util/exception.h" #include "usage.h" #include "about.h" +#include "util/output.h" using namespace std; using namespace CVC4; @@ -66,7 +67,7 @@ int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(OptionExcepti 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': @@ -104,6 +105,9 @@ int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(OptionExcepti fputs(lang_help, stdout); exit(1); + case 'd': + Debug.on(optarg); + case STATS: opts->statistics = true; break; diff --git a/src/main/main.cpp b/src/main/main.cpp index 4c3a21811..d4ee8fd0d 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -13,6 +13,7 @@ #include <iostream> #include <fstream> #include <cstdlib> +#include <cstring> #include <new> #include "config.h" @@ -22,6 +23,7 @@ #include "expr/expr_manager.h" #include "smt/smt_engine.h" #include "util/command.h" +#include "util/output.h" using namespace std; using namespace CVC4; @@ -44,18 +46,42 @@ int main(int argc, char *argv[]) { 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) { @@ -79,7 +105,7 @@ int main(int argc, char *argv[]) { 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(); diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp index 52f3c4668..04a82f721 100644 --- a/src/parser/antlr_parser.cpp +++ b/src/parser/antlr_parser.cpp @@ -9,12 +9,16 @@ #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"; @@ -63,7 +67,9 @@ AntlrParser::AntlrParser(antlr::TokenStream& lexer, int k) : } 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 { @@ -89,7 +95,7 @@ Expr AntlrParser::newExpression(Kind kind, const std::vector<Expr>& children) { 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!"); } @@ -161,3 +167,6 @@ Expr AntlrParser::createPrecedenceExpr(const std::vector<Expr>& exprs, 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 */ diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h index 0db12a0f0..ad23d45f8 100644 --- a/src/parser/antlr_parser.h +++ b/src/parser/antlr_parser.h @@ -18,7 +18,7 @@ #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 { diff --git a/src/parser/cvc/Makefile.am b/src/parser/cvc/Makefile.am index 4c1a5d92b..b132ede5c 100644 --- a/src/parser/cvc/Makefile.am +++ b/src/parser/cvc/Makefile.am @@ -18,7 +18,9 @@ libparsercvc_la_SOURCES = \ 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 diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 65a5d11c1..4c7e28dc0 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -15,7 +15,7 @@ #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" diff --git a/src/parser/smt/Makefile.am b/src/parser/smt/Makefile.am index 6017409fd..9769fabcb 100644 --- a/src/parser/smt/Makefile.am +++ b/src/parser/smt/Makefile.am @@ -18,7 +18,9 @@ libparsersmt_la_SOURCES = \ 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 diff --git a/src/parser/symbol_table.h b/src/parser/symbol_table.h index 3b08aa5f5..32532c734 100644 --- a/src/parser/symbol_table.h +++ b/src/parser/symbol_table.h @@ -9,6 +9,9 @@ ** **/ +#ifndef __CVC4__PARSER__SYMBOL_TABLE_H +#define __CVC4__PARSER__SYMBOL_TABLE_H + #include <string> #include <stack> #include <ext/hash_map> @@ -31,63 +34,65 @@ namespace parser { * 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 */ diff --git a/src/prop/minisat/core/Solver.C b/src/prop/minisat/core/Solver.C index d7a7bf8e1..4ea33e101 100644 --- a/src/prop/minisat/core/Solver.C +++ b/src/prop/minisat/core/Solver.C @@ -25,7 +25,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA // Constructor/Destructor: namespace CVC4 { -namespace MiniSat { +namespace prop { +namespace minisat { Solver::Solver() : @@ -741,6 +742,7 @@ void Solver::checkLiteralCount() } } -}/* CVC4::MiniSat namespace */ +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ }/* CVC4 namespace */ diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index e53cefc24..2383fd68c 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -17,14 +17,16 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, 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" @@ -33,7 +35,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA // Solver -- the main class: namespace CVC4 { -namespace MiniSat { +namespace prop { +namespace minisat { class Solver { public: @@ -41,7 +44,7 @@ public: // Constructor/Destructor: // Solver(); - ~Solver(); + CVC4_PUBLIC ~Solver(); // Problem specification: // @@ -56,7 +59,7 @@ public: 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. @@ -258,6 +261,7 @@ inline bool Solver::okay () const { return ok; } #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) { @@ -299,8 +303,9 @@ inline void Solver::printClause(const C& c) } } -}/* CVC4::MiniSat namespace */ +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ }/* CVC4 namespace */ //================================================================================================= -#endif /* CVC4_MiniSat_Solver_h */ +#endif /* __CVC4__PROP__MINISAT__SOLVER_H */ diff --git a/src/prop/minisat/core/SolverTypes.h b/src/prop/minisat/core/SolverTypes.h index 55e6d75fd..8860693e6 100644 --- a/src/prop/minisat/core/SolverTypes.h +++ b/src/prop/minisat/core/SolverTypes.h @@ -17,14 +17,15 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, 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: @@ -196,7 +197,8 @@ inline void Clause::strengthen(Lit p) calcAbstraction(); } -}/* CVC4::MiniSat namespace */ +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ }/* CVC4 namespace */ -#endif /* CVC4_MiniSat_SolverTypes_h */ +#endif /* __CVC4__PROP__MINISAT__SOLVERTYPES_H */ diff --git a/src/prop/minisat/mtl/Alg.h b/src/prop/minisat/mtl/Alg.h index a4ca4403b..0fe6d84c7 100644 --- a/src/prop/minisat/mtl/Alg.h +++ b/src/prop/minisat/mtl/Alg.h @@ -20,8 +20,11 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef CVC4_MiniSat_Alg_h #define CVC4_MiniSat_Alg_h +#include <cassert> + namespace CVC4 { -namespace MiniSat { +namespace prop { +namespace minisat { //================================================================================================= // Useful functions on vectors @@ -57,7 +60,8 @@ static inline bool find(V& ts, const T& t) return j < ts.size(); } -}/* CVC4::MiniSat namespace */ +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ }/* CVC4 namespace */ #endif /* CVC4_MiniSat_Alg_h */ diff --git a/src/prop/minisat/mtl/BasicHeap.h b/src/prop/minisat/mtl/BasicHeap.h index b22a35ada..39d825411 100644 --- a/src/prop/minisat/mtl/BasicHeap.h +++ b/src/prop/minisat/mtl/BasicHeap.h @@ -23,7 +23,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "Vec.h" namespace CVC4 { -namespace MiniSat { +namespace prop { +namespace minisat { //================================================================================================= // A heap implementation with support for decrease/increase key. @@ -99,7 +100,8 @@ class BasicHeap { //================================================================================================= -}/* CVC4::MiniSat namespace */ +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ }/* CVC4 namespace */ #endif /* CVC4_MiniSat_BasicHeap_h */ diff --git a/src/prop/minisat/mtl/BoxedVec.h b/src/prop/minisat/mtl/BoxedVec.h index 7c5b10e4c..05b801004 100644 --- a/src/prop/minisat/mtl/BoxedVec.h +++ b/src/prop/minisat/mtl/BoxedVec.h @@ -25,7 +25,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include <new> namespace CVC4 { -namespace MiniSat { +namespace prop { +namespace minisat { //================================================================================================= // Automatically resizable arrays @@ -53,7 +54,7 @@ class bvec { x->cap = size; return x; } - + }; Vec_t* ref; @@ -79,16 +80,16 @@ class bvec { 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: @@ -110,11 +111,11 @@ public: 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 () { @@ -122,10 +123,10 @@ public: 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(); } @@ -146,7 +147,8 @@ public: }; -}/* CVC4::MiniSat namespace */ +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ }/* CVC4 namespace */ #endif /* CVC4_MiniSat_BoxedVec_h */ diff --git a/src/prop/minisat/mtl/Heap.h b/src/prop/minisat/mtl/Heap.h index 84234705c..0c2019b65 100644 --- a/src/prop/minisat/mtl/Heap.h +++ b/src/prop/minisat/mtl/Heap.h @@ -21,9 +21,11 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #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. @@ -95,7 +97,7 @@ class Heap { indices[n] = heap.size(); heap.push(n); - percolateUp(indices[n]); + percolateUp(indices[n]); } @@ -107,19 +109,19 @@ class Heap { 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); } @@ -167,7 +169,8 @@ class Heap { }; -}/* CVC4::MiniSat namespace */ +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ }/* CVC4 namespace */ //================================================================================================= diff --git a/src/prop/minisat/mtl/Map.h b/src/prop/minisat/mtl/Map.h index f69fca6d5..9168dde0e 100644 --- a/src/prop/minisat/mtl/Map.h +++ b/src/prop/minisat/mtl/Map.h @@ -25,7 +25,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "Vec.h" namespace CVC4 { -namespace MiniSat { +namespace prop { +namespace minisat { //================================================================================================= // Default hash/equals functions @@ -83,7 +84,7 @@ class Map { cap = newsize; } - + public: Map () : table(NULL), cap(0), size(0) {} @@ -97,7 +98,7 @@ class Map { for (int i = 0; i < ps.size(); i++) if (equals(ps[i].key, k)){ d = ps[i].data; - return true; } + return true; } return false; } @@ -118,7 +119,8 @@ class Map { } }; -}/* CVC4::MiniSat namespace */ +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ }/* CVC4 namespace */ #endif /* CVC4_MiniSat_Map_h */ diff --git a/src/prop/minisat/mtl/Queue.h b/src/prop/minisat/mtl/Queue.h index e4e7e2159..e02ac7222 100644 --- a/src/prop/minisat/mtl/Queue.h +++ b/src/prop/minisat/mtl/Queue.h @@ -23,7 +23,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "Vec.h" namespace CVC4 { -namespace MiniSat { +namespace prop { +namespace minisat { //================================================================================================= @@ -83,7 +84,8 @@ public: //================================================================================================= -}/* CVC4::MiniSat namespace */ +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ }/* CVC4 namespace */ #endif /* CVC4_MiniSat_Queue_h */ diff --git a/src/prop/minisat/mtl/Sort.h b/src/prop/minisat/mtl/Sort.h index df5261a06..2b9d5bb15 100644 --- a/src/prop/minisat/mtl/Sort.h +++ b/src/prop/minisat/mtl/Sort.h @@ -23,7 +23,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "Vec.h" namespace CVC4 { -namespace MiniSat { +namespace prop { +namespace minisat { //================================================================================================= // Some sorting algorithms for vec's @@ -94,7 +95,8 @@ template <class T> void sort(vec<T>& v) { //================================================================================================= -}/* CVC4::MiniSat namespace */ +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ }/* CVC4 namespace */ #endif /* CVC4_MiniSat_Sort_h */ diff --git a/src/prop/minisat/mtl/Vec.h b/src/prop/minisat/mtl/Vec.h index 1a07cc334..fae1d0c5d 100644 --- a/src/prop/minisat/mtl/Vec.h +++ b/src/prop/minisat/mtl/Vec.h @@ -25,7 +25,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include <new> namespace CVC4 { -namespace MiniSat { +namespace prop { +namespace minisat { //================================================================================================= // Automatically resizable arrays @@ -132,7 +133,8 @@ void vec<T>::clear(bool dealloc) { 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 */ diff --git a/src/prop/minisat/simp/SimpSolver.C b/src/prop/minisat/simp/SimpSolver.C index 14b64b555..063332e74 100644 --- a/src/prop/minisat/simp/SimpSolver.C +++ b/src/prop/minisat/simp/SimpSolver.C @@ -25,7 +25,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA // Constructor/Destructor: namespace CVC4 { -namespace MiniSat { +namespace prop { +namespace minisat { SimpSolver::SimpSolver() : grow (0) @@ -226,11 +227,12 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& ou 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:; @@ -258,11 +260,12 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v) 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:; } @@ -701,5 +704,6 @@ void SimpSolver::toDimacs(const char* file) fprintf(stderr, "could not open file %s\n", file); } -}/* CVC4::MiniSat namespace */ +}/* CVC4::prop::minisat namespace */ +}/* CVC4::prop namespace */ }/* CVC4 namespace */ diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h index 221b4c6e2..f9e9b0387 100644 --- a/src/prop/minisat/simp/SimpSolver.h +++ b/src/prop/minisat/simp/SimpSolver.h @@ -17,23 +17,25 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, 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: // @@ -159,8 +161,9 @@ inline bool SimpSolver::isEliminated (Var v) const { return v < elimtable.size( 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 */ diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index e69de29bb..2fb73cbed 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -0,0 +1,123 @@ +/********************* -*- 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 */ diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 5969e82d1..a3355bf89 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -9,28 +9,38 @@ ** **/ -#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. @@ -39,7 +49,6 @@ public: };/* class PropEngine */ -}/* CVC4::prop namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__PROP__PROP_ENGINE_H */ +#endif /* __CVC4__PROP_ENGINE_H */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 05ee12462..412c0f3af 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -27,11 +27,12 @@ void SmtEngine::processAssertionList() { 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); } @@ -56,7 +57,7 @@ Result SmtEngine::query(Expr e) { return check(); } -Result SmtEngine::assert(Expr e) { +Result SmtEngine::assertFormula(Expr e) { e = preprocess(e); addFormula(e); return quickCheck(); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index ab3fc816a..30786511e 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -20,6 +20,8 @@ #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) @@ -54,6 +56,15 @@ class SmtEngine { /** 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 @@ -90,7 +101,14 @@ public: /* * 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. @@ -103,7 +121,7 @@ public: * 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 diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index fead8e224..d6d8691b2 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -9,11 +9,10 @@ ** **/ -#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. @@ -28,7 +27,6 @@ class TheoryEngine { public: };/* class TheoryEngine */ -}/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__THEORY_ENGINE_H */ +#endif /* __CVC4__THEORY_ENGINE_H */ 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 */ |