SatSolver Member List

This is the complete list of members for SatSolver, including all inherited members.

AddBinaryClause(Literal a, Literal b)	SatSolver
AddBinaryClauses(const std::vector< BinaryClause > &clauses)	SatSolver
AddClauseDuringSearch(absl::Span< const Literal > literals)	SatSolver
AddLastPropagator(SatPropagator *propagator)	SatSolver
AddLinearConstraint(bool use_lower_bound, Coefficient lower_bound, bool use_upper_bound, Coefficient upper_bound, std::vector< LiteralWithCoeff > *cst)	SatSolver
AddProblemClause(absl::Span< const Literal > literals, bool is_safe=true)	SatSolver
AddPropagator(SatPropagator *propagator)	SatSolver
AddTernaryClause(Literal a, Literal b, Literal c)	SatSolver
AddUnitClause(Literal true_literal)	SatSolver
AdvanceDeterministicTime(TimeLimit *limit)	SatSolver	inline
AllPreferences() const	SatSolver	inline
Assignment() const	SatSolver	inline
AssumptionLevel() const	SatSolver	inline
ASSUMPTIONS_UNSAT enum value	SatSolver
Backtrack(int target_level)	SatSolver
ClearNewlyAddedBinaryClauses()	SatSolver
CurrentDecisionLevel() const	SatSolver	inline
Decisions() const	SatSolver	inline
deterministic_time() const	SatSolver
EnqueueDecisionAndBackjumpOnConflict(Literal true_literal)	SatSolver
EnqueueDecisionAndBacktrackOnConflict(Literal true_literal, int *first_propagation_index=nullptr)	SatSolver
EnqueueDecisionIfNotConflicting(Literal true_literal)	SatSolver
ExtractClauses(Output *out)	SatSolver	inline
FEASIBLE enum value	SatSolver
FinishPropagation()	SatSolver
GetLastIncompatibleDecisions()	SatSolver
INFEASIBLE enum value	SatSolver
IsModelUnsat() const	SatSolver	inline
LIMIT_REACHED enum value	SatSolver
LiteralTrail() const	SatSolver	inline
MinimizeSomeClauses(int decisions_budget)	SatSolver
model()	SatSolver	inline
ModelIsUnsat() const	SatSolver	inline
NewBooleanVariable()	SatSolver	inline
NewlyAddedBinaryClauses()	SatSolver
NotifyThatModelIsUnsat()	SatSolver	inline
num_branches() const	SatSolver
num_failures() const	SatSolver
num_propagations() const	SatSolver
num_restarts() const	SatSolver
NumFixedVariables() const	SatSolver	inline
NumVariables() const	SatSolver	inline
parameters() const	SatSolver
ProblemIsPureSat() const	SatSolver	inline
ProcessNewlyFixedVariables()	SatSolver
Propagate()	SatSolver
ReapplyAssumptionsIfNeeded()	SatSolver
ResetAndSolveWithGivenAssumptions(const std::vector< Literal > &assumptions)	SatSolver
ResetDecisionHeuristic()	SatSolver	inline
ResetDecisionHeuristicAndSetAllPreferences(const std::vector< std::pair< Literal, double >> &prefs)	SatSolver	inline
ResetToLevelZero()	SatSolver
ResetWithGivenAssumptions(const std::vector< Literal > &assumptions)	SatSolver
RestoreSolverToAssumptionLevel()	SatSolver
SatSolver()	SatSolver
SatSolver(Model *model)	SatSolver	explicit
SaveDebugAssignment()	SatSolver
SetAssignmentPreference(Literal literal, double weight)	SatSolver	inline
SetAssumptionLevel(int assumption_level)	SatSolver
SetDratProofHandler(DratProofHandler *drat_proof_handler)	SatSolver	inline
SetNumVariables(int num_variables)	SatSolver
SetParameters(const SatParameters &parameters)	SatSolver
SetShareBinaryClauseCallback(const std::function< void(Literal, Literal)> &shared_binary_clauses_callback)	SatSolver	inline
Solve()	SatSolver
SolveWithTimeLimit(TimeLimit *time_limit)	SatSolver
Status enum name	SatSolver
TakePropagatorOwnership(std::unique_ptr< SatPropagator > propagator)	SatSolver	inline
TrackBinaryClauses(bool value)	SatSolver	inline
UnsatStatus() const	SatSolver	inline
~SatSolver()	SatSolver