Package net.sf.tweety.arg.adf.sat

Class NativeLingelingSolver

java.lang.Object

net.sf.tweety.logics.pl.sat.SatSolver

net.sf.tweety.arg.adf.sat.IncrementalSatSolver

net.sf.tweety.arg.adf.sat.NativeLingelingSolver

All Implemented Interfaces:

BeliefSetConsistencyTester<PlFormula>, ConsistencyTester<BeliefSet<PlFormula,?>>, ConsistencyWitnessProvider<PlBeliefSet,PlFormula>

public class NativeLingelingSolver
extends IncrementalSatSolver

Experimental lingeling binding

Author:

Mathias Hofer

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
private static class	NativeLingelingSolver.LingelingSolverState

Field Summary

Fields

Modifier and Type	Field	Description
private static java.lang.String	DEFAULT_LINUX_LIB
private static java.lang.String	DEFAULT_WIN_LIB

Constructor Summary

Constructors

Constructor	Description
NativeLingelingSolver()

Method Summary

Modifier and Type	Method	Description
private static void	add(long lgl, int lit)
private void	addClause(long lgl, int[] clause)
private static void	assume(long lgl, int lit)
private static boolean	changed(long lgl)
SatSolverState	createState()
private static boolean	deref(long lgl, int lit)
private static boolean	failed(long lgl, int lit)
private static boolean	fixed(long lgl, int lit)
private static void	flushCache(long lgl)
private static void	freeze(long lgl, int lit)
private static boolean	frozen(long lgl, int lit)
Interpretation<PlBeliefSet,PlFormula>	getWitness(java.util.Collection<PlFormula> formulas)	If the collection of formulas is consistent this method returns some model of it or, if it is inconsistent, null.
private static boolean	inconsistent(long lgl)
private static long	init()
boolean	isSatisfiable(java.util.Collection<PlFormula> formulas)	Checks whether the given set of formulas is satisfiable.
private static void	melt(long lgl, int lit)
private static void	meltAll(long lgl)
private static void	reduceCache(long lgl)
private static void	release(long lgl)
private static boolean	reusable(long lgl, int lit)
private static void	reuse(long lgl, int lit)
private static boolean	sat(long lgl)
private static boolean	usable(long lgl, int lit)

Methods inherited from class net.sf.tweety.logics.pl.sat.SatSolver

convertToDimacs, convertToDimacs, createTmpDimacsFile, createTmpDimacsFile, getDefaultSolver, getWitness, getWitness, hasDefaultSolver, isConsistent, isConsistent, isConsistent, setDefaultSolver, setTempFolder

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

DEFAULT_WIN_LIB

private static final java.lang.String DEFAULT_WIN_LIB

See Also:

Constant Field Values

DEFAULT_LINUX_LIB

private static final java.lang.String DEFAULT_LINUX_LIB

See Also:

Constant Field Values

Constructor Detail

NativeLingelingSolver

public NativeLingelingSolver()

Method Detail

getWitness

public Interpretation<PlBeliefSet,PlFormula> getWitness(java.util.Collection<PlFormula> formulas)

Description copied from class: SatSolver

If the collection of formulas is consistent this method returns some model of it or, if it is inconsistent, null.

Specified by:

getWitness in interface ConsistencyWitnessProvider<PlBeliefSet,PlFormula>

Specified by:

getWitness in class SatSolver

Parameters:

formulas - a set of formulas

Returns:

some model of the formulas or null.

isSatisfiable

public boolean isSatisfiable(java.util.Collection<PlFormula> formulas)

Description copied from class: SatSolver

Checks whether the given set of formulas is satisfiable.

Specified by:

isSatisfiable in class SatSolver

Parameters:

formulas - a set of formulas.

Returns:

"true" if the set is consistent.

createState

public SatSolverState createState()

Specified by:

createState in class IncrementalSatSolver

addClause

private void addClause(long lgl,
                       int[] clause)

init

private static long init()

release

private static void release(long lgl)

add

private static void add(long lgl,
                        int lit)

assume

private static void assume(long lgl,
                           int lit)

sat

private static boolean sat(long lgl)

deref

private static boolean deref(long lgl,
                             int lit)

fixed

private static boolean fixed(long lgl,
                             int lit)

failed

private static boolean failed(long lgl,
                              int lit)

inconsistent

private static boolean inconsistent(long lgl)

changed

private static boolean changed(long lgl)

reduceCache

private static void reduceCache(long lgl)

flushCache

private static void flushCache(long lgl)

freeze

private static void freeze(long lgl,
                           int lit)

frozen

private static boolean frozen(long lgl,
                              int lit)

melt

private static void melt(long lgl,
                         int lit)

meltAll

private static void meltAll(long lgl)

usable

private static boolean usable(long lgl,
                              int lit)

reusable

private static boolean reusable(long lgl,
                                int lit)

reuse

private static void reuse(long lgl,
                          int lit)