OKlibrary  0.2.1.6
Backtracking.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 10.2.2008 (Swansea) */
00002 /* Copyright 2008 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 /* Checks whether f determines satisfiability of formula-trees correctly */
00027 okltest_satisfiability_ft(f) := block([a,b,c],
00028   assert(f([false]) = false),
00029   assert(f([true]) = true),
00030   assert(f(["and"]) = true),
00031   assert(f(["or"]) = false),
00032   assert(f([a]) = true),
00033   assert(f([neg(a)]) = true),
00034   assert(f(["and", [a], [neg(a)]]) = false),
00035   assert(f(["equiv", [a], [a]]) = true),
00036   assert(f(["equiv", [a], [neg(a)]]) = false),
00037   assert(f(["xor", [a], [a]]) = false),
00038   assert(f(["xor", [a], [neg(a)]]) = true),
00039   assert(f(["not", ["impl", ["and", [a], [b]], ["or", [a], [neg(b)]]]]) = false),
00040   assert(f(["not", ["impl", ["or",[a],[b]], ["and",[a],[b]]]]) = true),
00041   assert(f(["not", ["impl", ["and", ["impl",[a],[b]], ["impl",[b],[c]]], ["impl",[a],[c]]]]) = false),
00042   true)$
00043