[−][src]Trait rust_smt::SMTSolver

pub trait SMTSolver {
    type S: Sort;
    type T: Term;
    type F: UninterpretedFunction;
    fn new() -> Self;

    fn declare_sort(&self, name: &str) -> Result<Self::S, SMTError>;

    fn lookup_sort(&self, s: Sorts) -> Result<Self::S, SMTError>;

    fn apply_sort(
        &self, 
        s: Sorts, 
        s1: &Self::S, 
        s2: &Self::S
    ) -> Result<Self::S, SMTError>;

    fn declare_fun(
        &self, 
        name: &str, 
        args: &[&Self::S], 
        sort: &Self::S
    ) -> Result<Self::F, SMTError>;

    fn declare_const(
        &self, 
        name: &str, 
        sort: &Self::S
    ) -> Result<Self::T, SMTError>;

    fn lookup_const(&self, f: Fn) -> Result<Self::T, SMTError>;

    fn const_from_int(
        &self, 
        value: i64, 
        sort: &Self::S
    ) -> Result<Self::T, SMTError>;

    fn const_from_string(
        &self, 
        value: &str, 
        sort: &Self::S
    ) -> Result<Self::T, SMTError>;

    fn apply_fun(
        &self, 
        f: &Function<Self::F>, 
        args: &[&Self::T]
    ) -> Result<Self::T, SMTError>;

    fn level(&self) -> u32;

    fn push(&mut self, n: u32) -> Result<bool, SMTError>;

    fn pop(&mut self, n: u32) -> Result<bool, SMTError>;

    fn assert(&mut self, t: &Self::T) -> Result<bool, SMTError>;

    fn check_sat(&mut self) -> CheckSatResult;

    fn get_value(&mut self, t: &Self::T) -> Result<Self::T, SMTError>;
}

Associated Types

type S: Sort

type T: Term

type F: UninterpretedFunction

Loading content...

Required methods

fn new() -> Self

fn declare_sort(&self, name: &str) -> Result<Self::S, SMTError>

fn lookup_sort(&self, s: Sorts) -> Result<Self::S, SMTError>

fn apply_sort(
    &self,
    s: Sorts,
    s1: &Self::S,
    s2: &Self::S
) -> Result<Self::S, SMTError>

fn declare_fun(
    &self,
    name: &str,
    args: &[&Self::S],
    sort: &Self::S
) -> Result<Self::F, SMTError>

fn declare_const(&self, name: &str, sort: &Self::S) -> Result<Self::T, SMTError>

fn lookup_const(&self, f: Fn) -> Result<Self::T, SMTError>

fn const_from_int(
    &self,
    value: i64,
    sort: &Self::S
) -> Result<Self::T, SMTError>

fn const_from_string(
    &self,
    value: &str,
    sort: &Self::S
) -> Result<Self::T, SMTError>

fn apply_fun(
    &self,
    f: &Function<Self::F>,
    args: &[&Self::T]
) -> Result<Self::T, SMTError>

fn level(&self) -> u32

fn push(&mut self, n: u32) -> Result<bool, SMTError>

fn pop(&mut self, n: u32) -> Result<bool, SMTError>

fn assert(&mut self, t: &Self::T) -> Result<bool, SMTError>

fn check_sat(&mut self) -> CheckSatResult

fn get_value(&mut self, t: &Self::T) -> Result<Self::T, SMTError>

Loading content...

Implementors

impl SMTSolver for Z3SMTSolver[src]

type S = Z3Sort

type T = Z3Term

type F = Z3UninterpretedFunction

Loading content...