xmt-lib 0.1.1

A grounder for SMT solvers
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

// Copyright Pierre Carbonnelle, 2025.

use peg::{error::ParseError, str::LineCol};
use rusqlite::Error as SqlError;
use thiserror::Error;

use crate::ast::{Identifier, Term};
use crate::ast::L;

/// The number of characters since the begin of a source file.
///
/// Used for error reporting.
#[derive(Clone, Copy, Debug, Ord, PartialOrd, Eq, PartialEq, Hash)]
pub struct Offset(pub usize);

#[derive(Error, Debug, PartialEq)]
pub enum SolverError {

    #[error("{0}")]
    ParseError(#[from] ParseError<LineCol>),

    #[error("{0}")]
    ExprError(String),

    #[error("{0}: {1}")]
    TermError(&'static str, L<Term>),

    #[error("{0}: {1}")]
    IdentifierError(&'static str, L<Identifier>),

    #[error("Database error: {0}")]
    DatabaseError(#[from] SqlError),

    #[error("{0}")]
    InternalError(usize),  // can't be fixed by the user
}

use crate::error::SolverError::*;


/// Show the error in the context of the relevant source code.
pub fn format_error(input: &str, e: SolverError) -> String {
    match e {

        ParseError(e) =>
            pretty_print(input, e.location, format!("Expected: {}\n", e.expected)),

        DatabaseError(e) => format!("****** Database Error: {}\n", e),

        ExprError(msg) => format!("****** Error: {}\n", msg),

        TermError(msg, term) => {
            match offset_to_line_col_utf8(&input, term.start()) {
                None => format!("****** Error: {}\n", msg),
                Some(location) =>
                    pretty_print(input, location, msg.to_string())
            }
        },

        IdentifierError(msg, id) => {
            let msg = if id.start() != Offset(0) { msg.to_string() }
                else { format!("{msg} for {id}") };
            match offset_to_line_col_utf8(&input, id.start()) {
                None => format!("****** Error: {}\n", msg),
                Some(location) =>
                    pretty_print(input, location, msg.to_string())
            }
        },

        InternalError(n) => format!("****** Internal Error: {}\n", n)
    }
}


/// Show the error in the context of the `input` source code.
fn pretty_print(input: &str, location: LineCol, msg: String) -> String {
    if let Some(source) = input.lines().nth(location.line-1) {
        chic::Error::new(format!("at position ({}, {}): {}", location.line, location.column, msg))
            .error(
                location.line,
                location.column - 1,
                location.column,
                &source,
                msg,
            )
            .to_string()
    } else {
        format!("****** Error: {msg} at {location}\n")
    }

}

fn offset_to_line_col_utf8(s: &str, offset: Offset) -> Option<LineCol> {
    if offset.0 > s.len() {
        return None;
    }

    let mut current_offset = 0;

    for (line_number, line) in s.split('\n').enumerate() {
        let char_indices: Vec<_> = line.char_indices().collect();
        let line_length = line.len() + 1; // Include the newline character

        if current_offset + line_length > offset.0 {
            for (column, (byte_index, _)) in char_indices.iter().enumerate() {
                if current_offset + byte_index >= offset.0 {
                    return Some(LineCol{column: column + 1, line: line_number + 1, offset:offset.0});
                }
            }
        }

        current_offset += line_length;
    }

    None
}