Package org.tweetyproject.arg.adf.sat.state

Class SynchronizedSatSolverState

java.lang.Object

org.tweetyproject.arg.adf.sat.state.SynchronizedSatSolverState

All Implemented Interfaces:

AutoCloseable, SatSolverState

public final class SynchronizedSatSolverState
extends Object
implements SatSolverState

A synchronized wrapper of SatSolverState. May be too restrictive, since it does not know anything about implementation details.

Author:

Mathias

Constructor Summary

Constructors

Constructor	Description
SynchronizedSatSolverState(SatSolverState delegate)

Method Summary

Modifier and Type	Method	Description
boolean	add(Clause clause)	Adds the given clause to the solver state.
void	assume(Literal literal)	Assumes the truth value of the given proposition for the next call to SatSolverState.satisfiable().
void	close()
boolean	satisfiable()	Computes if the current state is satisfiable.
Set<Literal>	witness()	Returns a witness of the satisfiability of all the clauses in the state, or null if the state is unsatisfiable.
Set<Literal>	witness(Collection<? extends Literal> filter)

Methods inherited from class java.lang.Object

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

Constructor Details

SynchronizedSatSolverState

public SynchronizedSatSolverState(SatSolverState delegate)

Parameters:

delegate - delegate

Method Details

satisfiable

public boolean satisfiable()

Description copied from interface: SatSolverState

Computes if the current state is satisfiable. Also takes made assumptions into account.

Note that it is up to the implementation if the current satisfiability status is cached or if it is computed for every call.

Specified by:

satisfiable in interface SatSolverState

Returns:

true if the state is satisfiable, false if it is not

witness

public Set<Literal> witness()

Description copied from interface: SatSolverState

Returns a witness of the satisfiability of all the clauses in the state, or null if the state is unsatisfiable.

Specified by:

witness in interface SatSolverState

Returns:

a witness if the state is sat, else returns null

witness

public Set<Literal> witness(Collection<? extends Literal> filter)

Specified by:

witness in interface SatSolverState

Parameters:

filter - filter

Returns:

Set

assume

public void assume(Literal literal)

Description copied from interface: SatSolverState

Assumes the truth value of the given proposition for the next call to SatSolverState.satisfiable(). There can be multiple assumptions, all of them are gone after the next SatSolverState.satisfiable() call.

Specified by:

assume in interface SatSolverState

Parameters:

literal - the atom for which we assume a value

add

public boolean add(Clause clause)

Description copied from interface: SatSolverState

Adds the given clause to the solver state.

Specified by:

add in interface SatSolverState

Parameters:

clause - a clause containing only literals - no constants!

Returns:

true if the clause could be added to the state, false if it failed

close

public void close()

Specified by:

close in interface AutoCloseable

Specified by:

close in interface SatSolverState