models for literal_exprt

This enables us to use decision_proceduret::get for handles that are
literal_exprt.

Author: Daniel Kroening

src/solvers/prop/prop_conv_solver.cpp

@@ -66,6 +66,10 @@ optionalt<bool> prop_conv_solvert::get_bool(const exprt &expr) const
 
     return prop.l_get(result->second).is_true();
   }
+  else if(expr.id() == ID_literal)
+  {
+    return prop.l_get(to_literal_expr(expr).get_literal()).is_true();
+  }
 
   // sub-expressions
 

src/solvers/smt2/smt2_conv.cpp

@@ -208,6 +208,24 @@ exprt smt2_convt::get(const exprt &expr) const
       return nil_exprt();
     return member_exprt(tmp, member_expr.get_component_name(), expr.type());
   }
+  else if(expr.id() == ID_literal)
+  {
+    auto l = to_literal_expr(expr).get_literal();
+    if(l_get(l).is_true())
+      return true_exprt();
+    else
+      return false_exprt();
+  }
+  else if(expr.id() == ID_not)
+  {
+    auto op = get(to_not_expr(expr).op());
+    if(op.is_true())
+      return false_exprt();
+    else if(op.is_false())
+      return true_exprt();
+  }
+  else if(expr.is_constant())
+    return expr;
 
   return nil_exprt();
 }