Updated contrib/update-copyright to handle Antlr (.g) parser/lexer inputs.
Updated copyright year.
Added a new "bool" theory (right now just to hold a kind.h contribution).
Added "kinds" files to UF and the new "bool" theory.
# .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
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
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';
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";
theory.cpp
libtheory_la_LIBADD = \
+ @builddir@/bool/libbool.la
@builddir@/uf/libuf.la
+ @builddir@/uf/libarith.la
-SUBDIRS = uf
+SUBDIRS = bool uf arith
--- /dev/null
+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
--- /dev/null
+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
--- /dev/null
+FALSE
+TRUE
+NOT
+AND
+IFF
+IMPLIES
+OR
+XOR
--- /dev/null
+/********************* -*- 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 */
--- /dev/null
+/********************* -*- 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 */
** 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
#include "theory/theory.h"
namespace CVC4 {
+namespace theory {
+}/* CVC4::theory namespace */
}/* CVC4 namespace */
** 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
#include "expr/node.h"
#include "util/literal.h"
+#include "theory/output_channel.h"
namespace CVC4 {
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
static bool standardEffortOnly(Effort e) { return e >= STANDARD && e < FULL_EFFORT; }
static bool fullEffort(Effort e) { return e >= FULL_EFFORT; }
+ /**
+ * Construct a theory.
+ */
+ Theory() {
+ }
+
/**
* Prepare for a Node.
*/
/**
* 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 */
** 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
** 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
noinst_LTLIBRARIES = libuf.la
libuf_la_SOURCES =
+
+EXTRA_DIST = kinds
projects / cvc5.git / commitdiff