yaspar_ir/lib.rs
1// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
2// SPDX-License-Identifier: Apache-2.0
3
4//! Yaspar-IR: typed representations of SMTLib scripts with checked building APIs.
5//!
6//! This crate provides parsing, type-checking, and programmatic construction of SMTLib-2.7
7//! scripts. It is fully compliant with the SMTLib standard, supporting quantifiers, datatypes
8//! (including polymorphic and mutually recursive declarations), and all standard logics.
9//!
10//! # Architecture
11//!
12//! The crate is organized around a two-level AST design:
13//!
14//! - **Untyped ASTs** ([`untyped`]) — faithful parsing results that preserve source location
15//! information for error reporting. These may be semantically malformed.
16//! - **Typed ASTs** ([`ast`]) — hashconsed, well-formed representations managed by a memory
17//! [`Arena`](ast::Arena). Hashconsing ensures that structurally identical sub-terms share a
18//! single allocation, making `clone()`, `==`, and `hash()` O(1) operations.
19//!
20//! # Typical workflow
21//!
22//! ```rust
23//! use yaspar_ir::ast::{Context, Typecheck};
24//! use yaspar_ir::untyped::UntypedAst;
25//!
26//! // 1. Parse
27//! let commands = UntypedAst.parse_script_str("(set-logic QF_LIA) (declare-const x Int)").unwrap();
28//! // 2. Type-check into a context
29//! let mut context = Context::new();
30//! let typed_commands = commands.type_check(&mut context).unwrap();
31//! // 3. Analyze or transform the typed terms
32//! ```
33//!
34//! # Building terms programmatically
35//!
36//! Typed ASTs can also be built without parsing, using either:
37//!
38//! - **Unchecked APIs** — low-level allocator methods on [`Context`](ast::Context) (e.g.
39//! `context.app(...)`, `context.forall(...)`). These are efficient but require the caller to
40//! maintain well-formedness invariants manually.
41//! - **Checked APIs** — the [`CheckedApi`](ast::CheckedApi) and
42//! [`ScopedSortApi`](ast::ScopedSortApi) traits, which validate scope, sort compatibility,
43//! and arity automatically via the `TC<T>` monad (`Result<T, String>`).
44//!
45//! See the [`ast`] module and the README for a comprehensive guide to the checked APIs.
46//!
47//! # Feature flags
48//!
49//! - `cnf` — enables NNF/CNF conversion (see `ast::cnf` module).
50//! - `implicant-generation` — enables implicant computation (see `ast::implicant` module).
51//! - `cache` — enables caching infrastructure for CNF and other algorithms.
52//! - `cvc5` — enables translation to cvc5 (see [`cvc5`] module and the [`ConvertToCvc5`](cvc5::ConvertToCvc5) trait).
53//!
54//! # Modules
55//!
56//! | Module | Description |
57//! |---|---|
58//! | [`ast`] | Typed AST types, the [`Context`](ast::Context), checked/unchecked building APIs, and term transformations |
59//! | [`untyped`] | Untyped ASTs with location information, and the parser entry point [`UntypedAst`](untyped::UntypedAst) |
60//! | [`traits`] | Core abstraction traits ([`Contains`](traits::Contains), [`Repr`](traits::Repr), [`AllocatableString`](traits::AllocatableString)) |
61//! | [`statics`] | Static constants (sort name strings, regex patterns) |
62//! | [`cvc5`] | Translation to cvc5-rs objects (`Sort`, `Term`, `Command`). Requires the `cvc5` feature. |
63
64mod allocator;
65pub mod ast;
66#[cfg(feature = "cvc5")]
67pub mod cvc5;
68mod locenv;
69mod macros;
70mod meta;
71mod raw;
72pub mod statics;
73pub mod traits;
74pub mod untyped;