theory_core 0.1.0

Neuro-symbolic reasoning core with SMT solver integration
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
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131

//! Simple Phase 2A demonstration tests

use anyhow::Result;
use theory_core::smt_stub::*;
use theory_core::*;

#[test]
fn test_constraint_ir_basic() -> Result<()> {
    // Test basic constraint IR construction
    let mut ir = ConstraintIR::new();

    // Add simple variable
    use theory_core::ir::{Domain, Variable, VariableMetadata};

    let var = Variable {
        name: "x".to_string(),
        domain: Domain::Boolean,
        metadata: VariableMetadata::default(),
    };

    let _var_id = ir.add_variable(var);

    // Add theory tag
    ir.add_theory_tag(theory_core::ir::TheoryTag::LRA);

    assert_eq!(ir.variables.len(), 1);
    assert_eq!(ir.theory_tags.len(), 1);

    Ok(())
}

#[test]
fn test_smt_backend_stub() -> Result<()> {
    let backend = SmtBackend::new(SmtBackendConfig::default())?;

    // Create simple constraint IR
    let mut ir = ConstraintIR::new();

    use theory_core::ir::{Domain, Variable, VariableMetadata};
    let var = Variable {
        name: "test_var".to_string(),
        domain: Domain::Boolean,
        metadata: VariableMetadata::default(),
    };

    ir.add_variable(var);

    // Test async solve in sync context using block_on
    let rt = tokio::runtime::Runtime::new().unwrap();
    let result = rt.block_on(async { backend.solve(&ir).await })?;

    // Stub should return satisfiable
    assert!(result.satisfiable);
    assert!(result.confidence > 0.5);
    assert!(!result.assignment.is_empty());

    Ok(())
}

#[test]
fn test_plausibility_checker() -> Result<()> {
    let checker = PlausibilityChecker::new(PlausibilityConfig::default());

    // Create minimal IR
    let mut ir = ConstraintIR::new();

    use theory_core::ir::{Domain, Variable, VariableMetadata};
    let var = Variable {
        name: "x".to_string(),
        domain: Domain::Boolean,
        metadata: VariableMetadata::default(),
    };

    ir.add_variable(var);

    // Create solution
    use std::collections::HashMap;
    let mut assignment = HashMap::new();
    assignment.insert("v0".to_string(), SolutionValue::Bool(true));

    let solution = SolutionResult {
        satisfiable: true,
        assignment,
        confidence: 0.95,
        estimated_time_ms: 5.0,
        winning_branch_id: None,
        winning_strategy: None,
        winning_backend: None,
        variable_ranges: None,
    };

    let result = checker.check_plausibility(&ir, &solution)?;

    assert!(result.plausible);
    assert!(result.confidence > 0.7);

    Ok(())
}

#[test]
fn test_routing_strategy() -> Result<()> {
    let router = SpeculateVerifyRouter::new();

    // Create constraint IR
    let mut ir = ConstraintIR::new();

    use theory_core::ir::{Domain, TheoryTag, Variable, VariableMetadata};
    let var = Variable {
        name: "x".to_string(),
        domain: Domain::Integer {
            min: Some(0),
            max: Some(100),
        },
        metadata: VariableMetadata::default(),
    };

    ir.add_variable(var);
    ir.add_theory_tag(TheoryTag::LRA);

    // Test routing decision
    let strategy = router.route(&ir)?;

    // Should return valid strategy
    match strategy {
        ReasoningStrategy::Speculate => println!("✓ Router chose speculative strategy"),
        ReasoningStrategy::Verify => println!("✓ Router chose verification strategy"),
        ReasoningStrategy::Hybrid => println!("✓ Router chose hybrid strategy"),
    }

    Ok(())
}