Merge pull request #6922 from diffblue/named_term

introduce named_term expressions

Author: kroening

src/solvers/flattening/boolbv.cpp

@@ -185,6 +185,12 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
   else if(expr.id()==ID_string_constant)
     return convert_bitvector(
       to_string_constant(expr).to_array_expr());
+  else if(expr.id() == ID_named_term)
+  {
+    const auto &named_term_expr = to_named_term_expr(expr);
+    set_to_true(equal_exprt(named_term_expr.symbol(), named_term_expr.value()));
+    return convert_symbol(named_term_expr.symbol());
+  }
   else if(expr.id()==ID_array)
     return convert_array(expr);
   else if(expr.id()==ID_vector)

src/solvers/prop/prop_conv_solver.cpp

@@ -300,6 +300,14 @@ literalt prop_conv_solvert::convert_bool(const exprt &expr)
       return equal ? prop.lequal(tmp1, tmp2) : prop.lxor(tmp1, tmp2);
     }
   }
+  else if(expr.id() == ID_named_term)
+  {
+    const auto &named_term_expr = to_named_term_expr(expr);
+    literalt value_converted = convert(named_term_expr.value());
+    set_to_true(
+      equal_exprt(named_term_expr.symbol(), literal_exprt(value_converted)));
+    return value_converted;
+  }
 
   return convert_rest(expr);
 }

src/solvers/smt2/smt2_conv.cpp

@@ -1607,6 +1607,14 @@ void smt2_convt::convert_expr(const exprt &expr)
         "unsupported type for " + shift_expr.id_string() + ": " +
         type.id_string());
   }
+  else if(expr.id() == ID_named_term)
+  {
+    const auto &named_term_expr = to_named_term_expr(expr);
+    out << "(! ";
+    convert(named_term_expr.value());
+    out << " :named "
+        << convert_identifier(named_term_expr.symbol().get_identifier()) << ')';
+  }
   else if(expr.id()==ID_with)
   {
     convert_with(to_with_expr(expr));

src/util/irep_ids.def

@@ -227,6 +227,7 @@ IREP_ID_ONE(ieee_float_equal)
 IREP_ID_ONE(ieee_float_notequal)
 IREP_ID_ONE(isnan)
 IREP_ID_ONE(lambda)
+IREP_ID_ONE(named_term)
 IREP_ID_ONE(array_comprehension)
 IREP_ID_ONE(array_of)
 IREP_ID_ONE(array_equal)

src/util/std_expr.h

@@ -3543,4 +3543,77 @@ inline bool can_cast_expr<class_method_descriptor_exprt>(const exprt &base)
   return base.id() == ID_virtual_function;
 }
 
+/// \brief Expression that introduces a new symbol that is equal to the operand.
+/// This expression corresponds to the SMT-LIB2 feature 'named term'.
+/// The symbol is not bound, i.e., visible outside of this expression.
+/// The expression roughly corresponds to Python's "walrus operator", but
+/// is not a side effect.
+class named_term_exprt : public binary_exprt
+{
+public:
+  explicit named_term_exprt(symbol_exprt symbol, exprt value)
+    : binary_exprt(
+        std::move(symbol),
+        ID_named_term,
+        value, // not moved, for type
+        value.type())
+  {
+    PRECONDITION(symbol.type() == type());
+  }
+
+  const symbol_exprt &symbol() const
+  {
+    return static_cast<const symbol_exprt &>(op0());
+  }
+
+  symbol_exprt &symbol()
+  {
+    return static_cast<symbol_exprt &>(op0());
+  }
+
+  const exprt &value() const
+  {
+    return op1();
+  }
+
+  exprt &value()
+  {
+    return op1();
+  }
+};
+
+template <>
+inline bool can_cast_expr<named_term_exprt>(const exprt &base)
+{
+  return base.id() == ID_named_term;
+}
+
+inline void validate_expr(const named_term_exprt &value)
+{
+  validate_operands(value, 2, "'named term' must have two operands");
+}
+
+/// \brief Cast an exprt to a \ref named_term_exprt
+///
+/// \a expr must be known to be \ref named_term_exprt.
+///
+/// \param expr: Source expression
+/// \return Object of type \ref named_term_exprt
+inline const named_term_exprt &to_named_term_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_named_term);
+  const named_term_exprt &ret = static_cast<const named_term_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
+/// \copydoc to_array_comprehension_expr(const exprt &)
+inline named_term_exprt &to_named_term_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_named_term);
+  named_term_exprt &ret = static_cast<named_term_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
 #endif // CPROVER_UTIL_STD_EXPR_H