diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-02-25 07:48:03 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-02-25 07:48:03 +0000 |
commit | 826f583ee14b922f39666dc827a5624fff753724 (patch) | |
tree | 03e7f1ad98b003dae5f6406bb990a715041d239c /src/theory/theory.h | |
parent | f716b67e7bedd90c4dd43617158c0f55c1811334 (diff) |
* src/expr/node.h: add a copy constructor. Apparently GCC doesn't
recognize an instantiation of the join conversion/copy ctor with
ref_count = ref_count_1 as a copy constructor. Problems with
reference counts ensue.
* src/theory/theory.h, src/theory/theory.cpp: Theory base
implementation work. Changed from continuation-style theory calls
to having an data member for the output channel. registerTerm() and
preRegisterTerm() work.
* src/theory/output_channel.h, src/theory/theory.h,
src/theory/theory.cpp, src/theory/uf/theory_uf.h,
src/theory/uf/theory_uf.cpp: merged ExplainOutputChannel into
OutputChannel.
* test/unit/expr/node_black.h: remove testPlusNode(),
testUMinusNode(), testMultNode().
* src/expr/attribute.h: new facilities ManagedAttribute<> and
CDAttribute<>, and add new template parameters to Attribute<>. Make
CDAttribute<>s work with context manager.
* src/expr/attribute.h, src/expr/node_manager.h: VarNameAttr and
TypeAttr are now "owned" (defined) by the NodeManager. The
AttributeManager knows nothing of specific attributes, it just as
all the code for dealing generically with attributes.
* test/unit/expr/node_white.h: test new attribute facilities.
* src/expr/soft_node.h: removed: We now have TNode, so SoftNode goes
away.
* src/theory/Makefile.am: fixed improper linking of theories
* src/theory/theory_engine.h: some implementation work (mainly stubs
for now, just to make sure TheoryUF can be instantiated properly,
etc.)
* src/expr/node_value.cpp, src/expr/node_value.h: move a number of
function implementations to the header and make them inline
* src/expr/node_manager.cpp, src/expr/node_manager.h: move a number of
function implementations to the header and make them inline
* src/theory/theoryof_table_prologue.h,
src/theory/theoryof_table_epilogue.h, src/theory/mktheoryof,
src/theory/Makefile.am: make the theoryOf() table from kinds and
implement TheoryEngine::theoryOf().
* src/theory/arith/Makefile, src/theory/bool/Makefile: generated these
stub Makefiles (with contrib/addsourcedir) as per policy
* src/theory/arith, src/theory/bool [directory properties]: add .deps
to svn:ignore.
* contrib/configure-in-place: permit configuring "in-place" in the
source directory.
* contrib/get-authors, contrib/dimacs_to_smt.pl,
contrib/update-copyright.pl, contrib/get-authors,
contrib/addsourcedir, src/expr/mkkind: copyright notice
* src/expr/node_manager.h, src/expr/node_builder.h,
src/prop/prop_engine.h, src/prop/prop_engine.cpp,
src/theory/theory_engine.h, src/smt/smt_engine.h, src/smt/smt_engine.cpp,
src/theory/output_channel.h: turn "const Node&"-typed formal
parameters into "TNode"
* src/theory/bool, src/theory/booleans: "bool" directory renamed "booleans"
to avoid keyword clash on containing namespace
* src/theory/booleans/theory_def.h, src/theory/uf/theory_def.h,
src/theory/arith/theory_def.h: "define" a theory simply (for automatic
theoryOf() generator).
* src/Makefile.am: build theory subdirectory before prop, smt, etc. so that
src/theory/theoryof_table.h header gets generated before it's needed
* src/expr/node_prologue.h, src/expr/node_middle.h: move "Kind" into a
separate CVC4::kind namespace to avoid its contents from cluttering
the CVC4 root namespace. Import the symbol "Kind" into the CVC4 namespace
but not the enum values.
* src/expr/node_manager.h, src/expr/node.h, src/expr/node_value.h,
src/expr/node_value.cpp, src/expr/expr.cpp, src/theory/uf/theory_uf.cpp,
src/prop/cnf_stream.cpp, src/parser/smt/smt_parser.g,
src/parser/cvc/cvc_parser.g, src/parser/antlr_parser.cpp,
test/unit/expr/node_white.h, test/unit/expr/node_black.h,
test/unit/expr/kind_black.h, test/unit/expr/node_builder_black.h:
update for having moved Kind into CVC4::kind.
* src/parser/parser.cpp: added file-does-not-exist check (was failing
silently).
Diffstat (limited to 'src/theory/theory.h')
-rw-r--r-- | src/theory/theory.h | 274 |
1 files changed, 244 insertions, 30 deletions
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 */ |