From 9ce65c5a963b03ee97fe9cb6c5aa65a3c04a80a8 Mon Sep 17 00:00:00 2001 From: yzhou Date: Tue, 21 Apr 2015 10:34:27 +0100 Subject: initial version --- .../ox/cs/pagoda/reasoner/ConsistencyManager.java | 269 +++++++++++++++++++++ 1 file changed, 269 insertions(+) create mode 100644 src/uk/ac/ox/cs/pagoda/reasoner/ConsistencyManager.java (limited to 'src/uk/ac/ox/cs/pagoda/reasoner/ConsistencyManager.java') diff --git a/src/uk/ac/ox/cs/pagoda/reasoner/ConsistencyManager.java b/src/uk/ac/ox/cs/pagoda/reasoner/ConsistencyManager.java new file mode 100644 index 0000000..a222645 --- /dev/null +++ b/src/uk/ac/ox/cs/pagoda/reasoner/ConsistencyManager.java @@ -0,0 +1,269 @@ +package uk.ac.ox.cs.pagoda.reasoner; + +import java.util.LinkedList; + +import org.semanticweb.HermiT.model.Atom; +import org.semanticweb.HermiT.model.AtomicConcept; +import org.semanticweb.HermiT.model.DLClause; +import org.semanticweb.HermiT.model.Variable; +import org.semanticweb.owlapi.model.OWLOntology; +import org.semanticweb.owlapi.model.OWLOntologyCreationException; +import org.semanticweb.owlapi.model.OWLOntologyManager; + +import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper; +import uk.ac.ox.cs.pagoda.query.AnswerTuples; +import uk.ac.ox.cs.pagoda.query.QueryManager; +import uk.ac.ox.cs.pagoda.query.QueryRecord; +import uk.ac.ox.cs.pagoda.reasoner.full.Checker; +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; +import uk.ac.ox.cs.pagoda.util.Utility; +import uk.ac.ox.cs.JRDFox.JRDFStoreException; +import uk.ac.ox.cs.JRDFox.store.DataStore; + +public class ConsistencyManager { + + protected MyQueryReasoner m_reasoner; + protected QueryManager m_queryManager; + + Timer t = new Timer(); + + public ConsistencyManager(MyQueryReasoner reasoner) { + m_reasoner = reasoner; + m_queryManager = reasoner.getQueryManager(); + } + + QueryRecord fullQueryRecord; + QueryRecord[] botQueryRecords; + + LinkedList toAddClauses; + + boolean checkRLLowerBound() { + fullQueryRecord = m_queryManager.create(QueryRecord.botQueryText, 0); + fullQueryRecord.updateLowerBoundAnswers(m_reasoner.rlLowerStore.evaluate(fullQueryRecord.getQueryText(), fullQueryRecord.getAnswerVariables())); + if (fullQueryRecord.getNoOfSoundAnswers() > 0) { + Utility.logInfo("Answers to bottom in the lower bound: ", fullQueryRecord.outputSoundAnswerTuple()); + return unsatisfiability(t.duration()); + } + return true; + } + + boolean checkELLowerBound() { + fullQueryRecord.updateLowerBoundAnswers(m_reasoner.elLowerStore.evaluate(fullQueryRecord.getQueryText(), fullQueryRecord.getAnswerVariables())); + if (fullQueryRecord.getNoOfSoundAnswers() > 0) { + Utility.logInfo("Answers to bottom in the lower bound: ", fullQueryRecord.outputSoundAnswerTuple()); + return unsatisfiability(t.duration()); + } + return true; + } + + boolean checkLazyUpper() { + if (m_reasoner.lazyUpperStore != null) { + AnswerTuples tuples = null; + try { + tuples = m_reasoner.lazyUpperStore.evaluate(fullQueryRecord.getQueryText(), fullQueryRecord.getAnswerVariables()); + if (!tuples.isValid()) { + Utility.logInfo("There are no contradictions derived in the lazy upper bound materialisation."); + return satisfiability(t.duration()); + } + } + finally { + if (tuples != null) tuples.dispose(); + } + } + return false; + } + + boolean check() { +// if (!checkRLLowerBound()) return false; +// if (!checkELLowerBound()) return false; +// if (checkLazyUpper()) return true; + + fullQueryRecord.updateUpperBoundAnswers(m_reasoner.trackingStore.evaluate(fullQueryRecord.getQueryText(), fullQueryRecord.getAnswerVariables())); + if (fullQueryRecord.getNoOfCompleteAnswers() == 0) + return satisfiability(t.duration()); + + extractBottomFragment(); + + try { + extractAxioms4Full(); + } catch (OWLOntologyCreationException e) { + e.printStackTrace(); + } + fullQueryRecord.saveRelevantClause(); + + boolean satisfiability; + + Checker checker; + for (QueryRecord r: getQueryRecords()) { + // TODO to be removed ... +// r.saveRelevantOntology("bottom" + r.getQueryID() + ".owl"); + checker = new HermitSummaryFilter(r); // m_reasoner.factory.getSummarisedReasoner(r); + satisfiability = checker.isConsistent(); + checker.dispose(); + if (!satisfiability) return unsatisfiability(t.duration()); + } + +// Checker checker = m_reasoner.factory.getSummarisedReasoner(fullQueryRecord); +// boolean satisfiable = checker.isConsistent(); +// checker.dispose(); +// if (!satisfiable) return unsatisfiability(t.duration()); + + return satisfiability(t.duration()); + } + + protected boolean unsatisfiability(double duration) { + fullQueryRecord.dispose(); + Utility.logDebug("The ontology and dataset is unsatisfiable."); + return false; + } + + protected boolean satisfiability(double duration) { + fullQueryRecord.dispose(); + Utility.logDebug("The ontology and dataset is satisfiable."); + return true; + } + + boolean fragmentExtracted = false; + + public void extractBottomFragment() { + if (fragmentExtracted) return ; + fragmentExtracted = true; + + UpperDatalogProgram upperProgram = m_reasoner.program.getUpper(); + int number = upperProgram.getBottomNumber(); + + if (number <= 1) { + botQueryRecords = new QueryRecord[] { fullQueryRecord }; + } + else { + QueryRecord[] tempQueryRecords = new QueryRecord[number - 1]; + QueryRecord record; + for (int i = 0; i < number - 1; ++i) { + tempQueryRecords[i] = record = m_queryManager.create(QueryRecord.botQueryText.replace("Nothing", "Nothing" + (i + 1)), 0, i + 1); + record.updateUpperBoundAnswers(m_reasoner.trackingStore.evaluate(record.getQueryText(), record.getAnswerVariables())); + } + + int bottomNumber = 0; + int[] group = new int[number - 1]; + for (int i = 0; i < number - 1; ++i) group[i] = i; + for (int i = 0; i < number - 1; ++i) + if (tempQueryRecords[i].processed()) tempQueryRecords[i].dispose(); + else if (group[i] == i) { + ++bottomNumber; + record = tempQueryRecords[i]; + for (int j = i + 1; j < number - 1; ++j) + if (record.hasSameGapAnswers(tempQueryRecords[j])) + group[j] = i; + } + + Utility.logInfo("There are " + bottomNumber + " different bottom fragments."); + toAddClauses = new LinkedList(); + int bottomCounter = 0; + botQueryRecords = new QueryRecord[bottomNumber]; + Variable X = Variable.create("X"); + for (int i = 0; i < number - 1; ++i) + if (!tempQueryRecords[i].processed()) + if (group[i] == i) { + botQueryRecords[bottomCounter] = record = tempQueryRecords[i]; + record.resetInfo(QueryRecord.botQueryText.replace("Nothing", "Nothing_final" + (++bottomCounter)), 0, group[i] = bottomCounter); + toAddClauses.add( + DLClause.create( + new Atom[] {Atom.create(AtomicConcept.create(AtomicConcept.NOTHING.getIRI() + "_final" + bottomCounter), X)}, + new Atom[] {Atom.create(AtomicConcept.create(AtomicConcept.NOTHING.getIRI() + (i + 1)), X)})); + } + else { + toAddClauses.add( + DLClause.create( + new Atom[] {Atom.create(AtomicConcept.create(AtomicConcept.NOTHING.getIRI() + "_final" + group[group[i]]), X)}, + new Atom[] {Atom.create(AtomicConcept.create(AtomicConcept.NOTHING.getIRI() + (i + 1)), X)})); + tempQueryRecords[i].dispose(); + } + + upperProgram.updateDependencyGraph(toAddClauses); + } + + String[] programs = collectTrackingProgramAndImport(); + if (programs.length == 0) + return ; + + DataStore store = m_reasoner.trackingStore.getDataStore(); + long oldTripleCount, tripleCount; + try { + Timer t1 = new Timer(); + oldTripleCount = store.getTriplesCount(); + for (String program: programs) + store.importRules(program); + store.applyReasoning(true); + tripleCount = store.getTriplesCount(); + + Utility.logInfo("tracking store after materialising tracking program: " + tripleCount + " (" + (tripleCount - oldTripleCount) + " new)", + "tracking store finished the materialisation of tracking program in " + t1.duration() + " seconds."); + + extractAxioms(); + store.clearRulesAndMakeFactsExplicit(); + } catch (JRDFStoreException e) { + e.printStackTrace(); + } catch (OWLOntologyCreationException e) { + e.printStackTrace(); + } + } + + private void extractAxioms4Full() throws OWLOntologyCreationException { + OWLOntologyManager manager = m_reasoner.encoder.getProgram().getOntology().getOWLOntologyManager(); + OWLOntology fullOntology = manager.createOntology(); + for (QueryRecord record: botQueryRecords) { + for (DLClause clause: record.getRelevantClauses()) { + fullQueryRecord.addRelevantClauses(clause); + } + manager.addAxioms(fullOntology, record.getRelevantOntology().getAxioms()); + } + fullQueryRecord.setRelevantOntology(fullOntology); + } + + private void extractAxioms() throws OWLOntologyCreationException { + OWLOntologyManager manager = m_reasoner.encoder.getProgram().getOntology().getOWLOntologyManager(); + for (QueryRecord record: botQueryRecords) { + record.setRelevantOntology(manager.createOntology()); + QueryTracker tracker = new QueryTracker(m_reasoner.encoder, m_reasoner.rlLowerStore, record); + m_reasoner.encoder.setCurrentQuery(record); + tracker.extractAxioms(m_reasoner.trackingStore); +// record.saveRelevantClause(); +// record.saveRelevantOntology("bottom" + record.getQueryID() + ".owl"); + Utility.logInfo("finish extracting axioms for bottom " + record.getQueryID()); + } + } + + private String[] collectTrackingProgramAndImport() { + String[] programs = new String[botQueryRecords.length]; + TrackingRuleEncoder encoder = m_reasoner.encoder; + + StringBuilder builder; + LinkedList currentClauses = new LinkedList(); + + for (int i = 0; i < botQueryRecords.length; ++i) { + encoder.setCurrentQuery(botQueryRecords[i]); + builder = new StringBuilder(encoder.getTrackingProgram()); +// encoder.saveTrackingRules("tracking_bottom" + (i + 1) + ".dlog"); + + for (DLClause clause: toAddClauses) + if (clause.getHeadAtom(0).getDLPredicate().toString().contains("_final" + (i + 1))) + currentClauses.add(clause); + + builder.append(DLClauseHelper.toString(currentClauses)); + programs[i] = builder.toString(); + + currentClauses.clear(); + } + + return programs; + } + + public QueryRecord[] getQueryRecords() { + return botQueryRecords; + } + +} -- cgit v1.2.3