smt-scope 0.1.7

A library for parsing and analysing SMT traces.
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

#[cfg(feature = "mem_dbg")]
use mem_dbg::{MemDbg, MemSize};

use crate::{
    items::{Term, TermIdx},
    FxHashMap,
};

#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
#[derive(Debug, Default)]
pub struct TheorySolving {
    /// Rewrites to equivalent terms.
    pub equivs: FxHashMap<TermIdx, TermIdx>,
    pub reprs: FxHashMap<Term, TermIdx>,
}

impl TheorySolving {
    pub fn new_term(&mut self, term: &Term) {}
}

/// https://github.com/Z3Prover/z3/blob/z3-4.13.4/src/ast/ast.cpp#L856-L878
const BASIC_NAMES: &[&str] = &[
    "true",
    "false",
    "=",
    "distinct",
    "ite",
    "if",
    "and",
    "or",
    "xor",
    "not",
    "=>",
    "implies",
    "iff",
    "if_then_else",
    "&&",
    "||",
    "equals",
    "equiv",
];

/// https://github.com/Z3Prover/z3/blob/z3-4.13.4/src/ast/arith_decl_plugin.cpp#L599-L640
const ARITH_NAMES: &[&str] = &[
    "<=",
    ">=",
    "<",
    ">",
    "+",
    "-",
    "~",
    "*",
    "/",
    "div",
    "divisible",
    "rem",
    "mod",
    "to_real",
    "to_int",
    "is_int",
    "abs",
    "^",
    "^0",
    "sin",
    "cos",
    "tan",
    "asin",
    "acos",
    "atan",
    "sinh",
    "cosh",
    "tanh",
    "asinh",
    "acosh",
    "atanh",
    "pi",
    "euler",
    "/0",
    "div0",
    "mod0",
];