use ternary_exprt

This uses ternary_exprt to strengthen the typing of expressions with three
operands.

Author: kroening

src/ebmc/output_verilog.cpp

@@ -910,7 +910,7 @@ void output_verilog_baset::invariants(const symbolt &symbol)
   assert(symbol.value.id()==ID_trans &&
          symbol.value.operands().size()==3);
 
-  invariant(symbol.value.op0());
+  invariant(to_ternary_expr(symbol.value).op0());
 }
 
 /*******************************************************************\

src/trans-netlist/instantiate_netlist.cpp

@@ -227,22 +227,22 @@ literalt instantiate_bmc_mapt::convert_bool(const exprt &expr)
       unsigned old_next=next;
       literalt result;
 
-      if(expr.op1().is_nil())
+      if(to_ternary_expr(expr).op1().is_nil())
       {
         mp_integer offset;
-        if(to_integer_non_constant(expr.op0(), offset))
+        if(to_integer_non_constant(to_ternary_expr(expr).op0(), offset))
           throw "failed to convert sva_cycle_delay offset";
 
         current = old_current + offset.to_ulong();
         next = old_next + offset.to_ulong();
-        result=convert_bool(expr.op2());
+        result = convert_bool(to_ternary_expr(expr).op2());
       }
       else
       {
         mp_integer from, to;
         if(
-          to_integer_non_constant(expr.op0(), from) ||
-          to_integer_non_constant(expr.op1(), to))
+          to_integer_non_constant(to_ternary_expr(expr).op0(), from) ||
+          to_integer_non_constant(to_ternary_expr(expr).op1(), to))
         {
           throw "failed to convert sva_cycle_delay offsets";
         }
@@ -254,7 +254,7 @@ literalt instantiate_bmc_mapt::convert_bool(const exprt &expr)
         {
           current = old_current + offset.to_ulong();
           next = old_next + offset.to_ulong();
-          disjuncts.push_back(convert_bool(expr.op2()));
+          disjuncts.push_back(convert_bool(to_ternary_expr(expr).op2()));
         }
 
         result=prop.lor(disjuncts);

src/trans-word-level/instantiate_word_level.cpp

@@ -150,34 +150,34 @@ void wl_instantiatet::instantiate_rec(exprt &expr)
       // save the current time frame, we'll change it
       save_currentt save_current(current);
 
-      if(expr.op1().is_nil())
+      if(to_ternary_expr(expr).op1().is_nil())
       {
         mp_integer offset;
-        if(to_integer_non_constant(expr.op0(), offset))
+        if(to_integer_non_constant(to_ternary_expr(expr).op0(), offset))
           throw "failed to convert sva_cycle_delay offset";
 
         current = save_current.saved + offset.to_ulong();
 
         // Do we exceed the bound? Make it 'true'
         if(current>=no_timeframes)
-          expr.op2()=true_exprt();
+          to_ternary_expr(expr).op2() = true_exprt();
         else
-          instantiate_rec(expr.op2());
+          instantiate_rec(to_ternary_expr(expr).op2());
 
-        expr=expr.op2();
+        expr = to_ternary_expr(expr).op2();
       }
       else
       {
         mp_integer from, to;
-        if(to_integer_non_constant(expr.op0(), from))
+        if(to_integer_non_constant(to_ternary_expr(expr).op0(), from))
           throw "failed to convert sva_cycle_delay offsets";
-          
-        if(expr.op1().id()==ID_infinity)
+
+        if(to_ternary_expr(expr).op1().id() == ID_infinity)
         {
           assert(no_timeframes!=0);
           to=no_timeframes-1;
         }
-        else if(to_integer_non_constant(expr.op1(), to))
+        else if(to_integer_non_constant(to_ternary_expr(expr).op1(), to))
           throw "failed to convert sva_cycle_delay offsets";
 
         // This is an 'or', and we let it fail if the bound is too small.
@@ -193,7 +193,7 @@ void wl_instantiatet::instantiate_rec(exprt &expr)
           }
           else
           {
-            disjuncts.push_back(expr.op2());
+            disjuncts.push_back(to_ternary_expr(expr).op2());
             instantiate_rec(disjuncts.back());
           }
         }

src/verilog/expr2verilog.cpp

@@ -98,7 +98,7 @@ Function: expr2verilogt::convert_sva_cycle_delay
 \*******************************************************************/
 
 std::string expr2verilogt::convert_sva_cycle_delay(
-  const exprt &src,
+  const ternary_exprt &src,
   unsigned precedence)
 {
   if(src.operands().size()!=3)
@@ -1003,7 +1003,7 @@ std::string expr2verilogt::convert(
     // not sure about precedence
 
   else if(src.id()==ID_sva_cycle_delay)
-    return convert_sva_cycle_delay(src, precedence=0);
+    return convert_sva_cycle_delay(to_ternary_expr(src), precedence = 0);
     // not sure about precedence
 
   else if(src.id()==ID_sva_sequence_concatenation)

src/verilog/expr2verilog_class.h

@@ -9,6 +9,7 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_VERILOG_EXPR2VERILOG_H
 #define CPROVER_VERILOG_EXPR2VERILOG_H
 
+#include <util/bitvector_expr.h>
 #include <util/std_expr.h>
 
 class expr2verilogt
@@ -91,7 +92,7 @@ class expr2verilogt
   virtual std::string convert_with(const with_exprt &, unsigned precedence);
 
   virtual std::string
-  convert_sva_cycle_delay(const exprt &, unsigned precedence);
+  convert_sva_cycle_delay(const ternary_exprt &, unsigned precedence);
 
   virtual std::string
   convert_sva_sequence_concatenation(const binary_exprt &, unsigned precedence);

src/verilog/verilog_typecheck_expr.cpp

@@ -286,7 +286,7 @@ void verilog_typecheck_exprt::convert_expr(exprt &expr)
      case 0: convert_nullary_expr(expr); break;
      case 1: convert_unary_expr  (to_unary_expr(expr)); break;
      case 2: convert_binary_expr (to_binary_expr(expr)); break;
-     case 3: convert_trinary_expr(static_cast<ternary_exprt &>(expr)); break;
+     case 3: convert_trinary_expr(to_ternary_expr(expr)); break;
      default:
       error().source_location=expr.source_location();
       error() << "no conversion for expression " << expr.id() << eom;