package org.semanticweb.clipper.hornshiq.cli;

import gnu.trove.procedure.TIntProcedure;
import gnu.trove.set.hash.TIntHashSet;

import java.util.Set;

import org.semanticweb.clipper.hornshiq.queryanswering.CQFormatter;
import org.semanticweb.clipper.hornshiq.queryanswering.ClipperManager;
import org.semanticweb.clipper.hornshiq.queryanswering.EnforcedRelation;
import org.semanticweb.clipper.hornshiq.queryanswering.IndexedEnfContainer;
import org.semanticweb.clipper.hornshiq.queryanswering.NamingStrategy;
import org.semanticweb.clipper.hornshiq.queryanswering.QAHornSHIQ;
import org.semanticweb.clipper.hornshiq.queryanswering.TBoxSaturation;
import org.semanticweb.clipper.util.BitSetUtil;
import org.semanticweb.clipper.util.BitSetUtilOpt;
import org.semanticweb.owlapi.model.OWLOntology;

import lombok.Getter;

import com.beust.jcommander.JCommander;
import com.beust.jcommander.Parameters;

@Getter
@Parameters(commandNames = { "pex" }, separators = "=", commandDescription = "output the Existence Axioms in the sturated ontology")
public class CommandPythonOntology extends ReasoningCommandBase {

	private CQFormatter formatter;

	public CommandPythonOntology(JCommander jc) {
		super(jc);
	}

	@Override
	boolean validate() {
		return true;
	}

	@Override
	void exec() {
		QAHornSHIQ qaHornSHIQ = new QAHornSHIQ();
		// note that naming strategy should be set after create new QAHornSHIQ
		qaHornSHIQ.setNamingStrategy(NamingStrategy.FRAGMENT);

		Set<OWLOntology> ontologies = loadOntologies();

		qaHornSHIQ.setOntologies(ontologies);

		qaHornSHIQ.preprocessOntologies();

		TBoxSaturation saturation = qaHornSHIQ.saturateTbox();

		IndexedEnfContainer enfs = saturation.getEnfContainer();

		formatter = new CQFormatter();

		int axid = 0;

		System.out.println("[");
		for (EnforcedRelation enf : enfs) {
			axid++;
			System.out.println(enf2Pex(enf, axid) + " ,");
		}
		System.out.println("]");
	}

	private String enf2Pex(EnforcedRelation e, int axid) {

		final StringBuilder sb = new StringBuilder();
		sb.append("ExistenceAxiom(");
		sb.append("[");
		e.getType1().forEach(new TIntProcedure() {
			@Override
			public boolean execute(int arg0) {
				sb.append("'").append(formatter.getUnaryPredicate(arg0))
						.append("', ");
				return false;
			}
		});
		sb.append("], [");
		e.getRoles().forEach(new TIntProcedure() {
			@Override
			public boolean execute(int r) {
				if (r % 2 == 0)
					sb.append("('").append(formatter.getBinaryPredicate(r))
							.append("', 'name'), ");
				else
					sb.append("('")
							.append(formatter.getBinaryPredicate(r - 1))
							.append("', 'inv'), ");
				return false;
			}
		});
		sb.append("], [");
		e.getType2().forEach(new TIntProcedure() {
			@Override
			public boolean execute(int arg0) {
				sb.append("'").append(formatter.getUnaryPredicate(arg0))
						.append("', ");
				return false;
			}
		});
		sb.append("]");
		sb.append(", ").append(axid);
		sb.append(")");

		return sb.toString();
	}
}

@@ -1969,17 +1969,77 @@
 axid) %7B%0A
+%09%09final int thing = ClipperManager.getInstance().getThing();
 %0A
-
 %09%09final 
@@ -2216,32 +2216,58 @@
 ute(int arg0) %7B%0A
+%09%09%09%09if (arg0 != thing) %7B%0A%09
 %09%09%09%09sb.append(%22'
@@ -2309,32 +2309,33 @@
 te(arg0))%0A%09%09%09%09%09%09
+%09
 .append(%22', %22);%0A
@@ -2326,32 +2326,38 @@
 .append(%22', %22);%0A
+%09%09%09%09%7D%0A
 %09%09%09%09return false
@@ -2343,36 +2343,35 @@
 %09%09%09%7D%0A%09%09%09%09return 
-fals
+tru
 e;%0A%09%09%09%7D%0A%09%09%7D);%0A%09%09
@@ -2624,24 +2624,16 @@
 nd(%22('%22)
-%0A%09%09%09%09%09%09%09
 .append(
@@ -2703,36 +2703,35 @@
  %22);%0A%09%09%09%09return 
-fals
+tru
 e;%0A%09%09%09%7D%0A%09%09%7D);%0A%09%09
@@ -2841,24 +2841,51 @@
 int arg0) %7B%0A
+%09%09%09%09if (arg0 != thing) %7B%0A%0A%09
 %09%09%09%09sb.appen
@@ -2935,24 +2935,25 @@
 rg0))%0A%09%09%09%09%09%09
+%09
 .append(%22', 
@@ -2952,24 +2952,30 @@
 end(%22', %22);%0A
+%09%09%09%09%7D%0A
 %09%09%09%09return f
@@ -2977,12 +2977,11 @@
 urn 
-fals
+tru
 e;%0A%09

fix a bug for loop in roles, types (TIntHasSet); remove owl:Thing from output