summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rwxr-xr-xcontrib/update-copyright.pl21
-rw-r--r--src/theory/Makefile.am4
-rw-r--r--src/theory/arith/Makefile.am10
-rw-r--r--src/theory/arith/kinds1
-rw-r--r--src/theory/bool/Makefile.am10
-rw-r--r--src/theory/bool/kinds8
-rw-r--r--src/theory/interrupted.h37
-rw-r--r--src/theory/output_channel.h90
-rw-r--r--src/theory/theory.cpp4
-rw-r--r--src/theory/theory.h31
-rw-r--r--src/theory/theory_engine.cpp2
-rw-r--r--src/theory/theory_engine.h2
-rw-r--r--src/theory/uf/Makefile.am2
-rw-r--r--src/theory/uf/kinds1
14 files changed, 197 insertions, 26 deletions
diff --git a/contrib/update-copyright.pl b/contrib/update-copyright.pl
index 1548e3fa6..948e276d1 100755
--- a/contrib/update-copyright.pl
+++ b/contrib/update-copyright.pl
@@ -19,22 +19,22 @@
# .deps, etc.)
#
# It ignores any file not ending with one of:
-# .c .cc .cpp .C .h .hh .hpp .H .y .yy .ypp .Y .l .ll .lpp .L
+# .c .cc .cpp .C .h .hh .hpp .H .y .yy .ypp .Y .l .ll .lpp .L .g
# (so, this includes emacs ~-backups, CVS detritus, etc.)
#
# It ignores any directory matching $excluded_directories
# (so, you should add here any sources imported but not covered under
# the license.)
-my $excluded_directories = '^(minisat|CVS)$';
+my $excluded_directories = '^(minisat|CVS|generated)$';
# Years of copyright for the template. E.g., the string
# "1985, 1987, 1992, 1997, 2008" or "2006-2009" or whatever.
-my $years = '2009';
+my $years = '2009, 2010';
my $standard_template = <<EOF;
** This file is part of the CVC4 prototype.
- ** Copyright (c) $years The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) $years 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
@@ -43,7 +43,7 @@ EOF
my $public_template = <<EOF;
** This file is part of the CVC4 prototype.
- ** Copyright (c) $years The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) $years 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
@@ -102,7 +102,7 @@ sub recurse {
next if $file =~ /$excluded_directories/;
recurse($srcdir.'/'.$file);
} else {
- next if !($file =~ /\.(c|cc|cpp|C|h|hh|hpp|H|y|yy|ypp|Y|l|ll|lpp|L)$/);
+ next if !($file =~ /\.(c|cc|cpp|C|h|hh|hpp|H|y|yy|ypp|Y|l|ll|lpp|L|g)$/);
print "$srcdir/$file...";
my $infile = $srcdir.'/'.$file;
my $outfile = $srcdir.'/#'.$file.'.tmp';
@@ -114,14 +114,19 @@ sub recurse {
my $minor_contributors = <$AUTHOR>; chomp $minor_contributors;
close $AUTHOR;
$_ = <$IN>;
- if(m,^(%{)?/\*\*\*\*\*,) {
+ if(m,^(%{)?/\*(\*| )\*\*\*,) {
print "updating\n";
if($file =~ /\.(y|yy|ypp|Y)$/) {
print $OUT "%{/******************* -*- C++ -*- */\n";
+ print $OUT "/** $file\n";
+ } elsif($file =~ /\.g$/) {
+ # avoid javadoc-style comment here; antlr complains
+ print $OUT "/* ******************* -*- C++ -*- */\n";
+ print $OUT "/* $file\n";
} else {
print $OUT "/********************* -*- C++ -*- */\n";
+ print $OUT "/** $file\n";
}
- print $OUT "/** $file\n";
print $OUT " ** Original author: $author\n";
print $OUT " ** Major contributors: $major_contributors\n";
print $OUT " ** Minor contributors (to current version): $minor_contributors\n";
diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am
index 4eba7811c..f6f4ae07e 100644
--- a/src/theory/Makefile.am
+++ b/src/theory/Makefile.am
@@ -12,6 +12,8 @@ libtheory_la_SOURCES = \
theory.cpp
libtheory_la_LIBADD = \
+ @builddir@/bool/libbool.la
@builddir@/uf/libuf.la
+ @builddir@/uf/libarith.la
-SUBDIRS = uf
+SUBDIRS = bool uf arith
diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am
new file mode 100644
index 000000000..461659765
--- /dev/null
+++ b/src/theory/arith/Makefile.am
@@ -0,0 +1,10 @@
+AM_CPPFLAGS = \
+ -D__BUILDING_CVC4LIB \
+ -I@srcdir@/../../include -I@srcdir@/../..
+AM_CXXFLAGS = -Wall -fvisibility=hidden
+
+noinst_LTLIBRARIES = libarith.la
+
+libarith_la_SOURCES =
+
+EXTRA_DIST = kinds
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
new file mode 100644
index 000000000..994416838
--- /dev/null
+++ b/src/theory/arith/kinds
@@ -0,0 +1 @@
+PLUS
diff --git a/src/theory/bool/Makefile.am b/src/theory/bool/Makefile.am
new file mode 100644
index 000000000..9c8b8365e
--- /dev/null
+++ b/src/theory/bool/Makefile.am
@@ -0,0 +1,10 @@
+AM_CPPFLAGS = \
+ -D__BUILDING_CVC4LIB \
+ -I@srcdir@/../../include -I@srcdir@/../..
+AM_CXXFLAGS = -Wall -fvisibility=hidden
+
+noinst_LTLIBRARIES = libbool.la
+
+libbool_la_SOURCES =
+
+EXTRA_DIST = kinds
diff --git a/src/theory/bool/kinds b/src/theory/bool/kinds
new file mode 100644
index 000000000..7f1267383
--- /dev/null
+++ b/src/theory/bool/kinds
@@ -0,0 +1,8 @@
+FALSE
+TRUE
+NOT
+AND
+IFF
+IMPLIES
+OR
+XOR
diff --git a/src/theory/interrupted.h b/src/theory/interrupted.h
new file mode 100644
index 000000000..03bf466c9
--- /dev/null
+++ b/src/theory/interrupted.h
@@ -0,0 +1,37 @@
+/********************* -*- C++ -*- */
+/** interrupted.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.
+ **
+ ** The theory output channel interface.
+ **/
+
+#ifndef __CVC4__THEORY__INTERRUPTED_H
+#define __CVC4__THEORY__INTERRUPTED_H
+
+#include "util/exception.h"
+
+namespace CVC4 {
+namespace theory {
+
+class CVC4_PUBLIC Interrupted : public CVC4::Exception {
+public:
+
+ // Constructors
+ Interrupted() : CVC4::Exception("CVC4::Theory::Interrupted") {}
+ Interrupted(const std::string& msg) : CVC4::Exception(msg) {}
+ Interrupted(const char* msg) : CVC4::Exception(msg) {}
+
+};/* class Interrupted */
+
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__INTERRUPTED_H */
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
new file mode 100644
index 000000000..42e68b7a9
--- /dev/null
+++ b/src/theory/output_channel.h
@@ -0,0 +1,90 @@
+/********************* -*- C++ -*- */
+/** output_channel.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.
+ **
+ ** The theory output channel interface.
+ **/
+
+#ifndef __CVC4__THEORY__OUTPUT_CHANNEL_H
+#define __CVC4__THEORY__OUTPUT_CHANNEL_H
+
+#include "theory/interrupted.h"
+
+namespace CVC4 {
+namespace theory {
+
+/**
+ * Generic "theory output channel" interface.
+ */
+class OutputChannel {
+public:
+
+ /**
+ * With safePoint(), the theory signals that it is at a safe point
+ * and can be interrupted.
+ */
+ virtual void safePoint() throw(Interrupted&) {
+ }
+
+ /**
+ * Indicate a theory conflict has arisen.
+ *
+ * @param n - a conflict at the current decision level
+ * @param safe - whether it is safe to be interrupted
+ */
+ virtual void conflict(Node n, bool safe = false) throw(Interrupted&) = 0;
+
+ /**
+ * Propagate a theory literal.
+ *
+ * @param n - a theory consequence at the current decision level
+ * @param safe - whether it is safe to be interrupted
+ */
+ virtual void propagate(Node n, bool safe = false) throw(Interrupted&) = 0;
+
+ /**
+ * Tell the core that a valid theory lemma at decision level 0 has
+ * been detected. (This request a split.)
+ *
+ * @param n - a theory lemma valid at decision level 0
+ * @param safe - whether it is safe to be interrupted
+ */
+ virtual void lemma(Node n, bool safe = false) throw(Interrupted&) = 0;
+
+};/* class OutputChannel */
+
+/**
+ * Generic "theory output channel" interface for explanations.
+ */
+class ExplainOutputChannel {
+public:
+
+ /**
+ * With safePoint(), the theory signals that it is at a safe point
+ * and can be interrupted. The default implementation never
+ * interrupts.
+ */
+ virtual void safePoint() throw(Interrupted&) {
+ }
+
+ /**
+ * Provide an explanation in response to an explanation request.
+ *
+ * @param n - an explanation
+ * @param safe - whether it is safe to be interrupted
+ */
+ virtual void explanation(Node n, bool safe = false) throw(Interrupted&) = 0;
+};/* class ExplainOutputChannel */
+
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__OUTPUT_CHANNEL_H */
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index c4b2b8d83..2972b4722 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -4,7 +4,7 @@
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
+ ** 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
@@ -16,5 +16,7 @@
#include "theory/theory.h"
namespace CVC4 {
+namespace theory {
+}/* CVC4::theory namespace */
}/* CVC4 namespace */
diff --git a/src/theory/theory.h b/src/theory/theory.h
index f0db8a7ae..dc862197e 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -4,7 +4,7 @@
** Major contributors: none
** Minor contributors (to current version): dejan
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
+ ** 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
@@ -18,6 +18,7 @@
#include "expr/node.h"
#include "util/literal.h"
+#include "theory/output_channel.h"
namespace CVC4 {
namespace theory {
@@ -26,12 +27,14 @@ namespace theory {
* Base class for T-solvers. Abstract DPLL(T).
*/
class Theory {
+
/**
* Return whether a node is shared or not. Used by setup().
*/
bool isShared(Node);
public:
+
/**
* Subclasses of Theory may add additional efforts. DO NOT CHECK
* equality with one of these values (e.g. if STANDARD xxx) but
@@ -55,6 +58,12 @@ public:
static bool fullEffort(Effort e) { return e >= FULL_EFFORT; }
/**
+ * Construct a theory.
+ */
+ Theory() {
+ }
+
+ /**
* Prepare for a Node.
*/
virtual void setup(Node) = 0;
@@ -62,30 +71,24 @@ public:
/**
* Assert a literal in the current context.
*/
- void assert(Literal);
+ void assertLiteral(Literal);
/**
* Check the current assignment's consistency.
*/
- virtual void check(Effort level = FULL_EFFORT) = 0;
+ virtual void check(OutputChannel& out, Effort level = FULL_EFFORT) = 0;
/**
* T-propagate new literal assignments in the current context.
*/
- // TODO design decision: instead of returning a set of literals
- // here, perhaps we have an interface back into the prop engine
- // where we assert directly. we might sometimes unknowingly assert
- // something clearly inconsistent (esp. in a parallel context).
- // This would allow the PropEngine to cancel our further work since
- // we're already inconsistent---also could strategize dynamically on
- // whether enough theory prop work has occurred.
- virtual void propagate(Effort level = FULL_EFFORT) = 0;
+ virtual void propagate(OutputChannel& out, Effort level = FULL_EFFORT) = 0;
/**
- * Return an explanation for the literal (which was previously
- * propagated by this theory)..
+ * Return an explanation for the literal represented by parameter n
+ * (which was previously propagated by this theory). Report
+ * explanations to an output channel.
*/
- virtual Node explain(Literal) = 0;
+ virtual void explain(OutputChannel& out, Node n, Effort level = FULL_EFFORT) = 0;
};/* class Theory */
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 2289f2fea..81bb38e68 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -4,7 +4,7 @@
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
+ ** 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
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 65a317433..b4a9f8f91 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -4,7 +4,7 @@
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
+ ** 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
diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am
index 4b36d2fe8..7895803a6 100644
--- a/src/theory/uf/Makefile.am
+++ b/src/theory/uf/Makefile.am
@@ -6,3 +6,5 @@ AM_CXXFLAGS = -Wall -fvisibility=hidden
noinst_LTLIBRARIES = libuf.la
libuf_la_SOURCES =
+
+EXTRA_DIST = kinds
diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds
new file mode 100644
index 000000000..5106136bc
--- /dev/null
+++ b/src/theory/uf/kinds
@@ -0,0 +1 @@
+APPLY
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback