diff options
Diffstat (limited to 'src/theory/theory.h')
-rw-r--r-- | src/theory/theory.h | 46 |
1 files changed, 34 insertions, 12 deletions
diff --git a/src/theory/theory.h b/src/theory/theory.h index 620c70710..72341869d 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -23,6 +23,7 @@ #include "expr/node.h" #include "expr/attribute.h" +#include "theory/valuation.h" #include "theory/output_channel.h" #include "context/context.h" #include "context/cdlist.h" @@ -37,10 +38,11 @@ namespace CVC4 { class TheoryEngine; namespace theory { - class Valuation; -}/* CVC4::theory namespace */ -namespace theory { +/** Tag for the "newFact()-has-been-called-in-this-context" flag on Nodes */ +struct AssertedAttrTag {}; +/** The "newFact()-has-been-called-in-this-context" flag on Nodes */ +typedef CVC4::expr::CDAttribute<AssertedAttrTag, bool> Asserted; /** * Base class for T-solvers. Abstract DPLL(T). @@ -88,16 +90,15 @@ protected: /** * Construct a Theory. */ - Theory(TheoryId id, context::Context* ctxt, OutputChannel& out) throw() : + Theory(TheoryId id, context::Context* ctxt, OutputChannel& out, Valuation valuation) throw() : d_id(id), d_context(ctxt), d_facts(ctxt), d_factsHead(ctxt, 0), - d_out(&out) { + d_out(&out), + d_valuation(valuation) { } - - /** * This is called at shutdown time by the TheoryEngine, just before * destruction. It is important because there are destruction @@ -114,10 +115,11 @@ protected: */ OutputChannel* d_out; - /** 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; + /** + * The valuation proxy for the Theory to communicate back with the + * theory engine (and other theories). + */ + Valuation d_valuation; /** * Returns the next atom in the assertFact() queue. Guarantees that @@ -135,6 +137,26 @@ protected: return fact; } + /** + * Provides access to the facts queue, primarily intended for theory + * debugging purposes. + * + * @return the iterator to the beginning of the fact queue + */ + context::CDList<Node>::const_iterator facts_begin() const { + return d_facts.begin(); + } + + /** + * Provides access to the facts queue, primarily intended for theory + * debugging purposes. + * + * @return the iterator to the end of the fact queue + */ + context::CDList<Node>::const_iterator facts_end() const { + return d_facts.end(); + } + public: static inline TheoryId theoryOf(TypeNode typeNode) { @@ -345,7 +367,7 @@ public: * and suspect this situation is the case, return Node::null() * rather than throwing an exception. */ - virtual Node getValue(TNode n, Valuation* valuation) { + virtual Node getValue(TNode n) { Unimplemented("Theory %s doesn't support Theory::getValue interface", identify().c_str()); return Node::null(); |