From e3d640788cf5804d3f0d5213f52f0dc8b78df1ca Mon Sep 17 00:00:00 2001 From: Federico Igne Date: Wed, 18 May 2022 15:31:40 +0100 Subject: feat: add consistency check for ACQuA query reasoner --- .../ox/cs/acqua/reasoner/AcquaQueryReasoner.scala | 23 +- .../ox/cs/acqua/reasoner/ConsistencyManager.scala | 336 +++++++++++++++++++++ 2 files changed, 347 insertions(+), 12 deletions(-) create mode 100644 src/main/scala/uk/ac/ox/cs/acqua/reasoner/ConsistencyManager.scala diff --git a/src/main/scala/uk/ac/ox/cs/acqua/reasoner/AcquaQueryReasoner.scala b/src/main/scala/uk/ac/ox/cs/acqua/reasoner/AcquaQueryReasoner.scala index de6e87c..2ee0f64 100644 --- a/src/main/scala/uk/ac/ox/cs/acqua/reasoner/AcquaQueryReasoner.scala +++ b/src/main/scala/uk/ac/ox/cs/acqua/reasoner/AcquaQueryReasoner.scala @@ -33,7 +33,6 @@ import uk.ac.ox.cs.pagoda.query.{ } import uk.ac.ox.cs.pagoda.query.QueryRecord.Step import uk.ac.ox.cs.pagoda.reasoner.{ - ConsistencyManager, MyQueryReasoner, QueryReasoner } @@ -62,7 +61,7 @@ class AcquaQueryReasoner(val ontology: Ontology) /** Compatibility convertions between PAGOdA and RSAComb */ import uk.ac.ox.cs.acqua.implicits.PagodaConverters._ - private var encoder: Option[TrackingRuleEncoder] = None + var encoder: Option[TrackingRuleEncoder] = None private var lazyUpperStore: Option[MultiStageQueryEngine] = None; private val timer: Timer = new Timer(); @@ -70,25 +69,25 @@ class AcquaQueryReasoner(val ontology: Ontology) private var _isConsistent: ConsistencyStatus = StatusUnchecked // TODO: explicit casting to MyQueryReasoner makes no sense. Find // another solution. Probably requires changing PAGOdA source code. - private val consistencyManager: ConsistencyManager = new ConsistencyManager(this.asInstanceOf[MyQueryReasoner]) + private val consistencyManager: ConsistencyManager = new ConsistencyManager(this) - private val rlLowerStore: BasicQueryEngine = new BasicQueryEngine("rl-lower-bound") - private val elLowerStore: KarmaQueryEngine = new KarmaQueryEngine("elho-lower-bound") + val rlLowerStore: BasicQueryEngine = new BasicQueryEngine("rl-lower-bound") + val elLowerStore: KarmaQueryEngine = new KarmaQueryEngine("elho-lower-bound") private lazy val lowerRSAEngine = new RSACombQueryReasoner(ontology, new Lowerbound) private lazy val upperRSAEngine = new RSACombQueryReasoner(ontology, new Upperbound) - private val trackingStore = new MultiStageQueryEngine("tracking", false); + val trackingStore = new MultiStageQueryEngine("tracking", false); var predicatesWithGap: Seq[String] = Seq.empty /* Load ontology into PAGOdA */ - private val datalog = new DatalogProgram(ontology.origin); + val datalog = new DatalogProgram(ontology.origin); //datalog.getGeneral().save(); if (!datalog.getGeneral().isHorn()) lazyUpperStore = Some(new MultiStageQueryEngine("lazy-upper-bound", true)) - importData(datalog.getAdditionalDataFile()); + importData(datalog.getAdditionalDataFile()) private val elhoOntology: OWLOntology = new ELHOProfile().getFragment(ontology.origin); - elLowerStore.processOntology(elhoOntology); + elLowerStore processOntology elhoOntology /** Performs nothing. @@ -121,7 +120,7 @@ class AcquaQueryReasoner(val ontology: Ontology) /* RL lower-bound check */ rlLowerStore.importRDFData(name, datafile); rlLowerStore.materialise("lower program", datalog.getLower.toString); - if (!consistencyManager.checkRLLowerBound()) { + if (!consistencyManager.checkRLLowerBound) { Utility logDebug s"time for satisfiability checking: ${timer.duration()}" _isConsistent = StatusInconsistent return false @@ -134,7 +133,7 @@ class AcquaQueryReasoner(val ontology: Ontology) elLowerStore.materialise("saturate named individuals", originalMarkProgram); elLowerStore.materialise("lower program", datalog.getLower.toString); elLowerStore.initialiseKarma(); - if (!consistencyManager.checkELLowerBound()) { + if (!consistencyManager.checkELLowerBound) { Utility logDebug s"time for satisfiability checking: ${timer.duration()}" _isConsistent = StatusInconsistent return false @@ -187,7 +186,7 @@ class AcquaQueryReasoner(val ontology: Ontology) */ def isConsistent(): Boolean = { if (_isConsistent == StatusUnchecked) { - _isConsistent = consistencyManager.check() + _isConsistent = consistencyManager.check Utility logDebug s"time for satisfiability checking: ${timer.duration()}" } Utility logInfo s"The ontology is ${_isConsistent}!" diff --git a/src/main/scala/uk/ac/ox/cs/acqua/reasoner/ConsistencyManager.scala b/src/main/scala/uk/ac/ox/cs/acqua/reasoner/ConsistencyManager.scala new file mode 100644 index 0000000..4b73f88 --- /dev/null +++ b/src/main/scala/uk/ac/ox/cs/acqua/reasoner/ConsistencyManager.scala @@ -0,0 +1,336 @@ +package uk.ac.ox.cs.acqua.reasoner + +import java.util.LinkedList +import scala.collection.JavaConverters._ + +import org.semanticweb.HermiT.model.{ + Atom, + AtomicConcept, + DLClause, + Variable +} +import org.semanticweb.owlapi.model.{ + OWLOntology, + OWLOntologyCreationException, + OWLOntologyManager +} +import uk.ac.ox.cs.JRDFox.JRDFStoreException +// import uk.ac.ox.cs.JRDFox.store.DataStore; +import uk.ac.ox.cs.JRDFox.store.DataStore.UpdateType +import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper +import uk.ac.ox.cs.pagoda.query.{ + AnswerTuples, + QueryRecord +} +// import uk.ac.ox.cs.pagoda.query.QueryManager; +import uk.ac.ox.cs.pagoda.reasoner.full.Checker +import uk.ac.ox.cs.pagoda.reasoner.light.BasicQueryEngine +// import uk.ac.ox.cs.pagoda.rules.UpperDatalogProgram; +import uk.ac.ox.cs.pagoda.summary.HermitSummaryFilter +import uk.ac.ox.cs.pagoda.tracking.QueryTracker +// import uk.ac.ox.cs.pagoda.tracking.TrackingRuleEncoder; +import uk.ac.ox.cs.pagoda.util.{ + Timer, + Utility +} +import uk.ac.ox.cs.pagoda.util.disposable.{ + Disposable, + DisposedException +} +// import uk.ac.ox.cs.pagoda.util.disposable.DisposedException; + +/** Consistency checker inspired by [[uk.ac.ox.cs.pagoda.reaseoner.ConsistencyManager]]. + * + * @param reasoner an [[AcquaQueryReasoner]] instance + * + * TODO: document public methods and rework the code to be more + * Scala-esque. + */ +class ConsistencyManager( + protected val reasoner: AcquaQueryReasoner +) extends Disposable { + + protected val queryManager = reasoner.getQueryManager + private val timer = new Timer() + private var fragmentExtracted = false + + private var fullQueryRecord: Option[QueryRecord] = None + private var botQueryRecords = Array.empty[QueryRecord] + private var toAddClauses = new LinkedList[DLClause]() + + + override def dispose(): Unit = { + super.dispose() + fullQueryRecord.map(_.dispose()) + } + + /** + * + */ + def extractBottomFragment(): Unit = { + if (isDisposed) throw new DisposedException + if (!fragmentExtracted) { + fragmentExtracted = true + + val upperProgram = reasoner.datalog.getUpper + val number = upperProgram.getBottomNumber + + if (number <= 1) { + botQueryRecords = Array[QueryRecord](fullQueryRecord.get) + } else { + var record: QueryRecord = null + var tempQueryRecords = new Array[QueryRecord](number-1) + for(i <- 0 until (number-1)) { + record = queryManager.create(QueryRecord.botQueryText.replace("Nothing", s"Nothing${i+1}"), 0, i + 1) + tempQueryRecords(i) = record + var iter: AnswerTuples = null + try { + iter = reasoner.trackingStore.evaluate(record.getQueryText, record.getAnswerVariables) + record updateUpperBoundAnswers iter + } finally { + if (iter != null) iter.dispose() + } + } + + var bottomNumber = 0; + val group = (0 until (number-1)).toArray + for(i <- 0 until (number-1)) + if (tempQueryRecords(i).isProcessed) + tempQueryRecords(i).dispose() + else if(group(i) == i) { + bottomNumber += 1 + record = tempQueryRecords(i) + for (j <- i until (number-1)) + if (record hasSameGapAnswers tempQueryRecords(j)) + group(j) = i + } + + Utility logInfo s"There are $bottomNumber different bottom fragments." + toAddClauses = new LinkedList[DLClause]() + var bottomCounter = 0 + botQueryRecords = new Array[QueryRecord](bottomNumber) + val X = Variable.create("X") + for(i <- 0 until (number-1)) { + if (!tempQueryRecords(i).isDisposed() && !tempQueryRecords(i).isProcessed()) { + if (group(i) == i) { + record = tempQueryRecords(i) + botQueryRecords(bottomCounter) = record + bottomCounter += 1 + group(i) = bottomCounter + record.resetInfo( + QueryRecord.botQueryText.replace( + "Nothing", + s"Nothing_final$bottomCounter" + ), 0, bottomCounter) + toAddClauses.add( + DLClause.create( + Array[Atom](Atom.create(AtomicConcept.create(s"${AtomicConcept.NOTHING.getIRI}_final$bottomCounter"), X)), + Array[Atom](Atom.create(AtomicConcept.create(s"${AtomicConcept.NOTHING.getIRI}${i+1}"), X)) + ) + ) + } else { + toAddClauses.add( + DLClause.create( + Array[Atom](Atom.create(AtomicConcept.create(s"${AtomicConcept.NOTHING.getIRI}_final${group(group(i))}"), X)), + Array[Atom](Atom.create(AtomicConcept.create(s"${AtomicConcept.NOTHING.getIRI}${i+1}"), X)) + ) + ) + tempQueryRecords(i).dispose() + } + } + } + upperProgram updateDependencyGraph toAddClauses + } + + val programs: Array[String] = collectTrackingProgramAndImport() + if (programs.length > 0) { + val datastore = reasoner.trackingStore.getDataStore + var oldTripleCount: Long = 0 + var tripleCount: Long = 0 + try { + val t1 = new Timer(); + oldTripleCount = datastore.getTriplesCount + for(program <- programs) + datastore.importRules(program, UpdateType.ScheduleForAddition) + datastore applyReasoning true + tripleCount = datastore.getTriplesCount + + Utility logDebug s"tracking store after materialising tracking program: $tripleCount (${tripleCount - oldTripleCount} new)" + Utility logDebug s"tracking store finished the materialisation of tracking program in ${t1.duration()} seconds." + + extractAxioms() + datastore.clearRulesAndMakeFactsExplicit() + } catch { + case e: JRDFStoreException => e.printStackTrace() + case e: OWLOntologyCreationException => e.printStackTrace() + } + } + } + } + + /** + * + * @note provided for compatibility reasons + */ + val getQueryRecords: Array[QueryRecord] = botQueryRecords + + /** RL lower bound check for satisfiability. */ + lazy val checkRLLowerBound: Boolean = { + if (isDisposed) throw new DisposedException + val record: QueryRecord = queryManager.create(QueryRecord.botQueryText, 0) + fullQueryRecord = Some(record) + + var iter: AnswerTuples = null + try { + iter = reasoner.rlLowerStore.evaluate(record.getQueryText, record.getAnswerVariables) + record updateLowerBoundAnswers iter + } finally { + iter.dispose() + } + + if (record.getNoOfSoundAnswers > 0) { + Utility logInfo s"Answers to bottom in the lower bound: ${record.outputSoundAnswerTuple}" + } + record.getNoOfSoundAnswers <= 0 + } + + /** ELHO lower bound check for satisfiability */ + lazy val checkELLowerBound: Boolean = { + if (isDisposed) throw new DisposedException + val record: QueryRecord = fullQueryRecord.get + + val answers: AnswerTuples = + reasoner.elLowerStore.evaluate( + record.getQueryText, + record.getAnswerVariables + ) + record updateLowerBoundAnswers answers + + if (record.getNoOfSoundAnswers > 0) { + Utility logInfo s"Answers to bottom in the lower bound: ${record.outputSoundAnswerTuple}" + } + record.getNoOfSoundAnswers <= 0 + } + + /** + * + */ + def checkUpper(upperStore: BasicQueryEngine): Boolean = { + if (isDisposed) throw new DisposedException + val record = fullQueryRecord.get + + if (upperStore != null) { + var tuples: AnswerTuples = null + try { + tuples = upperStore.evaluate(record.getQueryText, record.getAnswerVariables) + if (!tuples.isValid) { + Utility logInfo s"There are no contradictions derived in ${upperStore.getName} materialisation." + Utility logDebug "The ontology and dataset is satisfiable." + return true + } + } finally { + if (tuples != null) tuples.dispose() + } + } + false + } + + /** True if the KB associate with the [[reasoner]] is consistent. + * + * This is the main entry point of the consistency checker. + */ + lazy val check: Boolean = { + if (isDisposed) throw new DisposedException + val record = fullQueryRecord.get + var tuples: AnswerTuples = null + + try { + tuples = reasoner.trackingStore.evaluate( + record.getQueryText, + record.getAnswerVariables + ) + record updateUpperBoundAnswers tuples + } finally { + if (tuples != null) tuples.dispose() + } + + var satisfiability = true + if (record.getNoOfCompleteAnswers != 0) { + + extractBottomFragment() + + try { + extractAxioms4Full() + } catch { + case e: OWLOntologyCreationException => e.printStackTrace() + } + + var checker: Checker = null + for (r <- getQueryRecords) { + checker = new HermitSummaryFilter(r, true) + satisfiability = checker.isConsistent() + checker.dispose() + } + } + satisfiability + } + + /** + * + */ + private def extractAxioms4Full(): Unit = { + val manager: OWLOntologyManager = + reasoner.encoder.get + .getProgram + .getOntology + .getOWLOntologyManager + val fullOntology: OWLOntology = manager.createOntology() + for (record <- botQueryRecords) { + for (clause <- record.getRelevantClauses.asScala) { + fullQueryRecord.get addRelevantClauses clause + } + manager.addAxioms( + fullOntology, + record.getRelevantOntology.getAxioms() + ) + } + fullQueryRecord.get.setRelevantOntology(fullOntology) + } + + /** + * + */ + private def extractAxioms(): Unit = { + val manager: OWLOntologyManager = + reasoner.encoder.get + .getProgram + .getOntology + .getOWLOntologyManager + for (record <- botQueryRecords) { + record setRelevantOntology manager.createOntology() + val tracker: QueryTracker = new QueryTracker(reasoner.encoder.get, reasoner.rlLowerStore, record) + reasoner.encoder.get setCurrentQuery record + tracker extractAxioms reasoner.trackingStore + Utility logInfo s"finish extracting axioms for bottom ${record.getQueryID}" + } + } + + /** + * + */ + private def collectTrackingProgramAndImport(): Array[String] = { + val programs = new Array[String](botQueryRecords.length) + val encoder = reasoner.encoder.get + val currentClauses: LinkedList[DLClause] = new LinkedList[DLClause]() + + botQueryRecords.zipWithIndex map { case (record,i) => { + encoder setCurrentQuery record + val builder = new StringBuilder(encoder.getTrackingProgram) + val currentClauses = toAddClauses.asScala.filter{clause => + clause.getHeadAtom(0).getDLPredicate.toString().contains(s"_final${i + 1}") + }.asJava + builder append (DLClauseHelper toString currentClauses) + builder.toString + }} + } +} -- cgit v1.2.3