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 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207
// Copyright (c) Facebook, Inc. and its affiliates. // // This source code is licensed under the MIT license found in the // LICENSE file in the root directory of this source tree. // An abstract interface for SMT solvers, parameterized by implementations of // Sort, Term, and UninterpretedFunction. This interface aims to mimic the // SMT-LIB commands as closely as possible. See http:://www.smtlib.org for // documentation on the SMT standard and interface. See tests/test.rs for // examples of how to use the interface. pub mod smt_err; pub mod smt_ops; // Most functions return an SMTResult. If an error is returned, there are three // possibilities: // APIError - this results when the API is misused. // UnsupportedError - this results when the solver doesn't support a feature // InternalError - this results when the solver or a library call fails. // See smt_err.rs for more details. type SMTResult<T> = Result<T, smt_err::SMTError>; // The result of calling check_sat is either satisfiable (Sat), unsatisfiable // (Unsat), or unknown (Unknown). #[derive(Debug, PartialEq, Clone, Copy)] pub enum CheckSatResult { Sat, Unsat, Unknown, } // An abstract data type for SMT sorts. pub trait Sort: Clone + std::fmt::Debug + Eq + std::hash::Hash + Sized { // Get a string representing the SMT-LIB name for the Sort. The only // possible error is InternalError. fn to_string(&self) -> SMTResult<String>; } // An abstract data type for uninterpreted function symbols. pub trait UninterpretedFunction: std::fmt::Debug + std::clone::Clone + Sized { // Get the name of the uninterpreted function. The only possible error is // InternalError. fn to_string(&self) -> SMTResult<String>; } // A Function is either a built-in operator or an uninterpreted function. pub enum Function<'a, F: UninterpretedFunction> { Op(smt_ops::Fn<'a>), UF(F), } // An abstract data type for SMT terms. pub trait Term: std::fmt::Debug + std::clone::Clone + Sized { // Get a string for the SMT-LIB representation of the term. The only // possible error is InternalError. fn to_string(&self) -> SMTResult<String>; // For terms that are constant values representable as i64, return the // corresponding i64 value. Returns APIError if term is not a constant of // real, int, or bitvector type, or if it is a non-integral real constant, // or if the integral value doesn't fit in 64 bits. fn to_int(&self) -> SMTResult<i64>; } // An abstract data type for SMT solvers. pub trait SMTSolver { type S: Sort; type T: Term; type F: UninterpretedFunction; // Return a new solver object. fn new() -> Self; /////////////////////////////////////////////////////////////////////////// // Sorts // /////////////////////////////////////////////////////////////////////////// // Declare a new uninterpreted sort with the given name. Only // InternalError errors are possible. fn declare_sort(&self, name: &str) -> SMTResult<Self::S>; // Lookup a built-in sort belonging to an SMT-LIB theory. Returns an // APIError if s is a sort constructor (e.g. Array). fn lookup_sort(&self, s: smt_ops::Sorts) -> SMTResult<Self::S>; // Apply a built-in sort constructor of arity 2. Returns an APIError if s // is not a sort constructor of arity 2. fn apply_sort(&self, s: smt_ops::Sorts, s1: &Self::S, s2: &Self::S) -> SMTResult<Self::S>; // Create a record with field names given in fields and corresponding sorts // given in sorts. The fields are used together with the RecordSelect and // RecordUpdate operators to read from or update records of this sort. An // APIError results if the number of fields does not match the number of // sorts, if the field names are not all distinct, or if a record of the // same name has already been declared. fn declare_record_sort( &mut self, name: &str, fields: &[&str], sorts: &[&Self::S], ) -> SMTResult<Self::S>; /////////////////////////////////////////////////////////////////////////// // Functions // /////////////////////////////////////////////////////////////////////////// // Declare a new uninterpreted function with the given name. args specifies // the argument sorts, and sort specifies the return sort. Returns an // UninterpretedFunction object. Only InternalError errors are possible. fn declare_fun(&self, name: &str, args: &[&Self::S], sort: &Self::S) -> SMTResult<Self::F>; /////////////////////////////////////////////////////////////////////////// // Terms // /////////////////////////////////////////////////////////////////////////// // Declare a new constant with a given name and sort. Only InternalError // errors are possible. fn declare_const(&self, name: &str, sort: &Self::S) -> SMTResult<Self::T>; // Lookup a built-in constant belonging to an SMT-LIB theory. Returns an // APIError if f is not a built-in constant. fn lookup_const(&self, f: smt_ops::Fn) -> SMTResult<Self::T>; // Construct a constant from a 64-bit integer of a given sort. Supported // sorts are integer, real, and bitvector (for bitvector the value must be // non-negative and fit in the bit-width). If an invalid sort is used or // an invalid value is used with a bitvector sort, the result is an // APIError. fn const_from_int(&self, value: i64, sort: &Self::S) -> SMTResult<Self::T>; // Construct a constant of a given sort from a numeric string. Supported // sorts are integer, real, and bitvector. Expects only digits // (non-bitvectors can also have a single unary minus at the beginning, and // reals can have at most one decimal point). Currently does not check if // value fits within the bitwidth for bitvector sorts. Behavior in that // case is dependent on the solver. fn const_from_string(&self, value: &str, sort: &Self::S) -> SMTResult<Self::T>; // Construct a record literal of sort record_sort using the terms in // field_values. fn record_const(&self, record_sort: &Self::S, field_values: &[Self::T]) -> SMTResult<Self::T>; // Sams as above, except the arguments are in a vector of references to // terms rather than a vector of terms. fn record_const_refs( &self, record_sort: &Self::S, field_values: &[&Self::T], ) -> SMTResult<Self::T>; // Apply a function f to a vector of arguments to get a Term object. f can // be either a built-in function operator or the result of an earlier call // to declare_fun. The number and sorts of the terms in args should match // the arity and argument sorts of the function f. Behavior if the // arguments are incorrect is solver-dependent. If a solver does not // support an SMT-LIB operation, an UnsupportedError is returned. fn apply_fun(&self, f: &Function<Self::F>, args: &[Self::T]) -> SMTResult<Self::T>; // Sams as above, except the arguments are in a vector of references to // terms rather than a vector of terms. fn apply_fun_refs(&self, f: &Function<Self::F>, args: &[&Self::T]) -> SMTResult<Self::T>; /////////////////////////////////////////////////////////////////////////// // Solving // /////////////////////////////////////////////////////////////////////////// // Returns the current level of the solver. Initially the level is 0. The // level increases with each push and decreases with each pop. fn level(&self) -> u32; // A push sets a checkpoint in the state of the solver. This method pushes // n times. Returns Ok(true) if successful. Otherwise, returns // InternalError. fn push(&mut self, n: u32) -> SMTResult<bool>; // A pop restores the solver to the state it had at the last checkpoint. // This method pops n times. n must be less than or equal to the current // level. If it is not, returns an APIError. Otherwise, returns // InternalError if unsuccessful. fn pop(&mut self, n: u32) -> SMTResult<bool>; // Add an assertion t to the solver context. The sort of the assertion must // be Boolean. Returns Ok(true) if successful. Otherwise returns // InternalError. fn assert(&mut self, t: &Self::T) -> SMTResult<bool>; // Check the satisfiability of all the assertions in the current solver // context. Returns a CheckSatResult (see above). fn check_sat(&mut self) -> CheckSatResult; // After a call to check_sat that returns Sat, if the solver has model // production enabled, then it can report a concrete constant value for any // term t. get_value returns that value, given a term t. If check_sat has // not been called or if the most recent call returned unsat, an APIError // is returned. fn get_value(&mut self, t: &Self::T) -> SMTResult<Self::T>; } // Support for Z3 solver. #[macro_use] extern crate lazy_static; pub mod z3; pub use z3::Z3Solver; pub fn new_z3_solver() -> Z3Solver { Z3Solver::new() }