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 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326
use ast; use ast::Ast; use std::ffi::CStr; use std::fmt; use z3_sys::*; use Context; use Model; use Params; use SatResult; use Solver; use Z3_MUTEX; impl<'ctx> Solver<'ctx> { /// Create a new solver. This solver is a "combined solver" /// that internally uses a non-incremental (`solver1`) and an /// incremental solver (`solver2`). This combined solver changes /// its behaviour based on how it is used and how its parameters are set. /// /// If the solver is used in a non incremental way (i.e. no calls to /// [`Solver::push()`] or [`Solver::pop()`], and no calls to /// [`Solver::assert()`] or [`Solver::assert_and_track()`] after checking /// satisfiability without an intervening [`Solver::reset()`]) then `solver1` /// will be used. This solver will apply Z3's "default" tactic. /// /// The "default" tactic will attempt to probe the logic used by the /// assertions and will apply a specialized tactic if one is supported. /// Otherwise the general `(and-then simplify smt)` tactic will be used. /// /// If the solver is used in an incremental way then the combined solver /// will switch to using `solver2` (which behaves similarly to the general /// "smt" tactic). /// /// Note however it is possible to set the `solver2_timeout`, /// `solver2_unknown`, and `ignore_solver1` parameters of the combined /// solver to change its behaviour. /// /// The function [`Solver::get_model()`] retrieves a model if the /// assertions is satisfiable (i.e., the result is /// `SatResult::Sat`) and [model construction is enabled]. /// The function [`Solver::get_model()`] can also be used even /// if the result is `SatResult::Unknown`, but the returned model /// is not guaranteed to satisfy quantified assertions. /// /// [model construction is enabled]: struct.Config.html#method.set_model_generation /// [`Solver::assert()`]: #method.assert /// [`Solver::assert_and_track()`]: #method.assert_and_track /// [`Solver::get_model()`]: #method.get_model /// [`Solver::pop()`]: #method.pop /// [`Solver::push()`]: #method.push /// [`Solver::reset()`]: #method.reset /// pub fn new(ctx: &Context) -> Solver { Solver { ctx, z3_slv: unsafe { let guard = Z3_MUTEX.lock().unwrap(); let s = Z3_mk_solver(ctx.z3_ctx); Z3_solver_inc_ref(ctx.z3_ctx, s); s }, } } pub fn translate<'dest_ctx>(&self, dest: &'dest_ctx Context) -> Solver<'dest_ctx> { Solver { ctx: dest, z3_slv: unsafe { let guard = Z3_MUTEX.lock().unwrap(); let s = Z3_solver_translate(self.ctx.z3_ctx, self.z3_slv, dest.z3_ctx); Z3_solver_inc_ref(dest.z3_ctx, s); s }, } } /// Get this solver's context. pub fn get_context(&self) -> &'ctx Context { self.ctx } /// Assert a constraint into the solver. /// /// The functions [`Solver::check()`](#method.check) and /// [`Solver::check_assumptions()`](#method.check_assumptions) should be /// used to check whether the logical context is consistent or not. /// /// # See also: /// /// - [`Solver::assert_and_track()`](#method.assert_and_track) pub fn assert(&self, ast: &ast::Bool<'ctx>) { debug!("assert: {:?}", ast); let guard = Z3_MUTEX.lock().unwrap(); unsafe { Z3_solver_assert(self.ctx.z3_ctx, self.z3_slv, ast.z3_ast) }; } /// Assert a constraint `a` into the solver, and track it (in the /// unsat) core using the Boolean constant `p`. /// /// This API is an alternative to /// [`Solver::check_assumptions()`](#method.check_assumptions) /// for extracting unsat cores. Both APIs can be used in the same solver. /// The unsat core will contain a combination of the Boolean variables /// provided using [`Solver::assert_and_track()`](#method.assert_and_track) /// and the Boolean literals provided using /// [`Solver::check_assumptions()`](#method.check_assumptions). /// /// # See also: /// /// - [`Solver::assert()`](#method.assert) pub fn assert_and_track(&self, ast: &ast::Bool<'ctx>, p: &ast::Bool<'ctx>) { debug!("assert_and_track: {:?}", ast); let guard = Z3_MUTEX.lock().unwrap(); unsafe { Z3_solver_assert_and_track(self.ctx.z3_ctx, self.z3_slv, ast.z3_ast, p.z3_ast) }; } /// Remove all assertions from the solver. pub fn reset(&self) { let guard = Z3_MUTEX.lock().unwrap(); unsafe { Z3_solver_reset(self.ctx.z3_ctx, self.z3_slv) }; } /// Check whether the assertions in a given solver are consistent or not. /// /// The function [`Solver::get_model()`](#method.get_model) /// retrieves a model if the assertions is satisfiable (i.e., the /// result is `SatResult::Sat`) and [model construction is enabled]. /// Note that if the call returns `SatResult::Unknown`, Z3 does not /// ensure that calls to [`Solver::get_model()`](#method.get_model) /// succeed and any models produced in this case are not guaranteed /// to satisfy the assertions. /// /// The function [`Solver::get_proof()`](#method.get_proof) /// retrieves a proof if [proof generation was enabled] when the context /// was created, and the assertions are unsatisfiable (i.e., the result /// is `SatResult::Unsat`). /// /// # See also: /// /// - [`Config::set_model_generation()`](struct.Config.html#method.set_model_generation) /// - [`Config::set_proof_generation()`](struct.Config.html#method.set_proof_generation) /// - [`Solver::check_assumptions()`](#method.check_assumptions) /// /// [model construction is enabled]: struct.Config.html#method.set_model_generation /// [proof generation was enabled]: struct.Config.html#method.set_proof_generation pub fn check(&self) -> SatResult { let guard = Z3_MUTEX.lock().unwrap(); match unsafe { Z3_solver_check(self.ctx.z3_ctx, self.z3_slv) } { Z3_L_FALSE => SatResult::Unsat, Z3_L_UNDEF => SatResult::Unknown, Z3_L_TRUE => SatResult::Sat, _ => unreachable!(), } } /// Check whether the assertions in the given solver and /// optional assumptions are consistent or not. /// /// The function /// [`Solver::get_unsat_core()`](#method.get_unsat_core) /// retrieves the subset of the assumptions used in the /// unsatisfiability proof produced by Z3. /// /// # See also: /// /// - [`Solver::check()`](#method.check) pub fn check_assumptions(&self, assumptions: &[ast::Bool<'ctx>]) -> SatResult { let guard = Z3_MUTEX.lock().unwrap(); let a: Vec<Z3_ast> = assumptions.iter().map(|a| a.z3_ast).collect(); match unsafe { Z3_solver_check_assumptions(self.ctx.z3_ctx, self.z3_slv, a.len() as u32, a.as_ptr()) } { Z3_L_FALSE => SatResult::Unsat, Z3_L_UNDEF => SatResult::Unknown, Z3_L_TRUE => SatResult::Sat, _ => unreachable!(), } } /// Return a subset of the assumptions provided to either the last /// /// * `check_assumptions` call, or /// * sequence of `assert_and_track` calls followed by a `check` call. /// /// These are the assumptions Z3 used in the unsatisfiability proof. /// Assumptions are available in Z3. They are used to extract unsatisfiable /// cores. They may be also used to "retract" assumptions. Note that, /// assumptions are not really "soft constraints", but they can be used to /// implement them. /// /// # See also: /// /// - [`Solver::check_assumptions`](#method.check_assumptions) /// - [`Solver::assert_and_track`](#method.assert_and_track) pub fn get_unsat_core(&self) -> Vec<ast::Bool<'ctx>> { let z3_unsat_core = unsafe { let _guard = Z3_MUTEX.lock().unwrap(); Z3_solver_get_unsat_core(self.ctx.z3_ctx, self.z3_slv) }; if z3_unsat_core.is_null() { return vec![]; } let len = unsafe { let _guard = Z3_MUTEX.lock().unwrap(); Z3_ast_vector_size(self.ctx.z3_ctx, z3_unsat_core) }; let mut unsat_core = Vec::with_capacity(len as usize); for i in 0..len { let elem = unsafe { let _guard = Z3_MUTEX.lock().unwrap(); Z3_ast_vector_get(self.ctx.z3_ctx, z3_unsat_core, i) }; let elem = ast::Bool::new(self.ctx, elem); unsat_core.push(elem); } unsat_core } /// Create a backtracking point. /// /// The solver contains a stack of assertions. /// /// # See also: /// /// - [`Solver::pop()`](#method.pop) pub fn push(&self) { let guard = Z3_MUTEX.lock().unwrap(); unsafe { Z3_solver_push(self.ctx.z3_ctx, self.z3_slv) }; } /// Backtrack `n` backtracking points. /// /// # See also: /// /// - [`Solver::push()`](#method.push) pub fn pop(&self, n: u32) { let guard = Z3_MUTEX.lock().unwrap(); unsafe { Z3_solver_pop(self.ctx.z3_ctx, self.z3_slv, n) }; } /// Retrieve the model for the last [`Solver::check()`](#method.check) /// or [`Solver::check_assumptions()`](#method.check_assumptions) /// /// The error handler is invoked if a model is not available because /// the commands above were not invoked for the given solver, or if /// the result was `Z3_L_FALSE`. pub fn get_model(&self) -> Option<Model<'ctx>> { Model::of_solver(self) } /// Retrieve the proof for the last [`Solver::check()`](#method.check) /// or [`Solver::check_assumptions()`](#method.check_assumptions) /// /// The error handler is invoked if [proof generation is not enabled], /// or if the commands above were not invoked for the given solver, /// or if the result was different from `Z3_L_FALSE`. /// /// # See also: /// /// - [`Config::set_proof_generation()`](struct.Config.html#method.set_proof_generation) /// /// [proof generation is not enabled]: struct.Config.html#method.set_proof_generation // // This seems to actually return an Ast with kind `SortKind::Unknown`, which we don't // have an Ast subtype for yet. pub fn get_proof(&self) -> Option<impl Ast<'ctx>> { let m = unsafe { let _guard = Z3_MUTEX.lock().unwrap(); Z3_solver_get_proof(self.ctx.z3_ctx, self.z3_slv) }; if !m.is_null() { return Some(ast::Dynamic::new(self.ctx, m)); } else { return None; } } /// Return a brief justification for an "unknown" result (i.e., `SatResult::Unknown`) for /// the commands [`Solver::check()`](#method.check) and /// [`Solver::check_assumptions()`](#method.check_assumptions) pub fn get_reason_unknown(&self) -> Option<String> { let p = unsafe { Z3_solver_get_reason_unknown(self.ctx.z3_ctx, self.z3_slv) }; if p.is_null() { return None; } unsafe { CStr::from_ptr(p) } .to_str() .ok() .map(|s| s.to_string()) } /// Set the current solver using the given parameters. pub fn set_params(&self, params: &Params<'ctx>) { let guard = Z3_MUTEX.lock().unwrap(); unsafe { Z3_solver_set_params(self.ctx.z3_ctx, self.z3_slv, params.z3_params) }; } } impl<'ctx> fmt::Display for Solver<'ctx> { fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { let p = unsafe { Z3_solver_to_string(self.ctx.z3_ctx, self.z3_slv) }; if p.is_null() { return Result::Err(fmt::Error); } match unsafe { CStr::from_ptr(p) }.to_str() { Ok(s) => write!(f, "{}", s), Err(_) => Result::Err(fmt::Error), } } } impl<'ctx> fmt::Debug for Solver<'ctx> { fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { <Self as fmt::Display>::fmt(self, f) } } impl<'ctx> Drop for Solver<'ctx> { fn drop(&mut self) { let guard = Z3_MUTEX.lock().unwrap(); unsafe { Z3_solver_dec_ref(self.ctx.z3_ctx, self.z3_slv) }; } }