Permalink
Browse files

Add handy mk_sum2, mk_sub2, mk_mul2

And fix behavior of mk_sum, mk_sub, mk_mul for zero-length array
  • Loading branch information...
polazarus committed Nov 29, 2013
1 parent b0b379d commit 5a41c4d81bd1b1de2ab9e62f9ef3e60840dc3c1e
Showing with 120 additions and 9 deletions.
  1. +58 −0 test/specific.ml
  2. +62 −9 yices.idl
View
@@ -115,6 +115,29 @@ let test_mk_nor test_ctxt =
Yices.assert_simple ctx (Yices.mk_nor ctx [|f;f;f;f;f;f|]);
assert_equal Yices.True (Yices.check ctx)
let test_mk_sum2 test_ctxt =
let ctx = bracket_mk_context test_ctxt in
let n = Yices.mk_num ctx in
Yices.assert_simple ctx (Yices.mk_eq ctx (n 3) (Yices.mk_sum2 ctx (n 1) (n 2)));
Yices.assert_simple ctx (Yices.mk_eq ctx (n (-2)) (Yices.mk_sum2 ctx (n 0) (n (-2))));
assert_equal Yices.True (Yices.check ctx)
let test_mk_sub2 test_ctxt =
let ctx = bracket_mk_context test_ctxt in
let n = Yices.mk_num ctx in
Yices.assert_simple ctx (Yices.mk_eq ctx (n 56) (Yices.mk_sub2 ctx (n 81) (n 25)));
Yices.assert_simple ctx (Yices.mk_eq ctx (n (-502)) (Yices.mk_sub2 ctx (n (-2)) (n 500)));
assert_equal Yices.True (Yices.check ctx)
let test_mk_mul2 test_ctxt =
let ctx = bracket_mk_context test_ctxt in
let n = Yices.mk_num ctx in
Yices.assert_simple ctx (Yices.mk_eq ctx (n 952) (Yices.mk_mul2 ctx (n 56) (n 17)));
Yices.assert_simple ctx (Yices.mk_eq ctx (n 0) (Yices.mk_mul2 ctx (n 0) (n 1548)));
assert_equal Yices.True (Yices.check ctx)
(* Empty array tests *)
let test_mk_and_nil test_ctxt =
let ctx = bracket_mk_context test_ctxt in
Yices.assert_simple ctx (Yices.mk_and ctx [||]);
@@ -135,6 +158,35 @@ let test_mk_nor_nil test_ctxt =
Yices.assert_simple ctx (Yices.mk_nor ctx [||]);
assert_equal Yices.True (Yices.check ctx)
let test_mk_sum_nil test_ctxt =
let ctx = bracket_mk_context test_ctxt in
let n = Yices.mk_num ctx in
Yices.assert_simple ctx
(Yices.mk_eq ctx (n 0) (Yices.mk_sum ctx [||]));
assert_equal Yices.True (Yices.check ctx);
Yices.reset ctx;
Yices.assert_simple ctx
(Yices.mk_eq ctx (n 6) (Yices.mk_sum ctx [|n 1;n 2;n 3|]));
assert_equal ~msg:"non-empty array" Yices.True (Yices.check ctx)
let test_mk_sub_nil test_ctxt =
let ctx = bracket_mk_context test_ctxt in
assert_raises (Failure "mk_sub") (fun () -> Yices.mk_sub ctx [||]);
let n = Yices.mk_num ctx in
Yices.assert_simple ctx
(Yices.mk_eq ctx (n 6) (Yices.mk_sub ctx [|n 12;n 1;n 2;n 3|]));
assert_equal ~msg:"non-empty array" Yices.True (Yices.check ctx)
let test_mk_mul_nil test_ctxt =
let ctx = bracket_mk_context test_ctxt in
let n = Yices.mk_num ctx in
Yices.assert_simple ctx
(Yices.mk_eq ctx (n 1) (Yices.mk_mul ctx [||]));
assert_equal Yices.True (Yices.check ctx);
Yices.reset ctx;
Yices.assert_simple ctx
(Yices.mk_eq ctx (n 6) (Yices.mk_sub ctx [|n 12;n 1;n 2;n 3|]));
assert_equal ~msg:"non-empty array" Yices.True (Yices.check ctx)
let tests = [
"mk_and2" >:: test_mk_and2;
@@ -143,10 +195,16 @@ let tests = [
"mk_nand" >:: test_mk_nand;
"mk_nor2" >:: test_mk_nor2;
"mk_nor" >:: test_mk_nor;
"mk_sum2" >:: test_mk_sum2;
"mk_sub2" >:: test_mk_sub2;
"mk_mul2" >:: test_mk_mul2;
"zero-length array" >::: [
"mk_and" >:: test_mk_and_nil;
"mk_or" >:: test_mk_or_nil;
"mk_nand" >:: test_mk_nand_nil;
"mk_nor" >:: test_mk_nor_nil;
"mk_sum" >:: test_mk_sum_nil;
"mk_sub" >:: test_mk_sub_nil;
"mk_mul" >:: test_mk_mul_nil;
];
]
View
@@ -661,8 +661,7 @@ yices_var_decl yices_mk_bool_var_decl(yices_context ctx, [string] const char * n
quote(mli, "(**\n\
[mk_var_decl ctx name type] returns a new (global) variable declaration. It is an error to create two variables\n\
with the same name.\n\
[mk_var_decl ctx name type] returns a new (global) variable declaration. It is an error to create two variables with the same name.\n\
*)")
yices_var_decl yices_mk_var_decl(yices_context ctx, [string] const char * name, yices_type ty);
@@ -741,6 +740,8 @@ quote(mli, "(**\n\
[mk_or ctx args] returns an expression representing the disjunction (i.e. [or]) of the given arguments (as an array).\n\
\n\
{i (Since Ocamlyices 0.8)} If the array's length is 0, returns the expression for [false].\n\
\n\
@before 0.8 if called with a zero-length array, the program exits with a non-null exit cod.\n\
*)")
yices_expr yices_mk_or(yices_context ctx, [size_is(n)] yices_expr args[], unsigned int n) quote(call, "{\n\
_res = n == 0 ? yices_mk_false(ctx) : yices_mk_or(ctx, args, n);\n\
@@ -763,6 +764,8 @@ quote(mli, "(**\n\
[mk_and ctx args] returns an expression representing the conjunction (i.e. [and]) of the given arguments (as an array).\n\
\n\
{i (Since Ocamlyices 0.8)} If the array's length is 0, returns the expression for [true].\n\
\n\
@before 0.8 if called with a zero-length array, the program exits with a non-null exit code.\n\
*)")
yices_expr yices_mk_and(yices_context ctx, [size_is(n)] yices_expr args[], unsigned int n) quote(call, "{\n\
_res = n == 0 ? yices_mk_true(ctx) : yices_mk_and(ctx, args, n);\n\
@@ -921,30 +924,80 @@ yices_expr yices_mk_num_from_string(yices_context ctx, [string] const char * n);
quote(mli, "(**\n\
[mk_sum ctx arr] returns an expression representing [arr.(0) + ... + arr.(n)].\n\
[mk_sum ctx arr] returns an expression representing [arr.(0) + ... + arr.(n)].\n\
If the array's length is zero, returns the expression for zero.\n\
\n\
{b Warning!} [Array.length arr] must be greater than zero.\n\
@before 0.8 the program exists with a non-null exit code if the array's length is zero.\n\
*)")
yices_expr yices_mk_sum(yices_context ctx, [size_is(n), in] yices_expr args[],
unsigned int n);
unsigned int n)
quote(call, "{\n\
_res = (n == 0) ? yices_mk_num(ctx, 0) : yices_mk_sum(ctx, args, n);\n\
}");
quote(mli, "(**\n\
[mk_sum2 ctx a b] returns an expression representing [a + b].\n\
\n\
@since 0.8\n\
*)")
yices_expr yices_mk_sum2(yices_context ctx, yices_expr a, yices_expr b)
quote(call, "{\n\
yices_expr args[2] = { a, b };\n\
_res = yices_mk_sum(ctx, args, 2);\n\
}");
quote(mli, "(**\n\
[mk_sub ctx arr] returns an expression representing [arr.(0) - ... - arr.(n)].\n\
\n\
{b Warning!} [Array.length arr] must be greater than zero.\n\
@raise Failure if the array's lenth is zero.\n\
@before 0.8 the program exists with a non-null exit code if the array's length is zero.\n\
*)")
yices_expr yices_mk_sub(yices_context ctx, [size_is(n), in] yices_expr args[],
unsigned int n);
unsigned int n)
quote(call, "{\n\
if (n==0) caml_failwith(\"mk_sub\");\n\
_res = yices_mk_sub(ctx, args, n);\n\
}");
quote(mli, "(**\n\
[mk_sub2 ctx a b] returns an expression representing [a - b].\n\
\n\
@since 0.8\n\
*)")
yices_expr yices_mk_sub2(yices_context ctx, yices_expr a, yices_expr b)
quote(call, "{\n\
yices_expr args[2] = { a, b };\n\
_res = yices_mk_sub(ctx, args, 2);\n\
}");
quote(mli, "(**\n\
[mk_mul ctx arr] returns an expression representing [arr.(0) * ... * arr.(n)].\n\
[mk_mul ctx arr] returns an expression representing [arr.(0) * ... * arr.(n)].\n\
If the array's length is zero, returns the expression for zero.\n\
\n\
{b Warning!} [Array.length arr] must be greater than zero.\n\
@before 0.8 the program exists with a non-null exit code if the array's length is zero.\n\
*)")
yices_expr yices_mk_mul(yices_context ctx, [size_is(n), in] yices_expr args[],
unsigned int n);
unsigned int n)
quote(call, "{\n\
_res = (n == 0) ? yices_mk_num(ctx, 1) : yices_mk_mul(ctx, args, n);\n\
}");
quote(mli, "(**\n\
[mk_mul2 ctx a b] returns an expression representing [a * b].\n\
\n\
@since 0.8\n\
*)")
yices_expr yices_mk_mul2(yices_context ctx, yices_expr a, yices_expr b)
quote(call, "{\n\
yices_expr args[2] = { a, b };\n\
_res = yices_mk_mul(ctx, args, 2);\n\
}");
quote(mli, "(**\n\

0 comments on commit 5a41c4d

Please sign in to comment.