also notify assignments, not just goals

Daniel Kroening · Daniel Kroening · commit fcf83dc6feb9 · 2016-08-19T10:51:34.000+01:00
diff --git a/src/solvers/prop/cover_goals.cpp b/src/solvers/prop/cover_goals.cpp
@@ -41,6 +41,10 @@ Function: cover_goalst::mark
 
 void cover_goalst::mark()
 {
+  // notify observers
+  for(const auto & o : observers)
+    o->satisfying_assignment();
+
   for(auto & g : goals)
     if(g.status==goalt::statust::UNKNOWN &&
        prop_conv.l_get(g.condition).is_true())
diff --git a/src/solvers/prop/cover_goals.h b/src/solvers/prop/cover_goals.h
@@ -82,7 +82,8 @@ class cover_goalst:public messaget
   class observert
   {
   public:
-    virtual void goal_covered(const goalt &)=0;
+    virtual void goal_covered(const goalt &) { }
+    virtual void satisfying_assignment() { }
   };
   
   inline void register_observer(observert &o)

Original file line number	Diff line number	Diff line change
`@@ -82,7 +82,8 @@ class cover_goalst:public messaget`
`82`	`82`	`class observert`
`83`	`83`	`{`
`84`	`84`	`public:`
`85`		`- virtual void goal_covered(const goalt &)=0;`
	`85`	`+ virtual void goal_covered(const goalt &) { }`
	`86`	`+ virtual void satisfying_assignment() { }`
`86`	`87`	`};`
`87`	`88`
`88`	`89`	`inline void register_observer(observert &o)`