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

Class NativeLingelingSolver.LingelingSolverState

java.lang.Object

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

All Implemented Interfaces:

java.lang.AutoCloseable, SatSolverState

Enclosing class:

NativeLingelingSolver

private static class NativeLingelingSolver.LingelingSolverState
extends java.lang.Object
implements SatSolverState

Field Summary

Fields

Modifier and Type	Field	Description
private long	handle
private int	nextProposition	Keeps track of the int representation of fresh propositions
private java.util.Map<Proposition,java.lang.Integer>	propositionsToNative	Maps the propositions to their native representation.
private java.util.Set<Disjunction>	stateCache	Contains the disjunctions which were added after the last sat call and must be added before the next sat call.

Constructor Summary

Constructors

Modifier	Constructor	Description
private	LingelingSolverState(long handle)

Method Summary

Modifier and Type	Method	Description
boolean	add(java.util.Collection<Disjunction> clauses)
boolean	add(Disjunction clause)	Updates the state of the corresponding SAT-Solver by adding a clause.
void	assume(Proposition proposition, boolean value)
void	close()
private boolean	isTrue(Proposition p)
boolean	remove(Disjunction clause)	Tries to remove the given clause from the sat instance.
boolean	satisfiable()
Interpretation<PlBeliefSet,PlFormula>	witness()

Methods inherited from class java.lang.Object

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

Field Detail

propositionsToNative

private java.util.Map<Proposition,java.lang.Integer> propositionsToNative

Maps the propositions to their native representation.

stateCache

private java.util.Set<Disjunction> stateCache

Contains the disjunctions which were added after the last sat call and must be added before the next sat call.

nextProposition

private int nextProposition

Keeps track of the int representation of fresh propositions

handle

private long handle

Constructor Detail

LingelingSolverState

private LingelingSolverState(long handle)

Method Detail

close

public void close()
           throws java.lang.Exception

Specified by:

close in interface java.lang.AutoCloseable

Throws:

java.lang.Exception

isTrue

private boolean isTrue(Proposition p)

add

public boolean add(java.util.Collection<Disjunction> clauses)

Specified by:

add in interface SatSolverState

add

public boolean add(Disjunction clause)

Description copied from interface: SatSolverState

Updates the state of the corresponding SAT-Solver by adding a clause.

Specified by:

add in interface SatSolverState

Parameters:

clause - a clause containing only literals - no constants!

Returns:

true iff the

remove

public boolean remove(Disjunction clause)

Description copied from interface: SatSolverState

Tries to remove the given clause from the sat instance.

Specified by:

remove in interface SatSolverState

Returns:

true iff the removal was successful

witness

public Interpretation<PlBeliefSet,PlFormula> witness()

Specified by:

witness in interface SatSolverState

satisfiable

public boolean satisfiable()

Specified by:

satisfiable in interface SatSolverState

assume

public void assume(Proposition proposition,
                   boolean value)

Specified by:

assume in interface SatSolverState