module Z3

Constants

Re

A regular expression over some sequence sort - ‘Re(String)` for regexes over Strings, `Re(Seq(Int))` for regexes over sequences of Ints.

These are deliberately not Ruby Regexps, and nothing here converts between the two in either direction. Ruby’s regexes match unanchored, backtrack, and have backreferences and lookaround; Z3’s denote regular languages, match the whole sequence, and are closed under intersection and complement. Compiling one into the other would quietly change what a pattern means, so a Z3 regex is built out of the combinators here - or out of a String or a Seq, which ‘seq.to_re` turns into the regex matching exactly that one value and nothing else.

That last conversion is what makes ‘Z3::Re.Union(“cat”, “dog”)` work: anywhere a regex is expected, a Ruby String, a Ruby Array, a StringExpr or a SeqExpr means “the regex matching exactly this”. The one place it deliberately doesn’t happen is matches?, because that’s where Ruby’s reading and Z3’s differ.

‘==` comes from Expr and needs no help here, but it’s worth knowing what it means: Z3 decides it as *language equivalence*, not as sameness of terms, so ‘solver.prove! (a + b).star + a == a + (b + a).star` comes back proven. That’s the thing a backtracking regex engine can’t do at all.

Public Instance Methods

Add (*args)

Source

# File lib/z3/interface.rb, line 94
def Add(*args)
  Expr.Add(*args)
end

And (*args)

Source

# File lib/z3/interface.rb, line 106
def And(*args)
  BoolExpr.And(*args)
end

AtLeast (args, k)

Source

# File lib/z3/interface.rb, line 126
def AtLeast(args, k)
  BoolExpr.AtLeast(args, k)
end

AtMost (args, k)

Source

# File lib/z3/interface.rb, line 122
def AtMost(args, k)
  BoolExpr.AtMost(args, k)
end

Bitvec (v, n)

Source

# File lib/z3/interface.rb, line 17
def Bitvec(v, n)
  BitvecSort.new(n).var(v)
end

Bool (v)

Source

# File lib/z3/interface.rb, line 13
def Bool(v)
  BoolSort.new.var(v)
end

Const (v)

Source

# File lib/z3/interface.rb, line 36
def Const(v)
  Expr.sort_for_const(v).from_const(v)
end

Distinct (*args)

Source

# File lib/z3/interface.rb, line 86
def Distinct(*args)
  Expr.Distinct(*args)
end

Eq (*args)

Source

# File lib/z3/interface.rb, line 90
def Eq(*args)
  Expr.Eq(*args)
end

Exactly (args, k)

Source

# File lib/z3/interface.rb, line 130
def Exactly(args, k)
  BoolExpr.Exactly(args, k)
end

Exists (bound, body)

Source

# File lib/z3/interface.rb, line 74
def Exists(bound, body)
  Expr.Exists(bound, body)
end

False ()

Source

# File lib/z3/interface.rb, line 32
def False
  BoolSort.new.False
end

ForAll (bound, body)

Source

# File lib/z3/interface.rb, line 70
def ForAll(bound, body)
  Expr.ForAll(bound, body)
end

‘bound` is the variable, or variables, the quantifier binds - the very same ones the body was built out of, which Z3 rebinds inside it. Everywhere else they go on meaning what they always did.

Z3.ForAll(x, f[x] > 0)
Z3.Exists([x, y], f[x] == y)

A quantified problem is a different kind of problem: ‘Solver#check` can return `:unknown`, and on some inputs it doesn’t return at all - set ‘timeout` or `rlimit` on the solver if that matters.

FreshFunction (prefix, *sorts)

Source

# File lib/z3/interface.rb, line 52
def FreshFunction(prefix, *sorts)
  FuncDecl.declare_fresh(prefix, *sorts)
end

Same, but Z3 picks a name nothing has used yet by appending a number to ‘prefix` - for helper functions which shouldn’t collide with whatever the caller has named. The number comes from a counter shared by the whole context, so don’t count on getting any particular one.

Function (name, *sorts)

Source

# File lib/z3/interface.rb, line 44
def Function(name, *sorts)
  FuncDecl.declare(name, *sorts)
end

An uninterpreted function - a symbol the solver gets to decide the meaning of. The last sort is the range and the ones before it are the domain, the same order SMT-LIB’s ‘declare-fun` uses, so `Z3.Function(“f”, Int, Int, Bool)` is a two argument predicate. Apply it with `f[x, y]`.

IfThenElse (a,b,c)

Source

# File lib/z3/interface.rb, line 118
def IfThenElse(a,b,c)
  BoolExpr.IfThenElse(a,b,c)
end

Implies (a,b)

Source

# File lib/z3/interface.rb, line 114
def Implies(a,b)
  BoolExpr.Implies(a,b)
end

Int (v)

Source

# File lib/z3/interface.rb, line 5
def Int(v)
  IntSort.new.var(v)
end

Lambda (bound, body)

Source

# File lib/z3/interface.rb, line 79
def Lambda(bound, body)
  Expr.Lambda(bound, body)
end

An anonymous function, which comes back as an Array - ‘Z3.Lambda(x, x * 2)` is 6

Mul (*args)

Source

# File lib/z3/interface.rb, line 98
def Mul(*args)
  Expr.Mul(*args)
end

Or (*args)

Source

# File lib/z3/interface.rb, line 102
def Or(*args)
  BoolExpr.Or(*args)
end

Real (v)

Source

# File lib/z3/interface.rb, line 9
def Real(v)
  RealSort.new.var(v)
end

String (v)

Source

# File lib/z3/interface.rb, line 21
def String(v)
  StringSort.new.var(v)
end

True ()

Source

# File lib/z3/interface.rb, line 28
def True
  BoolSort.new.True
end

Xor (*args)

Source

# File lib/z3/interface.rb, line 110
def Xor(*args)
  Expr.Xor(*args)
end

set_param (k,v)

Source

# File lib/z3/interface.rb, line 145
def set_param(k,v)
  LowLevel.global_param_set(k,v)
end

version ()

Source

# File lib/z3/interface.rb, line 137
def version
  LowLevel.get_version.join(".")
end

version_at_least? (a, b=0, c=0, d=0)

Source

# File lib/z3/interface.rb, line 141
def version_at_least?(a, b=0, c=0, d=0)
  (LowLevel.get_version <=> [a, b, c, d]) >= 0
end