Mentions légales du service

Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found

Target

Select target project
  • rules/integraal
  • ulliana/integraal
2 results
Show changes
Commits on Source (229)
Showing
with 1685196 additions and 168 deletions
......@@ -88,3 +88,4 @@ tatooinetmp.conf
# ctags file
tags
build.xml
/integraal/integraal-explanation/gsat.gcnf
This diff is collapsed.
......@@ -94,36 +94,6 @@
<build>
<plugins>
<plugin>
<groupId>org.apache.maven.plugins</groupId>
<artifactId>maven-shade-plugin</artifactId>
<version>${maven-shade-plugin-version}</version>
<executions>
<execution>
<phase>package</phase>
<goals>
<goal>shade</goal>
</goals>
<configuration>
<shadedArtifactAttached>true</shadedArtifactAttached>
<shadedClassifierName>jar-with-dependencies</shadedClassifierName>
<finalName>integraal-with-dependencies</finalName>
<filters>
<filter>
<artifact>*:*</artifact>
<excludes>
<exclude>**/module-info.*</exclude>
<exclude>META-INF/*.SF</exclude>
<exclude>META-INF/**/*.class</exclude>
<exclude>META-INF/*.DSA</exclude>
<exclude>META-INF/*.RSA</exclude>
</excludes>
</filter>
</filters>
</configuration>
</execution>
</executions>
</plugin>
<plugin>
<groupId>org.apache.maven.plugins</groupId>
<artifactId>maven-compiler-plugin</artifactId>
......
......@@ -118,79 +118,6 @@
<build>
<plugins>
<plugin>
<groupId>org.apache.maven.plugins</groupId>
<artifactId>maven-shade-plugin</artifactId>
<version>${maven-shade-plugin-version}</version>
<executions>
<execution>
<id>build-integraal-commander</id>
<phase>package</phase>
<goals>
<goal>shade</goal>
</goals>
<configuration>
<transformers>
<transformer
implementation="org.apache.maven.plugins.shade.resource.ServicesResourceTransformer" />
<transformer
implementation="org.apache.maven.plugins.shade.resource.ManifestResourceTransformer">
<mainClass>
fr.boreal.api.integraal_commander.InteGraalCommander</mainClass>
</transformer>
</transformers>
<finalName>integraal-commander</finalName>
<shadedArtifactAttached>true</shadedArtifactAttached>
<shadedClassifierName>jar-with-dependencies</shadedClassifierName>
<filters>
<filter>
<artifact>*:*</artifact>
<excludes>
<exclude>**/module-info.*</exclude>
<exclude>META-INF/*.SF</exclude>
<exclude>META-INF/**/*.class</exclude>
<exclude>META-INF/*.DSA</exclude>
<exclude>META-INF/*.RSA</exclude>
</excludes>
</filter>
</filters>
</configuration>
</execution>
<execution>
<id>build-integraal-cli</id>
<phase>package</phase>
<goals>
<goal>shade</goal>
</goals>
<configuration>
<transformers>
<transformer
implementation="org.apache.maven.plugins.shade.resource.ServicesResourceTransformer" />
<transformer
implementation="org.apache.maven.plugins.shade.resource.ManifestResourceTransformer">
<mainClass>
fr.boreal.api.integraal_repl.IGRepl</mainClass>
</transformer>
</transformers>
<finalName>integraal-cli</finalName>
<shadedArtifactAttached>true</shadedArtifactAttached>
<shadedClassifierName>jar-with-dependencies</shadedClassifierName>
<filters>
<filter>
<artifact>*:*</artifact>
<excludes>
<exclude>**/module-info.*</exclude>
<exclude>META-INF/*.SF</exclude>
<exclude>META-INF/**/*.class</exclude>
<exclude>META-INF/*.DSA</exclude>
<exclude>META-INF/*.RSA</exclude>
</excludes>
</filter>
</filters>
</configuration>
</execution>
</executions>
</plugin>
<plugin>
<groupId>org.apache.maven.plugins</groupId>
<artifactId>maven-compiler-plugin</artifactId>
......
......@@ -86,7 +86,7 @@ public class IGCommands {
* Prints the substitutions from the iterator.
*
* @param subIt The iterator of substitutions containing the query results.
* @param vars The variables to print; this provides the order of the variables
* @param varsOrder The variables to print; this provides the order of the variables
* @param writer The DlgpWriter object used to write the results.break;
* @param max The maximum number of substitutions to print.
*/
......
......@@ -350,7 +350,8 @@ public enum InteGraalKeywords {
/**
* GRD Scheduler
*/
GRD
GRD,
BY_PREDICATE
}
/**
......
This diff is collapsed.
# Use an official Python image with Debian-based OS
FROM python:3.9-slim
# Set working directory
WORKDIR /usr/local/bin
# Install system dependencies
RUN apt-get update -y && apt-get install -y \
git \
build-essential \
zlib1g-dev \
&& rm -rf /var/lib/apt/lists/*
# Clone and build MARCO
RUN git clone https://github.com/liffiton/MARCO && \
cd MARCO/src/pyminisolvers && make && \
cd /usr/local/bin && mv ./MARCO/* .
# Ensure MARCO-MUS directory exists and move MARCO files
RUN mkdir -p /usr/local/bin/MARCO-MUS && \
mv /usr/local/bin/marco.py /usr/local/bin/MARCO-MUS/ && \
chmod +x /usr/local/bin/MARCO-MUS/marco.py
# Set environment variables for MARCO
ENV PATH="/usr/local/bin/MARCO-MUS:${PATH}"
ENV PYTHONPATH="/usr/local/bin/src:${PYTHONPATH}"
# Debugging step: Verify MARCO installation
RUN echo "===== Checking MARCO Installation =====" && \
ls -l /usr/local/bin/MARCO-MUS/ && \
echo "===== Checking Python Installation =====" && \
which python3 && python3 --version
# Test MARCO Execution inside Docker
RUN /usr/local/bin/MARCO-MUS/marco.py --help || echo "MARCO execution failed"
# Set MARCO as the default command
ENTRYPOINT ["python", "/usr/local/bin/MARCO-MUS/marco.py"]
......@@ -17,9 +17,15 @@
<description>Facilities for explaining answers to queries</description>
<dependencies>
<dependency>
<groupId>com.opencsv</groupId>
<artifactId>opencsv</artifactId>
<version>5.7.1</version> <!-- or the latest version -->
</dependency>
<dependency>
<groupId>${groupId}</groupId>
<artifactId>integraal-model</artifactId>
<version>${revision}</version>
</dependency>
<dependency>
<groupId>${groupId}</groupId>
......@@ -49,6 +55,19 @@
<groupId>${groupId}</groupId>
<artifactId>integraal-component</artifactId>
</dependency>
<dependency>
<groupId>org.ow2.sat4j</groupId>
<artifactId>org.ow2.sat4j.pb</artifactId>
<version>2.3.6</version>
</dependency>
<dependency>
<groupId>org.ow2.sat4j</groupId>
<artifactId>org.ow2.sat4j.pom</artifactId>
<version>2.3.6</version>
<type>pom</type>
</dependency>
<dependency>
<groupId>org.junit.jupiter</groupId>
<artifactId>junit-jupiter-api</artifactId>
......@@ -64,11 +83,35 @@
<artifactId>junit</artifactId>
<scope>test</scope>
</dependency>
<dependency>
<groupId>org.mockito</groupId>
<artifactId>mockito-core</artifactId>
<scope>test</scope>
</dependency>
<dependency>
<groupId>org.ow2.sat4j</groupId>
<artifactId>org.ow2.sat4j.sat</artifactId>
<version>2.3.6</version>
</dependency>
<dependency>
<groupId>org.ow2.sat4j</groupId>
<artifactId>org.ow2.sat4j.core</artifactId>
<version>2.3.6</version>
</dependency>
<dependency>
<groupId>org.mockito</groupId>
<artifactId>mockito-core</artifactId>
<scope>test</scope>
<groupId>fr.lirmm.graphik</groupId>
<artifactId>integraal-model</artifactId>
</dependency>
</dependencies>
</dependencies>
<build>
<testResources>
<testResource>
<directory>src/test/resources</directory>
<excludes>
<exclude>**/*</exclude>
</excludes>
</testResource>
</testResources>
</build>
</project>
\ No newline at end of file
package fr.boreal.explanation;
import fr.boreal.explanation.kb_gri.explainers.static_gri.FactSupportExplainer_KBGRI;
import fr.boreal.explanation.kb_gri.explainers.static_gri.KBSupportExplainer_KBGRI;
import fr.boreal.io.api.ParseException;
import fr.boreal.io.dlgp.DlgpParser;
import fr.boreal.model.kb.api.FactBase;
import fr.boreal.model.kb.api.KnowledgeBase;
import fr.boreal.model.kb.api.RuleBase;
import fr.boreal.model.kb.impl.KnowledgeBaseImpl;
import fr.boreal.model.kb.impl.RuleBaseImpl;
import fr.boreal.model.logicalElements.api.Atom;
import fr.boreal.model.logicalElements.factory.api.PredicateFactory;
import fr.boreal.model.logicalElements.factory.api.TermFactory;
import fr.boreal.model.logicalElements.factory.impl.SameObjectPredicateFactory;
import fr.boreal.model.logicalElements.factory.impl.SameObjectTermFactory;
import fr.boreal.model.rule.api.FORule;
import fr.boreal.storage.natives.SimpleInMemoryGraphStore;
import java.io.File;
import java.io.FileNotFoundException;
import java.util.ArrayList;
import java.util.Collection;
import java.util.Set;
public class InternalDLGPParser {
public InternalDLGPParser(File datalogProgrammeFile, File factsFile, File query_file) throws FileNotFoundException {
PredicateFactory predicateFactory = SameObjectPredicateFactory.instance();
TermFactory termFactory = SameObjectTermFactory.instance();
RuleBase rb = ParserForDLGP.parseRB(datalogProgrammeFile);
FactBase fb = ParserForDLGP.parseFB(datalogProgrammeFile);
KnowledgeBase kb = new KnowledgeBaseImpl(fb,rb);
Collection<Atom> queryAtoms = ParserForDLGP.parseQueries(query_file);
FactSupportExplainer_KBGRI explainer;
explainer = new FactSupportExplainer_KBGRI(kb);
for (Atom queryAtom : queryAtoms) {
Set<FactBase> explanations = explainer.getAllExplanations(queryAtom);
if (explanations.isEmpty()) {
throw new RuntimeException("No explanations found for " + queryAtom);
}
}
}
public static class ParserForDLGP {
public static KnowledgeBase parseKB(File dlgpFile) throws FileNotFoundException {
FactBase fb = new SimpleInMemoryGraphStore();
Collection<FORule> rules = new ArrayList<FORule>();
int ruleLabelNb = 0;
try (DlgpParser dlgp_parseur = new DlgpParser(dlgpFile)) {
while (dlgp_parseur.hasNext()) {
try {
Object result = dlgp_parseur.next();
if (result instanceof Atom) {
fb.add((Atom)result);
} else if (result instanceof FORule) {
((FORule) result).setLabel("r"+ruleLabelNb++);
rules.add((FORule)result);
}
} catch (ParseException e) {
throw new RuntimeException(
String.format("Error with the file %s ", dlgpFile),
e);
}
}
}
RuleBase rb = new RuleBaseImpl(rules);
KnowledgeBase kb = new KnowledgeBaseImpl(fb, rb);
return kb;
}
public static FactBase parseFB(File dlgpFile) throws FileNotFoundException {
FactBase fb = new SimpleInMemoryGraphStore();
try (DlgpParser dlgp_parseur = new DlgpParser(dlgpFile)) {
while (dlgp_parseur.hasNext()) {
try {
Object result = dlgp_parseur.next();
if (result instanceof Atom) {
fb.add((Atom)result);
}
} catch (ParseException e) {
throw new RuntimeException(
String.format("Error with the file %s ", dlgpFile),
e);
}
}
}
return fb;
}
public static RuleBase parseRB(File dlgpFile) throws FileNotFoundException {
Collection<FORule> rules = new ArrayList<FORule>();
try (DlgpParser dlgp_parseur = new DlgpParser(dlgpFile)) {
while (dlgp_parseur.hasNext()) {
try {
Object result = dlgp_parseur.next();if (result instanceof FORule) {
rules.add((FORule)result);
}
} catch (ParseException e) {
throw new RuntimeException(
String.format("Error with the file %s ", dlgpFile),
e);
}
}
}
RuleBase rb = new RuleBaseImpl(rules);
return rb;
}
public static Collection<Atom> parseQueries(File dlgpFile) throws FileNotFoundException {
try (DlgpParser dlgp_parseur = new DlgpParser(dlgpFile)) {
Collection<Atom> queryAtoms = new ArrayList<Atom>();
while (dlgp_parseur.hasNext()) {
try {
Object result = dlgp_parseur.next();
if (result instanceof Atom) {
queryAtoms.add((Atom)result);
}
} catch (ParseException e) {
throw new RuntimeException(
String.format("Error with the file %s ", dlgpFile),
e);
}
}
return queryAtoms;
}
}
}
}
\ No newline at end of file
package fr.boreal.explanation.api;
import fr.boreal.model.formula.api.FOFormulaConjunction;
import fr.boreal.model.kb.api.KnowledgeBase;
import fr.boreal.model.logicalElements.api.Atom;
import fr.boreal.model.query.api.Query;
import java.util.Arrays;
import java.util.Set;
/**
* Interface for an explainer which supports only ground atomic queries (expressed as atoms).
*
* @param <ExplanationType> the type of the (set of) explanations which is returned by the enumerator
*/
public interface AtomicQueryExplanationEnumerator<ExplanationType extends Object> {
/**
* Checks if an atom can be explained
*
* @param query
* @return true iff the query contains only constants and literals
*/
default boolean canExplain(KnowledgeBase kb, Atom query) {
var queryOK = Arrays.stream(query.getTerms()).allMatch(term -> term.isConstant() || term.isLiteral());
// check that all rules body and head are conjunctions
// TODO : check more in depth that the FOFormulaConjunction contains only atoms
// TODO : check that in the the data (be careful of federations) there are only constants and literals
// TODO : check that in the rules there are no functional terms
var rulesOK = true;
for (var r : kb.getRuleBase().getRules()) {
// rules must have a label
if (r.getLabel() == null || r.getLabel().isBlank()) {
throw new RuntimeException("rule label is empty: " + r);
}
if (!(r.getBody() instanceof FOFormulaConjunction || r.getBody() instanceof Atom)) {
rulesOK = false;
break;
}
if (!(r.getHead() instanceof FOFormulaConjunction || r.getHead() instanceof Atom)) {
rulesOK = false;
break;
}
}
return queryOK && rulesOK;
}
/**
*
* @param query
* @return the set of explanations for the query on the current KB
*/
Set<ExplanationType> explain(Atom query);
}
package fr.boreal.explanation.api.encoders;
import fr.boreal.model.logicalElements.api.Atom;
import java.util.Set;
import java.util.function.Predicate;
/**
* Computes at GSAT encoding of the GRI and the Query for GMUS enumeration
* @param <DataStructureType> the data structure holding the GRI
* @param <QueryType> the query type
*/
public interface GSATEncoder_GRI<DataStructureType, QueryType> {
/**
*
* @param filteredGRI
* @param query
* @param belongsToInitialFactbase
* @return at GSAT encoding of the filteredGRI and the Query for GMUS enumeration
*/
GSATEncodingResult_GRI encode(DataStructureType filteredGRI, QueryType query, Predicate<Atom> belongsToInitialFactbase);
}
package fr.boreal.explanation.api.encoders;
import com.google.common.collect.BiMap;
import fr.boreal.model.logicalElements.api.Atom;
import fr.boreal.model.rule.api.FORule;
import java.util.List;
import java.util.Set;
/**
*
* @param propVarIDMap map from propositional variables (as integers) to the corresponding KB atom or (term identifyin and atom)
* @param factIDMap map from bodyAtoms to integers
* @param ruleIDMap maps from rules to integers
* @param clauses encoded GSAT
* @param nbGroup number of groups in the GSAT
*/
public record GSATEncodingResult_GRI(BiMap<Atom, Integer> propVarIDMap,
//TODO : can we put a more precise object?
BiMap<Integer, Atom> factIDMap,
BiMap<Integer, FORule> ruleIDMap,
List<List<Integer>> clauses, int nbGroup) {}
package fr.boreal.explanation.api.explainers;
import fr.boreal.explanation.api.validators.AtomicKBExplanationValidator;
import fr.boreal.model.kb.api.KnowledgeBase;
import fr.boreal.model.logicalElements.api.Atom;
import java.util.Collection;
/**
* Interface for an explainer which supports only ground atomic queries (expressed as bodyAtoms).
*
* @param <ExplanationType> the type of the (set of) explanations which is returned by the enumerator
*/
public interface AtomicQueryExplainer<ExplanationType> extends QueryExplainer<ExplanationType, Atom, KnowledgeBase> {
/**
* Checks if an atom can be explained
*
* @param query
* @return true iff the query contains only constants and literals
*/
default boolean canExplain(KnowledgeBase kb, Atom query) {
return AtomicKBExplanationValidator.isValid(kb,query);
}
/**
* Runs the pipeline (with timing) on the given dataset and queries.
*/
void pipelineWithTimer(String datasetName, Collection<Atom> queries);
}
package fr.boreal.explanation.api.explainers;
import java.util.Iterator;
import java.util.Set;
/**
* Interface for an explainer
*
* @param <ExplanationType> the type of the (set of) explanations which is returned by the enumerator
* @param <QueryType> the type of the query
* @param <ExplanationContext> the context to use for finding explanations (eg. a knowledge base, a factbase, a rulebase)
*/
public interface QueryExplainer<ExplanationType, QueryType, ExplanationContext> {
/**
* @param query
* @return the set of explanations for the query on the current KB
*/
Set<ExplanationType> getAllExplanations(QueryType query);
/**
* @param query
* @return an iterator for the set of explanations for the query on the current KB
*/
default Iterator<ExplanationType> getExplanations(QueryType query) {
return getAllExplanations(query).iterator();
}
/**
* Checks if an atom can be explained
*
* @param query
* @param context to use for finding explanations (eg. a knowledge base, a factbase, a rulebase)
* @return true iff the explainer surpports the query and the knowledget base
*/
boolean canExplain(ExplanationContext context, QueryType query);
}
package fr.boreal.explanation.api.processors;
import com.google.common.collect.BiMap;
import fr.boreal.explanation.api.encoders.GSATEncoder_GRI;
import fr.boreal.explanation.api.solver.Solver;
import fr.boreal.explanation.solving_enumerating.marco.MARCOGMUSSolver;
import fr.boreal.explanation.solving_enumerating.marco.MARCOGMUSDecoder;
import fr.boreal.explanation.api.encoders.GSATEncodingResult_GRI;
import fr.boreal.explanation.solving_enumerating.sat4j.Sat4JSolver;
import fr.boreal.model.logicalElements.api.Atom;
import fr.boreal.model.rule.api.FORule;
import java.util.List;
import java.util.Set;
import java.util.function.Predicate;
public abstract class AbstractExplanationsProcessor_GMUS_GRI<ExplanationType, DataStructureGRI>
implements ExplanationProcessor_GRI<ExplanationType, DataStructureGRI, Atom> {
protected static Solver solver;
protected static final MARCOGMUSDecoder translator = new MARCOGMUSDecoder();
protected GSATEncodingResult_GRI encoding;
protected Object gmuses;
protected Set<ExplanationType> result;
protected AbstractExplanationsProcessor_GMUS_GRI(Solver solver) {
this.solver=solver;
}
@Override
public Set<ExplanationType> computeAllExplanations(DataStructureGRI filteredGRI, Atom query, Predicate<Atom> belongsToInitialFactbase) {
if(belongsToInitialFactbase.test(query)) {
return getQueryIsInTheIntitialFactbaseExplanation(query);
}
encode(filteredGRI, query, belongsToInitialFactbase);
assert encoding != null;
solve();
translate();
return result;
}
public void encode(DataStructureGRI filteredGRI, Atom query,Predicate<Atom> belongsToInitialFactbase) {
GSATEncoder_GRI encoder = getEncoder();
encoding = encoder.encode(filteredGRI, query,belongsToInitialFactbase);
assert encoding != null;
}
public void solve() {
this.gmuses = switch (solver) {
case MARCOGMUSSolver marco ->
marco.solve(encoding.propVarIDMap(), encoding.clauses(), encoding.nbGroup());
case Sat4JSolver ignore -> Sat4JSolver.enumerateGMUSes(encoding.clauses());
default -> throw new IllegalArgumentException("unsupported solver");
};
}
protected void translate() {
this.result = switch (solver) {
case MARCOGMUSSolver ignore -> translateMARCOGMUS((Set<String>) gmuses, encoding.factIDMap(), encoding.ruleIDMap());
case Sat4JSolver ignore -> translateSAT4JGMUS((List<List<List<Integer>>>) gmuses, encoding.factIDMap(), encoding.ruleIDMap());
default -> throw new IllegalArgumentException("unsupported solver");
};
}
public abstract Set<ExplanationType> translateMARCOGMUS(Set<String> gmuses, BiMap<Integer, Atom> factIDMap, BiMap<Integer, FORule> ruleIDMap);
public abstract Set<ExplanationType> translateSAT4JGMUS(List<List<List<Integer>>> gmuses,BiMap<Integer, Atom> factIDMap, BiMap<Integer, FORule> ruleIDMap);
public abstract GSATEncoder_GRI<DataStructureGRI, Atom> getEncoder();
/**
*
* @param query
* @return a default explanation considering that the query is in the intial factbase
*/
public abstract Set<ExplanationType> getQueryIsInTheIntitialFactbaseExplanation(Atom query) ;
}
package fr.boreal.explanation.api.processors;
import com.google.common.collect.BiMap;
import fr.boreal.explanation.api.encoders.GSATEncoder_GRI;
import fr.boreal.model.logicalElements.api.Atom;
import fr.boreal.model.rule.api.FORule;
import java.util.Iterator;
import java.util.List;
import java.util.Set;
import java.util.function.Predicate;
/**
* Uses the GRI to compute the Explanations of a Query
* Supports different ways to encode the GRI, as well as different types of Explanations, and Query types.
* @param <ExplanationType> the explanation return type
* @param <DataStructureType> to store the GRI
* @param <QueryType> the supported query
*/
public interface ExplanationProcessor_GRI<ExplanationType, DataStructureType, QueryType> {
/**
* @param GRI
* @param query
* @param belongsToInitialFactbase
* @return the set of all explanations of a query given the GRI
*/
Set<ExplanationType> computeAllExplanations(DataStructureType GRI, QueryType query, Predicate<Atom> belongsToInitialFactbase);
/**
* @param GRI
* @param query
* @param belongsToInitialFactbase
* @return an iterator for all explanations of a query given the GRI
*/
default Iterator<ExplanationType> computeExplanations(DataStructureType GRI, QueryType query, Predicate<Atom> belongsToInitialFactbase) {
return this.computeAllExplanations(GRI, query, belongsToInitialFactbase).iterator();
}
public Set<ExplanationType> getQueryIsInTheIntitialFactbaseExplanation(Atom query) ;
public GSATEncoder_GRI<DataStructureType, QueryType> getEncoder();
public abstract Set<ExplanationType> translateMARCOGMUS(Set<String> gmuses, BiMap<Integer, Atom> factIDMap, BiMap<Integer, FORule> ruleIDMap);
public abstract Set<ExplanationType> translateSAT4JGMUS(List<List<List<Integer>>> gmuses, BiMap<Integer, Atom> factIDMap, BiMap<Integer, FORule> ruleIDMap);
}