Uses of Interface
org.tweetyproject.arg.adf.syntax.pl.Clause

Packages that use Clause

Package	Description
org.tweetyproject.arg.adf.reasoner.sat.encodings
org.tweetyproject.arg.adf.reasoner.sat.processor
org.tweetyproject.arg.adf.sat
org.tweetyproject.arg.adf.sat.state
org.tweetyproject.arg.adf.syntax.pl
org.tweetyproject.arg.adf.transform

Uses of Clause in org.tweetyproject.arg.adf.reasoner.sat.encodings

Method parameters in org.tweetyproject.arg.adf.reasoner.sat.encodings with type arguments of type Clause

Modifier and Type	Method	Description
void	BipolarSatEncoding.encode(Consumer<Clause> consumer)	Encodes the bipolar Abstract Dialectical Framework (ADF) into a set of SAT clauses.
void	ConflictFreeInterpretationSatEncoding.encode(Consumer<Clause> consumer)	Encodes the conflict-free interpretation of the given ADF into a set of SAT clauses.
void	ConflictFreeInterpretationSatEncoding.encode(Consumer<Clause> consumer, Interpretation interpretation)	Encodes the conflict-free interpretation of the given ADF into a set of SAT clauses based on the provided interpretation.
void	FixPartialSatEncoding.encode(Consumer<Clause> consumer, Interpretation interpretation)
void	KBipolarSatEncoding.encode(Consumer<Clause> consumer)	Encodes the acceptance conditions of the arguments in the ADF into a SAT formula using a given consumer.
void	LargerInterpretationSatEncoding.encode(Consumer<Clause> consumer, Interpretation interpretation)
void	RefineLargerSatEncoding.encode(Consumer<Clause> consumer, Interpretation interpretation)
void	RefineUnequalSatEncoding.encode(Consumer<Clause> consumer, Interpretation interpretation)	Encodes the given interpretation into a set of SAT clauses that represent the refinement of the interpretation, ensuring that the resulting interpretation is not equal to the input interpretation.
void	RelativeSatEncoding.encode(Consumer<Clause> consumer, Interpretation interpretation)
void	RestrictedBipolarSatEncoding.encode(Consumer<Clause> consumer)	Encodes the restricted bipolar Abstract Dialectical Framework (ADF) into a set of SAT clauses based on the given partial interpretation.
void	RestrictedKBipolarSatEncoding.encode(Consumer<Clause> consumer)	Encodes the bipolar Abstract Dialectical Framework (ADF) into a set of SAT clauses.
void	SatEncoding.encode(Consumer<Clause> consumer)	Encodes the structure into a set of SAT clauses and provides them to the given consumer.
void	TwoValuedModelSatEncoding.encode(Consumer<Clause> consumer)	Encodes the two-valued model of the ADF into a set of SAT clauses and provides them to the given consumer.
void	TwoValuedModelSatEncoding.encode(Consumer<Clause> consumer, Interpretation interpretation)	Encodes a specific two-valued interpretation of the ADF into a set of SAT clauses and provides them to the given consumer.

Uses of Clause in org.tweetyproject.arg.adf.reasoner.sat.processor

Method parameters in org.tweetyproject.arg.adf.reasoner.sat.processor with type arguments of type Clause

Modifier and Type	Method	Description
void	KBipolarStateProcessor.process(Consumer<Clause> consumer)	Processes the state of the ADF and encodes the relationships into logical clauses.
void	RestrictedKBipolarStateProcessor.process(Consumer<Clause> consumer)	Processes the SAT encodings for the restricted bipolar or k-bipolar frameworks.
void	StateProcessor.process(Consumer<Clause> consumer)	Processes the current set of states and translates them into Clause objects.

Uses of Clause in org.tweetyproject.arg.adf.sat

Methods in org.tweetyproject.arg.adf.sat with parameters of type Clause

Modifier and Type	Method	Description
boolean	SatSolverState.add(Clause clause)	Adds the given clause to the solver state.

Uses of Clause in org.tweetyproject.arg.adf.sat.state

Methods in org.tweetyproject.arg.adf.sat.state with parameters of type Clause

Modifier and Type	Method	Description
boolean	AsynchronousCloseSatSolverState.add(Clause clause)
boolean	SynchronizedSatSolverState.add(Clause clause)

Uses of Clause in org.tweetyproject.arg.adf.syntax.pl

Methods in org.tweetyproject.arg.adf.syntax.pl that return Clause

Modifier and Type	Method	Description
static Clause	Clause.of()	Creates a clause with no literals.
static Clause	Clause.of(Collection<? extends Literal> literals)	Creates a clause from a collection of literals.
static Clause	Clause.of(Collection<? extends Literal> literals, Literal l)	Creates a clause from a collection of literals and an additional literal.
static Clause	Clause.of(Collection<? extends Literal> literals, Literal l1, Literal l2)	Creates a clause from a collection of literals and two additional literals.
static Clause	Clause.of(Collection<? extends Literal> literals, Literal l1, Literal l2, Literal l3)	Creates a clause from a collection of literals and three additional literals.
static Clause	Clause.of(Clause c, Literal l)	Creates a clause by extending an existing clause with an additional literal.
static Clause	Clause.of(Literal l)	Creates a clause with a single literal.
static Clause	Clause.of(Literal l1, Literal l2)	Creates a clause with two literals.
static Clause	Clause.of(Literal l1, Literal l2, Literal l3)	Creates a clause with three literals.

Methods in org.tweetyproject.arg.adf.syntax.pl with parameters of type Clause

Modifier and Type	Method	Description
static Clause	Clause.of(Clause c, Literal l)	Creates a clause by extending an existing clause with an additional literal.

Uses of Clause in org.tweetyproject.arg.adf.transform

Methods in org.tweetyproject.arg.adf.transform that return types with arguments of type Clause

Modifier and Type	Method	Description
Pair<Literal,Collection<Clause>>	TseitinTransformer.transform(AcceptanceCondition acc)

Method parameters in org.tweetyproject.arg.adf.transform with type arguments of type Clause

Modifier and Type	Method	Description
Literal	TseitinTransformer.collect(AcceptanceCondition acc, Consumer<Clause> clauses)