prop_conv_solvert::get_bool now always returns a value

The previous implementation has considered the case of an unknown expression
and a known expression with unknown value.  In both cases, the next layer
returns 'false'.

The new implementation now returns 'false' directly.

Author: Daniel Kroening

src/solvers/prop/prop_conv_solver.cpp

@@ -43,18 +43,16 @@ literalt prop_conv_solvert::get_literal(const irep_idt &identifier)
 }
 
 /// get a boolean value from counter example if not valid
-bool prop_conv_solvert::get_bool(const exprt &expr, tvt &value) const
+bool prop_conv_solvert::get_bool(const exprt &expr) const
 {
   // trivial cases
 
   if(expr.is_true())
   {
-    value = tvt(true);
-    return false;
+    return true;
   }
   else if(expr.is_false())
   {
-    value = tvt(false);
     return false;
   }
   else if(expr.id() == ID_symbol)
@@ -63,10 +61,9 @@ bool prop_conv_solvert::get_bool(const exprt &expr, tvt &value) const
       symbols.find(to_symbol_expr(expr).get_identifier());
 
     if(result == symbols.end())
-      return true;
+      return false; // default value
 
-    value = prop.l_get(result->second);
-    return false;
+    return prop.l_get(result->second).is_true();
   }
 
   // sub-expressions
@@ -75,58 +72,40 @@ bool prop_conv_solvert::get_bool(const exprt &expr, tvt &value) const
   {
     if(expr.type().id() == ID_bool && expr.operands().size() == 1)
     {
-      if(get_bool(expr.op0(), value))
-        return true;
-      value = !value;
-      return false;
+      return get_bool(expr.op0());
     }
   }
   else if(expr.id() == ID_and || expr.id() == ID_or)
   {
     if(expr.type().id() == ID_bool && expr.operands().size() >= 1)
     {
-      value = tvt(expr.id() == ID_and);
-
       forall_operands(it, expr)
       {
-        tvt tmp;
-        if(get_bool(*it, tmp))
-          return true;
+        auto tmp = get_bool(*it);
 
         if(expr.id() == ID_and)
         {
-          if(tmp.is_false())
-          {
-            value = tvt(false);
+          if(tmp == false)
             return false;
-          }
-
-          value = value && tmp;
         }
         else // or
         {
-          if(tmp.is_true())
-          {
-            value = tvt(true);
-            return false;
-          }
-
-          value = value || tmp;
+          if(tmp == true)
+            return true;
         }
       }
 
-      return false;
+      return expr.id() == ID_and;
     }
   }
 
   // check cache
 
   cachet::const_iterator cache_result = cache.find(expr);
   if(cache_result == cache.end())
-    return true;
-
-  value = prop.l_get(cache_result->second);
-  return false;
+    return false; // default value
+  else
+    return prop.l_get(cache_result->second).is_true();
 }
 
 literalt prop_conv_solvert::convert(const exprt &expr)
@@ -459,28 +438,12 @@ decision_proceduret::resultt prop_conv_solvert::dec_solve()
 
 exprt prop_conv_solvert::get(const exprt &expr) const
 {
-  tvt value;
-
-  if(expr.type().id() == ID_bool && !get_bool(expr, value))
-  {
-    switch(value.get_value())
-    {
-    case tvt::tv_enumt::TV_TRUE:
-      return true_exprt();
-    case tvt::tv_enumt::TV_FALSE:
-      return false_exprt();
-    case tvt::tv_enumt::TV_UNKNOWN:
-      return false_exprt(); // default
-    }
-  }
+  PRECONDITION(expr.type().id() == ID_bool);
 
-  exprt tmp = expr;
-  for(auto &op : tmp.operands())
-  {
-    exprt tmp_op = get(op);
-    op.swap(tmp_op);
-  }
-  return tmp;
+  if(get_bool(expr))
+    return true_exprt();
+  else
+    return false_exprt();
 }
 
 void prop_conv_solvert::print_assignment(std::ostream &out) const

src/solvers/prop/prop_conv_solver.h

@@ -112,7 +112,7 @@ class prop_conv_solvert : public prop_convt, public solver_resource_limitst
   bool post_processing_done = false;
 
   // get a _boolean_ value from counterexample if not valid
-  virtual bool get_bool(const exprt &expr, tvt &value) const;
+  virtual bool get_bool(const exprt &expr) const;
 
   virtual literalt convert_rest(const exprt &expr);
   virtual literalt convert_bool(const exprt &expr);