Add a method to convert the domain to a predicate to the basic domain API.

martin · martin · commit 028d8b648ed9 · 2018-07-24T15:27:18.000+01:00
This allows the domain to be converted to an assumption or an assertion
amongst other applications.
diff --git a/src/analyses/ai_domain.h b/src/analyses/ai_domain.h
@@ -119,6 +119,16 @@ class ai_domain_baset
   virtual bool ai_simplify_lhs(
     exprt &condition,
     const namespacet &ns) const;
+
+  // Gives a Boolean condition that is true for all values represented by the
+  // domain.  This allows domains to be converted into program invariants.
+  virtual exprt to_predicate(void) const
+  {
+    if(is_bottom())
+      return false_exprt();
+    else
+      return true_exprt();
+  }
 };
 
 #endif
