/**
* 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;
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.
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.
*/
* (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
* 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
* 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.
*/
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 */
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;
}
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;
}
projects / cvc5.git / commitdiff