operations_research::sat::LratProofHandler Member List

This is the complete list of members for operations_research::sat::LratProofHandler, including all inherited members.

AddAndProveInferredClauseByEnumeration(absl::Span< const Literal > new_clause, absl::Span< const ClauseId > ids_for_proof, const CompactVectorVector< int, Literal > &clauses_for_proof)	operations_research::sat::LratProofHandler
AddAssumedClause(ClauseId id, absl::Span< const Literal > clause)	operations_research::sat::LratProofHandler
AddImportedClause(ClauseId id, absl::Span< const Literal > clause)	operations_research::sat::LratProofHandler
AddInferredClause(ClauseId id, absl::Span< const Literal > clause, absl::Span< const ClauseId > unit_ids, bool exported=false)	operations_research::sat::LratProofHandler	inline
AddInferredClause(ClauseId id, absl::Span< const Literal > clause, absl::Span< const ClauseId > unit_ids, absl::Span< const LratChecker::RatIds > rat, bool exported=false)	operations_research::sat::LratProofHandler
AddProblemClause(ClauseId id, absl::Span< const Literal > clause)	operations_research::sat::LratProofHandler
Check()	operations_research::sat::LratProofHandler
Close(bool model_is_unsat)	operations_research::sat::LratProofHandler
DeleteClause(ClauseId id, absl::Span< const Literal > clause)	operations_research::sat::LratProofHandler
drat_check_enabled() const	operations_research::sat::LratProofHandler	inline
drat_output_enabled() const	operations_research::sat::LratProofHandler	inline
EndProblemClauses()	operations_research::sat::LratProofHandler
ExportClause(ClauseId id, absl::Span< const Literal > clause)	operations_research::sat::LratProofHandler
GetLratClauseForDebug(ClauseId id) const	operations_research::sat::LratProofHandler	inline
lrat_check_enabled() const	operations_research::sat::LratProofHandler	inline
lrat_output_enabled() const	operations_research::sat::LratProofHandler	inline
MaybeCreate(Model *model)	operations_research::sat::LratProofHandler	static
MaybeCreate(const SatParameters &params, ClauseIdGenerator *id_generator, SharedLratProofStatus *proof_status, SharedStatistics *stats)	operations_research::sat::LratProofHandler	static
num_assumed_clauses() const	operations_research::sat::LratProofHandler	inline
PinClause(ClauseId id, absl::Span< const Literal > clause)	operations_research::sat::LratProofHandler
UnpinClause(ClauseId id)	operations_research::sat::LratProofHandler
Valid() const	operations_research::sat::LratProofHandler