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

Class AsynchronousCloseSatSolverState

java.lang.Object
org.tweetyproject.arg.adf.sat.state.AsynchronousCloseSatSolverState
All Implemented Interfaces:
AutoCloseable, SatSolverState
public class AsynchronousCloseSatSolverState extends Object implements SatSolverState
Wrapper that closes a SAT solver state asynchronously via a provided executor.
Author:
Mathias Hofer

  • Constructor Details

    • AsynchronousCloseSatSolverState

      public AsynchronousCloseSatSolverState(SatSolverState delegate, Executor executor)
      Creates a new asynchronously closing SAT solver state.
      Parameters:
      delegate - the wrapped SAT solver state
      executor - the executor used to close the wrapped state asynchronously

  • 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)
      Description copied from interface: SatSolverState
      Returns a witness restricted to the given filter. Only literals contained in the filter are included in the returned set.
      Specified by:
      witness in interface SatSolverState
      Parameters:
      filter - the literals to keep in the witness
      Returns:
      a witness restricted to the given filter

    • 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