use std::collections::hash_map::Entry;
use std::collections::HashMap;
use std::error::Error;
use std::ffi::{CStr, CString};
extern crate z3_sys;
use z3_sys::*;
use crate::smt_err::SMTError;
use crate::smt_ops::*;
use crate::Function::*;
use crate::*;
use std::sync::Mutex;
lazy_static! {
static ref Z3_MUTEX: Mutex<()> = Mutex::new(());
}
macro_rules! mutex {
() => {
let _mutex = Z3_MUTEX.lock().unwrap();
};
}
#[derive(Debug, Eq, Hash, PartialEq)]
pub struct Z3Sort {
context: Z3_context,
sort: Z3_sort,
}
fn new_z3_sort(context: Z3_context, sort: Z3_sort, mutex: bool) -> Z3Sort {
unsafe {
if mutex {
mutex!();
}
Z3_inc_ref(context, Z3_sort_to_ast(context, sort));
}
Z3Sort { context, sort }
}
impl Clone for Z3Sort {
fn clone(&self) -> Z3Sort {
new_z3_sort(self.context, self.sort, true)
}
}
impl Drop for Z3Sort {
fn drop(&mut self) {
unsafe {
mutex!();
Z3_dec_ref(self.context, Z3_sort_to_ast(self.context, self.sort));
}
}
}
impl Sort for Z3Sort {
fn to_string(&self) -> SMTResult<String> {
unsafe {
mutex!();
let ptr = Z3_sort_to_string(self.context, self.sort) as *mut i8;
if ptr.is_null() {
Err(SMTError::new_internal("Unable to convert Sort to string"))
} else {
let cstr = CStr::from_ptr(ptr);
match cstr.to_str() {
Ok(s) => Ok(String::from(s)),
Err(e) => Err(SMTError::new_internal(e.description())),
}
}
}
}
}
#[derive(Debug, Eq, Hash, PartialEq)]
pub struct Z3UninterpretedFunction {
context: Z3_context,
decl: Z3_func_decl,
}
fn new_z3_uninterpreted_function(
context: Z3_context,
decl: Z3_func_decl,
mutex: bool,
) -> Z3UninterpretedFunction {
unsafe {
if mutex {
mutex!();
}
Z3_inc_ref(context, Z3_func_decl_to_ast(context, decl));
Z3UninterpretedFunction { context, decl }
}
}
impl Clone for Z3UninterpretedFunction {
fn clone(&self) -> Z3UninterpretedFunction {
new_z3_uninterpreted_function(self.context, self.decl, true)
}
}
impl Drop for Z3UninterpretedFunction {
fn drop(&mut self) {
unsafe {
mutex!();
Z3_dec_ref(self.context, Z3_func_decl_to_ast(self.context, self.decl));
}
}
}
impl UninterpretedFunction for Z3UninterpretedFunction {
fn to_string(&self) -> SMTResult<String> {
unsafe {
mutex!();
let ptr = Z3_get_decl_name(self.context, self.decl);
if ptr.is_null() {
Err(SMTError::new_internal(
"Unable to get name for UninterpretedFunction",
))
} else {
let ptr = Z3_get_symbol_string(self.context, ptr);
if ptr.is_null() {
Err(SMTError::new_internal(
"Unable to convert UninterpretedFunction name to string",
))
} else {
let cstr = CStr::from_ptr(ptr);
match cstr.to_str() {
Ok(s) => Ok(String::from(s)),
Err(e) => Err(SMTError::new_internal(e.description())),
}
}
}
}
}
}
#[derive(Debug, Eq, Hash, PartialEq)]
pub struct Z3Term {
context: Z3_context,
ast: Z3_ast,
}
fn new_z3_term(context: Z3_context, ast: Z3_ast, mutex: bool) -> Z3Term {
unsafe {
if mutex {
mutex!();
}
Z3_inc_ref(context, ast);
}
Z3Term { context, ast }
}
impl Clone for Z3Term {
fn clone(&self) -> Z3Term {
new_z3_term(self.context, self.ast, true)
}
}
impl Drop for Z3Term {
fn drop(&mut self) {
unsafe {
mutex!();
Z3_dec_ref(self.context, self.ast);
}
}
}
impl Term for Z3Term {
fn to_string(&self) -> SMTResult<String> {
unsafe {
mutex!();
let ptr = Z3_ast_to_string(self.context, self.ast) as *mut i8;
if ptr.is_null() {
Err(SMTError::new_internal("Unable to convert Term to string"))
} else {
let cstr = CStr::from_ptr(ptr);
match cstr.to_str() {
Ok(s) => Ok(String::from(s)),
Err(e) => Err(SMTError::new_internal(e.description())),
}
}
}
}
fn to_int(&self) -> SMTResult<i64> {
unsafe {
mutex!();
let z3sort = Z3_get_sort(self.context, self.ast);
let ok = match Z3_get_sort_kind(self.context, z3sort) {
SortKind::Int => true,
SortKind::Real => true,
SortKind::BV => true,
_ => false,
};
if !ok {
Err(SMTError::new_api(
"Term::to_int: sort of term is not int, real, or bitvector",
))
} else {
let ok = match Z3_get_ast_kind(self.context, self.ast) {
AstKind::Numeral => true,
_ => false,
};
if !ok {
Err(SMTError::new_api(
"Term::to_int: term is not a numeric constant",
))
} else {
let mut tmp: ::std::os::raw::c_longlong = 0;
let res = Z3_get_numeral_int64(self.context, self.ast, &mut tmp);
if res {
Ok(tmp)
} else {
Err(SMTError::new_api(
"Term::to_int: unable to convert to 64-bit integer",
))
}
}
}
}
}
}
struct RecordInfo {
field_map: HashMap<String, u32>,
cons_decl: Z3UninterpretedFunction,
}
pub struct Z3Solver {
config: Z3_config,
context: Z3_context,
solver: Z3_solver,
level: u32,
model: Option<Z3_model>,
last_result: CheckSatResult,
record_map: HashMap<Z3_sort, RecordInfo>,
}
impl Drop for Z3Solver {
fn drop(&mut self) {
unsafe {
self.record_map.clear();
mutex!();
if let Some(m) = self.model {
Z3_model_dec_ref(self.context, m);
}
Z3_solver_dec_ref(self.context, self.solver);
Z3_del_context(self.context);
Z3_del_config(self.config);
}
}
}
impl SMTSolver for Z3Solver {
type S = Z3Sort;
type T = Z3Term;
type F = Z3UninterpretedFunction;
fn new() -> Z3Solver {
unsafe {
mutex!();
let cfg = Z3_mk_config();
let cxt = Z3_mk_context(cfg);
let s = Z3_mk_solver(cxt);
Z3_solver_inc_ref(cxt, s);
Z3Solver {
config: cfg,
context: cxt,
solver: s,
level: 0,
model: None,
last_result: CheckSatResult::Unknown,
record_map: HashMap::new(),
}
}
}
fn declare_sort(&self, name: &str) -> SMTResult<Z3Sort> {
unsafe {
match CString::new(name) {
Err(e) => Err(SMTError::new_internal(e.description())),
Ok(str) => {
let sort = {
mutex!();
let sym = Z3_mk_string_symbol(self.context, str.as_ptr());
Z3_mk_uninterpreted_sort(self.context, sym)
};
Ok(new_z3_sort(self.context, sort, true))
}
}
}
}
fn lookup_sort(&self, s: Sorts) -> SMTResult<Z3Sort> {
unsafe {
mutex!();
match s {
Sorts::Bool => Ok(new_z3_sort(
self.context,
Z3_mk_bool_sort(self.context),
false,
)),
Sorts::Int => Ok(new_z3_sort(
self.context,
Z3_mk_int_sort(self.context),
false,
)),
Sorts::Real => Ok(new_z3_sort(
self.context,
Z3_mk_real_sort(self.context),
false,
)),
Sorts::Array => Err(SMTError::new_api("Use apply_sort to create Array sorts")),
Sorts::BitVec(i) => Ok(new_z3_sort(
self.context,
Z3_mk_bv_sort(self.context, i),
false,
)),
}
}
}
fn apply_sort(&self, s: Sorts, s1: &Z3Sort, s2: &Z3Sort) -> SMTResult<Z3Sort> {
unsafe {
match s {
Sorts::Array => {
let sort = {
mutex!();
Z3_mk_array_sort(self.context, s1.sort, s2.sort)
};
Ok(new_z3_sort(self.context, sort, true))
}
_ => Err(SMTError::new_api(
"apply_sort called with non-sort constructor",
)),
}
}
}
fn declare_record_sort(
&mut self,
name: &str,
fields: &[&str],
sorts: &[&Z3Sort],
) -> SMTResult<Z3Sort> {
let mut result = Ok(0 as Z3_sort);
if fields.len() != sorts.len() {
result = Err(SMTError::new_api(
"declare_record_sort: fields and sorts must have same length",
));
};
unsafe {
mutex!();
let record_name = name.to_string();
let cons_name = record_name.clone() + "_cons";
let recognizer_name = record_name.clone() + "_is_cons";
let record_name_sym = match CString::new(record_name.clone()) {
Err(e) => {
if result.is_ok() {
result = Err(SMTError::new_internal(e.description()));
}
0 as Z3_symbol
}
Ok(str) => Z3_mk_string_symbol(self.context, str.as_ptr()),
};
let cons_name_sym = match CString::new(cons_name) {
Err(e) => {
if result.is_ok() {
result = Err(SMTError::new_internal(e.description()));
};
0 as Z3_symbol
}
Ok(str) => Z3_mk_string_symbol(self.context, str.as_ptr()),
};
let recognizer_name_sym = match CString::new(recognizer_name) {
Err(e) => {
if result.is_ok() {
result = Err(SMTError::new_internal(e.description()));
};
0 as Z3_symbol
}
Ok(str) => Z3_mk_string_symbol(self.context, str.as_ptr()),
};
let mut selector_names = Vec::new();
let mut z3_sorts = Vec::new();
let mut sort_refs = Vec::new();
for (i, sort) in sorts.iter().enumerate() {
let selector_name = fields[i].to_string();
let selector_name_sym = match CString::new(selector_name) {
Err(e) => {
if result.is_ok() {
result = Err(SMTError::new_internal(e.description()));
};
0 as Z3_symbol
}
Ok(str) => Z3_mk_string_symbol(self.context, str.as_ptr()),
};
selector_names.push(selector_name_sym);
z3_sorts.push(sort.sort);
sort_refs.push(0);
}
if result.is_ok() {
let constructor = Z3_mk_constructor(
self.context,
cons_name_sym,
recognizer_name_sym,
fields.len() as ::std::os::raw::c_uint,
selector_names.as_ptr(),
z3_sorts.as_ptr(),
sort_refs.as_mut_ptr(),
);
let mut tmp = Vec::new();
tmp.push(constructor);
let datatype = Z3_mk_datatype(self.context, record_name_sym, 1, tmp.as_mut_ptr());
let dummy = 0 as Z3_func_decl;
let mut cons_decls = [dummy];
let mut tester_decls = [dummy];
let mut accessors = Vec::new();
for _sort in sorts {
accessors.push(dummy);
}
Z3_query_constructor(
self.context,
constructor,
fields.len() as ::std::os::raw::c_uint,
cons_decls.as_mut_ptr(),
tester_decls.as_mut_ptr(),
accessors.as_mut_ptr(),
);
let mut field_map = HashMap::new();
for (i, field) in fields.iter().enumerate() {
match field_map.entry(field.to_string()) {
Entry::Occupied(_) => {
if result.is_ok() {
result = Err(SMTError::new_api(
"declare_record_sort: field names must be distinct",
));
}
}
Entry::Vacant(v) => {
v.insert(i as u32);
}
}
}
match self.record_map.entry(datatype) {
Entry::Occupied(_) => {
if result.is_ok() {
result = Err(SMTError::new_api(
"declare_record_sort: record already exists",
));
}
}
Entry::Vacant(v) => {
let record_info = RecordInfo {
field_map,
cons_decl: new_z3_uninterpreted_function(
self.context,
cons_decls[0],
false,
),
};
v.insert(record_info);
}
};
Z3_del_constructor(self.context, constructor);
if result.is_ok() {
result = Ok(datatype);
}
}
};
match result {
Err(err) => Err(err),
Ok(sort) => Ok(new_z3_sort(self.context, sort, true)),
}
}
fn declare_fun(
&self,
name: &str,
args: &[&Z3Sort],
sort: &Z3Sort,
) -> SMTResult<Z3UninterpretedFunction> {
unsafe {
match CString::new(name) {
Err(e) => Err(SMTError::new_internal(e.description())),
Ok(str) => {
let decl = {
mutex!();
let sym = Z3_mk_string_symbol(self.context, str.as_ptr());
let mut tmp = Vec::new();
for arg in args {
tmp.push(arg.sort);
}
Z3_mk_func_decl(
self.context,
sym,
tmp.len() as ::std::os::raw::c_uint,
tmp.as_ptr(),
sort.sort,
)
};
Ok(new_z3_uninterpreted_function(self.context, decl, true))
}
}
}
}
fn declare_const(&self, name: &str, sort: &Z3Sort) -> SMTResult<Z3Term> {
unsafe {
match CString::new(name) {
Err(e) => Err(SMTError::new_internal(e.description())),
Ok(str) => {
let sym = Z3_mk_string_symbol(self.context, str.as_ptr());
let term = {
mutex!();
Z3_mk_const(self.context, sym, sort.sort)
};
Ok(new_z3_term(self.context, term, true))
}
}
}
}
fn lookup_const(&self, f: Fn) -> SMTResult<Z3Term> {
unsafe {
mutex!();
match f {
Fn::False => Ok(new_z3_term(self.context, Z3_mk_false(self.context), false)),
Fn::True => Ok(new_z3_term(self.context, Z3_mk_true(self.context), false)),
_ => Err(SMTError::new_api("lookup_const called with non-constant")),
}
}
}
fn const_from_int(&self, value: i64, sort: &Z3Sort) -> SMTResult<Z3Term> {
unsafe {
mutex!();
let sortkind = Z3_get_sort_kind(self.context, sort.sort);
let ok = match sortkind {
SortKind::Int => true,
SortKind::Real => true,
SortKind::BV => {
if value < 0 {
false
} else {
let size = Z3_get_bv_sort_size(self.context, sort.sort);
if size >= 63 {
true
} else {
value < ((1 as i64) << size)
}
}
}
_ => false,
};
if !ok {
if sortkind == SortKind::BV {
Err(SMTError::new_api("const_from_int: bitvector requires non-negative value representable in the bit-width"))
} else {
Err(SMTError::new_api(
"const_from_int: sort of term is not int, real, or bitvector",
))
}
} else {
Ok(new_z3_term(
self.context,
Z3_mk_int64(self.context, value, sort.sort),
false,
))
}
}
}
fn const_from_string(&self, value: &str, sort: &Z3Sort) -> SMTResult<Z3Term> {
unsafe {
mutex!();
let sortkind = Z3_get_sort_kind(self.context, sort.sort);
let mut ok = match sortkind {
SortKind::Int => true,
SortKind::Real => true,
SortKind::BV => true,
_ => false,
};
if !ok {
Err(SMTError::new_api(
"const_from_string: sort must be int, real or bitvector",
))
} else {
let mut dec = 0;
ok = true;
let mut neg = false;
for (i, c) in value.chars().enumerate() {
if c == '.' {
dec += 1;
} else if c == '-' && i == 0 {
neg = true;
} else if !c.is_digit(10) {
ok = false;
}
}
if sortkind != SortKind::Real && dec > 0 {
Err(SMTError::new_api(
"const_from_string: decimal not allowed in non-real",
))
} else if dec > 1 {
Err(SMTError::new_api(
"const_from_string: no more than one decimal place allowed",
))
} else if neg && sortkind == SortKind::BV {
Err(SMTError::new_api(
"const_from_string: negative value not allowed for bitvectors",
))
} else if !ok {
Err(SMTError::new_api(
"const_from_string: string contains invalid character: digit expected",
))
} else {
match CString::new(value) {
Err(e) => Err(SMTError::new_internal(e.description())),
Ok(str) => Ok(new_z3_term(
self.context,
Z3_mk_numeral(self.context, str.as_ptr(), sort.sort),
false,
)),
}
}
}
}
}
fn record_const(&self, record_sort: &Z3Sort, field_values: &[Z3Term]) -> SMTResult<Z3Term> {
let mut tmp = Vec::new();
for value in field_values {
tmp.push(value);
}
self.record_const_refs(record_sort, &tmp)
}
fn record_const_refs(
&self,
record_sort: &Z3Sort,
field_values: &[&Z3Term],
) -> SMTResult<Z3Term> {
let mut tmp = Vec::new();
for value in field_values {
tmp.push(value.ast);
}
match self.record_map.get(&record_sort.sort) {
None => Err(SMTError::new_api(
"record_const_refs: Non-record or unknown sort",
)),
Some(record_info) => unsafe {
mutex!();
Ok(new_z3_term(
self.context,
Z3_mk_app(
self.context,
record_info.cons_decl.decl,
tmp.len() as ::std::os::raw::c_uint,
tmp.as_ptr(),
),
false,
))
},
}
}
fn apply_fun(
&self,
f: &Function<Z3UninterpretedFunction>,
args: &[Z3Term],
) -> SMTResult<Z3Term> {
let mut tmp = Vec::new();
for arg in args {
tmp.push(arg);
}
self.apply_fun_refs(f, &tmp)
}
fn apply_fun_refs(
&self,
f: &Function<Z3UninterpretedFunction>,
args: &[&Z3Term],
) -> SMTResult<Z3Term> {
macro_rules! unary_fun {
( $z3fun:ident ) => {
Ok($z3fun(self.context, args[0].ast))
};
}
macro_rules! unary_int_fun {
( $z3fun:ident, $i:ident ) => {
Ok($z3fun(
self.context,
*$i as ::std::os::raw::c_uint,
args[0].ast,
))
};
}
macro_rules! binary_fun {
( $z3fun:ident ) => {
Ok($z3fun(self.context, args[0].ast, args[1].ast))
};
}
macro_rules! trinary_fun {
( $z3fun:ident ) => {
Ok($z3fun(self.context, args[0].ast, args[1].ast, args[2].ast))
};
}
macro_rules! nary_fun {
( $z3fun:ident ) => {{
let mut tmp = Vec::new();
for arg in args {
tmp.push(arg.ast);
}
Ok($z3fun(
self.context,
tmp.len() as ::std::os::raw::c_uint,
tmp.as_ptr(),
))
}};
}
let term = unsafe {
mutex!();
match f {
UF(f) => {
let mut tmp = Vec::new();
for arg in args {
tmp.push(arg.ast);
}
Ok(Z3_mk_app(
self.context,
f.decl,
tmp.len() as ::std::os::raw::c_uint,
tmp.as_ptr(),
))
}
Op(Fn::Not) => unary_fun!(Z3_mk_not),
Op(Fn::Implies) => binary_fun!(Z3_mk_implies),
Op(Fn::And) => nary_fun!(Z3_mk_and),
Op(Fn::Or) => nary_fun!(Z3_mk_or),
Op(Fn::Xor) => binary_fun!(Z3_mk_xor),
Op(Fn::Eq) => binary_fun!(Z3_mk_eq),
Op(Fn::Neq) => binary_fun!(Z3_mk_eq),
Op(Fn::Ite) => trinary_fun!(Z3_mk_ite),
Op(Fn::Distinct) => nary_fun!(Z3_mk_distinct),
Op(Fn::Uminus) => unary_fun!(Z3_mk_unary_minus),
Op(Fn::Minus) => nary_fun!(Z3_mk_sub),
Op(Fn::Plus) => nary_fun!(Z3_mk_add),
Op(Fn::Times) => nary_fun!(Z3_mk_mul),
Op(Fn::Divide) => binary_fun!(Z3_mk_div),
Op(Fn::Div) => binary_fun!(Z3_mk_div),
Op(Fn::Mod) => binary_fun!(Z3_mk_mod),
Op(Fn::Abs) => Err(SMTError::new_unsupported("Z3 does not support abs")),
Op(Fn::LE) => binary_fun!(Z3_mk_le),
Op(Fn::LT) => binary_fun!(Z3_mk_lt),
Op(Fn::GE) => binary_fun!(Z3_mk_ge),
Op(Fn::GT) => binary_fun!(Z3_mk_gt),
Op(Fn::ToReal) => unary_fun!(Z3_mk_int2real),
Op(Fn::ToInt) => unary_fun!(Z3_mk_real2int),
Op(Fn::IsInt) => unary_fun!(Z3_mk_is_int),
Op(Fn::Select) => binary_fun!(Z3_mk_select),
Op(Fn::Store) => trinary_fun!(Z3_mk_store),
Op(Fn::Concat) => binary_fun!(Z3_mk_concat),
Op(Fn::Bvnot) => unary_fun!(Z3_mk_bvnot),
Op(Fn::Bvand) => binary_fun!(Z3_mk_bvand),
Op(Fn::Bvor) => binary_fun!(Z3_mk_bvor),
Op(Fn::Bvneg) => unary_fun!(Z3_mk_bvneg),
Op(Fn::Bvadd) => binary_fun!(Z3_mk_bvadd),
Op(Fn::Bvmul) => binary_fun!(Z3_mk_bvmul),
Op(Fn::Bvudiv) => binary_fun!(Z3_mk_bvudiv),
Op(Fn::Bvurem) => binary_fun!(Z3_mk_bvurem),
Op(Fn::Bvshl) => binary_fun!(Z3_mk_bvshl),
Op(Fn::Bvlshr) => binary_fun!(Z3_mk_bvlshr),
Op(Fn::Bvult) => binary_fun!(Z3_mk_bvult),
Op(Fn::Bvnand) => binary_fun!(Z3_mk_bvnand),
Op(Fn::Bvnor) => binary_fun!(Z3_mk_bvnor),
Op(Fn::Bvxor) => binary_fun!(Z3_mk_bvxor),
Op(Fn::Bvxnor) => binary_fun!(Z3_mk_bvxnor),
Op(Fn::Bvcomp) => Err(SMTError::new_unsupported("Z3 does not support bvcomp")),
Op(Fn::Bvsub) => binary_fun!(Z3_mk_bvsub),
Op(Fn::Bvsdiv) => binary_fun!(Z3_mk_bvsdiv),
Op(Fn::Bvsrem) => binary_fun!(Z3_mk_bvsrem),
Op(Fn::Bvsmod) => binary_fun!(Z3_mk_bvsmod),
Op(Fn::Bvashr) => binary_fun!(Z3_mk_bvashr),
Op(Fn::Bvule) => binary_fun!(Z3_mk_bvule),
Op(Fn::Bvugt) => binary_fun!(Z3_mk_bvugt),
Op(Fn::Bvuge) => binary_fun!(Z3_mk_bvuge),
Op(Fn::Bvslt) => binary_fun!(Z3_mk_bvslt),
Op(Fn::Bvsle) => binary_fun!(Z3_mk_bvsle),
Op(Fn::Bvsgt) => binary_fun!(Z3_mk_bvsgt),
Op(Fn::Bvsge) => binary_fun!(Z3_mk_bvsge),
Op(Fn::Repeat(i)) => unary_int_fun!(Z3_mk_repeat, i),
Op(Fn::ZeroExtend(i)) => unary_int_fun!(Z3_mk_zero_ext, i),
Op(Fn::SignExtend(i)) => unary_int_fun!(Z3_mk_sign_ext, i),
Op(Fn::RotateLeft(i)) => unary_int_fun!(Z3_mk_rotate_left, i),
Op(Fn::RotateRight(i)) => unary_int_fun!(Z3_mk_rotate_right, i),
Op(Fn::Extract(i, j)) => Ok(Z3_mk_extract(
self.context,
*i as ::std::os::raw::c_uint,
*j as ::std::os::raw::c_uint,
args[0].ast,
)),
Op(Fn::RecordSelect(field)) => {
if args.len() != 1 {
Err(SMTError::new_api(
"RecordSelect should have exactly one argument",
))
} else {
let sort = Z3_get_sort(self.context, args[0].ast);
match self.record_map.get(&sort) {
None => Err(SMTError::new_api(
"RecordSelect applied to non-record or unknown sort",
)),
Some(record_info) => {
match record_info.field_map.get(&field.to_string()) {
None => Err(SMTError::new_api(
"RecordSelect applied with unknown field",
)),
Some(i) => {
let selector = Z3_get_datatype_sort_constructor_accessor(
self.context,
sort,
0,
*i,
);
let mut tmp = Vec::new();
tmp.push(args[0].ast);
Ok(Z3_mk_app(self.context, selector, 1, tmp.as_ptr()))
}
}
}
}
}
}
Op(Fn::RecordUpdate(field)) => {
if args.len() != 2 {
Err(SMTError::new_api(
"RecordUpdate should have exactly two arguments",
))
} else {
let sort = Z3_get_sort(self.context, args[0].ast);
match self.record_map.get(&sort) {
None => Err(SMTError::new_api(
"First argument of RecordUpdate is non-record or unknown sort",
)),
Some(record_info) => {
match record_info.field_map.get(&field.to_string()) {
None => Err(SMTError::new_api(
"RecordUpdate applied with unknown field",
)),
Some(i) => {
let selector = Z3_get_datatype_sort_constructor_accessor(
self.context,
sort,
0,
*i,
);
if Z3_get_sort(self.context, args[1].ast)
!= Z3_get_range(self.context, selector)
{
Err(SMTError::new_api("Second argument of RecordUpdate does not have correct sort"))
} else {
Ok(Z3_datatype_update_field(
self.context,
selector,
args[0].ast,
args[1].ast,
))
}
}
}
}
}
}
}
_ => Err(SMTError::new_unsupported(
"apply_fun called with unknown operator",
)),
}
};
match term {
Ok(t) => Ok(new_z3_term(self.context, t, true)),
Err(err) => Err(err),
}
}
fn level(&self) -> u32 {
self.level
}
fn push(&mut self, n: u32) -> SMTResult<bool> {
unsafe {
mutex!();
for _x in 0..n {
Z3_solver_push(self.context, self.solver);
}
}
self.level += n;
Ok(true)
}
fn pop(&mut self, n: u32) -> SMTResult<bool> {
if n > self.level {
Err(SMTError::new_api("pop: called with n > level"))
} else {
unsafe {
mutex!();
if let Some(m) = self.model {
Z3_model_dec_ref(self.context, m);
}
self.model = None;
Z3_solver_pop(self.context, self.solver, 1);
}
self.level -= n;
Ok(true)
}
}
fn assert(&mut self, t: &Z3Term) -> SMTResult<bool> {
unsafe {
mutex!();
Z3_solver_assert(self.context, self.solver, t.ast);
Ok(true)
}
}
fn check_sat(&mut self) -> CheckSatResult {
unsafe {
mutex!();
if let Some(m) = self.model {
Z3_model_dec_ref(self.context, m);
}
self.model = None;
self.last_result = match Z3_solver_check(self.context, self.solver) {
Z3_L_TRUE => CheckSatResult::Sat,
Z3_L_FALSE => CheckSatResult::Unsat,
_ => CheckSatResult::Unknown,
};
self.last_result
}
}
fn get_value(&mut self, t: &Z3Term) -> SMTResult<Z3Term> {
if self.last_result != CheckSatResult::Sat {
Err(SMTError::new_api(
"get_value: can only be called after a call to check_sat that returns Sat",
))
} else {
unsafe {
mutex!();
if self.model == None {
let m = Z3_solver_get_model(self.context, self.solver);
if !m.is_null() {
Z3_model_inc_ref(self.context, m);
self.model = Some(m);
}
}
if let Some(m) = self.model {
let mut tmp: Z3_ast = t.ast;
let res = Z3_model_eval(self.context, m, t.ast, true, &mut tmp);
if !res {
Err(SMTError::new_internal("Unable to get value"))
} else {
Ok(new_z3_term(self.context, tmp, false))
}
} else {
Err(SMTError::new_internal("Model not found"))
}
}
}
}
}