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 class	NativeLingelingSolver.LingelingSolverState

Field Summary

Fields

Modifier and Type	Field	Description
private static java.io.File	DEFAULT_WIN_LIB

Constructor Summary

Constructors

Constructor	Description
NativeLingelingSolver()

Method Summary

Modifier and Type	Method	Description
private void	add(long lgl, int lit)
private void	addClause(long lgl, int[] clause)
private void	assume(long lgl, int lit)
private boolean	changed(long lgl)
SatSolverState	createState()
private boolean	deref(long lgl, int lit)
private boolean	failed(long lgl, int lit)
private boolean	fixed(long lgl, int lit)
private void	flushCache(long lgl)
private void	freeze(long lgl, int lit)
private 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.
Interpretation<PlBeliefSet,PlFormula>	getWitness(SatSolverState state)
private boolean	inconsistent(long lgl)
private long	init()
boolean	isSatisfiable(java.util.Collection<PlFormula> formulas)	Checks whether the given set of formulas is satisfiable.
boolean	isSatisfiable(SatSolverState state)
private void	melt(long lgl, int lit)
private void	meltAll(long lgl)
private void	reduceCache(long lgl)
private void	release(long lgl)
private boolean	reusable(long lgl, int lit)
private void	reuse(long lgl, int lit)
private boolean	sat(long lgl)
private 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.io.File DEFAULT_WIN_LIB

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

isSatisfiable

public boolean isSatisfiable(SatSolverState state)

Specified by:

isSatisfiable in class IncrementalSatSolver

getWitness

public Interpretation<PlBeliefSet,PlFormula> getWitness(SatSolverState state)

Specified by:

getWitness in class IncrementalSatSolver

addClause

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

init

private long init()

release

private void release(long lgl)

add

private void add(long lgl,
                 int lit)

assume

private void assume(long lgl,
                    int lit)

sat

private boolean sat(long lgl)

deref

private boolean deref(long lgl,
                      int lit)

fixed

private boolean fixed(long lgl,
                      int lit)

failed

private boolean failed(long lgl,
                       int lit)

inconsistent

private boolean inconsistent(long lgl)

changed

private boolean changed(long lgl)

reduceCache

private void reduceCache(long lgl)

flushCache

private void flushCache(long lgl)

freeze

private void freeze(long lgl,
                    int lit)

frozen

private boolean frozen(long lgl,
                       int lit)

melt

private void melt(long lgl,
                  int lit)

meltAll

private void meltAll(long lgl)

usable

private boolean usable(long lgl,
                       int lit)

reusable

private boolean reusable(long lgl,
                         int lit)

reuse

private void reuse(long lgl,
                   int lit)