From c04bf12aa18266f4b172d1650263b507d11da245 Mon Sep 17 00:00:00 2001 From: Emiko Soroka Date: Tue, 12 Dec 2023 17:26:05 -0800 Subject: [PATCH 1/2] fix all the docs build issues? --- docs/make.jl | 4 ++-- docs/src/functions.md | 17 +++++++++++++---- src/BitVectorExpr.jl | 2 +- 3 files changed, 16 insertions(+), 7 deletions(-) diff --git a/docs/make.jl b/docs/make.jl index 637fcb8..28ab182 100644 --- a/docs/make.jl +++ b/docs/make.jl @@ -7,10 +7,10 @@ using Satisfiability fmt = Documenter.Writers.HTMLWriter.HTML(edit_link="main") makedocs(sitename="Satisfiability.jl", -repo = "https://github.com/elsoroka/Satisfiability.jl/blob/{commit}{path}#L{line}", +repo = Documenter.Remotes.GitHub("elsoroka", "Satisfiability.jl"), clean=true, draft=false, -root="docs", +checkdocs=:none, source = "src", workdir=pwd(), modules = [Satisfiability], diff --git a/docs/src/functions.md b/docs/src/functions.md index 33b7ce2..5fa4f53 100644 --- a/docs/src/functions.md +++ b/docs/src/functions.md @@ -9,6 +9,14 @@ Use the `@satvariable` macro to define a variable. ```@docs @satvariable ``` +Satisfiability.jl currently supports propositional logic, integer and real-valued arithmetic, and bitvectors. Support for additional SMT-LIB theories is planned in future versions. +```@docs +BoolExpr(name::String) +IntExpr(name::String) +RealExpr(name::String) +BitVectorExpr(name::String, length::Int) +``` + An **uninterpreted function** is a function where the mapping between input and output is not known. The task of the SMT solver is then to determine a mapping such that some SMT expression holds true. ```@docs @uninterpreted @@ -41,8 +49,8 @@ Base.abs(a::IntExpr) Base.:+(a::IntExpr, b::IntExpr) Base.:-(a::IntExpr, b::IntExpr) Base.:*(a::RealExpr, b::RealExpr) -div(a::IntExpr, b::IntExpr) -mod(a::IntExpr, b::IntExpr) +Base.div(a::IntExpr, b::IntExpr) +Base.mod(a::IntExpr, b::IntExpr) Base.:/(a::RealExpr, b::RealExpr) ``` @@ -79,7 +87,7 @@ The SMT-LIB standard BitVector is often used to represent operations on fixed-si In addition to supporting the comparison operators above and arithmetic operators `+`, `-`, and `*`, the following BitVector-specific operators are available. Note that unsigned integer division is available using `div`. Signed division is `sdiv`. ```@docs -Base.div(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8}) +div(a::AbstractBitVectorExpr, b::AbstractBitVectorExpr) sdiv(a::BitVectorExpr{UInt8}, b::BitVectorExpr{UInt8}) ``` @@ -137,7 +145,8 @@ save(prob::BoolExpr) ## Solving a SAT problem ```@docs -sat!(prob::BoolExpr) +sat!(prob::Array{T}) where T <: BoolExpr +sat!(solver::InteractiveSolver) value(zs::Array{T}) where T <: AbstractExpr ``` diff --git a/src/BitVectorExpr.jl b/src/BitVectorExpr.jl index 96ad3ef..0401339 100644 --- a/src/BitVectorExpr.jl +++ b/src/BitVectorExpr.jl @@ -153,7 +153,7 @@ div(e1::AbstractBitVectorExpr, e2::AbstractBitVectorExpr) = __bvnop(div, :bvudiv Signed integer division of two BitVectors. """ -sdiv(e1::AbstractBitVectorExpr, e2::AbstractBitVectorExpr) = __bvnop(div, :bvsdiv, BitVectorExpr, [e1, e2]) +sdiv(e1::AbstractBitVectorExpr, e2::AbstractBitVectorExpr) = __bvnop(__signfix(div), :bvsdiv, BitVectorExpr, [e1, e2]) # unary minus, this is an arithmetic minus not a bit flip. -(e::BitVectorExpr) = __bv1op(e, -, :bvneg) From 1ec1319ce6d75583ec34e0de6f6f6cfba75acfb5 Mon Sep 17 00:00:00 2001 From: Emiko Soroka Date: Tue, 12 Dec 2023 17:32:19 -0800 Subject: [PATCH 2/2] we don't need to specify the repo --- docs/make.jl | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/make.jl b/docs/make.jl index 28ab182..ebe33a7 100644 --- a/docs/make.jl +++ b/docs/make.jl @@ -7,7 +7,7 @@ using Satisfiability fmt = Documenter.Writers.HTMLWriter.HTML(edit_link="main") makedocs(sitename="Satisfiability.jl", -repo = Documenter.Remotes.GitHub("elsoroka", "Satisfiability.jl"), +#repo = Documenter.Remotes.GitHub("elsoroka", "Satisfiability.jl"), clean=true, draft=false, checkdocs=:none,