[Toss-devel-svn] SF.net SVN: toss:[1643] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
[Toss-devel-svn] SF.net SVN: toss:[1643] trunk/Toss
|
From: <luk...@us...> - 2012-01-17 22:23:35
|
Revision: 1643
http://toss.svn.sourceforge.net/toss/?rev=1643&view=rev
Author: lukstafi
Date: 2012-01-17 22:23:28 +0000 (Tue, 17 Jan 2012)
Log Message:
-----------
js_of_ocaml-friendly changes: pa_macro-based conditional compilation of RealQuantElim and Unix references.
Modified Paths:
--------------
trunk/Toss/Formula/Aux.ml
trunk/Toss/Formula/Aux.mli
trunk/Toss/Formula/FormulaParser.mly
trunk/Toss/Formula/Lexer.mll
trunk/Toss/Formula/Tokens.mly
trunk/Toss/Makefile
trunk/Toss/Solver/Solver.ml
trunk/Toss/www/reference/reference.tex
Modified: trunk/Toss/Formula/Aux.ml
===================================================================
--- trunk/Toss/Formula/Aux.ml 2012-01-17 02:25:49 UTC (rev 1642)
+++ trunk/Toss/Formula/Aux.ml 2012-01-17 22:23:28 UTC (rev 1643)
@@ -1,7 +1,11 @@
(* Auxiliary functions that operate on standard library data
structures and standard library-like definitions. *)
-let gettimeofday () = Unix.gettimeofday (); (* 1. *)
+let gettimeofday () =
+ IFDEF NOUNIX
+ THEN 1.
+ ELSE Unix.gettimeofday ()
+ ENDIF
exception Timeout of string
Modified: trunk/Toss/Formula/Aux.mli
===================================================================
--- trunk/Toss/Formula/Aux.mli 2012-01-17 02:25:49 UTC (rev 1642)
+++ trunk/Toss/Formula/Aux.mli 2012-01-17 22:23:28 UTC (rev 1643)
@@ -52,7 +52,7 @@
(** Random element of a list. *)
val random_elem : 'a list -> 'a
-(** Concatenate results of a function. *)
+(** Concatenate results of a function. Tail-recursive. *)
val concat_map : ('a -> 'b list) -> 'a list -> 'b list
(** Map a second list and prepend the result to the first list, by
Modified: trunk/Toss/Formula/FormulaParser.mly
===================================================================
--- trunk/Toss/Formula/FormulaParser.mly 2012-01-17 02:25:49 UTC (rev 1642)
+++ trunk/Toss/Formula/FormulaParser.mly 2012-01-17 22:23:28 UTC (rev 1643)
@@ -55,7 +55,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 re = real_expr
+ | COLON LET_CMD COLON v = ID EQ def = real_expr IN_MOD re = real_expr
{ RLet (":" ^ v, def, re) }
real_ineq:
@@ -88,13 +88,13 @@
| MINUS ID OPEN fo_var_list CLOSE { Rel ("-"^$2, Array.of_list $4) }
| ID EQ ID { Eq (fo_var_of_s $1, fo_var_of_s $3) }
| ID NEQ ID { Not(Eq (fo_var_of_s $1,fo_var_of_s $3))}
- | ID IN ID { In (fo_var_of_s $1, mso_var_of_s $3) }
+ | ID IN_MOD ID { In (fo_var_of_s $1, mso_var_of_s $3) }
| real_ineq { let (p, s) = $1 in RealExpr (p, s) }
| NOT formula_expr { Not ($2) }
| EX var_list formula_expr { Ex ($2, $3) }
| ALL var_list formula_expr { All ($2, $3) }
| TC ID COMMA ID formula_expr { FormulaSubst.make_lfp_tc $2 $4 $5 }
- | TC IN ID COMMA ID formula_expr { FormulaSubst.make_mso_tc $3 $5 $6 }
+ | TC IN_MOD ID COMMA ID formula_expr { FormulaSubst.make_mso_tc $3 $5 $6 }
| TC INT ID COMMA ID formula_expr { FormulaSubst.make_fo_tc_conj $2 $3 $5 $6 }
| LFP ID OPEN fo_var_list CLOSE EQ formula_expr
{ let vs = Array.of_list $4 in if Array.length vs <> 1 then
@@ -120,7 +120,7 @@
{ 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 phi = formula_expr
+ EQ body = formula_expr IN_MOD phi = formula_expr
{ Let (rel, args, body, phi) } %prec LET_CMD
Modified: trunk/Toss/Formula/Lexer.mll
===================================================================
--- trunk/Toss/Formula/Lexer.mll 2012-01-17 02:25:49 UTC (rev 1642)
+++ trunk/Toss/Formula/Lexer.mll 2012-01-17 22:23:28 UTC (rev 1643)
@@ -1,9 +1,11 @@
{
+ let test = "test"
+
type token =
- | ID of (string)
- | INT of (int)
- | FLOAT of (float)
- | BOARD_STRING of (string)
+ | ID of string
+ | INT of int
+ | FLOAT of float
+ | BOARD_STRING of string
| APOSTROPHE
| COLON
| SEMICOLON
@@ -37,7 +39,7 @@
| CLOSESQ
| OPEN
| CLOSE
- | IN
+ | IN_MOD
| AND
| OR
| XOR
@@ -176,7 +178,7 @@
| '}' { CLOSECUR }
| '[' { OPENSQ }
| ']' { CLOSESQ }
- | "in" { IN }
+ | "in" { IN_MOD }
| "and" { AND }
| "or" { OR }
| "xor" { XOR }
Modified: trunk/Toss/Formula/Tokens.mly
===================================================================
--- trunk/Toss/Formula/Tokens.mly 2012-01-17 02:25:49 UTC (rev 1642)
+++ trunk/Toss/Formula/Tokens.mly 2012-01-17 22:23:28 UTC (rev 1643)
@@ -7,7 +7,7 @@
%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
-%token IN AND OR XOR NOT EX ALL TC
+%token IN_MOD AND OR XOR NOT EX ALL TC
%token WITH EMB PRE INV POST UPDATE DYNAMICS TRUE FALSE ASSOC COND PAYOFF MOVES
%token MATCH ADD_CMD DEL_CMD GET_CMD SET_CMD LET_CMD EVAL_CMD
%token ELEM_MOD ELEMS_MOD REL_MOD RELS_MOD ALLOF_MOD SIG_MOD FUN_MOD DATA_MOD LOC_MOD TIMEOUT_MOD TIME_MOD PLAYER_MOD PLAYERS_MOD
@@ -26,7 +26,7 @@
%left OR
%left AND
%left COMMA
-%nonassoc EQ IN
+%nonassoc EQ IN_MOD
%left NOT EX ALL
%%
Modified: trunk/Toss/Makefile
===================================================================
--- trunk/Toss/Makefile 2012-01-17 02:25:49 UTC (rev 1642)
+++ trunk/Toss/Makefile 2012-01-17 22:23:28 UTC (rev 1643)
@@ -35,14 +35,16 @@
# -------- MAIN OCAMLBUILD PART --------
-OCB_LFLAG=-lflags -I,+oUnit,-I,+sqlite3,-I,+js_of_ocaml,-I,+site-lib/oUnit,-I,+site-lib/sqlite3
-OCB_CFLAG=-cflags -I,+oUnit,-I,+sqlite3,-I,+js_of_ocaml,-I,+site-lib/oUnit,-I,+site-lib/sqlite3,-g
+# TODO: Hard-coded path to js_of_ocaml.
+OCB_LFLAG=-lflags -I,/usr/local/lib/ocaml/3.12.0/js_of_ocaml,-I,+oUnit,-I,+sqlite3,-I,+js_of_ocaml,-I,+site-lib/oUnit,-I,+site-lib/sqlite3
+OCB_CFLAG=-cflags -I,/usr/local/lib/ocaml/3.12.0/js_of_ocaml,-I,+oUnit,-I,+sqlite3,-I,+js_of_ocaml,-I,+site-lib/oUnit,-I,+site-lib/sqlite3,-g
OCB_LIB=-libs str,nums,unix,oUnit,sqlite3
OCB_LIBJS=-libs str,js_of_ocaml
-OCB_PP=-pp "camlp4o ../caml_extensions/pa_let_try.cmo js_of_ocaml/pa_js.cmo"
+OCB_PP=-pp "camlp4o -I /usr/local/lib/ocaml/3.12.0 ../caml_extensions/pa_let_try.cmo pa_macro.cmo js_of_ocaml/pa_js.cmo"
+OCB_PPJS=-pp "camlp4o -I /usr/local/lib/ocaml/3.12.0 ../caml_extensions/pa_let_try.cmo pa_macro.cmo -DNOREALQE -DNOUNIX js_of_ocaml/pa_js.cmo"
OCAMLBUILD=ocamlbuild -log build.log -j 8 -menhir ../menhir_conf $(OCB_PP) \
$(OCB_LIB) $(OCB_CFLAG) $(OCB_LFLAG)
-OCAMLBUILDJS=ocamlbuild -log build.log -j 8 -menhir ../menhir_conf $(OCB_PP) \
+OCAMLBUILDJS=ocamlbuild -log build.log -j 8 -menhir ../menhir_conf $(OCB_PPJS) \
$(OCB_LIBJS) $(OCB_CFLAG) $(OCB_LFLAG)
OCAMLBUILDNOPP=ocamlbuild -log build.log -j 8 -menhir ../menhir_conf \
$(OCB_LIB) $(OCB_CFLAG) $(OCB_LFLAG)
Modified: trunk/Toss/Solver/Solver.ml
===================================================================
--- trunk/Toss/Solver/Solver.ml 2012-01-17 02:25:49 UTC (rev 1642)
+++ trunk/Toss/Solver/Solver.ml 2012-01-17 22:23:28 UTC (rev 1643)
@@ -265,10 +265,14 @@
| [] ->
let poly = poly_of assgn p in
if check then
- if not (RealQuantElim.sat [(poly, sgn)]) then Empty else
- if RealQuantElim.sat [(poly, SignTable.neg_sign_op sgn)] then
- Real [[(poly, sgn)]]
- else Any
+ (IFDEF NOREALQE
+ THEN failwith "Solver.ml: RealQuantElim is not enabled"
+ ELSE
+ ( if not (RealQuantElim.sat [(poly, sgn)]) then Empty else
+ if RealQuantElim.sat [(poly, SignTable.neg_sign_op sgn)] then
+ Real [[(poly, sgn)]]
+ else Any)
+ ENDIF)
else Real [[(poly, sgn)]]
| v :: vs ->
let append_elem_asg acc e =
Modified: trunk/Toss/www/reference/reference.tex
===================================================================
--- trunk/Toss/www/reference/reference.tex 2012-01-17 02:25:49 UTC (rev 1642)
+++ trunk/Toss/www/reference/reference.tex 2012-01-17 22:23:28 UTC (rev 1643)
@@ -1226,7 +1226,10 @@
\[ \tp^{n-1,k}(\frakA,\ol{a}) \ \land\
\Land_{\sfx \in V} \Land_{g \in G_\sfx} \tau_{\sfx, g}. \]
+\section{Distinguishing Structures}
+
+
\section{Learning Games}
Let us start by showing how to learn two-player zero-sum games with payoffs only
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|