Implement the symbolic case of eval_rvalue_discriminant

1 files changed, 11 insertions, 2 deletions

diff --git a/src/Synthesis.ml b/src/Synthesis.ml
index f3cc5f91..9ce6c8da 100644
--- a/src/Synthesis.ml
+++ b/src/Synthesis.ml
@@ -26,11 +26,20 @@ open InterpreterUtils
  *   `s := op1 + op2`
  * *)
 
-(** TODO: rename to synthesize_symbolic_expansion_{non_enum,one_variant}? *)
-let synthesize_symbolic_expansion (sv : V.symbolic_value)
+(** Synthesize code for a symbolic expansion which doesn't lead to branching
+    (i.e., applied on a value which is not an enumeration with several variants).
+ *)
+let synthesize_symbolic_expansion_no_branching (sv : V.symbolic_value)
     (see : symbolic_expansion) : unit =
   ()
 
+(** Synthesize code for a symbolic expansion which leads to branching
+    (for instance when evaluating the discriminant of a symbolic value).
+ *)
+let synthesize_symbolic_expansion_branching (sv : V.symbolic_value)
+    (seel : symbolic_expansion list) : unit =
+  ()
+
 let synthesize_unary_op (unop : E.unop) (op : V.typed_value)
     (dest : V.symbolic_value) : unit =
   ()