SeMiTONE

SeMiTONE (Satisfiability Modulo TheOries NEtwork) is a highly modular, Rust-native foundation for building custom Satisfiability Modulo Theories (SMT) and Optimization Modulo Theories (OMT) solvers.

While most SMT projects provide monolithic, black-box solvers, SeMiTONE takes a different approach. It provides the core mathematical engine and backtrackable data structures required to evaluate formulas against background theories, deliberately delegating the "search" phase (e.g., DPLL/CDCL branching loops and resolution heuristics) to external modules.

This makes SeMiTONE the perfect building block for researchers and engineers who need deep integration of logic reasoning into their own architectures without being constrained by a rigid, pre-packaged solver.

🚀 Key Features

• Lazy Lemmatization Framework: Seamlessly delegates theory evaluation to specialized underlying modules, enabling an efficient DPLL(T) architecture.
• Advanced Theory Support:
  • Linear Real Arithmetic (LRA): Fast simplex-based evaluation with native support for infinitesimals, strict/non-strict bounds, Gomory fractional cuts, and Branch & Bound for integer variables.
  • Enumerative Domains (Enum): Arc-consistency propagation for finite domains.
• CDCL-Ready: Automatically performs conflict analysis, generates precise no-goods (theory lemmas), and computes optimal backjump levels (e.g., 1UIP) to aggressively prune the search space.
• Fully Incremental: Features zero-cost context switching (push/pop) and solving under assumptions, ideal for iterative constraint refinement.
• Rust-Native Performance: Zero-allocation pivoting, sparse matrix representations, and robust memory management.

🎯 Ideal Use Cases

SeMiTONE is designed for domains that require tightly coupled, custom logic reasoning, such as:

• Timeline-based Automated Planning: Formulating and solving complex temporal networks and resource constraints.
• Cognitive Architectures: Integrating semantic reasoning and dynamic constraint satisfaction into intelligent agents.
• Custom SMT/OMT Solvers: Building specialized solvers tailored to niche theories or domain-specific heuristics.

🛠️ Quick Look

SeMiTONE exposes a clean, strongly-typed AST to build and assert constraints. A typical interaction is:

1. assert formulas (returns false on trivial, immediate inconsistency),
2. call propagate (returns Ok(()) if feasible, or Err((backtrack_level, no_good)) on conflict),
3. choose a branch with decide (or decide_enum), then call propagate again.

Below is a compact conceptual example:

use semitone::{
  ast::ArithExpr,
  SeMiTONE,
};

let mut solver = SeMiTONE::new();

// Declare variables across different theories
let x = solver.new_real();
let y = solver.new_real();
let state = solver.new_enum(vec![1, 2, 3]);

// Build constraints: (x + y = 10) AND (x > 6)
let eq_expr = (x.clone() + y.clone()).eq(ArithExpr::from(10));
let gt_expr = x.gt(ArithExpr::from(6));

// 1) Assert constraints into the network.
//    `assert` returns false only for immediate/trivial inconsistencies.
let system = eq_expr & gt_expr;
if !solver.assert(&system) {
  println!("Trivial inconsistency detected during assert.");
} else {
  // 2) Propagate current consequences.
  match solver.propagate() {
    Ok(()) => {
      // 3) Make a decision and propagate again.
      // `decide_enum` is a convenience wrapper around a SAT-level decision.
      if solver.decide_enum(&state, 2) {
        match solver.propagate() {
          Ok(()) => println!("Branch is still feasible after the decision."),
          Err((level, no_good)) => {
            println!("Conflict after decide: backtrack to level {}", level);
            println!("No-good: {:?}", no_good);
          }
        }
      } else {
        println!("Decision was immediately inconsistent.");
      }
    }
    Err((level, no_good)) => {
      println!("Conflict during propagation: backtrack to level {}", level);
      println!("No-good: {:?}", no_good);
    }
  }
}

Note: As SeMiTONE delegates search to external modules, you will need to wrap the network in your own decision loop to explore the boolean space and extract a final model.

📄 License

This project is licensed under the MIT License - see the LICENSE file for details.