diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-05-09 21:25:17 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-05-09 21:25:17 +0000 |
commit | 1ce0650dcf8ce30424b546deb540974cc510c215 (patch) | |
tree | 74a9985463234fc9adfed2de209c134ed7da359b /src/context | |
parent | 690fb2843d9845e405fee54eb2d8023eebbd5b72 (diff) |
* simplifying equality engine interface
* notifications are now through the interface subclass instead of a template
* notifications include constants being merged
* changed contextNotifyObj::notify to contextNotifyObj::contextNotifyPop so it's more descriptive and doesn't clutter methods when subclassed
* sat solver now has explicit methods to make true and false constants
* 0-level literals are removed from explanations of propagations
Diffstat (limited to 'src/context')
-rw-r--r-- | src/context/context.cpp | 4 | ||||
-rw-r--r-- | src/context/context.h | 16 | ||||
-rw-r--r-- | src/context/stacking_map.h | 16 | ||||
-rw-r--r-- | src/context/stacking_vector.h | 4 |
4 files changed, 23 insertions, 17 deletions
diff --git a/src/context/context.cpp b/src/context/context.cpp index abb1575d4..da60a5bc4 100644 --- a/src/context/context.cpp +++ b/src/context/context.cpp @@ -80,7 +80,7 @@ void Context::pop() { while(pCNO != NULL) { // pre-store the "next" pointer in case pCNO deletes itself on notify() ContextNotifyObj* next = pCNO->d_pCNOnext; - pCNO->notify(); + pCNO->contextNotifyPop(); pCNO = next; } @@ -101,7 +101,7 @@ void Context::pop() { while(pCNO != NULL) { // pre-store the "next" pointer in case pCNO deletes itself on notify() ContextNotifyObj* next = pCNO->d_pCNOnext; - pCNO->notify(); + pCNO->contextNotifyPop(); pCNO = next; } diff --git a/src/context/context.h b/src/context/context.h index f0dbff72b..165c35c58 100644 --- a/src/context/context.h +++ b/src/context/context.h @@ -658,6 +658,7 @@ public: * the ContextObj objects have been restored). */ class ContextNotifyObj { + /** * Context is our friend so that when the Context is deleted, any * remaining ContextNotifyObj can be removed from the Context list. @@ -686,6 +687,15 @@ class ContextNotifyObj { */ ContextNotifyObj**& prev() throw() { return d_ppCNOprev; } +protected: + + /** + * This is the method called to notify the object of a pop. It must be + * implemented by the subclass. It is protected since context is out + * friend. + */ + virtual void contextNotifyPop() = 0; + public: /** @@ -703,12 +713,6 @@ public: */ virtual ~ContextNotifyObj() throw(AssertionException); - /** - * This is the method called to notify the object of a pop. It must be - * implemented by the subclass. - */ - virtual void notify() = 0; - };/* class ContextNotifyObj */ inline void ContextObj::makeCurrent() throw(AssertionException) { diff --git a/src/context/stacking_map.h b/src/context/stacking_map.h index 2dec1845c..ba644596e 100644 --- a/src/context/stacking_map.h +++ b/src/context/stacking_map.h @@ -96,6 +96,14 @@ class StackingMap : context::ContextNotifyObj { /** Our current offset in the d_trace stack (context-dependent). */ context::CDO<size_t> d_offset; +protected: + + /** + * Called by the Context when a pop occurs. Cancels everything to the + * current context level. Overrides ContextNotifyObj::contextNotifyPop(). + */ + void contextNotifyPop(); + public: typedef typename MapType::const_iterator const_iterator; @@ -128,12 +136,6 @@ public: */ void set(ArgType n, const ValueType& newValue); - /** - * Called by the Context when a pop occurs. Cancels everything to the - * current context level. Overrides ContextNotifyObj::notify(). - */ - void notify(); - };/* class StackingMap<> */ template <class KeyType, class ValueType, class KeyHash> @@ -146,7 +148,7 @@ void StackingMap<KeyType, ValueType, KeyHash>::set(ArgType n, const ValueType& n } template <class KeyType, class ValueType, class KeyHash> -void StackingMap<KeyType, ValueType, KeyHash>::notify() { +void StackingMap<KeyType, ValueType, KeyHash>::contextNotifyPop() { Trace("sm") << "SM cancelling : " << d_offset << " < " << d_trace.size() << " ?" << std::endl; while(d_offset < d_trace.size()) { std::pair<ArgType, ValueType> p = d_trace.back(); diff --git a/src/context/stacking_vector.h b/src/context/stacking_vector.h index 9987731d4..ed311b952 100644 --- a/src/context/stacking_vector.h +++ b/src/context/stacking_vector.h @@ -82,7 +82,7 @@ public: * Called by the Context when a pop occurs. Cancels everything to the * current context level. Overrides ContextNotifyObj::notify(). */ - void notify(); + void contextNotifyPop(); };/* class StackingVector<> */ @@ -99,7 +99,7 @@ void StackingVector<T>::set(size_t n, const T& newValue) { } template <class T> -void StackingVector<T>::notify() { +void StackingVector<T>::contextNotifyPop() { Trace("sv") << "SV cancelling : " << d_offset << " < " << d_trace.size() << " ?" << std::endl; while(d_offset < d_trace.size()) { std::pair<size_t, T> p = d_trace.back(); |