elaborate prop_convt::handle(expr)

This change adds three features:

1) Non-boolean expressions are returned verbatim.

2) Boolean expressions that are determined to be a constant (e.g., by means
of constant folding) are returned as constants, to enable further
optimisation by users.

3) Literals returned are frozen, to simplify incremental usage.

Author: Daniel Kroening

src/solvers/prop/prop_conv.cpp

@@ -10,11 +10,30 @@ Author: Daniel Kroening, [email protected]
 
 #include "literal_expr.h"
 
+#include <util/std_expr.h>
+
 #include <algorithm>
 
 exprt prop_convt::handle(const exprt &expr)
 {
-  return literal_exprt(convert(expr));
+  // We can only improve Booleans.
+  if(expr.type().id() != ID_bool)
+    return expr;
+
+  // We convert to a literal to obtain a 'small' handle
+  literalt l = convert(expr);
+
+  // The literal may be a constant as a result of non-trivial
+  // propagation. We return constants as such.
+  if(l.is_true())
+    return true_exprt();
+  else if(l.is_false())
+    return false_exprt();
+
+  // freeze to enable incremental use
+  set_frozen(l);
+
+  return literal_exprt(l);
 }
 
 /// determine whether a variable is in the final conflict