import java.io.File

import de.tu_dresden.lat.forgettingBasedProofs._
import de.tu_dresden.lat.forgettingBasedProofs.adaptors.{LetheBasedForgetter, OWLApiBasedJustifier}
import org.semanticweb.owlapi.apibinding.OWLManager
import org.semanticweb.owlapi.model.IRI

object Test {

    def main(args: Array[String]) = {

      val ontologyManager = OWLManager.createOWLOntologyManager()
      val forgetter = LetheBasedForgetter.ALC_ABox
      val justifier = OWLApiBasedJustifier.UsingHermiT(ontologyManager)
      val ontology = ontologyManager.loadOntologyFromOntologyDocument(new File("pizza.owl"))
      val proofGenerator = new CompleteForgettingBasedProofGenerator(ontology, forgetter, justifier, true)

      val dataFactory = ontologyManager.getOWLDataFactory()

      val lhs = dataFactory.getOWLClass(IRI.create("http://www.co-ode.org/ontologies/pizza/pizza.owl#Margherita"))
      val rhs = dataFactory.getOWLClass(IRI.create("http://www.co-ode.org/ontologies/pizza/pizza.owl#VegetarianPizzaEquivalent2"))

      val proof = proofGenerator.proveSubsumption(lhs,rhs)

      //proofGenerator.proveUnsatisfiability(dataFactory.getOWLClass(IRI.create("http://www.co-ode.org/ontologies/pizza/pizza.owl#IceCream")))

      println("Done!")

      println()
      println("------------------------------------------")
      println()
      println("WE PRESENT TO YOU NOW")
      println("...")
      println("THE PROOF!")
      println()
      println()
      ProofFormatter.format(proof)

      ProofGraphVisualiser.drawProof(proof, "Margherita is a Pizza.png")

    /*  val visualiser = new ProofDotVisualizer()

      visualiser.setFileName("Margherita is a VegetarianPizza")

      visualiser.format(proofGenerator.proof)

     */
    }
}
