diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/Makefile.am | 28 | ||||
-rw-r--r-- | src/theory/arith/Makefile | 4 | ||||
-rw-r--r-- | src/theory/arith/Makefile.am | 4 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.h | 23 | ||||
-rw-r--r-- | src/theory/arith/theory_def.h | 9 | ||||
-rw-r--r-- | src/theory/booleans/Makefile | 4 | ||||
-rw-r--r-- | src/theory/booleans/Makefile.am (renamed from src/theory/bool/Makefile.am) | 6 | ||||
-rw-r--r-- | src/theory/booleans/kinds (renamed from src/theory/bool/kinds) | 0 | ||||
-rw-r--r-- | src/theory/booleans/theory_bool.h | 24 | ||||
-rw-r--r-- | src/theory/booleans/theory_def.h | 9 | ||||
-rwxr-xr-x | src/theory/mktheoryof | 57 | ||||
-rw-r--r-- | src/theory/output_channel.h | 57 | ||||
-rw-r--r-- | src/theory/theory.cpp | 20 | ||||
-rw-r--r-- | src/theory/theory.h | 274 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 53 | ||||
-rw-r--r-- | src/theory/theoryof_table_epilogue.h | 21 | ||||
-rw-r--r-- | src/theory/theoryof_table_middle.h | 35 | ||||
-rw-r--r-- | src/theory/theoryof_table_prologue.h | 21 | ||||
-rw-r--r-- | src/theory/uf/Makefile.am | 1 | ||||
-rw-r--r-- | src/theory/uf/theory_def.h | 7 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 22 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.h | 15 |
22 files changed, 590 insertions, 104 deletions
diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index f6f4ae07e..951dbeb78 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -6,14 +6,34 @@ AM_CXXFLAGS = -Wall -fvisibility=hidden noinst_LTLIBRARIES = libtheory.la libtheory_la_SOURCES = \ + @srcdir@/theoryof_table.h \ theory_engine.h \ theory_engine.cpp \ theory.h \ theory.cpp libtheory_la_LIBADD = \ - @builddir@/bool/libbool.la - @builddir@/uf/libuf.la - @builddir@/uf/libarith.la + @builddir@/booleans/libbooleans.la \ + @builddir@/uf/libuf.la \ + @builddir@/arith/libarith.la -SUBDIRS = bool uf arith +EXTRA_DIST = \ + @srcdir@/theoryof_table.h \ + theoryof_table_prologue.h \ + theoryof_table_middle.h \ + theoryof_table_epilogue.h + +@srcdir@/theoryof_table.h: @srcdir@/mktheoryof theoryof_table_prologue.h theoryof_table_middle.h theoryof_table_epilogue.h @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds + chmod +x @srcdir@/mktheoryof + (@srcdir@/mktheoryof \ + @srcdir@/theoryof_table_prologue.h \ + @srcdir@/theoryof_table_middle.h \ + @srcdir@/theoryof_table_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@/theoryof_table.h) || (rm -f @srcdir@/theoryof_table.h && exit 1) + +BUILT_SOURCES = @srcdir@/theoryof_table.h +dist-hook: @srcdir@/theoryof_table.h +MAINTAINERCLEANFILES = @srcdir@/theoryof_table.h + +SUBDIRS = booleans uf arith diff --git a/src/theory/arith/Makefile b/src/theory/arith/Makefile new file mode 100644 index 000000000..5016522e8 --- /dev/null +++ b/src/theory/arith/Makefile @@ -0,0 +1,4 @@ +topdir = ../../.. +srcdir = src/theory/arith + +include $(topdir)/Makefile.subdir diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am index 461659765..226d5af12 100644 --- a/src/theory/arith/Makefile.am +++ b/src/theory/arith/Makefile.am @@ -5,6 +5,8 @@ AM_CXXFLAGS = -Wall -fvisibility=hidden noinst_LTLIBRARIES = libarith.la -libarith_la_SOURCES = +libarith_la_SOURCES = \ + theory_def.h \ + theory_arith.h EXTRA_DIST = kinds diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h new file mode 100644 index 000000000..5b596afd4 --- /dev/null +++ b/src/theory/arith/theory_arith.h @@ -0,0 +1,23 @@ +#include "theory/theory.h" + +namespace CVC4 { +namespace theory { +namespace arith { + +class TheoryArith : public TheoryImpl<TheoryArith> { +public: + TheoryArith(context::Context* c, OutputChannel& out) : + TheoryImpl<TheoryArith>(c, out) { + } + + void preRegisterTerm(TNode n) { Unimplemented(); } + void registerTerm(TNode n) { Unimplemented(); } + void check(Effort e) { Unimplemented(); } + void propagate(Effort e) { Unimplemented(); } + void explain(TNode n, Effort e) { Unimplemented(); } +}; + +} +} +} + diff --git a/src/theory/arith/theory_def.h b/src/theory/arith/theory_def.h new file mode 100644 index 000000000..9b01a458e --- /dev/null +++ b/src/theory/arith/theory_def.h @@ -0,0 +1,9 @@ +#include "theory/arith/theory_arith.h" + +namespace CVC4 { + namespace theory { + namespace arith { + typedef TheoryArith TheoryARITH; + } + } +} diff --git a/src/theory/booleans/Makefile b/src/theory/booleans/Makefile new file mode 100644 index 000000000..a74a72d83 --- /dev/null +++ b/src/theory/booleans/Makefile @@ -0,0 +1,4 @@ +topdir = ../../.. +srcdir = src/theory/bool + +include $(topdir)/Makefile.subdir diff --git a/src/theory/bool/Makefile.am b/src/theory/booleans/Makefile.am index 9c8b8365e..cbdf13add 100644 --- a/src/theory/bool/Makefile.am +++ b/src/theory/booleans/Makefile.am @@ -3,8 +3,10 @@ AM_CPPFLAGS = \ -I@srcdir@/../../include -I@srcdir@/../.. AM_CXXFLAGS = -Wall -fvisibility=hidden -noinst_LTLIBRARIES = libbool.la +noinst_LTLIBRARIES = libbooleans.la -libbool_la_SOURCES = +libbooleans_la_SOURCES = \ + theory_def.h \ + theory_bool.h EXTRA_DIST = kinds diff --git a/src/theory/bool/kinds b/src/theory/booleans/kinds index 7f1267383..7f1267383 100644 --- a/src/theory/bool/kinds +++ b/src/theory/booleans/kinds diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h new file mode 100644 index 000000000..26e5a69fb --- /dev/null +++ b/src/theory/booleans/theory_bool.h @@ -0,0 +1,24 @@ +#include "theory/theory.h" +#include "context/context.h" + +namespace CVC4 { +namespace theory { +namespace booleans { + +class TheoryBool : public TheoryImpl<TheoryBool> { +public: + TheoryBool(context::Context* c, OutputChannel& out) : + TheoryImpl<TheoryBool>(c, out) { + } + + void preRegisterTerm(TNode n) { Unimplemented(); } + void registerTerm(TNode n) { Unimplemented(); } + void check(Effort e) { Unimplemented(); } + void propagate(Effort e) { Unimplemented(); } + void explain(TNode n, Effort e) { Unimplemented(); } +}; + +} +} +} + diff --git a/src/theory/booleans/theory_def.h b/src/theory/booleans/theory_def.h new file mode 100644 index 000000000..37aacb353 --- /dev/null +++ b/src/theory/booleans/theory_def.h @@ -0,0 +1,9 @@ +#include "theory/booleans/theory_bool.h" + +namespace CVC4 { + namespace theory { + namespace booleans { + typedef TheoryBool TheoryBOOLEANS; + } + } +} diff --git a/src/theory/mktheoryof b/src/theory/mktheoryof new file mode 100755 index 000000000..38c2153d6 --- /dev/null +++ b/src/theory/mktheoryof @@ -0,0 +1,57 @@ +#!/bin/bash +# +# mktheoryof +# Morgan Deters <mdeters@cs.nyu.edu> for CVC4 +# Copyright (c) 2010 The CVC4 Project +# +# The purpose of this script is to create theoryof_table.h from a +# prologue, epilogue, and a list of theory kinds. +# +# Invocation: +# +# mktheoryof prologue-file epilogue-file theory-kind-files... +# +# Output is to standard out. +# + +cat <<EOF +/********************* -*- C++ -*- */ +/** theoryof_table.h + ** + ** Copyright 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 + +registers= +cat "$prologue" +while [ $# -gt 0 ]; do + b=$(basename $(dirname "$1")) + B=$(echo "$b" | tr 'a-z' 'A-Z') + echo "#include \"theory/$b/theory_def.h\"" + registers="$registers + /* from $b */ + void registerTheory(::CVC4::theory::$b::Theory$B* th) { +" + for r in `cat "$1"`; do + registers="$registers d_table[::CVC4::kind::$r] = th; +" + done + registers="$registers } +" + shift +done +echo +cat "$middle" +echo "$registers" +cat "$epilogue" diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index c530434f5..ad558e115 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -25,9 +25,21 @@ namespace theory { * Generic "theory output channel" interface. */ class OutputChannel { + /** Disallow copying: private constructor */ + OutputChannel(const OutputChannel&); + + /** Disallow assignment: private operator=() */ + OutputChannel& operator=(const OutputChannel&); + public: /** + * Construct an OutputChannel. + */ + OutputChannel() { + } + + /** * Destructs an OutputChannel. This implementation does nothing, * but we need a virtual destructor for safety in case subclasses * have a destructor. @@ -39,24 +51,28 @@ public: * With safePoint(), the theory signals that it is at a safe point * and can be interrupted. */ - virtual void safePoint() throw(Interrupted&) { + virtual void safePoint() throw(Interrupted) { } /** * Indicate a theory conflict has arisen. * - * @param n - a conflict at the current decision level + * @param n - a conflict at the current decision level. This should + * be an OR-kinded node of literals that are false in the current + * assignment. + * * @param safe - whether it is safe to be interrupted */ - virtual void conflict(Node n, bool safe = false) throw(Interrupted&) = 0; + virtual void conflict(TNode n, bool safe = false) throw(Interrupted) = 0; /** * Propagate a theory literal. * - * @param n - a theory consequence at the current decision level + * @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; + virtual void propagate(TNode n, bool safe = false) throw(Interrupted) = 0; /** * Tell the core that a valid theory lemma at decision level 0 has @@ -65,31 +81,7 @@ public: * @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: - - /** - * Destructs an ExplainOutputChannel. This implementation does - * nothing, but we need a virtual destructor for safety in case - * subclasses have a destructor. - */ - virtual ~ExplainOutputChannel() { - } - - /** - * 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&) { - } + virtual void lemma(TNode n, bool safe = false) throw(Interrupted) = 0; /** * Provide an explanation in response to an explanation request. @@ -97,8 +89,9 @@ public: * @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 */ + virtual void explanation(TNode n, bool safe = false) throw(Interrupted) = 0; + +};/* class OutputChannel */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index cf52de75e..17a35f2ed 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -14,24 +14,14 @@ **/ #include "theory/theory.h" +#include "util/Assert.h" -namespace CVC4 { -namespace theory { - -bool Theory::done() { - return d_nextAssertion >= d_assertions.size(); -} +#include <vector> +using namespace std; -Node Theory::get() { - Node n = d_assertions[d_nextAssertion]; - d_nextAssertion = d_nextAssertion + 1; - return n; -} - -void Theory::assertFact(const Node& n){ - d_assertions.push_back(n); -} +namespace CVC4 { +namespace theory { }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/theory.h b/src/theory/theory.h index 76b9697dc..e079d67bd 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -17,25 +17,91 @@ #define __CVC4__THEORY__THEORY_H #include "expr/node.h" +#include "expr/attribute.h" #include "theory/output_channel.h" #include "context/context.h" +#include <queue> +#include <vector> + +#include <typeinfo> + namespace CVC4 { namespace theory { +template <class T> +class TheoryImpl; + /** * Base class for T-solvers. Abstract DPLL(T). + * + * This is essentially an interface class. The TheoryEngine has + * pointers to Theory. But each individual theory implementation T + * should inherit from TheoryImpl<T>, which specializes a few things + * for that theory. */ class Theory { +private: + + template <class T> + friend class TheoryImpl; + + /** + * Construct a Theory. + */ + Theory(context::Context* ctxt, OutputChannel& out) throw() : + d_context(ctxt), + d_out(&out) { + } + + /** + * Disallow default construction. + */ + Theory(); + +protected: + + /** + * The output channel for the Theory. + */ + context::Context* d_context; + + /** + * The output channel for the Theory. + */ + OutputChannel* d_out; + + /** + * The assertFact() queue. + */ + // FIXME CD: on backjump we clear the facts IFF the queue gets + // emptied on every DL. In general I guess we need a CDQueue<>? + // Perhaps one that asserts it's empty at each push? + std::queue<Node> d_facts; /** * Return whether a node is shared or not. Used by setup(). */ - bool isShared(const Node& n); + bool isShared(TNode n) throw(); + + /** + * Returns true if the assertFact queue is empty + */ + bool done() throw() { + return d_facts.empty(); + } public: /** + * Destructs a Theory. This implementation does nothing, but we + * need a virtual destructor for safety in case subclasses have a + * destructor. + */ + virtual ~Theory() { + } + + /** * Subclasses of Theory may add additional efforts. DO NOT CHECK * equality with one of these values (e.g. if STANDARD xxx) but * rather use range checks (or use the helper functions below). @@ -58,20 +124,34 @@ public: static bool fullEffort(Effort e) { return e >= FULL_EFFORT; } /** - * Construct a Theory. + * Set the output channel associated to this theory. */ - Theory(context::Context* c) : d_assertions(c), d_nextAssertion(c, 0){} + void setOutputChannel(OutputChannel& out) { + d_out = &out; + } /** - * Destructs a Theory. This implementation does nothing, but we - * need a virtual destructor for safety in case subclasses have a - * destructor. + * Get the output channel associated to this theory. */ - virtual ~Theory() { + OutputChannel& getOutputChannel() { + return *d_out; + } + + /** + * Get the output channel associated to this theory [const]. + */ + const OutputChannel& getOutputChannel() const { + return *d_out; } /** - * Prepare for a Node. + * Pre-register a term. Done one time for a Node, ever. + * + */ + virtual void preRegisterTerm(TNode) = 0; + + /** + * Register a term. * * When get() is called to get the next thing off the theory queue, * setup() is called on its subterms (in TheoryEngine). Then setup() @@ -81,55 +161,189 @@ public: * setup() MUST NOT MODIFY context-dependent objects that it hasn't * itself just created. */ - - /*virtual void setup(const Node& n) = 0;*/ - - virtual void registerTerm(TNode n) = 0; + virtual void registerTerm(TNode) = 0; /** * Assert a fact in the current context. */ - void assertFact(const Node& n); + void assertFact(TNode n) { + d_facts.push(n); + } /** * Check the current assignment's consistency. */ - virtual void check(OutputChannel& out, - Effort level = FULL_EFFORT) = 0; + virtual void check(Effort level = FULL_EFFORT) = 0; /** * T-propagate new literal assignments in the current context. */ - virtual void propagate(OutputChannel& out, - Effort level = FULL_EFFORT) = 0; + virtual void propagate(Effort level = FULL_EFFORT) = 0; /** * Return an explanation for the literal represented by parameter n * (which was previously propagated by this theory). Report * explanations to an output channel. */ - virtual void explain(OutputChannel& out, - const Node& n, - Effort level = FULL_EFFORT) = 0; -private: - context::CDList<Node> d_assertions; - context::CDO<unsigned> d_nextAssertion; + virtual void explain(TNode n, Effort level = FULL_EFFORT) = 0; + + // + // CODE INVARIANT CHECKING (used only with CVC4_ASSERTIONS) + // -protected: /** - * Returns the next atom in the assertFact() queue. - * Guarentees that registerTerm is called on the theory specific subterms. - * @return the next atom in the assertFact() queue. + * Different states at which invariants are checked. */ - Node get(); + enum ReadyState { + ABOUT_TO_PUSH, + ABOUT_TO_POP + };/* enum ReadyState */ /** - * Returns true if the assertFactQueue is empty + * Public invariant checker. Assert that this theory is in a valid + * state for the (external) system state. This implementation + * checks base invariants and then calls theoryReady(). This + * function may abort in the case of a failed assert, or return + * false (the caller should assert that the return value is true). + * + * @param s the state about which to check invariants */ - bool done(); + bool ready(ReadyState s) { + if(s == ABOUT_TO_PUSH) { + Assert(d_facts.empty(), "Theory base code invariant broken: " + "fact queue is nonempty on context push"); + } + + return theoryReady(s); + } + +protected: + + /** + * Check any invariants at the ReadyState given. Only called by + * Theory class, and then only with CVC4_ASSERTIONS enabled. This + * function may abort in the case of a failed assert, or return + * false (the caller should assert that the return value is true). + * + * @param s the state about which to check invariants + */ + virtual bool theoryReady(ReadyState s) { + return true; + } };/* class Theory */ + +/** + * Base class for T-solver implementations. Each individual + * implementation T of the Theory interface should inherit from + * TheoryImpl<T>. This class specializes some things for a particular + * theory implementation. + * + * The problem with this is that Theory implementations cannot be + * further subclassed without designing all non-children in the type + * DAG to play the same trick as here (be template-polymorphic in their + * most-derived child), linearizing the inheritance hierarchy (viewing + * each instantiation separately). + */ +template <class T> +class TheoryImpl : public Theory { + +protected: + + /** + * Construct a Theory. + */ + TheoryImpl(context::Context* ctxt, OutputChannel& out) : + Theory(ctxt, out) { + /* FIXME: assert here that a TheoryImpl<T> doesn't already exist + * for this NodeManager?? If it does, we're hosed because they'll + * share per-theory node attributes. */ + } + + /** Tag for the "registerTerm()-has-been-called" flag on Nodes */ + struct Registered {}; + /** The "registerTerm()-has-been-called" flag on Nodes */ + typedef CVC4::expr::CDAttribute<Registered, bool> RegisteredAttr; + + /** Tag for the "preRegisterTerm()-has-been-called" flag on Nodes */ + struct PreRegistered {}; + /** The "preRegisterTerm()-has-been-called" flag on Nodes */ + typedef CVC4::expr::Attribute<PreRegistered, bool> PreRegisteredAttr; + + /** + * Returns the next atom in the assertFact() queue. Guarantees that + * registerTerm() has been called on the theory specific subterms. + * + * @return the next atom in the assertFact() queue. + */ + Node get(); +};/* class TheoryImpl<T> */ + +template <class T> +Node TheoryImpl<T>::get() { + Warning.printf("testing %s == %s\n", typeid(*this).name(), typeid(T).name()); + /*Assert(typeid(*this) == typeid(T), + "Improper Theory inheritance chain detected.");*/ + + Assert( !d_facts.empty(), + "Theory::get() called with assertion queue empty!" ); + + Node fact = d_facts.front(); + d_facts.pop(); + + if(! fact.getAttribute(RegisteredAttr())) { + std::vector<TNode> toReg; + toReg.push_back(fact); + + /* Essentially this is doing a breadth-first numbering of + * non-registered subterms with children. Any non-registered + * leaves are immediately registered. */ + for(std::vector<TNode>::iterator workp = toReg.begin(); + workp != toReg.end(); + ++workp) { + + TNode n = *workp; + + for(TNode::iterator i = n.begin(); i != n.end(); ++i) { + TNode c = *i; + + if(! c.getAttribute(RegisteredAttr())) { + if(c.getNumChildren() == 0) { + c.setAttribute(RegisteredAttr(), true); + registerTerm(c); + } else { + toReg.push_back(c); + } + } + } + } + + /* Now register the list of terms in reverse order. Between this + * and the above registration of leaves, this should ensure that + * all subterms in the entire tree were registered in + * reverse-topological order. */ + for(std::vector<TNode>::reverse_iterator i = toReg.rend(); + i != toReg.rbegin(); + ++i) { + + TNode n = *i; + + /* Note that a shared TNode in the DAG rooted at "fact" could + * appear twice on the list, so we have to avoid hitting it + * twice. */ + // FIXME when ExprSets are online, use one of those to avoid + // duplicates in the above? + if(! n.getAttribute(RegisteredAttr())) { + n.setAttribute(RegisteredAttr(), true); + registerTerm(n); + } + } + } + + return fact; +} + }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 348d7e6df..7d630f667 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -18,6 +18,8 @@ #include "expr/node.h" #include "theory/theory.h" +#include "theory/uf/theory_uf.h" +#include "theory/theoryof_table.h" namespace CVC4 { @@ -34,20 +36,67 @@ class SmtEngine; */ class TheoryEngine { + /** Associated SMT engine */ SmtEngine* d_smt; + /** A table of Kinds to pointers to Theory */ + theory::TheoryOfTable theoryOfTable; + + /** + * An output channel for Theory that passes messages + * back to a TheoryEngine. + */ + class EngineOutputChannel : public theory::OutputChannel { + TheoryEngine* d_engine; + public: + void setEngine(TheoryEngine& engine) throw() { + d_engine = &engine; + } + + void conflict(TNode, bool) throw(theory::Interrupted) { + } + + void propagate(TNode, bool) throw(theory::Interrupted) { + } + + void lemma(TNode, bool) throw(theory::Interrupted) { + } + + void explanation(TNode, bool) throw(theory::Interrupted) { + } + }; + + EngineOutputChannel d_theoryOut; + theory::booleans::TheoryBool d_bool; + theory::uf::TheoryUF d_uf; + theory::arith::TheoryArith d_arith; + public: /** * Construct a theory engine. */ - TheoryEngine(SmtEngine* smt) : d_smt(smt) { + TheoryEngine(SmtEngine* smt, context::Context* ctxt) : + d_smt(smt), + d_theoryOut(), + d_bool(ctxt, d_theoryOut), + d_uf(ctxt, d_theoryOut), + d_arith(ctxt, d_theoryOut) { + d_theoryOut.setEngine(*this); + theoryOfTable.registerTheory(&d_bool); + theoryOfTable.registerTheory(&d_uf); + theoryOfTable.registerTheory(&d_arith); } /** * Get the theory associated to a given Node. + * + * @returns the theory, or NULL if the TNode is + * of built-in type. */ - CVC4::theory::Theory* theoryOf(const Node& n); + theory::Theory* theoryOf(TNode n) { + return theoryOfTable[n]; + } };/* class TheoryEngine */ diff --git a/src/theory/theoryof_table_epilogue.h b/src/theory/theoryof_table_epilogue.h new file mode 100644 index 000000000..7483248ec --- /dev/null +++ b/src/theory/theoryof_table_epilogue.h @@ -0,0 +1,21 @@ +/********************* */ +/** theoryof_table_epilogue.h + ** Original author: mdeters + ** 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 theoryOf table. + **/ + +};/* class TheoryOfTable */ + +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__THEORYOF_TABLE_H */ diff --git a/src/theory/theoryof_table_middle.h b/src/theory/theoryof_table_middle.h new file mode 100644 index 000000000..17a945d01 --- /dev/null +++ b/src/theory/theoryof_table_middle.h @@ -0,0 +1,35 @@ +/********************* */ +/** theoryof_table_middle.h + ** Original author: mdeters + ** 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 theoryOf table. + **/ + +namespace CVC4 { +namespace theory { + +class Theory; + +class TheoryOfTable { + + Theory** d_table; + +public: + + TheoryOfTable() : + d_table(new Theory*[::CVC4::kind::LAST_KIND]) { + } + + Theory* operator[](TNode n) { + Assert(n.getKind() >= 0 && n.getKind() < ::CVC4::kind::LAST_KIND, + "illegal to inquire theoryOf(UNDEFINED_KIND or out-of-range)"); + return d_table[n.getKind()]; + } diff --git a/src/theory/theoryof_table_prologue.h b/src/theory/theoryof_table_prologue.h new file mode 100644 index 000000000..5f8c28723 --- /dev/null +++ b/src/theory/theoryof_table_prologue.h @@ -0,0 +1,21 @@ +/********************* */ +/** theoryof_table_prologue.h + ** Original author: mdeters + ** 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 theoryOf table. + **/ + +#ifndef __CVC4__THEORY__THEORYOF_TABLE_H +#define __CVC4__THEORY__THEORYOF_TABLE_H + +#include "expr/kind.h" +#include "util/Assert.h" + diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am index 537b8b124..156733c5b 100644 --- a/src/theory/uf/Makefile.am +++ b/src/theory/uf/Makefile.am @@ -6,6 +6,7 @@ AM_CXXFLAGS = -Wall -fvisibility=hidden noinst_LTLIBRARIES = libuf.la libuf_la_SOURCES = \ + theory_def.h \ ecdata.h \ ecdata.cpp \ theory_uf.h \ diff --git a/src/theory/uf/theory_def.h b/src/theory/uf/theory_def.h new file mode 100644 index 000000000..8e3f5e9f1 --- /dev/null +++ b/src/theory/uf/theory_def.h @@ -0,0 +1,7 @@ +namespace CVC4 { + namespace theory { + namespace uf { + class TheoryUF; + } + } +} diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 1efe13b9b..47bda5bc4 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -19,9 +19,10 @@ #include "expr/kind.h" using namespace CVC4; -using namespace context; -using namespace theory; -using namespace uf; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::uf; @@ -30,8 +31,8 @@ Node getOperator(Node x) { return Node::null(); } -TheoryUF::TheoryUF(Context* c) : - Theory(c), +TheoryUF::TheoryUF(Context* c, OutputChannel& out) : + TheoryImpl<TheoryUF>(c, out), d_pending(c), d_currentPendingIdx(c,0), d_disequality(c), @@ -40,13 +41,16 @@ TheoryUF::TheoryUF(Context* c) : TheoryUF::~TheoryUF(){} +void TheoryUF::preRegisterTerm(TNode n){ +} + void TheoryUF::registerTerm(TNode n){ d_registered.push_back(n); ECData* ecN; - if(n.hasAttribute(ECAttr(),&ecN)){ + if(n.hasAttribute(ECAttr(), ecN)){ /* registerTerm(n) is only called when a node has not been seen in the * current context. ECAttr() is not a context-dependent attribute. * When n.hasAttribute(ECAttr(),...) is true on a registerTerm(n) call, @@ -222,9 +226,9 @@ void TheoryUF::merge(){ } } -void TheoryUF::check(OutputChannel& out, Effort level){ +void TheoryUF::check(Effort level){ while(!done()){ - Node assertion = get(); + Node assertion;// = get(); switch(assertion.getKind()){ case EQUAL: @@ -252,7 +256,7 @@ void TheoryUF::check(OutputChannel& out, Effort level){ TNode left = (*diseqIter)[0]; TNode right = (*diseqIter)[1]; if(sameCongruenceClass(left, right)){ - out.conflict(*diseqIter, true); + d_out->conflict(*diseqIter, true); } } } diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index b68a96e65..4bb18bd43 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -21,7 +21,6 @@ #include "expr/attribute.h" #include "theory/theory.h" -#include "theory/output_channel.h" #include "context/context.h" #include "theory/uf/ecdata.h" @@ -30,9 +29,8 @@ namespace CVC4 { namespace theory { namespace uf { +class TheoryUF : public TheoryImpl<TheoryUF> { - -class TheoryUF : public Theory { private: @@ -72,7 +70,7 @@ private: public: /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ - TheoryUF(context::Context* c); + TheoryUF(context::Context* c, OutputChannel& out); /** Destructor for the TheoryUF object. */ ~TheoryUF(); @@ -82,14 +80,13 @@ public: //has pending changes to the contracts void registerTerm(TNode n); + void preRegisterTerm(TNode n); - void check(OutputChannel& out, Effort level= FULL_EFFORT); + void check(Effort level); - void propagate(OutputChannel& out, Effort level= FULL_EFFORT){} + void propagate(Effort level) {} - void explain(OutputChannel& out, - const Node& n, - Effort level = FULL_EFFORT){} + void explain(TNode n, Effort level) {} private: /** |