/*
A simple implementation of Russel&Norvig's clausification algorithm.
Copyright 2010-2011 Adam Pease, apease@articulatesoftware.com
This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with this program ; if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston,
MA 02111-1307 USA
*/
package atp;
import java.util.*;
public class Clausifier {
public static int varCounter = 0;
public static int skolemCounter = 0;
public static int axiomCounter = 0;
public static String typePrefix = "axiom";
/** ***************************************************************
* a->b is the same as -a|b
*/
private static BareFormula removeImp(BareFormula form) {
BareFormula result = new BareFormula();
result.op = Lexer.Or;
BareFormula newLHS = new BareFormula();
newLHS.op = Lexer.Negation;
if (form.child2 != null)
result.child2 = removeImpEq(form.child2);
if (form.child1 != null)
newLHS.child1 = removeImpEq(form.child1);
if (form.lit1 != null)
newLHS.lit1 = form.lit1;
if (form.lit2 != null)
result.lit2 = form.lit2;
result.child1 = newLHS;
return result;
}
/** ***************************************************************
* ab)&(b->a)
*/
private static BareFormula removeEq(BareFormula form) {
BareFormula result = new BareFormula();
BareFormula lhs = new BareFormula();
if (form.child1 != null)
lhs.child1 = form.child1;
if (form.child2 != null)
lhs.child2 = form.child2;
if (form.lit1 != null)
lhs.lit1 = form.lit1;
if (form.lit2 != null)
lhs.lit2 = form.lit2;
lhs.op = Lexer.Implies;
BareFormula rhs = new BareFormula();
if (form.child1 != null)
rhs.child2 = form.child1;
if (form.child2 != null)
rhs.child1 = form.child2;
if (form.lit1 != null)
rhs.lit2 = form.lit1;
if (form.lit2 != null)
rhs.lit1 = form.lit2;
rhs.op = Lexer.Implies;
result.op = Lexer.And;
result.child1 = lhs;
result.child2 = rhs;
return removeImpEq(result);
}
/** ***************************************************************
* ab is the same as
* (a->b)&(b->a)
* a->b is the same as -a|b
*/
private static BareFormula removeImpEq(BareFormula form) {
if (form.op.equals(Lexer.Implies)) {
return removeImp(form);
}
else if (form.op.equals(Lexer.Equiv)) {
return removeEq(form);
}
else if (form.op.equals(Lexer.BImplies)) {
return removeBImp(form);
}
else {
BareFormula result = form.deepCopy();
if (result.child1 != null)
result.child1 = removeImpEq(result.child1);
if (result.child2 != null)
result.child2 = removeImpEq(result.child2);
return result;
}
}
/** ***************************************************************
* -(p | q) becomes -p & -q
* -(p & q) becomes -p | -q
* -![X]:p becomes ?[X]:-p
* -?[X]:p becomes ![X]:-p
* --p becomes p
* @param flip when true indicates to change the operator of the given
* literal
*/
private static Literal moveNegationIn(Literal lit, boolean flip) {
if (!flip)
return lit;
Literal result = lit.deepCopy();
if (result.atom.getFunc().equals(Lexer.EqualSign) && flip)
result.atom.t = Lexer.NotEqualSign;
else if (result.atom.getFunc().equals(Lexer.NotEqualSign) && flip)
result.atom.t = Lexer.EqualSign;
else
result.negated = !result.negated;
return result;
}
/** ***************************************************************
*/
private static BareFormula moveNegationIn(BareFormula form) {
return moveNegationIn(form,false);
}
/** ***************************************************************
*/
private static String flipOperator(String s) {
if (s.equals("|"))
return "&";
else if (s.equals("&"))
return "|";
else if (s.equals("~|"))
return "|";
else if (s.equals("~&"))
return "&";
else if (s.equals("!"))
return "?";
else if (s.equals("?"))
return "!";
return s;
}
/** ***************************************************************
* -(p | q) becomes -p & -q
* -(p & q) becomes -p | -q
* -![X]:p becomes ?[X]:-p
* -?[X]:p becomes ![X]:-p
* --p becomes p
*/
private static BareFormula moveNegationIn(BareFormula form, boolean flip) {
//System.out.println("INFO in Clausifier.moveNegationIn(): " + form + " " + flip);
BareFormula result = form.deepCopy();
if (result.op.equals("~")) { // there is no child2 or lit2 in this case
//System.out.println("INFO in Clausifier.moveNegationIn(): has a negation: " + result);
if (flip) {
//System.out.println("INFO in Clausifier.moveNegationIn(): negations cancel: " + result);
if (result.child1 != null)
result = moveNegationIn(result.child1,false);
if (result.lit1 != null)
result.lit1 = moveNegationIn(result.lit1,false);
}
else {
//System.out.println("INFO in Clausifier.moveNegationIn(): negation with no flip: " + result);
if (result.child1 != null) {
result = moveNegationIn(result.child1,true);
}
else if (result.lit1 != null) { // should handle a no-op parent
result.lit1 = moveNegationIn(result.lit1,true);
result.op = "";
}
}
}
else {
if (flip) {
//System.out.println("INFO in Clausifier.moveNegationIn(): flipping: " + result);
result.op = flipOperator(result.op);
if (result.child2 != null)
result.child2 = moveNegationIn(form.child2,true);
if (result.child1 != null)
result.child1 = moveNegationIn(form.child1,true);
if (result.lit1 != null && !BareFormula.isQuantifier(result.op))
result.lit1 = moveNegationIn(form.lit1,true);
if (result.lit2 != null)
result.lit2 = moveNegationIn(form.lit2,true);
}
else {
//System.out.println("INFO in Clausifier.moveNegationIn(): 5: " + result);
if (result.child2 != null)
result.child2 = moveNegationIn(form.child2,false);
if (result.child1 != null)
result.child1 = moveNegationIn(form.child1,false);
if (result.lit1 != null && !BareFormula.isQuantifier(result.op))
result.lit1 = moveNegationIn(form.lit1,false);
if (result.lit2 != null)
result.lit2 = moveNegationIn(form.lit2,false);
}
}
//System.out.println("INFO in Clausifier.moveNegationIn(): 6 returning: " + result);
return result;
}
/** ***************************************************************
*/
private static Term generateNewVar() {
return Term.string2Term("VAR" + Integer.toString(varCounter++));
}
/** ***************************************************************
* The scope of variables in quantifiers is local to the quantifier,
* but to avoid confusion, variables of the same name but different scope
* in a formula are renamed.
*
* ![X]:p(X) | ?[X]:q(X) becomes
* ![X]:p(X) | ?[Y]:q(Y)
*/
public static BareFormula standardizeVariables(BareFormula form) {
BareFormula result = form.deepCopy();
if (form.child1 != null)
result.child1 = standardizeVariables(form.child1);
if (form.child2 != null)
result.child2 = standardizeVariables(form.child2);
if (BareFormula.isQuantifier(form.op)) {
Substitutions subst = new Substitutions();
Term oldVar = form.lit1.atom;
Term newVar = generateNewVar();
subst.addSubst(oldVar,newVar);
return result.substitute(subst);
}
return result;
}
/** ***************************************************************
*/
private static BareFormula moveQuantLeftChild(BareFormula form) {
//System.out.println("Child1 has quantifier. Current result: " + form);
BareFormula newParent = new BareFormula();
newParent.op = form.child1.op;
newParent.lit1 = form.child1.lit1; // child1 has quantifier list
BareFormula newChild = new BareFormula();
newParent.child2 = newChild;
if (form.child2 != null)
newChild.child2 = form.child2;
if (form.lit2 != null)
newChild.lit2 = form.lit2;
if (form.child1.child2 != null)
newChild.child1 = form.child1.child2;
if (form.child1.lit2 != null)
newChild.lit1 = form.child1.lit2;
newChild.op = form.op;
//System.out.println("Child1 has quantifier. New result: " + newParent);
return newParent;
}
/** ***************************************************************
*/
private static BareFormula moveQuantRightChild(BareFormula form) {
//System.out.println("Child2 is not null: " + form.child2);
//System.out.println("Child2 has quantifier. Current result: " + form);
BareFormula newParent = new BareFormula();
newParent.op = form.child2.op;
newParent.lit1 = form.child2.lit1; // child2 has a quantifier list
BareFormula newChild = new BareFormula();
newParent.child2 = newChild;
if (form.child1 != null)
newChild.child1 = form.child1;
if (form.lit1 != null)
newChild.lit1 = form.lit1;
if (form.child2.child2 != null)
newChild.child2 = form.child2.child2;
if (form.child2.lit2 != null)
newChild.lit2 = form.child2.lit2;
newChild.op = form.op;
//System.out.println("Child2 has quantifier. New result: " + newParent);
return newParent;
}
/** ***************************************************************
* [op1 child1 child2]
* [op2 lit1 child3] [op3 lit2 child4]
* becomes
* [op2 lit1 new1]
* [op3 lit2 new2]
* [op1 child3 child4]
*/
private static BareFormula moveQuantBothChildren(BareFormula form) {
BareFormula newParent = new BareFormula();
BareFormula newMidChild = new BareFormula();
BareFormula newBottomChild = new BareFormula();
newParent.op = form.child1.op;
newParent.lit1 = form.child1.lit1;
newParent.child2 = newMidChild;
newMidChild.op = form.child2.op;
newMidChild.lit1 = form.child2.lit1;
newMidChild.child2 = newBottomChild;
newBottomChild.op = form.op;
if (form.child1.child2 != null)
newBottomChild.child1 = form.child1.child2;
if (form.child1.lit2 != null)
newBottomChild.lit1 = form.child1.lit2;
if (form.child2.child2 != null)
newBottomChild.child2 = form.child2.child2;
if (form.child2.lit2 != null)
newBottomChild.lit2 = form.child2.lit2;
return newParent;
}
/** ***************************************************************
* p|![X]q(X)
* becomes
* ![X]p | q(X)
*/
private static BareFormula moveQuantifiersLeftIterate(BareFormula form) {
//System.out.println("INFO in Clausifier.moveQuantifiersLeft(): " + form);
//System.out.println("op: " + form.op);
if (form == null)
return null;
BareFormula result = form.deepCopy();
if (BareFormula.isQuantifier(form.op)) {
//System.out.println("Formula has quantifier(1): " + form);
result.op = form.op;
result.lit1 = form.lit1; // child1 not needed since it's null when there's a quantifier
result.child2 = moveQuantifiersLeftIterate(form.child2);
result.lit2 = form.lit2;
//System.out.println("Formula has quantifier: " + result);
return result;
}
if (form.child2 != null)
result.child2 = moveQuantifiersLeftIterate(form.child2);
if (form.child1 != null)
result.child1 = moveQuantifiersLeftIterate(form.child1);
if (result.child2 != null && BareFormula.isQuantifier(result.child2.op) &&
result.child1 != null && BareFormula.isQuantifier(result.child1.op)) {
changed = true;
return moveQuantBothChildren(result);
}
if (result.child2 != null && BareFormula.isQuantifier(result.child2.op)) {
changed = true;
return moveQuantRightChild(result);
}
if (result.child1 != null && BareFormula.isQuantifier(result.child1.op)) {
changed = true;
return moveQuantLeftChild(result);
}
return result;
}
private static boolean changed = true;
/** ***************************************************************
*/
private static BareFormula moveQuantifiersLeft(BareFormula form) {
BareFormula result = form.deepCopy();
while (changed) {
changed = false;
result = moveQuantifiersLeftIterate(result);
}
return result;
}
/** ***************************************************************
*/
private static Term generateNewSkolem(HashSet args) {
StringBuffer argList = new StringBuffer();
Iterator it = args.iterator();
while (it.hasNext()) {
Term t = it.next();
argList.append(t.toString());
if (it.hasNext())
argList.append(",");
}
if (argList.length() > 0)
return Term.string2Term("skf" + Integer.toString(varCounter++) + "(" + argList + ")");
else
return Term.string2Term("skf" + Integer.toString(varCounter++));
}
/** ***************************************************************
*/
private static BareFormula skolemizationRecurse(BareFormula form,
HashSet uList) {
//System.out.println("INFO in Clausifier.skolemizationRecurse(): " + form);
//System.out.println(uList);
BareFormula result = form.deepCopy();
if (form.child1 != null)
result.child1 = skolemizationRecurse(form.child1,uList);
if (form.child2 != null)
result.child2 = skolemizationRecurse(form.child2,uList);
if (form.op.equals("?")) { // existential
Term var = form.lit1.atom;
Term skolem = generateNewSkolem(uList);
Substitutions subst = new Substitutions();
subst.addSubst(var,skolem);
//System.out.println("calling substitution with: " + subst);
result = result.substitute(subst);
result.op = ""; // not sure if this is ok
if (result.child2 != null)
result = result.child2;
//System.out.println("returning result: " + result);
return result;
}
if (form.op.equals("!")) // universal
uList.add(form.lit1.atom);
return result;
}
/** ***************************************************************
* Create a unique function in place of every existentially quantified variable.
* Include every universally quantified variable that is in scope, inside the function.
* ![X]:p(X) => (?[Y]:h(Y) & a(X,Y))
* becomes
* ![X]:p(X) => (h(skf(X)) & a(X,skf(X)))
*/
private static BareFormula skolemization(BareFormula form) {
return skolemizationRecurse(form,new HashSet());
}
/** ***************************************************************
* Remove universal quantifiers
*/
private static BareFormula removeUQuant(BareFormula form) {
BareFormula result = form.deepCopy();
if (form.child1 != null)
result.child1 = removeUQuant(form.child1);
if (form.child2 != null)
result.child2 = removeUQuant(form.child2);
if (form.op.equals("!")) {
return result.child2;
}
else
return result;
}
/** ***************************************************************
* (a & b) | c becomes (a | c) & (b | c)
*/
private static BareFormula distributeAndOverOrRecurse(BareFormula form) {
//System.out.println("INFO in Clausifier.distributeAndOverOrRecurse(): " + KIF.format(form.toKIFString()) + " " + changed);
BareFormula result = form.deepCopy();
if (form.child1 != null)
result.child1 = distributeAndOverOr(form.child1);
if (form.child2 != null)
result.child2 = distributeAndOverOr(form.child2);
//System.out.println("INFO in Clausifier.distributeAndOverOrRecurse(): (2): " + KIF.format(form.toKIFString()));
if (form.op.equals("|")) {
//System.out.println("INFO in Clausifier.distributeAndOverOrRecurse(): top level or: " + KIF.format(form.toKIFString()));
if (result.child1 != null && result.child1.op.equals("&")) {
//System.out.println("INFO in Clausifier.distributeAndOverOrRecurse(): child1 and: " + KIF.format(form.toKIFString()));
BareFormula newParent = new BareFormula();
newParent.op = "&";
BareFormula newChild1 = new BareFormula();
newChild1.op = "|";
if (result.child1.child1 != null)
newChild1.child1 = result.child1.child1;
if (result.child1.lit1 != null)
newChild1.lit1 = result.child1.lit1;
if (result.child2 != null)
newChild1.child2 = result.child2;
if (result.lit2 != null)
newChild1.lit2 = result.lit2;
BareFormula newChild2 = new BareFormula();
newChild2.op = "|";
if (result.child1.child2 != null)
newChild2.child1 = result.child1.child2;
if (result.child1.lit2 != null)
newChild2.lit1 = result.child1.lit2;
if (result.child2 != null)
newChild2.child2 = result.child2;
if (result.lit2 != null)
newChild2.lit2 = result.lit2;
newParent.child1 = newChild1;
newParent.child2 = newChild2;
changed = true;
//System.out.println("INFO in Clausifier.distributeAndOverOrRecurse(): result: " + KIF.format(newParent.toKIFString()));
return newParent;
}
else if (result.child2 != null && result.child2.op.equals("&")) {
//System.out.println("INFO in Clausifier.distributeAndOverOrRecurse(): child2 and: " + KIF.format(form.toKIFString()));
BareFormula newParent = new BareFormula();
newParent.op = "&";
BareFormula newChild1 = new BareFormula();
newChild1.op = "|";
if (result.child2.child1 != null)
newChild1.child1 = result.child2.child1;
if (result.child2.lit1 != null)
newChild1.lit1 = result.child2.lit1;
if (result.child1 != null)
newChild1.child2 = result.child1;
if (result.lit1 != null)
newChild1.lit2 = result.lit1;
BareFormula newChild2 = new BareFormula();
newChild2.op = "|";
if (result.child2.child2 != null)
newChild2.child1 = result.child2.child2;
if (result.child2.lit2 != null)
newChild2.lit1 = result.child2.lit2;
if (result.child1 != null)
newChild2.child2 = result.child1;
if (result.lit1 != null)
newChild2.lit2 = result.lit1;
newParent.child1 = newChild1;
newParent.child2 = newChild2;
changed = true;
//System.out.println("INFO in Clausifier.distributeAndOverOrRecurse(): result: " + KIF.format(newParent.toKIFString()));
return newParent;
}
}
return result;
}
/** ***************************************************************
*/
private static BareFormula distributeAndOverOr(BareFormula form) {
BareFormula result = form.deepCopy();
changed = true;
while (changed) {
changed = false;
result = distributeAndOverOrRecurse(result);
}
return result;
}
/** ***************************************************************
*/
private static ArrayList separateConjunctions(BareFormula form) {
ArrayList result = new ArrayList();
if (form.op.equals("&")) {
if (form.child1 != null)
result.addAll(separateConjunctions(form.child1));
if (form.child2 != null)
result.addAll(separateConjunctions(form.child2));
}
else
result.add(form);
return result;
}
/** ***************************************************************
* (a | b) | c becomes a | b | c
*/
private static Clause flatten(BareFormula form) {
Clause result = new Clause();
if (!Term.emptyString(form.op) && !form.op.equals("|")) {
System.out.println("Error in Clausifier.flatten(): operator '" + form.op + "' is not a disjunction");
return result;
}
if (form.lit1 != null)
result.add(form.lit1);
if (form.lit2 != null)
result.add(form.lit2);
if (form.child1 != null)
result.addAll(flatten(form.child1).literals);
if (form.child2 != null)
result.addAll(flatten(form.child2).literals);
return result;
}
/** ***************************************************************
*/
private static ArrayList flattenAll(ArrayList forms) {
ArrayList result = new ArrayList();
for (int i = 0; i < forms.size(); i++) {
BareFormula form = forms.get(i);
Clause c = flatten(form);
c.name = "cnf" + Integer.toString(axiomCounter++);
c.type = typePrefix;
result.add(c);
}
return result;
}
/** ***************************************************************
*/
public static ArrayList clausify(BareFormula bf) {
BareFormula result = bf.deepCopy();
BareFormula newresult = SmallCNFization.formulaOpSimplify(result);
if (newresult != null)
result = newresult;
result = removeImpEq(result);
result = moveNegationIn(result);
result = standardizeVariables(result);
result = moveQuantifiersLeft(result);
result = skolemization(result);
result = removeUQuant(result);
result = distributeAndOverOr(result);
ArrayList forms = separateConjunctions(result);
ArrayList clauses = flattenAll(forms);
return clauses;
}
/** ***************************************************************
*/
public static ArrayList clausify(Formula f) {
typePrefix = f.type;
return clausify(f.form);
}
/** ***************************************************************
* *************** Unit Tests ******************
*/
/** ***************************************************************
*/
private static void testRemoveImpEq() {
System.out.println();
System.out.println("================== testRemoveImpEq ======================");
BareFormula form = BareFormula.string2form("a=>b");
System.out.println("input: " + form);
form = removeImpEq(form);
System.out.println(form);
System.out.println();
form = BareFormula.string2form("ab");
System.out.println("input: " + form);
form = removeImpEq(form);
System.out.println(form);
System.out.println();
form = BareFormula.string2form("((((![X]:a(X))|b(X))|(?[X]:(?[Y]:p(X,f(Y)))))q(g(a),X))");
System.out.println("input: " + form);
form = removeImpEq(form);
System.out.println(form);
System.out.println();
}
/** ***************************************************************
*/
private static void testMoveQuantifiersLeft() {
System.out.println();
System.out.println("================== testMoveQuantifiersLeft ======================");
BareFormula form = BareFormula.string2form("p|![X]:q(X)");
/*
System.out.println("input: " + form);
form = moveQuantifiersLeft(form);
System.out.println("result should be ![X]:p | q(X): " + form);
System.out.println();
form = BareFormula.string2form("~((![X]:a(X)) | b(X))");
System.out.println("input: " + form);
form = moveQuantifiersLeft(form);
System.out.println("result: " + form);
System.out.println();
form = BareFormula.string2form("~(((![X]:a(X)) | b(X)) | (?[X]:(?[Y]:p(X, f(Y)))))");
System.out.println("input: " + form);
form = moveQuantifiersLeft(form);
System.out.println("result: " + form);
System.out.println();
form = BareFormula.string2form("( (~(((![X]:a(X)) | b(X)) | (?[X]:(?[Y]:p(X, f(Y)))))) | q(g(a), X))");
System.out.println("input: " + form);
form = moveQuantifiersLeft(form);
System.out.println("result: " + form);
System.out.println();
*/
form = BareFormula.string2form("( ( (~(((![X]:a(X)) | b(X)) | (?[X]:(?[Y]:p(X, f(Y)))))) | q(g(a), X)) & " +
"((~q(g(a), X)) | (((![X]:a(X)) | b(X)) | (?[X]:(?[Y]:p(X, f(Y)))))))");
System.out.println("input: " + form);
form = moveQuantifiersLeft(form);
System.out.println("result: " + form);
System.out.println();
}
/** ***************************************************************
*/
private static void testMoveNegationIn() {
System.out.println();
System.out.println("================== testMoveNegationIn ======================");
BareFormula form = BareFormula.string2form("~(p | q)");
System.out.println("input: " + form);
form = moveNegationIn(form);
System.out.println("result should be -p & -q: " + form);
System.out.println();
form = BareFormula.string2form("~(p & q)");
System.out.println("input: " + form);
form = moveNegationIn(form);
System.out.println("result should be -p | -q: " + form);
System.out.println();
form = BareFormula.string2form("~![X]:p");
System.out.println("input: " + form);
form = moveNegationIn(form);
System.out.println("result should be ?[X]:-p: " + form);
System.out.println();
form = BareFormula.string2form("~?[X]:p");
System.out.println("input: " + form);
form = moveNegationIn(form);
System.out.println("result should be ![X]:-p: " + form);
System.out.println();
form = BareFormula.string2form("~~p");
System.out.println("input: " + form);
form = moveNegationIn(form);
System.out.println("result should be p: " + form);
System.out.println();
form = BareFormula.string2form("(~(?[Y]:p(X, f(Y))))");
System.out.println("input: " + form);
form = moveNegationIn(form);
System.out.println("result: " + form);
System.out.println();
form = BareFormula.string2form("(~(?[X]:(?[Y]:p(X, f(Y)))))");
System.out.println("input: " + form);
form = moveNegationIn(form);
System.out.println("expected result: (![X]:(![Y]:~p(X, f(Y))))");
System.out.println("result: " + form);
System.out.println();
form = BareFormula.string2form("~(((![X]:a(X))|b(X))|(?[X]:(?[Y]:p(X, f(Y)))))");
System.out.println("input: " + form);
form = moveNegationIn(form);
System.out.println("result should be ( ((?[X]:(~a(X))|~b(X)) & (![X]:(![Y]:~p(X, f(Y)))) ): ");
System.out.println("actual: "+ form);
System.out.println();
form = BareFormula.string2form("(((~(((![X]:a(X))|b(X))|(?[X]:(?[Y]:p(X, f(Y))))))|q(g(a), X))&((~q(g(a), X))|(((![X]:a(X))|b(X))|(?[X]:(?[Y]:p(X, f(Y)))))))");
System.out.println("input: " + form);
form = moveNegationIn(form);
System.out.println("expected: ( ( ((( (?[X]:~a(X)) & ~b(X)) & (![X]:(![Y]:~p(X, f(Y)))) )) | q(g(a), X)) & " +
"((~q(g(a), X)) | (((![X]:a(X))|b(X)) | (?[X]:(?[Y]:p(X, f(Y)))) )))");
System.out.println("result: " + form);
System.out.println();
}
/** ***************************************************************
*/
private static void testStandardizeVariables() {
System.out.println();
System.out.println("================== testStandardizeVariables ======================");
BareFormula form = BareFormula.string2form("~((![X]:a(X)) | b(X))");
System.out.println("input: " + form);
form = standardizeVariables(form);
System.out.println("result should be : ~((![VAR2]:a(VAR2)) | b(VAR1))");
System.out.println("actual: "+ form);
System.out.println();
form = BareFormula.string2form("(((~(((![X]:a(X))|b(X))|(?[X]:(?[Y]:p(X, f(Y))))))|q(g(a), X))&((~q(g(a), X))|(((![X]:a(X))|b(X))|(?[X]:(?[Y]:p(X, f(Y)))))))");
System.out.println("input: " + form);
form = standardizeVariables(form);
//System.out.println("result should be : ~((![VAR2]:a(VAR2)) | b(VAR1))");
System.out.println("actual: "+ form);
System.out.println();
}
/** ***************************************************************
*/
private static void testSkolemization() {
System.out.println();
System.out.println("================== testSkolemization ======================");
BareFormula form = BareFormula.string2form("(?[VAR0]:(![VAR3]:(![VAR2]:(?[VAR5]:(![VAR1]:(?[VAR4]:((((~a(VAR0)&~b(X))&~p(VAR2, f(VAR1)))|q(g(a), X))&(~q(g(a), X)|((a(VAR3)|b(X))|p(VAR5, f(VAR4)))))))))))");
System.out.println("input: " + form);
form = skolemization(form);
System.out.println("actual: "+ form);
System.out.println();
}
/** ***************************************************************
*/
private static void testDistribute() {
System.out.println();
System.out.println("================== testDistribute ======================");
BareFormula form = BareFormula.string2form("(a & b) | c");
/*
System.out.println("input: " + form);
form = distributeAndOverOr(form);
System.out.println("result should be : (a | c) & (b | c)");
System.out.println("actual: " + form);
System.out.println();
form = BareFormula.string2form("(a & b) | (c & d)");
System.out.println("input: " + form);
form = distributeAndOverOr(form);
System.out.println("result should be : (a | c) & (a | d) & (b | c) & (d | b)");
System.out.println("actual: " + form);
System.out.println();
*/
KIF.init();
form = BareFormula.string2form("(((~holdsAt(VAR2, VAR1)|releasedAt(VAR2, plus(VAR1, n1)))|(happens(skf3, VAR1)&terminates(skf3, VAR2, VAR1)))|holdsAt(VAR2, plus(VAR1, n1)))");
System.out.println("input: " + form);
form = distributeAndOverOr(form);
System.out.println("actual: " + form);
System.out.println(KIF.format(form.toKIFString()));
System.out.println();
}
/** ***************************************************************
*/
private static void testClausificationSteps(String s) {
KIF.init();
System.out.println();
System.out.println("================== testClausification ======================");
BareFormula form = BareFormula.string2form(s);
System.out.println("input: " + form);
System.out.println(KIF.format(form.toKIFString()));
System.out.println();
form = removeImpEq(form);
System.out.println("after Remove Implications and Equivalence: " + form);
System.out.println(KIF.format(form.toKIFString()));
System.out.println();
form = moveNegationIn(form);
System.out.println("after Move Negation In: " + form);
System.out.println(KIF.format(form.toKIFString()));
System.out.println();
form = standardizeVariables(form);
System.out.println("after Standardize Variables: " + form);
System.out.println(KIF.format(form.toKIFString()));
System.out.println();
form = moveQuantifiersLeft(form);
System.out.println("after Move Quantifiers: " + form);
System.out.println(KIF.format(form.toKIFString()));
System.out.println();
form = skolemization(form);
System.out.println("after Skolemization: " + form);
System.out.println(KIF.format(form.toKIFString()));
System.out.println();
form = removeUQuant(form);
System.out.println("after remove universal quantifiers: " + form);
System.out.println(KIF.format(form.toKIFString()));
System.out.println();
form = distributeAndOverOr(form);
System.out.println("after Distribution: " + form);
System.out.println(KIF.format(form.toKIFString()));
System.out.println();
ArrayList forms = separateConjunctions(form);
System.out.println("after separation: " + forms);
System.out.println(KIF.format(form.toKIFString()));
System.out.println();
ArrayList clauses = flattenAll(forms);
System.out.println("after flattening: " + clauses);
System.out.println();
}
/** ***************************************************************
*/
private static void testClausification() {
//testClausificationSteps("((((![X]:a(X))|b(X))|(?[X]:(?[Y]:p(X,f(Y)))))q(g(a),X))");
testClausificationSteps("(![Fluent]:(![Time]:(((holdsAt(Fluent, Time)&(~releasedAt(Fluent, plus(Time, n1))))&(~(?[Event]:(happens(Event, Time)&terminates(Event, Fluent, Time)))))=>holdsAt(Fluent, plus(Time, n1)))))).");
}
/** ***************************************************************
*/
private static void testClausificationSimple() {
System.out.println();
System.out.println("================== testClausificationSimple ======================");
BareFormula form = BareFormula.string2form("((((![X]:a(X))|b(X))|(?[X]:(?[Y]:p(X,f(Y)))))q(g(a),X))");
System.out.println("input: " + form);
System.out.println();
ArrayList result = clausify(form);
for (int i = 0; i < result.size(); i++)
System.out.println(result.get(i));
}
/** ***************************************************************
*/
private static void testFileClaus(String filename) {
System.out.println();
System.out.println("================== testClaus ======================");
ClauseSet cs = Formula.file2clauses(filename);
for (int i = 0; i < cs.clauses.size(); i++)
System.out.println(cs.clauses.get(i));
}
/** ***************************************************************
*/
public static void main(String[] args) {
//testRemoveImpEq();
//testMoveNegationIn();
//testMoveQuantifiersLeft();
//testStandardizeVariables();
//testSkolemization();
//testDistribute();
//testClausification();
//testClausificationSimple();
testFileClaus(args[0]);
}
}