effect pass disable flag

bin/main.ml

@@ -5,15 +5,15 @@ open Tv_sanity.Solver_pipeline
 open Tv_sanity.Utilities
 
 (** Parse and process a single SMT-LIB2 file with main pipeline *)
-let process_file filename timeout_ms =
+let process_file filename timeout_ms optimise_effects =
   try
     let state = parse_file filename in
     let base_filename = Filename.remove_extension filename in
 
     (* Create debug directory if in debug mode *)
     (if is_debug_enabled () then ignore (create_debug_directory (Filename.basename base_filename)));
 
-    let _ = optimize_with_z3_tactics state timeout_ms base_filename in
+    let _ = optimize_with_z3_tactics state timeout_ms optimise_effects base_filename in
     true
   with
   | exn ->
@@ -26,12 +26,15 @@ let () =
   (* Command line argument variables *)
   let timeout_ms = ref 30000 in  (* Default 30 second timeout *)
   let input_files = ref [] in
+  let effect_optimiser = ref true in
 
   (* Argument specification *)
   let spec = [
     ("--debug", Arg.Unit (fun () -> set_debug_mode true),
      " Enable debug mode with debug directory creation");
-    ("--timeout", Arg.Int (fun t -> timeout_ms := t),
+    ("--no-effect", Arg.Clear effect_optimiser,
+     "disable effect optimiser");
+    ("--timeout", Arg.Set_int timeout_ms,
      "<timeout_ms> Timeout in milliseconds for solver operations (default: 30000)");
   ] in
 
@@ -50,7 +53,7 @@ let () =
       Arg.usage spec usage_msg;
       exit 1
   | [filename] ->
-      if process_file filename !timeout_ms then exit 0 else exit 1
+      if process_file filename !timeout_ms !effect_optimiser then exit 0 else exit 1
   | _ ->
       Printf.printf "Error: Too many input files specified\n";
       Arg.usage spec usage_msg;

lib/program_parser.ml

@@ -457,9 +457,9 @@ let process_program program state =
   (program,effs)
 
 let order_effects effects effs =
-  List.map (fun effect ->
-    match StringMap.find_opt effect.qname effs with
-    | Some (preds,source,target) -> { effect with preds ; source_location = Some source ; target_location = Some target }
+  List.map (fun ef ->
+    match StringMap.find_opt ef.qname effs with
+    | Some (preds,source,target) -> { ef with preds ; source_location = Some source ; target_location = Some target }
     | None -> failwith "missing effect")  effects
 
 let join_effs a b =

lib/solver_pipeline.ml

@@ -112,10 +112,13 @@ let inject_synth_pc_disjunctions_in_state state =
   { state with arbitrary = state.arbitrary @ [initial_vars;final_vars] }
 
 (** Main function for Z3 tactic + CVC5 workflow *)
-let optimize_with_z3_tactics state timeout_ms base_filename =
-  let cvc_time = 30000 in
+let optimize_with_z3_tactics state timeout_ms optimise_effects base_filename =
+  let cvc_time = timeout_ms in
   debug_printf "Starting Effect Optimization...\n";
-  let (state,time) = get_time (fun () -> Effect_optimizer.optimize_queries_to_fixpoint state timeout_ms base_filename) in
+  let (state,time) = if optimise_effects then 
+    get_time (fun () -> Effect_optimizer.optimize_queries_to_fixpoint state timeout_ms base_filename)
+    else (get_time (fun () -> state))
+    in
   debug_printf "Finished Effect Optimization in %.2fms\n" time;
   debug_printf "Starting Simplification...\n";
   let (split,time) = get_time (fun () ->

readme.txt

@@ -0,0 +1,3 @@
+
+
+- [used with z3 4.13](https://lazamar.co.uk/nix-versions/?package=z3&version=4.13.4&fullName=z3-4.13.4&keyName=z3&revision=c5dd43934613ae0f8ff37c59f61c507c2e8f980d&channel=nixpkgs-unstable#instructions)