Crate oxiz_theories 

OxiZ Theory Solvers

This crate provides theory solvers for the CDCL(T) framework:

• EUF (Equality with Uninterpreted Functions) using E-graphs
• LRA/LIA (Linear Real/Integer Arithmetic) using Simplex
• BV (BitVectors) using bit-blasting and word-level propagation
• Arrays (Extensional Arrays) using read-over-write axioms
• FP (Floating-Point) IEEE 754 using bit-blasting
• Datatypes (Algebraic Data Types) for lists, trees, enums
• Strings (Word Equations + Regular Expressions) using Brzozowski derivatives
• Sets (Set Theory) with union, intersection, membership, cardinality, and powerset
• Difference Logic (DL) for constraints x - y ≤ c using Bellman-Ford
• UTVPI (Unit Two-Variable Per Inequality) for constraints ±x ± y ≤ c
• Pseudo-Boolean (PB) for cardinality and weighted constraints
• Special Relations for partial/total orders, transitive closure
• Nelson-Oppen theory combination

Architecture

Each theory solver implements the Theory trait which provides:

• assert_literal: Process a new assignment
• propagate: Perform theory propagation
• check: Check consistency and produce conflicts
• explain: Generate explanations for propagated literals
• backtrack: Handle backtracking

Examples

Theory Combination

use oxiz_theories::{TheoryCombiner, CombinationConfig};
use oxiz_theories::euf::EufSolver;
use oxiz_theories::arithmetic::LraSolver;

// Create a combiner with EUF and LRA
let config = CombinationConfig::default();
let combiner = TheoryCombiner::new(config);

User Propagator

use oxiz_theories::user_propagator::{UserPropagator, PropagatorCallback};

struct MyPropagator;

impl PropagatorCallback for MyPropagator {
    fn on_push(&mut self) {}
    fn on_pop(&mut self, _num_scopes: u32) {}
    fn on_fixed(&mut self, _term: TermId, _value: bool) -> Vec<TermId> {
        vec![]
    }
}

Re-exports

pub use combination::Purifier;

pub use combination::SharedVar;

pub use combination::TheoryCombiner;

pub use config::BranchingHeuristic;

pub use config::BvConfig;

pub use config::CombinationConfig;

pub use config::CombinationMode;

pub use config::LiaConfig;

pub use config::PivotingRule;

pub use config::SimplexConfig;

pub use config::TheoryConfig;

pub use datatype::Constructor;

pub use datatype::DatatypeDecl;

pub use datatype::DatatypeSolver;

pub use datatype::DatatypeSort;

pub use datatype::Field;

pub use datatype::Selector;

pub use error::ConflictInfo;

pub use error::ResourceLimit;

pub use error::SolverStats;

pub use error::TheoryError;

pub use error::TheoryResult;

pub use fp::FpFormat;

pub use fp::FpRoundingMode;

pub use fp::FpSolver;

pub use fp::FpValue;

pub use hashcons::HashConsTable;

pub use hashcons::HcTerm;

pub use propagation::Propagation;

pub use propagation::PropagationPriority;

pub use propagation::PropagationQueue;

pub use propagation::PropagationStats;

pub use simplify::SimplifyContext;

pub use simplify::SimplifyResult;

pub use simplify::SimplifyStats;

pub use string::Regex;

pub use string::RegexOp;

pub use string::StringSolver;

pub use watched::WatchList;

pub use watched::WatchStats;

pub use watched::WatchedConstraint;

pub use array_eager_expand::EagerArrayExpander;

pub use array_eager_expand::EagerExpandConfig;

pub use array_eager_expand::EagerExpandStats;

pub use array_eager_expand::ExpandedArray;

pub use fp_interval_prop::FpInterval;

pub use fp_interval_prop::FpIntervalPropagator;

pub use fp_interval_prop::FpIntervalStats;

pub use fp_interval_prop::RoundingMode as FpIntervalRoundingMode;

pub use string_length_prop::LengthConstraint;

pub use string_length_prop::LengthDomain;

pub use string_length_prop::LengthPropStats;

pub use string_length_prop::LengthPropagator;

pub use quantifier::InstantiationLemma;

pub use quantifier::QuantifierConfig;

pub use quantifier::QuantifierSolver;

pub use quantifier::QuantifierStats;

pub use quantifier::TrackedQuantifier;

pub use quantifier_code_tree::CodeTree;

pub use quantifier_code_tree::CodeTreeInstr;

pub use quantifier_code_tree::CodeTreeStats;

pub use quantifier_code_tree::CompiledPattern;

pub use quantifier_code_tree::Match;

pub use quantifier_code_tree::PatternVar;

pub use recfun::CaseDef;

pub use recfun::RecFunConfig;

pub use recfun::RecFunDef;

pub use recfun::RecFunId;

pub use recfun::RecFunSolver;

pub use recfun::RecFunStats;

pub use user_propagator::Consequence;

pub use user_propagator::PropagatorContext;

pub use user_propagator::PropagatorResult;

pub use user_propagator::UserPropagator;

pub use user_propagator::UserPropagatorManager;

pub use user_propagator::UserPropagatorStats;

pub use special_relations::RelationDef;

pub use special_relations::RelationEdge;

pub use special_relations::RelationKind;

pub use special_relations::RelationProperties;

pub use special_relations::SpecialRelationSolver;

pub use special_relations::SpecialRelationStats;

pub use pb::PbConfig;

pub use pb::PbConstraint;

pub use pb::PbConstraintKind;

pub use pb::PbSolver;

pub use pb::PbStats;

pub use pb::WeightedLiteral;

pub use diff_logic::BellmanFord;

pub use diff_logic::ConstraintGraph;

pub use diff_logic::DenseDiffLogic;

pub use diff_logic::DiffConstraint;

pub use diff_logic::DiffEdge;

pub use diff_logic::DiffLogicConfig;

pub use diff_logic::DiffLogicResult;

pub use diff_logic::DiffLogicSolver;

pub use diff_logic::DiffLogicStats;

pub use diff_logic::DiffVar;

pub use diff_logic::NegativeCycle;

pub use utvpi::DetectedConstraint;

pub use utvpi::DoubledGraph;

pub use utvpi::DoubledNode;

pub use utvpi::Sign;

pub use utvpi::UtConstraint;

pub use utvpi::UtConstraintKind;

pub use utvpi::UtEdge;

pub use utvpi::UtvpiConfig;

pub use utvpi::UtvpiDetector;

pub use utvpi::UtvpiDetectorStats;

pub use utvpi::UtvpiResult;

pub use utvpi::UtvpiSolver;

pub use utvpi::UtvpiStats;

pub use checking::ArithCheckConfig;

pub use checking::ArithChecker;

pub use checking::ArrayChecker;

pub use checking::BvChecker;

pub use checking::CheckResult;

pub use checking::CheckerStats;

pub use checking::CombinedChecker;

pub use checking::Literal;

pub use checking::ProofChecker;

pub use checking::ProofStep;

pub use checking::ProofStepKind;

pub use checking::QuantChecker;

pub use checking::TheoryChecker;

pub use checking::TheoryKind;

pub use wmaxsat::SoftClause;

pub use wmaxsat::WMaxSatConfig;

pub use wmaxsat::WMaxSatResult;

pub use wmaxsat::WMaxSatSolver;

pub use wmaxsat::WMaxSatStats;

pub use wmaxsat::Weight as WMaxWeight;

pub use character::AdvancedCharSolver;

pub use character::CaseFoldMode;

pub use character::CaseFolder;

pub use character::CharClass;

pub use character::CharConfig;

pub use character::CharConstraint;

pub use character::CharDomain;

pub use character::CharNormalizer;

pub use character::CharResult;

pub use character::CharSolver;

pub use character::CharStats;

pub use character::CharValue;

pub use character::CharVar;

pub use character::CharWidth;

pub use character::CodePoint;

pub use character::NormalizationForm;

pub use character::UnicodeBlock;

pub use character::UnicodeCategory;

pub use character::UnicodeScript;

pub use set::CardConstraint;

pub use set::CardConstraintKind;

pub use set::CardDomain;

pub use set::CardPropagator;

pub use set::CardResult;

pub use set::CardStats;

pub use set::EnumSet;

pub use set::FiniteSetEnumerator;

pub use set::MemberConstraint;

pub use set::MemberDomain;

pub use set::MemberPropagator;

pub use set::MemberResult;

pub use set::MemberStats;

pub use set::MemberVar;

pub use set::PowersetBuilder;

pub use set::PowersetConstraint;

pub use set::PowersetIter;

pub use set::PowersetResult;

pub use set::PowersetStats;

pub use set::SetBinOp;

pub use set::SetComplement;

pub use set::SetConfig;

pub use set::SetConstraint;

pub use set::SetDifference;

pub use set::SetElement;

pub use set::SetEnumConfig;

pub use set::SetEnumResult;

pub use set::SetEnumStats;

pub use set::SetExpr;

pub use set::SetIntersection;

pub use set::SetOp;

pub use set::SetOpBuilder;

pub use set::SetOpResult;

pub use set::SetOpStats;

pub use set::SetResult;

pub use set::SetSolver;

pub use set::SetSort;

pub use set::SetStats;

pub use set::SetUnion;

pub use set::SetVar;

pub use set::SetVarId;

pub use set::SubsetConstraint;

pub use set::SubsetDomain;

pub use set::SubsetGraph;

pub use set::SubsetPropagator;

pub use set::SubsetResult;

pub use set::SubsetStats;

pub use sls::BackboneDetector;

pub use sls::BmsConfig;

pub use sls::BmsSelector;

pub use sls::CcanrConfig;

pub use sls::CcanrEnhancer;

pub use sls::ClauseId;

pub use sls::ClauseImportance;

pub use sls::ClauseSimplifier;

pub use sls::ClauseWeightManager;

pub use sls::DdfwConfig;

pub use sls::DdfwManager;

pub use sls::DiversificationManager;

pub use sls::DiversificationStrategy;

pub use sls::FocusedWalk;

pub use sls::FocusedWalkConfig;

pub use sls::HybridSlsInterface;

pub use sls::NoveltyConfig;

pub use sls::NoveltySelector;

pub use sls::PhaseMode;

pub use sls::PhaseSaver;

pub use sls::PortfolioConfig;

pub use sls::PortfolioSls;

pub use sls::RestartManager;

pub use sls::RestartStrategy;

pub use sls::SlsAlgorithm;

pub use sls::SlsConfig;

pub use sls::SlsResult;

pub use sls::SlsSolver;

pub use sls::SlsStats;

pub use sls::SolutionLearner;

pub use sls::SolutionVerifier;

pub use sls::SparrowConfig;

pub use sls::SparrowSelector;

pub use sls::VarActivity;

pub use sls::VarSelectHeuristic;

pub use sls::VerificationResult;

pub use sls::WeightedSlsConfig;

pub use sls::WeightedSlsSolver;

pub use sls::WeightedSlsStats;

pub use sls::WeightingScheme;

pub use sls::YalsatConfig;

pub use sls::YalsatSolver;

Modules

arithmetic

Linear Arithmetic theory solver

array

Array theory solver

array_eager_expand

Array Theory Eager Expansion.

bv

BitVector theory solver

character

Auto-generated module structure

checking

Theory Checking Framework

combination

Nelson-Oppen Theory Combination

config

Configuration options for theory solvers

datatype

Algebraic Datatype Theory Solver

diff_logic

Difference Logic Theory Solver

error

Error types for theory solvers

euf

Equality with Uninterpreted Functions (EUF) theory solver

fp

Floating-Point Theory Solver (QF_FP)

fp_interval_prop

Floating-Point Interval Propagation.

hashcons

Hash Consing for Efficient Term Sharing

nlsat

NLSAT Theory Wrapper

pb

Pseudo-Boolean and Cardinality Constraint Solver

propagation

Theory Propagation Queue with Priority Scheduling

quantifier

Quantifier Theory Solver

quantifier_code_tree

E-matching Code Tree for Multi-Pattern Matching.

recfun

Recursive Function Theory

set

Set Theory Solver for SMT

simplify

Theory-Specific Simplification and Preprocessing

sls

Stochastic Local Search (SLS) Theory Integration

special_relations

Special Relations Theory

string

String Theory Solver

string_length_prop

String Theory Length Constraint Propagation.

user_propagator

User Propagator Framework

utvpi

UTVPI (Unit Two-Variable Per Inequality) Theory Solver

watched

Watched Literals for Theory Constraints

wmaxsat

Weighted MaxSAT Theory Solver

Structs

EqualityNotification

Equality notification for Nelson-Oppen theory combination When one theory derives that two terms are equal, it notifies other theories

Enums

TheoryCheckResult

Result of a theory check

TheoryId

Unique identifier for a theory

Traits

Theory

Trait for theory solvers

TheoryCombination

Interface for theory combination via Nelson-Oppen Theories implement this to participate in equality sharing