Skip to content

Commit

Permalink
Merge pull request #62 from mykelk/windows_tests
Browse files Browse the repository at this point in the history
Make tests compatible with windows
  • Loading branch information
elsoroka authored Aug 4, 2024
2 parents e3596fc + ba11aab commit d7cf982
Show file tree
Hide file tree
Showing 6 changed files with 39 additions and 35 deletions.
24 changes: 12 additions & 12 deletions test/bitvector_tests.jl
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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

Expand Down
2 changes: 1 addition & 1 deletion test/output_parse_tests.jl
Original file line number Diff line number Diff line change
Expand Up @@ -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))))
"
Expand Down
4 changes: 4 additions & 0 deletions test/runtests.jl
Original file line number Diff line number Diff line change
Expand Up @@ -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!()

Expand Down
32 changes: 16 additions & 16 deletions test/smt_representation_tests.jl
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand All @@ -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
Expand All @@ -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

Expand All @@ -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
4 changes: 2 additions & 2 deletions test/solver_interface_tests.jl
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
8 changes: 4 additions & 4 deletions test/ufunc_tests.jl
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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"

Expand All @@ -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"
Expand Down

0 comments on commit d7cf982

Please sign in to comment.