Add PrecompileTools workload

Project.toml

@@ -4,11 +4,13 @@ authors = ["Shashi Gowda <shashigowda91@gmail.com>"]
 version = "1.4.0"
 
 [deps]
+PrecompileTools = "aea7be01-6a6a-4083-8856-8a6e6704d82a"
 Symbolics = "0c5d862f-8b57-4792-8d23-62f2024744c7"
 SymbolicUtils = "d1185830-fcd6-423d-90d6-eec64667417b"
 Z3 = "06b161dc-0161-11ea-0f74-41f836f4024b"
 
 [compat]
+PrecompileTools = "1.2"
 Symbolics = "7"
 SymbolicUtils = "4.3"
 Z3 = "1.0"

src/SymbolicSMT.jl

@@ -6,6 +6,7 @@ import Symbolics
 using Symbolics: Num, unwrap, wrap, @variables
 import Z3
 using Z3: BoolVal, BoolVar, Context, Float64Val, IntVal, IntVar, Solver, add, check
+using PrecompileTools: @compile_workload, @setup_workload
 
 export Constraints, issatisfiable, isprovable, resolve, unsat_core
 # Re-export useful Symbolics.jl functionality
@@ -555,4 +556,15 @@ function resolve(expr::Num, cs::Constraints)
     return result isa Bool ? result : wrap(result)
 end
 
+@setup_workload begin
+    @variables x::Real
+    constraints = Constraints([x > 0])
+
+    @compile_workload begin
+        issatisfiable(x > 1, constraints)
+        isprovable(x > 0, constraints)
+        resolve(x > 1, constraints)
+    end
+end
+
 end # module

test/precompile_workload.jl

@@ -0,0 +1,10 @@
+using SymbolicSMT
+using Symbolics
+using Test
+
+@variables x::Real
+constraints = Constraints([x > 0])
+
+@test issatisfiable(x > 1, constraints)
+@test isprovable(x > 0, constraints)
+@test isequal(resolve(x > 1, constraints), x > 1)

test/runtests.jl

@@ -23,6 +23,9 @@ if GROUP == "All" || GROUP == "Core"
         @safetestset "Regression Tests" begin
             include("regression.jl")
         end
+        @safetestset "Precompile workload" begin
+            include("precompile_workload.jl")
+        end
         @safetestset "Unsat Core Tests" begin
             include("unsat_core.jl")
         end