Parse counterexample from swine via solver.from_string

Author: SeRin-Yang

z3rro/src/model.rs

@@ -8,13 +8,6 @@ use std::{
 
 use num::{BigInt, BigRational};
 
-use smtlib_lowlevel::{
-    ast::{
-        FunctionDef, GetModelResponse, Identifier, ModelResponse, QualIdentifier, SpecConstant,
-        Term,
-    },
-    lexicon::{Decimal, Symbol},
-};
 
 use thiserror::Error;
 
@@ -23,67 +16,21 @@ use z3::{
     FuncDecl, FuncInterp, Model,
 };
 
-#[derive(Debug)]
-pub enum ModelSource<'ctx> {
-    Z3Model(Model<'ctx>),
-    SwineModel(GetModelResponse<'ctx>),
-}
-
-/// Convert a decimal string `d_str` into a pair of a numerator (`num`) and 
-/// a denominator (`den`) in the form of '[numeral]' strings such that: 
-/// d_str = num / den
-fn from_str_to_num_den(d_str: &str) -> Option<(BigInt, BigInt)> {
-    if d_str.is_empty() {
-        return None;
-    }
-
-    if d_str.ends_with(".0") {
-        let num = BigInt::from_str(&d_str.replace(".0", "")).ok()?;
-        Some((num, BigInt::from(1)))
-    } else if let Some(pos) = d_str.find('.') {
-        let den = BigInt::from(10).pow((d_str.len() - pos - 1).try_into().unwrap());
-        let num = BigInt::from_str(&d_str.replace(".", "")).ok()?;
-
-        Some((num, den))
-    } else {
-        let num = BigInt::from_str(d_str).ok()?;
-        Some((num, BigInt::from(1)))
-    }
-}
-
-/// Find a `FunctionDef` object defined for a given symbol `symbol` within the `model_res`.
-fn find_fun_def<'ctx>(
-    model_res: &GetModelResponse<'ctx>,
-    symbol: &str,
-) -> Option<&'ctx FunctionDef<'ctx>> {
-    model_res.0.iter().find_map(|m_res| {
-        if let ModelResponse::DefineFun(fun_def) = m_res {
-            if fun_def.0.0 == symbol {
-                Some(fun_def)
-            } else {
-                None
-            }
-        } else {
-            None
-        }
-    })
-}
-
 /// A [`z3::Model`] which keeps track of the accessed constants. This is useful
 /// to later print those constants which were not accessed by any of the
 /// [`SmtEval`] implementations (e.g. stuff generated by Z3 we don't know
 /// about). This way, we can print the whole model and pretty-print everything
 /// we know, and then print the rest of the assignments in the model as well.
 #[derive(Debug)]
 pub struct InstrumentedModel<'ctx> {
-    model: ModelSource<'ctx>,
+    model: Model<'ctx>,
     // TODO: turn this into a HashSet of FuncDecls when the type implements Hash
     accessed_decls: RefCell<im_rc::HashSet<String>>,
     accessed_exprs: RefCell<im_rc::HashSet<Dynamic<'ctx>>>,
 }
 
 impl<'ctx> InstrumentedModel<'ctx> {
-    pub fn new(model: ModelSource<'ctx>) -> Self {
+    pub fn new(model: Model<'ctx>) -> Self {
         InstrumentedModel {
             model,
             accessed_decls: Default::default(),
@@ -113,20 +60,14 @@ impl<'ctx> InstrumentedModel<'ctx> {
     /// the model.
     pub fn eval<T: Ast<'ctx>>(&self, ast: &T, model_completion: bool) -> Option<T> {
         self.add_children_accessed(Dynamic::from_ast(ast));
-        match &self.model {
-            ModelSource::Z3Model(model) => {
-                let res = model.eval(ast, model_completion)?;
-                Some(res)
-            }
-            ModelSource::SwineModel(_) => todo!(),
-        }
+        let res = self.model.eval(ast, model_completion)?;
+        Some(res)
     }
 
     /// Get the function interpretation for this `f`.
     pub fn get_func_interp(&self, f: &FuncDecl<'ctx>) -> Option<FuncInterp<'ctx>> {
         self.accessed_decls.borrow_mut().insert(f.name());
-        todo!()
-        // self.model.get_func_interp(f)
+        self.model.get_func_interp(f)
     }
 
     /// Add this ast node and all its children to the accessed set.
@@ -151,12 +92,9 @@ impl<'ctx> InstrumentedModel<'ctx> {
     /// Iterate over all function declarations that were not accessed using
     /// `eval` so far.
     pub fn iter_unaccessed(&self) -> impl Iterator<Item = FuncDecl<'ctx>> + '_ {
-        todo!()
-        /*
         self.model
             .iter()
             .filter(|decl| !self.accessed_decls.borrow().contains(&decl.name()))
-         */
     }
 
     /// Reset the internally tracked accessed declarations and expressions.
@@ -166,17 +104,15 @@ impl<'ctx> InstrumentedModel<'ctx> {
     }
 
     pub fn into_model(self) -> Model<'ctx> {
-        todo!()
-        // self.model
+        self.model
     }
 }
 
 /// The [`Display`] implementation simply defers to the underlying
 /// [`z3::Model`]'s implementation.
 impl Display for InstrumentedModel<'_> {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
-        todo!()
-        // f.write_fmt(format_args!("{}", &self.model))
+        f.write_fmt(format_args!("{}", &self.model))
     }
 }
 
@@ -200,164 +136,64 @@ impl<'ctx> SmtEval<'ctx> for Bool<'ctx> {
     type Value = bool;
 
     fn eval(&self, model: &InstrumentedModel<'ctx>) -> Result<bool, SmtEvalError> {
-        match model.model {
-            ModelSource::Z3Model(_) => {
-                model
-                .eval(self, true)
-                .ok_or(SmtEvalError::EvalError)?
-                .as_bool()
-                .ok_or(SmtEvalError::ParseError)
-            },
-            ModelSource::SwineModel(s_model) => {
-
-                let name: String = self.decl().name();
-
-                match find_fun_def(&s_model, &name) {
-                    Some(fun_def) => match fun_def.3 {
-                        Term::Identifier(QualIdentifier::Identifier(Identifier::Simple(Symbol(
-                            "true",
-                        )))) => Ok(true),
-                        Term::Identifier(QualIdentifier::Identifier(Identifier::Simple(Symbol(
-                            "false",
-                        )))) => Ok(false),
-                        _ => Err(SmtEvalError::EvalError),
-                    },
-                    None => Err(SmtEvalError::EvalError),
-                }
-            },
-        }
+        model
+            .eval(self, true)
+            .ok_or(SmtEvalError::EvalError)?
+            .as_bool()
+            .ok_or(SmtEvalError::ParseError)
     }
 }
 
 impl<'ctx> SmtEval<'ctx> for Int<'ctx> {
     type Value = BigInt;
 
     fn eval(&self, model: &InstrumentedModel<'ctx>) -> Result<BigInt, SmtEvalError> {
-        match model.model {
-            ModelSource::Z3Model(_) => {
-                // TODO: Z3's as_i64 only returns an i64 value. is there something more complete?
-                let value = model
-                    .eval(self, true)
-                    .ok_or(SmtEvalError::EvalError)?
-                    .as_i64()
-                    .ok_or(SmtEvalError::ParseError)?;
-                Ok(BigInt::from(value))
-            }
-            ModelSource::SwineModel(s_model) => {
-                let name = self.decl().name();
-                match find_fun_def(&s_model, &name) {
-                    Some(fun_def) => match fun_def.3 {
-                        Term::SpecConstant(SpecConstant::Numeral(numeral)) => {
-                            if let Ok(n) = numeral.into_u128() {
-                                Ok(BigInt::from(n))
-                            } else {
-                                Err(SmtEvalError::EvalError)
-                            }
-                        }
-                        _ => Err(SmtEvalError::EvalError),
-                    },
-                    None => Err(SmtEvalError::EvalError),
-                }
-            },
-        }
+        // TODO: Z3's as_i64 only returns an i64 value. is there something more complete?
+        let value = model
+            .eval(self, true)
+            .ok_or(SmtEvalError::EvalError)?
+            .as_i64()
+            .ok_or(SmtEvalError::ParseError)?;
+        Ok(BigInt::from(value))
     }
 }
 
 impl<'ctx> SmtEval<'ctx> for Real<'ctx> {
     type Value = BigRational;
 
     fn eval(&self, model: &InstrumentedModel<'ctx>) -> Result<Self::Value, SmtEvalError> {
-        match model.model {
-            ModelSource::Z3Model(_) => {
-                let res = model
-                    .eval(self, false) // TODO
-                    .ok_or(SmtEvalError::EvalError)?;
-
-                // The .as_real() method only returns a pair of i64 values. If the
-                // results don't fit in these types, we start some funky string parsing.
-                if let Some((num, den)) = res.as_real() {
-                    Ok(BigRational::new(num.into(), den.into()))
-                } else {
-                    // we parse a string of the form "(/ num.0 denom.0)"
-                    let division_expr = format!("{:?}", res);
-                    if !division_expr.starts_with("(/ ") || !division_expr.ends_with(".0)") {
-                        return Err(SmtEvalError::ParseError);
-                    }
-
-                    let mut parts = division_expr.split_ascii_whitespace();
+        let res = model
+            .eval(self, false) // TODO
+            .ok_or(SmtEvalError::EvalError)?;
+
+        // The .as_real() method only returns a pair of i64 values. If the
+        // results don't fit in these types, we start some funky string parsing.
+        if let Some((num, den)) = res.as_real() {
+            Ok(BigRational::new(num.into(), den.into()))
+        } else {
+            // we parse a string of the form "(/ num.0 denom.0)"
+            let division_expr = format!("{:?}", res);
+            if !division_expr.starts_with("(/ ") || !division_expr.ends_with(".0)") {
+                return Err(SmtEvalError::ParseError);
+            }
 
-                    let first_part = parts.next().ok_or(SmtEvalError::ParseError)?;
-                    if first_part != "(/" {
-                        return Err(SmtEvalError::ParseError);
-                    }
+            let mut parts = division_expr.split_ascii_whitespace();
 
-                    let second_part = parts.next().ok_or(SmtEvalError::ParseError)?;
-                    let second_part = second_part.replace(".0", "");
-                    let numerator = BigInt::from_str(&second_part).map_err(|_| SmtEvalError::ParseError)?;
+            let first_part = parts.next().ok_or(SmtEvalError::ParseError)?;
+            if first_part != "(/" {
+                return Err(SmtEvalError::ParseError);
+            }
 
-                    let third_part = parts.next().ok_or(SmtEvalError::ParseError)?;
-                    let third_part = third_part.replace(".0)", "");
-                    let denominator =
-                        BigInt::from_str(&third_part).map_err(|_| SmtEvalError::ParseError)?;
+            let second_part = parts.next().ok_or(SmtEvalError::ParseError)?;
+            let second_part = second_part.replace(".0", "");
+            let numerator = BigInt::from_str(&second_part).map_err(|_| SmtEvalError::ParseError)?;
 
-                    Ok(BigRational::new(numerator, denominator))
-                }
-            },
-            ModelSource::SwineModel(s_model) => {
-                let name = self.decl().name();
+            let third_part = parts.next().ok_or(SmtEvalError::ParseError)?;
+            let third_part = third_part.replace(".0)", "");
+            let denominator =
+                BigInt::from_str(&third_part).map_err(|_| SmtEvalError::ParseError)?;
 
-                match find_fun_def(&s_model, &name) {
-                    Some(fun_def) => match fun_def.3 {
-                        Term::SpecConstant(SpecConstant::Decimal(Decimal(d_str))) => {
-                            let f = (*d_str).parse::<f64>().map_err(|_| SmtEvalError::EvalError)?;
-                            let res = BigRational::from_float(f).ok_or(SmtEvalError::EvalError)?;
-                            Ok(res)
-                        }
-                        Term::Application(QualIdentifier::Identifier(Identifier::Simple(Symbol("/"))), [t1, t2]) => {
-                            let mut num = BigInt::from(1);
-                            let mut den = BigInt::from(1);
-                            match t1 {
-                                Term::SpecConstant(SpecConstant::Numeral(numeral)) => {
-                                    let n = numeral.into_u128().map_err(|_| SmtEvalError::EvalError)?;
-                                    num *= BigInt::from(n);
-                                },
-                                Term::SpecConstant(SpecConstant::Decimal(Decimal(d_str))) => {
-                                    if let Some((n, d)) = from_str_to_num_den(d_str) {
-                                        num *= n;
-                                        den *= d;
-                                    } else {
-                                        return Err(SmtEvalError::EvalError);
-                                    }
-                                },
-                                _ => {
-                                    return Err(SmtEvalError::EvalError);
-                                },
-                            }
-                            match t2 {
-                                Term::SpecConstant(SpecConstant::Numeral(numeral)) => {
-                                    let n = numeral.into_u128().map_err(|_| SmtEvalError::EvalError)?;
-                                    den *= BigInt::from(n);
-                                },
-                                Term::SpecConstant(SpecConstant::Decimal(Decimal(d_str))) => {
-                                    if let Some((n, d)) = from_str_to_num_den(d_str) {
-                                        den *= n;
-                                        num *= d;
-                                    } else {
-                                        return Err(SmtEvalError::EvalError);
-                                    }
-                                },
-                                _ => {
-                                    return Err(SmtEvalError::EvalError);
-                                },
-                            }
-                            Ok(BigRational::new(num, den))
-                        }
-                        _ => Err(SmtEvalError::EvalError),
-                    },
-                    None => Err(SmtEvalError::EvalError),
-                }
-            },
+            Ok(BigRational::new(numerator, denominator))
         }
-        
     }
 }