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

Class SimpleSatSolverState

java.lang.Object

net.sf.tweety.arg.adf.sat.SimpleSatSolverState

All Implemented Interfaces:

java.lang.AutoCloseable, SatSolverState

public class SimpleSatSolverState
extends java.lang.Object
implements SatSolverState

A dummy state that can be used in combination with non-incremental Sat-Solvers and SimpleIncrementalSatSolver at positions where a SatSolverState is required.

Maintains an internal collection of disjunctions.

Author:

Mathias Hofer

Field Summary

Fields

Modifier and Type	Field	Description
private java.util.Collection<Disjunction>	assume
private SatSolver	solver
private java.util.Collection<PlFormula>	state

Constructor Summary

Constructors

Constructor	Description
SimpleSatSolverState(SatSolver solver)

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()
boolean	remove(Disjunction clause)	Tries to remove the given clause from the sat instance.
Interpretation<PlBeliefSet,PlFormula>	witness()

Methods inherited from class java.lang.Object

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

Methods inherited from interface net.sf.tweety.arg.adf.sat.SatSolverState

satisfiable

Field Detail

solver

private SatSolver solver

state

private java.util.Collection<PlFormula> state

assume

private java.util.Collection<Disjunction> assume

Constructor Detail

SimpleSatSolverState

SimpleSatSolverState(SatSolver solver)

Parameters:

solver -

Method Detail

close

public void close()
           throws java.lang.Exception

Specified by:

close in interface java.lang.AutoCloseable

Throws:

java.lang.Exception

witness

public Interpretation<PlBeliefSet,PlFormula> witness()

Specified by:

witness in interface SatSolverState

assume

public void assume(Proposition proposition,
                   boolean value)

Specified by:

assume 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

add

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

Specified by:

add in interface SatSolverState

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