Definition at line 619 of file clause.h.
|
| | BinaryImplicationGraph (Model *model) |
| | BinaryImplicationGraph (const BinaryImplicationGraph &)=delete |
| BinaryImplicationGraph & | operator= (const BinaryImplicationGraph &)=delete |
| | ~BinaryImplicationGraph () override |
| bool | Propagate (Trail *trail) final |
| absl::Span< const Literal > | Reason (const Trail &trail, int trail_index, int64_t conflict_id) const final |
| void | Reimply (Trail *trail, int old_trail_index) final |
| void | Resize (int num_variables) |
| int64_t | literal_size () const |
| bool | IsEmpty () const final |
| bool | AddBinaryClause (ClauseId id, Literal a, Literal b, bool delete_non_representative_id=true) |
| bool | AddBinaryClause (Literal a, Literal b) |
| bool | AddImplication (Literal a, Literal b) |
| ClauseId | GetClauseId (Literal a, Literal b) const |
| void | EnableSharing (bool enable) |
| void | SetAdditionCallback (std::function< void(Literal, Literal)> f) |
| ABSL_MUST_USE_RESULT bool | AddAtMostOne (absl::Span< const Literal > at_most_one) |
| void | MinimizeConflictFirst (const Trail &trail, std::vector< Literal > *c, SparseBitset< BooleanVariable > *marked, std::vector< ClauseId > *clause_ids, bool also_use_decisions) |
| void | AppendImplicationChains (absl::Span< const Literal > literals, std::vector< ClauseId > *clause_ids) |
| void | RemoveFixedVariables () |
| bool | DetectEquivalences (bool log_info=false) |
| bool | IsDag () const |
| const std::vector< LiteralIndex > & | ReverseTopologicalOrder () const |
| absl::Span< const Literal > | Implications (Literal l) const |
| Literal | RepresentativeOf (Literal l) const |
| bool | ComputeTransitiveReduction (bool log_info=false) |
| bool | TransformIntoMaxCliques (std::vector< std::vector< Literal > > *at_most_ones, int64_t max_num_explored_nodes=1e8) |
| bool | MergeAtMostOnes (absl::Span< std::vector< Literal > > at_most_ones, int64_t max_num_explored_nodes=1e8, double *dtime=nullptr) |
| const std::vector< std::vector< Literal > > & | GenerateAtMostOnesWithLargeWeight (absl::Span< const Literal > literals, absl::Span< const double > lp_values, absl::Span< const double > reduced_costs) |
| std::vector< absl::Span< const Literal > > | HeuristicAmoPartition (std::vector< Literal > *literals) |
| int64_t | num_propagations () const |
| int64_t | num_inspections () const |
| int64_t | num_minimization () const |
| int64_t | num_literals_removed () const |
| bool | IsRedundant (Literal l) const |
| int64_t | num_redundant_literals () const |
| int64_t | num_current_equivalences () const |
| int64_t | num_redundant_implications () const |
| int64_t | ComputeNumImplicationsForLog () const |
| template<typename Output> |
| void | ExtractAllBinaryClauses (Output *out) const |
| bool | AddBinaryClauseAndChangeReason (ClauseId id, Literal a, Literal b) |
| const std::vector< Literal > & | DirectImplications (Literal literal) |
| LiteralIndex | RandomImpliedLiteral (Literal lhs) |
| int | DirectImplicationsEstimatedSize (Literal literal) const |
| bool | FindFailedLiteralAroundVar (BooleanVariable var, bool *is_unsat) |
| int64_t | NumImplicationOnVariableRemoval (BooleanVariable var) |
| void | RemoveBooleanVariable (BooleanVariable var, std::deque< std::vector< Literal > > *postsolve_clauses) |
| bool | IsRemoved (Literal l) const |
| void | RemoveAllRedundantVariables (std::deque< std::vector< Literal > > *postsolve_clauses) |
| void | CleanupAllRemovedAndFixedVariables () |
| void | ResetWorkDone () |
| int64_t | WorkDone () const |
| absl::Span< const Literal > | GetAllImpliedLiterals (Literal root) |
| bool | LiteralIsImplied (Literal l) const |
| void | ClearImpliedLiterals () |
| template<bool use_weight = true> |
| std::vector< Literal > | ExpandAtMostOneWithWeight (absl::Span< const Literal > at_most_one, const util_intops::StrongVector< LiteralIndex, bool > &can_be_included, const util_intops::StrongVector< LiteralIndex, double > &expanded_lp_values) |
| void | ResetAtMostOneIterator () |
| absl::Span< const Literal > | NextAtMostOne () |
| bool | RemoveDuplicatesAndFixedVariables () |
| bool | HasNoDuplicates () |
| absl::Span< const int > | AtMostOneIndices (Literal lit) const |
| bool | FixLiteral (Literal true_literal, absl::Span< const ClauseId > clause_ids={}) |
| | SatPropagator (const std::string &name) |
| | SatPropagator (const SatPropagator &)=delete |
| SatPropagator & | operator= (const SatPropagator &)=delete |
| virtual | ~SatPropagator ()=default |
| void | SetPropagatorId (int id) |
| int | PropagatorId () const |
| virtual void | Untrail (const Trail &, int trail_index) |
| bool | PropagatePreconditionsAreSatisfied (const Trail &trail) const |
| bool | PropagationIsDone (const Trail &trail) const |
| const std::string & | name () const |
1.15.0