[Toss-devel-svn] SF.net SVN: toss:[1734] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
[Toss-devel-svn] SF.net SVN: toss:[1734] trunk/Toss
|
From: <luk...@us...> - 2012-06-25 18:03:59
|
Revision: 1734
http://toss.svn.sourceforge.net/toss/?rev=1734&view=rev
Author: lukaszkaiser
Date: 2012-06-25 18:03:52 +0000 (Mon, 25 Jun 2012)
Log Message:
-----------
Test corrections and unicode for formulas.
Modified Paths:
--------------
trunk/Toss/Arena/Arena.ml
trunk/Toss/Arena/ContinuousRule.ml
trunk/Toss/Arena/DiscreteRule.ml
trunk/Toss/Client/eval.html
trunk/Toss/Formula/Formula.ml
trunk/Toss/Formula/Formula.mli
trunk/Toss/Formula/FormulaParser.mly
trunk/Toss/Formula/FormulaSubstTest.ml
trunk/Toss/Formula/FormulaTest.ml
trunk/Toss/Formula/Lexer.mll
trunk/Toss/Formula/Tokens.mly
trunk/Toss/Solver/Solver.ml
trunk/Toss/Solver/StructureTest.ml
trunk/Toss/Term/Rewriting.ml
trunk/Toss/Term/RewritingTest.ml
trunk/Toss/Term/tests/sasha_basic.log
trunk/Toss/Term/tests/sasha_basic.trs
Modified: trunk/Toss/Arena/Arena.ml
===================================================================
--- trunk/Toss/Arena/Arena.ml 2012-06-25 14:30:21 UTC (rev 1733)
+++ trunk/Toss/Arena/Arena.ml 2012-06-25 18:03:52 UTC (rev 1734)
@@ -105,7 +105,7 @@
Format.fprintf f "@ @[<0>PLAYER@ %s@ {@ %a}@]@," (Aux.rev_assoc pnames player)
(fun f (payoff, moves) ->
Format.fprintf f "@[<1>PAYOFF@ @[<1>%a@]@]@ "
- (Formula.fprint_real(* _nobra 0 *)) payoff;
+ (Formula.fprint_real ~unicode:false (* _nobra 0 *)) payoff;
if moves <> [] then
Format.fprintf f "@[<1>MOVES@ %a@]@ "
(Aux.fprint_sep_list ";" (fun f ({
@@ -185,11 +185,11 @@
if !equational_def_style then
Format.fprintf ppf "@[<1>REL@ %s@,(@[<1>%a@])@ =@ @[<1>%a@]"
drel (Aux.fprint_sep_list "," Format.pp_print_string) args
- Formula.fprint body
+ (Formula.fprint ~unicode:false) body
else
Format.fprintf ppf "@[<1>REL@ %s@,(@[<1>%a@])@ {@,@[<1>%a@,@]}"
drel (Aux.fprint_sep_list "," Format.pp_print_string) args
- Formula.fprint body;
+ (Formula.fprint ~unicode:false) body;
Format.fprintf ppf "@]@ ";
) defined_rels;
Format.fprintf ppf "@[<1>PLAYERS@ %a@]@ "
@@ -268,6 +268,7 @@
let add_def_rels struc rels = List.fold_left add_def_rel_single struc rels
let add_def_fun_single struc (f, v, def_re) =
+ LOG 1 "adding fun %s def %s" f (Formula.real_str def_re);
let elems = Structure.elements struc in
let asg e = AssignmentSet.FO (v, [(e, AssignmentSet.Any)]) in
let fval e = Solver.M.get_real_val ~asg:(asg e) def_re struc in
Modified: trunk/Toss/Arena/ContinuousRule.ml
===================================================================
--- trunk/Toss/Arena/ContinuousRule.ml 2012-06-25 14:30:21 UTC (rev 1733)
+++ trunk/Toss/Arena/ContinuousRule.ml 2012-06-25 18:03:52 UTC (rev 1734)
@@ -246,14 +246,16 @@
(DiscreteRule.fprint_full print_compiled) r.discrete;
if has_dynamics r then
Format.fprintf f "@ @[<hv>dynamics@ %a@]"
- (Formula.fprint_eqs ~diff:true) (List.sort Pervasives.compare r.dynamics);
+ (Formula.fprint_eqs ~unicode:false ~diff:true)
+ (List.sort Pervasives.compare r.dynamics);
if has_update r then
Format.fprintf f "@ @[<hv>update@ %a@]"
- (Formula.fprint_eqs ~diff:false) (List.sort Pervasives.compare r.update);
- if r.inv <> Formula.And [] then
- Format.fprintf f "@ @[<1>inv@ %a@]" Formula.fprint r.inv;
+ (Formula.fprint_eqs ~unicode:false ~diff:false)
+ (List.sort Pervasives.compare r.update);
+ if r.inv <> Formula.And [] then
+ Format.fprintf f "@ @[<1>inv@ %a@]" (Formula.fprint ~unicode:false) r.inv;
if r.post <> Formula.And [] then
- Format.fprintf f "@ @[<1>post@ %a@]" Formula.fprint r.post;
+ Format.fprintf f "@ @[<1>post@ %a@]" (Formula.fprint ~unicode:false) r.post;
Format.fprintf f "@]"
let fprint = fprint_full false
Modified: trunk/Toss/Arena/DiscreteRule.ml
===================================================================
--- trunk/Toss/Arena/DiscreteRule.ml 2012-06-25 14:30:21 UTC (rev 1733)
+++ trunk/Toss/Arena/DiscreteRule.ml 2012-06-25 18:03:52 UTC (rev 1734)
@@ -1185,7 +1185,8 @@
(Aux.fprint_sep_list "," matched) r.rule_s;
Format.fprintf f "@]";
if (fst r.pre <> Formula.And [] || snd r.pre <> []) then
- Format.fprintf f "@ @[<1>pre@ %a@]" Formula.fprint (fst r.pre);
+ Format.fprintf f "@ @[<1>pre@ %a@]"
+ (Formula.fprint ~unicode:false) (fst r.pre);
if (snd r.pre <> []) then
let before_str (name, b) = if b then name else "not " ^ name in
let before_s = String.concat ", " (List.map before_str (snd r.pre)) in
@@ -1310,7 +1311,7 @@
Format.fprintf f "@]") in
Format.fprintf f "@[<1>MATCH@ %a@ "
- (Formula.fprint_prec (-1)) r.match_formula;
+ (Formula.fprint_prec false (-1)) r.match_formula;
del_part ();
if del_elems <> [] || r.del_tuples <> []
then Format.fprintf f "@ ";
Modified: trunk/Toss/Client/eval.html
===================================================================
--- trunk/Toss/Client/eval.html 2012-06-25 14:30:21 UTC (rev 1733)
+++ trunk/Toss/Client/eval.html 2012-06-25 18:03:52 UTC (rev 1734)
@@ -156,15 +156,15 @@
<p>Relations:</p>
-<textarea id="relations" rows="3" cols="40">
-E(x, y) = &y = &x + 1
+<textarea id="relations" rows="3" cols="60">
+E(x, y) = (&y = &x + 1) ∨ (&x=15 ∧ &y=1)
</textarea>
<p>Positions:</p>
-<textarea id="positions" rows="3" cols="40">
+<textarea id="positions" rows="3" cols="60">
:x(a) = &a;
-:y(a) = &a * (10 - &a) / 10
+:y(a) = &a · (10 - &a) / 10
</textarea>
<p>Elements: <input id="no-elems" type="text" size="4" value="15"></input>
Modified: trunk/Toss/Formula/Formula.ml
===================================================================
--- trunk/Toss/Formula/Formula.ml 2012-06-25 14:30:21 UTC (rev 1733)
+++ trunk/Toss/Formula/Formula.ml 2012-06-25 18:03:52 UTC (rev 1734)
@@ -86,13 +86,13 @@
type sign_op = EQZero | GZero | LZero | GEQZero | LEQZero | NEQZero
(* Print a sign_op as string. *)
-let sign_op_str = function
+let sign_op_str ?(unicode=false) = function
| EQZero -> " = 0"
| GZero -> " > 0"
| LZero -> " < 0"
- | GEQZero -> " >= 0"
- | LEQZero -> " =< 0"
- | NEQZero -> " <> 0"
+ | GEQZero -> if unicode then " ≥ 0" else " >= 0"
+ | LEQZero -> if unicode then " ≤ 0" else " =< 0"
+ | NEQZero -> if unicode then " ≠ 0" else " <> 0"
(* This type describes formulas of relational logic with equality.
@@ -165,111 +165,127 @@
let fprint_var f v = Format.pp_print_string f (var_str v)
(* Bracket-savvy encodings: 0 or, 1 and, 2 not ex all *)
-let rec fprint_prec prec f = function
+let rec fprint_prec unicode prec f = function
| Rel (s, vars) ->
Format.fprintf f "%s(%a)" s
(Aux.fprint_sep_list "," fprint_var) (Array.to_list vars)
| Eq (x, y) -> Format.fprintf f "%s = %s" (var_str x) (var_str y)
- | In (x, y) -> Format.fprintf f "%s in %s" (var_str x) (var_str y)
+ | In (x, y) ->
+ if unicode then
+ Format.fprintf f "%s ∈ %s" (var_str x) (var_str y)
+ else
+ Format.fprintf f "%s in %s" (var_str x) (var_str y)
| SO (r, vars) ->
Format.fprintf f "%a(%a)" fprint_var r
(Aux.fprint_sep_list "," fprint_var) (Array.to_list vars)
| RealExpr (p, s) ->
- Format.fprintf f "@[(%a%s)@]" (fprint_real_prec 0) p (sign_op_str s)
+ Format.fprintf f "@[(%a%s)@]" (fprint_real_prec unicode 0)
+ p (sign_op_str ~unicode s)
| Not phi ->
- let lb, rb =
- if prec > 2 then "(", ")" else "", "" in
- Format.fprintf f "@[<1>%snot@ %a%s@]" lb (fprint_prec 2) phi rb
+ let lb, rb = if prec > 2 then "(", ")" else "", "" in
+ if unicode then
+ Format.fprintf f "@[<1>%s¬@ %a%s@]" lb (fprint_prec unicode 2) phi rb
+ else
+ Format.fprintf f "@[<1>%snot@ %a%s@]" lb (fprint_prec unicode 2) phi rb
| And [] -> Format.fprintf f "true"
| Or [] -> Format.fprintf f "false"
- | And [phi] -> fprint_prec prec f phi
- | Or [phi] -> fprint_prec prec f phi
+ | And [phi] -> fprint_prec unicode prec f phi
+ | Or [phi] -> fprint_prec unicode prec f phi
| And flist ->
let lb, rb = if prec = 0 || prec > 1 then "(", ")" else "", "" in
+ let sep = if unicode then " ∧" else " and" in
Format.fprintf f "@[<1>%s%a%s@]" lb
- (Aux.fprint_sep_list " and" (fprint_prec 1)) flist rb
+ (Aux.fprint_sep_list sep (fprint_prec unicode 1)) flist rb
| Or flist ->
let lb, rb = if prec > 0 then "(", ")" else "", "" in
+ let sep = if unicode then " ∨" else " or" in
Format.fprintf f "@[<1>%s%a%s@]" lb
- (Aux.fprint_sep_list " or" (fprint_prec 0)) flist rb
+ (Aux.fprint_sep_list sep (fprint_prec unicode 0)) flist rb
| Ex (x, phi) ->
let lb, rb = if prec > 2 then "(", ")" else "", "" in
- Format.fprintf f "@[<1>%sex@ %a@ %a%s@]" lb
- (Aux.fprint_sep_list "," fprint_var) x (fprint_prec 2) phi rb
+ let quant = if unicode then "∃" else "ex" in
+ Format.fprintf f "@[<1>%s%s@ %a@ %a%s@]" lb quant
+ (Aux.fprint_sep_list "," fprint_var) x (fprint_prec unicode 2) phi rb
| All (x, phi) ->
let lb, rb = if prec > 2 then "(", ")" else "", "" in
- Format.fprintf f "@[<1>%sall@ %a@ %a%s@]" lb
- (Aux.fprint_sep_list "," fprint_var) x (fprint_prec 2) phi rb
+ let quant = if unicode then "∀" else "all" in
+ Format.fprintf f "@[<1>%s%s@ %a@ %a%s@]" lb quant
+ (Aux.fprint_sep_list "," fprint_var) x (fprint_prec unicode 2) phi rb
| Lfp (r, vs, fpphi) ->
Format.fprintf f "@[<1>lfp %a(%a) = (%a)@]" fprint_var r
(Aux.fprint_sep_list "," fprint_var) (Array.to_list vs)
- (fprint_prec prec) fpphi
+ (fprint_prec unicode prec) fpphi
| Gfp (r, vs, fpphi) ->
Format.fprintf f "@[<1>gfp %a(%a) = (%a)@]" fprint_var r
(Aux.fprint_sep_list "," fprint_var) (Array.to_list vs)
- (fprint_prec prec) fpphi
+ (fprint_prec unicode prec) fpphi
| Let (r, args, rphi, inphi) ->
Format.fprintf f "@[<1>let %s(%s) = %a in@]@ %a" r (String.concat ", " args)
- (fprint_prec prec) rphi (fprint_prec prec) inphi
+ (fprint_prec unicode prec) rphi (fprint_prec unicode prec) inphi
(* Bracket-savvy precedences: 0 +, 2 * *)
-and fprint_real_prec prec f = function
+and fprint_real_prec unicode prec f = function
| RVar s -> Format.fprintf f "%s" s
| Const fl -> Format.fprintf f "%F" fl
| Plus (r1, Times (Const fl, r2)) when fl = -1. -> (* r1 - r2 short *)
let lb, rb = if prec > 0 then "(", ")" else "", "" in
Format.fprintf f "@[<1>%s%a@ -@ %a%s@]" lb
- (fprint_real_prec 0) r1 (fprint_real_prec 1) r2 rb
+ (fprint_real_prec unicode 0) r1 (fprint_real_prec unicode 1) r2 rb
| Times (r1, r2) ->
- let lb, rb =
- if prec > 2 then "(", ")" else "", "" in
- Format.fprintf f "@[<1>%s%a@ *@ %a%s@]" lb
- (fprint_real_prec 2) r1 (fprint_real_prec 2) r2 rb
+ let lb, rb = if prec > 2 then "(", ")" else "", "" in
+ let m = if unicode then "·" else "*" in
+ Format.fprintf f "@[<1>%s%a@ %s@ %a%s@]" lb
+ (fprint_real_prec unicode 2) r1 m (fprint_real_prec unicode 2) r2 rb
| Plus (r1, r2) ->
let lb, rb = if prec > 0 then "(", ")" else "", "" in
Format.fprintf f "@[<1>%s%a@ +@ %a%s@]" lb
- (fprint_real_prec 0) r1 (fprint_real_prec 0) r2 rb
+ (fprint_real_prec unicode 0) r1 (fprint_real_prec unicode 0) r2 rb
| Pow (r1, r2) ->
let lb, rb = if prec > 2 then "(", ")" else "", "" in
Format.fprintf f "@[<1>%s%a^%a%s@]" lb
- (fprint_real_prec 4) r1 (fprint_real_prec 4) r2 rb
+ (fprint_real_prec unicode 4) r1 (fprint_real_prec unicode 4) r2 rb
| Fun (s, v) -> Format.fprintf f ":%s(%s)" s (var_str v)
- | Char phi -> Format.fprintf f "@[<1>:(@,%a@,)@]" (fprint_prec 0) phi
+ | Char phi -> Format.fprintf f "@[<1>:(@,%a@,)@]" (fprint_prec unicode 0) phi
| Sum (vl, phi, r) ->
- Format.fprintf f "@[<1>Sum@ (@,%a@ |@ %a@ :@ %a@,)@]"
- (Aux.fprint_sep_list "," fprint_var) vl (fprint_prec 0) phi
- (fprint_real_prec 0) r
+ let sum = if unicode then "∑" else "Sum" in
+ Format.fprintf f "@[<1>%s@ (@,%a@ |@ %a@ :@ %a@,)@]" sum
+ (Aux.fprint_sep_list "," fprint_var) vl (fprint_prec unicode 0) phi
+ (fprint_real_prec unicode 0) r
| RLet (v, lre, inre) ->
Format.fprintf f "@[<1>let %s = %a in %a@]" v
- (fprint_real_prec prec) lre (fprint_real_prec prec) inre
+ (fprint_real_prec unicode prec) lre (fprint_real_prec unicode prec) inre
-let fprint f phi = fprint_prec 0 f phi
-let fprint_real f phi = fprint_real_prec 0 f phi
-let sprint phi = AuxIO.sprint_of_fprint fprint phi
-let print phi = AuxIO.print_of_fprint fprint phi
-let print_real r = AuxIO.print_of_fprint fprint_real r
-let sprint_real r = AuxIO.sprint_of_fprint fprint_real r
-let str f = sprint f
-let real_str r = sprint_real r
+let fprint ?(unicode=false) f phi = fprint_prec unicode 0 f phi
+let fprint_real ?(unicode=false) f phi = fprint_real_prec unicode 0 f phi
+let sprint ?(unicode=false) phi =
+ AuxIO.sprint_of_fprint (fprint_prec unicode 0) phi
+let print ?(unicode=false) phi =
+ AuxIO.print_of_fprint (fprint_prec unicode 0) phi
+let print_real ?(unicode=false) r =
+ AuxIO.print_of_fprint (fprint_real_prec unicode 0) r
+let sprint_real ?(unicode=false) r =
+ AuxIO.sprint_of_fprint (fprint_real_prec unicode 0) r
+let str ?(unicode=false) f = sprint ~unicode f
+let real_str ?(unicode=false) r = sprint_real ~unicode r
type eq_sys = ((string * string) * real_expr) list
(* Print an equation system. *)
-let fprint_eqs ?(diff=false) ppf eqs =
+let fprint_eqs ?(unicode=false) ?(diff=false) ppf eqs =
let sing ppf ((f, a), t) =
let mid_str = if diff then "'" else "" in
Format.fprintf ppf "@[<1>:%s(%s)%s@ =@ @[<1>%a@]@]"
- f a mid_str fprint_real t in
+ f a mid_str (fprint_real ~unicode) t in
Format.fprintf ppf "@[<hv>%a@]" (Aux.fprint_sep_list ";" sing) eqs
(* Print an equation system as a string. *)
-let eq_str ?(diff=false) eqs =
+let eq_str ?(unicode=false) ?(diff=false) eqs =
let sing_str ((f, a), t) =
let mid_str = if diff then "' = " else " = " in
- let l_str = real_str (Fun (f, `FO a)) in
- let r_str = real_str t in
+ let l_str = real_str ~unicode (Fun (f, `FO a)) in
+ let r_str = real_str ~unicode t in
l_str ^ mid_str ^ r_str in
" " ^ (String.concat ";\n " (List.map sing_str eqs))
Modified: trunk/Toss/Formula/Formula.mli
===================================================================
--- trunk/Toss/Formula/Formula.mli 2012-06-25 14:30:21 UTC (rev 1733)
+++ trunk/Toss/Formula/Formula.mli 2012-06-25 18:03:52 UTC (rev 1734)
@@ -42,7 +42,7 @@
type sign_op = EQZero | GZero | LZero | GEQZero | LEQZero | NEQZero
(** Print a sign_op as string. *)
-val sign_op_str : sign_op -> string
+val sign_op_str : ?unicode: bool -> sign_op -> string
(** This type describes formulas of relational logic with equality.
@@ -96,24 +96,25 @@
val var_list_str: [< var] list -> string
(** Print a formula as a string. *)
-val str : formula -> string
+val str : ?unicode: bool -> formula -> string
val mona_str : formula -> string
-val print : formula -> unit
-val sprint : formula -> string
-val fprint : Format.formatter -> formula -> unit
+val print : ?unicode: bool -> formula -> unit
+val sprint : ?unicode: bool -> formula -> string
+val fprint : ?unicode: bool -> Format.formatter -> formula -> unit
(** Print a real_expr as a string. *)
-val real_str : real_expr -> string
-val print_real : real_expr -> unit
-val sprint_real : real_expr -> string
-val fprint_real : Format.formatter -> real_expr -> unit
+val real_str : ?unicode: bool -> real_expr -> string
+val print_real : ?unicode: bool -> real_expr -> unit
+val sprint_real : ?unicode: bool -> real_expr -> string
+val fprint_real : ?unicode: bool -> Format.formatter -> real_expr -> unit
-val fprint_prec : int -> Format.formatter -> formula -> unit
-val fprint_real_prec : int -> Format.formatter -> real_expr -> unit
+val fprint_prec : bool -> int -> Format.formatter -> formula -> unit
+val fprint_real_prec : bool -> int -> Format.formatter -> real_expr -> unit
(** Print an equation system. *)
-val fprint_eqs : ?diff : bool -> Format.formatter -> eq_sys -> unit
-val eq_str : ?diff:bool -> eq_sys -> string
+val fprint_eqs : ?unicode: bool -> ?diff: bool ->
+ Format.formatter -> eq_sys -> unit
+val eq_str : ?unicode: bool -> ?diff: bool -> eq_sys -> string
(** {2 Formula syntax check} *)
Modified: trunk/Toss/Formula/FormulaParser.mly
===================================================================
--- trunk/Toss/Formula/FormulaParser.mly 2012-06-25 14:30:21 UTC (rev 1733)
+++ trunk/Toss/Formula/FormulaParser.mly 2012-06-25 18:03:52 UTC (rev 1734)
@@ -62,7 +62,7 @@
{ Formula.Sum ($3, $5, $7) }
| COLON OPEN formula_expr CLOSE { Char (Formula.flatten $3) }
| OPEN real_expr CLOSE { $2 }
- | COLON LET_CMD COLON v = ID EQ def = real_expr IN_MOD re = real_expr
+ | LET_CMD COLON v = ID EQ def = real_expr IN_MOD re = real_expr
{ RLet (":" ^ v, def, re) }
real_ineq:
@@ -125,8 +125,11 @@
| formula_expr MID formula_expr { Or [$1; $3] }
| formula_expr XOR formula_expr { And [Or [$1; $3]; Not (And [$1; $3])] }
| formula_expr RARR formula_expr { Or [Not ($1); $3] }
+ | formula_expr RDARR formula_expr { Or [Not ($1); $3] }
| formula_expr LRARR formula_expr
{ Or [And [Not ($1); Not ($3)]; And [$1; $3]] }
+ | formula_expr LRDARR formula_expr
+ { Or [And [Not ($1); Not ($3)]; And [$1; $3]] }
| OPEN formula_expr CLOSE { $2 }
| LET_CMD rel = ID args = delimited (OPEN, separated_list (COMMA, ID), CLOSE)
EQ body = formula_expr IN_MOD phi = formula_expr
Modified: trunk/Toss/Formula/FormulaSubstTest.ml
===================================================================
--- trunk/Toss/Formula/FormulaSubstTest.ml 2012-06-25 14:30:21 UTC (rev 1733)
+++ trunk/Toss/Formula/FormulaSubstTest.ml 2012-06-25 18:03:52 UTC (rev 1734)
@@ -110,7 +110,7 @@
"let Next(x, y) = E(x, y) and R(y) in R(a)")
"lfp R(a) = (P(a) or ex y (E(a, y) and y in R))";
exp_eq "let R(x) = P(x) in :(R(a)) > 1" ":(P(a)) > 1";
- exp_eq "(:let :x = 3 in :x) > 1" "3 > 1";
+ exp_eq "(let :x = 3 in :x) > 1" "3 > 1";
);
"fv" >::
Modified: trunk/Toss/Formula/FormulaTest.ml
===================================================================
--- trunk/Toss/Formula/FormulaTest.ml 2012-06-25 14:30:21 UTC (rev 1733)
+++ trunk/Toss/Formula/FormulaTest.ml 2012-06-25 18:03:52 UTC (rev 1734)
@@ -55,6 +55,12 @@
test_pp "all y (R(x, y) or not P(y))";
test_pp "(:x - (:y + :z) < 0)";
test_pp "(:x - :y + :z < 0)";
+
+ let test_pp_unicode f_s = assert_equal ~printer:(fun x -> x) f_s
+ (str ~unicode:true (flatten (formula_of_string f_s))) in
+ test_pp_unicode "∃ y (R(x, y) ∧ P(y))";
+ test_pp_unicode "∀ y (R(x, y) ∨ ¬ P(y))";
+ test_pp_unicode "(∑ (x | P(x) : 2. · :f(x)) ≥ 0)";
);
"rk4" >::
Modified: trunk/Toss/Formula/Lexer.mll
===================================================================
--- trunk/Toss/Formula/Lexer.mll 2012-06-25 14:30:21 UTC (rev 1733)
+++ trunk/Toss/Formula/Lexer.mll 2012-06-25 18:03:52 UTC (rev 1734)
@@ -152,24 +152,33 @@
| '&' { AMP }
| '|' { MID }
| "Sum" { SUM }
+ | "∑" { SUM }
| '+' { PLUS }
| '-' { MINUS }
+ | "−" { MINUS }
| '*' { TIMES }
+ | "·" { TIMES }
+ | "×" { TIMES }
| '/' { DIV }
| '^' { POW }
| '>' { GR }
| ">=" { GREQ }
+ | "≥" { GREQ }
| '<' { LT }
| "=<" { EQLT }
+ | "≤" { EQLT }
| '=' { EQ }
| "<>" { LTGR }
| "!=" { NEQ }
+ | "≠" { NEQ }
| "!" { NOT }
| "<-" { LARR }
| "<=" { LDARR }
| "->" { RARR }
| "=>" { RDARR }
+ | "⇒" { RDARR }
| "<->" { LRARR }
+ | "⇔" { LRDARR }
| "<=>" { LRDARR }
| "--" { INTERV }
| '(' { OPEN }
@@ -180,12 +189,20 @@
| ']' { CLOSESQ }
| "in" { IN_MOD }
| "and" { AND }
+ | "∧" { AND }
| "or" { OR }
+ | "∨" { OR }
| "xor" { XOR }
+ | "⊕" { XOR }
| "not" { NOT }
+ | "¬" { NOT }
| "ex" { EX }
+ | "\\E" { EX }
| "exists" { EX }
+ | "∃" { EX }
| "all" { ALL }
+ | "\\A" { ALL }
+ | "∀" { ALL }
| "tc" { TC }
| "TC" { TC }
| "with" { WITH }
Modified: trunk/Toss/Formula/Tokens.mly
===================================================================
--- trunk/Toss/Formula/Tokens.mly 2012-06-25 14:30:21 UTC (rev 1733)
+++ trunk/Toss/Formula/Tokens.mly 2012-06-25 18:03:52 UTC (rev 1734)
@@ -14,7 +14,7 @@
%token CURRENT UNIVERSAL RULE_SPEC STATE_SPEC CLASS LFP GFP EOF
/* List in order of increasing precedence. */
-%nonassoc LET_CMD
+%nonassoc LET_CMD IN_MOD
%nonassoc COND
%left LARR
%right RARR
@@ -26,7 +26,7 @@
%left OR
%left AND
%left COMMA
-%nonassoc EQ IN_MOD
+%nonassoc EQ
%left NOT EX ALL
%%
Modified: trunk/Toss/Solver/Solver.ml
===================================================================
--- trunk/Toss/Solver/Solver.ml 2012-06-25 14:30:21 UTC (rev 1733)
+++ trunk/Toss/Solver/Solver.ml 2012-06-25 18:03:52 UTC (rev 1734)
@@ -507,6 +507,10 @@
(Array.of_list (List.map var_str all_vs)) [tp] in
acc +. (get_real_val solver tp_asg r struc) in
List.fold_left add_val 0. tps
+ | RLet _ ->
+ let e = FormulaSubst.expand_real_expr expr in
+ LOG 1 "get_real_val: expanded to: %s" (real_str e);
+ get_real_val solver asg e struc
| _ ->
check_timeout "Solver.get_real_val.other";
let rec get_rval = function
@@ -579,8 +583,8 @@
let check struc phi = check_cache (
check solver ~formula:(register_formula_s struc solver phi) struc)
- let get_real_val ?asg re struc = check_cache (
- check_cache (get_real_val_cache ?asg solver struc re))
+ let get_real_val ?asg re struc =
+ check_cache (get_real_val_cache ?asg solver struc re)
let set_timeout t = timeout := t
let clear_timeout () = timeout := (fun () -> false);
Modified: trunk/Toss/Solver/StructureTest.ml
===================================================================
--- trunk/Toss/Solver/StructureTest.ml 2012-06-25 14:30:21 UTC (rev 1733)
+++ trunk/Toss/Solver/StructureTest.ml 2012-06-25 18:03:52 UTC (rev 1734)
@@ -373,10 +373,7 @@
" in
let (_, st) = struc_from_trs s in
assert_equal ~printer:(fun x -> x)
- ("[F0_0\\, F1_0\\, F2, F3, F4, F5 | R {(F0_0\\, F1_0\\); (F1_0\\, F2);"^
- " (F2, F3); (F3, F4); (F4, F5)} | x {F0_0\\->0., F1_0\\->1.," ^
- " F2->2., F3->3., F4->4., F5->5.}; y {F0_0\\->0., F1_0\\->1.," ^
- " F2->2., F3->3., F4->4., F5->5.}]") (Structure.str st);
+ ("[F0_0\\[ @: Tnatural_number], F1_0\\[ @: Tnatural_number], F2[ @: Tnatural_number], F3[ @: Tnatural_number], F4[ @: Tnatural_number], F5[ @: Tnatural_number] | R {(F0_0\\[ @: Tnatural_number], F1_0\\[ @: Tnatural_number]); (F1_0\\[ @: Tnatural_number], F2[ @: Tnatural_number]); (F2[ @: Tnatural_number], F3[ @: Tnatural_number]); (F3[ @: Tnatural_number], F4[ @: Tnatural_number]); (F4[ @: Tnatural_number], F5[ @: Tnatural_number])} | x {F0_0\\[ @: Tnatural_number]->0., F1_0\\[ @: Tnatural_number]->1., F2[ @: Tnatural_number]->2., F3[ @: Tnatural_number]->3., F4[ @: Tnatural_number]->4., F5[ @: Tnatural_number]->5.}; y {F0_0\\[ @: Tnatural_number]->0., F1_0\\[ @: Tnatural_number]->1., F2[ @: Tnatural_number]->2., F3[ @: Tnatural_number]->3., F4[ @: Tnatural_number]->4., F5[ @: Tnatural_number]->5.}]") (Structure.str st);
);
"sprint simple" >::
Modified: trunk/Toss/Term/Rewriting.ml
===================================================================
--- trunk/Toss/Term/Rewriting.ml 2012-06-25 14:30:21 UTC (rev 1733)
+++ trunk/Toss/Term/Rewriting.ml 2012-06-25 18:03:52 UTC (rev 1734)
@@ -55,10 +55,6 @@
| (Term (n1, _, _), Term (n2, _, [||])) when (n1 = n2) ->
raise NO_MATCH (* used cons vs. functional cons *)
| (Term (n1, _, _), Term (n2, _, _)) when (n1 = n2) ->
- (*Printf.printf "check_clash_match: [1] %s(%d) %s(%d): %a -- %a\n"
- n1 (Array.length a1) n2 (Array.length a2)
- (Aux.array_fprint (fun o t->output_string o (Coding.term_to_string t))) a1
- (Aux.array_fprint (fun o t->output_string o (Coding.term_to_string t))) a2;*)
failwith "curried functions not supported (yet?)"
| (Term (n1, _, _), Term (n2, _, _)) -> (* when (n2.[0] != 'F') *)
raise NO_MATCH
@@ -80,15 +76,12 @@
raise NO_MATCH (* non-0-arg fun and functional term *)
| _ -> failwith "rewriting not this function"
-(* Merging substitutions according to variable names. FIXME: perhaps
- use [Term.combine_mgu_sb], otherwise streamline. *)
+(* Merging substitutions according to variable names.
+ FIXME: perhaps use [Term.combine_mgu_sb], otherwise streamline.
+ NOTE: we assume that the rules are left-linear (checked above). *)
let merge_substs substs =
let merged_substs = Aux.collect substs in
- let mkcm b = (* if List.length b <> 1 then failwith "cm" else *)
- snd (List.hd b) in
- let make_cm (a, b) = (false, (a, mkcm b)) in
- let (clashes, substs) = List.split (map make_cm merged_substs) in
- (exists (fun x -> x) clashes, substs)
+ (false, List.map (fun (a, b) -> (a, snd (List.hd b))) merged_substs)
(* The final function for applying a rewrite rule with clash checking and
@@ -101,7 +94,7 @@
if merge_clash then term
else
let result = Coding.apply_s merged_substs right in
- (* For now, we copy over the supertypes fro the original, as
+ (* For now, we copy over the supertypes from the original, as
the old rewriting ignores supertypes. *)
match term, result with
| Term (_, oldtys, _), Term (n, _, args) ->
@@ -179,21 +172,21 @@
else
let (steps, res) = basic_normalise rr rr_spec m rewritten in
(steps + steps_c + 1, res)
- | Term (n, t, a) when n.[0] = 'F' ->
- (let (prev_steps, prev_res) = basic_normalise_arr rr rr_spec m a in
- let nmlized = Term (n, t, prev_res) in
- let found= try Some (TermHashtbl.find m nmlized) with Not_found -> None in
- match found with Some (r) -> (prev_steps, r) | None ->
- let rewritten = rr nmlized in
- if rewritten = nmlized then (prev_steps, rewritten) else
- let (steps, res) = basic_normalise rr rr_spec m rewritten in
- let memory_size = TermHashtbl.length m in
- let threshold = (memory_size / cMEM_USE_INCREASE_FACTOR) + 1 in
- let size_addon = min (size_up_to 256 nmlized) threshold in
- if steps > threshold + size_addon then
- (TermHashtbl.add m nmlized res; (0, res))
- else (prev_steps + steps + 1, res)
- )
+ | Term (n, t, a) when n.[0] = 'F' -> (
+ let (prev_steps, prev_res) = basic_normalise_arr rr rr_spec m a in
+ let nmlized = Term (n, t, prev_res) in
+ let found= try Some (TermHashtbl.find m nmlized) with Not_found -> None in
+ match found with Some (r) -> (prev_steps, r) | None -> (
+ let rewritten = rr nmlized in
+ if rewritten = nmlized then (prev_steps, nmlized) else (
+ let (steps, res) = basic_normalise rr rr_spec m rewritten in
+ let memory_size = TermHashtbl.length m in
+ let threshold = (memory_size / cMEM_USE_INCREASE_FACTOR) + 1 in
+ let size_addon = min (size_up_to 256 nmlized) threshold in
+ if steps > threshold + size_addon then
+ (TermHashtbl.add m nmlized res; (0, res))
+ else (prev_steps + steps + 1, res)
+ )))
| Term (n, t, a) ->
let (steps, res) = basic_normalise_arr rr rr_spec m a in
(steps, Term (n, t, res))
Modified: trunk/Toss/Term/RewritingTest.ml
===================================================================
--- trunk/Toss/Term/RewritingTest.ml 2012-06-25 14:30:21 UTC (rev 1733)
+++ trunk/Toss/Term/RewritingTest.ml 2012-06-25 18:03:52 UTC (rev 1734)
@@ -51,7 +51,7 @@
let t3 = Term ("Fand", [|boolean_tp|], [|var_x_b; t1|]) in
test_ne rrs "Fand[ @: Tboolean] (@V [x @: Tboolean @: 0 ], Ftrue[ @: Tboolean] )" t3;
let t4 = Term (if_then_else_name, [|boolean_tp|], [|var_x_b; t1; t1|]) in
- test_ne rrs ("Fif_\?_then_\?_else_\?[ @: Tboolean] (@V [x @: Tboolean @: 0 ], Fand[ @: Tboolean] (Ftrue[ @: Tboolean], Ftrue[ @: Tboolean] ), Fand[ @: Tboolean] (Ftrue[ @: Tboolean], Ftrue[ @: Tboolean] ) )") t4;
+ test_ne rrs ("Fif_\\?_then_\\?_else_\\?[ @: Tboolean] (@V [x @: Tboolean @: 0 ], Fand[ @: Tboolean] (Ftrue[ @: Tboolean], Ftrue[ @: Tboolean] ), Fand[ @: Tboolean] (Ftrue[ @: Tboolean], Ftrue[ @: Tboolean] ) )") t4;
let t5 = Term ("Ckot", [|char_tp|], [|var_x_b; t1; t1|]) in
test_ne rrs "Ckot[ @: Tchar] (@V [x @: Tboolean @: 0 ], Ftrue[ @: Tboolean], Ftrue[ @: Tboolean] )" t5;
);
Modified: trunk/Toss/Term/tests/sasha_basic.log
===================================================================
--- trunk/Toss/Term/tests/sasha_basic.log 2012-06-25 14:30:21 UTC (rev 1733)
+++ trunk/Toss/Term/tests/sasha_basic.log 2012-06-25 18:03:52 UTC (rev 1734)
@@ -255,7 +255,7 @@
hanoi (0 , startPeg , goalPeg) => []
New rewrite rule defined.
-hanoi (noDiscs , startPeg , goalPeg) => hanoi (noDiscs - 1 , startPeg , remainingPeg (startPeg , goalPeg) ) + [ (startPeg , goalPeg) ] + hanoi (noDiscs - 1 , remainingPeg (startPeg , goalPeg) , goalPeg)
+hanoi (noDiscs , startPeg , goalPeg) => hanoi (noDiscs - 1 , startPeg , remainingPeg (startPeg , goalPeg) ) + ( [ (startPeg , goalPeg) ] + hanoi (noDiscs - 1 , remainingPeg (startPeg , goalPeg) , goalPeg) )
Closed context.
Modified: trunk/Toss/Term/tests/sasha_basic.trs
===================================================================
--- trunk/Toss/Term/tests/sasha_basic.trs 2012-06-25 14:30:21 UTC (rev 1733)
+++ trunk/Toss/Term/tests/sasha_basic.trs 2012-06-25 18:03:52 UTC (rev 1734)
@@ -130,8 +130,8 @@
hanoi (0, startPeg, goalPeg) => [];
hanoi (noDiscs, startPeg, goalPeg) =>
hanoi (noDiscs - 1, startPeg, remainingPeg (startPeg, goalPeg)) +
- [(startPeg, goalPeg)] +
- hanoi (noDiscs - 1, remainingPeg (startPeg, goalPeg), goalPeg);
+ ( [(startPeg, goalPeg)] +
+ hanoi (noDiscs - 1, remainingPeg (startPeg, goalPeg), goalPeg) );
***;
// Horner's algorithm for polynomial evaluation;
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
