[Toss-devel-svn] SF.net SVN: toss:[1581] trunk/Toss
Status: Beta
Brought to you by:
lukaszkaiser
Menu
▾
▴
[Toss-devel-svn] SF.net SVN: toss:[1581] trunk/Toss
|
From: <luk...@us...> - 2011-09-29 23:05:52
|
Revision: 1581
http://toss.svn.sourceforge.net/toss/?rev=1581&view=rev
Author: lukaszkaiser
Date: 2011-09-29 23:05:45 +0000 (Thu, 29 Sep 2011)
Log Message:
-----------
Removing wrong test, trying out some (wrong?) protection against upper-case translated vars.
Modified Paths:
--------------
trunk/Toss/GGP/GDL.ml
trunk/Toss/Solver/SolverTest.ml
Modified: trunk/Toss/GGP/GDL.ml
===================================================================
--- trunk/Toss/GGP/GDL.ml 2011-09-29 22:34:18 UTC (rev 1580)
+++ trunk/Toss/GGP/GDL.ml 2011-09-29 23:05:45 UTC (rev 1581)
@@ -74,14 +74,19 @@
"(" ^ f ^ " " ^
String.concat " " (Array.to_list (Array.map term_str args)) ^ ")"
-let rec term_to_name ?(nested=false) = function
- | Const c -> c
- | Var v -> v
- | Func (f, args) ->
- f ^ "_" ^ (if nested then "_S_" else "") ^
- String.concat "_"
- (Array.to_list (Array.map (term_to_name ~nested:true) args)) ^
- (if nested then "_Z_" else "")
+let rec term_to_name ?(nested=false) term =
+ let not_fo s = (* if strings are bad for FO vars, we add a prefix *)
+ (s = "") || (s.[0] = ':') || (s.[0] = '|') ||
+ (((Char.uppercase s.[0]) = s.[0]) && (not (Aux.is_digit s.[0]))) in
+ let s = match term with
+ | Const c -> c
+ | Var v -> v
+ | Func (f, args) ->
+ f ^ "_" ^ (if nested then "_S_" else "") ^
+ String.concat "_"
+ (Array.to_list (Array.map (term_to_name ~nested:true) args)) ^
+ (if nested then "_Z_" else "") in
+ if not_fo s then "t" ^ s else s
let rec term_vars = function
| Const _ -> Aux.Strings.empty
Modified: trunk/Toss/Solver/SolverTest.ml
===================================================================
--- trunk/Toss/Solver/SolverTest.ml 2011-09-29 22:34:18 UTC (rev 1580)
+++ trunk/Toss/Solver/SolverTest.ml 2011-09-29 23:05:45 UTC (rev 1581)
@@ -236,230 +236,6 @@
"Sum (x, y | R (x, y) : 1)" 2.;
);
-
- "eval: GDL translation tictactoe" >::
- (fun () ->
- let phi = "(cell_12(e) and cell_12(e) and
- cell_02(e) and cell_02(e) and
- control__BLANK_(ctrl) and cell_2b(e) and
- control_0xplayer(ctrl) and
- not
- (((ex cell_m5__BLANK___BLANK_
- (ex cell_m4_2__BLANK_, cell_m4_3__BLANK_
- (EQ___cell_0__cell_0(cell_m5__BLANK___BLANK_, cell_m4_2__BLANK_) and
- EQ___cell_0__cell_0(cell_m5__BLANK___BLANK_,
- cell_m4_3__BLANK_) and EQ___cell_0__cell_0(cell_m4_2__BLANK_,
- cell_m5__BLANK___BLANK_) and
- EQ___cell_0__cell_0(cell_m4_2__BLANK_, cell_m4_3__BLANK_) and
- EQ___cell_0__cell_0(cell_m4_3__BLANK_,
- cell_m5__BLANK___BLANK_) and
- EQ___cell_0__cell_0(cell_m4_3__BLANK_, cell_m4_2__BLANK_) and
- cell_11(cell_m5__BLANK___BLANK_) and
- cell_2x(cell_m5__BLANK___BLANK_) and
- cell__BLANK___BLANK___BLANK_(cell_m5__BLANK___BLANK_) and
- cell_12(cell_m4_2__BLANK_) and cell_2x(cell_m4_2__BLANK_) and
- cell__BLANK___BLANK___BLANK_(cell_m4_2__BLANK_) and
- cell_13(cell_m4_3__BLANK_) and cell_2x(cell_m4_3__BLANK_) and
- cell__BLANK___BLANK___BLANK_(cell_m4_3__BLANK_)) and
- cell__BLANK___BLANK___BLANK_(cell_m5__BLANK___BLANK_)) or
- ex cell__BLANK__m6__BLANK_
- (ex cell_2_n4__BLANK_, cell_3_n4__BLANK_
- (EQ___cell_1__cell_1(cell__BLANK__m6__BLANK_, cell_2_n4__BLANK_) and
- EQ___cell_1__cell_1(cell__BLANK__m6__BLANK_,
- cell_3_n4__BLANK_) and EQ___cell_1__cell_1(cell_2_n4__BLANK_,
- cell__BLANK__m6__BLANK_) and
- EQ___cell_1__cell_1(cell_2_n4__BLANK_, cell_3_n4__BLANK_) and
- EQ___cell_1__cell_1(cell_3_n4__BLANK_,
- cell__BLANK__m6__BLANK_) and
- EQ___cell_1__cell_1(cell_3_n4__BLANK_, cell_2_n4__BLANK_) and
- cell_01(cell__BLANK__m6__BLANK_) and
- cell_2x(cell__BLANK__m6__BLANK_) and
- cell__BLANK___BLANK___BLANK_(cell__BLANK__m6__BLANK_) and
- cell_02(cell_2_n4__BLANK_) and cell_2x(cell_2_n4__BLANK_) and
- cell__BLANK___BLANK___BLANK_(cell_2_n4__BLANK_) and
- cell_03(cell_3_n4__BLANK_) and cell_2x(cell_3_n4__BLANK_) and
- cell__BLANK___BLANK___BLANK_(cell_3_n4__BLANK_)) and
- cell__BLANK___BLANK___BLANK_(cell__BLANK__m6__BLANK_)) or
- ((ex cell_1_1__BLANK_, cell_2_2__BLANK_, cell_3_3__BLANK_
- (true and
- cell_01(cell_1_1__BLANK_) and cell_11(cell_1_1__BLANK_) and
- cell_2x(cell_1_1__BLANK_) and
- cell__BLANK___BLANK___BLANK_(cell_1_1__BLANK_) and
- cell_02(cell_2_2__BLANK_) and cell_12(cell_2_2__BLANK_) and
- cell_2x(cell_2_2__BLANK_) and
- cell__BLANK___BLANK___BLANK_(cell_2_2__BLANK_) and
- cell_03(cell_3_3__BLANK_) and cell_13(cell_3_3__BLANK_) and
- cell_2x(cell_3_3__BLANK_) and
- cell__BLANK___BLANK___BLANK_(cell_3_3__BLANK_)) or
- ex cell_1_3__BLANK_, cell_2_2__BLANK_, cell_3_1__BLANK_
- (true and
- cell_01(cell_1_3__BLANK_) and cell_13(cell_1_3__BLANK_) and
- cell_2x(cell_1_3__BLANK_) and
- cell__BLANK___BLANK___BLANK_(cell_1_3__BLANK_) and
- cell_02(cell_2_2__BLANK_) and cell_12(cell_2_2__BLANK_) and
- cell_2x(cell_2_2__BLANK_) and
- cell__BLANK___BLANK___BLANK_(cell_2_2__BLANK_) and
- cell_03(cell_3_1__BLANK_) and cell_11(cell_3_1__BLANK_) and
- cell_2x(cell_3_1__BLANK_) and
- cell__BLANK___BLANK___BLANK_(cell_3_1__BLANK_))) and
- true)) and
- true) or
- ((ex cell_m5__BLANK___BLANK_
- (ex cell_m4_2__BLANK_, cell_m4_3__BLANK_
- (EQ___cell_0__cell_0(cell_m5__BLANK___BLANK_, cell_m4_2__BLANK_) and
- EQ___cell_0__cell_0(cell_m5__BLANK___BLANK_,
- cell_m4_3__BLANK_) and EQ___cell_0__cell_0(cell_m4_2__BLANK_,
- cell_m5__BLANK___BLANK_) and
- EQ___cell_0__cell_0(cell_m4_2__BLANK_, cell_m4_3__BLANK_) and
- EQ___cell_0__cell_0(cell_m4_3__BLANK_,
- cell_m5__BLANK___BLANK_) and
- EQ___cell_0__cell_0(cell_m4_3__BLANK_, cell_m4_2__BLANK_) and
- cell_11(cell_m5__BLANK___BLANK_) and
- cell_2o(cell_m5__BLANK___BLANK_) and
- cell__BLANK___BLANK___BLANK_(cell_m5__BLANK___BLANK_) and
- cell_12(cell_m4_2__BLANK_) and cell_2o(cell_m4_2__BLANK_) and
- cell__BLANK___BLANK___BLANK_(cell_m4_2__BLANK_) and
- cell_13(cell_m4_3__BLANK_) and cell_2o(cell_m4_3__BLANK_) and
- cell__BLANK___BLANK___BLANK_(cell_m4_3__BLANK_)) and
- cell__BLANK___BLANK___BLANK_(cell_m5__BLANK___BLANK_)) or
- ex cell__BLANK__m6__BLANK_
- (ex cell_2_n4__BLANK_, cell_3_n4__BLANK_
- (EQ___cell_1__cell_1(cell__BLANK__m6__BLANK_, cell_2_n4__BLANK_) and
- EQ___cell_1__cell_1(cell__BLANK__m6__BLANK_,
- cell_3_n4__BLANK_) and EQ___cell_1__cell_1(cell_2_n4__BLANK_,
- cell__BLANK__m6__BLANK_) and
- EQ___cell_1__cell_1(cell_2_n4__BLANK_, cell_3_n4__BLANK_) and
- EQ___cell_1__cell_1(cell_3_n4__BLANK_,
- cell__BLANK__m6__BLANK_) and
- EQ___cell_1__cell_1(cell_3_n4__BLANK_, cell_2_n4__BLANK_) and
- cell_01(cell__BLANK__m6__BLANK_) and
- cell_2o(cell__BLANK__m6__BLANK_) and
- cell__BLANK___BLANK___BLANK_(cell__BLANK__m6__BLANK_) and
- cell_02(cell_2_n4__BLANK_) and cell_2o(cell_2_n4__BLANK_) and
- cell__BLANK___BLANK___BLANK_(cell_2_n4__BLANK_) and
- cell_03(cell_3_n4__BLANK_) and cell_2o(cell_3_n4__BLANK_) and
- cell__BLANK___BLANK___BLANK_(cell_3_n4__BLANK_)) and
- cell__BLANK___BLANK___BLANK_(cell__BLANK__m6__BLANK_)) or
- ((ex cell_1_1__BLANK_, cell_2_2__BLANK_, cell_3_3__BLANK_
- (true and
- cell_01(cell_1_1__BLANK_) and cell_11(cell_1_1__BLANK_) and
- cell_2o(cell_1_1__BLANK_) and
- cell__BLANK___BLANK___BLANK_(cell_1_1__BLANK_) and
- cell_02(cell_2_2__BLANK_) and cell_12(cell_2_2__BLANK_) and
- cell_2o(cell_2_2__BLANK_) and
- cell__BLANK___BLANK___BLANK_(cell_2_2__BLANK_) and
- cell_03(cell_3_3__BLANK_) and cell_13(cell_3_3__BLANK_) and
- cell_2o(cell_3_3__BLANK_) and
- cell__BLANK___BLANK___BLANK_(cell_3_3__BLANK_)) or
- ex cell_1_3__BLANK_, cell_2_2__BLANK_, cell_3_1__BLANK_
- (true and
- cell_01(cell_1_3__BLANK_) and cell_13(cell_1_3__BLANK_) and
- cell_2o(cell_1_3__BLANK_) and
- cell__BLANK___BLANK___BLANK_(cell_1_3__BLANK_) and
- cell_02(cell_2_2__BLANK_) and cell_12(cell_2_2__BLANK_) and
- cell_2o(cell_2_2__BLANK_) and
- cell__BLANK___BLANK___BLANK_(cell_2_2__BLANK_) and
- cell_03(cell_3_1__BLANK_) and cell_11(cell_3_1__BLANK_) and
- cell_2o(cell_3_1__BLANK_) and
- cell__BLANK___BLANK___BLANK_(cell_3_1__BLANK_))) and
- true)) and
- true) or
- (not
- ex cell_m7_n5__BLANK_
- (true and
- cell_2b(cell_m7_n5__BLANK_) and
- cell__BLANK___BLANK___BLANK_(cell_m7_n5__BLANK_)) and
- true)) and
- not C(e) and not e = ctrl)" in
- let struc = "[cell_1_1__BLANK_, cell_1_2__BLANK_, cell_1_3__BLANK_, cell_2_1__BLANK_,
- cell_2_2__BLANK_, cell_2_3__BLANK_, cell_3_1__BLANK_, cell_3_2__BLANK_,
- cell_3_3__BLANK_, val__b, val__o, val__oplayer, val__x, val__xplayer,
- control__BLANK_ |
- C {val__b; val__o; val__oplayer; val__x; val__xplayer; control__BLANK_};
- EQ___cell_0__cell_0 {
- (cell_1_1__BLANK_, cell_1_1__BLANK_);
- (cell_1_1__BLANK_, cell_1_2__BLANK_);
- (cell_1_1__BLANK_, cell_1_3__BLANK_);
- (cell_1_2__BLANK_, cell_1_1__BLANK_);
- (cell_1_2__BLANK_, cell_1_2__BLANK_);
- (cell_1_2__BLANK_, cell_1_3__BLANK_);
- (cell_1_3__BLANK_, cell_1_1__BLANK_);
- (cell_1_3__BLANK_, cell_1_2__BLANK_);
- (cell_1_3__BLANK_, cell_1_3__BLANK_);
- (cell_2_1__BLANK_, cell_2_1__BLANK_);
- (cell_2_1__BLANK_, cell_2_2__BLANK_);
- (cell_2_1__BLANK_, cell_2_3__BLANK_);
- (cell_2_2__BLANK_, cell_2_1__BLANK_);
- (cell_2_2__BLANK_, cell_2_2__BLANK_);
- (cell_2_2__BLANK_, cell_2_3__BLANK_);
- (cell_2_3__BLANK_, cell_2_1__BLANK_);
- (cell_2_3__BLANK_, cell_2_2__BLANK_);
- (cell_2_3__BLANK_, cell_2_3__BLANK_);
- (cell_3_1__BLANK_, cell_3_1__BLANK_);
- (cell_3_1__BLANK_, cell_3_2__BLANK_);
- (cell_3_1__BLANK_, cell_3_3__BLANK_);
- (cell_3_2__BLANK_, cell_3_1__BLANK_);
- (cell_3_2__BLANK_, cell_3_2__BLANK_);
- (cell_3_2__BLANK_, cell_3_3__BLANK_);
- (cell_3_3__BLANK_, cell_3_1__BLANK_);
- (cell_3_3__BLANK_, cell_3_2__BLANK_);
- (cell_3_3__BLANK_, cell_3_3__BLANK_)
- };
- EQ___cell_1__cell_1 {
- (cell_1_1__BLANK_, cell_1_1__BLANK_);
- (cell_1_1__BLANK_, cell_2_1__BLANK_);
- (cell_1_1__BLANK_, cell_3_1__BLANK_);
- (cell_1_2__BLANK_, cell_1_2__BLANK_);
- (cell_1_2__BLANK_, cell_2_2__BLANK_);
- (cell_1_2__BLANK_, cell_3_2__BLANK_);
- (cell_1_3__BLANK_, cell_1_3__BLANK_);
- (cell_1_3__BLANK_, cell_2_3__BLANK_);
- (cell_1_3__BLANK_, cell_3_3__BLANK_);
- (cell_2_1__BLANK_, cell_1_1__BLANK_);
- (cell_2_1__BLANK_, cell_2_1__BLANK_);
- (cell_2_1__BLANK_, cell_3_1__BLANK_);
- (cell_2_2__BLANK_, cell_1_2__BLANK_);
- (cell_2_2__BLANK_, cell_2_2__BLANK_);
- (cell_2_2__BLANK_, cell_3_2__BLANK_);
- (cell_2_3__BLANK_, cell_1_3__BLANK_);
- (cell_2_3__BLANK_, cell_2_3__BLANK_);
- (cell_2_3__BLANK_, cell_3_3__BLANK_);
- (cell_3_1__BLANK_, cell_1_1__BLANK_);
- (cell_3_1__BLANK_, cell_2_1__BLANK_);
- (cell_3_1__BLANK_, cell_3_1__BLANK_);
- (cell_3_2__BLANK_, cell_1_2__BLANK_);
- (cell_3_2__BLANK_, cell_2_2__BLANK_);
- (cell_3_2__BLANK_, cell_3_2__BLANK_);
- (cell_3_3__BLANK_, cell_1_3__BLANK_);
- (cell_3_3__BLANK_, cell_2_3__BLANK_);
- (cell_3_3__BLANK_, cell_3_3__BLANK_)
- };
- R (cell_1_1__BLANK_); R0 (cell_2_2__BLANK_); R1 (cell_3_3__BLANK_);
- R2 (cell_1_3__BLANK_); R3 (cell_3_1__BLANK_);
- cell_01 {cell_1_1__BLANK_; cell_1_2__BLANK_; cell_1_3__BLANK_};
- cell_02 {cell_2_1__BLANK_; cell_2_2__BLANK_; cell_2_3__BLANK_};
- cell_03 {cell_3_1__BLANK_; cell_3_2__BLANK_; cell_3_3__BLANK_};
- cell_11 {cell_1_1__BLANK_; cell_2_1__BLANK_; cell_3_1__BLANK_};
- cell_12 {cell_1_2__BLANK_; cell_2_2__BLANK_; cell_3_2__BLANK_};
- cell_13 {cell_1_3__BLANK_; cell_2_3__BLANK_; cell_3_3__BLANK_};
- cell_2b {
- cell_1_1__BLANK_; cell_1_2__BLANK_; cell_1_3__BLANK_; cell_2_1__BLANK_;
- cell_2_2__BLANK_; cell_2_3__BLANK_; cell_3_1__BLANK_; cell_3_2__BLANK_;
- cell_3_3__BLANK_
- };
- cell_2o:1 {}; cell_2x:1 {}; control_0oplayer:1 {};
- control_0xplayer (control__BLANK_); control__BLANK_ (control__BLANK_);
- role {val__oplayer; val__xplayer}; val__0b (val__b); val__0o (val__o);
- val__0oplayer (val__oplayer); val__0x (val__x);
- val__0xplayer (val__xplayer);
- val___BLANK_ {val__b; val__o; val__oplayer; val__x; val__xplayer}
- |
-]" in
-
- eval_eq struc phi
- "{ e->cell_2_2__BLANK_, ctrl->control__BLANK_ }";
- );
-
]
This was sent by the SourceForge.net collaborative development platform, the world's largest Open Source development site.
|
