Commit ad063ef7 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Fix verifythis_2016_matrix_multiplication and add it to the bench.

parent 9e6dacc7
......@@ -85,63 +85,14 @@ theory Matrix
lemma set_def1,
lemma set_def2,
lemma set_def3,
lemma set_def4
lemma set_def4,
axiom rows_and_cols_nonnegative,
axiom extensionality
use import int.Int
end
theory FixedMatrix
use import int.Int
constant r: int
constant c: int
type mat 'a
function rows (mat 'a) : int = r
function cols (mat 'a) : int = c
axiom r_and_c_nonnegative:
0 <= r /\ 0 <= c
clone export MatrixGen with
type mat 'a = mat 'a,
function rows = rows,
function cols = cols,
goal rows_and_cols_nonnegative
use HighOrd
function create (f: int -> int -> 'a) : mat 'a
axiom create_get:
forall f: int -> int -> 'a, i j: int.
0 <= i < r -> 0 <= j < c -> get (create f) i j = f i j
end
theory SquareFixedMatrix
use import int.Int
constant d: int
axiom dimension_nonnegative:
0 <= d
clone export FixedMatrix with
function r = d,
function c = d,
goal r_and_c_nonnegative
end
(* theory Square_Matrix = Matrix with axiom rows_and_cols_nonnegative:
forall m: mat 'a. 0 <= rows m /\ 0 <= cols m /\ rows m = cols m *)
module MatrixArithmetic
use import int.Int
......
......@@ -5,8 +5,6 @@
<prover id="1" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.5" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../matrices.mlw" proved="true">
<theory name="MatrixGen" proved="true">
</theory>
<theory name="Matrix" proved="true">
<goal name="set_def1" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="10"/></proof>
......@@ -21,16 +19,6 @@
<proof prover="1"><result status="valid" time="0.00" steps="22"/></proof>
</goal>
</theory>
<theory name="FixedMatrix" proved="true">
<goal name="rows_and_cols_nonnegative" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
</theory>
<theory name="SquareFixedMatrix" proved="true">
<goal name="r_and_c_nonnegative" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
</theory>
<theory name="MatrixArithmetic" proved="true">
<goal name="zero_neutral" proved="true">
<transf name="split_goal_right" proved="true" >
......
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