From 240fdea43de18f2163db80d3144170dc73877343 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Thu, 21 Mar 2024 17:15:46 +0100 Subject: [PATCH] Update json example --- rsc/extra/worker_json_example.json | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) diff --git a/rsc/extra/worker_json_example.json b/rsc/extra/worker_json_example.json index 7e62a2e95e..b422e2040a 100644 --- a/rsc/extra/worker_json_example.json +++ b/rsc/extra/worker_json_example.json @@ -5,16 +5,13 @@ "type 'a set\n\nlogic empty : 'a set\nlogic add : 'a , 'a set -> 'a set\n\\logic mem : 'a , 'a set -> prop\n\naxiom mem_empty:\n forall x : 'a.\n not mem(x, empty : 'a set)\n\naxiom mem_add:\n forall x, y : 'a. forall s : 'a set.\n mem(x, add(y, s)) <->\n (x = y or mem(x, s))\n\nlogic is1, is2 : int set\nlogic iss : int set set\n\ngoal g_4:\n is1 = is2 -> \n (not mem(1, add(2+3, empty : int set))) and\n mem (is1, add (is2, iss)) " } +// TODO: update this example // Example of Json file that represent all options that can be set in the worker : { - "debug": false, "debug_ac": false, "debug_adt": false, - "debug_arith": false, "debug_arrays": false, "debug_bitv": false, - "debug_cc": false, "debug_combine": false, "debug_constr": false, + "debug": false, "debug_constr": false, "debug_explanations": false, "debug_fm": false, "debug_fpa": 0, - "debug_gc": false, "debug_interpretation": false, "debug_ite": false, - "debug_matching": 0, "debug_sat": false, "debug_split": false, - "debug_sum": false, "debug_triggers": false, "debug_types": false, - "debug_typing": false, "debug_uf": false, "debug_unsat_core": false, + "debug_gc": false, "debug_interpretation": false, + "debug_split": false, "debug_types": false, "debug_unsat_core": false, "debug_use": false, "debug_warnings": false, "rule": 0, "case_split_policy": "AfterTheoryAssume", "enable_adts_cs": false, "max_split": 0, "replay": false, "replay_all_used_context": false,