summaryrefslogtreecommitdiff
path: root/src/expr
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr')
-rw-r--r--src/expr/Makefile.am20
-rw-r--r--src/expr/command.cpp74
-rw-r--r--src/expr/command.h297
-rw-r--r--src/expr/kind.h100
-rw-r--r--src/expr/kind_epilogue.h25
-rw-r--r--src/expr/kind_middle.h33
-rw-r--r--src/expr/kind_prologue.h34
-rwxr-xr-xsrc/expr/mkkind54
8 files changed, 535 insertions, 102 deletions
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index 046281702..3212fc0a0 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -15,11 +15,27 @@ libexpr_la_SOURCES = \
node_manager.h \
expr_manager.h \
node_attribute.h \
- kind.h \
+ @srcdir@/kind.h \
node.cpp \
node_builder.cpp \
node_manager.cpp \
expr_manager.cpp \
node_value.cpp \
- expr.cpp
+ expr.cpp \
+ command.h \
+ command.cpp
+EXTRA_DIST = @srcdir@/kind.h kind_prologue.h kind_middle.h kind_epilogue.h
+
+@srcdir@/kind.h: @srcdir@/mkkind kind_prologue.h kind_middle.h kind_epilogue.h @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds
+ chmod +x @srcdir@/mkkind
+ (@srcdir@/mkkind \
+ @srcdir@/kind_prologue.h \
+ @srcdir@/kind_middle.h \
+ @srcdir@/kind_epilogue.h \
+ `grep '^SUBDIRS = ' @top_srcdir@/src/theory/Makefile.in | cut -d' ' -f3- | tr ' ' "\n" | xargs -i__D__ echo @top_srcdir@/src/theory/__D__/kinds` \
+ > @srcdir@/kind.h) || (rm -f @srcdir@/kind.h && exit 1)
+
+BUILT_SOURCES = @srcdir@/kind.h
+dist-hook: @srcdir@/kind.h
+MAINTAINERCLEANFILES = @srcdir@/kind.h
diff --git a/src/expr/command.cpp b/src/expr/command.cpp
new file mode 100644
index 000000000..2f8dd789e
--- /dev/null
+++ b/src/expr/command.cpp
@@ -0,0 +1,74 @@
+/********************* -*- C++ -*- */
+/** command.cpp
+ ** Original author: mdeters
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 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.
+ **
+ ** Implementation of command objects.
+ **/
+
+#include "expr/command.h"
+#include "smt/smt_engine.h"
+
+using namespace std;
+
+namespace CVC4 {
+
+ostream& operator<<(ostream& out, const Command* c) {
+ if (c == NULL) {
+ out << "null";
+ } else {
+ c->toStream(out);
+ }
+ return out;
+}
+
+CommandSequence::~CommandSequence() {
+ for(unsigned i = d_index; i < d_commandSequence.size(); ++i) {
+ delete d_commandSequence[i];
+ }
+}
+
+void CommandSequence::invoke(SmtEngine* smtEngine) {
+ for(; d_index < d_commandSequence.size(); ++d_index) {
+ d_commandSequence[d_index]->invoke(smtEngine);
+ delete d_commandSequence[d_index];
+ }
+}
+
+void CheckSatCommand::toStream(ostream& out) const {
+ if(d_expr.isNull()) {
+ out << "CheckSat()";
+ } else {
+ out << "CheckSat(" << d_expr << ")";
+ }
+}
+
+void CommandSequence::toStream(ostream& out) const {
+ out << "CommandSequence[" << endl;
+ for(unsigned i = d_index; i < d_commandSequence.size(); ++i) {
+ out << *d_commandSequence[i] << endl;
+ }
+ out << "]";
+}
+
+void DeclarationCommand::toStream(std::ostream& out) const {
+ out << "Declare(";
+ bool first = true;
+ for(unsigned i = 0; i < d_declaredSymbols.size(); ++i) {
+ if(!first) {
+ out << ", ";
+ }
+ out << d_declaredSymbols[i];
+ first = false;
+ }
+ out << ")";
+}
+
+}/* CVC4 namespace */
diff --git a/src/expr/command.h b/src/expr/command.h
new file mode 100644
index 000000000..dedefb782
--- /dev/null
+++ b/src/expr/command.h
@@ -0,0 +1,297 @@
+/********************* -*- C++ -*- */
+/** command.h
+ ** Original author: mdeters
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): cconway
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 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.
+ **
+ ** Implementation of the command pattern on SmtEngines. Command
+ ** objects are generated by the parser (typically) to implement the
+ ** commands in parsed input (see Parser::parseNextCommand()), or by
+ ** client code.
+ **/
+
+#ifndef __CVC4__COMMAND_H
+#define __CVC4__COMMAND_H
+
+#include <iostream>
+#include <sstream>
+#include <string>
+#include <vector>
+
+#include "cvc4_config.h"
+#include "expr/expr.h"
+#include "util/result.h"
+
+namespace CVC4 {
+
+class SmtEngine;
+class Command;
+
+inline std::ostream& operator<<(std::ostream&, const Command&) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream&, const Command*) CVC4_PUBLIC;
+
+class CVC4_PUBLIC Command {
+public:
+ virtual void invoke(CVC4::SmtEngine* smt_engine) = 0;
+ virtual ~Command() {};
+ virtual void toStream(std::ostream&) const = 0;
+ std::string toString() const;
+};/* class Command */
+
+class CVC4_PUBLIC EmptyCommand : public Command {
+public:
+ EmptyCommand(std::string name = "");
+ void invoke(CVC4::SmtEngine* smt_engine);
+ void toStream(std::ostream& out) const;
+private:
+ std::string d_name;
+};/* class EmptyCommand */
+
+class CVC4_PUBLIC AssertCommand : public Command {
+public:
+ AssertCommand(const BoolExpr& e);
+ void invoke(CVC4::SmtEngine* smt_engine);
+ void toStream(std::ostream& out) const;
+protected:
+ BoolExpr d_expr;
+};/* class AssertCommand */
+
+class CVC4_PUBLIC DeclarationCommand : public EmptyCommand {
+public:
+ DeclarationCommand(const std::vector<std::string>& ids);
+ void toStream(std::ostream& out) const;
+protected:
+ std::vector<std::string> d_declaredSymbols;
+};
+
+class CVC4_PUBLIC CheckSatCommand : public Command {
+public:
+ CheckSatCommand(const BoolExpr& e);
+ void invoke(SmtEngine* smt);
+ Result getResult();
+ void toStream(std::ostream& out) const;
+protected:
+ BoolExpr d_expr;
+ Result d_result;
+};/* class CheckSatCommand */
+
+class CVC4_PUBLIC QueryCommand : public Command {
+public:
+ QueryCommand(const BoolExpr& e);
+ void invoke(SmtEngine* smt);
+ Result getResult();
+ void toStream(std::ostream& out) const;
+protected:
+ BoolExpr d_expr;
+ Result d_result;
+};/* class QueryCommand */
+
+class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command {
+public:
+ /** The status an SMT benchmark can have */
+ enum BenchmarkStatus {
+ /** Benchmark is satisfiable */
+ SMT_SATISFIABLE,
+ /** Benchmark is unsatisfiable */
+ SMT_UNSATISFIABLE,
+ /** The status of the benchmark is unknown */
+ SMT_UNKNOWN
+ };
+ SetBenchmarkStatusCommand(BenchmarkStatus status);
+ void invoke(SmtEngine* smt);
+ void toStream(std::ostream& out) const;
+protected:
+ BenchmarkStatus d_status;
+};/* class SetBenchmarkStatusCommand */
+
+inline std::ostream& operator<<(std::ostream& out,
+ SetBenchmarkStatusCommand::BenchmarkStatus bs)
+ CVC4_PUBLIC;
+
+class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command {
+public:
+ SetBenchmarkLogicCommand(std::string logic);
+ void invoke(SmtEngine* smt);
+ void toStream(std::ostream& out) const;
+protected:
+ std::string d_logic;
+};/* class SetBenchmarkLogicCommand */
+
+class CVC4_PUBLIC CommandSequence : public Command {
+public:
+ CommandSequence();
+ ~CommandSequence();
+ void invoke(SmtEngine* smt);
+ void addCommand(Command* cmd);
+ void toStream(std::ostream& out) const;
+
+ typedef std::vector<Command*>::iterator iterator;
+ typedef std::vector<Command*>::const_iterator const_iterator;
+
+ const_iterator begin() const { return d_commandSequence.begin(); }
+ const_iterator end() const { return d_commandSequence.end(); }
+
+ iterator begin() { return d_commandSequence.begin(); }
+ iterator end() { return d_commandSequence.end(); }
+
+private:
+ /** All the commands to be executed (in sequence) */
+ std::vector<Command*> d_commandSequence;
+ /** Next command to be executed */
+ unsigned int d_index;
+};/* class CommandSequence */
+
+}/* CVC4 namespace */
+
+/* =========== inline function definitions =========== */
+
+#include "smt/smt_engine.h"
+
+namespace CVC4 {
+
+inline std::ostream& operator<<(std::ostream& out, const Command& c) {
+ c.toStream(out);
+ return out;
+}
+
+/* class Command */
+
+inline std::string Command::toString() const {
+ std::stringstream ss;
+ toStream(ss);
+ return ss.str();
+}
+
+/* class EmptyCommand */
+
+inline EmptyCommand::EmptyCommand(std::string name) :
+ d_name(name) {
+}
+
+inline void EmptyCommand::invoke(SmtEngine* smt_engine) {
+}
+
+inline void EmptyCommand::toStream(std::ostream& out) const {
+ out << "EmptyCommand(" << d_name << ")";
+}
+
+/* class AssertCommand */
+
+inline AssertCommand::AssertCommand(const BoolExpr& e) :
+ d_expr(e) {
+}
+
+inline void AssertCommand::invoke(SmtEngine* smt_engine) {
+ smt_engine->assertFormula(d_expr);
+}
+
+inline void AssertCommand::toStream(std::ostream& out) const {
+ out << "Assert(" << d_expr << ")";
+}
+
+/* class CheckSatCommand */
+
+inline CheckSatCommand::CheckSatCommand(const BoolExpr& e) :
+ d_expr(e) {
+}
+
+inline void CheckSatCommand::invoke(SmtEngine* smt_engine) {
+ d_result = smt_engine->checkSat(d_expr);
+}
+
+inline Result CheckSatCommand::getResult() {
+ return d_result;
+}
+
+/* class QueryCommand */
+
+inline QueryCommand::QueryCommand(const BoolExpr& e) :
+ d_expr(e) {
+}
+
+inline void QueryCommand::invoke(CVC4::SmtEngine* smt_engine) {
+ d_result = smt_engine->query(d_expr);
+}
+
+inline Result QueryCommand::getResult() {
+ return d_result;
+}
+
+inline void QueryCommand::toStream(std::ostream& out) const {
+ out << "Query(";
+ d_expr.printAst(out, 0);
+ out << ")";
+}
+
+/* class CommandSequence */
+
+inline CommandSequence::CommandSequence() :
+ d_index(0) {
+}
+
+inline void CommandSequence::addCommand(Command* cmd) {
+ d_commandSequence.push_back(cmd);
+}
+
+/* class DeclarationCommand */
+
+inline DeclarationCommand::DeclarationCommand(const std::vector<std::string>& ids) :
+ d_declaredSymbols(ids) {
+}
+
+/* class SetBenchmarkStatusCommand */
+
+inline SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus s) :
+ d_status(s) {
+}
+
+inline void SetBenchmarkStatusCommand::invoke(SmtEngine* smt) {
+ // FIXME: TODO: something to be done with the status
+}
+
+inline void SetBenchmarkStatusCommand::toStream(std::ostream& out) const {
+ out << "SetBenchmarkStatus(" << d_status << ")";
+}
+
+/* class SetBenchmarkLogicCommand */
+
+inline SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string l) :
+ d_logic(l) {
+}
+
+inline void SetBenchmarkLogicCommand::invoke(SmtEngine* smt) {
+ // FIXME: TODO: something to be done with the logic
+}
+
+inline void SetBenchmarkLogicCommand::toStream(std::ostream& out) const {
+ out << "SetBenchmarkLogic(" << d_logic << ")";
+}
+
+/* output stream insertion operator for benchmark statuses */
+inline std::ostream& operator<<(std::ostream& out,
+ SetBenchmarkStatusCommand::BenchmarkStatus bs) {
+ switch(bs) {
+
+ case SetBenchmarkStatusCommand::SMT_SATISFIABLE:
+ return out << "sat";
+
+ case SetBenchmarkStatusCommand::SMT_UNSATISFIABLE:
+ return out << "unsat";
+
+ case SetBenchmarkStatusCommand::SMT_UNKNOWN:
+ return out << "unknown";
+
+ default:
+ return out << "SetBenchmarkStatusCommand::[UNKNOWNSTATUS!]";
+ }
+}
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__COMMAND_H */
diff --git a/src/expr/kind.h b/src/expr/kind.h
deleted file mode 100644
index 575a4790c..000000000
--- a/src/expr/kind.h
+++ /dev/null
@@ -1,100 +0,0 @@
-/********************* -*- C++ -*- */
-/** kind.h
- ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): cconway, dejan
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 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.
- **
- ** Kinds of Nodes.
- **/
-
-#ifndef __CVC4__KIND_H
-#define __CVC4__KIND_H
-
-#include "cvc4_config.h"
-#include <iostream>
-
-namespace CVC4 {
-
-// TODO: create this file (?) from theory solver headers so that we
-// have a collection of kinds from all. This file is mainly a
-// placeholder for design & development work.
-
-enum Kind {
- /* undefined */
- UNDEFINED_KIND = -1,
- /** Null Kind */
- NULL_EXPR,
-
- /* built-ins */
- EQUAL,
- ITE,
- SKOLEM,
- VARIABLE,
- APPLY,
-
- /* propositional connectives */
- FALSE,
- TRUE,
-
- NOT,
-
- AND,
- IFF,
- IMPLIES,
- OR,
- XOR,
-
- /* from arith */
- PLUS,
- MINUS,
- MULT
-};/* enum Kind */
-
-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;
- case VARIABLE: out << "VARIABLE"; break;
- case APPLY: out << "APPLY"; break;
-
- /* propositional connectives */
- case FALSE: out << "FALSE"; break;
- case TRUE: out << "TRUE"; break;
-
- case NOT: out << "NOT"; break;
-
- case AND: out << "AND"; break;
- case IFF: out << "IFF"; break;
- case IMPLIES: out << "IMPLIES"; break;
- case OR: out << "OR"; break;
- case XOR: out << "XOR"; break;
-
- /* from arith */
- case PLUS: out << "PLUS"; break;
- case MINUS: out << "MINUS"; break;
- case MULT: out << "MULT"; break;
-
- default: out << "UNKNOWNKIND!" << int(k); break;
- }
-
- return out;
-}
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__KIND_H */
diff --git a/src/expr/kind_epilogue.h b/src/expr/kind_epilogue.h
new file mode 100644
index 000000000..0db7038d8
--- /dev/null
+++ b/src/expr/kind_epilogue.h
@@ -0,0 +1,25 @@
+/********************* -*- C++ -*- */
+/** kind_epilogue.h
+ ** Original author:
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 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.
+ **
+ ** Kinds of Nodes.
+ **/
+
+ case LAST_KIND: out << "LAST_KIND"; break;
+ default: out << "UNKNOWNKIND!" << int(k); break;
+ }
+
+ return out;
+}
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__KIND_H */
diff --git a/src/expr/kind_middle.h b/src/expr/kind_middle.h
new file mode 100644
index 000000000..6c352c3c9
--- /dev/null
+++ b/src/expr/kind_middle.h
@@ -0,0 +1,33 @@
+/********************* -*- C++ -*- */
+/** kind_middle.h
+ ** Original author:
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 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.
+ **
+ ** Kinds of Nodes.
+ **/
+
+ LAST_KIND
+
+};/* enum Kind */
+
+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;
+ case VARIABLE: out << "VARIABLE"; break;
diff --git a/src/expr/kind_prologue.h b/src/expr/kind_prologue.h
new file mode 100644
index 000000000..cf9d2e3be
--- /dev/null
+++ b/src/expr/kind_prologue.h
@@ -0,0 +1,34 @@
+/********************* -*- C++ -*- */
+/** kind_prologue.h
+ ** Original author:
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 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.
+ **
+ ** Kinds of Nodes.
+ **/
+
+#ifndef __CVC4__KIND_H
+#define __CVC4__KIND_H
+
+#include "cvc4_config.h"
+#include <iostream>
+
+namespace CVC4 {
+
+enum Kind {
+ /* undefined */
+ UNDEFINED_KIND = -1,
+ /** Null Kind */
+ NULL_EXPR,
+
+ /* built-ins */
+ EQUAL,
+ ITE,
+ SKOLEM,
+ VARIABLE,
diff --git a/src/expr/mkkind b/src/expr/mkkind
new file mode 100755
index 000000000..c8ad61571
--- /dev/null
+++ b/src/expr/mkkind
@@ -0,0 +1,54 @@
+#!/bin/bash
+#
+# mkkind
+# Morgan Deters <mdeters@cs.nyu.edu> for CVC4
+#
+# The purpose of this script is to create kind.h from a prologue,
+# middle, epilogue, and a list of theory kinds.
+#
+# Invocation:
+#
+# mkkind prologue-file middle-file epilogue-file theory-kind-files...
+#
+# Output is to standard out.
+#
+
+cat <<EOF
+/********************* -*- C++ -*- */
+/** kind.h
+ **
+ ** Copyright 2009, 2010 The AcSys Group, New York University, and as below.
+ **
+ ** This header file automatically generated by:
+ **
+ ** $0 $@
+ **
+ ** for the CVC4 project.
+ **
+ **/
+
+EOF
+
+prologue=$1; shift
+middle=$1; shift
+epilogue=$1; shift
+
+cases=
+cat "$prologue"
+while [ $# -gt 0 ]; do
+ b=$(basename $(dirname "$1"))
+ echo
+ echo " /* from $b */"
+ cases="$cases
+ /* from $b */
+"
+ for r in `cat "$1"`; do
+ echo " $r,"
+ cases="$cases case $r: out << \"$r\"; break;
+"
+ done
+ shift
+done
+cat "$middle"
+echo "$cases"
+cat "$epilogue"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback