(--

This file exercises the logic.cecil data structures.

--)

include "logic.cecil";


-- test construction and canonicalization:
print("f1==(not a or not b) and c: ");
let f1:Formula := And(Or(Not(Variable("a")),
			 Not(Variable("b"))),
		      Variable("c"));
print_line(f1);

print("f2==not ((true or a) and (not not false and b or c)): ");
let f2:Formula := Not(And(Or(True,
			     Variable("a")),
			  Or(And(Not(Not(False)),
				 Variable("b")),
			     Variable("c"))));
print_line(f2);

print("f3==not (a or not a) implies false: ");
let f3:Formula := Implies(Not(Or(Variable("a"),
				 Not(Variable("a")))),
			  False);
print_line(f3);

print("f4==true implies false: ");
let f4:Formula := Implies(True, False);
print_line(f4);

print("f5==not f4: ");
let f5:Formula := Not(f4);
print_line(f5);

print("f6==a and not false or b: ");
let f6:Formula := Or(And(Variable("a"), Not(False)), Variable("b"));
print_line(f6);

print("f6b==a and not false or b: ");
let f6b:Formula := Or(And(Variable("a"), Not(False)), Variable("b"));
print_line(f6b);

-- test structural equality testing
print("f1 = f1: ");
print_line(f1 = f1);
print("f2 = f2: ");
print_line(f2 = f2);
print("f1 = f2: ");
print_line(f1 = f2);
print("f2 = f1: ");
print_line(f2 = f1);
print("f6 = f6b: ");
print_line(f6 = f6b);

-- test evaluation
let bindings:m_table[string,bool] := new_assoc_table[string,bool]();
bindings!"a" := true;
bindings!"b" := false;
bindings!"c" := true;

print("f1[" || bindings.elems_print_string || "]: ");
print_line(f1.evaluate(bindings));
print("f2[" || bindings.elems_print_string || "]: ");
print_line(f2.evaluate(bindings));
print("f3[" || bindings.elems_print_string || "]: ");
print_line(f3.evaluate(bindings));
print("f4[" || bindings.elems_print_string || "]: ");
print_line(f4.evaluate(bindings));
print("f5[" || bindings.elems_print_string || "]: ");
print_line(f5.evaluate(bindings));
print("f6[" || bindings.elems_print_string || "]: ");
print_line(f6.evaluate(bindings));

-- varsDo testing
print("f1's vars: ");
f1.varsDo(&(name:string){ name.print; " ".print; }); print_line();
print("f2's vars: ");
f2.varsDo(&(name:string){ name.print; " ".print; }); print_line();
print("f3's vars: ");
f3.varsDo(&(name:string){ name.print; " ".print; }); print_line();
print("f4's vars: ");
f4.varsDo(&(name:string){ name.print; " ".print; }); print_line();
print("f5's vars: ");
f5.varsDo(&(name:string){ name.print; " ".print; }); print_line();
print("f6's vars: ");
f6.varsDo(&(name:string){ name.print; " ".print; }); print_line();

-- tautology testing
print("f1 is tautology: ");
print_line(f1.isTautology);
print("f2 is tautology: ");
print_line(f2.isTautology);
print("f3 is tautology: ");
print_line(f3.isTautology);
print("f4 is tautology: ");
print_line(f4.isTautology);
print("f5 is tautology: ");
print_line(f5.isTautology);
print("f6 is tautology: ");
print_line(f6.isTautology);