Skip to content

Commit

Permalink
Update json example
Browse files Browse the repository at this point in the history
  • Loading branch information
Halbaroth committed Mar 22, 2024
1 parent fcaa34c commit 240fdea
Showing 1 changed file with 4 additions and 7 deletions.
11 changes: 4 additions & 7 deletions rsc/extra/worker_json_example.json
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down

0 comments on commit 240fdea

Please sign in to comment.