Add documentation to src/chc/*.rs

Author: coord-e

src/chc/clause_builder.rs

@@ -1,3 +1,11 @@
+//! A builder for [`Clause`]s.
+//!
+//! This module provides [`ClauseBuilder`], a helper for constructing [`Clause`]s. It is
+//! particularly useful for managing the universally quantified variables of a clause. It can
+//! automatically create fresh [`TermVarIdx`] for variables from other domains (e.g.,
+//! [`crate::rty::FunctionParamIdx`]), simplifying the generation of clauses from higher-level
+//! representations.
+
 use std::any::{Any, TypeId};
 use std::collections::HashMap;
 use std::fmt::Debug;
@@ -8,6 +16,7 @@ use rustc_index::IndexVec;
 
 use super::{Atom, Body, Clause, DebugInfo, Sort, TermVarIdx};
 
+/// A convenience trait to represent constraints on variables used in [`ClauseBuilder`] at once.
 pub trait Var: Eq + Ord + Hash + Copy + Debug + 'static {}
 impl<T: Eq + Ord + Hash + Copy + Debug + 'static> Var for T {}
 
@@ -54,6 +63,17 @@ impl Hash for dyn Key {
     }
 }
 
+/// A builder for a [`Clause`].
+///
+/// [`Clause`] contains a list of universally quantified variables, a head atom, and a body formula.
+/// When building the head and body, we usually have some formulas that represents variables using
+/// something other than [`TermVarIdx`] (e.g. [`crate::rty::FunctionParamIdx`] or [`crate::refine::Var`]).
+/// These variables are usually OK to be universally quantified in the clause, so we want to keep
+/// the mapping of them to [`TermVarIdx`] and use it to convert the variables in the formulas
+/// during the construction of the clause.
+///
+/// Also see [`crate::rty::ClauseBuilderExt`], which provides a higher-level API on top of this
+/// to build clauses from [`crate::rty::Refinement`]s.
 #[derive(Clone, Default)]
 pub struct ClauseBuilder {
     vars: IndexVec<TermVarIdx, Sort>,

src/chc/debug.rs

@@ -1,3 +1,10 @@
+//! Attachable debug information for CHC clauses.
+//!
+//! The [`DebugInfo`] struct captures contextual information (like `tracing` spans) at the time
+//! of a clause's creation. This information is then pretty-printed as comments in the
+//! generated SMT-LIB2 file, which helps in tracing a clause back to its origin in the
+//! Thrust codebase.
+
 #[derive(Debug, Clone)]
 pub struct Display<'a> {
     inner: &'a DebugInfo,
@@ -19,6 +26,7 @@ impl<'a> std::fmt::Display for Display<'a> {
     }
 }
 
+/// A purely informational metadata that can be attached to a clause.
 #[derive(Debug, Clone, Default)]
 pub struct DebugInfo {
     contexts: Vec<(String, String)>,

src/chc/format_context.rs

@@ -1,7 +1,22 @@
+//! A context for formatting a CHC system into SMT-LIB2.
+//!
+//! This module provides [`FormatContext`], which is responsible for translating parts of [`chc::System`]
+//! into a representation that is compatible with SMT solvers. It handles tasks like
+//! monomorphization of polymorphic datatypes and applying solver-specific workarounds.
+//! The [`super::smtlib2`] module uses this context to perform the final rendering to the SMT-LIB2 format.
+
 use std::collections::BTreeSet;
 
 use crate::chc::{self, hoice::HoiceDatatypeRenamer};
 
+/// A context for formatting a CHC system.
+///
+/// This subsumes a representational difference between [`chc::System`] and resulting SMT-LIB2.
+/// - Gives a naming convention of symbols to represent built-in datatypes of [`chc::System`] in SMT-LIB2,
+/// - Gives a stringified representation of [`chc::Sort`]s,
+/// - Monomorphizes polymorphic datatypes of [`chc::System`] to be compatible with several CHC solvers,
+/// - Renames datatypes to be compatible with Hoice (see [`HoiceDatatypeRenamer`]),
+/// - etc.
 #[derive(Debug, Clone)]
 pub struct FormatContext {
     renamer: HoiceDatatypeRenamer,

src/chc/hoice.rs

@@ -1,4 +1,5 @@
-/// hopv/hoice#73
+//! A workaround for a bug in the Hoice CHC solver.
+
 use std::collections::{HashMap, HashSet};
 
 use crate::chc;
@@ -53,6 +54,10 @@ impl<'a> SortDatatypes<'a> {
     }
 }
 
+/// Rename to ensure the referring datatype name is lexicographically larger than the referred one.
+///
+/// Workaround for <https://github.com/hopv/hoice/issues/73>. Applied indirectly via
+/// [`crate::chc::format_context::FormatContext`] when formatting [`crate::chc::System`] as SMT-LIB2.
 #[derive(Debug, Clone, Default)]
 pub struct HoiceDatatypeRenamer {
     prefixes: HashMap<chc::DatatypeSymbol, String>,

src/chc/smtlib2.rs

@@ -1,5 +1,14 @@
+//! Wrappers around CHC structures to display them in SMT-LIB2 format.
+//!
+//! The main entry point is the [`System`] wrapper, which takes a [`chc::System`] and provides a
+//! [`std::fmt::Display`] implementation that produces a complete SMT-LIB2.
+//! It uses [`FormatContext`] to handle the complexities of the conversion,
+//! such as naming convention and solver-specific workarounds.
+//! The output of this module is what gets passed to the external CHC solver.
+
 use crate::chc::{self, format_context::FormatContext};
 
+/// A helper struct to display a list of items.
 #[derive(Debug, Clone)]
 struct List<T> {
     open: Option<&'static str>,
@@ -79,6 +88,7 @@ impl<T> List<T> {
     }
 }
 
+/// A wrapper around a [`chc::Term`] that provides a [`std::fmt::Display`] implementation in SMT-LIB2 format.
 #[derive(Debug, Clone)]
 struct Term<'ctx, 'a> {
     ctx: &'ctx FormatContext,
@@ -202,6 +212,7 @@ impl<'ctx, 'a> Term<'ctx, 'a> {
     }
 }
 
+/// A wrapper around a [`chc::Atom`] that provides a [`std::fmt::Display`] implementation in SMT-LIB2 format.
 #[derive(Debug, Clone)]
 pub struct Atom<'ctx, 'a> {
     ctx: &'ctx FormatContext,
@@ -242,6 +253,7 @@ impl<'ctx, 'a> Atom<'ctx, 'a> {
     }
 }
 
+/// A wrapper around a [`chc::Formula`] that provides a [`std::fmt::Display`] implementation in SMT-LIB2 format.
 #[derive(Debug, Clone)]
 pub struct Formula<'ctx, 'a> {
     ctx: &'ctx FormatContext,
@@ -278,6 +290,7 @@ impl<'ctx, 'a> Formula<'ctx, 'a> {
     }
 }
 
+/// A wrapper around a [`chc::Body`] that provides a [`std::fmt::Display`] implementation in SMT-LIB2 format.
 #[derive(Debug, Clone)]
 pub struct Body<'ctx, 'a> {
     ctx: &'ctx FormatContext,
@@ -304,6 +317,7 @@ impl<'ctx, 'a> Body<'ctx, 'a> {
     }
 }
 
+/// A wrapper around a [`chc::Clause`] that provides a [`std::fmt::Display`] implementation in SMT-LIB2 format.
 #[derive(Debug, Clone)]
 pub struct Clause<'ctx, 'a> {
     ctx: &'ctx FormatContext,
@@ -340,6 +354,7 @@ impl<'ctx, 'a> Clause<'ctx, 'a> {
     }
 }
 
+/// A wrapper around a [`chc::DatatypeSelector`] that provides a [`std::fmt::Display`] implementation in SMT-LIB2 format.
 #[derive(Debug, Clone)]
 pub struct DatatypeSelector<'ctx, 'a> {
     ctx: &'ctx FormatContext,
@@ -363,6 +378,7 @@ impl<'ctx, 'a> DatatypeSelector<'ctx, 'a> {
     }
 }
 
+/// A wrapper around a [`chc::DatatypeCtor`] that provides a [`std::fmt::Display`] implementation in SMT-LIB2 format.
 #[derive(Debug, Clone)]
 pub struct DatatypeCtor<'ctx, 'a> {
     ctx: &'ctx FormatContext,
@@ -386,6 +402,7 @@ impl<'ctx, 'a> DatatypeCtor<'ctx, 'a> {
     }
 }
 
+/// A wrapper around a slice of [`chc::Datatype`] that provides a [`std::fmt::Display`] implementation in SMT-LIB2 format.
 #[derive(Debug, Clone)]
 pub struct Datatypes<'ctx, 'a> {
     ctx: &'ctx FormatContext,
@@ -423,6 +440,8 @@ impl<'ctx, 'a> Datatypes<'ctx, 'a> {
     }
 }
 
+/// A wrapper around a [`chc::Datatype`] that provides a [`std::fmt::Display`] implementation for the
+/// discriminant function in SMT-LIB2 format.
 #[derive(Debug, Clone)]
 pub struct DatatypeDiscrFun<'ctx, 'a> {
     ctx: &'ctx FormatContext,
@@ -458,6 +477,8 @@ impl<'ctx, 'a> DatatypeDiscrFun<'ctx, 'a> {
     }
 }
 
+/// A wrapper around a [`chc::Datatype`] that provides a [`std::fmt::Display`] implementation for the
+/// matcher predicate in SMT-LIB2 format.
 #[derive(Debug, Clone)]
 pub struct MatcherPredFun<'ctx, 'a> {
     ctx: &'ctx FormatContext,
@@ -507,6 +528,7 @@ impl<'ctx, 'a> MatcherPredFun<'ctx, 'a> {
     }
 }
 
+/// A wrapper around a [`chc::System`] that provides a [`std::fmt::Display`] implementation in SMT-LIB2 format.
 #[derive(Debug, Clone)]
 pub struct System<'a> {
     ctx: FormatContext,

src/chc/solver.rs

@@ -1,3 +1,10 @@
+//! A generic interface for running external command-line CHC solvers.
+//!
+//! This module provides the [`Config`] struct for configuring and running an external
+//! CHC solver. It supports setting the solver command, arguments, and timeout, and can
+//! be configured through environment variables.
+
+/// An error that can occur when solving a [`crate::chc::System`].
 #[derive(Debug, thiserror::Error)]
 pub enum CheckSatError {
     #[error("unsat")]
@@ -12,6 +19,7 @@ pub enum CheckSatError {
     Io(#[from] std::io::Error),
 }
 
+/// A configuration for running a command-line CHC solver.
 #[derive(Debug, Clone)]
 pub struct CommandConfig {
     pub name: String,
@@ -84,6 +92,13 @@ impl CommandConfig {
     }
 }
 
+/// A configuration for solving a [`crate::chc::System`].
+///
+/// This struct holds the configuration for the solver, including the solver command, its
+/// arguments, and a timeout. It can also be configured to run a preprocessor on the SMT-LIB2
+/// file before passing it to the solver.
+///
+/// The configuration can be loaded from environment variables using [`Config::from_env`].
 #[derive(Debug, Clone)]
 pub struct Config {
     pub solver: CommandConfig,

src/chc/unbox.rs

@@ -1,3 +1,5 @@
+//! An optimization that removes `Box` sorts and terms from a CHC system.
+
 use super::*;
 
 fn unbox_term(term: Term) -> Term {
@@ -118,6 +120,11 @@ fn unbox_datatype(datatype: Datatype) -> Datatype {
     }
 }
 
+/// Remove all `Box` sorts and `Box`/`BoxCurrent` terms from the system.
+///
+/// The box values in Thrust represent an owned pointer, but are logically equivalent to the inner type.
+/// This pass removes them to reduce the complexity of the CHCs sent to the solver.
+/// This function traverses a [`System`] and removes all `Box` related constructs.
 pub fn unbox(system: System) -> System {
     let System {
         clauses,