From 5fbb341a673ec5fa42f260bb137f423ac2aea324 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 8 Mar 2011 21:43:45 +0000 Subject: [PATCH] Clean up Theory base class as per code review bug #60; also fixes to CodeTimer statistic, and adding a CodeTimer to TheoryEngine::EngineOutputChannel::newFact() for investigation into (possible) slow or redundant theory registration. --- src/include/cvc4_public.h | 5 +- src/theory/theory.h | 91 +++++++++++------------------------- src/theory/theory_engine.cpp | 2 + src/theory/theory_engine.h | 5 ++ src/util/stats.h | 23 +++++---- 5 files changed, 53 insertions(+), 73 deletions(-) diff --git a/src/include/cvc4_public.h b/src/include/cvc4_public.h index 2ac1facb0..a2db90457 100644 --- a/src/include/cvc4_public.h +++ b/src/include/cvc4_public.h @@ -68,13 +68,16 @@ #ifdef __GNUC__ # define CVC4_UNUSED __attribute__((unused)) +# define CVC4_NORETURN __attribute__ ((noreturn)) +# define CVC4_CONST_FUNCTION __attribute__ ((const)) #else /* ! __GNUC__ */ # define CVC4_UNUSED +# define CVC4_NORETURN +# define CVC4_CONST_FUNCTION #endif /* __GNUC__ */ #define EXPECT_TRUE(x) __builtin_expect( (x), true ) #define EXPECT_FALSE(x) __builtin_expect( (x), false ) -#define CVC4_NORETURN __attribute__ ((noreturn)) #ifndef NULL # define NULL ((void*) 0) diff --git a/src/theory/theory.h b/src/theory/theory.h index 85ea375f7..620c70710 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -75,8 +75,8 @@ private: /** * The assertFact() queue. * - * These can not be TNodes as some atoms (such as equalities) are sent across theories withouth being stored - * in a global map. + * These can not be TNodes as some atoms (such as equalities) are sent + * across theories without being stored in a global map. */ context::CDList d_facts; @@ -201,15 +201,19 @@ public: FULL_EFFORT = 100 };/* enum Effort */ - // TODO add compiler annotation "constant function" here - static bool minEffortOnly(Effort e) { return e == MIN_EFFORT; } - static bool quickCheckOrMore(Effort e) { return e >= QUICK_CHECK; } - static bool quickCheckOnly(Effort e) { return e >= QUICK_CHECK && - e < STANDARD; } - static bool standardEffortOrMore(Effort e) { return e >= STANDARD; } - static bool standardEffortOnly(Effort e) { return e >= STANDARD && - e < FULL_EFFORT; } - static bool fullEffort(Effort e) { return e >= FULL_EFFORT; } + // simple, useful predicates for effort values + static inline bool minEffortOnly(Effort e) CVC4_CONST_FUNCTION + { return e == MIN_EFFORT; } + static inline bool quickCheckOrMore(Effort e) CVC4_CONST_FUNCTION + { return e >= QUICK_CHECK; } + static inline bool quickCheckOnly(Effort e) CVC4_CONST_FUNCTION + { return e >= QUICK_CHECK && e < STANDARD; } + static inline bool standardEffortOrMore(Effort e) CVC4_CONST_FUNCTION + { return e >= STANDARD; } + static inline bool standardEffortOnly(Effort e) CVC4_CONST_FUNCTION + { return e >= STANDARD && e < FULL_EFFORT; } + static inline bool fullEffort(Effort e) CVC4_CONST_FUNCTION + { return e >= FULL_EFFORT; } /** * Get the id for this Theory. @@ -239,13 +243,6 @@ public: return *d_out; } - /** - * Get the output channel associated to this theory [const]. - */ - const OutputChannel& getOutputChannel() const { - return *d_out; - } - /** * Pre-register a term. Done one time for a Node, ever. */ @@ -312,7 +309,10 @@ public: * (which was previously propagated by this theory). Report * explanations to an output channel. */ - virtual void explain(TNode n) { } + virtual void explain(TNode n) { + Unimplemented("Theory %s propagated a node but doesn't implement the " + "Theory::explain() interface!", identify().c_str()); + } /** * Return the value of a node (typically used after a ). If the @@ -345,7 +345,11 @@ public: * and suspect this situation is the case, return Node::null() * rather than throwing an exception. */ - virtual Node getValue(TNode n, Valuation* valuation) = 0; + virtual Node getValue(TNode n, Valuation* valuation) { + Unimplemented("Theory %s doesn't support Theory::getValue interface", + identify().c_str()); + return Node::null(); + } /** * The theory should only add (via .operator<< or .append()) to the @@ -363,7 +367,7 @@ public: * assertFact() queue using get(). A Theory can raise conflicts, * add lemmas, and propagate literals during presolve(). */ - virtual void presolve() { }; + virtual void presolve() { } /** * Notification sent to the theory wheneven the search restarts. @@ -379,51 +383,10 @@ public: */ virtual std::string identify() const = 0; - virtual void notifyOptions(const Options& opt) {} - - // - // CODE INVARIANT CHECKING (used only with CVC4_ASSERTIONS) - // - /** - * Different states at which invariants are checked. + * Notify the theory of the current set of options. */ - enum ReadyState { - ABOUT_TO_PUSH, - ABOUT_TO_POP - };/* enum ReadyState */ - - /** - * 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 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; - } + virtual void notifyOptions(const Options& opt) { } };/* class Theory */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index a577e8f9b..3c59b43e4 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -52,6 +52,8 @@ typedef expr::Attribute IteRewriteAttr; }/* CVC4::theory namespace */ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) { + TimerStat::CodeTimer codeTimer(d_newFactTimer); + //FIXME: Assert(fact.isLiteral(), "expected literal"); if (fact.getKind() == kind::NOT) { // No need to register negations - only atoms diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 7a82a1b05..4b37d4dd6 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -74,6 +74,11 @@ class TheoryEngine { */ std::vector d_propagatedLiterals; + /** Time spent in newFact() (largely spent doing term registration) */ + KEEP_STATISTIC(TimerStat, + d_newFactTimer, + "theory::newFactTimer"); + public: EngineOutputChannel(TheoryEngine* engine, context::Context* context) : diff --git a/src/util/stats.h b/src/util/stats.h index 978893a51..4dbf31120 100644 --- a/src/util/stats.h +++ b/src/util/stats.h @@ -509,16 +509,20 @@ public: inline ::timespec& operator+=(::timespec& a, const ::timespec& b) { // assumes a.tv_nsec and b.tv_nsec are in range const long nsec_per_sec = 1000000000L; // one thousand million + Assert(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec); + Assert(b.tv_nsec >= 0 && b.tv_nsec < nsec_per_sec); a.tv_sec += b.tv_sec; long nsec = a.tv_nsec + b.tv_nsec; - while(nsec < 0) { + Assert(nsec >= 0); + if(nsec < 0) { nsec += nsec_per_sec; - ++a.tv_sec; + --a.tv_sec; } - while(nsec >= nsec_per_sec) { + if(nsec >= nsec_per_sec) { nsec -= nsec_per_sec; - --a.tv_sec; + ++a.tv_sec; } + Assert(nsec >= 0 && nsec < nsec_per_sec); a.tv_nsec = nsec; return a; } @@ -527,16 +531,19 @@ inline ::timespec& operator+=(::timespec& a, const ::timespec& b) { inline ::timespec& operator-=(::timespec& a, const ::timespec& b) { // assumes a.tv_nsec and b.tv_nsec are in range const long nsec_per_sec = 1000000000L; // one thousand million + Assert(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec); + Assert(b.tv_nsec >= 0 && b.tv_nsec < nsec_per_sec); a.tv_sec -= b.tv_sec; long nsec = a.tv_nsec - b.tv_nsec; - while(nsec < 0) { + if(nsec < 0) { nsec += nsec_per_sec; - ++a.tv_sec; + --a.tv_sec; } - while(nsec >= nsec_per_sec) { + if(nsec >= nsec_per_sec) { nsec -= nsec_per_sec; - --a.tv_sec; + ++a.tv_sec; } + Assert(nsec >= 0 && nsec < nsec_per_sec); a.tv_nsec = nsec; return a; } -- 2.30.2