package hu.bme.mit.inf.dslreasoner.logic.model.builder
import hu.bme.mit.inf.dslreasoner.logic.model.logiclanguage.Type
import hu.bme.mit.inf.dslreasoner.logic.model.logicproblem.LogicProblem
import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.LogicResult
import hu.bme.mit.inf.dslreasoner.logic.model.logicresult.ModelResult
import hu.bme.mit.inf.dslreasoner.workspace.ReasonerWorkspace
import java.math.BigDecimal
import java.util.HashMap
import java.util.LinkedList
import java.util.List
import java.util.Map
import java.util.SortedSet
import java.util.TreeSet
abstract class LogicReasoner {
def abstract LogicResult solve(LogicProblem problem, LogicSolverConfiguration configuration,
ReasonerWorkspace workspace) throws LogicReasonerException
def abstract List extends LogicModelInterpretation> getInterpretations(ModelResult modelResult)
}
public class LogicReasonerException extends Exception {
new(String message, Exception cause) {
super(message, cause)
}
new(Exception cause) {
super("The reasoner has failed", cause)
}
new(String message) {
super(message)
}
}
abstract class SolverConfiguration {
public static val Unlimited = -1;
public static val String UndefinedPath = null
/** The URI string to the independent solver application */
public String solverPath = UndefinedPath
/** Max runtime limit in seconds. */
public int runtimeLimit = Unlimited
/** Max memory limit in megabytes. */
public int memoryLimit = Unlimited
/** Documentation level of the solver. */
public DocumentationLevel documentationLevel = DocumentationLevel::NONE
/** Progress monitor for the solver to
*
(optionally) report progress via {@link progressMonitor.worked}
* (optionally) inform about cancellation request via {@link progressMonitor.isCancelled}
* or via a listener registered by {@link progressMonitor.addCancelListener}
*/
public SolverProgressMonitor progressMonitor = new NullSolverProgressMonitor
}
abstract class LogicSolverConfiguration extends SolverConfiguration {
public var TypeScopes typeScopes = new TypeScopes;
public var SolutionScope solutionScope = new SolutionScope
}
/**
* Describes the amount of debug information required to write to the workspace.
*
*/
public enum DocumentationLevel {
/**
* The solver writes only temporary files.
*/
NONE,
/**
* The solver is requested to write important artifacts and documents that are constructed during the generation.
* This option should not affect the performance of the solver seriously.
*/
NORMAL,
/**
* The solver is requested create additional documents to aid troubleshooting.
* The documents can constructed at the cost of performance.
*/
FULL
}
/**
* Defines the the size of the generated models. Constant Unlimited
defines no upper limit to the type.
*/
public class TypeScopes {
public static val Unlimited = Integer.MAX_VALUE;
/**
* Sets the Integers that are already in the scope of the problem.
*/
public var SortedSet knownIntegers = new TreeSet
/**
* Sets the number of Integers that has to be used to solve the problem.
*/
public var minNewIntegers = 0
public var maxNewIntegers = Unlimited
public var SortedSet knownReals = new TreeSet
/**
* Sets the number of Reals that has to be used to solve the problem.
*/
public var minNewReals = 0
public var maxNewReals = Unlimited
public var SortedSet knownStrings = new TreeSet
/**
* Sets the number of Strings that has to be used to solve the problem.
*/
public var minNewStrings = 0
public var maxNewStrings = Unlimited
/**
* Defines the minimal number of newly added elements. Default value is 0.
*/
public var minNewElements = 0
/**
* Defines the maximal number of newly added elements. Default value is TypeScopes.Unlimited
.
*/
public var maxNewElements = Unlimited
/**
*
*/
public var Map minNewElementsByType = new HashMap
/**
*
*/
public var Map maxNewElementsByType = new HashMap
/**
* Checks if the scope contains negative elements
*/
def public validateTypeScopes(TypeScopes scopes) {
val res = new LinkedList
if(scopes.maxNewElements < 0) {
res += '''Inconsistent scope: Maximal number of new elements is negative.'''
}
if(scopes.maxNewIntegers < 0) {
res += '''Inconsistent scope: Maximal number of new integer values is negative.'''
}
if(scopes.maxNewReals < 0) {
res += '''Inconsistent scope: Maximal number of new real values is negative.'''
}
if(scopes.maxNewStrings < 0) {
res += '''Inconsistent scope: Maximal number of new string values is negative.'''
}
for(x : scopes.minNewElementsByType.entrySet) {
if(x.value < 0) {
res += '''Inconsistent scope: Maximal number of new "«x.key.name»" elements is negative.'''
}
}
return res
}
}
/**
* Defines the required number of solutions for the problem.
* Constant All
defines that all solution for the problem is requested.
*/
public class SolutionScope {
public static val All = Integer.MAX_VALUE;
public var numberOfRequiredSolutions = 1
}
/** Progress monitor class for a solver to
* (optionally) report progress via {@link worked}
* (optionally) inform about cancellation request via {@link isCancelled}
* or via a listener registered by {@link addCancelListener}
*/
public abstract class SolverProgressMonitor {
protected var volatile cancelled = false
protected var progress = 0.0
/**
* Method to report progress, e.g. finishing translation or founding one of the model.
* The sum of all {@link amount} should be 1.0, which is reached when all model is generated.
* By default,
* forward transformation should take 0.1 work unit (implemented in {@link#workedForwardTransformation}),
* founding all solution 0.8 (implemented in {@link#workedModelFound})
* and backward transformation 0.1 again (implemented in {@link#workedBackwardTransformation}).
*/
def public void worked(double amount) {
progress+=amount
processWorked(amount)
}
def public void workedForwardTransformation() {worked(0.1)}
def public void workedModelFound(int numberOfRequestedModels) {
if(numberOfRequestedModels > 0) {
worked(0.8/numberOfRequestedModels)
}
}
def public void workedSearchFinished() { worked(0.1+0.8-progress) }
def public void workedBackwardTransformation(int numberOfFoundModels) {worked(0.1/numberOfFoundModels)}
def public void workedBackwardTransformationFinished() { worked(1.0-progress) }
protected def void processWorked(double amount)
/**
* Requesting the solver to stop with the solutions already found.
* It is not guaranteed however that the solver finishes.
*/
def public void cancel() {
cancelled = true
}
def public boolean isCancelled() {
cancelled
}
}
public class NullSolverProgressMonitor extends SolverProgressMonitor {
override protected processWorked(double amount) { }
}