lib/smt/src/root.zig

daab053ee43316e1809a84551d573ddd1e5bf3d2

  1 //! The package decides whether a formula over Boolean values, fixed-width bit-vectors, finite
  2 //! arrays and uninterpreted functions can be made true. It pairs a SAT solver that learns new
  3 //! clauses from conflicts (conflict-driven clause learning) with a reader and writer for the
  4 //! standard text language of SMT solvers.
  5 //!
  6 //! A program that checks machine arithmetic, for example whether a 4-bit addition can overflow or
  7 //! whether a divisor can be zero, asks whether some values of its variables make a formula true. It
  8 //! needs one of three answers: yes with a value for every named variable, no with evidence it can
  9 //! check, or unknown when a limit on conflicts runs out. It asks many questions of one formula that
 10 //! differ only in temporary hypotheses, and after a no it wants to know which hypotheses the no
 11 //! depends on. It exchanges formulas and evidence with other tools as text.
 12 //!
 13 //! A SAT solver works on Boolean variables and clauses alone, so every bit-vector operation, every
 14 //! array read and write and every function application has to become clauses before the solver sees
 15 //! it. An array whose index has w bits has 2 to the power w cells, so spelling out every cell grows
 16 //! exponentially with the index width. A function with no definition still has to return equal
 17 //! results for equal arguments, and clauses say so only when the encoding adds them. Questions
 18 //! asked of one formula share the solver's clauses, so whatever one question adds stays for the
 19 //! next unless the solver removes it. A no is only as sound as the solver that gave it, so a caller
 20 //! that acts on a no wants evidence that a separate check can confirm without running the solver's
 21 //! search. Evidence describes the formula of one solve, and any later change to the clauses, the
 22 //! variables or the hypotheses makes it describe a formula the solver no longer holds.
 23 //!
 24 //! [MiniSat](https://doi.org/10.1007/978-3-540-24605-3_37), by Niklas Eén and Niklas Sörensson, is
 25 //! a conflict-driven clause-learning SAT solver. The package keeps its way of solving: each clause
 26 //! of two or more literals watches two of them, each conflict while at least one decision is in
 27 //! force yields a learned clause, and a solve can run under assumed literals.
 28 //! [SMT-LIB](https://smt-lib.org/) is the standard text language of SMT solvers and the catalog of
 29 //! their theories. The package keeps its syntax for sorts, declarations and assertions, and its
 30 //! operator names for Booleans, fixed-size bit-vectors, arrays and uninterpreted functions.
 31 //!
 32 //! Terms live in one table that owns every term and function declaration it holds (*context*,
 33 //! `Context`), and each term is its 32-bit index in that table (`Term`). The encoder
 34 //! (`bitvec.Encoder`) turns each bit-vector into one Boolean variable per bit and each operator
 35 //! into the clauses of and, or and exclusive-or gates. The encoder gives an array one cell of
 36 //! element bits for each index value, and it refuses an index wider than eight bits with
 37 //! `ArrayIndexTooWide`, so an array has at most 256 cells. For every pair of applications of one
 38 //! function, the encoder adds one clause saying that equal arguments force equal results.
 39 //!
 40 //! A solve under temporary assumptions discards every clause added during it when it completes, the
 41 //! clauses learned under those assumptions included. When no cap on learned clauses is set
 42 //! (`max_learned_clauses`), the solve keeps the clauses learned before it. After a no under
 43 //! assumptions, the solver reports a set of assumptions that the clauses refute together
 44 //! (`Solver.lastUnsatCore`), and the set can hold an assumption the no does not need. After each
 45 //! unsatisfiable answer, the solver keeps a trace for that solve's clauses and assumptions: a list
 46 //! of clauses that ends in the empty clause. To check one clause of the trace, a checker assumes
 47 //! its literals false together with the assumptions and propagates unit clauses over the formula
 48 //! and the earlier clauses of the trace. The clause passes when that propagation reaches a conflict
 49 //! (Reverse Unit Propagation). `Solver.lastProofArtifact` copies the trace together with the
 50 //! clauses and assumptions it rests on (*proof artifact*), and `ProofArtifact.valid` checks that
 51 //! copy again without the solver. The trace covers the clauses the encoder produced, so checking it
 52 //! confirms the answer for the Boolean encoding and leaves the translation from terms to clauses to
 53 //! the encoder. Adding a variable, a clause or an assumption, changing assumption frames, or
 54 //! solving again clears the recorded core and trace, so evidence holds only until the next change
 55 //! to the solver.
 56 //!
 57 //! The package reads and writes SMT-LIB scripts (`smtlib`), formulas as a plain-text list of
 58 //! clauses written as signed variable numbers, the DIMACS format (`dimacs`), and proof artifacts in
 59 //! a line format of its own (`proof`). A caller builds terms in a `Context`, hands it and a
 60 //! `sat.Solver` to `bitvec.Encoder`, asserts and assumes Boolean terms, solves, and then reads a
 61 //! `Model` after a yes, or the core and the proof artifact after a no. The `sat` namespace holds
 62 //! the solver (`Solver`) with its literal, status, statistics, restart and proof types. The `choir`
 63 //! namespace defines the Boolean, bit-vector and array operators, function application, variables,
 64 //! Boolean and bit-vector constants, and named assertions as the operations and types of a compiler
 65 //! intermediate representation, and the namespace has no operation for the term language's integer
 66 //! constants or its integer operators `add`, `mul`, `le`, `lt`, `ge` and `gt`, and it also has no
 67 //! operation for the term language's `distinct`, which takes operands of any one sort. The term
 68 //! table `Context` takes no part, and a caller makes those operations known to a context of the
 69 //! intermediate representation, the `ir.Context` in the signatures of `choir.SmtDialect`, a
 70 //! different type, in one of three ways before building them: `choir.registerDialect` records a
 71 //! loader that the `ir.Context` runs when it first meets the dialect's name, `choir.loadDialect`
 72 //! loads them at once, and each type getter of `choir.SmtDialect` loads them on first use. The root
 73 //! re-exports the types callers name most, so `smt.Solver`, `smt.Literal`, `smt.Status`,
 74 //! `smt.Context`, `smt.Term`, `smt.Script` and `smt.Model` need no namespace.
 75 //!
 76 //! The example adds two variables, adds the clauses (a or b) and the negation of a, and solves.
 77 //!
 78 //! ```zig
 79 //! const smt = @import("smt");
 80 //!
 81 //! var solver = smt.Solver.init(allocator);
 82 //! defer solver.deinit();
 83 //!
 84 //! const a = try solver.addVariable();
 85 //! const b = try solver.addVariable();
 86 //! try solver.addClause(&.{
 87 //!     smt.Literal.positive(a),
 88 //!     smt.Literal.positive(b),
 89 //! });
 90 //! try solver.addClause(&.{smt.Literal.negative(a)});
 91 //!
 92 //! const result = try solver.solve();
 93 //! ```
 94 
 95 pub const sat = @import("sat/root.zig");
 96 pub const bitvec = @import("bitvec.zig");
 97 pub const dimacs = @import("dimacs.zig");
 98 pub const proof = @import("proof.zig");
 99 pub const choir = @import("choir/root.zig");
100 pub const term = @import("term.zig");
101 pub const smtlib = @import("smtlib/root.zig");
102 
103 pub const Solver = sat.Solver;
104 pub const ConflictScratch = sat.ConflictScratch;
105 pub const Literal = sat.Literal;
106 pub const Status = sat.Status;
107 pub const BoolValue = sat.BoolValue;
108 pub const SolveStats = sat.SolveStats;
109 pub const RestartPolicy = sat.RestartPolicy;
110 pub const ProofClause = sat.ProofClause;
111 pub const ProofStep = sat.ProofStep;
112 pub const ProofArtifact = sat.ProofArtifact;
113 
114 pub const Context = term.Context;
115 pub const Sort = term.Sort;
116 pub const Term = term.Term;
117 pub const Function = term.Function;
118 pub const FunctionDecl = term.FunctionDecl;
119 pub const Expr = term.Expr;
120 pub const Script = term.Script;
121 pub const Model = bitvec.Model;
122 pub const ModelValue = bitvec.ModelValue;