@@ -181,8 +181,8 @@ fn test_floating_point_bits() {
181
181
assert ! ( sig64 == Some ( 53 ) ) ;
182
182
assert ! ( exp128 == Some ( 15 ) ) ;
183
183
assert ! ( sig128 == Some ( 113 ) ) ;
184
- assert ! ( expi == None ) ;
185
- assert ! ( sigi == None ) ;
184
+ assert ! ( expi. is_none ( ) ) ;
185
+ assert ! ( sigi. is_none ( ) ) ;
186
186
}
187
187
188
188
#[ test]
@@ -361,7 +361,7 @@ fn test_float_add() {
361
361
362
362
let x = ast:: Float :: new_const_float32 ( & ctx, "x" ) ;
363
363
let x_plus_one = ast:: Float :: round_towards_zero ( & ctx) . add ( & x, & ast:: Float :: from_f32 ( & ctx, 1.0 ) ) ;
364
- let y = ast:: Float :: from_f32 ( & ctx, 3.14 ) ;
364
+ let y = ast:: Float :: from_f32 ( & ctx, std :: f32 :: consts :: PI ) ;
365
365
366
366
solver. assert ( & x_plus_one. _eq ( & y) ) ;
367
367
assert_eq ! ( solver. check( ) , SatResult :: Sat ) ;
@@ -994,12 +994,12 @@ fn test_goal_is_inconsistent() {
994
994
let false_bool = ast:: Bool :: from_bool ( & ctx, false ) ;
995
995
let goal = Goal :: new ( & ctx, false , false , false ) ;
996
996
goal. assert ( & false_bool) ;
997
- assert_eq ! ( goal. is_inconsistent( ) , true ) ;
997
+ assert ! ( goal. is_inconsistent( ) ) ;
998
998
999
999
let true_bool = ast:: Bool :: from_bool ( & ctx, true ) ;
1000
1000
let goal = Goal :: new ( & ctx, false , false , false ) ;
1001
1001
goal. assert ( & true_bool) ;
1002
- assert_eq ! ( goal. is_inconsistent( ) , false ) ;
1002
+ assert ! ( ! goal. is_inconsistent( ) ) ;
1003
1003
}
1004
1004
1005
1005
#[ test]
@@ -1010,14 +1010,14 @@ fn test_goal_is_sat() {
1010
1010
let false_bool = ast:: Bool :: from_bool ( & ctx, false ) ;
1011
1011
let goal = Goal :: new ( & ctx, false , false , false ) ;
1012
1012
goal. assert ( & false_bool) ;
1013
- assert_eq ! ( goal. is_decided_sat( ) , false ) ;
1014
- assert_eq ! ( goal. is_decided_unsat( ) , true ) ;
1013
+ assert ! ( ! goal. is_decided_sat( ) ) ;
1014
+ assert ! ( goal. is_decided_unsat( ) ) ;
1015
1015
1016
1016
let true_bool = ast:: Bool :: from_bool ( & ctx, true ) ;
1017
1017
let goal = Goal :: new ( & ctx, false , false , false ) ;
1018
1018
goal. assert ( & true_bool) ;
1019
- assert_eq ! ( goal. is_decided_unsat( ) , false ) ;
1020
- assert_eq ! ( goal. is_decided_sat( ) , true ) ;
1019
+ assert ! ( ! goal. is_decided_unsat( ) ) ;
1020
+ assert ! ( goal. is_decided_sat( ) ) ;
1021
1021
}
1022
1022
1023
1023
#[ test]
@@ -1255,10 +1255,10 @@ fn test_goal_apply_tactic() {
1255
1255
after_formulas : Vec < Bool > ,
1256
1256
) {
1257
1257
assert_eq ! ( goal. get_formulas:: <Bool >( ) , before_formulas) ;
1258
- let params = Params :: new ( & ctx) ;
1258
+ let params = Params :: new ( ctx) ;
1259
1259
1260
- let tactic = Tactic :: new ( & ctx, "sat-preprocess" ) ;
1261
- let repeat_tactic = Tactic :: repeat ( & ctx, & tactic, 100 ) ;
1260
+ let tactic = Tactic :: new ( ctx, "sat-preprocess" ) ;
1261
+ let repeat_tactic = Tactic :: repeat ( ctx, & tactic, 100 ) ;
1262
1262
let apply_results = repeat_tactic. apply ( & goal, Some ( & params) ) ;
1263
1263
let goal_results = apply_results
1264
1264
. unwrap ( )
@@ -1525,11 +1525,11 @@ fn test_ast_safe_decl() {
1525
1525
let x_not = x. not ( ) ;
1526
1526
assert_eq ! ( x_not. safe_decl( ) . unwrap( ) . kind( ) , DeclKind :: NOT ) ;
1527
1527
1528
- let f = FuncDecl :: new ( & ctx, "f" , & [ & Sort :: int ( & ctx) ] , & Sort :: int ( ctx) ) ;
1529
- let x = ast:: Int :: new_const ( & ctx, "x" ) ;
1528
+ let f = FuncDecl :: new ( ctx, "f" , & [ & Sort :: int ( ctx) ] , & Sort :: int ( ctx) ) ;
1529
+ let x = ast:: Int :: new_const ( ctx, "x" ) ;
1530
1530
let f_x: ast:: Int = f. apply ( & [ & x] ) . try_into ( ) . unwrap ( ) ;
1531
- let f_x_pattern: Pattern = Pattern :: new ( & ctx, & [ & f_x] ) ;
1532
- let forall = ast:: forall_const ( & ctx, & [ & x] , & [ & f_x_pattern] , & x. _eq ( & f_x) ) ;
1531
+ let f_x_pattern: Pattern = Pattern :: new ( ctx, & [ & f_x] ) ;
1532
+ let forall = ast:: forall_const ( ctx, & [ & x] , & [ & f_x_pattern] , & x. _eq ( & f_x) ) ;
1533
1533
assert ! ( forall. safe_decl( ) . is_err( ) ) ;
1534
1534
assert_eq ! (
1535
1535
format!( "{}" , forall. safe_decl( ) . err( ) . unwrap( ) ) ,
@@ -1542,16 +1542,22 @@ fn test_ast_safe_decl() {
1542
1542
fn test_regex_capital_foobar_intersect_az_plus_is_unsat ( ) {
1543
1543
let cfg = Config :: new ( ) ;
1544
1544
let ctx = & Context :: new ( & cfg) ;
1545
- let solver = Solver :: new ( & ctx) ;
1545
+ let solver = Solver :: new ( ctx) ;
1546
1546
let s = ast:: String :: new_const ( ctx, "s" ) ;
1547
1547
1548
- let re = ast:: Regexp :: intersect ( ctx, & [
1549
- & ast:: Regexp :: concat ( ctx, & [
1550
- & ast:: Regexp :: literal ( ctx, "FOO" ) ,
1551
- & ast:: Regexp :: literal ( ctx, "bar" )
1552
- ] ) ,
1553
- & ast:: Regexp :: plus ( & ast:: Regexp :: range ( ctx, & 'a' , & 'z' ) )
1554
- ] ) ;
1548
+ let re = ast:: Regexp :: intersect (
1549
+ ctx,
1550
+ & [
1551
+ & ast:: Regexp :: concat (
1552
+ ctx,
1553
+ & [
1554
+ & ast:: Regexp :: literal ( ctx, "FOO" ) ,
1555
+ & ast:: Regexp :: literal ( ctx, "bar" ) ,
1556
+ ] ,
1557
+ ) ,
1558
+ & ast:: Regexp :: plus ( & ast:: Regexp :: range ( ctx, & 'a' , & 'z' ) ) ,
1559
+ ] ,
1560
+ ) ;
1555
1561
solver. assert ( & s. regex_matches ( & re) ) ;
1556
1562
assert ! ( solver. check( ) == SatResult :: Unsat ) ;
1557
1563
}
0 commit comments