So we need to override ==/!= on TrueClass, FalseClass, Float, Integer, Rational, etc.

This could cause performance issues, but the alternative is a lot of brokenness. Perhaps we need a bit of C to improve performance here.

This used to sort of work, but not in any consistent way.

My program brute forces all pythagorean triples for x+y+z=1..1000, which is not very fast. It seems running out of memory (or really anything that causes .check to return :unknown will also cause the solver to crash as satisfiability unknown, at around Bool<((x + y) + z) = 558>:

/home/unihedron/.rvm/gems/ruby-2.4.1/gems/z3-0.0.20181126/lib/z3/solver.rb:44:in `satisfiable?': Satisfiability unknown (Z3::Exception)

Re-running the program (but manually check for solver.check == :sat while trapping solver.check to print for debugging (and waiting another ~10 minutes (lol)) reveals that it does return :unknown sometimes (even if, that was put as the parameter to a new instance of running the program, and correctly returns when there's... more memory? idk)

I don't believe that it's necessary to throw an exception, and as the C API Z3_solver_check docs says:

The function Z3_solver_get_model retrieves a model if the assertions is satisfiable (i.e., the result is Z3_L_TRUE) and model construction is enabled. Note that if the call returns Z3_L_UNDEF, Z3 does not ensure that calls to Z3_solver_get_model succeed and any models produced in this case are not guaranteed to satisfy the assertions.

this implies, to me, that :unknown is a normal case and handling it should still be permitted normally (with undefined behaviour in mind) and treated as just false instead of throwing an exception, since the convention of method_name? methods just return a boolean.

(Now I have manually handled it with: when :unknown; puts "redoing..."; redo else by handling program flow based on the value of check myself.)

I think it should be made either 1. to be more obvious that the method can throw an exception, or 2. only to return booleans without throwing.

Looks like the Z3 API changed, hacking...

Here's my environment info

macOS 10.12.6

$ ruby --version
ruby 2.5.0p0 (2017-12-25 revision 61468) [x86_64-darwin16]

$ brew info z3
z3: stable 4.6.0 (bottled), HEAD
High-performance theorem prover
https://github.com/Z3Prover/z3
/usr/local/Cellar/z3/4.6.0 (92 files, 82.9MB) *
  Poured from bottle on 2018-02-03 at 12:17:16
From: https://github.com/Homebrew/homebrew-core/blob/master/Formula/z3.rb

Here's the output

[2] pry(main)> require_relative 'lib/z3'
FFI::NotFoundError: Function 'Z3_get_smtlib_assumption' not found in [libz3.dylib]
from /Users/lazzarello/.gem/ruby/2.5.0/gems/ffi-1.9.18/lib/ffi/library.rb:275:in `attach_function

Is the upstream header file z3_api.h the reference for function names?

I can't require z3 and don't know why

C:\Users\asus>irb
irb(main):001:0> require 'z3'

There is the log

Traceback (most recent call last):
15: from D:/Ruby26-x64/bin/irb.cmd:31:in <main>' 14: from D:/Ruby26-x64/bin/irb.cmd:31:in load'
13: from D:/Ruby26-x64/lib/ruby/gems/2.6.0/gems/irb-1.0.0/exe/irb:11:in <top (required)>' 12: from (irb):1 11: from D:/Ruby26-x64/lib/ruby/2.6.0/rubygems/core_ext/kernel_require.rb:34:in require'
10: from D:/Ruby26-x64/lib/ruby/2.6.0/rubygems/core_ext/kernel_require.rb:130:in rescue in require' 9: from D:/Ruby26-x64/lib/ruby/2.6.0/rubygems/core_ext/kernel_require.rb:130:in require'
8: from D:/Ruby26-x64/lib/ruby/gems/2.6.0/gems/z3-0.0.20181229/lib/z3.rb:5:in <top (required)>' 7: from D:/Ruby26-x64/lib/ruby/gems/2.6.0/gems/z3-0.0.20181229/lib/z3.rb:5:in require_relative'
6: from D:/Ruby26-x64/lib/ruby/gems/2.6.0/gems/z3-0.0.20181229/lib/z3/very_low_level.rb:4:in <top (required)>' 5: from D:/Ruby26-x64/lib/ruby/gems/2.6.0/gems/z3-0.0.20181229/lib/z3/very_low_level.rb:5:in module:Z3'
4: from D:/Ruby26-x64/lib/ruby/gems/2.6.0/gems/z3-0.0.20181229/lib/z3/very_low_level.rb:7:in <module:VeryLowLevel>' 3: from D:/Ruby26-x64/lib/ruby/gems/2.6.0/gems/ffi-1.12.2-x64-mingw32/lib/ffi/library.rb:99:in ffi_lib'
2: from D:/Ruby26-x64/lib/ruby/gems/2.6.0/gems/ffi-1.12.2-x64-mingw32/lib/ffi/library.rb:99:in map' 1: from D:/Ruby26-x64/lib/ruby/gems/2.6.0/gems/ffi-1.12.2-x64-mingw32/lib/ffi/library.rb:145:in block in ffi_lib'
)oadError (Could not open library 'z3': �Ҳ���ָ����ģ�顣

Specifications seems to want an archaic version of ffi. Is it intended or just not updated?

I have been doing Advent of Code in Ruby and most people used Z3 for Day 24 Part 2.

I found this gem and figured I'd give it a try, but had a difficult time figuring out how to use it due to the non-existent documentation. The only resource I could find online was a singular blog post detailing how someone used it for AoC 2022. If I hadn't found that blog post I would have had no way of using the library.

It would help tremendously to have some snippets detailing how to use this gem. Z3 is a very powerful tool and it's great that people are working to expose advanced math tooling to Ruby users. Thank you for putting the work in to build this gem! I don't want your hard work to go to waste, and I think this gem would benefit greatly from clear documentation on how to install the gem and interface with the API

Nice work! I was almost ready to wrap Z3 in Ruby bindings then found your project.

I got two errors when building.

Failures:

1. Z3::FloatExpr to_s
   Failure/Error: expect(float_double.from_const(1234 * 0.5**1040).to_s).to eq("1.205078125B-1030")

   expected: "1.205078125B-1030"
   got: "0.00470733642578125B-1022"

   (compared using ==)

   ./spec/float_expr_spec.rb:104:in `block (2 levels) in module:Z3'

2. Regexp Crossword Solver experienced-5.txt matches output
   Failure/Error: expect(s).to match Regexp.new(/\A(?:#{rx})\z/)

   expected "TOBKH" to match /\A(?:IT(BE|AD)\1)\z/
   Diff:
   @@ -1,2 +1,2 @@
   -/\A(?:IT(BE|AD)\1)\z/
   +"TOBKH"

   ./spec/integration/regexp_crossword_solver_spec.rb:23:in `block (5 levels) in <top (required)>'

   ./spec/integration/regexp_crossword_solver_spec.rb:22:in `each'

   ./spec/integration/regexp_crossword_solver_spec.rb:22:in `block (4 levels) in <top (required)>'

Environment:

Windows 10
ruby 3.0.2p107 (2021-07-07 revision 0db68f0233) [x64-mingw32]
library: Z3 version 4.8.17 - 32 bit
gem: z3 (0.0.20220320)

z3 installed from: https://github.com/Z3Prover/z3/releases/download/z3-4.8.17/z3-4.8.17-x86-win.zip

z3 installation folder content (Windows):

z3-4.8.17-x86-win\bin:
  com.microsoft.z3.jar
  libz3.dll
  libz3.lib
  libz3.pdb
  libz3java.dll
  libz3java.lib
  Microsoft.Z3.deps.json
  Microsoft.Z3.dll
  Microsoft.Z3.pdb
  Microsoft.Z3.xml
  msvcp140.dll
  msvcp140_1.dll
  msvcp140_2.dll
  msvcp140_atomic_wait.dll
  msvcp140_codecvt_ids.dll
  vcomp140.dll
  vcruntime140.dll
  z3.exe

Example used from Getting Started: https://dev.to/taw/100-languages-speedrun-episode-23-ruby-z3-19b9

Issue log:

C:/Ruby30-x64/lib/ruby/gems/3.0.0/gems/ffi-1.15.5-x64-mingw32/lib/ffi/library.rb:145:in `block in ffi_lib': 
Could not open library 'libz3.so.4.8': The specified module could not be found.\r (LoadError)
.
Could not open library 'libz3.so.4.8.dll': The specified module could not be found.\r
.
Could not open library 'libz3.so': The specified module could not be found.\r
.
Could not open library 'libz3.so.dll': The specified module could not be found.\r
.
Could not open library 'z3': The specified module could not be found.\r
.
Could not open library 'z3.dll': The specified module could not be found.\r
        from C:/Ruby30-x64/lib/ruby/gems/3.0.0/gems/ffi-1.15.5-x64-mingw32/lib/ffi/library.rb:99:in `map'
        from C:/Ruby30-x64/lib/ruby/gems/3.0.0/gems/ffi-1.15.5-x64-mingw32/lib/ffi/library.rb:99:in `ffi_lib'
        from C:/Ruby30-x64/lib/ruby/gems/3.0.0/gems/z3-0.0.20220320/lib/z3/very_low_level.rb:7:in `<module:VeryLowLevel>'
        from C:/Ruby30-x64/lib/ruby/gems/3.0.0/gems/z3-0.0.20220320/lib/z3/very_low_level.rb:5:in `<module:Z3>'
        from C:/Ruby30-x64/lib/ruby/gems/3.0.0/gems/z3-0.0.20220320/lib/z3/very_low_level.rb:4:in `<top (required)>'
        from C:/Ruby30-x64/lib/ruby/gems/3.0.0/gems/z3-0.0.20220320/lib/z3.rb:5:in `require_relative'
        from C:/Ruby30-x64/lib/ruby/gems/3.0.0/gems/z3-0.0.20220320/lib/z3.rb:5:in `<top (required)>'
        from <internal:C:/Ruby30-x64/lib/ruby/3.0.0/rubygems/core_ext/kernel_require.rb>:160:in `require'
        from <internal:C:/Ruby30-x64/lib/ruby/3.0.0/rubygems/core_ext/kernel_require.rb>:160:in `rescue in require'
        from <internal:C:/Ruby30-x64/lib/ruby/3.0.0/rubygems/core_ext/kernel_require.rb>:149:in `require'
        from solve.rb:3:in `<main>'
<internal:C:/Ruby30-x64/lib/ruby/3.0.0/rubygems/core_ext/kernel_require.rb>:85:in `require': cannot load such file -- z3 (LoadError)
        from <internal:C:/Ruby30-x64/lib/ruby/3.0.0/rubygems/core_ext/kernel_require.rb>:85:in `require'

Potential root cause identified in
c:\Ruby30-x64\lib\ruby\gems\3.0.0\gems\z3-0.0.20220320\lib\z3\very_low_level.rb
https://github.com/taw/z3/blob/master/lib/z3/very_low_level.rb#L7
ffi_lib ["libz3.so.4.8", "libz3.so", "z3"]

Issue could be solved by additional library name (compare with windows installation folder content above):
ffi_lib ["libz3.so.4.8", "libz3.so", "z3", "libz3"]

Is there a reason to have IntExpr#mod but not the operator equivalent?

Without it, we have the inconsistency that Integer does not support .mod while IntExpr does not support %, so you need to be careful of the order in which you put things when building expressions, which is a bit annoying.

Also, Ruby allows using % with non-integer numbers, I am not sure this is the case for Z3, but we can still add it to IntExpr anyway.

I can do a PR, but AFAICT it's barely more than adding an alias in int_expr.rb :)

It is possible to add a license file or header to this project to explain the terms in which it can be used? I'd love to be able to use this library at work, but without a license our legal team won't approve. For reference, this is what the Z3 library itself uses: https://github.com/Z3Prover/z3/blob/master/LICENSE.txt

z3 provides some api for simplifying expressions.

the python api allows for this

In [1]: from z3 import *

In [2]: x = Int('x')

In [3]: y = Int('y')

In [4]: print simplify(x < y + x + 2)
Not(y <= -2)

there's a LowLevel method in this ruby api for exposing simplification, but no way for the ast expression from the ast to be printed is available.

[1] pry(main)> require 'z3'
=> true
[2] pry(main)> x = Z3.Int('x')
=> Int<x>
[3] pry(main)> y = Z3.Int('y')
=> Int<y>
[4] pry(main)> Z3::LowLevel.simplify(x < y + x + 2)
=> #<FFI::Pointer address=0x007fa5644e4258>

def_API('Z3_simplify', AST, (_in(CONTEXT), _in(AST)))

is exposed in

      def simplify(ast) #=> :ast_pointer
        VeryLowLevel.Z3_simplify(_ctx_pointer, ast._ast)
      end

which is never called anywhere

(and VeryLowLevel.Z3_simplify is )

attach_function :Z3_simplify, [:ctx_pointer, :ast_pointer], :ast_pointer

this can be done through this (not supposed to be public) api

[1] pry(main)> require 'z3'
=> true
[2] pry(main)> x = Z3.Int('x')
=> Int<x>
[3] pry(main)> y = Z3.Int('y')
=> Int<y>
[5] pry(main)> ast = Z3::LowLevel.simplify(x < y + x + 2)
=> #<FFI::Pointer address=0x007fe7eb95c258>
[8] pry(main)> Z3::VeryLowLevel.Z3_ast_to_string(Z3::Context.instance._context, ast)
=> "(not (<= y (- 2)))"

but not as far as i can tell through a public one

s = Z3::FuncDecl.new((x < y + x + 2)._ast)
Z3::Exception: FuncDecls must have AST kind func decl

for example

If we have

a = Z3.Bool('a')
b = Z3.Bool('b')
c = Z3.Bool('c')
d = Z3.Bool('d')
e = Z3.Bool('e')
f = Z3.Bool('f')
g = Z3.Bool('g')
z = Z3.Bool('z')
solver.assert a
solver.assert Z3.And(Z3::Implies(a, Z3.And(b,c,z)))
solver.assert Z3::Implies(d,Z3.And(e, g))
solver.assert d == Z3.False
if solver.check
  model = solver.model
  model.each do |var, value|
    if value.to_b
      p var
    end
  end
end

I want to get installation dependency for a, which shall be only b,c,z, but it runs output as b,c,e,g,z.
Note, d depends on e,g, but d is not connected to a, which is just a noise.

The same codes of python z3 gets the wanted result

a, b, c, d, e, f, g, z = Bools('a b c d e f g z')
q1 = And([Implies(a, dep) for dep in [b, c, z]])
q2 = Implies(d, And(e, g))

s = Solver()
s.add(a, q1, q2)
if s.check() == sat:
    m = s.model()
    r = [x.name() for x in m if is_true(m[x])]
    print("Install a:")
    print(r)
else:
    print("Not installable")

I'm trying to solve https://projecteuler.net/problem=39 with this. Not exactly important, no need to click into the link if you can't be bothered. Here's my code (which finds pythagorean triples summing to 120) trying to understand the library which might demonstrate something interesting:

require 'z3'

z3=Z3::Solver.new
x=Z3.Int("x")
y=Z3.Int("y")
z=Z3.Int("z")
z3.assert Z3.And(*[x,y,z].map{|v|v > 0}, x<y, y<z)
z3.assert x**2+y**2==z**2
z3.assert x+y+z==120
z3.assert x>0
while z3.satisfiable?
vx=0
z3.model.each{|x,y|p "#{x}=#{y}"
vx=y.to_i if x=="x"}
z3.pop
z3.assert x>vx
end

The problem is that on vx=y.to_i if x=="x", the x here is apparently Int<x>, so trying to compare if it is the x variable without calling .to_s first will not work. I get:

/home/unihedron/.rvm/gems/ruby-2.4.1/gems/z3-0.0.20181126/lib/z3/expr/expr.rb:41:in `sort_for_const': No idea how to autoconvert `String': `"x"' (Z3::Exception)
	from /home/unihedron/.rvm/gems/ruby-2.4.1/gems/z3-0.0.20181126/lib/z3/expr/expr.rb:26:in `block in coerce_to_same_sort'
	from /home/unihedron/.rvm/gems/ruby-2.4.1/gems/z3-0.0.20181126/lib/z3/expr/expr.rb:26:in `map'
	from /home/unihedron/.rvm/gems/ruby-2.4.1/gems/z3-0.0.20181126/lib/z3/expr/expr.rb:26:in `coerce_to_same_sort'
	from /home/unihedron/.rvm/gems/ruby-2.4.1/gems/z3-0.0.20181126/lib/z3/expr/expr.rb:99:in `Eq'
	from /home/unihedron/.rvm/gems/ruby-2.4.1/gems/z3-0.0.20181126/lib/z3/expr/expr.rb:16:in `=='
	from 39.rb:14:in `block in <main>'
	from /home/unihedron/.rvm/gems/ruby-2.4.1/gems/z3-0.0.20181126/lib/z3/model.rb:49:in `block in each'
	from /home/unihedron/.rvm/gems/ruby-2.4.1/gems/z3-0.0.20181126/lib/z3/model.rb:45:in `each'
	from /home/unihedron/.rvm/gems/ruby-2.4.1/gems/z3-0.0.20181126/lib/z3/model.rb:45:in `each'
	from uniscript:13:in `<main>'

Recall that I have set x=Z3.Int("x"), so now my next attempt at fixing the loop:

z3.model.each{|k,v|p "#{k}=#{v}"
vx=v.to_i if k==x}

This kind of works, I get a different exception on the .pop line:

/home/unihedron/.rvm/gems/ruby-2.4.1/gems/z3-0.0.20181126/lib/z3/exception.rb:22:in `block in <module:Z3>': Z3 library failed with error Z3_IOB (Z3::Exception)
	from /home/unihedron/.rvm/gems/ruby-2.4.1/gems/z3-0.0.20181126/lib/z3/low_level_auto.rb:2017:in `Z3_solver_pop'
	from /home/unihedron/.rvm/gems/ruby-2.4.1/gems/z3-0.0.20181126/lib/z3/low_level_auto.rb:2017:in `solver_pop'
	from /home/unihedron/.rvm/gems/ruby-2.4.1/gems/z3-0.0.20181126/lib/z3/solver.rb:17:in `pop'
	from uniscript:15:in `<main>'

which I could fix afterwards, but the problem is k==x will always be truthy, because k (also x, now that I think about it) extending to == will always be some "comparable rule", which to the ruby engine is a truthy value.

Proposition: I would like a way to check the identity of an expr, something like Z3.ExprEq(x, y) which tells if x and y are the same expr, without resorting to something hacky like .eql? and trusting the same object is reused

(Note: the current best workaround is k.to_s=="x", which is not very intuitive or clean IMO)

I have been trying to use this gem to solve Advent of Code Day 24.

My friend implemented a solution using a Python Z3 library.

I translated that logic over to Ruby.

The above code seems to give the correct answer for the provided test input but with some caveats. I get a correct answer, but only if I feed Z3 only 3 out of the 5 possible "stones". If I feed all 5 stones into Z3, it cannot finish computing an answer in a reasonable amount of time. 4 stones doesn't work either.

When I switch to the actual input the gem seems unable to solve the system. This holds true even if I feed it only 3 stones. I tried changing which 3 stones I feed it and that doesn't seem to speed anything up. I don't understand how changing the input values would explode the time complexity, but I also don't understand how Z3 works in general.

I'm rather flummoxed tbh. My logic appears to mirror my friend's Python implementation. FWIW, he fed Python Z3 ~350 stones and got an answer in a reasonable amount of time. My ruby script has been running for 2+ hours with no end in sight.