OKlibrary  0.2.1.6
Formulas.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 9.2.2008 (Swansea) */
00002 /* Copyright 2008, 2009 Oliver Kullmann
00003 This file is part of the OKlibrary. OKlibrary is free software; you can redistribute
00004 it and/or modify it under the terms of the GNU General Public License as published by
00005 the Free Software Foundation and included in this library; either version 3 of the
00006 License, or any later version. */
00007 
00022 oklib_include("OKlib/ComputerAlgebra/TestSystem/Lisp/Asserts.mac")$
00023 
00024 kill(f)$
00025 
00026 /* ***********************************
00027    * Representation of formulas      *
00028    ***********************************
00029 */
00030 
00031 okltest_var_prpl(f) := block([v],
00032   assert(f(v) = {v}),
00033   assert(f(neg(v)) = {v}),
00034   assert(f(true) = {}),
00035   assert(f(false) = {}),
00036   true)$
00037 
00038 okltest_var_ft(f) := block([v,w],
00039   assert(f([true]) = {}),
00040   assert(f([false]) = {}),
00041   assert(f([v]) = {v}),
00042   assert(f([neg(v)]) = {v}),
00043   assert(f(["and", [v], [w]]) = {v,w}),
00044   true)$
00045 
00046 /* ******************************************
00047    * Basic transformations of formula trees *
00048    ******************************************
00049 */
00050 
00051 okltest_elimination_constants_ft(f) := block([x],
00052   assert(f([x]) = [x]),
00053   assert(f(["or",[x],[true]]) = [true]),
00054   assert(f(["or",[x],[false]]) = ["or", [x]]),
00055   assert(f(["or",[x],[false],[true]]) = [true]),
00056   assert(f(["and",[x],[true]]) = ["and", [x]]),
00057   assert(f(["and",[x],[false]]) = [false]),
00058   assert(f(["and",[x],[true],[false]]) = [false]),
00059   assert(f(["xor",[x],[false]]) = ["xor",[x]]),
00060   true)$
00061 
00062 
00063 /* ***********************
00064    * Partial assignments *
00065    ***********************
00066 */
00067 
00068 okltest_apply_pa_prpl(f) := block([v,w,phi],
00069   assert(f(phi,false) = false),
00070   assert(f(phi,true) = true),
00071   assert(f({},v) = v),
00072   assert(f({},neg(v)) = neg(v)),
00073   assert(f({w},v) = v),
00074   assert(f({neg(w)},v) = v),
00075   assert(f({w}, neg(v)) = neg(v)),
00076   assert(f({neg(w)}, neg(v)) = neg(v)),
00077   assert(f({neg(v)},v) = false),
00078   assert(f({v},v) = true),
00079   assert(f({neg(v)}, neg(v)) = true),
00080   assert(f({v}, neg(v)) = false),
00081   true)$
00082 
00083 
00084 /* ******************
00085    * Measures       *
00086    ******************
00087 */
00088 
00089 /* ******************
00090    * Translations   *
00091    ******************
00092 */
00093 
00094 
00095 
00096 /* ****************************
00097    * Tseitin translation      *
00098    ****************************
00099 */
00100 
00101 okltest_tseitin_trans_list_rel(f) := block([F,T,a,b,c,d],
00102   F : ["and",
00103     ["or", ["and", [a], [b]], ["and", [c], [d]]],
00104     ["or", ["and", [neg(a)], [b]], ["and", [c], [neg(d)]]]],
00105   T : append(["and", [tstr_var([])]], f(F,[])),
00106   assert(nvar_ft(T) = 16-1 + 4),
00107   T : basic_simplification_ft(T),
00108   assert(nvar_ft(T) = 16-1 + 4),
00109   true)$
00110 
00111 okltest_tseitin_trans_list(f) := block([F,T,a,b,c,d],
00112   F : ["and",
00113     ["or", ["and", [a], [b]], ["and", [c], [d]]],
00114     ["or", ["and", [neg(a)], [b]], ["and", [c], [neg(d)]]]],
00115   T : append(["and", [tstr_var([])]], f(F)),
00116   assert(nvar_ft(T) = 16-1 + 4),
00117   T : basic_simplification_ft(T),
00118   assert(nvar_ft(T) = 16-1 + 4),
00119   true)$
00120 
00121 okltest_tseitin_trans_basic(f) := block([F,T,a,b,c,d],
00122   F : ["and",
00123     ["or", ["and", [a], [b]], ["and", [c], [d]]],
00124     ["or", ["and", [neg(a)], [b]], ["and", [c], [neg(d)]]]],
00125   T : f(F),
00126   assert(nvar_ft(T) = 16-1 + 4),
00127   T : basic_simplification_ft(T),
00128   assert(nvar_ft(T) = 16-1 + 4),
00129   true)$
00130