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

use crate::surrogate::SolutionValue;
use std::fmt;

impl fmt::Display for SolutionValue {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            SolutionValue::Bool(b) => write!(f, "{}", b),
            SolutionValue::Integer(i) => write!(f, "{}", i),
            SolutionValue::Real(r) => write!(f, "{}", r),
            SolutionValue::String(s) => write!(f, "\"{}\"", s),
            SolutionValue::BitVector { value, width } => {
                write!(f, "0b{:0width$b}", value, width = *width as usize)
            }
        }
    }
}