Skip to main content

Ctrl+K

Historical manual preserved at the documentation replacement. Use the current manual for supported behavior.

Primo documentation

Work status

Current implementation and qualification
Active work
Open leads register

Using Primo

Build and run Primo
SMT-LIB input and results
Request a model
Repeated queries and scopes
Command-line options and output

Core architecture

Architecture
Incremental SMT sessions
Finalized model interpretations
Tactic architecture
- Tactic reference
Boolean DAG representation and bounded associative flattening
Root-polarity clausification experiment
SAT backend: IPASIR-UP and CaDiCaL
DPLL(T) integration
Preprocessing
Structural automatic preprocessing selection
Quantifiers: parsing and term representation
Entailment checks and fail masks for quantifier instantiation

Theories

EUF And Congruence Closure
- Boolean Arguments in EUF
- QF_UF disequality propagation heuristics
Arithmetic
Nelson-Oppen theory combination
Wrong answer: congruence is dropped for Bool-sorted function arguments
Difference logic

Evidence and practice

Contributing to Primo: draft
Public repository migration: draft
- Documentation restructuring before public release
- Documentation inventory audit and proposed contents
Experiments
Run Log
- Benchmark records in Git with a generated SQLite index
Failure taxonomy
- Finite-Domain Fuzzing
Docket: TermId-order sensitivity
Maintain the documentation
Qualification snapshot before the manual rewrite

Paper notes

Literature
- Paper summaries
- LRA Related Work
IPASIR-UP: User Propagators for CDCL
Reported QF_LRA results
Yices: architecture, dynamic Ackermannization, and lemma reuse
Clause forgetting: correctness and termination
Polarity-aware CNF in SMT
Don’t-care reasoning and relevance
CVC4 architecture
FastSMT strategy synthesis
Evidence about useful tactic configurations
Fast congruence closure and extensions
Fast Congruence Closure Implementation Note
Exploiting Symmetry In SMT Problems
Using SAT And SMT Solvers For Finite Model Finding With Sorts
Nelson-Oppen Closure Methods
de Moura-Bjorner Model-Based Theory Combination
A Fast Linear-Arithmetic Solver for DPLL(T)
Arithmetic Solving in Z3
- Word-sized GCD: what the literature says
Integer division, modulo, and absolute value
Integer-model repair and MIP primal heuristics
Early LRA atom canonicalization
An Effective SMT Engine for Formal Verification (Griggio’s thesis)
Decision Procedures for Linear Arithmetic (Bromberger’s thesis)
Monotone (one-sided) variable elimination: what to cite
Fast and Flexible Difference Constraint Propagation for DPLL(T)
Revisiting Enumerative Instantiation
Fair and Adventurous Enumeration of Quantifier Instantiations

Reference

Bibliography
LLM2SMT retrospective

Search

Ctrl+K

By Primo contributors