Merge pull request #28 from elsoroka/dev

fix all the docs build issues?

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],

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
 ```
 

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)