[Toss-devel-svn] SF.net SVN: toss:[1675] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
[Toss-devel-svn] SF.net SVN: toss:[1675] trunk/Toss
|
From: <luk...@us...> - 2012-02-13 03:07:28
|
Revision: 1675
http://toss.svn.sourceforge.net/toss/?rev=1675&view=rev
Author: lukaszkaiser
Date: 2012-02-13 03:07:19 +0000 (Mon, 13 Feb 2012)
Log Message:
-----------
Integrating the num library, tests update in RealQuantElim.
Modified Paths:
--------------
trunk/Toss/Formula/Sat/Makefile
trunk/Toss/Makefile
trunk/Toss/Server/Tests.ml
trunk/Toss/Solver/RealQuantElim/Makefile
trunk/Toss/Solver/RealQuantElim/OrderedPoly.ml
trunk/Toss/Solver/RealQuantElim/OrderedPoly.mli
trunk/Toss/Solver/RealQuantElim/Poly.ml
trunk/Toss/Solver/RealQuantElim/SignTable.ml
Added Paths:
-----------
trunk/Toss/Solver/Num/
trunk/Toss/Solver/Num/Integers.ml
trunk/Toss/Solver/Num/Integers.mli
trunk/Toss/Solver/Num/IntegersTest.ml
trunk/Toss/Solver/Num/Makefile
trunk/Toss/Solver/Num/MiscNum.ml
trunk/Toss/Solver/Num/MiscNum.mli
trunk/Toss/Solver/Num/Naturals.ml
trunk/Toss/Solver/Num/NaturalsTest.ml
trunk/Toss/Solver/Num/Numbers.ml
trunk/Toss/Solver/Num/Numbers.mli
trunk/Toss/Solver/Num/NumbersTest.ml
trunk/Toss/Solver/Num/Rationals.ml
trunk/Toss/Solver/Num/Rationals.mli
trunk/Toss/Solver/Num/RationalsTest.ml
trunk/Toss/Solver/RealQuantElim/OrderedPolySetTest.ml
trunk/Toss/Solver/RealQuantElim/OrderedPolyTest.ml
trunk/Toss/Solver/RealQuantElim/PolyTest.ml
trunk/Toss/Solver/RealQuantElim/RealQuantElimTest.ml
trunk/Toss/Solver/RealQuantElim/SignTableTest.ml
Removed Paths:
-------------
trunk/Toss/Solver/RealQuantElim/N.ml
trunk/Toss/Solver/RealQuantElim/TestOrderedPoly.ml
trunk/Toss/Solver/RealQuantElim/TestOrderedPolySet.ml
trunk/Toss/Solver/RealQuantElim/TestPoly.ml
trunk/Toss/Solver/RealQuantElim/TestRealQuantElim.ml
trunk/Toss/Solver/RealQuantElim/TestSignTable.ml
Modified: trunk/Toss/Formula/Sat/Makefile
===================================================================
--- trunk/Toss/Formula/Sat/Makefile 2012-02-11 22:40:58 UTC (rev 1674)
+++ trunk/Toss/Formula/Sat/Makefile 2012-02-13 03:07:19 UTC (rev 1675)
@@ -1,20 +1,6 @@
-MINISATDIR = minisat
+all: tests
-all: SatSolver.o MiniSATWrap.o
-
-SatSolver.o: $(MINISATDIR)/Solver.C
- if [ ! -e minisat/SatSolver.o ]; then \
- g++ -O2 -fPIC -c -I $(MINISATDIR) $(MINISATDIR)/Solver.C -o SatSolver.o; \
- mv SatSolver.o minisat/; \
- fi
-
-MiniSATWrap.o: MiniSATWrap.C
- if [ ! -e minisat/MiniSATWrap.o ]; then \
- g++ -O2 -fPIC -c -I /usr/lib/ocaml -I $(MINISATDIR) MiniSATWrap.C; \
- mv MiniSATWrap.o minisat/; \
- fi
-
%Test:
make -C ../.. Formula/Sat/$@
@@ -25,4 +11,3 @@
clean:
rm -f *.cma *.cmi *~ *.cmxa *.cmx *.a *.annot Sat.cmxa SatTest
rm -f *.o *.cmo *.cmo *.cmi *~ *.cma *.cmo *.a *.annot
- rm -f minisat/SatSolver.o minisat/MiniSATWrap.o
Modified: trunk/Toss/Makefile
===================================================================
--- trunk/Toss/Makefile 2012-02-11 22:40:58 UTC (rev 1674)
+++ trunk/Toss/Makefile 2012-02-13 03:07:19 UTC (rev 1675)
@@ -59,15 +59,16 @@
FormulaINCSatINC=MenhirLib,Formula
FormulaINC=MenhirLib,Formula,Formula/Sat,Formula/Sat/dpll
-SolverINC=MenhirLib,Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim
-ArenaINC=MenhirLib,Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver
-PlayINC=MenhirLib,Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver,Arena
-LearnINC=MenhirLib,Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver,Arena
-GGPINC=MenhirLib,Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver,Arena,Play
-ClientINC=MenhirLib,Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver,Arena,Play
-ServerINC=MenhirLib,Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver,Arena,Play,GGP,Learn
+SolverINC=MenhirLib,Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver/Num
+SolverINCRealQuantElimINC=MenhirLib,Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver/Num
+ArenaINC=MenhirLib,Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver/Num,Solver
+PlayINC=MenhirLib,Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver/Num,Solver,Arena
+LearnINC=MenhirLib,Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver/Num,Solver,Arena
+GGPINC=MenhirLib,Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver/Num,Solver,Arena,Play
+ClientINC=MenhirLib,Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver/Num,Solver,Arena,Play
+ServerINC=MenhirLib,Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver/Num,Solver,Arena,Play,GGP,Learn
-.INC=MenhirLib,Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver,Arena,Play,GGP,Learn,Server
+.INC=MenhirLib,Formula,Formula/Sat,Formula/Sat/dpll,Solver/RealQuantElim,Solver/Num,Solver,Arena,Play,GGP,Learn,Server
%.native: %.ml caml_extensions/pa_let_try.cmo caml_extensions/pa_log.cmo
$(OCAMLBUILD) -Is $($(subst /,INC,$(dir $@))) $@
Modified: trunk/Toss/Server/Tests.ml
===================================================================
--- trunk/Toss/Server/Tests.ml 2012-02-11 22:40:58 UTC (rev 1674)
+++ trunk/Toss/Server/Tests.ml 2012-02-13 03:07:19 UTC (rev 1675)
@@ -13,6 +13,10 @@
]
let solver_tests = "Solver", [
+ "NaturalsTest", [NaturalsTest.tests];
+ "IntegersTest", [IntegersTest.tests];
+ "RationalsTest", [RationalsTest.tests];
+ "NumbersTest", [NumbersTest.tests];
"StructureTest", [StructureTest.tests];
"AssignmentsTest", [AssignmentsTest.tests];
"SolverTest", [SolverTest.tests; SolverTest.bigtests];
Added: trunk/Toss/Solver/Num/Integers.ml
===================================================================
--- trunk/Toss/Solver/Num/Integers.ml (rev 0)
+++ trunk/Toss/Solver/Num/Integers.ml 2012-02-13 03:07:19 UTC (rev 1675)
@@ -0,0 +1,406 @@
+(***********************************************************************)
+(* *)
+(* Objective Caml *)
+(* *)
+(* Valerie Menissier-Morain, projet Cristal, INRIA Rocquencourt *)
+(* *)
+(* Copyright 1996 Institut National de Recherche en Informatique et *)
+(* en Automatique. All rights reserved. This file is distributed *)
+(* under the terms of the GNU Library General Public License, with *)
+(* the special exception on linking. *)
+(* *)
+(***********************************************************************)
+
+
+open MiscNum
+open Naturals.N
+
+type big_int =
+ { sign : int;
+ abs_value : nat }
+
+let create_big_int sign nat =
+ if sign = 1 || sign = -1 ||
+ (sign = 0 && is_zero_nat nat 0 (num_digits_nat nat))
+ then { sign = sign;
+ abs_value = nat }
+ else invalid_arg "create_big_int"
+
+(* Sign of a big_int *)
+let sign_big_int bi = bi.sign
+
+let zero_big_int =
+ { sign = 0;
+ abs_value = make_nat 1 }
+
+let unit_big_int =
+ { sign = 1;
+ abs_value = nat_of_int 1 }
+
+(* Number of digits in a big_int *)
+let num_digits_big_int bi = num_digits_nat (bi.abs_value)
+
+(* Opposite of a big_int *)
+let minus_big_int bi =
+ { sign = - bi.sign;
+ abs_value = copy_nat (bi.abs_value) 0 (num_digits_big_int bi)}
+
+(* Absolute value of a big_int *)
+let abs_big_int bi =
+ { sign = if bi.sign = 0 then 0 else 1;
+ abs_value = copy_nat (bi.abs_value) 0 (num_digits_big_int bi)}
+
+(* Comparison operators on big_int *)
+
+(*
+ compare_big_int (bi, bi2) = sign of (bi-bi2)
+ i.e. 1 if bi > bi2
+ 0 if bi = bi2
+ -1 if bi < bi2
+*)
+let compare_big_int bi1 bi2 =
+ if bi1.sign = 0 && bi2.sign = 0 then 0
+ else if bi1.sign < bi2.sign then -1
+ else if bi1.sign > bi2.sign then 1
+ else if bi1.sign = 1 then
+ compare_nat (bi1.abs_value) (bi2.abs_value)
+ else
+ compare_nat (bi2.abs_value) (bi1.abs_value)
+
+let eq_big_int bi1 bi2 = compare_big_int bi1 bi2 = 0
+and le_big_int bi1 bi2 = compare_big_int bi1 bi2 <= 0
+and ge_big_int bi1 bi2 = compare_big_int bi1 bi2 >= 0
+and lt_big_int bi1 bi2 = compare_big_int bi1 bi2 < 0
+and gt_big_int bi1 bi2 = compare_big_int bi1 bi2 > 0
+
+let max_big_int bi1 bi2 = if lt_big_int bi1 bi2 then bi2 else bi1
+and min_big_int bi1 bi2 = if gt_big_int bi1 bi2 then bi2 else bi1
+
+(* Operations on big_int *)
+
+let add_big_int bi1 bi2 =
+ let size_bi1 = num_digits_big_int bi1
+ and size_bi2 = num_digits_big_int bi2 in
+ if bi1.sign = bi2.sign
+ then (* Add absolute values if signs are the same *)
+ { sign = bi1.sign;
+ abs_value =
+ match compare_nat (bi1.abs_value) (bi2.abs_value) with
+ -1 -> let res = create_nat (succ size_bi2) in
+ (blit_nat res 0 (bi2.abs_value) 0 size_bi2;
+ set_digit_nat res size_bi2 0;
+ add_nat res (bi1.abs_value);
+ res)
+ |_ -> let res = create_nat (succ size_bi1) in
+ (blit_nat res 0 (bi1.abs_value) 0 size_bi1;
+ set_digit_nat res size_bi1 0;
+ add_nat res (bi2.abs_value);
+ res)}
+
+ else (* Subtract absolute values if signs are different *)
+ match compare_nat (bi1.abs_value) (bi2.abs_value) with
+ | 0 -> zero_big_int
+ | 1 -> { sign = bi1.sign;
+ abs_value = let res = copy_nat (bi1.abs_value) 0 size_bi1 in
+ sub_nat res (bi2.abs_value);
+ res }
+ | _ -> { sign = bi2.sign;
+ abs_value = let res = copy_nat (bi2.abs_value) 0 size_bi2 in
+ sub_nat res (bi1.abs_value);
+ res }
+
+(* Coercion with int type *)
+let big_int_of_int i =
+ { sign = sign_int i;
+ abs_value =
+ let res = (create_nat 1)
+ in (if i = monster_int
+ then (set_digit_nat res 0 biggest_int;
+ incr_nat res)
+ else set_digit_nat res 0 (abs i));
+ res }
+
+let big_int_of_nat nat =
+ let length = num_digits_nat nat in
+ { sign = if is_zero_nat nat 0 length then 0 else 1;
+ abs_value = copy_nat nat 0 length }
+
+let add_int_big_int i bi = add_big_int (big_int_of_int i) bi
+
+let sub_big_int bi1 bi2 = add_big_int bi1 (minus_big_int bi2)
+
+(* Returns i * bi *)
+let mult_int_big_int i bi =
+ let size_bi = num_digits_big_int bi in
+ let size_res = succ size_bi in
+ if i = monster_int
+ then let res = create_nat size_res in
+ blit_nat res 0 (bi.abs_value) 0 size_bi;
+ set_digit_nat res size_bi 0;
+ mult_digit_nat res (bi.abs_value) (biggest_int);
+ { sign = - (sign_big_int bi);
+ abs_value = res }
+ else let res = make_nat (size_res) in
+ mult_digit_nat res (bi.abs_value) (abs i);
+ { sign = (sign_int i) * (sign_big_int bi);
+ abs_value = res }
+
+let mult_big_int bi1 bi2 =
+ let size_bi1 = num_digits_big_int bi1
+ and size_bi2 = num_digits_big_int bi2 in
+ let size_res = size_bi1 + size_bi2 in
+ let res = make_nat (size_res) in
+ { sign = bi1.sign * bi2.sign;
+ abs_value =
+ if size_bi2 > size_bi1
+ then (mult_nat res (bi2.abs_value) (bi1.abs_value); res)
+ else (mult_nat res (bi1.abs_value) (bi2.abs_value); res)
+ }
+
+(* (quotient, rest) of the euclidian division of 2 big_int *)
+let quomod_big_int bi1 bi2 =
+ if bi2.sign = 0 then raise Division_by_zero
+ else
+ let size_bi1 = num_digits_big_int bi1
+ and size_bi2 = num_digits_big_int bi2 in
+ match compare_nat (bi1.abs_value) (bi2.abs_value) with
+ -1 -> (* 1/2 -> 0, reste 1, -1/2 -> -1, reste 1 *)
+ (* 1/-2 -> 0, reste 1, -1/-2 -> 1, reste 1 *)
+ if bi1.sign >= 0 then
+ (big_int_of_int 0, bi1)
+ else if bi2.sign >= 0 then
+ (big_int_of_int(-1), add_big_int bi2 bi1)
+ else
+ (big_int_of_int 1, sub_big_int bi1 bi2)
+ | 0 -> (big_int_of_int (bi1.sign * bi2.sign), zero_big_int)
+ | _ -> let bi1_negatif = bi1.sign = -1 in
+ let size_q =
+ if bi1_negatif
+ then succ (max (succ (size_bi1 - size_bi2)) 1)
+ else max (succ (size_bi1 - size_bi2)) 1
+ and size_r = succ (max size_bi1 size_bi2)
+ (* r is long enough to contain both quotient and remainder *)
+ (* of the euclidian division *)
+ in
+ (* set up quotient, remainder *)
+ let q = create_nat size_q
+ and r = create_nat size_r in
+ blit_nat r 0 (bi1.abs_value) 0 size_bi1;
+ set_to_zero_nat r size_bi1 (size_r - size_bi1);
+
+ (* do the division of |bi1| by |bi2|
+ - at the beginning, r contains |bi1|
+ - at the end, r contains
+ * in the size_bi2 least significant digits, the remainder
+ * in the size_r-size_bi2 most significant digits, the quotient
+ note the conditions for application of div_nat are verified here
+ *)
+ div_nat r (bi2.abs_value);
+
+ (* separate quotient and remainder *)
+ blit_nat q 0 r size_bi2 (size_r - size_bi2);
+ let not_null_mod = not (is_zero_nat r 0 size_bi2) in
+
+ (* correct the signs, adjusting the quotient and remainder *)
+ if bi1_negatif && not_null_mod
+ then
+ (* bi1<0, r>0, noting r for (r, size_bi2) the remainder, *)
+ (* we have |bi1|=q * |bi2| + r with 0 < r < |bi2|, *)
+ (* thus -bi1 = q * |bi2| + r *)
+ (* and bi1 = (-q) * |bi2| + (-r) with -|bi2| < (-r) < 0 *)
+ (* thus bi1 = -(q+1) * |bi2| + (|bi2|-r) *)
+ (* with 0 < (|bi2|-r) < |bi2| *)
+ (* so the quotient has for sign the opposite of the bi2'one *)
+ (* and for value q+1 *)
+ (* and the remainder is strictly positive *)
+ (* has for value |bi2|-r *)
+ (let new_r = copy_nat (bi2.abs_value) 0 size_bi2 in
+ (* new_r contains (r, size_bi2) the remainder *)
+ { sign = - bi2.sign;
+ abs_value = (set_digit_nat q (pred size_q) 0;
+ incr_nat q; q) },
+ { sign = 1;
+ abs_value = let rlimit = copy_nat r 0 size_bi2 in
+ sub_nat new_r rlimit;
+ new_r })
+ else
+ (if bi1_negatif then set_digit_nat q (pred size_q) 0;
+ { sign = if is_zero_nat q 0 size_q
+ then 0
+ else bi1.sign * bi2.sign;
+ abs_value = q },
+ { sign = if not_null_mod then 1 else 0;
+ abs_value = copy_nat r 0 size_bi2 })
+
+let div_big_int bi1 bi2 = fst (quomod_big_int bi1 bi2)
+let mod_big_int bi1 bi2 = snd (quomod_big_int bi1 bi2)
+
+let gcd_big_int bi1 bi2 =
+ let size_bi1 = num_digits_big_int bi1
+ and size_bi2 = num_digits_big_int bi2 in
+ if is_zero_nat (bi1.abs_value) 0 size_bi1 then abs_big_int bi2
+ else if is_zero_nat (bi2.abs_value) 0 size_bi2 then
+ { sign = 1;
+ abs_value = bi1.abs_value }
+ else
+ { sign = 1;
+ abs_value =
+ match compare_nat (bi1.abs_value) (bi2.abs_value) with
+ | 0 -> bi1.abs_value
+ | 1 ->
+ let res = copy_nat (bi1.abs_value) 0 size_bi1 in
+ let len = gcd_nat res (bi2.abs_value) in
+ copy_nat res 0 len
+ | _ ->
+ let res = copy_nat (bi2.abs_value) 0 size_bi2 in
+ let len = gcd_nat res (bi1.abs_value) in
+ copy_nat res 0 len
+ }
+
+(* Coercion operators *)
+
+let monster_big_int = big_int_of_int monster_int;;
+
+let monster_nat = monster_big_int.abs_value;;
+
+let is_int_big_int bi =
+ num_digits_big_int bi == 1 &&
+ match compare_nat bi.abs_value monster_nat with
+ | 0 -> bi.sign == -1
+ | -1 -> true
+ | _ -> false;;
+
+let int_of_big_int bi =
+ try let n = int_of_nat bi.abs_value in
+ if bi.sign = -1 then - n else n
+ with Failure _ ->
+ if eq_big_int bi monster_big_int then monster_int
+ else failwith "int_of_big_int";;
+
+(* Coercion with nat type *)
+let nat_of_big_int bi =
+ if bi.sign = -1
+ then failwith "nat_of_big_int"
+ else copy_nat (bi.abs_value) 0 (num_digits_big_int bi)
+
+
+(* Coercion with string type *)
+
+let string_of_big_int bi =
+ if bi.sign = -1
+ then "-" ^ string_of_nat bi.abs_value
+ else string_of_nat bi.abs_value
+
+
+let sys_big_int_of_string_aux s ofs len sgn =
+ if len < 1 then failwith "sys_big_int_of_string";
+ let n = nat_of_string s ofs len in
+ if is_zero_nat n 0 (num_digits_nat n) then zero_big_int
+ else {sign = sgn; abs_value = n}
+;;
+
+let sys_big_int_of_string s ofs len =
+ if len < 1 then failwith "sys_big_int_of_string";
+ match s.[ofs] with
+ | '-' -> sys_big_int_of_string_aux s (ofs+1) (len-1) (-1)
+ | '+' -> sys_big_int_of_string_aux s (ofs+1) (len-1) 1
+ | _ -> sys_big_int_of_string_aux s ofs len 1
+;;
+
+let big_int_of_string s =
+ sys_big_int_of_string s 0 (String.length s)
+
+
+let power_int_positive_int i n =
+ match sign_int n with
+ | 0 -> unit_big_int
+ | -1 -> invalid_arg "power_int_positive_int"
+ | _ -> let nat = power_base_int (abs i) n in
+ { sign = if i >= 0 then sign_int i else
+ if n land 1 = 0 then 1 else -1;
+ abs_value = nat}
+
+(* base_power_big_int compute bi*base^n *)
+let base_power_big_int base n bi =
+ match sign_int n with
+ | 0 -> bi
+ | -1 -> let nat = power_base_int base (-n) in
+ let len_nat = num_digits_nat nat
+ and len_bi = num_digits_big_int bi in
+ if len_bi < len_nat then
+ invalid_arg "base_power_big_int"
+ else if len_bi = len_nat &&
+ compare_digits_nat (bi.abs_value) nat = -1
+ then invalid_arg "base_power_big_int" else
+ let copy = create_nat (succ len_bi) in
+ blit_nat copy 0 (bi.abs_value) 0 len_bi;
+ set_digit_nat copy len_bi 0;
+ div_nat copy nat;
+ if not (is_zero_nat copy 0 len_nat)
+ then invalid_arg "base_power_big_int"
+ else { sign = bi.sign;
+ abs_value = copy_nat copy len_nat 1 }
+ | _ -> let nat = power_base_int base n in
+ let len_nat = num_digits_nat nat
+ and len_bi = num_digits_big_int bi in
+ let new_len = len_bi + len_nat in
+ let res = make_nat new_len in
+ if len_bi > len_nat
+ then mult_nat res (bi.abs_value) nat
+ else mult_nat res nat (bi.abs_value);
+ if is_zero_nat res 0 new_len
+ then zero_big_int
+ else create_big_int (bi.sign) res
+
+
+(* Coercion with float type *)
+
+let float_of_big_int bi =
+ float_of_string (string_of_big_int bi)
+
+
+(* round off of the futur last digit (of the integer represented by the string
+ argument of the function) that is now the previous one.
+ if s contains an integer of the form (10^n)-1
+ then s <- only 0 digits and the result_int is true
+ else s <- the round number and the result_int is false *)
+let round_futur_last_digit s off_set length =
+ let l = pred (length + off_set) in
+ if Char.code(String.get s l) >= Char.code '5'
+ then
+ let rec round_rec l =
+ if l < off_set then true else begin
+ let current_char = String.get s l in
+ if current_char = '9' then
+ (String.set s l '0'; round_rec (pred l))
+ else
+ (String.set s l (Char.chr (succ (Char.code current_char)));
+ false)
+ end
+ in round_rec (pred l)
+ else false
+
+
+(* Approximation with floating decimal point a` la approx_ratio_exp *)
+let approx_big_int prec bi =
+ let len_bi = num_digits_big_int bi in
+ let n =
+ max 0
+ (int_of_big_int (
+ add_int_big_int
+ (-prec)
+ (div_big_int (mult_big_int (big_int_of_int (pred len_bi))
+ (big_int_of_string "963295986"))
+ (big_int_of_string "100000000")))) in
+ let s =
+ string_of_big_int (div_big_int bi (power_int_positive_int 10 n)) in
+ let (sign, off, len) =
+ if String.get s 0 = '-'
+ then ("-", 1, succ prec)
+ else ("", 0, prec) in
+ if (round_futur_last_digit s off (succ prec))
+ then (sign^"1."^(String.make prec '0')^"e"^
+ (string_of_int (n + 1 - off + String.length s)))
+ else (sign^(String.sub s off 1)^"."^
+ (String.sub s (succ off) (pred prec))
+ ^"e"^(string_of_int (n - succ off + String.length s)))
Added: trunk/Toss/Solver/Num/Integers.mli
===================================================================
--- trunk/Toss/Solver/Num/Integers.mli (rev 0)
+++ trunk/Toss/Solver/Num/Integers.mli 2012-02-13 03:07:19 UTC (rev 1675)
@@ -0,0 +1,128 @@
+(** Operations on arbitrary-precision integers, subset of Big_int module. *)
+
+type big_int
+(** The type of big integers. *)
+
+val zero_big_int : big_int
+(** The big integer [0]. *)
+
+val unit_big_int : big_int
+(** The big integer [1]. *)
+
+
+(** {2 Arithmetic operations} *)
+
+val minus_big_int : big_int -> big_int
+(** Unary negation. *)
+
+val abs_big_int : big_int -> big_int
+(** Absolute value. *)
+
+val add_big_int : big_int -> big_int -> big_int
+(** Addition. *)
+
+val add_int_big_int : int -> big_int -> big_int
+(** Addition of a small integer to a big integer. *)
+
+val sub_big_int : big_int -> big_int -> big_int
+(** Subtraction. *)
+
+val mult_big_int : big_int -> big_int -> big_int
+(** Multiplication of two big integers. *)
+
+val mult_int_big_int : int -> big_int -> big_int
+(** Multiplication of a big integer by a small integer *)
+
+val quomod_big_int : big_int -> big_int -> big_int * big_int
+(** Euclidean division of two big integers.
+ The first part of the result is the quotient,
+ the second part is the remainder.
+ Writing [(q,r) = quomod_big_int a b], we have
+ [a = q * b + r] and [0 <= r < |b|].
+ Raise [Division_by_zero] if the divisor is zero. *)
+
+val div_big_int : big_int -> big_int -> big_int
+(** Euclidean quotient of two big integers.
+ This is the first result [q] of [quomod_big_int] (see above). *)
+
+val mod_big_int : big_int -> big_int -> big_int
+(** Euclidean modulus of two big integers.
+ This is the second result [r] of [quomod_big_int] (see above). *)
+
+val gcd_big_int : big_int -> big_int -> big_int
+(** Greatest common divisor of two big integers. *)
+
+
+(** {2 Comparisons and tests} *)
+
+val sign_big_int : big_int -> int
+(** Return [0] if the given big integer is zero,
+ [1] if it is positive, and [-1] if it is negative. *)
+
+val compare_big_int : big_int -> big_int -> int
+(** [compare_big_int a b] returns [0] if [a] and [b] are equal,
+ [1] if [a] is greater than [b], and [-1] if [a] is smaller than [b]. *)
+
+val eq_big_int : big_int -> big_int -> bool
+val le_big_int : big_int -> big_int -> bool
+val ge_big_int : big_int -> big_int -> bool
+val lt_big_int : big_int -> big_int -> bool
+val gt_big_int : big_int -> big_int -> bool
+(** Usual boolean comparisons between two big integers. *)
+
+val max_big_int : big_int -> big_int -> big_int
+(** Return the greater of its two arguments. *)
+
+val min_big_int : big_int -> big_int -> big_int
+(** Return the smaller of its two arguments. *)
+
+val num_digits_big_int : big_int -> int
+(** Return the number of machine words used to store the
+ given big integer. *)
+
+
+(** {2 Conversions to and from strings} *)
+
+val string_of_big_int : big_int -> string
+(** Return the string representation of the given big integer,
+ in decimal (base 10). *)
+
+val big_int_of_string : string -> big_int
+(** Convert a string to a big integer, in decimal.
+ The string consists of an optional [-] or [+] sign,
+ followed by one or several decimal digits. *)
+
+
+(** {2 Conversions to and from other numerical types} *)
+
+val big_int_of_int : int -> big_int
+(** Convert a small integer to a big integer. *)
+
+val big_int_of_nat : Naturals.N.nat -> big_int
+(** Convert a natural to a big integer. *)
+
+val is_int_big_int : big_int -> bool
+(** Test whether the given big integer is small enough to
+ be representable as a small integer (type [int])
+ without loss of precision. On a 32-bit platform,
+ [is_int_big_int a] returns [true] if and only if
+ [a] is between 2{^30} and 2{^30}-1. On a 64-bit platform,
+ [is_int_big_int a] returns [true] if and only if
+ [a] is between -2{^62} and 2{^62}-1. *)
+
+val int_of_big_int : big_int -> int
+(** Convert a big integer to a small integer (type [int]).
+ Raises [Failure "int_of_big_int"] if the big integer
+ is not representable as a small integer. *)
+
+val float_of_big_int : big_int -> float
+(** Returns a floating-point number approximating the given big integer. *)
+
+
+(** {2 For internal use} *)
+
+val nat_of_big_int : big_int -> Naturals.N.nat
+val approx_big_int: int -> big_int -> string
+val base_power_big_int: int -> int -> big_int -> big_int
+val round_futur_last_digit : string -> int -> int -> bool
+val sys_big_int_of_string: string -> int -> int -> big_int
Added: trunk/Toss/Solver/Num/IntegersTest.ml
===================================================================
--- trunk/Toss/Solver/Num/IntegersTest.ml (rev 0)
+++ trunk/Toss/Solver/Num/IntegersTest.ml 2012-02-13 03:07:19 UTC (rev 1675)
@@ -0,0 +1,491 @@
+open OUnit
+open Integers
+
+let eq_bool (b1, b2) = assert_equal ~printer:string_of_bool b1 b2
+let eq_int (i1, i2) = assert_equal ~printer:string_of_int i1 i2
+let eq_string (s1, s2) = assert_equal ~printer:(fun x -> x) s1 s2
+let eq_big_int (bi1, bi2) = eq_bool (Integers.eq_big_int bi1 bi2, true)
+
+let failwith_test f x except =
+ try let _ = ignore (f x) in eq_string ("worked", "failed") with
+ e -> eq_bool (e = except, true)
+
+let rec gcd_int i1 i2 = if i2 = 0 then abs i1 else gcd_int i2 (i1 mod i2)
+
+let length_of_int = Sys.word_size - 2
+let monster_int = 1 lsl length_of_int
+let biggest_int = monster_int - 1
+let least_int = - biggest_int
+
+let pi_1000_digits =
+"3141592653 :10
+5897932384 :20
+6264338327 :30
+9502884197 :40
+1693993751 :50
+0582097494 :60
+4592307816 :70
+4062862089 :80
+9862803482 :90
+5342117067 :100
+9821480865 :110
+1328230664 :120
+7093844609 :130
+5505822317 :140
+2535940812 :150
+8481117450 :160
+2841027019 :170
+3852110555 :180
+9644622948 :190
+9549303819 :200
+6442881097 :210
+5665933446 :220
+1284756482 :230
+3378678316 :240
+5271201909 :250
+1456485669 :260
+2346034861 :270
+0454326648 :280
+2133936072 :290
+6024914127 :300
+3724587006 :310
+6063155881 :320
+7488152092 :330
+0962829254 :340
+0917153643 :350
+6789259036 :360
+0011330530 :370
+5488204665 :380
+2138414695 :390
+1941511609 :400
+4330572703 :410
+6575959195 :420
+3092186117 :430
+3819326117 :440
+9310511854 :450
+8074462379 :460
+9627495673 :470
+5188575272 :480
+4891227938 :490
+1830119491 :500
+2983367336 :510
+2440656643 :520
+0860213949 :530
+4639522473 :540
+7190702179 :550
+8609437027 :560
+7053921717 :570
+6293176752 :580
+3846748184 :590
+6766940513 :600
+2000568127 :610
+1452635608 :620
+2778577134 :630
+2757789609 :640
+1736371787 :650
+2146844090 :660
+1224953430 :670
+1465495853 :680
+7105079227 :690
+9689258923 :700
+5420199561 :710
+1212902196 :720
+0864034418 :730
+1598136297 :740
+7477130996 :750
+0518707211 :760
+3499999983 :770
+7297804995 :780
+1059731732 :790
+8160963185 :800
+9502445945 :810
+5346908302 :820
+6425223082 :830
+5334468503 :840
+5261931188 :850
+1710100031 :860
+3783875288 :870
+6587533208 :880
+3814206171 :890
+7766914730 :900
+3598253490 :910
+4287554687 :920
+3115956286 :930
+3882353787 :940
+5937519577 :950
+8185778053 :960
+2171226806 :970
+6130019278 :980
+7661119590 :990
+9216420198 :1000
+"
+
+let tests = "Integers" >::: [
+ "compare_big_int" >::
+ (fun () ->
+ eq_int (compare_big_int zero_big_int zero_big_int, 0);
+ eq_int (compare_big_int zero_big_int (big_int_of_int 1), (-1));
+ eq_int (compare_big_int zero_big_int (big_int_of_int (-1)), 1);
+ eq_int (compare_big_int (big_int_of_int 1) zero_big_int, 1);
+ eq_int (compare_big_int (big_int_of_int (-1)) zero_big_int, (-1));
+ eq_int (compare_big_int (big_int_of_int 1) (big_int_of_int 1), 0);
+ eq_int (compare_big_int (big_int_of_int (-1)) (big_int_of_int (-1)), 0);
+ eq_int (compare_big_int (big_int_of_int 1) (big_int_of_int (-1)), 1);
+ eq_int (compare_big_int (big_int_of_int (-1)) (big_int_of_int 1), (-1));
+ eq_int (compare_big_int (big_int_of_int 1) (big_int_of_int 2), (-1));
+ eq_int (compare_big_int (big_int_of_int 2) (big_int_of_int 1), 1);
+ eq_int (compare_big_int (big_int_of_int (-1)) (big_int_of_int (-2)), 1);
+ eq_int (compare_big_int (big_int_of_int (-2)) (big_int_of_int (-1)), -1);
+ );
+
+ "add_big_int" >::
+ (fun () ->
+ eq_big_int (add_big_int zero_big_int zero_big_int, zero_big_int);
+ eq_big_int (add_big_int zero_big_int (big_int_of_int 1),
+ big_int_of_int 1);
+ eq_big_int (add_big_int (big_int_of_int 1) zero_big_int,
+ big_int_of_int 1);
+ eq_big_int (add_big_int zero_big_int (big_int_of_int (-1)),
+ big_int_of_int (-1));
+ eq_big_int (add_big_int (big_int_of_int (-1)) zero_big_int,
+ big_int_of_int (-1));
+ eq_big_int (add_big_int (big_int_of_int 1) (big_int_of_int 1),
+ big_int_of_int 2);
+ eq_big_int (add_big_int (big_int_of_int 1) (big_int_of_int 2),
+ big_int_of_int 3);
+ eq_big_int (add_big_int (big_int_of_int 2) (big_int_of_int 1),
+ big_int_of_int 3);
+ eq_big_int (add_big_int (big_int_of_int (-1)) (big_int_of_int (-1)),
+ big_int_of_int (-2));
+ eq_big_int (add_big_int (big_int_of_int (-1)) (big_int_of_int (-2)),
+ big_int_of_int (-3));
+ eq_big_int (add_big_int (big_int_of_int (-2)) (big_int_of_int (-1)),
+ big_int_of_int (-3));
+ eq_big_int (add_big_int (big_int_of_int 1) (big_int_of_int (-1)),
+ zero_big_int);
+ eq_big_int (add_big_int (big_int_of_int (-1)) (big_int_of_int 1),
+ zero_big_int);
+ eq_big_int (add_big_int (big_int_of_int 1) (big_int_of_int (-2)),
+ big_int_of_int (-1));
+ eq_big_int (add_big_int (big_int_of_int (-2)) (big_int_of_int 1),
+ big_int_of_int (-1));
+ eq_big_int (add_big_int (big_int_of_int (-1)) (big_int_of_int 2),
+ big_int_of_int 1);
+ eq_big_int (add_big_int (big_int_of_int 2) (big_int_of_int (-1)),
+ big_int_of_int 1);
+ );
+
+ "sub_big_int" >::
+ (fun () ->
+ eq_big_int (sub_big_int zero_big_int zero_big_int, zero_big_int);
+ eq_big_int (sub_big_int zero_big_int (big_int_of_int 1),
+ big_int_of_int (-1));
+ eq_big_int (sub_big_int (big_int_of_int 1) zero_big_int,
+ big_int_of_int 1);
+ eq_big_int (sub_big_int zero_big_int (big_int_of_int (-1)),
+ big_int_of_int 1);
+ eq_big_int (sub_big_int (big_int_of_int (-1)) zero_big_int,
+ big_int_of_int (-1));
+ eq_big_int (sub_big_int (big_int_of_int 1) (big_int_of_int 1),
+ zero_big_int);
+ eq_big_int (sub_big_int (big_int_of_int 1) (big_int_of_int 2),
+ big_int_of_int (-1));
+ eq_big_int (sub_big_int (big_int_of_int 2) (big_int_of_int 1),
+ big_int_of_int 1);
+ eq_big_int (sub_big_int (big_int_of_int (-1)) (big_int_of_int (-1)),
+ zero_big_int);
+ eq_big_int (sub_big_int (big_int_of_int (-1)) (big_int_of_int (-2)),
+ big_int_of_int 1);
+ eq_big_int (sub_big_int (big_int_of_int (-2)) (big_int_of_int (-1)),
+ big_int_of_int (-1));
+ eq_big_int (sub_big_int (big_int_of_int 1) (big_int_of_int (-1)),
+ big_int_of_int 2);
+ eq_big_int (sub_big_int (big_int_of_int (-1)) (big_int_of_int 1),
+ big_int_of_int (-2));
+ eq_big_int (sub_big_int (big_int_of_int 1) (big_int_of_int (-2)),
+ big_int_of_int 3);
+ eq_big_int (sub_big_int (big_int_of_int (-2)) (big_int_of_int 1),
+ big_int_of_int (-3));
+ eq_big_int (sub_big_int (big_int_of_int (-1)) (big_int_of_int 2),
+ big_int_of_int (-3));
+ eq_big_int (sub_big_int (big_int_of_int 2) (big_int_of_int (-1)),
+ big_int_of_int 3);
+ );
+
+ "mult_int_big_int" >::
+ (fun () ->
+ eq_big_int (mult_int_big_int 0 (big_int_of_int 3), zero_big_int);
+ eq_big_int (mult_int_big_int 1 (big_int_of_int 3), big_int_of_int 3);
+ eq_big_int (mult_int_big_int 1 zero_big_int, zero_big_int);
+ eq_big_int (mult_int_big_int 2 (big_int_of_int 3), big_int_of_int 6);
+ );
+
+ "mult_big_int" >::
+ (fun () ->
+ eq_big_int (mult_big_int zero_big_int zero_big_int,
+ zero_big_int);
+ eq_big_int (mult_big_int (big_int_of_int 2) (big_int_of_int 3),
+ big_int_of_int 6);
+ eq_big_int (mult_big_int (big_int_of_int 2) (big_int_of_int (-3)),
+ big_int_of_int (-6));
+ eq_big_int (mult_big_int (big_int_of_string "12724951")
+ (big_int_of_string "81749606400"),
+ big_int_of_string "1040259735709286400");
+ eq_big_int (mult_big_int (big_int_of_string "26542080")
+ (big_int_of_string "81749606400"),
+ big_int_of_string "2169804593037312000");
+ );
+
+ "quomod_big_int" >::
+ (fun () ->
+ let (quotient, modulo) =
+ quomod_big_int (big_int_of_int 1) (big_int_of_int 1) in
+ eq_big_int (quotient, big_int_of_int 1);
+ eq_big_int (modulo, zero_big_int);
+
+ let (quotient, modulo) =
+ quomod_big_int (big_int_of_int 1) (big_int_of_int (-1)) in
+ eq_big_int (quotient, big_int_of_int (-1));
+ eq_big_int (modulo, zero_big_int);
+
+ let (quotient, modulo) =
+ quomod_big_int (big_int_of_int (-1)) (big_int_of_int 1) in
+ eq_big_int (quotient, big_int_of_int (-1));
+ eq_big_int (modulo, zero_big_int);
+
+ let (quotient, modulo) =
+ quomod_big_int (big_int_of_int 3) (big_int_of_int 2) in
+ eq_big_int (quotient, big_int_of_int 1);
+ eq_big_int (modulo, big_int_of_int 1);
+
+ let (quotient, modulo) =
+ quomod_big_int (big_int_of_int 5) (big_int_of_int 3) in
+ eq_big_int (quotient, big_int_of_int 1);
+ eq_big_int (modulo, big_int_of_int 2);
+
+ let (quotient, modulo) =
+ quomod_big_int (big_int_of_int (-5)) (big_int_of_int 3) in
+ eq_big_int (quotient, big_int_of_int (-2));
+ eq_big_int (modulo, big_int_of_int 1);
+
+ let (quotient, modulo) =
+ quomod_big_int (big_int_of_int 1) (big_int_of_int 2) in
+ eq_big_int (quotient, zero_big_int);
+ eq_big_int (modulo, big_int_of_int 1);
+
+ let (quotient, modulo) =
+ quomod_big_int (big_int_of_int (-1)) (big_int_of_int 3) in
+ eq_big_int (quotient, minus_big_int unit_big_int);
+ eq_big_int (modulo, big_int_of_int 2);
+
+ failwith_test
+ (quomod_big_int (big_int_of_int 1)) zero_big_int
+ Division_by_zero;
+
+ let (quotient, modulo) =
+ quomod_big_int (big_int_of_int 10) (big_int_of_int 20) in
+ eq_big_int (quotient, big_int_of_int 0);
+ eq_big_int (modulo, big_int_of_int 10);
+
+ let (quotient, modulo) =
+ quomod_big_int (big_int_of_int (-10)) (big_int_of_int 20) in
+ eq_big_int (quotient, big_int_of_int (-1));
+ eq_big_int (modulo, big_int_of_int 10);
+
+ let (quotient, modulo) =
+ quomod_big_int (big_int_of_int 10) (big_int_of_int (-20)) in
+ eq_big_int (quotient, big_int_of_int 0);
+ eq_big_int (modulo, big_int_of_int 10);
+
+ let (quotient, modulo) =
+ quomod_big_int (big_int_of_int (-10)) (big_int_of_int (-20)) in
+ eq_big_int (quotient, big_int_of_int 1);
+ eq_big_int (modulo, big_int_of_int 10);
+ );
+
+ "gcd_big_int" >::
+ (fun () ->
+ eq_big_int (gcd_big_int zero_big_int zero_big_int,
+ zero_big_int);
+ eq_big_int (gcd_big_int zero_big_int (big_int_of_int 1),
+ big_int_of_int 1);
+ eq_big_int (gcd_big_int (big_int_of_int 1) zero_big_int,
+ big_int_of_int 1);
+ eq_big_int (gcd_big_int (big_int_of_int 1) (big_int_of_int 2),
+ big_int_of_int 1);
+ eq_big_int (gcd_big_int (big_int_of_int 2) (big_int_of_int 1),
+ big_int_of_int 1);
+ eq_big_int (gcd_big_int (big_int_of_int 1) (big_int_of_int 1),
+ big_int_of_int 1);
+ eq_big_int (gcd_big_int (big_int_of_int 9) (big_int_of_int 16),
+ big_int_of_int 1);
+ eq_big_int (gcd_big_int (big_int_of_int 12) (big_int_of_int 16),
+ big_int_of_int 4);
+ for i = 9 to 28 do
+ let n1 = Random.int 1000000000
+ and n2 = Random.int 100000 in
+ eq_int
+ (int_of_big_int (gcd_big_int (big_int_of_int n1) (big_int_of_int n2)),
+ gcd_int n1 n2);
+ done;
+ );
+
+ "int_of_big_int" >::
+ (fun () ->
+ eq_int (int_of_big_int (big_int_of_int 1), 1);
+ eq_int (int_of_big_int (big_int_of_int(-1)), -1);
+ eq_int (int_of_big_int zero_big_int, 0);
+ eq_int (int_of_big_int (big_int_of_int max_int), max_int);
+ eq_int (int_of_big_int (big_int_of_int min_int), min_int);
+ failwith_test
+ (fun () -> int_of_big_int (add_big_int (big_int_of_int 1)
+ (big_int_of_int max_int))) ()
+ (Failure "int_of_big_int");
+ failwith_test
+ (fun () -> int_of_big_int (sub_big_int (big_int_of_int 1)
+ (big_int_of_int min_int))) ()
+ (Failure "int_of_big_int");
+ failwith_test
+ (fun () -> int_of_big_int (mult_big_int (big_int_of_int min_int)
+ (big_int_of_int 2))) ()
+ (Failure "int_of_big_int");
+ );
+
+ "is_int_big_int" >::
+ (fun () ->
+ eq_bool (is_int_big_int (big_int_of_int 1), true);
+ eq_bool (is_int_big_int (big_int_of_int (-1)), true);
+ eq_bool (is_int_big_int (add_big_int (big_int_of_int 1)
+ (big_int_of_int biggest_int)),
+ false);
+ eq_int (int_of_big_int (big_int_of_int monster_int), monster_int);
+ eq_bool (is_int_big_int (big_int_of_string (string_of_int biggest_int)),
+ true);
+ eq_bool (is_int_big_int (big_int_of_string (string_of_int least_int)),
+ true);
+ eq_bool (is_int_big_int (big_int_of_string (string_of_int monster_int)),
+ true);
+ eq_bool (is_int_big_int (add_big_int (big_int_of_int 1)
+ (big_int_of_int (biggest_int))),
+ false);
+ eq_bool (is_int_big_int (add_big_int (big_int_of_int 1)
+ (big_int_of_int (biggest_int))),
+ false);
+ eq_bool (is_int_big_int
+ (minus_big_int (big_int_of_string(string_of_int monster_int))),
+ false);
+ );
+
+ "string_of_big_int" >::
+ (fun () ->
+ eq_string (string_of_big_int (big_int_of_int 1), "1");
+ );
+
+ "big_int_of_string" >::
+ (fun () ->
+ eq_big_int (big_int_of_string "1", big_int_of_int 1);
+ eq_big_int (big_int_of_string "-1", big_int_of_int (-1));
+ eq_big_int (big_int_of_string "0", zero_big_int);
+ failwith_test big_int_of_string "sdjdkfighdgf" (Failure "invalid digit");
+ eq_big_int (big_int_of_string "123", big_int_of_int 123);
+ eq_big_int (big_int_of_string "3456", big_int_of_int 3456);
+ eq_big_int (big_int_of_string "-3456", big_int_of_int (-3456));
+
+ let implode = List.fold_left (^) "" in
+ let l = List.rev [
+"174679877494298468451661416292903906557638850173895426081611831060970135303";
+"044177587617233125776581034213405720474892937404345377707655788096850784519";
+"539374048533324740018513057210881137248587265169064879918339714405948322501";
+"445922724181830422326068913963858377101914542266807281471620827145038901025";
+"322784396182858865537924078131032036927586614781817695777639491934361211399";
+"888524140253852859555118862284235219972858420374290985423899099648066366558";
+"238523612660414395240146528009203942793935957539186742012316630755300111472";
+"852707974927265572257203394961525316215198438466177260614187266288417996647";
+"132974072337956513457924431633191471716899014677585762010115338540738783163";
+"739223806648361958204720897858193606022290696766988489073354139289154127309";
+"916985231051926209439373780384293513938376175026016587144157313996556653811";
+"793187841050456120649717382553450099049321059330947779485538381272648295449";
+"847188233356805715432460040567660999184007627415398722991790542115164516290";
+"619821378529926683447345857832940144982437162642295073360087284113248737998";
+"046564369129742074737760485635495880623324782103052289938185453627547195245";
+"688272436219215066430533447287305048225780425168823659431607654712261368560";
+"702129351210471250717394128044019490336608558608922841794819375031757643448";
+"32"
+ ] in
+ let bi1 = big_int_of_string (implode (List.rev l)) in
+ let bi2 = big_int_of_string (implode (List.rev ("3" :: List.tl l))) in
+ eq_big_int (bi1, (add_big_int (mult_big_int bi2 (big_int_of_string "10"))
+ (big_int_of_string "2")));
+ );
+
+ "power_base_int" >::
+ (fun () ->
+ eq_big_int (big_int_of_nat (Naturals.N.power_base_int 10 0),unit_big_int);
+ eq_big_int (big_int_of_nat (Naturals.N.power_base_int 10 8),
+ big_int_of_int 100000000);
+ eq_big_int (big_int_of_nat(Naturals.N.power_base_int 2 (length_of_int+2)),
+ big_int_of_nat (let nat = Naturals.N.make_nat 2 in
+ Naturals.N.set_digit_nat nat 1 1;
+ nat));
+ );
+
+ "base_power_big_int" >::
+ (fun () ->
+ eq_big_int (base_power_big_int 10 0 (big_int_of_int 2), big_int_of_int 2);
+ eq_big_int (base_power_big_int 10 2 (big_int_of_int 2),
+ big_int_of_int 200);
+ eq_big_int (base_power_big_int 10 1 (big_int_of_int 123),
+ big_int_of_int 1230);
+ );
+
+ "pi digits" >::
+ (fun () ->
+ (* Pi digits computed with the streaming algorithm given on pages 4, 6
+ & 7 of "Unbounded Spigot Algorithms for the Digits of Pi", Jeremy
+ Gibbons, August 2004. *)
+ let ( !$ ) = big_int_of_int
+ and ( +$ ) = add_big_int
+ and ( *$ ) = mult_big_int in
+
+ let zero = zero_big_int
+ and one = unit_big_int
+ and three = !$ 3
+ and four = !$ 4
+ and ten = !$ 10
+ and neg_ten = !$(-10) in
+
+ (* Linear Fractional (aka Moebius) Transformations *)
+ let floor_ev (q, r, s, t) x = div_big_int (q *$ x +$ r) (s *$ x +$ t) in
+ let unit = (one, zero, zero, one) in
+ let comp (q, r, s, t) (q', r', s', t') =
+ (q *$ q' +$ r *$ s', q *$ r' +$ r *$ t',
+ s *$ q' +$ t *$ s', s *$ r' +$ t *$ t') in
+
+ let next z = floor_ev z three in
+ let safe z n = Integers.eq_big_int n (floor_ev z four) in
+ let prod z n = comp (ten, neg_ten *$ n, zero, one) z in
+ let cons z k = let den = 2 * k + 1 in
+ comp z (!$ k, !$(2 * den), zero, !$ den) in
+
+ let rec digit k z n row col acc =
+ if n > 0 then
+ let y = next z in
+ if safe z y then
+ if col = 10 then (
+ let row = row + 10 in
+ digit k (prod z y) (n - 1) row 1
+ ((Printf.sprintf "\t:%i\n%s" row (string_of_big_int y)) :: acc)
+ ) else (
+ digit k (prod z y) (n - 1) row (col + 1)
+ ((string_of_big_int y) :: acc)
+ )
+ else digit (k + 1) (cons z k) n row col acc
+ else
+ (Printf.sprintf "%*s\t:%i\n" (10 - col) "" (row + col)) :: acc in
+
+ let digits n = digit 1 unit n 0 0 [] in
+ eq_string (String.concat "" (List.rev (digits 1000)), pi_1000_digits);
+ );
+]
+
+let exec = AuxIO.run_test_if_target "IntegersTest" tests
Added: trunk/Toss/Solver/Num/Makefile
===================================================================
--- trunk/Toss/Solver/Num/Makefile (rev 0)
+++ trunk/Toss/Solver/Num/Makefile 2012-02-13 03:07:19 UTC (rev 1675)
@@ -0,0 +1,15 @@
+all: tests
+
+%Test:
+ make -C ../.. Solver/$@Verbose
+
+NaturalsTest:
+IntegersTest:
+RationalsTest:
+NumbersTest:
+
+.PHONY: clean
+
+clean:
+ make -C .. clean
+ rm -f *~
Added: trunk/Toss/Solver/Num/MiscNum.ml
===================================================================
--- trunk/Toss/Solver/Num/MiscNum.ml (rev 0)
+++ trunk/Toss/Solver/Num/MiscNum.ml 2012-02-13 03:07:19 UTC (rev 1675)
@@ -0,0 +1,45 @@
+(***********************************************************************)
+(* *)
+(* Objective Caml *)
+(* *)
+(* Valerie Menissier-Morain, projet Cristal, INRIA Rocquencourt *)
+(* *)
+(* Copyright 1996 Institut National de Recherche en Informatique et *)
+(* en Automatique. All rights reserved. This file is distributed *)
+(* under the terms of the GNU Library General Public License, with *)
+(* the special exception on linking. *)
+(* *)
+(***********************************************************************)
+
+
+(* Arith flags. *)
+
+let error_when_null_denominator_flag = ref true
+
+let normalize_ratio_flag = ref false
+
+let floating_precision = ref 12
+
+let approx_printing_flag = ref false
+
+
+(* Some extra operations on integers *)
+
+let rec gcd_int i1 i2 =
+ if i2 = 0 then abs i1 else gcd_int i2 (i1 mod i2)
+
+let rec num_bits_int_aux n =
+ if n = 0 then 0 else succ(num_bits_int_aux (n lsr 1))
+
+let num_bits_int n = num_bits_int_aux (abs n)
+
+let sign_int i = if i = 0 then 0 else if i > 0 then 1 else -1
+
+let length_of_int = Sys.word_size - 2
+
+let monster_int = 1 lsl length_of_int
+let biggest_int = monster_int - 1
+let least_int = - biggest_int
+
+let compare_int n1 n2 =
+ if n1 == n2 then 0 else if n1 > n2 then 1 else -1
Added: trunk/Toss/Solver/Num/MiscNum.mli
===================================================================
--- trunk/Toss/Solver/Num/MiscNum.mli (rev 0)
+++ trunk/Toss/Solver/Num/MiscNum.mli 2012-02-13 03:07:19 UTC (rev 1675)
@@ -0,0 +1,20 @@
+(** Numeric support functions from Arith_flags and Int_misc OCaml modules. *)
+
+(** Arith flags. *)
+
+val error_when_null_denominator_flag : bool ref
+val normalize_ratio_flag : bool ref
+val floating_precision : int ref
+val approx_printing_flag : bool ref
+
+
+(** Some extra operations on integers *)
+
+val gcd_int: int -> int -> int
+val num_bits_int: int -> int
+val compare_int: int -> int -> int
+val sign_int: int -> int
+val length_of_int: int
+val biggest_int: int
+val least_int: int
+val monster_int: int
Added: trunk/Toss/Solver/Num/Naturals.ml
===================================================================
--- trunk/Toss/Solver/Num/Naturals.ml (rev 0)
+++ trunk/Toss/Solver/Num/Naturals.ml 2012-02-13 03:07:19 UTC (rev 1675)
@@ -0,0 +1,89 @@
+IFDEF JAVASCRIPT THEN
+module N = (struct
+ type nat = int ref
+
+ let create_nat s = if s > 1 then failwith "MJS" else ref 0
+ let set_to_zero_nat s i1 i2 =
+ if i1 > 1 || i2 > 1 then failwith "MJS" else s := 0
+ let make_nat len =
+ if len < 0 then invalid_arg "make_nat" else
+ let res = create_nat len in set_to_zero_nat res 0 len; res
+
+ let blit_nat n1 i1 n2 i2 i3 =
+ if i1 > 1 || i2 > 1 || i3 > 1 then failwith "MJS" else n1 := !n2
+ let copy_nat nat offset length =
+ if offset > 1 || length > 1 then failwith "MJS" else ref (!nat)
+
+ let set_digit_nat n d x =
+ if d > 1 then failwith "MJS" else n := x
+ let num_digits_nat n = 1
+
+ let is_zero_nat n i1 i2 =
+ if i1 > 1 || i2 > 1 then failwith "MJS" else !n = 0
+ let int_of_nat n = !n
+ let nat_of_int i = ref i
+ let incr_nat n = n := !n + 1
+ let add_nat n x = n := !n + !x
+ let sub_nat n x = n := !n - !x
+ let mult_digit_nat n x i = n := !x * i
+ let mult_nat n x1 x2 = n := !x1 * !x2
+ let div_nat n x = n := !n / !x
+ let compare_digits_nat n m = !n - !m
+ let compare_nat n m = !n - !m
+ let gcd_nat n m = MiscNum.gcd_int !n !m
+ let string_of_nat n = string_of_int !n
+ let nat_of_string s ofs len = ref (int_of_string (String.sub s ofs len))
+ let power_base_int i j = failwith "MJS"
+end)
+ELSE
+module N = (struct
+ type nat = Nat.nat * int (* store number size *)
+
+ let create_nat s = (Nat.create_nat s, s)
+ let set_to_zero_nat (s, l) i1 i2 = Nat.set_to_zero_nat s i1 i2
+ let make_nat len =
+ if len < 0 then invalid_arg "make_nat" else
+ let res = create_nat len in set_to_zero_nat res 0 len; res
+
+ let blit_nat (n1, l1) i1 (n2, l2) i2 i3 = Nat.blit_nat n1 i1 n2 i2 i3
+ let copy_nat nat offset length =
+ let res = create_nat (length) in
+ blit_nat res 0 nat offset length;
+ res
+
+ let set_digit_nat (n, l) d x = Nat.set_digit_nat n d x
+ let num_digits_nat (n, l) =
+ Nat.num_digits_nat n 0 (Nat.length_nat n)
+
+ let is_zero_nat (n, _) i1 i2 = Nat.is_zero_nat n i1 i2
+ let int_of_nat (n, l) = Nat.int_of_nat n
+ let nat_of_int i = (Nat.nat_of_int i, 1)
+ let incr_nat (n, l) = ignore (Nat.incr_nat n 0 l 1)
+
+ let add_nat (n, ln) (x, lx) =
+ (*Nat.add_nat n 0 (Nat.num_digits_nat n) x 0 (Nat.num_digits_nat x) 0*)
+ ignore (Nat.add_nat n 0 ln x 0 lx 0)
+
+ let sub_nat (n, ln) (x, lx) = ignore (Nat.sub_nat n 0 ln x 0 lx 1)
+
+ let mult_digit_nat (n, ln) (x, lx) i =
+ ignore (Nat.mult_digit_nat n 0 ln x 0 lx (Nat.nat_of_int i) 0)
+
+ let mult_nat (n, ln) (x1, l1) (x2, l2) =
+ ignore (Nat.mult_nat n 0 ln x1 0 l1 x2 0 l2)
+
+ let div_nat (n, ln) (x, lx) = Nat.div_nat n 0 ln x 0 lx
+
+ let compare_digits_nat (n, ln) (m, lm) = Nat.compare_digits_nat n ln m lm
+ let compare_nat (n, ln) (m, lm) = Nat.compare_nat n 0 ln m 0 lm
+ let gcd_nat (n, ln) (m, lm) = Nat.gcd_nat n 0 ln m 0 lm
+ let string_of_nat (n, _) = Nat.string_of_nat n
+ let nat_of_string s ofs len =
+ let n = Nat.sys_nat_of_string 10 s ofs len in
+ (n, Nat.num_digits_nat n 0 (Nat.length_nat n))
+
+ let power_base_int i j =
+ let n = Nat.power_base_int i j in
+ (n, Nat.num_digits_nat n 0 (Nat.length_nat n))
+end)
+ENDIF
Added: trunk/Toss/Solver/Num/NaturalsTest.ml
===================================================================
--- trunk/Toss/Solver/Num/NaturalsTest.ml (rev 0)
+++ trunk/Toss/Solver/Num/NaturalsTest.ml 2012-02-13 03:07:19 UTC (rev 1675)
@@ -0,0 +1,94 @@
+open OUnit
+open Naturals.N
+
+let eq_bool (b1, b2) = assert_equal ~printer:string_of_bool b2 b1
+let eq_int (i1, i2) = assert_equal ~printer:string_of_int i2 i1
+let eq_string (s1, s2) = assert_equal ~printer:(fun x -> x) s2 s1
+
+(* Can compare nats less than 2**32 *)
+let equal_nat ?(res=true) (n1, n2) =
+ let eq = (compare_nat n1 n2 = 0) in
+ eq_bool (eq, res)
+
+let rec gcd_int i1 i2 =
+ if i2 = 0 then abs i1 else gcd_int i2 (i1 mod i2)
+
+let nat_of_str s = nat_of_string s 0 (String.length s)
+
+let tests = "Naturals" >::: [
+ "num_digits_nat" >::
+ (fun () ->
+ eq_int (let r = make_nat 2 in
+ set_digit_nat r 1 1;
+ num_digits_nat r, 2);
+ );
+
+ "equal_nat" >::
+ (fun () ->
+ let zero_nat = make_nat 1 in
+ equal_nat (zero_nat, zero_nat);
+ equal_nat (nat_of_int 1, nat_of_int 1);
+ equal_nat (nat_of_str "2", nat_of_str "2");
+ equal_nat ~res:false (nat_of_str "2", nat_of_str "3");
+ );
+
+ "incr_nat" >::
+ (fun () ->
+ let zero = nat_of_int 0 in
+ incr_nat zero;
+ equal_nat (zero, nat_of_int 1);
+
+ let n = nat_of_int 1 in
+ incr_nat n;
+ equal_nat (n, nat_of_int 2);
+ );
+
+ "is_zero_nat" >::
+ (fun () ->
+ let n = nat_of_int 1 in
+ eq_bool (is_zero_nat n 0 1, false);
+ eq_bool (is_zero_nat (make_nat 1) 0 1, true);
+ eq_bool (is_zero_nat (make_nat 2) 0 2, true);
+
+ let r = make_nat 2 in
+ set_digit_nat r 1 1;
+ eq_bool (is_zero_nat r 0 1, true);
+ );
+
+ "string_of_nat && nat_of_string" >::
+ (fun () ->
+ let n = make_nat 4 in
+ eq_string (string_of_nat n, "0");
+
+ for i = 1 to 20 do
+ let s = String.make i '0' in
+ String.set s 0 '1';
+ eq_string (string_of_nat (nat_of_str s), s)
+ done;
+
+ let s = "3333333333333333333333333333333333333333333333333333333333333" ^
+ "3333333333333333333333333333333333333333333333333333333333333333333" ^
+ "33333333" in
+ equal_nat (nat_of_str s,
+ (let nat = make_nat 15 in
+ set_digit_nat nat 0 3;
+ mult_digit_nat nat (nat_of_str (String.sub s 0 135)) 10;
+ nat));
+
+ eq_string (string_of_nat (nat_of_str "1073741824"), "1073741824");
+ );
+
+ "gcd_nat" >::
+ (fun () ->
+ for i = 1 to 20 do
+ let n1 = Random.int 1000000000
+ and n2 = Random.int 100000 in
+ let nat1 = nat_of_int n1
+ and nat2 = nat_of_int n2 in
+ ignore (gcd_nat nat1 nat2);
+ eq_int (int_of_nat nat1, gcd_int n1 n2);
+ done
+ );
+]
+
+let exec = AuxIO.run_test_if_target "NaturalsTest" tests
Added: trunk/Toss/Solver/Num/Numbers.ml
===================================================================
--- trunk/Toss/Solver/Num/Numbers.ml (rev 0)
+++ trunk/Toss/Solver/Num/Numbers.ml 2012-02-13 03:07:19 UTC (rev 1675)
@@ -0,0 +1,300 @@
+(***********************************************************************)
+(* *)
+(* Objective Caml *)
+(* *)
+(* Valerie Menissier-Morain, projet Cristal, INRIA Rocquencourt *)
+(* *)
+(* Copyright 1996 Institut National de Recherche en Informatique et *)
+(* en Automatique. All rights reserved. This file is distributed *)
+(* under the terms of the GNU Library General Public License, with *)
+(* the special exception on linking. *)
+(* *)
+(***********************************************************************)
+
+open MiscNum
+open Integers
+open Rationals
+
+type num = Int of int | Big_int of big_int | Ratio of ratio
+
+let sign_num = function
+ | Int i -> sign_int i
+ | Big_int bi -> sign_big_int bi
+ | Ratio r -> sign_ratio r
+
+let abs_num = function
+ | Int i ->
+ if i = monster_int then
+ Big_int (minus_big_int (big_int_of_int i))
+ else Int (abs i)
+ | Big_int bi -> Big_int (abs_big_int bi)
+ | Ratio r -> Ratio (abs_ratio r)
+
+let biggest_INT = big_int_of_int biggest_int
+let least_INT = big_int_of_int least_int
+let num_of_big_int bi =
+ if le_big_int bi biggest_INT && ge_big_int bi least_INT
+ then Int (int_of_big_int bi)
+ else Big_int bi
+
+let num_of_ratio r =
+ ignore (normalize_ratio r);
+ if not (is_integer_ratio r) then Ratio r
+ else if is_int_big_int (numerator_ratio r) then
+ Int (int_of_big_int (numerator_ratio r))
+ else Big_int (numerator_ratio r)
+
+(* Operations on num *)
+
+let is_integer_num = function
+ | Int _ -> true
+ | Big_int _ -> true
+ | Ratio r -> is_integer_ratio r
+
+let add_num a b = match (a,b) with
+ | ((Int int1), (Int int2)) ->
+ let r = int1 + int2 in
+ if (int1 lxor int2) lor (int1 lxor (r lxor (-1))) < 0
+ then Int r (* No overflow *)
+ else Big_int(add_big_int (big_int_of_int int1) (big_int_of_int int2))
+
+ | ((Int i), (Big_int bi)) ->
+ num_of_big_int (add_int_big_int i bi)
+
+ | ((Big_int bi), (Int i)) ->
+ num_of_big_int (add_int_big_int i bi)
+
+ | ((Int i), (Ratio r)) ->
+ Ratio (add_int_ratio i r)
+ | ((Ratio r), (Int i)) ->
+ Ratio (add_int_ratio i r)
+
+ | ((Big_int bi1), (Big_int bi2)) -> num_of_big_int (add_big_int bi1 bi2)
+
+ | ((Big_int bi), (Ratio r)) ->
+ Ratio (add_big_int_ratio bi r)
+
+ | ((Ratio r), (Big_int bi)) ->
+ Ratio (add_big_int_ratio bi r)
+
+ | ((Ratio r1), (Ratio r2)) -> num_of_ratio (add_ratio r1 r2)
+
+let ( +/ ) = add_num
+
+let minus_num = function
+ | Int i ->
+ if i = monster_int
+ then Big_int (minus_big_int (big_int_of_int i))
+ else Int (-i)
+ | Big_int bi -> Big_int (minus_big_int bi)
+ | Ratio r -> Ratio (minus_ratio r)
+
+let sub_num n1 n2 = add_num n1 (minus_num n2)
+
+let ( -/ ) = sub_num
+
+let mult_num a b = match (a,b) with
+ | ((Int int1), (Int int2)) ->
+ if num_bits_int int1 + num_bits_int int2 < length_of_int
+ then Int (int1 * int2)
+ else num_of_big_int (mult_big_int (big_int_of_int int1)
+ (big_int_of_int int2))
+
+ | ((Int i), (Big_int bi)) ->
+ num_of_big_int (mult_int_big_int i bi)
+
+ | ((Big_int bi), (Int i)) ->
+ num_of_big_int (mult_int_big_int i bi)
+
+ | ((Int i), (Ratio r)) ->
+ num_of_ratio (mult_int_ratio i r)
+
+ | ((Ratio r), (Int i)) ->
+ num_of_ratio (mult_int_ratio i r)
+
+ | ((Big_int bi1), (Big_int bi2)) ->
+ num_of_big_int (mult_big_int bi1 bi2)
+
+ | ((Big_int bi), (Ratio r)) ->
+ num_of_ratio (mult_big_int_ratio bi r)
+
+ | ((Ratio r), (Big_int bi)) ->
+ num_of_ratio (mult_big_int_ratio bi r)
+
+ | ((Ratio r1), (Ratio r2)) ->
+ num_of_ratio (mult_ratio r1 r2)
+
+let ( */ ) = mult_num
+
+let div_num n1 n2 =
+ match n1 with
+ | Int i1 ->
+ (match n2 with
+ | Int i2 ->
+ num_of_ratio (create_ratio (big_int_of_int i1) (big_int_of_int i2))
+ | Big_int bi2 -> num_of_ratio (create_ratio (big_int_of_int i1) bi2)
+ | Ratio r2 -> num_of_ratio (div_int_ratio i1 r2)
+ )
+
+ | Big_int bi1 ->
+ (match n2 with
+ | Int i2 -> num_of_ratio (create_ratio bi1 (big_int_of_int i2))
+ | Big_int bi2 -> num_of_ratio (create_ratio bi1 bi2)
+ | Ratio r2 -> num_of_ratio (div_big_int_ratio bi1 r2)
+ )
+
+ | Ratio r1 ->
+ (match n2 with
+ | Int i2 -> num_of_ratio (div_ratio_int r1 i2)
+ | Big_int bi2 -> num_of_ratio (div_ratio_big_int r1 bi2)
+ | Ratio r2 -> num_of_ratio (div_ratio r1 r2)
+ )
+
+let ( // ) = div_num
+
+let floor_num = function
+ | Int i as n -> n
+ | Big_int bi as n -> n
+ | Ratio r -> num_of_big_int (floor_ratio r)
+
+
+(* The function [quo_num] is equivalent to
+ let quo_num x y = floor_num (div_num x y)
+ However, this definition is vastly inefficient (cf PR #3473):
+ we define here a better way of computing the same thing.
+*)
+let quo_num n1 n2 =
+ match n1 with
+ | Int i1 ->
+ (match n2 with
+ | Int i2 -> Int (i1 / i2)
+ | Big_int bi2 -> num_of_big_int (div_big_int (big_int_of_int i1) bi2)
+ | Ratio r2 -> num_of_big_int (floor_ratio (div_int_ratio i1 r2))
+ )
+
+ | Big_int bi1 ->
+ (match n2 with
+ | Int i2 -> num_of_big_int (div_big_int bi1 (big_int_of_int i2))
+ | Big_int bi2 -> num_of_big_int (div_big_int bi1 bi2)
+ | Ratio r2 -> num_of_big_int (floor_ratio (div_big_int_ratio bi1 r2))
+ )
+
+ | Ratio r1 ->
+ (match n2 with
+ | Int i2 -> num_of_big_int (floor_ratio (div_ratio_int r1 i2))
+ | Big_int bi2 ->
+ num_of_big_int (floor_ratio (div_ratio_big_int r1 bi2))
+ | Ratio r2 -> num_of_big_int (floor_ratio (div_ratio r1 r2))
+ )
+
+(* The function [mod_num] is equivalent to:
+ let mod_num x y = sub_num x (mult_num y (quo_num x y));;
+ However, as for [quo_num] above, this definition is inefficient:
+ we define here a better way of computing the same thing.
+*)
+let mod_num n1 n2 =
+ match n1 with
+ | Int i1 ->
+ (match n2 with
+ | Int i2 -> Int (i1 mod i2)
+ | Big_int bi2 -> num_of_big_int (mod_big_int (big_int_of_int i1) bi2)
+ | Ratio _r2 -> sub_num n1 (mult_num n2 (quo_num n1 n2))
+ )
+
+ | Big_int bi1 ->
+ (match n2 with
+ | Int i2 -> num_of_big_int (mod_big_int bi1 (big_int_of_int i2))
+ | Big_int bi2 -> num_of_big_int (mod_big_int bi1 bi2)
+ | Ratio _r2 -> sub_num n1 (mult_num n2 (quo_num n1 n2))
+ )
+
+ | Ratio _r1 -> sub_num n1 (mult_num n2 (quo_num n1 n2))
+
+
+(* Comparisons on nums *)
+
+let eq_num a b = match (a,b) with
+ | ((Int int1), (Int int2)) -> int1 = int2
+ | ((Int i), (Big_int bi)) -> eq_big_int (big_int_of_int i) bi
+ | ((Big_int bi), (Int i)) -> eq_big_int (big_int_of_int i) bi
+ | ((Int i), (Ratio r)) -> eq_big_int_ratio (big_int_of_int i) r
+ | ((Ratio r), (Int i)) -> eq_big_int_ratio (big_int_of_int i) r
+ | ((Big_int...
[truncated message content] |
