rustproof_libsmt/backends/
backend.rs

1//! Module that defines traits that need to be implemented, as a prerequisite to implement
2//! `Context`, that provies it SMT solver capabilities.
3
4use std::collections::HashMap;
5use std::fmt::Debug;
6use std::fmt;
7
8use backends::smtlib2::SMTProc;
9
10#[derive(Clone, Debug)]
11pub enum SMTError {
12    Undefined,
13    Unsat,
14    AssertionError(String),
15}
16
17#[derive(Clone, Debug)]
18pub enum SMTRes {
19    Sat(String, Option<String>),
20    Unsat(String, Option<String>),
21    Error(String, Option<String>),
22}
23
24
25pub type SMTResult<T> = Result<T, SMTError>;
26
27/// Trait a backend should implement to support SMT solving.
28///
29/// This is a minimalistic API and has to be expanded in the future to support more SMT operations
30/// and to grow this into a full SMTLib Crate.
31///
32/// All functions names are analogous in meaning to their usage in the original SMT-LIB2 sense.
33/// TODO:
34///  - define_fun
35///  - declare_sort
36///  - define_sort
37///  - get_proof
38///  - get_unsat_core
39///  - get_value
40///  - get_assignment
41///  - push
42///  - pop
43///  - get_option
44///  - set_option
45///  - get_info
46///  - set_info
47///  - exit
48pub trait SMTBackend {
49    type Idx: Debug + Clone;
50    type Logic: Logic;
51
52    fn set_logic<S: SMTProc>(&mut self, &mut S);
53    //fn declare_fun<T: AsRef<str>>(&mut self, Option<T>, Option<Vec<Type>>, Type) -> Self::Idx;
54
55    fn new_var<T, P>(&mut self, Option<T>, P) -> Self::Idx
56        where T: AsRef<str>,
57              P: Into<<<Self as SMTBackend>::Logic as Logic>::Sorts>;
58
59    fn assert<T: Into<<<Self as SMTBackend>::Logic as Logic>::Fns>>(&mut self, T, &[Self::Idx]) -> Self::Idx;
60    fn check_sat<S: SMTProc>(&mut self, &mut S, bool) -> SMTRes;
61    fn solve<S: SMTProc>(&mut self, &mut S, bool) -> (SMTResult<HashMap<Self::Idx, u64>>, SMTRes);
62}
63
64pub trait Logic: fmt::Display + Clone + Copy {
65    type Fns: SMTNode + fmt::Display + Debug + Clone;
66    type Sorts: fmt::Display + Debug + Clone;
67
68    fn free_var<T: AsRef<str>>(T, Self::Sorts) -> Self::Fns;
69}
70
71pub trait SMTNode: fmt::Display {
72    /// Returns true if the node is a symbolic variable
73    fn is_var(&self) -> bool;
74    /// Returns true if the node is a constant value
75    fn is_const(&self) -> bool;
76    /// Returns true if the node is a function
77    fn is_fn(&self) -> bool {
78        !self.is_var() && !self.is_const()
79    }
80}
rustproof_libsmt/backends/backend.rs

rustproof_libsmt/backends/
backend.rs
