summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/include/cvc4_public.h5
-rw-r--r--src/theory/theory.h91
-rw-r--r--src/theory/theory_engine.cpp2
-rw-r--r--src/theory/theory_engine.h5
-rw-r--r--src/util/stats.h23
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<Node> 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.
@@ -240,13 +244,6 @@ public:
}
/**
- * 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.
*/
virtual void preRegisterTerm(TNode) { }
@@ -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<IteRewriteTag, Node> 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<TNode> 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;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback