Bipolar

org-tweetyproject-arg-adf/src/main/java/org/tweetyproject/arg/adf/reasoner/AbstractADFReasoner.java

@@ -0,0 +1,97 @@
+/*
+ *  This file is part of "TweetyProject", a collection of Java libraries for
+ *  logical aspects of artificial intelligence and knowledge representation.
+ *
+ *  TweetyProject is free software: you can redistribute it and/or modify
+ *  it under the terms of the GNU Lesser General Public License version 3 as
+ *  published by the Free Software Foundation.
+ *
+ *  This program is distributed in the hope that it will be useful,
+ *  but WITHOUT ANY WARRANTY; without even the implied warranty of
+ *  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ *  GNU Lesser General Public License for more details.
+ *
+ *  You should have received a copy of the GNU Lesser General Public License
+ *  along with this program. If not, see <http://www.gnu.org/licenses/>.
+ *
+ *  Copyright 2026 The TweetyProject Team <http://tweetyproject.org/contact/>
+ */
+package org.tweetyproject.arg.adf.reasoner;
+
+import org.tweetyproject.arg.adf.semantics.interpretation.Interpretation;
+import org.tweetyproject.arg.adf.syntax.Argument;
+import org.tweetyproject.arg.adf.syntax.adf.AbstractDialecticalFramework;
+import org.tweetyproject.arg.dung.semantics.Extension;
+import org.tweetyproject.arg.dung.syntax.DungTheory;
+import org.tweetyproject.commons.InferenceMode;
+import org.tweetyproject.commons.ModelProvider;
+import org.tweetyproject.commons.QualitativeReasoner;
+
+import java.util.Collection;
+import java.util.HashSet;
+
+/**
+ * Abstract class for reasoners of ADF semantics
+ *
+ * @author Lars Bengel
+ */
+public abstract class AbstractADFReasoner implements QualitativeReasoner<AbstractDialecticalFramework, Argument>, ModelProvider<Argument,AbstractDialecticalFramework,Interpretation> {
+    @Override
+    public Boolean query(AbstractDialecticalFramework bbase, Argument formula) {
+        return this.query(bbase, formula, InferenceMode.SKEPTICAL);
+    }
+
+    /**
+     * Determine the set of acceptable arguments wrt. the given inference mode
+     * @param bbase some ADF
+     * @param inferenceMode the inference mode
+     * @return the set of acceptable arguments
+     */
+    public Collection<Argument> queryAll(AbstractDialecticalFramework bbase, InferenceMode inferenceMode) {
+        Collection<Argument> result = new HashSet<>();
+        Collection<Interpretation> models = this.getModels(bbase);
+        if(inferenceMode.equals(InferenceMode.CREDULOUS)) {
+            for (Interpretation model : models)
+                result.addAll(model.satisfied());
+        } else {
+            result.addAll(bbase);
+            for(Interpretation model: models)
+                result.retainAll(model.satisfied());
+        }
+        return result;
+    }
+
+    /**
+     * Queries the given ADF for the given argument using the given
+     * inference type.
+     * @param beliefbase an ADF
+     * @param formula a single argument
+     * @param inferenceMode either InferenceMode.SKEPTICAL or InferenceMode.CREDULOUS
+     * @return "true" if the argument is accepted
+     */
+    public Boolean query(AbstractDialecticalFramework beliefbase, Argument formula, InferenceMode inferenceMode) {
+        Collection<Interpretation> models = this.getModels(beliefbase);
+        if(inferenceMode.equals(InferenceMode.SKEPTICAL)){
+            for(Interpretation m: models)
+                if(!m.satisfies(formula))
+                    return false;
+            return true;
+        }
+        // so its credulous semantics
+        for(Interpretation m: models){
+            if(m.satisfies(formula))
+                return true;
+        }
+        return false;
+    }
+
+    @Override
+    public boolean isInstalled() {
+        return true;
+    }
+
+    @Override
+    public Interpretation getModel(AbstractDialecticalFramework bbase) {
+        return getModels(bbase).iterator().next();
+    }
+}

org-tweetyproject-arg-adf/src/main/java/org/tweetyproject/arg/adf/reasoner/AbstractDialecticalFrameworkReasoner.java

@@ -37,7 +37,7 @@
  * @deprecated use {@link AbstractDialecticalFramework#query()} instead
  */
 @Deprecated( forRemoval = true, since = "1.19" )
-public abstract class AbstractDialecticalFrameworkReasoner {
+public abstract class AbstractDialecticalFrameworkReasoner extends AbstractADFReasoner {
 
 	private final IncrementalSatSolver solver;
 

org-tweetyproject-arg-adf/src/main/java/org/tweetyproject/arg/adf/reasoner/sat/execution/ParallelExecution.java

@@ -47,6 +47,7 @@
 import org.tweetyproject.arg.adf.sat.SatSolverState;
 import org.tweetyproject.arg.adf.semantics.interpretation.Interpretation;
 import org.tweetyproject.arg.adf.syntax.Argument;
+import org.tweetyproject.arg.adf.syntax.adf.AbstractDialecticalFramework;
 
 /**
  * ParallelExecution class
@@ -414,6 +415,21 @@ public Set<Argument> undecided() {
 		public Set<Argument> arguments() {
 			return Set.of();
 		}
+
+		@Override
+		public boolean satisfies(Argument formula) throws IllegalArgumentException {
+			return false;
+		}
+
+		@Override
+		public boolean satisfies(Collection<Argument> formulas) throws IllegalArgumentException {
+			return false;
+		}
+
+		@Override
+		public boolean satisfies(AbstractDialecticalFramework beliefBase) throws IllegalArgumentException {
+			return false;
+		}
 	}
 
 }

org-tweetyproject-arg-adf/src/main/java/org/tweetyproject/arg/adf/sat/solver/NativeMinisatSolver.java

@@ -41,19 +41,46 @@ public final class NativeMinisatSolver implements IncrementalSatSolver {
 
 	private static final String DEFAULT_WIN_LIB = "/minisat.dll";
 	private static final String DEFAULT_LINUX_LIB = "/minisat.so";
+	private static volatile boolean loaded = false;
+
 /**
  * NativeMinisatSolver
  */
 	public NativeMinisatSolver() {
+		loadLibrary();
+	}
+
+	private static synchronized void loadLibrary() {
+		if (loaded) return;
 		String osName = System.getProperty("os.name").toLowerCase();
 		String lib = null;
 		if (osName.contains("win")) {
 			lib = DEFAULT_WIN_LIB;
 		} else if (osName.contains("nux")) {
 			lib = DEFAULT_LINUX_LIB;
 		}
-		String path = getClass().getResource(lib).getPath();
-		System.load(path);
+		if (lib == null) {
+			throw new UnsatisfiedLinkError("Unsupported OS: " + osName);
+		}
+		try {
+			java.net.URL resource = NativeMinisatSolver.class.getResource(lib);
+			String path = resource.getPath();
+			if (path.contains("!")) {
+				// Library is bundled inside a JAR — extract to a temp file first
+				String suffix = lib.substring(lib.lastIndexOf('.'));
+				java.io.File tempFile = java.io.File.createTempFile("minisat", suffix);
+				tempFile.deleteOnExit();
+				try (java.io.InputStream is = NativeMinisatSolver.class.getResourceAsStream(lib)) {
+					java.nio.file.Files.copy(is, tempFile.toPath(), java.nio.file.StandardCopyOption.REPLACE_EXISTING);
+				}
+				System.load(tempFile.getAbsolutePath());
+			} else {
+				System.load(path);
+			}
+			loaded = true;
+		} catch (java.io.IOException e) {
+			throw new RuntimeException("Failed to extract native minisat library", e);
+		}
 	}
 
 	/*

org-tweetyproject-arg-adf/src/main/java/org/tweetyproject/arg/adf/semantics/interpretation/Interpretation.java

@@ -46,7 +46,7 @@
  * @author Mathias Hofer
  *
  */
-public interface Interpretation {
+public interface Interpretation extends org.tweetyproject.commons.Interpretation<AbstractDialecticalFramework, Argument> {
 /**
  *
  * @param adf adf

org-tweetyproject-arg-adf/src/main/java/org/tweetyproject/arg/adf/semantics/interpretation/Interpretations.java

@@ -18,22 +18,20 @@
  */
 package org.tweetyproject.arg.adf.semantics.interpretation;
 
-import java.util.Collections;
-import java.util.Iterator;
-import java.util.Objects;
-import java.util.Set;
+import java.util.*;
 
 import org.tweetyproject.arg.adf.syntax.Argument;
 import org.tweetyproject.arg.adf.syntax.adf.AbstractDialecticalFramework;
 import org.tweetyproject.arg.adf.util.UnionSetView;
+import org.tweetyproject.commons.AbstractInterpretation;
 
 /**
  * @author Mathias Hofer
  *
  */
 final class Interpretations {
 
-	static final class EmptyInterpretation implements Interpretation {
+	static final class EmptyInterpretation extends AbstractInterpretation<AbstractDialecticalFramework,Argument> implements Interpretation {
 
 		private final Set<Argument> undecided;
 
@@ -128,6 +126,16 @@ public String toString() {
 			builder.append("}");
 			return builder.toString();
 		}
+
+		@Override
+		public boolean satisfies(Argument formula) throws IllegalArgumentException {
+			return false;
+		}
+
+		@Override
+		public boolean satisfies(AbstractDialecticalFramework beliefBase) throws IllegalArgumentException {
+			throw new IllegalArgumentException("Satisfaction of belief bases by ADF interpretations is undefined.");
+		}
 	}
 
 	/**
@@ -138,7 +146,7 @@ public String toString() {
 	 * @author Mathias Hofer
 	 *
 	 */
-	static final class SetInterpretation implements Interpretation {
+	static final class SetInterpretation extends AbstractInterpretation<AbstractDialecticalFramework,Argument> implements Interpretation {
 
 		private final Set<Argument> satisfied;
 
@@ -235,9 +243,19 @@ public String toString() {
 			s.append("}");
 			return s.toString();
 		}
+
+		@Override
+		public boolean satisfies(Argument formula) throws IllegalArgumentException {
+			return satisfied().contains(formula);
+		}
+
+		@Override
+		public boolean satisfies(AbstractDialecticalFramework beliefBase) throws IllegalArgumentException {
+			throw new IllegalArgumentException("Satisfaction of belief bases by ADF interpretations is undefined.");
+		}
 	}
 
-	static final class SingleSatisfiedInterpretation implements Interpretation {
+	static final class SingleSatisfiedInterpretation extends AbstractInterpretation<AbstractDialecticalFramework,Argument> implements Interpretation {
 
 		private final Argument argument;
 
@@ -306,9 +324,19 @@ public boolean equals(Object obj) {
 		public String toString() {
 			return new StringBuilder("{t(").append("argument").append(")}").toString();
 		}
+
+		@Override
+		public boolean satisfies(Argument formula) throws IllegalArgumentException {
+			return satisfied().contains(formula);
+		}
+
+		@Override
+		public boolean satisfies(AbstractDialecticalFramework beliefBase) throws IllegalArgumentException {
+			throw new IllegalArgumentException("Satisfaction of belief bases by ADF interpretations is undefined.");
+		}
 	}
 
-	static final class SingleUnsatisfiedInterpretation implements Interpretation {
+	static final class SingleUnsatisfiedInterpretation extends AbstractInterpretation<AbstractDialecticalFramework,Argument> implements Interpretation {
 
 		private final Argument argument;
 
@@ -377,9 +405,19 @@ public boolean equals(Object obj) {
 		public String toString() {
 			return new StringBuilder("{f(").append("argument").append(")}").toString();
 		}
+
+		@Override
+		public boolean satisfies(Argument formula) throws IllegalArgumentException {
+			return satisfied().contains(formula);
+		}
+
+		@Override
+		public boolean satisfies(AbstractDialecticalFramework beliefBase) throws IllegalArgumentException {
+			throw new IllegalArgumentException("Satisfaction of belief bases by ADF interpretations is undefined.");
+		}
 	}
 
-	static final class SingleUndecidedInterpretation implements Interpretation {
+	static final class SingleUndecidedInterpretation extends AbstractInterpretation<AbstractDialecticalFramework,Argument> implements Interpretation {
 
 		private final Argument argument;
 
@@ -448,6 +486,16 @@ public boolean equals(Object obj) {
 		public String toString() {
 			return new StringBuilder("{u(").append("argument").append(")}").toString();
 		}
+
+		@Override
+		public boolean satisfies(Argument formula) throws IllegalArgumentException {
+			return satisfied().contains(formula);
+		}
+
+		@Override
+		public boolean satisfies(AbstractDialecticalFramework beliefBase) throws IllegalArgumentException {
+			throw new IllegalArgumentException("Satisfaction of belief bases by ADF interpretations is undefined.");
+		}
 	}
 
 }

org-tweetyproject-arg-adf/src/main/java/org/tweetyproject/arg/adf/semantics/interpretation/TwoValuedInterpretationIterator.java

@@ -29,6 +29,8 @@
 import java.util.Set;
 
 import org.tweetyproject.arg.adf.syntax.Argument;
+import org.tweetyproject.arg.adf.syntax.adf.AbstractDialecticalFramework;
+import org.tweetyproject.commons.AbstractInterpretation;
 
 /**
  * TwoValuedInterpretationIterator class
@@ -74,7 +76,7 @@ public Interpretation next() {
 		return new TwoValuedInterpretation(arguments, value++);
 	}
 
-	private static final class TwoValuedInterpretation implements Interpretation {
+	private static final class TwoValuedInterpretation extends AbstractInterpretation<AbstractDialecticalFramework,Argument> implements Interpretation {
 
 		private final Map<Argument, Integer> indexMap;
 
@@ -148,6 +150,15 @@ public Set<Argument> arguments() {
 			return indexMap.keySet();
 		}
 
+		@Override
+		public boolean satisfies(Argument formula) throws IllegalArgumentException {
+			return satisfied().contains(formula);
+		}
+
+		@Override
+		public boolean satisfies(AbstractDialecticalFramework beliefBase) throws IllegalArgumentException {
+			throw new IllegalArgumentException("Satisfaction of belief bases by ADF interpretations is undefined.");
+		}
 	}
 
 }