From 92a04e03876154a946b729855a72e1e871304fe5 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 4 Feb 2010 02:46:17 +0000 Subject: [PATCH] Added theory output channel interfaces and "Interrupted" exception. 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. --- contrib/update-copyright.pl | 21 +++++---- src/theory/Makefile.am | 4 +- src/theory/arith/Makefile.am | 10 ++++ src/theory/arith/kinds | 1 + src/theory/bool/Makefile.am | 10 ++++ src/theory/bool/kinds | 8 ++++ src/theory/interrupted.h | 37 +++++++++++++++ src/theory/output_channel.h | 90 ++++++++++++++++++++++++++++++++++++ src/theory/theory.cpp | 4 +- src/theory/theory.h | 31 +++++++------ src/theory/theory_engine.cpp | 2 +- src/theory/theory_engine.h | 2 +- src/theory/uf/Makefile.am | 2 + src/theory/uf/kinds | 1 + 14 files changed, 197 insertions(+), 26 deletions(-) create mode 100644 src/theory/arith/Makefile.am create mode 100644 src/theory/arith/kinds create mode 100644 src/theory/bool/Makefile.am create mode 100644 src/theory/bool/kinds create mode 100644 src/theory/interrupted.h create mode 100644 src/theory/output_channel.h create mode 100644 src/theory/uf/kinds 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 = <; 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 @@ -54,6 +57,12 @@ public: 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. */ @@ -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 -- 2.30.2