From 8421b363a7c4dde5d5078eb789ed6793642ea1e1 Mon Sep 17 00:00:00 2001 From: Devin Jean Date: Fri, 26 Jul 2024 15:17:40 -0500 Subject: [PATCH] Real fn renames and Eq refactor Rename `_eq` to `eq` for consistency with `le`, `ge`, etc. Remove `PartialEq` and `Eq` from concrete `Ast` types to avoid accidental use. Add `ast_eq` to `Ast` to allow for explicit ast equality checks. Rename some `Real` methods involving fractions to "rational" instead of "real". Extend `Real::from_rational` (prev. `Real::from_real` to take `i64` for num/den). --- z3/src/ast.rs | 65 +++++++++------ z3/tests/lib.rs | 174 ++++++++++++++++++++++----------------- z3/tests/objectives.rs | 4 +- z3/tests/ops.rs | 35 ++++---- z3/tests/semver_tests.rs | 4 +- 5 files changed, 165 insertions(+), 117 deletions(-) diff --git a/z3/src/ast.rs b/z3/src/ast.rs index a52de25b..433bf245 100644 --- a/z3/src/ast.rs +++ b/z3/src/ast.rs @@ -2,7 +2,6 @@ use log::debug; use std::borrow::Borrow; -use std::cmp::{Eq, PartialEq}; use std::convert::{TryFrom, TryInto}; use std::ffi::{CStr, CString}; use std::fmt; @@ -189,6 +188,7 @@ macro_rules! varop { pub trait Ast<'ctx>: fmt::Debug { fn get_ctx(&self) -> &'ctx Context; fn get_z3_ast(&self) -> Z3_ast; + fn ast_eq(&self, other: &dyn Ast<'ctx>) -> bool; // This would be great, but gives error E0071 "expected struct, variant or union type, found Self" // so I don't think we can write a generic constructor like this. @@ -216,6 +216,14 @@ pub trait Ast<'ctx>: fmt::Debug { where Self: Sized; + #[deprecated = "Please use eq instead"] + fn _eq(&self, other: &Self) -> Bool<'ctx> + where + Self: Sized, + { + self.eq(other) + } + /// Compare this `Ast` with another `Ast`, and get a [`Bool`] /// representing the result. /// @@ -223,16 +231,24 @@ pub trait Ast<'ctx>: fmt::Debug { /// `Ast`s being compared must be the same type. // // Note that we can't use the binop! macro because of the `pub` keyword on it - fn _eq(&self, other: &Self) -> Bool<'ctx> + fn eq(&self, other: &Self) -> Bool<'ctx> + where + Self: Sized, + { + self.safe_eq(other).unwrap() + } + + #[deprecated = "Please use safe_eq instead"] + fn _safe_eq(&self, other: &Self) -> Result, SortDiffers<'ctx>> where Self: Sized, { - self._safe_eq(other).unwrap() + self.safe_eq(other) } /// Compare this `Ast` with another `Ast`, and get a Result. Errors if the sort does not /// match for the two values. - fn _safe_eq(&self, other: &Self) -> Result, SortDiffers<'ctx>> + fn safe_eq(&self, other: &Self) -> Result, SortDiffers<'ctx>> where Self: Sized, { @@ -442,6 +458,11 @@ macro_rules! impl_ast { fn get_z3_ast(&self) -> Z3_ast { self.z3_ast } + + fn ast_eq(&self, other: &dyn Ast<'ctx>) -> bool { + assert_eq!(self.ctx, other.get_ctx()); + unsafe { Z3_is_eq_ast(self.ctx.z3_ctx, self.z3_ast, other.get_z3_ast()) } + } } impl<'ctx> From<$ast<'ctx>> for Z3_ast { @@ -450,15 +471,6 @@ macro_rules! impl_ast { } } - impl<'ctx> PartialEq for $ast<'ctx> { - fn eq(&self, other: &$ast<'ctx>) -> bool { - assert_eq!(self.ctx, other.ctx); - unsafe { Z3_is_eq_ast(self.ctx.z3_ctx, self.z3_ast, other.z3_ast) } - } - } - - impl<'ctx> Eq for $ast<'ctx> {} - impl<'ctx> Clone for $ast<'ctx> { fn clone(&self) -> Self { debug!( @@ -579,10 +591,15 @@ impl<'ctx> Real<'ctx> { pub fn from_big_rational(ctx: &'ctx Context, value: &BigRational) -> Real<'ctx> { let num = value.numer(); let den = value.denom(); - Real::from_real_str(ctx, &num.to_str_radix(10), &den.to_str_radix(10)).unwrap() + Real::from_rational_str(ctx, &num.to_str_radix(10), &den.to_str_radix(10)).unwrap() } + #[deprecated = "Please use from_rational_str instead"] pub fn from_real_str(ctx: &'ctx Context, num: &str, den: &str) -> Option> { + Self::from_rational_str(ctx, num, den) + } + + pub fn from_rational_str(ctx: &'ctx Context, num: &str, den: &str) -> Option> { let sort = Sort::real(ctx); let ast = unsafe { let fraction_cstring = CString::new(format!("{num:} / {den:}")).unwrap(); @@ -906,19 +923,21 @@ impl<'ctx> Real<'ctx> { } } + #[deprecated = "Please use from_rational instead"] pub fn from_real(ctx: &'ctx Context, num: i32, den: i32) -> Real<'ctx> { - unsafe { - Self::wrap(ctx, { - Z3_mk_real( - ctx.z3_ctx, - num as ::std::os::raw::c_int, - den as ::std::os::raw::c_int, - ) - }) - } + Self::from_rational(ctx, num as i64, den as i64) } + pub fn from_rational(ctx: &'ctx Context, num: i64, den: i64) -> Real<'ctx> { + Real::from_rational_str(ctx, &num.to_string(), &den.to_string()).unwrap() + } + + #[deprecated = "Please use as_rational instead"] pub fn as_real(&self) -> Option<(i64, i64)> { + self.as_rational() + } + + pub fn as_rational(&self) -> Option<(i64, i64)> { unsafe { let mut num: i64 = 0; let mut den: i64 = 0; diff --git a/z3/tests/lib.rs b/z3/tests/lib.rs index 59b294e4..5ba03bf8 100644 --- a/z3/tests/lib.rs +++ b/z3/tests/lib.rs @@ -12,6 +12,13 @@ mod objectives; mod ops; mod semver_tests; +fn slice_ast_eq<'ctx, T: Ast<'ctx>>(a: &[T], b: &[T]) -> bool { + if a.len() != b.len() { + return false; + } + a.iter().zip(b.iter()).all(|(a, b)| a.ast_eq(b)) +} + #[test] fn test_config() { let _ = env_logger::try_init(); @@ -63,7 +70,7 @@ fn test_solving_for_model() { let solver = Solver::new(&ctx); solver.assert(&x.gt(&y)); solver.assert(&y.gt(&zero)); - solver.assert(&y.rem(&seven)._eq(&two)); + solver.assert(&y.rem(&seven).eq(&two)); let x_plus_two = ast::Int::add(&ctx, &[&x, &two]); solver.assert(&x_plus_two.gt(&seven)); assert_eq!(solver.check(), SatResult::Sat); @@ -92,7 +99,7 @@ fn test_solving_for_model_cloned() { let solver = Solver::new(&ctx); solver.assert(&x.gt(&y)); solver.assert(&y.gt(&zero)); - solver.assert(&y.rem(&seven)._eq(&two)); + solver.assert(&y.rem(&seven).eq(&two)); let x_plus_two = ast::Int::add(&ctx, &[&x, &two]); solver.assert(&x_plus_two.gt(&seven)); let cloned = solver.clone(); @@ -118,7 +125,7 @@ fn test_cloning_ast() { let zero = ast::Int::from_i64(&ctx, 0); let solver = Solver::new(&ctx); - solver.assert(&x._eq(&zero)); + solver.assert(&x.eq(&zero)); assert_eq!(solver.check(), SatResult::Sat); let model = solver.get_model().unwrap(); @@ -192,7 +199,7 @@ fn test_bitvector_from_str() { let b = ast::BV::from_str(&ctx, 129, "340282366920938463463374607431768211456").unwrap(); let solver = Solver::new(&ctx); - solver.assert(&a._eq(&b)); + solver.assert(&a.eq(&b)); assert_eq!(solver.check(), SatResult::Sat); let model = solver.get_model().unwrap(); @@ -239,10 +246,10 @@ fn test_ast_translate() { let translated_a = a.translate(&destination); let slv = Solver::new(&destination); - slv.assert(&translated_a._eq(&ast::Int::from_u64(&destination, 2))); + slv.assert(&translated_a.eq(&ast::Int::from_u64(&destination, 2))); assert_eq!(slv.check(), SatResult::Sat); - slv.assert(&translated_a._eq(&ast::Int::from_u64(&destination, 3))); + slv.assert(&translated_a.eq(&ast::Int::from_u64(&destination, 3))); assert_eq!(slv.check(), SatResult::Unsat); } @@ -269,7 +276,7 @@ fn test_solver_to_smtlib2() { let solver1 = Solver::new(&ctx); let t1 = ast::Bool::from_bool(&ctx, true); let t2 = ast::Bool::from_bool(&ctx, true); - solver1.assert(&t1._eq(&t2)); + solver1.assert(&t1.eq(&t2)); let s1_smt2 = solver1.to_smt2(); let solver2 = Solver::new(&ctx); solver2.from_string(s1_smt2); @@ -286,12 +293,12 @@ fn test_solver_translate() { let translated_a = a.translate(&destination); let slv = Solver::new(&destination); - slv.assert(&translated_a._eq(&ast::Int::from_u64(&destination, 2))); + slv.assert(&translated_a.eq(&ast::Int::from_u64(&destination, 2))); assert_eq!(slv.check(), SatResult::Sat); let translated_slv = slv.translate(&source); // Add a new constraint, make the old one unsatisfiable, while the copy remains satisfiable. - slv.assert(&translated_a._eq(&ast::Int::from_u64(&destination, 3))); + slv.assert(&translated_a.eq(&ast::Int::from_u64(&destination, 3))); assert_eq!(slv.check(), SatResult::Unsat); assert_eq!(translated_slv.check(), SatResult::Sat); } @@ -306,7 +313,7 @@ fn test_model_translate() { let translated_a = a.translate(&destination); let slv = Solver::new(&source); - slv.assert(&a._eq(&ast::Int::from_u64(&source, 2))); + slv.assert(&a.eq(&ast::Int::from_u64(&source, 2))); assert_eq!(slv.check(), SatResult::Sat); let model = slv.get_model().unwrap(); @@ -426,7 +433,7 @@ fn test_substitution() { let substitutions = &[(&y, &z)]; - assert!(x_plus_y.substitute(substitutions) == x_plus_z); + assert!(x_plus_y.substitute(substitutions).ast_eq(&x_plus_z)); } #[test] @@ -436,7 +443,7 @@ fn test_real_cmp() { let solver = Solver::new(&ctx); let x = ast::Real::new_const(&ctx, "x"); - let x_plus_1 = ast::Real::add(&ctx, &[&x, &ast::Real::from_real(&ctx, 1, 1)]); + let x_plus_1 = ast::Real::add(&ctx, &[&x, &ast::Real::from_rational(&ctx, 1, 1)]); // forall x, x < x + 1 let forall = ast::forall_const(&ctx, &[&x], &[], &x.lt(&x_plus_1)); @@ -463,7 +470,7 @@ fn test_float_add() { let x_plus_one = ast::Float::round_towards_zero(&ctx).add(&x, &ast::Float::from_f32(&ctx, 1.0)); let y = ast::Float::from_f32(&ctx, std::f32::consts::PI); - solver.assert(&x_plus_one._eq(&y)); + solver.assert(&x_plus_one.eq(&y)); assert_eq!(solver.check(), SatResult::Sat); } @@ -473,9 +480,10 @@ fn test_arbitrary_size_real() { let ctx = Context::new(&cfg); let solver = Solver::new(&ctx); - let x = ast::Real::from_real_str(&ctx, "99999999999999999999998", "99999999999999999999999") - .unwrap(); - let y = ast::Real::from_real(&ctx, 1, 1); + let x = + ast::Real::from_rational_str(&ctx, "99999999999999999999998", "99999999999999999999999") + .unwrap(); + let y = ast::Real::from_rational(&ctx, 1, 1); solver.assert(&x.lt(&y)); assert_eq!(solver.check(), SatResult::Sat); @@ -491,7 +499,7 @@ fn test_arbitrary_size_int() { let one = ast::Int::from_i64(&ctx, 1); let y = ast::Int::from_str(&ctx, "99999999999999999999999").unwrap(); - solver.assert(&ast::Int::add(&ctx, &[&x, &one])._eq(&y)); + solver.assert(&ast::Int::add(&ctx, &[&x, &one]).eq(&y)); assert_eq!(solver.check(), SatResult::Sat); } @@ -501,14 +509,15 @@ fn test_arbitrary_size_real_from_bigrational() { let ctx = Context::new(&cfg); let solver = Solver::new(&ctx); - let x = ast::Real::from_real_str(&ctx, "99999999999999999999998", "99999999999999999999999") - .unwrap(); + let x = + ast::Real::from_rational_str(&ctx, "99999999999999999999998", "99999999999999999999999") + .unwrap(); let num = BigInt::from_str("99999999999999999999998").unwrap(); let den = BigInt::from_str("99999999999999999999999").unwrap(); let ratio = BigRational::new(num, den); let y = ast::Real::from_big_rational(&ctx, &ratio); - solver.assert(&x._eq(&y)); + solver.assert(&x.eq(&y)); assert_eq!(solver.check(), SatResult::Sat); } @@ -525,7 +534,7 @@ fn test_arbitrary_size_int_from_bigint() { let num2 = BigInt::from_str("99999999999999999999999").unwrap(); let z = ast::Int::from_big_int(&ctx, &num2); - solver.assert(&ast::Int::add(&ctx, &[&x, &y])._eq(&z)); + solver.assert(&ast::Int::add(&ctx, &[&x, &y]).eq(&z)); assert_eq!(solver.check(), SatResult::Sat); } @@ -540,12 +549,12 @@ fn test_string_eq() { let z = ast::String::from_str(&ctx, "bar").unwrap(); let h = ast::String::new_const(&ctx, "h"); - solver.assert(&x._eq(&y)); - solver.assert(&x._eq(&z).not()); - solver.assert(&h._eq(&x)); + solver.assert(&x.eq(&y)); + solver.assert(&x.eq(&z).not()); + solver.assert(&h.eq(&x)); assert_eq!(solver.check(), SatResult::Sat); - solver.assert(&h._eq(&z)); + solver.assert(&h.eq(&z)); assert_eq!(solver.check(), SatResult::Unsat); } @@ -559,7 +568,7 @@ fn test_string_concat() { let y = ast::String::from_str(&ctx, "bar").unwrap(); let z = ast::String::from_str(&ctx, "foobar").unwrap(); - solver.assert(&ast::String::concat(&ctx, &[&x, &y])._eq(&z)); + solver.assert(&ast::String::concat(&ctx, &[&x, &y]).eq(&z)); assert_eq!(solver.check(), SatResult::Sat); } @@ -628,10 +637,10 @@ fn test_rec_func_def() { let solver = Solver::new(&ctx); - solver.assert(&x._eq(&fac.apply(&[&ast::Int::from_i64(&ctx, 4)]).as_int().unwrap())); - solver.assert(&y._eq(&ast::Int::mul(&ctx, &[&ast::Int::from_i64(&ctx, 5), &x]))); - solver.assert(&y._eq(&fac.apply(&[&ast::Int::from_i64(&ctx, 5)]).as_int().unwrap())); - solver.assert(&y._eq(&ast::Int::from_i64(&ctx, 120))); + solver.assert(&x.eq(&fac.apply(&[&ast::Int::from_i64(&ctx, 4)]).as_int().unwrap())); + solver.assert(&y.eq(&ast::Int::mul(&ctx, &[&ast::Int::from_i64(&ctx, 5), &x]))); + solver.assert(&y.eq(&fac.apply(&[&ast::Int::from_i64(&ctx, 5)]).as_int().unwrap())); + solver.assert(&y.eq(&ast::Int::from_i64(&ctx, 120))); assert_eq!(solver.check(), SatResult::Sat); } @@ -660,13 +669,13 @@ fn test_rec_func_def_unsat() { let solver = Solver::new(&ctx); - solver.assert(&x._eq(&fac.apply(&[&ast::Int::from_i64(&ctx, 4)]).as_int().unwrap())); - solver.assert(&y._eq(&ast::Int::mul(&ctx, &[&ast::Int::from_i64(&ctx, 5), &x]))); - solver.assert(&y._eq(&fac.apply(&[&ast::Int::from_i64(&ctx, 5)]).as_int().unwrap())); + solver.assert(&x.eq(&fac.apply(&[&ast::Int::from_i64(&ctx, 4)]).as_int().unwrap())); + solver.assert(&y.eq(&ast::Int::mul(&ctx, &[&ast::Int::from_i64(&ctx, 5), &x]))); + solver.assert(&y.eq(&fac.apply(&[&ast::Int::from_i64(&ctx, 5)]).as_int().unwrap())); // If fac was an uninterpreted function, this assertion would work. // To see this, comment out `fac.add_def(&[&n.into()], &body);` - solver.assert(&y._eq(&ast::Int::from_i64(&ctx, 25))); + solver.assert(&y.eq(&ast::Int::from_i64(&ctx, 25))); assert_eq!(solver.check(), SatResult::Unsat); } @@ -688,7 +697,7 @@ fn test_solver_unknown() { let y_cube = ast::Int::mul(&ctx, &[&y, &y, &y]); let z_cube = ast::Int::mul(&ctx, &[&z, &z, &z]); let sum_of_cubes = &ast::Int::add(&ctx, &[&x_cube, &y_cube, &z_cube]); - let sum_of_cubes_is_42 = sum_of_cubes._eq(&ast::Int::from_i64(&ctx, 42)); + let sum_of_cubes_is_42 = sum_of_cubes.eq(&ast::Int::from_i64(&ctx, 42)); let solver = Solver::new(&ctx); solver.assert(&sum_of_cubes_is_42); @@ -714,7 +723,7 @@ fn test_optimize_unknown() { let y_cube = ast::Int::mul(&ctx, &[&y, &y, &y]); let z_cube = ast::Int::mul(&ctx, &[&z, &z, &z]); let sum_of_cubes = &ast::Int::add(&ctx, &[&x_cube, &y_cube, &z_cube]); - let sum_of_cubes_is_42 = sum_of_cubes._eq(&ast::Int::from_i64(&ctx, 42)); + let sum_of_cubes_is_42 = sum_of_cubes.eq(&ast::Int::from_i64(&ctx, 42)); let optimize = Optimize::new(&ctx); optimize.assert(&sum_of_cubes_is_42); @@ -756,10 +765,10 @@ fn test_get_unsat_core() { let x = ast::Int::new_const(&ctx, "x"); let x_is_three = ast::Bool::new_const(&ctx, "x-is-three"); - solver.assert_and_track(&x._eq(&ast::Int::from_i64(&ctx, 3)), &x_is_three); + solver.assert_and_track(&x.eq(&ast::Int::from_i64(&ctx, 3)), &x_is_three); let x_is_five = ast::Bool::new_const(&ctx, "x-is-five"); - solver.assert_and_track(&x._eq(&ast::Int::from_i64(&ctx, 5)), &x_is_five); + solver.assert_and_track(&x.eq(&ast::Int::from_i64(&ctx, 5)), &x_is_five); assert!( solver.get_unsat_core().is_empty(), @@ -771,8 +780,8 @@ fn test_get_unsat_core() { let unsat_core = solver.get_unsat_core(); assert_eq!(unsat_core.len(), 2); - assert!(unsat_core.contains(&x_is_three)); - assert!(unsat_core.contains(&x_is_five)); + assert!(unsat_core.iter().any(|x| x.ast_eq(&x_is_three))); + assert!(unsat_core.iter().any(|x| x.ast_eq(&x_is_five))); } #[test] @@ -791,10 +800,10 @@ fn test_optimize_get_unsat_core() { let x = Int::new_const(&ctx, "x"); let x_is_three = Bool::new_const(&ctx, "x-is-three"); - optimize.assert_and_track(&x._eq(&Int::from_i64(&ctx, 3)), &x_is_three); + optimize.assert_and_track(&x.eq(&Int::from_i64(&ctx, 3)), &x_is_three); let x_is_five = Bool::new_const(&ctx, "x-is-five"); - optimize.assert_and_track(&x._eq(&Int::from_i64(&ctx, 5)), &x_is_five); + optimize.assert_and_track(&x.eq(&Int::from_i64(&ctx, 5)), &x_is_five); assert!( optimize.get_unsat_core().is_empty(), @@ -806,20 +815,20 @@ fn test_optimize_get_unsat_core() { let unsat_core = optimize.get_unsat_core(); assert_eq!(unsat_core.len(), 2); - assert!(unsat_core.contains(&x_is_three)); - assert!(unsat_core.contains(&x_is_five)); + assert!(unsat_core.iter().any(|x| x.ast_eq(&x_is_three))); + assert!(unsat_core.iter().any(|x| x.ast_eq(&x_is_five))); // try check API - let a = x._eq(&Int::from_i64(&ctx, 4)); - let b = x._eq(&Int::from_i64(&ctx, 6)); + let a = x.eq(&Int::from_i64(&ctx, 4)); + let b = x.eq(&Int::from_i64(&ctx, 6)); let result = optimize.check(&[a.clone(), b.clone()]); assert_eq!(result, SatResult::Unsat); let unsat_core = optimize.get_unsat_core(); assert_eq!(unsat_core.len(), 2); - assert!(unsat_core.contains(&a)); - assert!(unsat_core.contains(&b)); + assert!(unsat_core.iter().any(|x| x.ast_eq(&a))); + assert!(unsat_core.iter().any(|x| x.ast_eq(&b))); } #[test] @@ -874,7 +883,7 @@ fn test_datatype_builder() { .apply(&[&just_five]) .as_int() .unwrap(); - solver.assert(&five._eq(&five_two)); + solver.assert(&five.eq(&five_two)); assert_eq!(solver.check(), SatResult::Sat); } @@ -934,14 +943,14 @@ fn test_recursive_datatype() { .apply(&[&cons_five_nil]) .as_int() .unwrap(); - solver.assert(&car_cons_five_is_five._eq(&five)); + solver.assert(&car_cons_five_is_five.eq(&five)); assert_eq!(solver.check(), SatResult::Sat); let cdr_cons_five_is_nil = list_sort.variants[1].accessors[1] .apply(&[&cons_five_nil]) .as_datatype() .unwrap(); - solver.assert(&cdr_cons_five_is_nil._eq(&nil.as_datatype().unwrap())); + solver.assert(&cdr_cons_five_is_nil.eq(&nil.as_datatype().unwrap())); assert_eq!(solver.check(), SatResult::Sat); } @@ -990,7 +999,7 @@ fn test_mutually_recursive_datatype() { .apply(&[&leaf_ten]) .as_int() .unwrap(); - solver.assert(&leaf_ten_val_is_ten._eq(&ten.clone())); + solver.assert(&leaf_ten_val_is_ten.eq(&ten.clone())); assert_eq!(solver.check(), SatResult::Sat); let nil = tree_list_sort.variants[0].constructor.apply(&[]); @@ -1012,13 +1021,13 @@ fn test_mutually_recursive_datatype() { // n2 = Tree.node(TreeList.cons(n1, TreeList.nil)) let n2 = tree_sort.variants[1].constructor.apply(&[&n1_cons_nil]); - solver.assert(&n2._eq(&n1).not()); + solver.assert(&n2.eq(&n1).not()); // assert(TreeList.car(Tree.children(n2)) == n1) solver.assert( &tree_list_sort.variants[1].accessors[0] .apply(&[&tree_sort.variants[1].accessors[0].apply(&[&n2])]) - ._eq(&n1), + .eq(&n1), ); assert_eq!(solver.check(), SatResult::Sat); } @@ -1181,7 +1190,7 @@ fn test_set_membership() { let one = ast::Int::from_u64(&ctx, 1); solver.push(); - solver.assert(&set._eq(&ast::Set::empty(&ctx, &Sort::int(&ctx)))); + solver.assert(&set.eq(&ast::Set::empty(&ctx, &Sort::int(&ctx)))); solver.push(); solver.assert(&set.member(&one)); @@ -1212,7 +1221,7 @@ fn test_set_membership() { solver.push(); // A singleton set of 1 will contain 1 - solver.assert(&set._eq(&ast::Set::empty(&ctx, &Sort::int(&ctx)).add(&one))); + solver.assert(&set.eq(&ast::Set::empty(&ctx, &Sort::int(&ctx)).add(&one))); solver.assert(&set.member(&one)); assert_eq!(solver.check(), SatResult::Sat); solver.pop(1); @@ -1249,7 +1258,7 @@ fn test_array_store_select() { let set = ast::Array::new_const(&ctx, "integer_array", &Sort::int(&ctx), &Sort::int(&ctx)) .store(&zero, &one); - solver.assert(&set.select(&zero)._eq(&one.into()).not()); + solver.assert(&set.select(&zero).eq(&one.into()).not()); assert_eq!(solver.check(), SatResult::Unsat); } @@ -1265,7 +1274,15 @@ fn test_goal_get_formulas() { goal.assert(&a); goal.assert(&b); goal.assert(&c); - assert_eq!(goal.get_formulas::(), vec![a, b, c],); + let res = goal.get_formulas::(); + match res.as_slice() { + [ga, gb, gc] => { + assert!(ga.ast_eq(&a)); + assert!(gb.ast_eq(&b)); + assert!(gc.ast_eq(&c)); + } + x => panic!("{:?}", x), + } } #[test] @@ -1288,7 +1305,15 @@ fn test_tactic_skip() { .list_subgoals() .collect::>(); let goal_result = goal_results.first().unwrap(); - assert_eq!(goal_result.get_formulas::(), vec![a.clone(), b, a],); + let res = goal_result.get_formulas::(); + match res.as_slice() { + [ga, gb, gc] => { + assert!(ga.ast_eq(&a.clone())); + assert!(gb.ast_eq(&b)); + assert!(gc.ast_eq(&a)); + } + x => panic!("{:?}", x), + } } #[test] @@ -1353,7 +1378,7 @@ fn test_tactic_and_then() { .list_subgoals() .collect::>(); let goal_result = goal_results.first().unwrap(); - assert_eq!(goal_result.get_formulas::(), vec![a, b]); + assert!(slice_ast_eq(&goal_result.get_formulas::(), &[a, b])); } #[test] @@ -1378,7 +1403,7 @@ fn test_tactic_or_else() { .list_subgoals() .collect::>(); let goal_result = goal_results.first().unwrap(); - assert_eq!(goal_result.get_formulas::(), vec![a, b]); + assert!(slice_ast_eq(&goal_result.get_formulas::(), &[a, b])); } #[test] @@ -1392,7 +1417,7 @@ fn test_goal_apply_tactic() { before_formulas: Vec, after_formulas: Vec, ) { - assert_eq!(goal.get_formulas::(), before_formulas); + assert!(slice_ast_eq(&goal.get_formulas::(), &before_formulas)); let params = Params::new(ctx); let tactic = Tactic::new(ctx, "sat-preprocess"); @@ -1403,11 +1428,10 @@ fn test_goal_apply_tactic() { .list_subgoals() .collect::>(); let goal_result = goal_results.first().unwrap(); - assert_eq!( - goal_result.get_formulas::(), - after_formulas, - "Before: {before_formulas:?}" - ); + assert!(slice_ast_eq( + &goal_result.get_formulas::(), + &after_formulas + )); } let a = ast::Bool::new_const(&ctx, "a"); @@ -1647,7 +1671,7 @@ fn test_ast_safe_eq() { let sd: SortDiffers<'_> = SortDiffers::new(other_bool.get_sort(), other_string.get_sort()); - let result = x._safe_eq(&y); + let result = x.safe_eq(&y); assert!(result.is_err()); let err = result.err().unwrap(); assert_eq!(err.left(), sd.left()); @@ -1666,7 +1690,7 @@ fn test_ast_safe_decl() { let x = ast::Int::new_const(ctx, "x"); let f_x: ast::Int = f.apply(&[&x]).try_into().unwrap(); let f_x_pattern: Pattern = Pattern::new(ctx, &[&f_x]); - let forall = ast::forall_const(ctx, &[&x], &[&f_x_pattern], &x._eq(&f_x)); + let forall = ast::forall_const(ctx, &[&x], &[&f_x_pattern], &x.eq(&f_x)); assert!(forall.safe_decl().is_err()); assert_eq!( format!("{}", forall.safe_decl().err().unwrap()), @@ -1749,7 +1773,7 @@ fn test_array_example1() { let sel = aex.select(&Int::from_u64(ctx, 0)); - g.assert(&sel._eq(&BV::from_u64(ctx, 42, 32).into())); + g.assert(&sel.eq(&BV::from_u64(ctx, 42, 32).into())); let xc = Int::new_const(ctx, "x"); @@ -1757,7 +1781,7 @@ fn test_array_example1() { let fapp = fd.apply(&[&xc as &dyn Ast]); - g.assert(&Int::from_u64(ctx, 123)._eq(&xc.clone().add(&fapp.as_int().unwrap()))); + g.assert(&Int::from_u64(ctx, 123).eq(&xc.clone().add(&fapp.as_int().unwrap()))); let s = &Solver::new(ctx); for a in g.get_formulas() { @@ -1804,15 +1828,15 @@ fn return_number_args_in_given_entry() { let solver = Solver::new(ctx); solver.assert( &f.apply(&[&Int::from_u64(ctx, 0), &Int::from_u64(ctx, 1)]) - ._eq(&Int::from_u64(ctx, 10).into()), + .eq(&Int::from_u64(ctx, 10).into()), ); solver.assert( &f.apply(&[&Int::from_u64(ctx, 1), &Int::from_u64(ctx, 2)]) - ._eq(&Int::from_u64(ctx, 20).into()), + .eq(&Int::from_u64(ctx, 20).into()), ); solver.assert( &f.apply(&[&Int::from_u64(ctx, 1), &Int::from_u64(ctx, 0)]) - ._eq(&Int::from_u64(ctx, 10).into()), + .eq(&Int::from_u64(ctx, 10).into()), ); assert!(solver.check() == SatResult::Sat); @@ -1857,7 +1881,7 @@ fn iterate_all_solutions() { .map(|fd| { modifications.push( fd.apply(&[]) - ._eq(&model.get_const_interp(&fd.apply(&[])).unwrap()) + .eq(&model.get_const_interp(&fd.apply(&[])).unwrap()) .not(), ); format!( diff --git a/z3/tests/objectives.rs b/z3/tests/objectives.rs index 5644f2be..4dcb4de9 100644 --- a/z3/tests/objectives.rs +++ b/z3/tests/objectives.rs @@ -151,11 +151,11 @@ fn test_optimize_assert_soft_and_get_objectives() { } assert_eq!( - ite_children[1].as_real().unwrap().as_real().unwrap(), + ite_children[1].as_real().unwrap().as_rational().unwrap(), (0, 1) ); assert_eq!( - ite_children[2].as_real().unwrap().as_real().unwrap(), + ite_children[2].as_real().unwrap().as_rational().unwrap(), (1, 1) ); } diff --git a/z3/tests/ops.rs b/z3/tests/ops.rs index 2b1a12cd..05ccea54 100644 --- a/z3/tests/ops.rs +++ b/z3/tests/ops.rs @@ -188,7 +188,12 @@ fn test_bool_ops() { } fn assert_bool_child<'c>(node: &impl Ast<'c>, idx: usize, expected: &Bool<'c>) { - assert_eq!(&node.nth_child(idx).unwrap().as_bool().unwrap(), expected); + assert!(node + .nth_child(idx) + .unwrap() + .as_bool() + .unwrap() + .ast_eq(expected)); } #[test] @@ -198,13 +203,13 @@ fn test_ast_children() { let a = Bool::new_const(&ctx, "a"); assert_eq!(a.num_children(), 0); - assert_eq!(a.nth_child(0), None); - assert_eq!(a.children(), vec![]); + assert!(a.nth_child(0).is_none()); + assert!(a.children().is_empty()); let not_a = a.not(); assert_eq!(not_a.num_children(), 1); assert_bool_child(¬_a, 0, &a); - assert_eq!(not_a.nth_child(1), None); + assert!(not_a.nth_child(1).is_none()); let b = Bool::new_const(&ctx, "b"); // This is specifically testing for an array of values, not an array of slices @@ -212,11 +217,11 @@ fn test_ast_children() { assert_eq!(a_or_b.num_children(), 2); assert_bool_child(&a_or_b, 0, &a); assert_bool_child(&a_or_b, 1, &b); - assert_eq!(a_or_b.nth_child(2), None); + assert!(a_or_b.nth_child(2).is_none()); let children = a_or_b.children(); assert_eq!(children.len(), 2); - assert_eq!(children[0].as_bool().unwrap(), a); - assert_eq!(children[1].as_bool().unwrap(), b); + assert!(children[0].as_bool().unwrap().ast_eq(&a)); + assert!(children[1].as_bool().unwrap().ast_eq(&b)); let c = Bool::new_const(&ctx, "c"); let a_and_b_and_c = Bool::and(&ctx, &[&a, &b, &c]); @@ -224,11 +229,11 @@ fn test_ast_children() { assert_bool_child(&a_and_b_and_c, 0, &a); assert_bool_child(&a_and_b_and_c, 1, &b); assert_bool_child(&a_and_b_and_c, 2, &c); - assert_eq!(a_and_b_and_c.nth_child(3), None); + assert!(a_and_b_and_c.nth_child(3).is_none()); let children = a_and_b_and_c.children(); - assert_eq!(children[0].as_bool().unwrap(), a); - assert_eq!(children[1].as_bool().unwrap(), b); - assert_eq!(children[2].as_bool().unwrap(), c); + assert!(children[0].as_bool().unwrap().ast_eq(&a)); + assert!(children[1].as_bool().unwrap().ast_eq(&b)); + assert!(children[2].as_bool().unwrap().ast_eq(&c)); } fn assert_ast_attributes<'c, T: Ast<'c>>(expr: &T, is_const: bool) { @@ -302,15 +307,15 @@ fn test_real_approx() { let ctx = Context::new(&Config::default()); let x = Real::new_const(&ctx, "x"); let xx = &x * &x; - let zero = Real::from_real(&ctx, 0, 1); - let two = Real::from_real(&ctx, 2, 1); + let zero = Real::from_rational(&ctx, 0, 1); + let two = Real::from_rational(&ctx, 2, 1); let s = Solver::new(&ctx); s.assert(&x.ge(&zero)); - s.assert(&xx._eq(&two)); + s.assert(&xx.eq(&two)); assert_eq!(s.check(), SatResult::Sat); let m = s.get_model().unwrap(); let res = m.eval(&x, false).unwrap(); - assert_eq!(res.as_real(), None); // sqrt is irrational + assert_eq!(res.as_rational(), None); // sqrt is irrational println!("f64 res: {}", res.approx_f64()); assert!((res.approx_f64() - ::std::f64::consts::SQRT_2).abs() < 1e-20); assert_eq!(res.approx(0), "1."); diff --git a/z3/tests/semver_tests.rs b/z3/tests/semver_tests.rs index 4941e206..e038255d 100644 --- a/z3/tests/semver_tests.rs +++ b/z3/tests/semver_tests.rs @@ -222,7 +222,7 @@ fn test_solve_simple_semver_example() { ); opt.assert( &k_ast - ._eq(&ast::Int::from_u64(&ctx, n as u64)) + .eq(&ast::Int::from_u64(&ctx, n as u64)) .implies(&r_ast.ge(&ast::Int::from_u64(&ctx, low as u64))), ); } @@ -241,7 +241,7 @@ fn test_solve_simple_semver_example() { ); opt.assert( &k_ast - ._eq(&ast::Int::from_u64(&ctx, n as u64)) + .eq(&ast::Int::from_u64(&ctx, n as u64)) .implies(&r_ast.le(&ast::Int::from_u64(&ctx, high as u64))), ); }