tiny.smt

Overview · API · Code relationships · Verification · Audit

Overview

The package decides whether a formula over Boolean values, fixed-width bit-vectors, finite arrays and uninterpreted functions can be made true. It pairs a SAT solver that learns new clauses from conflicts (conflict-driven clause learning) with a reader and writer for the standard text language of SMT solvers.

A program that checks machine arithmetic, for example whether a 4-bit addition can overflow or whether a divisor can be zero, asks whether some values of its variables make a formula true. It needs one of three answers: yes with a value for every named variable, no with evidence it can check, or unknown when a limit on conflicts runs out. It asks many questions of one formula that differ only in temporary hypotheses, and after a no it wants to know which hypotheses the no depends on. It exchanges formulas and evidence with other tools as text.

A SAT solver works on Boolean variables and clauses alone, so every bit-vector operation, every array read and write and every function application has to become clauses before the solver sees it. An array whose index has w bits has 2 to the power w cells, so spelling out every cell grows exponentially with the index width. A function with no definition still has to return equal results for equal arguments, and clauses say so only when the encoding adds them. Questions asked of one formula share the solver's clauses, so whatever one question adds stays for the next unless the solver removes it. A no is only as sound as the solver that gave it, so a caller that acts on a no wants evidence that a separate check can confirm without running the solver's search. Evidence describes the formula of one solve, and any later change to the clauses, the variables or the hypotheses makes it describe a formula the solver no longer holds.

MiniSat, by Niklas Eén and Niklas Sörensson, is a conflict-driven clause-learning SAT solver. The package keeps its way of solving: each clause of two or more literals watches two of them, each conflict while at least one decision is in force yields a learned clause, and a solve can run under assumed literals. SMT-LIB is the standard text language of SMT solvers and the catalog of their theories. The package keeps its syntax for sorts, declarations and assertions, and its operator names for Booleans, fixed-size bit-vectors, arrays and uninterpreted functions.

Terms live in one table that owns every term and function declaration it holds (context, Context), and each term is its 32-bit index in that table (Term). The encoder (bitvec.Encoder) turns each bit-vector into one Boolean variable per bit and each operator into the clauses of and, or and exclusive-or gates. The encoder gives an array one cell of element bits for each index value, and it refuses an index wider than eight bits with ArrayIndexTooWide, so an array has at most 256 cells. For every pair of applications of one function, the encoder adds one clause saying that equal arguments force equal results.

A solve under temporary assumptions discards every clause added during it when it completes, the clauses learned under those assumptions included. When no cap on learned clauses is set (max_learned_clauses), the solve keeps the clauses learned before it. After a no under assumptions, the solver reports a set of assumptions that the clauses refute together (Solver.lastUnsatCore), and the set can hold an assumption the no does not need. After each unsatisfiable answer, the solver keeps a trace for that solve's clauses and assumptions: a list of clauses that ends in the empty clause. To check one clause of the trace, a checker assumes its literals false together with the assumptions and propagates unit clauses over the formula and the earlier clauses of the trace. The clause passes when that propagation reaches a conflict (Reverse Unit Propagation). Solver.lastProofArtifact copies the trace together with the clauses and assumptions it rests on (proof artifact), and ProofArtifact.valid checks that copy again without the solver. The trace covers the clauses the encoder produced, so checking it confirms the answer for the Boolean encoding and leaves the translation from terms to clauses to the encoder. Adding a variable, a clause or an assumption, changing assumption frames, or solving again clears the recorded core and trace, so evidence holds only until the next change to the solver.

The package reads and writes SMT-LIB scripts (smtlib), formulas as a plain-text list of clauses written as signed variable numbers, the DIMACS format (dimacs), and proof artifacts in a line format of its own (proof). A caller builds terms in a Context, hands it and a sat.Solver to bitvec.Encoder, asserts and assumes Boolean terms, solves, and then reads a Model after a yes, or the core and the proof artifact after a no. The sat namespace holds the solver (Solver) with its literal, status, statistics, restart and proof types. The choir namespace defines the Boolean, bit-vector and array operators, function application, variables, Boolean and bit-vector constants, and named assertions as the operations and types of a compiler intermediate representation, and the namespace has no operation for the term language's integer constants or its integer operators add, mul, le, lt, ge and gt, and it also has no operation for the term language's distinct, which takes operands of any one sort. The term table Context takes no part, and a caller makes those operations known to a context of the intermediate representation, the ir.Context in the signatures of choir.SmtDialect, a different type, in one of three ways before building them: choir.registerDialect records a loader that the ir.Context runs when it first meets the dialect's name, choir.loadDialect loads them at once, and each type getter of choir.SmtDialect loads them on first use. The root re-exports the types callers name most, so smt.Solver, smt.Literal, smt.Status, smt.Context, smt.Term, smt.Script and smt.Model need no namespace.

The example adds two variables, adds the clauses (a or b) and the negation of a, and solves.

1const smt = @import("smt");23var solver = smt.Solver.init(allocator);4defer solver.deinit();56const a = try solver.addVariable();7const b = try solver.addVariable();8try solver.addClause(&.{9    smt.Literal.positive(a),10    smt.Literal.positive(b),11});12try solver.addClause(&.{smt.Literal.negative(a)});1314const result = try solver.solve();

Definitions

Types and contracts

Public types and contracts.

• Context: One table that owns every term and function declaration it holds.
• ConflictScratch: Scratch memory for one conflict analysis at a time, in storage its caller hands over: a buffer of up to one literal per variable and one mark bit per variable.
• ProofArtifact: The clauses, assumptions and steps behind one unsatisfiable answer, copied out of the solver and owned by the caller.
• Model: The values a satisfying assignment gives: one per named constant, and one entry per encoded application of each uninterpreted function.
• Literal: A variable or its negation, packed into one 32-bit number.
• ModelValue: The value of a constant, a function argument or a function result in a model: a Boolean, a bit-vector or an array, for code that reads one from a Model to print it or compare it with an expected value.
• BoolValue: A truth value that may also be unset.
• Expr: One term: a tag naming its operator and a payload holding its operands.
• Function: A function declaration, named by its index in the declaration table of the Context that holds it.
• FunctionDecl: One declared function: its name, the sorts of its arguments and the sort of its result.
• Script: A logic name and the list of terms asserted over one Context.
• Sort: The sort of a term: Boolean, integer, a bit-vector of a given width, or an array from bit-vectors to bit-vectors.
• Term: A term, named by its index in the table of the Context that built it.
• ProofClause: One starting clause of a ProofArtifact: a clause the checker takes as given.
• ProofStep: One step of a proof trace: a clause that has to follow from the starting clauses, the assumptions and the earlier steps by unit propagation.
• RestartPolicy: The restart schedule: the search goes back to the first decision after a conflict count that starts at first_conflict_interval and multiplies by growth after each restart.
• SolveStats: Counts of the work one solve did.
• Status: The answer of one solve.
• Solver: A SAT solver that learns a clause from each conflict above decision level zero over the clauses a caller adds, answers under assumed literals, and records an unsat core and a proof trace after each unsatisfiable answer.

Namespaces

Public namespaces.

• term: The formulas the package solves are trees of typed expressions over Booleans, integers, bit-vectors and arrays, with named constants and uninterpreted functions, and each expression has a sort.
• sat: A SAT solver that learns a new clause from each conflict it analyzes, with the types a caller builds clauses from and reads answers and evidence through.
• choir: A checker that asks an SMT solver about a program can state its questions as formulas in the same intermediate representation as the program.
• smtlib: Reads SMT-LIB scripts into terms and writes terms back as SMT-LIB text.
• bitvec: Decides formulas over Booleans, fixed-width bit-vectors, arrays and uninterpreted functions by turning them into clauses for a SAT solver, and reads a satisfying assignment back as a value for each constant.
• dimacs: Reads and writes Boolean formulas in conjunctive normal form as plain text.
• proof: A plain-text format for the evidence behind one unsatisfiable answer, with a writer and a reader.

Code relationships

Direct static dependencies extracted from parsed source by semantic graph analysis.

Uses: tiny.accy, tiny.bench, tiny.hypothesis, tiny.simd, tiny.sys
Used by: None

Verification

No verification records are cataloged for this module in this build.

Audit