diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/Makefile.am | 4 | ||||
-rw-r--r-- | src/theory/arith/Makefile.am | 10 | ||||
-rw-r--r-- | src/theory/arith/kinds | 1 | ||||
-rw-r--r-- | src/theory/bool/Makefile.am | 10 | ||||
-rw-r--r-- | src/theory/bool/kinds | 8 | ||||
-rw-r--r-- | src/theory/interrupted.h | 37 | ||||
-rw-r--r-- | src/theory/output_channel.h | 90 | ||||
-rw-r--r-- | src/theory/theory.cpp | 4 | ||||
-rw-r--r-- | src/theory/theory.h | 31 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 2 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 2 | ||||
-rw-r--r-- | src/theory/uf/Makefile.am | 2 | ||||
-rw-r--r-- | src/theory/uf/kinds | 1 |
13 files changed, 184 insertions, 18 deletions
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 |