Module AltErgoLib.Th_util

type answer = (Explanation.t * AltErgoLib.Expr.Set.t list) option
type theory =
  1. | Th_arith
  2. | Th_sum
  3. | Th_adt
  4. | Th_arrays
  5. | Th_bitv
  6. | Th_UF
val pp_theory : Ppx_deriving_runtime.Format.formatter -> theory -> Ppx_deriving_runtime.unit
val show_theory : theory -> Ppx_deriving_runtime.string
type lit_origin =
  1. | Subst
    (*

    Only equalities can be Subst literals, and they are oriented: the left-hand side is always an uninterpreted term or AC symbol application. Effectively, Subst literals are the substitutions generated by calls to X.solve and propagated through the CC(X) and AC(X) algorithms.

    In practice, a Subst equality r = rr is generated when the corresponding substitution is performed by CC(X), i.e. when rr becomes the class representative for r.

    *)
  2. | CS of theory * Numbers.Q.t
    (*

    Literals of CS origin come from the case splits performed by a specific theory. Usually, they are equalities of the shape x = v where x is an uninterpreted term and v a value; however, this is not necessarily the case (e.g. CS literals from the theory of arrays are often disequalities).

    Depending on the theory, the shape of CS literals can be restricted. In particular, CS literals of the Th_UF theory: those come from model generation in the union-find, and are assignments, i.e. equalities x = v where x is uninterpreted and v is a value.

    The rational argument estimates the size of the split -- usually, the number of possible values the theory could choose for this specific uninterpreted term.

    *)
  3. | NCS of theory * Numbers.Q.t
    (*

    Literals of NCS origin are created from a literal of CS origin when the choice made in a case split turns out to be unsatisfiable. The literal is a negation of a CS literal that was built by the corresponding theory, with the restrictions that this implies.

    *)
  4. | Other
    (*

    Literals of Other are those that are not covered by any of the cases described above. In particular, user assertions, SAT decisions, SAT propagations and theory propagations all have the Other origin.

    *)

Indicates where asserted literals come from.

Note that literals are deduplicated before being propagated to the relations. Subst literals are preserved, but other kinds of literals may be subsumed.

type case_split = Shostak.Combine.r Xliteral.view * bool * lit_origin

A case split is a triple (a, is_cs, origin).

The literal a is simply the literal that is the source of the split, or its negation (depending on origin).

The origin should be either CS or NCS. Case splits returned by relations have an origin of CS, which is then flipped to NCS if a contradiction is found involving a.

The is_cs flag should *always* be true, unless the literal a is a *unit fact*, i.e. a fact that is true in all possible environments, not merely the current one. Note that it is acceptable for unit facts to be returned with is_cs = true; but if the is_cs flag is false, the solver *will* assume that the literal can't take part in any conflict. Returning is_cs = false if the literal is not an unit fact **is unsound**.

TL;DR: When in doubt, just set is_cs to true.

type optimized_split = {
  1. value : Objective.Value.t;
  2. case_split : case_split;
    (*

    The underlying case-split. Notice that the value propagate by this case-split doesn't always agree with the objective value value. Indeed, value isn't always a proper model value when the problem is unbounded or some objective functions involved strict inequalities.

    *)
}
type 'literal acts = {
  1. acts_add_decision_lit : 'literal -> unit;
    (*

    Ask the SAT solver to decide on the given formula before it can answer SAT. The order of decisions among multiple calls of acts_add_decision_lit is unspecified.

    Decisions added using acts_add_decision_lit are forgotten when backtracking.

    *)
  2. acts_add_split : 'literal -> unit;
    (*

    Let the SAT solver know about a case split. The SAT solver should decide on the provided formula before answering Sat, although it is not required to do so. The order of decisions among multiple calls of acts_add_split is unspecified, and the solver is allowed to drop some of them.

    Splits added using acts_add_split are forgotten when backtracking.

    *)
  3. acts_add_objective : Objective.Function.t -> Objective.Value.t -> 'literal -> unit;
    (*

    Ask the SAT solver to optimistically select the appropriate value for the given objective function (encoded as a decision in the 'literal). If the solver backtracks on that decision, the theory will have an opportunity to select another value in a context where the 'literal is negated.

    In case multiple objectives are added before the solver gets to make a decision, only the *last* objective is taken into consideration; you cannot assume that the objective has been optimized until the objective is sent back to the theory through add_objective.

    Objectives added using acts_add_objective are forgotten when backtracking.

    *)
}

The type of actions that a theory can take.

Inspired by mSAT's equivalent type 1.

1 : https://github.com/Gbury/mSAT/blob/ \ 1496a48bc8b948e4d5a2bc20edaec33a6901c8fa/src/core/Solver_intf.ml#L104