make tests compatible with windows

test/bitvector_tests.jl

@@ -100,17 +100,17 @@ end
     @satvariable(a, BitVector, 8)
     @satvariable(b, BitVector, 8)
 
-    @test smt(concat(a, b, a), assert=false) == "(declare-fun a () (_ BitVec 8))
+    @test smt(concat(a, b, a), assert=false) ≈ "(declare-fun a () (_ BitVec 8))
 (declare-fun b () (_ BitVec 8))
 (define-fun concat_17d687cb15cd0d00 () (_ BitVec 24) (concat a b a))\n"
-    @test smt((a + b) << 0x2, assert=false) == "(declare-fun a () (_ BitVec 8))
+    @test smt((a + b) << 0x2, assert=false) ≈ "(declare-fun a () (_ BitVec 8))
 (declare-fun b () (_ BitVec 8))
 (define-fun bvshl_e76bba3dcff1a5b9 () (_ BitVec 8) (bvshl (bvadd a b) #x02))\n"
 
-    @test smt(0xff >= b) == "(declare-fun b () (_ BitVec 8))
+    @test smt(0xff >= b) ≈ "(declare-fun b () (_ BitVec 8))
 (assert (bvuge #xff b))\n"
 
-    @test smt(0xff == a) == "(declare-fun a () (_ BitVec 8))
+    @test smt(0xff == a) ≈ "(declare-fun a () (_ BitVec 8))
 (assert (= #xff a))\n"
 
 end
@@ -120,27 +120,27 @@ end
     @satvariable(b, BitVector, 8)
 
     @satvariable(c, Int)
-    @test smt(int2bv(c, 64), assert=false) == "(declare-fun c () Int)
+    @test smt(int2bv(c, 64), assert=false) ≈ "(declare-fun c () Int)
 (define-fun int2bv_1a6e7a9c3b2f1483 () (_ BitVec 64) ((_ int2bv 64) (as c Int)))\n"
 
-    @test smt(bv2int(b) < 1) == "(declare-fun b () (_ BitVec 8))
+    @test smt(bv2int(b) < 1) ≈ "(declare-fun b () (_ BitVec 8))
 (assert (< (bv2int b) 1))\n"
 
-    @test smt(a[1:8] == 0xff) == "(declare-fun a () (_ BitVec 8))
+    @test smt(a[1:8] == 0xff) ≈ "(declare-fun a () (_ BitVec 8))
 (assert (= ((_ extract 7 0) a) #xff))\n"
 
     @satvariable(x, BitVector, 8)
-    @test smt(repeat(x,2) == 0xff) == "(declare-fun x () (_ BitVec 8))
+    @test smt(repeat(x,2) == 0xff) ≈ "(declare-fun x () (_ BitVec 8))
 (assert (= (concat x x) #x00ff))\n"
 
-    @test smt(zero_extend(x,4) == 0x0) == "(declare-fun x () (_ BitVec 8))
+    @test smt(zero_extend(x,4) == 0x0) ≈ "(declare-fun x () (_ BitVec 8))
 (assert (= ((_ zero_extend 4) x) #x000))\n"
-    @test smt(sign_extend(x,4) == 0x0) == "(declare-fun x () (_ BitVec 8))
+    @test smt(sign_extend(x,4) == 0x0) ≈ "(declare-fun x () (_ BitVec 8))
 (assert (= ((_ sign_extend 4) x) #x000))\n"
 
-    @test smt(rotate_left(x,2) == 0x0) == "(declare-fun x () (_ BitVec 8))
+    @test smt(rotate_left(x,2) == 0x0) ≈ "(declare-fun x () (_ BitVec 8))
 (assert (= ((_ rotate_left 2) x) #x00))\n"
-    @test smt(rotate_right(x,2) == 0x0) == "(declare-fun x () (_ BitVec 8))
+    @test smt(rotate_right(x,2) == 0x0) ≈ "(declare-fun x () (_ BitVec 8))
 (assert (= ((_ rotate_right 2) x) #x00))\n"
 end
 

test/output_parse_tests.jl

@@ -86,7 +86,7 @@ end
     b = a
     @satvariable(a, Real)
     hashname = Satisfiability.__get_hash_name(:add, [b, a], is_commutative=true)
-    @test smt(b+a, assert=false) == "(declare-fun a () Real)
+    @test smt(b+a, assert=false) ≈ "(declare-fun a () Real)
 (declare-fun a () Int)
 (define-fun $hashname () Real (+ (as a Real) (to_real (as a Int))))
 "

test/runtests.jl

@@ -2,6 +2,10 @@ push!(LOAD_PATH, "../../src")
 push!(LOAD_PATH, "./")
 using Satisfiability
 using Test, Logging
+
+normalize_endings(s::String) = replace(s, "\r\n" => "\n")
+Base.isapprox(str1::String, str2::String) = normalize_endings(str1) == normalize_endings(str2)
+
 SET_DUPLICATE_NAME_WARNING!(false)
 CLEAR_VARNAMES!()
 

test/smt_representation_tests.jl

@@ -9,26 +9,26 @@ using Test
     @satvariable(ztensorbool[1:2,1:4,1:5], Bool)
     @satvariable(ztensorint[1:2,1:4,1:5], Int)
     @satvariable(ztensorreal[1:2,1:4,1:5], Real)
-    
+
     # indexed expression correctly declared
-    @test smt(z12[1,2]) == "(declare-fun z12_1_2 () Bool)\n(assert z12_1_2)\n"
+    @test smt(z12[1,2]) ≈ "(declare-fun z12_1_2 () Bool)\n(assert z12_1_2)\n"
     #1d and 2d expression, with and without assert
-    @test smt(z2) == "(declare-fun z2_1 () Bool)\n(assert z2_1)\n"
-    @test smt(z12, assert=false) == "(declare-fun z12_1_1 () Bool)\n(declare-fun z12_1_2 () Bool)\n"
+    @test smt(z2) ≈ "(declare-fun z2_1 () Bool)\n(assert z2_1)\n"
+    @test smt(z12, assert=false) ≈ "(declare-fun z12_1_1 () Bool)\n(declare-fun z12_1_2 () Bool)\n"
 
     # idea from https://microsoft.github.io/z3guide/docs/logic/propositional-logic
     # broadcast expression correctly generated
-    @test smt(β1 .∧ z2) == smt(z2, assert=false)*smt(β1, assert=false)*"(assert (and z2_1 $(Satisfiability.convert_to_ascii("β1"))))\n"
+    @test smt(β1 .∧ z2) ≈ smt(z2, assert=false)*smt(β1, assert=false)*"(assert (and z2_1 $(Satisfiability.convert_to_ascii("β1"))))\n"
 
     # indexing creates a 1d expression
-    @test smt(β1 ∧ z12[1,2]) == smt(z12[1,2], assert=false)*smt(β1, assert=false)*"(assert (and z12_1_2 $(Satisfiability.convert_to_ascii("β1"))))\n"
+    @test smt(β1 ∧ z12[1,2]) ≈ smt(z12[1,2], assert=false)*smt(β1, assert=false)*"(assert (and z12_1_2 $(Satisfiability.convert_to_ascii("β1"))))\n"
 
-    @test smt(z12[1,1] ∧ z12[1,2]) == smt(z12[1,1], assert=false)*smt(z12[1,2], assert=false)*"(assert (and z12_1_1 z12_1_2))\n"
+    @test smt(z12[1,1] ∧ z12[1,2]) ≈ smt(z12[1,1], assert=false)*smt(z12[1,2], assert=false)*"(assert (and z12_1_1 z12_1_2))\n"
 
     # broadcast and and or
-    @test smt(or(β1 .∨ z12)) == smt(z12, assert=false)*smt(β1, assert=false)*"(assert (or z12_1_1 z12_1_2 $(Satisfiability.convert_to_ascii("β1"))))\n"
+    @test smt(or(β1 .∨ z12)) ≈ smt(z12, assert=false)*smt(β1, assert=false)*"(assert (or z12_1_1 z12_1_2 $(Satisfiability.convert_to_ascii("β1"))))\n"
 
-    @test smt(and(β1 .∧ z12)) == smt(z12, assert=false)*smt(β1, assert=false)*"(assert (and z12_1_1 z12_1_2 $(Satisfiability.convert_to_ascii("β1"))))\n"
+    @test smt(and(β1 .∧ z12)) ≈ smt(z12, assert=false)*smt(β1, assert=false)*"(assert (and z12_1_1 z12_1_2 $(Satisfiability.convert_to_ascii("β1"))))\n"
 
 end
 
@@ -37,19 +37,19 @@ end
     @satvariable(z12[1:1, 1:2], Bool)
 
     # implies, also tests \r\n
-    @test smt(z1 ⟹ z12[1,2], line_ending="\r\n") == "(declare-fun z1 () Bool)\r\n(declare-fun z12_1_2 () Bool)\r\n(assert (=> z1 z12_1_2))\r\n"
+    @test smt(z1 ⟹ z12[1,2], line_ending="\r\n") ≈ "(declare-fun z1 () Bool)\r\n(declare-fun z12_1_2 () Bool)\r\n(assert (=> z1 z12_1_2))\r\n"
 
     # iff, also tests \r\n
-    @test smt(z1 ⟺ z12[1,2], line_ending="\r\n") == smt(z1, assert=false, line_ending="\r\n")*smt(z12[1,2], assert=false, line_ending="\r\n")*"(assert (= z1 z12_1_2))\r\n"
+    @test smt(z1 ⟺ z12[1,2], line_ending="\r\n") ≈ smt(z1, assert=false, line_ending="\r\n")*smt(z12[1,2], assert=false, line_ending="\r\n")*"(assert (= z1 z12_1_2))\r\n"
 
     # xor
-    @test smt(xor(z12[1,1], z12[1,2])) == smt(z12[1,1], assert=false)*smt(z12[1,2], assert=false)*"(assert (xor z12_1_1 z12_1_2))\n"
+    @test smt(xor(z12[1,1], z12[1,2])) ≈ smt(z12[1,1], assert=false)*smt(z12[1,2], assert=false)*"(assert (xor z12_1_1 z12_1_2))\n"
 
     # if-then-else
     @satvariable(x, Bool)
     @satvariable(y, Bool)
     @satvariable(z, Bool)
-    @test smt(ite(x,y,z)) == smt(x, assert=false)*smt(y, assert=false)*smt(z, assert=false)*"(assert (ite x y z))\n"
+    @test smt(ite(x,y,z)) ≈ smt(x, assert=false)*smt(y, assert=false)*smt(z, assert=false)*"(assert (ite x y z))\n"
 end
 
 @testset "Generate nested expr without duplications" begin
@@ -58,11 +58,11 @@ end
 
     xy = and(x,y)
     yx = and(y,x)
-    @test smt(or(xy, yx)) == smt(x, assert=false)*smt(y, assert=false)*"(assert (or (and x y)))\n"
+    @test smt(or(xy, yx)) ≈ smt(x, assert=false)*smt(y, assert=false)*"(assert (or (and x y)))\n"
 
     # Generate a nested expr with not (1-ary op) without duplicating statements
     nx = ¬x
-    @test smt(and(¬x, ¬x)) == smt(x, assert=false)*
+    @test smt(and(¬x, ¬x)) ≈ smt(x, assert=false)*
 "(assert (and (not x)))\n"
 end
 
@@ -72,7 +72,7 @@ end
 
     save(z1 .∧ z12, io=open("outfile.smt", "w"), check_sat=true)
     text = read(open("outfile.smt", "r"), String)
-    @test text == smt(z1 .∧ z12)*"(check-sat)\n"
+    @test text ≈ smt(z1 .∧ z12)*"(check-sat)\n"
     @satvariable(a, Int)
     @test_logs (:warn, "Top-level expression must be Boolean to produce a valid SMT program.") match_mode=:any save(a, io=open("outfile.smt", "w"), check_sat=true)
 end

test/solver_interface_tests.jl

@@ -155,15 +155,15 @@ end
     @satvariable(a, Int)
     @satvariable(b, Int)
     expr1 = a + b + 2
-    @test smt(expr1, assert=false) == "(declare-fun a () Int)
+    @test smt(expr1, assert=false) ≈ "(declare-fun a () Int)
 (declare-fun b () Int)
 (define-fun add_99dce5c325207b7 () Int (+ a b 2))\n"
 
     expr = and(expr1 <= a, b + 1 >= b)
     result = "(declare-fun b () Int)
 (declare-fun a () Int)
 (assert (and (>= (+ b 1) b) (<= (+ a b 2) a)))\n"
-    @test smt(expr) == result
+    @test smt(expr) ≈ result
 
     status = sat!(expr, solver=Z3(), logic="QF_LIA")
     @test status == :SAT

test/ufunc_tests.jl

@@ -7,10 +7,10 @@ CLEAR_VARNAMES!()
 @testset "Construct ufuncs" begin
     @satvariable(a, Int)
     @uninterpreted(p, Int, Bool)
-    @test smt(p(a), assert=false) == "(declare-fun p(Int) Bool)
+    @test smt(p(a), assert=false) ≈ "(declare-fun p(Int) Bool)
 (declare-fun a () Int)
 (define-fun p_a () Bool (p a))\n"
-  @test smt(p(a), assert=true) == "(declare-fun p(Int) Bool)
+  @test smt(p(a), assert=true) ≈ "(declare-fun p(Int) Bool)
 (declare-fun a () Int)
 (assert (p a))\n"
     @test isa(p(a), BoolExpr)
@@ -31,7 +31,7 @@ CLEAR_VARNAMES!()
     @test_throws MethodError q(1.5)
     @test_throws MethodError p(true)
 
-    @test smt(p(a), assert=false) == "(declare-fun p(Int) Bool)
+    @test smt(p(a), assert=false) ≈ "(declare-fun p(Int) Bool)
 (declare-fun a () Int)
 (define-fun p_a () Bool (p a))\n"
 
@@ -42,7 +42,7 @@ CLEAR_VARNAMES!()
     y0 = y[1:8]
     @uninterpreted(f, (BitVector, 32), (BitVector, 32))
     expr = f(x) == f(y)
-    @test smt(expr) == "(declare-fun f((_ BitVec 32)) (_ BitVec 32))
+    @test smt(expr) ≈ "(declare-fun f((_ BitVec 32)) (_ BitVec 32))
 (declare-fun x () (_ BitVec 32))
 (declare-fun y () (_ BitVec 32))
 (assert (= (f x) (f y)))\n"