Skip to content

Commit ae52982

Browse files
SeRin-YangSeRin-Yang
committed
Move code of eval_ast_bool/int/real into SmtEval::eval
1 parent 793a281 commit ae52982

File tree

1 file changed

+182
-148
lines changed

1 file changed

+182
-148
lines changed

‎z3rro/src/model.rs‎

Lines changed: 182 additions & 148 deletions
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,49 @@ pub enum ModelSource<'ctx> {
2929
SwineModel(GetModelResponse<'ctx>),
3030
}
3131

32+
/// Convert a decimal string `d_str` into a pair of a numerator (`num`) and
33+
/// a denominator (`den`) in the form of '[numeral]' strings such that:
34+
/// d_str = num / den
35+
fn from_str_to_num_den(d_str: &str) -> Option<(String, String)> {
36+
if d_str.is_empty() {
37+
return None;
38+
}
39+
40+
if let Some(pos) = d_str.find('.') {
41+
let den = "1".to_string() + &"0".repeat(d_str.len() - pos - 1);
42+
43+
let mut num = d_str.to_string();
44+
num.remove(pos);
45+
num.trim_start_matches('0');
46+
47+
if num.is_empty() {
48+
num = "0".to_string();
49+
}
50+
51+
Some((num, den))
52+
} else {
53+
Some((d_str.to_string(), "1".to_string()))
54+
}
55+
}
56+
57+
/// Find a `FunctionDef` object defined for a given symbol `symbol` within the `model_res`.
58+
fn find_fun_def<'ctx>(
59+
model_res: &GetModelResponse<'ctx>,
60+
symbol: &str,
61+
) -> Option<&'ctx FunctionDef<'ctx>> {
62+
model_res.0.iter().find_map(|m_res| {
63+
if let ModelResponse::DefineFun(fun_def) = m_res {
64+
if fun_def.0.0 == symbol {
65+
Some(fun_def)
66+
} else {
67+
None
68+
}
69+
} else {
70+
None
71+
}
72+
})
73+
}
74+
3275
/// A [`z3::Model`] which keeps track of the accessed constants. This is useful
3376
/// to later print those constants which were not accessed by any of the
3477
/// [`SmtEval`] implementations (e.g. stuff generated by Z3 we don't know
@@ -82,115 +125,6 @@ impl<'ctx> InstrumentedModel<'ctx> {
82125
}
83126
}
84127

85-
pub fn eval_ast_bool(&self, ast: &Bool<'ctx>) -> Option<Bool<'ctx>> {
86-
let name = ast.decl().name();
87-
88-
if let ModelSource::SwineModel(s_model) = &self.model {
89-
match Self::find_fun_def(s_model, &name) {
90-
Some(fun_def) => match fun_def.3 {
91-
Term::Identifier(QualIdentifier::Identifier(Identifier::Simple(Symbol(
92-
"true",
93-
)))) => Some(Bool::from_bool(ast.get_ctx(), true)),
94-
Term::Identifier(QualIdentifier::Identifier(Identifier::Simple(Symbol(
95-
"false",
96-
)))) => Some(Bool::from_bool(ast.get_ctx(), false)),
97-
_ => None,
98-
},
99-
None => None,
100-
}
101-
} else {
102-
None
103-
}
104-
}
105-
106-
pub fn eval_ast_int(&self, ast: &Int<'ctx>) -> Option<Int<'ctx>> {
107-
let name = ast.decl().name();
108-
109-
if let ModelSource::SwineModel(s_model) = &self.model {
110-
match Self::find_fun_def(s_model, &name) {
111-
Some(fun_def) => match fun_def.3 {
112-
Term::SpecConstant(SpecConstant::Numeral(numeral)) => {
113-
if let Ok(n) = numeral.into_u128() {
114-
let n_str = n.to_string();
115-
Int::from_str(ast.get_ctx(), &n_str)
116-
} else {
117-
None
118-
}
119-
}
120-
_ => None,
121-
},
122-
None => None,
123-
}
124-
} else {
125-
None
126-
}
127-
}
128-
129-
pub fn eval_ast_real(&self, ast: &Real<'ctx>) -> Option<Real<'ctx>> {
130-
let name = ast.decl().name();
131-
132-
if let ModelSource::SwineModel(s_model) = &self.model {
133-
match Self::find_fun_def(s_model, &name) {
134-
Some(fun_def) => match fun_def.3 {
135-
Term::SpecConstant(SpecConstant::Decimal(Decimal(d_str))) => {
136-
if let Some((num, den)) = Self::from_str_to_num_den(d_str) {
137-
Real::from_real_str(ast.get_ctx(), &num, &den)
138-
} else {
139-
None
140-
}
141-
}
142-
_ => None,
143-
},
144-
None => None,
145-
}
146-
} else {
147-
None
148-
}
149-
}
150-
151-
/// Convert a decimal string `d_str` into a pair of a numerator (`num`) and
152-
/// a denominator (`den`) in the form of '[numeral]' strings such that:
153-
/// d_str = num / den
154-
pub fn from_str_to_num_den(d_str: &str) -> Option<(String, String)> {
155-
if d_str.is_empty() {
156-
return None;
157-
}
158-
159-
if let Some(pos) = d_str.find('.') {
160-
let den = "1".to_string() + &"0".repeat(d_str.len() - pos - 1);
161-
162-
let mut num = d_str.to_string();
163-
num.remove(pos);
164-
num.trim_start_matches('0');
165-
166-
if num.is_empty() {
167-
num = "0".to_string();
168-
}
169-
170-
Some((num, den))
171-
} else {
172-
Some((d_str.to_string(), "1".to_string()))
173-
}
174-
}
175-
176-
/// Find a `FunctionDef` object defined for a given symbol `symbol` within the `model_res`.
177-
pub fn find_fun_def(
178-
model_res: &GetModelResponse<'ctx>,
179-
symbol: &str,
180-
) -> Option<&'ctx FunctionDef<'ctx>> {
181-
model_res.0.iter().find_map(|m_res| {
182-
if let ModelResponse::DefineFun(fun_def) = m_res {
183-
if fun_def.0.0 == symbol {
184-
Some(fun_def)
185-
} else {
186-
None
187-
}
188-
} else {
189-
None
190-
}
191-
})
192-
}
193-
194128
/// Get the function interpretation for this `f`.
195129
pub fn get_func_interp(&self, f: &FuncDecl<'ctx>) -> Option<FuncInterp<'ctx>> {
196130
self.accessed_decls.borrow_mut().insert(f.name());
@@ -269,64 +203,164 @@ impl<'ctx> SmtEval<'ctx> for Bool<'ctx> {
269203
type Value = bool;
270204

271205
fn eval(&self, model: &InstrumentedModel<'ctx>) -> Result<bool, SmtEvalError> {
272-
model
273-
.eval(self, true)
274-
.ok_or(SmtEvalError::EvalError)?
275-
.as_bool()
276-
.ok_or(SmtEvalError::ParseError)
206+
match model.model {
207+
ModelSource::Z3Model(_) => {
208+
model
209+
.eval(self, true)
210+
.ok_or(SmtEvalError::EvalError)?
211+
.as_bool()
212+
.ok_or(SmtEvalError::ParseError)
213+
},
214+
ModelSource::SwineModel(s_model) => {
215+
216+
let name: String = self.decl().name();
217+
218+
match find_fun_def(&s_model, &name) {
219+
Some(fun_def) => match fun_def.3 {
220+
Term::Identifier(QualIdentifier::Identifier(Identifier::Simple(Symbol(
221+
"true",
222+
)))) => Ok(true),
223+
Term::Identifier(QualIdentifier::Identifier(Identifier::Simple(Symbol(
224+
"false",
225+
)))) => Ok(false),
226+
_ => Err(SmtEvalError::EvalError),
227+
},
228+
None => Err(SmtEvalError::EvalError),
229+
}
230+
},
231+
}
277232
}
278233
}
279234

280235
impl<'ctx> SmtEval<'ctx> for Int<'ctx> {
281236
type Value = BigInt;
282237

283238
fn eval(&self, model: &InstrumentedModel<'ctx>) -> Result<BigInt, SmtEvalError> {
284-
// TODO: Z3's as_i64 only returns an i64 value. is there something more complete?
285-
let value = model
286-
.eval(self, true)
287-
.ok_or(SmtEvalError::EvalError)?
288-
.as_i64()
289-
.ok_or(SmtEvalError::ParseError)?;
290-
Ok(BigInt::from(value))
239+
match model.model {
240+
ModelSource::Z3Model(_) => {
241+
// TODO: Z3's as_i64 only returns an i64 value. is there something more complete?
242+
let value = model
243+
.eval(self, true)
244+
.ok_or(SmtEvalError::EvalError)?
245+
.as_i64()
246+
.ok_or(SmtEvalError::ParseError)?;
247+
Ok(BigInt::from(value))
248+
}
249+
ModelSource::SwineModel(s_model) => {
250+
let name = self.decl().name();
251+
match find_fun_def(&s_model, &name) {
252+
Some(fun_def) => match fun_def.3 {
253+
Term::SpecConstant(SpecConstant::Numeral(numeral)) => {
254+
if let Ok(n) = numeral.into_u128() {
255+
Ok(BigInt::from(n))
256+
} else {
257+
Err(SmtEvalError::EvalError)
258+
}
259+
}
260+
_ => Err(SmtEvalError::EvalError),
261+
},
262+
None => Err(SmtEvalError::EvalError),
263+
}
264+
},
265+
}
291266
}
292267
}
293268

294269
impl<'ctx> SmtEval<'ctx> for Real<'ctx> {
295270
type Value = BigRational;
296271

297272
fn eval(&self, model: &InstrumentedModel<'ctx>) -> Result<Self::Value, SmtEvalError> {
298-
let res = model
299-
.eval(self, false) // TODO
300-
.ok_or(SmtEvalError::EvalError)?;
301-
302-
// The .as_real() method only returns a pair of i64 values. If the
303-
// results don't fit in these types, we start some funky string parsing.
304-
if let Some((num, den)) = res.as_real() {
305-
Ok(BigRational::new(num.into(), den.into()))
306-
} else {
307-
// we parse a string of the form "(/ num.0 denom.0)"
308-
let division_expr = format!("{:?}", res);
309-
if !division_expr.starts_with("(/ ") || !division_expr.ends_with(".0)") {
310-
return Err(SmtEvalError::ParseError);
311-
}
273+
match model.model {
274+
ModelSource::Z3Model(_) => {
275+
let res = model
276+
.eval(self, false) // TODO
277+
.ok_or(SmtEvalError::EvalError)?;
278+
279+
// The .as_real() method only returns a pair of i64 values. If the
280+
// results don't fit in these types, we start some funky string parsing.
281+
if let Some((num, den)) = res.as_real() {
282+
Ok(BigRational::new(num.into(), den.into()))
283+
} else {
284+
// we parse a string of the form "(/ num.0 denom.0)"
285+
let division_expr = format!("{:?}", res);
286+
if !division_expr.starts_with("(/ ") || !division_expr.ends_with(".0)") {
287+
return Err(SmtEvalError::ParseError);
288+
}
312289

313-
let mut parts = division_expr.split_ascii_whitespace();
290+
let mut parts = division_expr.split_ascii_whitespace();
314291

315-
let first_part = parts.next().ok_or(SmtEvalError::ParseError)?;
316-
if first_part != "(/" {
317-
return Err(SmtEvalError::ParseError);
318-
}
292+
let first_part = parts.next().ok_or(SmtEvalError::ParseError)?;
293+
if first_part != "(/" {
294+
return Err(SmtEvalError::ParseError);
295+
}
319296

320-
let second_part = parts.next().ok_or(SmtEvalError::ParseError)?;
321-
let second_part = second_part.replace(".0", "");
322-
let numerator = BigInt::from_str(&second_part).map_err(|_| SmtEvalError::ParseError)?;
297+
let second_part = parts.next().ok_or(SmtEvalError::ParseError)?;
298+
let second_part = second_part.replace(".0", "");
299+
let numerator = BigInt::from_str(&second_part).map_err(|_| SmtEvalError::ParseError)?;
323300

324-
let third_part = parts.next().ok_or(SmtEvalError::ParseError)?;
325-
let third_part = third_part.replace(".0)", "");
326-
let denominator =
327-
BigInt::from_str(&third_part).map_err(|_| SmtEvalError::ParseError)?;
301+
let third_part = parts.next().ok_or(SmtEvalError::ParseError)?;
302+
let third_part = third_part.replace(".0)", "");
303+
let denominator =
304+
BigInt::from_str(&third_part).map_err(|_| SmtEvalError::ParseError)?;
328305

329-
Ok(BigRational::new(numerator, denominator))
306+
Ok(BigRational::new(numerator, denominator))
307+
}
308+
},
309+
ModelSource::SwineModel(s_model) => {
310+
let name = self.decl().name();
311+
312+
match find_fun_def(&s_model, &name) {
313+
Some(fun_def) => match fun_def.3 {
314+
Term::SpecConstant(SpecConstant::Decimal(Decimal(d_str))) => {
315+
let f = (*d_str).parse::<f64>().map_err(|_| SmtEvalError::EvalError)?;
316+
let res = BigRational::from_float(f).ok_or(SmtEvalError::EvalError)?;
317+
Ok(res)
318+
}
319+
Term::Application(QualIdentifier::Identifier(Identifier::Simple(Symbol("/"))), [t1, t2]) => {
320+
let mut num = BigInt::from(1);
321+
let mut den = BigInt::from(1);
322+
match t1 {
323+
Term::SpecConstant(SpecConstant::Numeral(numeral)) => {
324+
let n = numeral.into_u128().map_err(|_| SmtEvalError::EvalError)?;
325+
num *= BigInt::from(n);
326+
},
327+
Term::SpecConstant(SpecConstant::Decimal(Decimal(d_str))) => {
328+
if let Some((n, d)) = from_str_to_num_den(d_str) {
329+
num *= BigInt::from_str(&n).map_err(|_| SmtEvalError::EvalError)?;
330+
den *= BigInt::from_str(&d).map_err(|_| SmtEvalError::EvalError)?;
331+
} else {
332+
return Err(SmtEvalError::EvalError);
333+
}
334+
},
335+
_ => {
336+
return Err(SmtEvalError::EvalError);
337+
},
338+
}
339+
match t2 {
340+
Term::SpecConstant(SpecConstant::Numeral(numeral)) => {
341+
let n = numeral.into_u128().map_err(|_| SmtEvalError::EvalError)?;
342+
den *= BigInt::from(n);
343+
},
344+
Term::SpecConstant(SpecConstant::Decimal(Decimal(d_str))) => {
345+
if let Some((n, d)) = from_str_to_num_den(d_str) {
346+
den *= BigInt::from_str(&n).map_err(|_| SmtEvalError::EvalError)?;
347+
num *= BigInt::from_str(&d).map_err(|_| SmtEvalError::EvalError)?;
348+
} else {
349+
return Err(SmtEvalError::EvalError);
350+
}
351+
},
352+
_ => {
353+
return Err(SmtEvalError::EvalError);
354+
},
355+
}
356+
Ok(BigRational::new(num, den))
357+
}
358+
_ => Err(SmtEvalError::EvalError),
359+
},
360+
None => Err(SmtEvalError::EvalError),
361+
}
362+
},
330363
}
364+
331365
}
332366
}

0 commit comments

Comments
 (0)