Commit daf92378 authored by Clément Fumex's avatar Clément Fumex

In a driver, add the possibility to remove all the locally defined

axioms with a single "remove allprops".

use remove allprops in the driver for bitvectors.
parent 955ddf6f
......@@ -4,67 +4,19 @@
theory bv.BV64
syntax converter of_int "(_ bv%1 64)"
syntax function to_uint "(bv2nat %1)"
remove prop to_uint_of_int
remove prop to_uint_extensionality
remove prop to_uint_bounds
remove prop to_uint_add
remove prop to_uint_sub
remove prop to_uint_neg
remove prop to_uint_mul
remove prop to_uint_udiv
remove prop to_uint_urem
remove prop to_uint_lsr
remove prop to_uint_lsl
end
theory bv.BV32
syntax converter of_int "(_ bv%1 32)"
syntax function to_uint "(bv2nat %1)"
remove prop to_uint_of_int
remove prop to_uint_extensionality
remove prop to_uint_bounds
remove prop to_uint_add
remove prop to_uint_sub
remove prop to_uint_neg
remove prop to_uint_mul
remove prop to_uint_udiv
remove prop to_uint_urem
remove prop to_uint_lsr
remove prop to_uint_lsl
end
theory bv.BV16
syntax converter of_int "(_ bv%1 16)"
syntax function to_uint "(bv2nat %1)"
remove prop to_uint_of_int
remove prop to_uint_extensionality
remove prop to_uint_bounds
remove prop to_uint_add
remove prop to_uint_sub
remove prop to_uint_neg
remove prop to_uint_mul
remove prop to_uint_udiv
remove prop to_uint_urem
remove prop to_uint_lsr
remove prop to_uint_lsl
end
theory bv.BV8
syntax converter of_int "(_ bv%1 8)"
syntax function to_uint "(bv2nat %1)"
remove prop to_uint_of_int
remove prop to_uint_extensionality
remove prop to_uint_bounds
remove prop to_uint_add
remove prop to_uint_sub
remove prop to_uint_neg
remove prop to_uint_mul
remove prop to_uint_udiv
remove prop to_uint_urem
remove prop to_uint_lsr
remove prop to_uint_lsl
end
......@@ -20,26 +20,7 @@ theory bv.BV_Gen
syntax function asr_bv "(bvashr %1 %2)"
syntax predicate eq "(= %1 %2)"
remove prop nth_out_of_bound
remove prop Nth_zero
remove prop Nth_ones
remove prop two_power_size_val
remove prop max_int_val
remove prop eq_sub_equiv
remove prop Extensionality
remove prop Nth_bw_or
remove prop Nth_bw_and
remove prop Nth_bw_xor
remove prop Nth_bw_not
remove prop Nth_rotate_left
remove prop Nth_rotate_right
remove prop Nth_bv_is_nth
remove prop Lsr_nth_low
remove prop Lsr_nth_high
remove prop Asr_nth_low
remove prop Asr_nth_high
remove prop Lsl_nth_low
remove prop Lsl_nth_high
remove allprops
syntax predicate ult "(bvult %1 %2)"
syntax predicate ule "(bvule %1 %2)"
......@@ -107,8 +88,7 @@ theory bv.BV8
end
theory bv.BVConverter_Gen
remove prop toSmall_to_uint
remove prop toBig_to_uint
remove allprops
end
theory bv.BVConverter_32_64
......@@ -142,75 +122,5 @@ theory bv.BVConverter_8_16
end
theory bv.Pow2int
remove prop Power_0
remove prop Power_s
remove prop Power_1
remove prop Power_sum
remove prop pow2pos
remove prop pow2_0
remove prop pow2_1
remove prop pow2_2
remove prop pow2_3
remove prop pow2_4
remove prop pow2_5
remove prop pow2_6
remove prop pow2_7
remove prop pow2_8
remove prop pow2_9
remove prop pow2_10
remove prop pow2_11
remove prop pow2_12
remove prop pow2_13
remove prop pow2_14
remove prop pow2_15
remove prop pow2_16
remove prop pow2_17
remove prop pow2_18
remove prop pow2_19
remove prop pow2_20
remove prop pow2_21
remove prop pow2_22
remove prop pow2_23
remove prop pow2_24
remove prop pow2_25
remove prop pow2_26
remove prop pow2_27
remove prop pow2_28
remove prop pow2_29
remove prop pow2_30
remove prop pow2_31
remove prop pow2_32
remove prop pow2_33
remove prop pow2_34
remove prop pow2_35
remove prop pow2_36
remove prop pow2_37
remove prop pow2_38
remove prop pow2_39
remove prop pow2_40
remove prop pow2_41
remove prop pow2_42
remove prop pow2_43
remove prop pow2_44
remove prop pow2_45
remove prop pow2_46
remove prop pow2_47
remove prop pow2_48
remove prop pow2_49
remove prop pow2_50
remove prop pow2_51
remove prop pow2_52
remove prop pow2_53
remove prop pow2_54
remove prop pow2_55
remove prop pow2_56
remove prop pow2_57
remove prop pow2_58
remove prop pow2_59
remove prop pow2_60
remove prop pow2_61
remove prop pow2_62
remove prop pow2_63
remove prop pow2_64
remove allprops
end
......@@ -28,7 +28,7 @@ transformation "eliminate_epsilon"
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification"*)
(* Prepare for counter-example query: get rid of some quantifiers (makes it
(* Prepare for counter-example query: get rid of some quantifiers (makes it
possible to query model values of the variables in premises) and introduce
counter-example projections *)
transformation "prepare_for_counterexmp"
......@@ -82,67 +82,19 @@ end
theory bv.BV64
syntax converter of_int "((_ int2bv 64) %1)"
syntax function to_uint "(bv2int %1)"
remove prop to_uint_of_int
remove prop to_uint_extensionality
remove prop to_uint_bounds
remove prop to_uint_add
remove prop to_uint_sub
remove prop to_uint_neg
remove prop to_uint_mul
remove prop to_uint_udiv
remove prop to_uint_urem
remove prop to_uint_lsr
remove prop to_uint_lsl
end
theory bv.BV32
syntax converter of_int "((_ int2bv 32) %1)"
syntax function to_uint "(bv2int %1)"
remove prop to_uint_of_int
remove prop to_uint_extensionality
remove prop to_uint_bounds
remove prop to_uint_add
remove prop to_uint_sub
remove prop to_uint_neg
remove prop to_uint_mul
remove prop to_uint_udiv
remove prop to_uint_urem
remove prop to_uint_lsr
remove prop to_uint_lsl
end
theory bv.BV16
syntax converter of_int "((_ int2bv 16) %1)"
syntax function to_uint "(bv2int %1)"
remove prop to_uint_of_int
remove prop to_uint_extensionality
remove prop to_uint_bounds
remove prop to_uint_add
remove prop to_uint_sub
remove prop to_uint_neg
remove prop to_uint_mul
remove prop to_uint_udiv
remove prop to_uint_urem
remove prop to_uint_lsr
remove prop to_uint_lsl
end
theory bv.BV8
syntax converter of_int "((_ int2bv 8) %1)"
syntax function to_uint "(bv2int %1)"
remove prop to_uint_of_int
remove prop to_uint_extensionality
remove prop to_uint_bounds
remove prop to_uint_add
remove prop to_uint_sub
remove prop to_uint_neg
remove prop to_uint_mul
remove prop to_uint_udiv
remove prop to_uint_urem
remove prop to_uint_lsr
remove prop to_uint_lsl
end
......@@ -7,7 +7,7 @@
<prover id="2" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="3" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<file name="../bitcount.mlw" expanded="true">
<theory name="BitCount8bit_fact" sum="0a9542b8845049b148e46227080d891f">
<theory name="BitCount8bit_fact" sum="c75ce9e432c578193a79df3868b92c50">
<goal name="nth_as_bv_is_int">
<proof prover="0" timelimit="25" memlimit="1000"><result status="valid" time="0.32" steps="118"/></proof>
<proof prover="1" timelimit="25"><result status="valid" time="0.33"/></proof>
......@@ -86,7 +86,7 @@
<proof prover="2"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="WP_parameter step2.5.5" expl="5. assertion">
<proof prover="1" timelimit="25"><result status="valid" time="15.65"/></proof>
<proof prover="1" timelimit="25"><result status="valid" time="17.54"/></proof>
</goal>
</transf>
</goal>
......@@ -177,7 +177,7 @@
</transf>
</goal>
</theory>
<theory name="BitCount32bit_fact" sum="7fdd50eb80427905b5fb8d3c73c0432e">
<theory name="BitCount32bit_fact" sum="7fe1723c3933d65064c895efddfb876f" expanded="true">
<goal name="WP_parameter step1" expl="VC for step1">
<transf name="split_goal_wp">
<goal name="WP_parameter step1.1" expl="1. assertion">
......@@ -262,7 +262,7 @@
<proof prover="3" timelimit="20"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="WP_parameter step2.5.5" expl="5. assertion">
<proof prover="1" timelimit="20"><result status="valid" time="5.22"/></proof>
<proof prover="1" timelimit="20"><result status="valid" time="5.92"/></proof>
</goal>
</transf>
</goal>
......@@ -357,7 +357,6 @@
<goal name="WP_parameter step3.7.6" expl="6. assertion">
<proof prover="0" timelimit="20" memlimit="1000"><result status="valid" time="0.03" steps="90"/></proof>
<proof prover="1" timelimit="20"><result status="valid" time="0.02"/></proof>
<proof prover="3" timelimit="20"><result status="valid" time="2.57"/></proof>
</goal>
<goal name="WP_parameter step3.7.7" expl="7. assertion">
<proof prover="1" timelimit="20"><result status="valid" time="0.23"/></proof>
......@@ -368,7 +367,7 @@
</transf>
</goal>
<goal name="WP_parameter step3.8" expl="8. postcondition">
<proof prover="2" timelimit="20"><result status="valid" time="0.20"/></proof>
<proof prover="2" timelimit="20"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="WP_parameter step3.9" expl="9. postcondition">
<proof prover="0" timelimit="20" memlimit="1000"><result status="valid" time="0.46" steps="171"/></proof>
......@@ -377,8 +376,8 @@
</goal>
</transf>
</goal>
<goal name="WP_parameter step4" expl="VC for step4">
<transf name="split_goal_wp">
<goal name="WP_parameter step4" expl="VC for step4" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter step4.1" expl="1. precondition">
<transf name="split_goal_wp">
<goal name="WP_parameter step4.1.1" expl="1. VC for step4">
......@@ -401,7 +400,7 @@
<proof prover="2" timelimit="20"><result status="valid" time="0.05"/></proof>
<proof prover="3" timelimit="20"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter step4.3" expl="3. precondition">
<goal name="WP_parameter step4.3" expl="3. precondition" expanded="true">
<proof prover="0" timelimit="20" memlimit="1000"><result status="valid" time="0.04" steps="75"/></proof>
<proof prover="1" timelimit="20"><result status="valid" time="0.04"/></proof>
<proof prover="2" timelimit="20"><result status="valid" time="0.03"/></proof>
......@@ -447,8 +446,8 @@
<proof prover="2" timelimit="20"><result status="valid" time="0.03"/></proof>
<proof prover="3" timelimit="20"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter step4.9" expl="9. assertion">
<transf name="split_goal_wp">
<goal name="WP_parameter step4.9" expl="9. assertion" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter step4.9.1" expl="1. assertion">
<proof prover="0" timelimit="20" memlimit="1000"><result status="valid" time="0.11" steps="143"/></proof>
<proof prover="1" timelimit="20"><result status="valid" time="0.37"/></proof>
......@@ -460,19 +459,17 @@
<proof prover="1" timelimit="20"><result status="valid" time="2.90"/></proof>
<proof prover="2" timelimit="20"><result status="valid" time="0.13"/></proof>
</goal>
<goal name="WP_parameter step4.9.4" expl="4. assertion">
<goal name="WP_parameter step4.9.4" expl="4. assertion" expanded="true">
<proof prover="0" timelimit="20" memlimit="1000"><result status="valid" time="0.06" steps="90"/></proof>
<proof prover="1" timelimit="20"><result status="valid" time="0.05"/></proof>
<proof prover="3" timelimit="20"><result status="valid" time="5.05"/></proof>
</goal>
<goal name="WP_parameter step4.9.5" expl="5. assertion">
<proof prover="2" timelimit="20"><result status="valid" time="0.08"/></proof>
<proof prover="3" timelimit="20"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter step4.9.6" expl="6. assertion">
<goal name="WP_parameter step4.9.6" expl="6. assertion" expanded="true">
<proof prover="0" timelimit="20" memlimit="1000"><result status="valid" time="0.05" steps="91"/></proof>
<proof prover="1" timelimit="20"><result status="valid" time="0.06"/></proof>
<proof prover="3" timelimit="20"><result status="valid" time="1.55"/></proof>
</goal>
<goal name="WP_parameter step4.9.7" expl="7. assertion">
<proof prover="1" timelimit="20"><result status="valid" time="0.51"/></proof>
......@@ -610,7 +607,7 @@
</transf>
</goal>
</theory>
<theory name="Hamming" sum="d2e0fa2839f0ea7f837e2de931961eca" expanded="true">
<theory name="Hamming" sum="f58ac4e32def3758c49cf4ca64ad01d8">
<goal name="WP_parameter hammingD" expl="VC for hammingD">
<transf name="split_goal_wp">
<goal name="WP_parameter hammingD.1" expl="1. assertion">
......@@ -622,7 +619,7 @@
</transf>
</goal>
<goal name="symmetric">
<proof prover="1" timelimit="20"><result status="valid" time="6.96"/></proof>
<proof prover="1" timelimit="20"><result status="valid" time="7.86"/></proof>
<proof prover="3" timelimit="20"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="numof_ytpmE">
......@@ -657,7 +654,7 @@
<proof prover="2" timelimit="20"><result status="valid" time="0.04"/></proof>
</goal>
</theory>
<theory name="AsciiCode" sum="2355b20157d5f66a9c56cab2c9c206e8" expanded="true">
<theory name="AsciiCode" sum="0f11e672ebddf479fb932b64c9e6c843" expanded="true">
<goal name="WP_parameter bv_even" expl="VC for bv_even">
<transf name="split_goal_wp">
<goal name="WP_parameter bv_even.1" expl="1. assertion">
......@@ -778,7 +775,7 @@
<proof prover="0"><result status="valid" time="0.02" steps="71"/></proof>
</goal>
<goal name="WP_parameter tmp.3" expl="3. postcondition" expanded="true">
<proof prover="2" timelimit="30"><result status="valid" time="18.28"/></proof>
<proof prover="2" timelimit="30"><result status="valid" time="23.99"/></proof>
</goal>
<goal name="WP_parameter tmp.4" expl="4. postcondition" expanded="true">
<proof prover="0"><result status="valid" time="1.44" steps="572"/></proof>
......@@ -789,7 +786,7 @@
<proof prover="0" memlimit="1000"><result status="valid" time="0.27" steps="240"/></proof>
</goal>
</theory>
<theory name="GrayCode" sum="84dd0ed6aa73f35416328e1c3f203705" expanded="true">
<theory name="GrayCode" sum="08e01c52536014ef570bfe551bad657b" expanded="true">
<goal name="iso" expanded="true">
</goal>
<goal name="WP_parameter grayIsGray" expl="VC for grayIsGray" expanded="true">
......
......@@ -7,7 +7,7 @@
<prover id="2" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="3" name="Z3" version="4.3.2" timelimit="5" memlimit="1000"/>
<file name="../bitvector_examples.mlw" expanded="true">
<theory name="Test_proofinuse" sum="6fb94f39a17f6d336d37a4eb24fc9921" expanded="true">
<theory name="Test_proofinuse" sum="bd0fd6bbcea5b5adc03536c5e643efb1" expanded="true">
<goal name="WP_parameter shift_is_div" expl="VC for shift_is_div" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter shift_is_div.1" expl="1. assertion" expanded="true">
......@@ -103,7 +103,7 @@
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
</theory>
<theory name="Hackers_delight_mod" sum="df93f6196fe77d1d941fdbcbcaace732" expanded="true">
<theory name="Hackers_delight_mod" sum="a496501341c99e842ff5afc76bf4e611" expanded="true">
<goal name="WP_parameter dm1" expl="VC for dm1" expanded="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
......@@ -172,7 +172,7 @@
<proof prover="2"><result status="valid" time="0.07"/></proof>
</goal>
</theory>
<theory name="Test_imperial_violet" sum="0916a7dc63483a6d85503c2aea8ed311" expanded="true">
<theory name="Test_imperial_violet" sum="02f8456e7087c14a7dce80467987dec3" expanded="true">
<goal name="bv32_bounds_bv" expanded="true">
<proof prover="0"><result status="valid" time="0.13" steps="144"/></proof>
<proof prover="1"><result status="valid" time="0.25"/></proof>
......@@ -199,7 +199,7 @@
<proof prover="1"><result status="valid" time="0.95"/></proof>
</goal>
</theory>
<theory name="Test_from_bitvector_example" sum="69d7af24e60703d28350a145d0e363f9" expanded="true">
<theory name="Test_from_bitvector_example" sum="10570a298afc58c4a36facbd4f2facd5" expanded="true">
<goal name="Test1" expanded="true">
<proof prover="0"><result status="valid" time="0.14" steps="101"/></proof>
<proof prover="1"><result status="valid" time="0.22"/></proof>
......@@ -247,7 +247,7 @@
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter lsr29" expl="VC for lsr29" expanded="true">
<proof prover="1"><result status="valid" time="0.52"/></proof>
<proof prover="1"><result status="valid" time="0.36"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
......
......@@ -8,7 +8,7 @@
<prover id="3" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="1.00.prv" timelimit="5" memlimit="1000"/>
<file name="../bitwalker.mlw" expanded="true">
<theory name="Bitwalker" sum="04c17077c9393556d197378eef4ec2fc" expanded="true">
<theory name="Bitwalker" sum="d4430f5ae75e998e1d531d208d35f01e" expanded="true">
<goal name="nth64">
<proof prover="0"><result status="valid" time="0.10" steps="135"/></proof>
<proof prover="3"><result status="valid" time="0.46"/></proof>
......@@ -5820,7 +5820,7 @@
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter poke_64bit_bv.5" expl="5. VC for poke_64bit_bv">
<proof prover="1"><result status="valid" time="0.20"/></proof>
<proof prover="1"><result status="valid" time="0.08"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="WP_parameter poke_64bit_bv.6" expl="6. VC for poke_64bit_bv">
......@@ -5828,7 +5828,7 @@
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter poke_64bit_bv.7" expl="7. VC for poke_64bit_bv">
<proof prover="1"><result status="valid" time="0.20"/></proof>
<proof prover="1"><result status="valid" time="0.08"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter poke_64bit_bv.8" expl="8. VC for poke_64bit_bv">
......@@ -6272,7 +6272,7 @@
</goal>
<goal name="WP_parameter poke.22.3" expl="3. assertion">
<proof prover="0"><result status="valid" time="0.13" steps="102"/></proof>
<proof prover="1"><result status="valid" time="0.23"/></proof>
<proof prover="1"><result status="valid" time="0.10"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.12"/></proof>
</goal>
......@@ -6304,7 +6304,7 @@
</goal>
<goal name="WP_parameter poke.27" expl="27. loop invariant preservation">
<proof prover="0"><result status="valid" time="1.20" steps="128"/></proof>
<proof prover="2"><result status="valid" time="0.25"/></proof>
<proof prover="2"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="WP_parameter poke.28" expl="28. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.42" steps="122"/></proof>
......
......@@ -10,14 +10,14 @@
<file name="../hackers-delight.mlw" expanded="true">
<theory name="Utils" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="Utils_Spec" sum="3f0ae9505cd1d20116a2836d82f8ab3d" expanded="true">
<theory name="Utils_Spec" sum="48173d335d17e665b5bf6ed0b7333c02" expanded="true">
<goal name="countZero">
<proof prover="1"><result status="valid" time="0.03"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="numOfZero">
<proof prover="0"><result status="valid" time="0.47" steps="239"/></proof>
<proof prover="3"><result status="valid" time="0.33"/></proof>
<proof prover="3"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="countStep">
<proof prover="1" timelimit="30"><result status="valid" time="4.95"/></proof>
......@@ -30,14 +30,14 @@
<goal name="WP_parameter countSpec_Aux" expl="VC for countSpec_Aux">
<transf name="split_goal_wp">
<goal name="WP_parameter countSpec_Aux.1" expl="1. postcondition">
<proof prover="0"><result status="valid" time="0.47" steps="265"/></proof>
<proof prover="0"><result status="valid" time="0.03" steps="86"/></proof>
<proof prover="1"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.28"/></proof>
<proof prover="3"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="WP_parameter countSpec_Aux.2" expl="2. variant decrease">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.41"/></proof>
<proof prover="3"><result status="valid" time="0.66"/></proof>
</goal>
<goal name="WP_parameter countSpec_Aux.3" expl="3. assertion">
<transf name="split_goal_wp">
......@@ -69,7 +69,7 @@
<goal name="WP_parameter hamming_spec" expl="VC for hamming_spec" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter hamming_spec.1" expl="1. assertion" expanded="true">
<proof prover="0"><result status="valid" time="2.43" steps="944"/></proof>
<proof prover="0"><result status="valid" time="2.43" steps="956"/></proof>
<proof prover="3"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="WP_parameter hamming_spec.2" expl="2. postcondition">
......@@ -83,7 +83,7 @@
</goal>
<goal name="separation">
<proof prover="1"><result status="valid" time="0.19"/></proof>
<proof prover="2"><result status="valid" time="0.52"/></proof>
<proof prover="2"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="WP_parameter numof_or" expl="VC for numof_or">
<proof prover="1"><result status="valid" time="0.53"/></proof>
......@@ -93,8 +93,8 @@
<goal name="WP_parameter triangleInequalityInt" expl="VC for triangleInequalityInt" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter triangleInequalityInt.1" expl="1. assertion" expanded="true">
<proof prover="2" timelimit="70"><result status="valid" time="0.77"/></proof>
<proof prover="4"><result status="valid" time="0.75"/></proof>
<proof prover="2" timelimit="70"><result status="valid" time="1.34"/></proof>
<proof prover="4"><result status="valid" time="1.31"/></proof>
</goal>
<goal name="WP_parameter triangleInequalityInt.2" expl="2. postcondition" expanded="true">
<proof prover="0"><result status="valid" time="0.05" steps="79"/></proof>
......@@ -107,14 +107,14 @@
<proof prover="1" timelimit="15"><result status="valid" time="2.35"/></proof>
</goal>
</theory>
<theory name="Hackers_delight" sum="c1471f5279d8e24b7242c18b19325bf4" expanded="true">
<theory name="Hackers_delight" sum="144a5949c45c6cffa10ffc47afc51177" expanded="true">
<goal name="WP_parameter ascii" expl="VC for ascii">
<proof prover="1"><result status="valid" time="0.09"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="asciiProp">
<proof prover="1" timelimit="20"><result status="valid" time="0.66"/></proof>
<proof prover="2" timelimit="20"><result status="valid" time="2.72"/></proof>
<proof prover="2" timelimit="20"><result status="valid" time="1.69"/></proof>
</goal>
<goal name="iso">
<proof prover="1"><result status="valid" time="0.43"/></proof>
......
......@@ -20,7 +20,7 @@
</theory>
<theory name="BitsSpec" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="Bits" sum="89d1f7f114f012f8e0dea70cfcddc67e">
<theory name="Bits" sum="6cd5db16655631752af29773c65bc6c2">
<goal name="WP_parameter empty" expl="VC for empty">
<proof prover="0"><result status="valid" time="0.03" steps="80"/></proof>
<proof prover="1"><result status="valid" time="0.06"/></proof>
......@@ -31,7 +31,7 @@
</goal>
<goal name="WP_parameter remove_singleton" expl="VC for remove_singleton">
<proof prover="0"><result status="valid" time="0.90" steps="668"/></proof>
<proof prover="1"><result status="valid" time="1.73"/></proof>
<proof prover="1"><result status="valid" time="2.29"/></proof>
</goal>
<goal name="WP_parameter add_singleton" expl="VC for add_singleton">
<proof prover="1"><result status="valid" time="1.17"/></proof>
......@@ -127,7 +127,7 @@
<proof prover="1"><result status="valid" time="1.52"/></proof>
</goal>
</theory>
<theory name="NQueensBits" sum="3a6aea3add6d6b05881981ce9401f001" expanded="true">
<theory name="NQueensBits" sum="cfb4c367c0c6e2b8f7d6a8cce009c9e4" expanded="true">
<goal name="WP_parameter t" expl="VC for t" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter t.1" expl="1. assertion" expanded="true">
......@@ -2192,7 +2192,7 @@
</goal>
<goal name="WP_parameter t.19" expl="19. assertion">
<proof prover="0"><result status="valid" time="0.25" steps="156"/></proof>
<proof prover="1"><result status="valid" time="1.29"/></proof>
<proof prover="1"><result status="valid" time="0.87"/></proof>
<proof prover="3"><result status="valid" time="0.11"/></proof>
<proof prover="4"><result status="valid" time="0.04"/></proof>
</goal>
......@@ -2208,7 +2208,7 @@
<goal name="WP_parameter t.22" expl="22. assertion">
<transf name="split_goal_wp">
<goal name="WP_parameter t.22.1" expl="1. assertion">
<proof prover="1" timelimit="30"><result status="valid" time="4.35"/></proof>
<proof prover="1" timelimit="30"><result status="valid" time="5.89"/></proof>
<proof prover="3" timelimit="30"><result status="valid" time="0.31"/></proof>
<proof prover="4" timelimit="30"><result status="valid" time="0.87"/></proof>
</goal>
......@@ -2334,7 +2334,7 @@
<proof prover="4"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="WP_parameter t.45" expl="45. loop invariant preservation">
<proof prover="1"><result status="valid" time="1.22"/></proof>
<proof prover="1"><result status="valid" time="0.97"/></proof>
<proof prover="3"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="WP_parameter t.46" expl="46. loop invariant preservation">
......
......@@ -154,6 +154,12 @@ let load_driver = let driver_tag = ref (-1) in fun env file extra_files ->
| Rremovepr (q) ->
let td = remove_prop (find_pr th q) in
add_meta th td meta
| Rremoveall ->
let it key _ = match (Mid.find key th.th_known).d_node with
| Dprop (_,symb,_) -> add_meta th (remove_prop symb) meta
| _ -> ()
in
Mid.iter it th.th_local
| Rconverter (q,s,b) ->
let cs = syntax_converter (find_ls th q) s b in
add_meta th cs meta
......
......@@ -33,6 +33,7 @@ type th_rule =
| Rsyntaxps of qualid * string * bool
| Rconverter of qualid * string * bool
| Rremovepr of qualid
| Rremoveall
| Rmeta of string * metarg list
type theory_rules = {
......
......@@ -47,6 +47,7 @@
"predicate", PREDICATE;
"type", TYPE;
"prop", PROP;
"allprops", ALL;
"filename", FILENAME;
"transformation", TRANSFORM;
"plugin", PLUGIN;
......
......@@ -28,7 +28,7 @@
%token UNDERSCORE LEFTPAR RIGHTPAR DOT QUOTE EOF
%token BLACKLIST
%token MODULE EXCEPTION VAL CONVERTER
%token FUNCTION PREDICATE TYPE PROP FILENAME TRANSFORM PLUGIN
%token FUNCTION PREDICATE TYPE PROP ALL FILENAME TRANSFORM PLUGIN
%token LEFTPAR_STAR_RIGHTPAR COMMA CONSTANT
%token LEFTSQ RIGHTSQ LARROW
......@@ -90,6 +90,7 @@ trule:
| syntax PREDICATE qualid STRING { Rsyntaxps ($3, $4, $1) }
| syntax CONVERTER qualid STRING { Rconverter ($3, $4, $1) }
| REMOVE PROP qualid { Rremovepr ($3) }
| REMOVE ALL { Rremoveall }
| META ident meta_args { Rmeta ($2, $3) }
| META STRING meta_args { Rmeta ($2, $3) }
......
......@@ -116,7 +116,13 @@ let load_driver env file extra_files =
| Rconverter _ ->
Loc.errorm "Syntax converter cannot be used in pure theories"
| Rremovepr (q) ->
ignore (find_pr th q)
ignore (find_pr th q)
| Rremoveall ->
let it key _ = match (Mid.find key th.th_known).Decl.d_node with
| Decl.Dprop (_,symb,_) -> ignore symb
| _ -> ()
in
Mid.iter it th.th_local
| Rmeta (s,al) ->
let rec ty_of_pty = function
| PTyvar x ->
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment