[Toss-devel-svn] SF.net SVN: toss:[1205] trunk/Toss

[<luk...@us...>]

Revision: 1205
          http://toss.svn.sourceforge.net/toss/?rev=1205&view=rev
Author:   lukstafi
Date:     2010-11-28 16:10:41 +0000 (Sun, 28 Nov 2010)

Log Message:
-----------
Printing adjustments.

Modified Paths:
--------------
    trunk/Toss/Arena/ContinuousRule.ml
    trunk/Toss/Formula/Formula.ml
    trunk/Toss/Formula/Formula.mli
    trunk/Toss/Solver/FFSolverTest.ml

Modified: trunk/Toss/Arena/ContinuousRule.ml
===================================================================
--- trunk/Toss/Arena/ContinuousRule.ml	2010-11-28 15:34:57 UTC (rev 1204)
+++ trunk/Toss/Arena/ContinuousRule.ml	2010-11-28 16:10:41 UTC (rev 1205)
@@ -202,12 +202,12 @@
     Format.fprintf f "@ @[<hv>update@ %a@]"
       (Term.fprint_eqs ~diff:false) r.update;
   if r.discrete.DiscreteRule.pre <> Formula.And [] then
-    Format.fprintf f "@ @[<1>pre@ %a@]" (Formula.fprint_nobra 0)
+    Format.fprintf f "@ @[<1>pre@ %a@]" Formula.fprint
       r.discrete.DiscreteRule.pre;
   if r.inv <> Formula.And [] then
-    Format.fprintf f "@ @[<1>inv@ %a@]" (Formula.fprint_nobra 0) r.inv;
+    Format.fprintf f "@ @[<1>inv@ %a@]" Formula.fprint r.inv;
   if r.post <> Formula.And [] then
-    Format.fprintf f "@ @[<1>post@ %a@]" (Formula.fprint_nobra 0) r.post;
+    Format.fprintf f "@ @[<1>post@ %a@]" Formula.fprint r.post;
   Format.fprintf f "@]"
 
 let print r = fprint Format.std_formatter r

Modified: trunk/Toss/Formula/Formula.ml
===================================================================
--- trunk/Toss/Formula/Formula.ml	2010-11-28 15:34:57 UTC (rev 1204)
+++ trunk/Toss/Formula/Formula.ml	2010-11-28 16:10:41 UTC (rev 1205)
@@ -163,104 +163,65 @@
 
 
 
-let rec fprint_formula f = function
-    Rel (s, vars) -> Format.fprintf f "%s(%a)" s fprint_var_tup 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)
-  | RealExpr (p, s) -> 
-      Format.fprintf f "@[(%a %s)@]" fprint_real p (sign_op_str s)
-  | Not phi -> Format.fprintf f "@[(not %a)@]" fprint_formula phi
-  | And [] -> Format.fprintf f "true"
-  | Or [] -> Format.fprintf f "false"
-  | And (flist) -> fprint_f_list " and " f flist
-  | Or (flist) -> fprint_f_list " or " f flist
-  | Ex (x, phi) -> 
-      Format.fprintf f "ex %a@ @[<1>(%a)@]" fprint_var_list x fprint_formula phi
-  | All (x, phi) -> 
-      Format.fprintf f "all %a@ @[<1>(%a)@]" fprint_var_list x fprint_formula phi
-
-and fprint_f_list sep f = function
-    [] -> Format.fprintf f "[]"
-  | [phi] -> fprint_formula f phi
-  | lst -> 
-      let rec fprlst fm = function
-          [] -> ()
-        | [x] -> Format.fprintf fm "%a" fprint_formula x
-        | x :: xs -> 
-            Format.fprintf fm "%a@ %s@ %a" fprint_formula x sep fprlst xs in
-      Format.fprintf f "@[<1>(%a)@]" fprlst lst
-
-and fprint_real f = function
-    RVar s -> Format.fprintf f "%s" s
-  | Const fl -> Format.fprintf f "%F" fl
-  | Times (r1, r2) -> 
-      Format.fprintf f "@[(%a@ *@ %a)@]" fprint_real r1 fprint_real r2
-  | Plus (r1, r2) -> 
-      Format.fprintf f "@[(%a@ +@ %a)@]" fprint_real r1 fprint_real r2
-  | Fun (s, v) -> Format.fprintf f ":%s(%s)" s (var_str v)
-  | Char phi -> Format.fprintf f "@[<1>:(%a)@]" fprint_formula phi
-  | Sum (vl, phi, r) -> 
-      Format.fprintf f "@[<1>Sum (%s | %a : %a)@]" 
-        (var_list_str vl) fprint_formula phi fprint_real r
-
 let fprint_var f v = Format.pp_print_string f (var_str v)
 
-(* Bracket-savvy precedences: 0 or, 1 and, 2 not ex all *)
-let rec fprint_nobra prec f = function
+(* Bracket-savvy encodings: 0 or, 1 and, 2 not ex all *)
+let rec fprint_prec 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)
   | RealExpr (p, s) -> 
-    Format.fprintf f "@[(%a %s)@]" (fprint_real_nobra 0) p (sign_op_str s)
+    Format.fprintf f "@[(%a %s)@]" (fprint_real_prec 0) p (sign_op_str s)
   | Not phi ->
     let lb, rb =
       if prec > 2 then "(", ")" else "", "" in
-    Format.fprintf f "@[<1>%snot@ %a%s@]" lb (fprint_nobra 2) phi rb
+    Format.fprintf f "@[<1>%snot@ %a%s@]" lb (fprint_prec 2) phi rb
   | And [] -> Format.fprintf f "true"
   | Or [] -> Format.fprintf f "false"
-  | And [phi] -> fprint_nobra prec f phi
-  | Or [phi] -> fprint_nobra prec f phi
+  | And [phi] -> fprint_prec prec f phi
+  | Or [phi] -> fprint_prec prec f phi
   | And flist ->
-    let lb, rb = if prec > 1 then "(", ")" else "", "" in
+    let lb, rb = if prec = 0 || prec > 1 then "(", ")" else "", "" in
     Format.fprintf f "@[<1>%s%a%s@]" lb
-      (Aux.fprint_sep_list " and" (fprint_nobra 1)) flist rb
+      (Aux.fprint_sep_list " and" (fprint_prec 1)) flist rb
   | Or flist ->
     let lb, rb = if prec > 0 then "(", ")" else "", "" in
     Format.fprintf f "@[<1>%s%a%s@]" lb
-      (Aux.fprint_sep_list " or" (fprint_nobra 0)) flist rb
+      (Aux.fprint_sep_list " or" (fprint_prec 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_nobra 2) phi rb
+      (Aux.fprint_sep_list "," fprint_var) x (fprint_prec 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_nobra 2) phi rb
+      (Aux.fprint_sep_list "," fprint_var) x (fprint_prec 2) phi rb
 
 (* Bracket-savvy precedences: 0 +, 2 * *)
-and fprint_real_nobra prec f = function
+and fprint_real_prec prec f = function
     RVar s -> Format.fprintf f "%s" s
   | Const fl -> Format.fprintf f "%F" fl
   | Times (r1, r2) -> 
     let lb, rb =
       if prec > 2 then "(", ")" else "", "" in
     Format.fprintf f "@[<1>%s%a@ *@ %a%s@]" lb
-      (fprint_real_nobra 2) r1 (fprint_real_nobra 2) r2 rb
+      (fprint_real_prec 2) r1 (fprint_real_prec 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_nobra 0) r1 (fprint_real_nobra 0) r2 rb
+      (fprint_real_prec 0) r1 (fprint_real_prec 0) r2 rb
   | Fun (s, v) -> Format.fprintf f ":%s(%s)" s (var_str v)
-  | Char phi -> Format.fprintf f "@[<1>:(@,%a@,)@]" (fprint_nobra 0) phi
+  | Char phi -> Format.fprintf f "@[<1>:(@,%a@,)@]" (fprint_prec 0) phi
   | Sum (vl, phi, r) -> 
       Format.fprintf f "@[<1>Sum@ (@,%a@ |@ %a@ :@ %a@,)@]" 
-        (Aux.fprint_sep_list "," fprint_var) vl (fprint_nobra 0) phi
-        (fprint_real_nobra 0) r
+        (Aux.fprint_sep_list "," fprint_var) vl (fprint_prec 0) phi
+        (fprint_real_prec 0) r
 
 
-let fprint f phi = Format.fprintf f "@[%a@]" fprint_formula phi
+let fprint f phi = fprint_prec 0 f phi
+let fprint_real f phi = fprint_real_prec 0 f phi
 let print phi = fprint Format.std_formatter phi
 let sprint phi =
   ignore (Format.flush_str_formatter ());

Modified: trunk/Toss/Formula/Formula.mli
===================================================================
--- trunk/Toss/Formula/Formula.mli	2010-11-28 15:34:57 UTC (rev 1204)
+++ trunk/Toss/Formula/Formula.mli	2010-11-28 16:10:41 UTC (rev 1205)
@@ -90,8 +90,8 @@
 val sprint_real : real_expr -> string
 val fprint_real : Format.formatter -> real_expr -> unit
 
-val fprint_nobra : int -> Format.formatter -> formula -> unit
-val fprint_real_nobra : int -> Format.formatter -> real_expr -> unit
+val fprint_prec : int -> Format.formatter -> formula -> unit
+val fprint_real_prec : int -> Format.formatter -> real_expr -> unit
 
 (* --------------- BASIC HELPER FUNCTIONS USED IN PARSER ------------------- *)
 

Modified: trunk/Toss/Solver/FFSolverTest.ml
===================================================================
--- trunk/Toss/Solver/FFSolverTest.ml	2010-11-28 15:34:57 UTC (rev 1204)
+++ trunk/Toss/Solver/FFSolverTest.ml	2010-11-28 16:10:41 UTC (rev 1205)
@@ -284,7 +284,7 @@
       let heur_phi = formula_of_str
         "(((R(x, y) and R(y, z)) or (C(x, y) and C(y, z)) or ex u, v ((C(z, u) and C(y, v) and R(y, u) and R(x, v))) or ex u, v ((R(y, u) and R(x, v) and C(v, y) and C(u, z)))) and (P(z) or P(y) or P(x)) and (not Q(x)) and (not Q(y)) and (not Q(z))) and (not ex x, y, z ((((P(x) and P(y)) and P(z)) and ((((R(x, y) and R(y, z)) or (C(x, y) and C(y, z))) or ex u, v ((((R(x, v) and C(v, y)) and R(y, u)) and C(u, z)))) or ex u, v ((((R(x, v) and C(y, v)) and R(y, u)) and C(z, u)))))))"
       in
-      Printf.printf "heur_phi=%s\n%!"(Formula.str heur_phi);
+      (* Printf.printf "heur_phi=%s\n%!"(Formula.str heur_phi); *)
       let ttt = struc_of_str
 "[  | P:1 { }; Q:1 { } |  ] \"
          
@@ -294,7 +294,7 @@
          
 .  .  .  
 \"" in
-      FFTNF.debug_level := 3;
+      (* FFTNF.debug_level := 3; *)
       assert_equal ~printer:(fun x->x)
         ""
         (Formula.str (FFSolver.normalize_for_model
@@ -339,7 +339,7 @@
 ...   ...   ...   ...   
 ...   ...   ...   ...   
 \"" in
-      FFTNF.debug_level := 3;
+      (* FFTNF.debug_level := 3; *)
       assert_equal ~printer:(fun x->x)
         ""
         (Formula.str (FFSolver.normalize_for_model


This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.