oxiz-solver 0.2.0

Main CDCL(T) Solver API for OxiZ
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46

//! Conflict Analysis and Minimization.
//!
//! This module provides advanced conflict analysis techniques for CDCL(T)
//! solving, including conflict minimization, explanation generation, and
//! relevancy tracking.

#[allow(unused_imports)]
use crate::prelude::*;

pub mod clause_learning;
pub mod explanation_cache;
pub mod explanation_generator;
pub mod implication_graph;
pub mod minimizer;
pub mod recursive_minimizer;
pub mod relevancy;
pub mod theory_explainer;
pub mod uip_selection;

pub use clause_learning::{
    ClauseId, ClauseLearner, ClauseLearningConfig, ClauseLearningStats, ClauseMinimizer,
    ImplicationGraph as ClauseImplicationGraph, ImplicationNode as ClauseImplicationNode,
    LearnedClause, LearnedDatabase,
};

pub use explanation_cache::{
    CacheConfig, CacheKey, CacheStats, Explanation as CachedExplanation, ExplanationCache,
};
pub use explanation_generator::{
    Explanation, ExplanationConfig, ExplanationGenerator, ExplanationStats,
};
pub use implication_graph::{
    ImplicationGraph, ImplicationGraphConfig, ImplicationGraphStats, ImplicationNode, Level, Var,
};
pub use minimizer::{ConflictMinimizer, MinimizerConfig, MinimizerStats};
pub use recursive_minimizer::{
    Lit as RecursiveLit, Reason, RecursiveMinConfig, RecursiveMinStats, RecursiveMinimizer,
};
pub use relevancy::{ImplicationEdge, RelevancyConfig, RelevancyStats, RelevancyTracker};
pub use theory_explainer::{
    ExplainerConfig, ExplainerStats, ExplanationType, TheoryExplainer, TheoryExplanation,
};
pub use uip_selection::{
    ImplicationNode as UipImplicationNode, Level as UipLevel, UipConfig, UipSelector, UipStats,
    UipStrategy,
};