tiny.smt.sat.types

1pub const types = @import("types.zig");

1//! The values a caller hands to the solver and reads back from it: literals, answers, truth values2//! that may be unset, counts of a solve's work, and the restart schedule.3//!4//! A caller writes clauses as literals over variables numbered from 0, reads one of three answers5//! after each solve, and reads the value of each variable after a satisfiable answer. Clause files6//! in the common text format number variables from 1 and write a negated variable as a negative7//! number (DIMACS), so a caller reading or writing them converts each literal.8//!9//! The solver keeps one list per literal, so a literal has to map to a small number that can index10//! an array. A literal packs its variable and its sign into one 32-bit number (`Literal.raw`):11//! twice the variable index, plus one for a negated literal. That number indexes the solver's12//! per-literal lists directly, and negating a literal flips its lowest bit. `Literal.fromDimacs`13//! and `Literal.toDimacs` convert between that number and the signed numbers of the text format. A14//! truth value has a third state, unset (`BoolValue.unset`), for an unassigned variable.15/// The answer of one solve. A caller switches on it to decide whether to read a satisfying16/// assignment, an unsat core and a proof, or neither.17pub const Status = enum {18    /// Some assignment makes every clause and every assumption of the solve true. `Solver.value`19    /// and `Solver.literalValue` read that assignment until the next solve.20    sat,21    /// No assignment makes every clause and every assumption of the solve true. The solver then22    /// holds a proof trace that ends in the empty clause, and after a solve under assumptions an23    /// unsat core.24    unsat,25    /// The solve ran out of its conflict limit (`Solver.conflict_budget`) before it reached an26    /// answer, or while core minimization certified a smaller core. After the second case the core27    /// is empty, but the proof trace still holds a refutation under every assumption of the solve.28    unknown,29};3031/// A truth value that may also be unset. A caller switches on the value `Solver.literalValue`32/// returns to read a literal in a satisfying assignment.33pub const BoolValue = enum {34    /// The variable is unassigned, or the literal names a variable at or above the solver's35    /// variable count.36    unset,37    /// The literal or variable is false.38    false,39    /// The literal or variable is true.40    true,4142    /// Returns `.true` for true and `.false` for false. The solver and the proof checker record an43    /// assigned value through it.44    pub fn fromBool(value: bool) BoolValue {45        return if (value) .true else .false;46    }4748    /// Returns the opposite value, and `.unset` for `.unset`. The solver and the proof checker read49    /// a negated literal's value from its variable's value through it.50    pub fn invert(self: BoolValue) BoolValue {51        return switch (self) {52            .unset => .unset,53            .false => .true,54            .true => .false,55        };56    }57};5859/// Counts of the work one solve did. A caller reads them from `Solver.lastSolveStats` to report how60/// much work a solve took. The solver sets every count to zero when a solve starts. The counts61/// cover the main search: the extra solves of core minimization change only `proof_steps`, which62/// takes the certified trace's length.63pub const SolveStats = struct {64    /// Decisions the search made, each giving an unassigned variable a value.65    decisions: usize = 0,66    /// Decisions that gave the variable the value it last held, in this solve or an earlier one,67    /// counted within `decisions`.68    phase_saved_decisions: usize = 0,69    /// Literals the search assigned because every other literal of a clause was false. Unit clauses70    /// of the formula and assumptions sit outside the count.71    propagations: usize = 0,72    /// Times the main search found a clause with every literal false. `Solver.conflict_budget`73    /// limits this count.74    conflicts: usize = 0,75    /// Clauses the search learned from conflicts in this solve.76    learned_clauses: usize = 0,77    /// Learned clauses the solver removed to stay within `Solver.max_learned_clauses`, removals at78    /// the start of the solve included.79    evicted_clauses: usize = 0,80    /// Steps in the proof trace at the end of the solve: one per learned clause, plus the final81    /// empty clause after an unsatisfiable answer. After core minimization certified a smaller82    /// core, the count is the certifying solve's step count.83    proof_steps: usize = 0,84    /// Times the search went back to the first decision, on the restart schedule or to remove85    /// learned clauses.86    restarts: usize = 0,87    /// The largest number of decisions in force at once during the solve.88    max_decision_level: u32 = 0,89    /// Conflicts found at decision level zero, counted within `conflicts`. Assumptions sit below90    /// every decision, so a conflict among the assumptions counts here.91    root_conflicts: usize = 0,92};9394/// The restart schedule: the search goes back to the first decision after a conflict count that95/// starts at `first_conflict_interval` and multiplies by `growth` after each restart. A caller96/// passes one to `Solver.setRestartPolicy` to change the schedule, for example to restart after97/// every conflict. The default restarts after 128 conflicts, then after 256 more, then 512,98/// doubling each time. The solver keeps its learned clauses across a restart. The count starts over99/// at each solve, and a restart happens only while a decision is in force.100pub const RestartPolicy = struct {101    /// Conflicts before the first restart of each solve, 128 by default. Zero turns restarts off.102    first_conflict_interval: usize = 128,103    /// The factor the interval grows by after each restart, 2 by default. A factor of 0 or 1 keeps104    /// the interval fixed, and the interval stops growing at the largest `usize`.105    growth: usize = 2,106107    /// Returns a policy that turns restarts off: an interval of 0 and a growth of 1. A caller that108    /// turns restarts off passes it to `Solver.setRestartPolicy`.109    pub fn disabled() RestartPolicy {110        return .{ .first_conflict_interval = 0, .growth = 1 };111    }112};113114/// A variable or its negation, packed into one 32-bit number. A caller builds every clause and115/// every assumption from literals. Variables are numbered from 0 in the order `Solver.addVariable`116/// returns them.117pub const Literal = struct {118    /// The packed number: twice the variable index, plus one for a negated literal. Two literals119    /// are equal when their `raw` values are equal, and callers compare literals that way.120    raw: u32,121122    /// Returns the literal of variable `variable_index`, unnegated when `polarity` is true and123    /// negated when it is false. Code that picks the sign at run time calls it. An index of124    /// 2147483648 or more overflows the packed number, which panics in safe builds.125    pub fn init(variable_index: u32, polarity: bool) Literal {126        return .{ .raw = variable_index * 2 + if (polarity) @as(u32, 0) else @as(u32, 1) };127    }128129    /// Returns the unnegated literal of variable `variable_index`. A caller writes a clause whose130    /// signs it knows in its source.131    pub fn positive(variable_index: u32) Literal {132        return init(variable_index, true);133    }134135    /// Returns the negated literal of variable `variable_index`. A caller writes a clause whose136    /// signs it knows in its source.137    pub fn negative(variable_index: u32) Literal {138        return init(variable_index, false);139    }140141    /// Returns the variable index of the literal. A caller finds which variable a literal names,142    /// for example to check it against a variable count.143    pub fn variable(self: Literal) u32 {144        return self.raw >> 1;145    }146147    /// Returns true for an unnegated literal. A caller reads a literal's sign to evaluate it under148    /// an assignment.149    pub fn isPositive(self: Literal) bool {150        return self.raw & 1 == 0;151    }152153    /// Returns the literal of the same variable with the opposite sign. An encoder calls it to154    /// state the negation of a condition.155    pub fn negated(self: Literal) Literal {156        return .{ .raw = self.raw ^ 1 };157    }158159    /// Returns the packed number as a `usize`. The solver indexes its per-literal lists of watching160    /// clauses by it, two entries per variable.161    pub fn index(self: Literal) usize {162        return @intCast(self.raw);163    }164165    /// Returns the literal a DIMACS number stands for: variable `|value| - 1`, negated when `value`166    /// is negative. The DIMACS and proof readers call it on each number of a clause. The call167    /// returns `error.InvalidDimacsLiteral` for 0, the number that ends a clause in that format.168    /// The value -2147483648 makes it panic, because its negation does not fit in 32 bits.169    pub fn fromDimacs(value: i32) !Literal {170        if (value == 0) return error.InvalidDimacsLiteral;171        const magnitude: u32 = @intCast(if (value < 0) -value else value);172        return init(magnitude - 1, value > 0);173    }174175    /// Returns the DIMACS number of the literal: the variable index plus one, negative for a176    /// negated literal. The DIMACS and proof writers call it on each literal they print. Variable177    /// index 2147483647 makes it panic, because its number does not fit in `i32`.178    pub fn toDimacs(self: Literal) i32 {179        const one_based: i32 = @intCast(self.variable() + 1);180        return if (self.isPositive()) one_based else -one_based;181    }182};