[Toss-devel-svn] SF.net SVN: toss:[1418] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
[Toss-devel-svn] SF.net SVN: toss:[1418] trunk/Toss
|
From: <luk...@us...> - 2011-04-19 00:36:00
|
Revision: 1418
http://toss.svn.sourceforge.net/toss/?rev=1418&view=rev
Author: lukaszkaiser
Date: 2011-04-19 00:35:53 +0000 (Tue, 19 Apr 2011)
Log Message:
-----------
First attempt at fixed-points, starting slowly with Booleans.
Modified Paths:
--------------
trunk/Toss/Formula/BoolFormula.ml
trunk/Toss/Formula/BoolFormula.mli
trunk/Toss/Formula/Lexer.mll
trunk/Toss/Formula/Makefile
trunk/Toss/Formula/Sat/Sat.ml
trunk/Toss/Formula/Tokens.mly
trunk/Toss/TossFullTest.ml
trunk/Toss/TossTest.ml
Added Paths:
-----------
trunk/Toss/Formula/BoolFunction.ml
trunk/Toss/Formula/BoolFunction.mli
trunk/Toss/Formula/BoolFunctionParser.mly
trunk/Toss/Formula/BoolFunctionTest.ml
Modified: trunk/Toss/Formula/BoolFormula.ml
===================================================================
--- trunk/Toss/Formula/BoolFormula.ml 2011-04-18 18:28:26 UTC (rev 1417)
+++ trunk/Toss/Formula/BoolFormula.ml 2011-04-19 00:35:53 UTC (rev 1418)
@@ -258,30 +258,22 @@
(* Flatten conjunctions and disjunctions. *)
let rec flatten phi =
- let is_conjunction = function BAnd _ -> true | _ -> false in
- let is_disjunction = function BOr _ -> true | _ -> false in
+ let get_conjunctions = function BAnd fl -> fl | f -> [f] in
+ let get_disjunctions = function BOr fl -> fl | f -> [f] in
+ let fold_acc f xl =
+ List.fold_left (fun acc x -> (f x) @ acc) [] xl in
+ let rev_collect_conj xl = fold_acc get_conjunctions xl in
+ let rev_collect_disj xl = fold_acc get_disjunctions xl in
match phi with
| BNot (BNot psi) -> psi
| BNot (BVar v) -> BVar (-v)
| BNot psi -> BNot (flatten psi)
| BOr (flist) ->
- if not (List.exists is_disjunction flist) then
- BOr (List.map flatten flist)
- else
- (BOr (List.flatten (List.map
- (function
- | BOr psis -> List.map flatten psis
- | psi -> [flatten psi] ) flist)))
+ BOr (rev_collect_disj (List.rev_map flatten flist))
| BAnd (flist) ->
- if not (List.exists is_conjunction flist) then
- BAnd (List.map flatten flist)
- else (BAnd (List.flatten (List.map
- (function
- | BAnd psis -> List.map flatten psis
- | psi -> [flatten psi] ) flist)))
+ BAnd (rev_collect_conj (List.rev_map flatten flist))
| _ -> phi
-
(* Absorb trues and falses *)
let rec neutral_absorbing = function
| BVar _ as lit -> lit
@@ -646,25 +638,29 @@
List.filter (fun x -> List.for_all (fun y -> x=y || not(subset y x)) cnf) cnf
-let convert phi =
+let convert ?(disc_vars=[]) phi =
(* input is a Boolean combination; output is a list of list of integers
interpreted as a cnf *)
let (aux_separator, aux_cnf_formula) =
match !auxcnf_generation with
| 0 -> failwith "this function must not be called w/o auxcnf-converion"
| 1 -> (* use Tseitin conversion *)
- auxcnf_of_bool_formula
- (to_reduced_form (flatten_sort (to_nnf ~neg:false phi)))
+ auxcnf_of_bool_formula
+ (to_reduced_form (flatten (to_nnf ~neg:false phi)))
| 2 -> (* or Plaisted-Greenbaum conversion *)
- pg_auxcnf_of_bool_formula (flatten_sort (to_nnf ~neg:false phi))
+ let arg = flatten (to_nnf ~neg:false phi) in
+ if !debug_level > 0 then print_endline "CNF conv: arg computed";
+ pg_auxcnf_of_bool_formula arg
| _ -> failwith "undefined parameter value" in
if !debug_level > 0 then (
print_endline ("Separator is: " ^ string_of_int aux_separator);
- print_endline ("Converting Aux-CNF: " ^ str aux_cnf_formula);
+ if !debug_level > 1 then
+ print_endline ("Converting Aux-CNF: " ^ str aux_cnf_formula);
);
let aux_cnf = listcnf_of_boolcnf aux_cnf_formula in
- let cnf_llist = Sat.convert_aux_cnf aux_separator aux_cnf in
- if !debug_level > 0 then
+ let cnf_llist = Sat.convert_aux_cnf ~disc_vars aux_separator aux_cnf in
+ if !debug_level > 0 then print_endline ("Converted CNF. ");
+ if !debug_level > 1 then
print_endline ("Converted CNF: " ^ (Sat.cnf_str cnf_llist));
let simplified =
if (!simplification land 1) > 0 then
@@ -697,31 +693,32 @@
(* ------- Boolean quantifier elimination using CNF conversion ------- *)
-let to_cnf_basic phi =
- let cnf = convert phi in
+let to_cnf_basic ?(disc_vars=[]) phi =
+ let cnf = convert ~disc_vars phi in
neutral_absorbing
(BAnd (List.rev_map (fun lits -> BOr (List.map lit_of_int lits)) cnf))
-let to_cnf ?(tm=1200.) phi =
+let to_cnf ?(disc_vars=[]) ?(tm=1200.) phi =
try
Sat.set_timeout tm;
- let res = to_cnf_basic phi in
+ let res = to_cnf_basic ~disc_vars phi in
Sat.clear_timeout ();
Some (res)
with Aux.Timeout _ -> None
-let try_cnf tm phi =
- match to_cnf ~tm phi with None -> phi | Some psi -> psi
+let try_cnf ?(disc_vars=[]) tm phi =
+ match to_cnf ~disc_vars ~tm phi with None -> phi | Some psi -> psi
-let to_dnf_basic phi = to_nnf ~neg:true (to_cnf_basic (to_nnf ~neg:true phi))
+let to_dnf_basic ?(disc_vars=[]) phi =
+ to_nnf ~neg:true (to_cnf_basic ~disc_vars (to_nnf ~neg:true phi))
-let to_dnf ?(tm=1200.) phi =
- match to_cnf ~tm (to_nnf ~neg:true phi) with
+let to_dnf ?(disc_vars=[]) ?(tm=1200.) phi =
+ match to_cnf ~disc_vars ~tm (to_nnf ~neg:true phi) with
| None -> None
| Some psi -> Some (to_nnf ~neg:true psi)
-let try_dnf tm phi =
- match to_dnf ~tm phi with None -> phi | Some psi -> psi
+let try_dnf ?(disc_vars=[]) tm phi =
+ match to_dnf ~disc_vars ~tm phi with None -> phi | Some psi -> psi
let univ ?(dbg=0) v phi =
if dbg > 0 then Printf.printf "Univ subst in %s\n%!" (str phi);
@@ -744,7 +741,7 @@
let (tm_jump, cutvar, has_vars_mem) = (1.1, 3, Hashtbl.create 31)
-let _ = debug_elim := false
+let _ () = debug_elim := true
(* Returns a quantifier-free formula equivalent to All (vars, phi).
The list [vars] contains only positive literals and [phi] is in NNF. *)
@@ -764,7 +761,7 @@
let (simp_fs, _) = List.fold_left do_elim ([], 0) fs in
if !debug_elim then Printf.printf "%s done %!" prefix;
let res = match to_dnf ~tm:(5. *. tout) (BAnd simp_fs) with
- | None ->
+ | None ->
if !debug_elim then
Printf.printf "(non-dnf %i)\n%!" (size (BAnd simp_fs));
BAnd simp_fs
@@ -826,7 +823,7 @@
if !debug_elim then
Printf.printf "%s vars %i list %i (cnf conv) %!" prefix
(List.length vars) (List.length fs);
- let bool_cnf = match to_cnf ~tm:(3. *. tout) phi with
+ let bool_cnf = match to_cnf ~disc_vars:vars ~tm:(3.*.tout) phi with
| None -> raise (Aux.Timeout "!!none")
| Some psi -> psi in
if !debug_elim then Printf.printf "success \n%!";
@@ -972,7 +969,7 @@
| None ->
if !debug_elim then (
Printf.printf "EX ELIM NO DNF\n%!";
- Printf.printf "%s \n%!" (str res_raw);
+ (* Printf.printf "%s \n%!" (str res_raw); *)
);
res_raw
| Some r ->
@@ -989,7 +986,7 @@
| None ->
if !debug_elim then (
Printf.printf "ALL ELIM NO CNF\n%!";
- Printf.printf "%s \n%!" (str res_raw);
+ (* Printf.printf "%s \n%!" (str res_raw); *)
);
res_raw
| Some r ->
Modified: trunk/Toss/Formula/BoolFormula.mli
===================================================================
--- trunk/Toss/Formula/BoolFormula.mli 2011-04-18 18:28:26 UTC (rev 1417)
+++ trunk/Toss/Formula/BoolFormula.mli 2011-04-19 00:35:53 UTC (rev 1418)
@@ -49,7 +49,7 @@
(** Convert a Boolean formula to NNF and additionally negate if [neg] is set. *)
val to_nnf : ?neg : bool -> bool_formula -> bool_formula
-val convert : bool_formula -> int list list
+val convert : ?disc_vars: int list -> bool_formula -> int list list
(** Convert an arbitrary formula to CNF via Boolean combinations. *)
val formula_to_cnf : Formula.formula -> Formula.formula
Added: trunk/Toss/Formula/BoolFunction.ml
===================================================================
--- trunk/Toss/Formula/BoolFunction.ml (rev 0)
+++ trunk/Toss/Formula/BoolFunction.ml 2011-04-19 00:35:53 UTC (rev 1418)
@@ -0,0 +1,131 @@
+(* Represent Boolean functions. *)
+
+let debug_level = ref 0
+let set_debug_level i = (debug_level := i;)
+
+
+(* ----------------------- BASIC TYPE DEFINITION -------------------------- *)
+
+(* This type describes Boolean functions *)
+type bool_function =
+ | Fun of string * string list
+ | PosVar of string * string
+ | NegVar of string * string
+ | Not of bool_function
+ | And of bool_function list
+ | Or of bool_function list
+ | Ex of (string * string) list * bool_function
+ | Mu of string * (string * string) list * bool_function
+
+
+(* ----------------------- PRINTING FUNCTIONS ------------------------------- *)
+
+(* Print to formatter. *)
+let rec fprint f = function
+ | Fun (s, vars) ->
+ Format.fprintf f "%s(%a)" s
+ (Aux.fprint_sep_list "," (fun f s -> Format.fprintf f "%s" s)) vars
+ | PosVar (m, n) -> Format.fprintf f "%s.%s=1" m n
+ | NegVar (m, n) -> Format.fprintf f "%s.%s=0" m n
+ | Not phi -> Format.fprintf f "@[<1>!%a@]" fprint phi
+ | And [] -> Format.fprintf f "true"
+ | Or [] -> Format.fprintf f "false"
+ | And [phi] -> fprint f phi
+ | Or [phi] -> fprint f phi
+ | And flist ->
+ Format.fprintf f "@[<1>(%a)@]" (Aux.fprint_sep_list " &" fprint) flist
+ | Or flist ->
+ Format.fprintf f "@[<1>(%a)@]" (Aux.fprint_sep_list " |" fprint) flist
+ | Ex (mod_vars, phi) ->
+ let fprint_mod_var f (md, vn) = Format.fprintf f "%s %s" md vn in
+ Format.fprintf f "@[<1>(exists@ %a.@ %a)@]"
+ (Aux.fprint_sep_list "," fprint_mod_var) mod_vars fprint phi
+ | Mu (name, mod_vars, def) ->
+ let fprint_mod_var f (md, vn) = Format.fprintf f "%s %s" md vn in
+ Format.fprintf f "@[<1>mu bool %s(%a)@ %a@]" name
+ (Aux.fprint_sep_list "," fprint_mod_var) mod_vars fprint def
+
+(* Print to stdout. *)
+let print phi = (
+ Format.print_flush();
+ fprint Format.std_formatter phi;
+ Format.print_flush();
+)
+
+(* Print to string. *)
+let sprint phi =
+ ignore (Format.flush_str_formatter ());
+ Format.fprintf Format.str_formatter "@[%a@]" fprint phi;
+ Format.flush_str_formatter ()
+
+(* Another name for sprint. *)
+let str f = sprint f
+
+(* --------------------- BASIC FUNCTIONS ------------------------ *)
+
+(* Compute the size of a Boolean function. *)
+let rec size ?(acc=0) = function
+ | Fun _ | PosVar _ | NegVar _ -> acc + 1
+ | Not phi | Ex (_, phi) | Mu (_, _, phi) -> size ~acc:(acc + 1) phi
+ | And flist | Or flist ->
+ List.fold_left (fun i f -> size ~acc:i f) (acc + 1) flist
+
+(* Convert a Boolean function to NNF, additionally negate if [neg] is set. *)
+let rec to_nnf ?(neg=false) = function
+ | Fun (n, a) -> if neg then Not (Fun (n, a)) else Fun (n, a)
+ | PosVar (m, n) -> if neg then NegVar (m, n) else PosVar (m, n)
+ | NegVar (m, n) -> if neg then PosVar (m, n) else NegVar (m, n)
+ | Not phi -> if neg then to_nnf ~neg:false phi else to_nnf ~neg:true phi
+ | And (flist) when neg -> Or (List.map (to_nnf ~neg:true) flist)
+ | And (flist) -> And (List.map (to_nnf ~neg:false) flist)
+ | Or (flist) when neg -> And (List.map (to_nnf ~neg:true) flist)
+ | Or (flist) -> Or (List.map (to_nnf ~neg:false) flist)
+ | x -> if neg then Not x else x
+
+(* Flatten conjunctions and disjunctions, apply [f] to the lists. *)
+let rec flatten_f f phi =
+ let get_conjunctions = function And fl -> fl | f -> [f] in
+ let get_disjunctions = function Or fl -> fl | f -> [f] in
+ let fold_acc f xl =
+ List.fold_left (fun acc x -> (f x) @ acc) [] xl in
+ let rev_collect_conj xl = fold_acc get_conjunctions xl in
+ let rev_collect_disj xl = fold_acc get_disjunctions xl in
+ match phi with
+ | Not (Not psi) -> psi
+ | Not (PosVar (m, n)) -> NegVar (m, n)
+ | Not (NegVar (m, n)) -> PosVar (m, n)
+ | Not psi -> Not (flatten_f f psi)
+ | Or (flist) ->
+ Or (f (rev_collect_disj (List.rev_map (flatten_f f) flist)))
+ | And (flist) ->
+ And (f (rev_collect_conj (List.rev_map (flatten_f f) flist)))
+ | Ex (vs, phi) -> Ex (vs, flatten_f f phi)
+ | Mu (n, vs, phi) -> Mu (n, vs, flatten_f f phi)
+ | _ -> phi
+
+(* Just Flatten. *)
+let flatten psi = flatten_f (fun x -> x) psi
+
+(* Flatten and sort. *)
+let flatten_sort psi = flatten_f (List.sort Pervasives.compare) psi
+
+(* Flatten and perform trivial simplifications (e.g. absorb true, false) *)
+let rec triv_simp phi = match flatten phi with
+ | Fun _ | PosVar _ | NegVar _ as lit -> lit
+ | Not psi -> Not (triv_simp psi)
+ | Or psis ->
+ if (List.exists (fun psi -> psi = And []) psis) then (And []) else
+ let filtered_once = List.filter (fun psi -> psi <> Or []) psis in
+ let new_psis = List.map triv_simp filtered_once in
+ let filtered = List.filter (fun psi -> psi <> Or []) new_psis in
+ if (List.exists (fun psi -> psi = And []) filtered) then (And []) else
+ Or filtered
+ | And psis ->
+ if (List.exists (fun psi -> psi = Or []) psis) then (Or []) else
+ let filtered_once = List.filter (fun psi -> psi <> And []) psis in
+ let new_psis = List.map triv_simp filtered_once in
+ let filtered = List.filter (fun psi -> psi <> And []) new_psis in
+ if (List.exists (fun psi -> psi = Or []) filtered) then (Or []) else
+ And filtered
+ | Ex (vs, phi) -> Ex (vs, triv_simp phi)
+ | Mu (n, vs, phi) -> Mu (n, vs, triv_simp phi)
Added: trunk/Toss/Formula/BoolFunction.mli
===================================================================
--- trunk/Toss/Formula/BoolFunction.mli (rev 0)
+++ trunk/Toss/Formula/BoolFunction.mli 2011-04-19 00:35:53 UTC (rev 1418)
@@ -0,0 +1,47 @@
+(** Represent Boolean functions. *)
+
+(** {2 Debugging} *)
+
+(** Set debugging level. *)
+val set_debug_level : int -> unit
+
+
+(** {2 Basic Type Definition} *)
+
+(** This type describes Boolean functions *)
+type bool_function =
+ | Fun of string * string list
+ | PosVar of string * string
+ | NegVar of string * string
+ | Not of bool_function
+ | And of bool_function list
+ | Or of bool_function list
+ | Ex of (string * string) list * bool_function
+ | Mu of string * (string * string) list * bool_function
+
+
+(** {2 Printing Functions} *)
+
+(** Print to stdout. *)
+val print : bool_function -> unit
+
+(** Print to string. *)
+val sprint : bool_function -> string
+
+(** Another name for sprint. *)
+val str : bool_function -> string
+
+(** Print to formatter. *)
+val fprint : Format.formatter -> bool_function -> unit
+
+
+(** {2 Basic Functions} *)
+
+(** Compute the size of a Boolean function. *)
+val size : ?acc : int -> bool_function -> int
+
+(** Flatten conjunctions and disjunctions. *)
+val flatten : bool_function -> bool_function
+
+(** Flatten and perform trivial simplifications (e.g. absorb true, false) *)
+val triv_simp : bool_function -> bool_function
Added: trunk/Toss/Formula/BoolFunctionParser.mly
===================================================================
--- trunk/Toss/Formula/BoolFunctionParser.mly (rev 0)
+++ trunk/Toss/Formula/BoolFunctionParser.mly 2011-04-19 00:35:53 UTC (rev 1418)
@@ -0,0 +1,46 @@
+/* Tokens taken from Lexer.mll */
+
+%{
+ open Lexer
+ open BoolFunction
+%}
+
+%start parse_bool_function
+%type <BoolFunction.bool_function> parse_bool_function bool_function_expr
+
+
+%%
+
+id_pair:
+ | ID ID { ($1, $2) }
+
+%public bool_function_expr:
+ | TRUE { And [] }
+ | FALSE { Or [] }
+ | bool_function_expr AND bool_function_expr { And [$1; $3] }
+ | bool_function_expr OR bool_function_expr { Or [$1; $3] }
+ | bool_function_expr AMP bool_function_expr { And [$1; $3] }
+ | bool_function_expr MID bool_function_expr { Or [$1; $3] }
+ | bool_function_expr RARR bool_function_expr { Or [Not ($1); $3] }
+ | bool_function_expr LRARR bool_function_expr
+ { Or [And [Not ($1); Not ($3)]; And [$1; $3]] }
+ | bool_function_expr XOR bool_function_expr
+ { And [Or [$1; $3]; Not (And [$1; $3])] }
+ | ID DOT ID EQ INT
+ { if $5 = 0 then NegVar($1, $3) else PosVar($1, $3) }
+ | NOT ID DOT ID { NegVar ($2, $4) }
+ | ID DOT ID { PosVar ($1, $3) }
+ | name = ID args = delimited (OPEN, separated_list (COMMA, ID), CLOSE)
+ { Fun (name, args) }
+ | EX vars = separated_list (COMMA, id_pair) phi = bool_function_expr
+ { Ex (vars, phi) }
+ | EX vars = separated_list (COMMA, id_pair) DOT phi = bool_function_expr
+ { Ex (vars, phi) }
+ | LFP n = ID vars = separated_list (COMMA, id_pair) phi = bool_function_expr
+ { Mu (n, vars, phi) }
+ | NOT bool_function_expr { Not ($2) }
+ | OPEN bool_function_expr CLOSE { $2 }
+
+
+parse_bool_function:
+ | bool_function_expr EOF { triv_simp $1 };
Added: trunk/Toss/Formula/BoolFunctionTest.ml
===================================================================
--- trunk/Toss/Formula/BoolFunctionTest.ml (rev 0)
+++ trunk/Toss/Formula/BoolFunctionTest.ml 2011-04-19 00:35:53 UTC (rev 1418)
@@ -0,0 +1,39 @@
+open OUnit
+open BoolFunction
+
+let _ = ( BoolFunction.set_debug_level 0; )
+
+let bf_of_string s =
+ BoolFunctionParser.parse_bool_function Lexer.lex (Lexing.from_string s)
+
+let assert_eq_string arg msg x y =
+ let full_msg = msg ^ " (argument: " ^ arg ^ ")" in
+ assert_equal ~printer:(fun x -> x) ~msg:full_msg
+ ("\n" ^ x ^ "\n") ("\n" ^ y ^ "\n")
+
+let tests = "BoolFunction" >::: [
+ "parsing and printing" >::
+ (fun () ->
+ let test_parse_print s res =
+ assert_eq_string s "Parse and Print" res (str (bf_of_string s)) in
+
+ test_parse_print "MyRel (m)" "MyRel(m)";
+ test_parse_print "Rel (m) | m.a1 = 0" "(Rel(m) | m.a1=0)";
+ test_parse_print "(R(m)&m.a1=1)|m.a2=0" "((R(m) & m.a1=1) | m.a2=0)";
+ test_parse_print
+ ("(false |((m.a1=0 & m.a2=0 & m.a3=0)) " ^
+ "|((m.a1=0 & m.a2=1 & m.a3=0)) |((m.a1=1 & m.a2=1 & m.a3=0)))")
+ ("((m.a1=0 & m.a2=0 & m.a3=0) | (m.a1=0 & m.a2=1 & m.a3=0) |\n " ^
+ "(m.a1=1 & m.a2=1 & m.a3=0))");
+ test_parse_print "true & !pc.b1 & !pc.b2 & !pc.b3"
+ "(pc.b1=0 & pc.b2=0 & pc.b3=0)";
+ test_parse_print "(false | (true))" "true";
+ test_parse_print ("(exists M t_mod, PC t_pc, Loc tL, Glob tG. (" ^
+ "target(t_mod,t_pc) & Reach(t_mod, t_pc, tL, tG)))")
+ ("(exists M t_mod, PC t_pc, Loc tL, Glob tG.\n " ^
+ "(target(t_mod, t_pc) & Reach(t_mod, t_pc, tL, tG)))");
+ );
+]
+
+let exec = Aux.run_test_if_target "BoolFunctionTest" tests
+
Modified: trunk/Toss/Formula/Lexer.mll
===================================================================
--- trunk/Toss/Formula/Lexer.mll 2011-04-18 18:28:26 UTC (rev 1417)
+++ trunk/Toss/Formula/Lexer.mll 2011-04-19 00:35:53 UTC (rev 1418)
@@ -8,6 +8,8 @@
| COLON
| SEMICOLON
| COMMA
+ | DOT
+ | AMP
| MID
| SUM
| PLUS
@@ -77,6 +79,7 @@
| STATE_SPEC
| LEFT_SPEC
| RIGHT_SPEC
+ | LFP
| EOF
let reset_as_file lexbuf s =
@@ -137,6 +140,8 @@
| ':' { COLON }
| ';' { SEMICOLON }
| ',' { COMMA }
+ | '.' { DOT }
+ | '&' { AMP }
| '|' { MID }
| "Sum" { SUM }
| '+' { PLUS }
@@ -151,6 +156,7 @@
| '=' { EQ }
| "<>" { LTGR }
| "!=" { NEQ }
+ | "!" { NOT }
| "<-" { LARR }
| "<=" { LDARR }
| "->" { RARR }
@@ -170,6 +176,7 @@
| "xor" { XOR }
| "not" { NOT }
| "ex" { EX }
+ | "exists" { EX }
| "all" { ALL }
| "tc" { TC }
| "TC" { TC }
@@ -208,6 +215,9 @@
| "STATE" { STATE_SPEC }
| "LEFT" { LEFT_SPEC }
| "RIGHT" { RIGHT_SPEC }
+ | "LFP" { LFP }
+ | "lfp" { LFP }
+ | "mu" { LFP }
| ['0'-'9']+ as n { INT (int_of_string n) }
| '-' ['0'-'9']+ as n { INT (int_of_string n) }
| ['0'-'9']* '.' ['0'-'9']+ as x { FLOAT (float_of_string x) }
Modified: trunk/Toss/Formula/Makefile
===================================================================
--- trunk/Toss/Formula/Makefile 2011-04-18 18:28:26 UTC (rev 1417)
+++ trunk/Toss/Formula/Makefile 2011-04-19 00:35:53 UTC (rev 1418)
@@ -6,6 +6,7 @@
AuxTest:
FormulaTest:
BoolFormulaTest:
+BoolFunctionTest:
FormulaOpsTest:
FFTNFTest:
Modified: trunk/Toss/Formula/Sat/Sat.ml
===================================================================
--- trunk/Toss/Formula/Sat/Sat.ml 2011-04-18 18:28:26 UTC (rev 1417)
+++ trunk/Toss/Formula/Sat/Sat.ml 2011-04-19 00:35:53 UTC (rev 1418)
@@ -259,16 +259,18 @@
let convert_aux_cnf ?(disc_vars=[]) ?(bound=None) aux_separator aux_cnf =
(match bound with Some i -> max_clause := i | None -> max_clause := -1;);
cur_clause := 0;
- if !debug_level > 0 then print_endline (" converting: " ^ (cnf_str aux_cnf));
+ if !debug_level > 0 then print_endline (" converting in Sat ");
+ if !debug_level > 1 then print_endline (" converting: " ^ (cnf_str aux_cnf));
let (bound, cnf_form) = (aux_separator, aux_cnf) in
- if !debug_level > 2 then
- print_endline (" formula for sat: " ^ (cnf_str cnf_form));
register_new_formula cnf_form;
MiniSAT.set_threshold bound;
let rec lit_set acc = function
[] -> acc
| x :: xs -> lit_set (List.fold_left (fun s i-> IntSet.add i s) acc x) xs in
- let f = perform_conversion disc_vars (lit_set IntSet.empty cnf_form) cnf_form bound [] in
+ let literals = (lit_set IntSet.empty cnf_form) in
+ if !debug_level > 0 then print_endline (" starting converting in Sat ");
+ let f = perform_conversion disc_vars literals cnf_form bound [] in
let form = List.rev_map (fun cl -> List.map (fun v -> -v) cl) f in
- if !debug_level > 0 then print_endline (" converted: " ^ (cnf_str form));
+ if !debug_level > 0 then print_endline (" converted in Sat ");
+ if !debug_level > 1 then print_endline (" converted: " ^ (cnf_str form));
simplify [] (simplify [] form)
Modified: trunk/Toss/Formula/Tokens.mly
===================================================================
--- trunk/Toss/Formula/Tokens.mly 2011-04-18 18:28:26 UTC (rev 1417)
+++ trunk/Toss/Formula/Tokens.mly 2011-04-19 00:35:53 UTC (rev 1418)
@@ -3,7 +3,7 @@
%token <float> FLOAT
%token <string> BOARD_STRING
%token APOSTROPHE
-%token COLON SEMICOLON COMMA MID
+%token COLON SEMICOLON COMMA DOT AMP MID
%token SUM PLUS MINUS TIMES DIV POW GR GREQ LT EQLT EQ LTGR NEQ
%token LARR LDARR RARR RDARR LRARR LRDARR INTERV
%token OPENCUR CLOSECUR OPENSQ CLOSESQ OPEN CLOSE
@@ -11,7 +11,7 @@
%token WITH EMB PRE INV POST UPDATE DYNAMICS TRUE FALSE ASSOC COND PAYOFF MOVES
%token ADD_CMD DEL_CMD GET_CMD SET_CMD EVAL_CMD
%token ELEM_MOD REL_MOD ALLOF_MOD SIG_MOD FUN_MOD DATA_MOD LOC_MOD TIMEOUT_MOD TIME_MOD PLAYER_MOD PLAYERS_MOD
-%token MODEL_SPEC RULE_SPEC STATE_SPEC LEFT_SPEC RIGHT_SPEC EOF
+%token MODEL_SPEC RULE_SPEC STATE_SPEC LEFT_SPEC RIGHT_SPEC LFP EOF
/* List in order of increasing precedence. */
%nonassoc COND
Modified: trunk/Toss/TossFullTest.ml
===================================================================
--- trunk/Toss/TossFullTest.ml 2011-04-18 18:28:26 UTC (rev 1417)
+++ trunk/Toss/TossFullTest.ml 2011-04-19 00:35:53 UTC (rev 1418)
@@ -6,6 +6,7 @@
SatTest.tests;
BoolFormulaTest.tests;
BoolFormulaTest.bigtests;
+ BoolFunctionTest.tests;
FormulaOpsTest.tests;
FFTNFTest.tests;
]
Modified: trunk/Toss/TossTest.ml
===================================================================
--- trunk/Toss/TossTest.ml 2011-04-18 18:28:26 UTC (rev 1417)
+++ trunk/Toss/TossTest.ml 2011-04-19 00:35:53 UTC (rev 1418)
@@ -5,6 +5,7 @@
FormulaTest.tests;
SatTest.tests;
BoolFormulaTest.tests;
+ BoolFunctionTest.tests;
FormulaOpsTest.tests;
FFTNFTest.tests;
]
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
