In [1]:

    

from boole.elab.prelude import *
from boole.interfaces.z3_interface import *


    

In [2]:

    

Men, (Alex, Bill, Charles)= defenum('Men', ('Alex', 'Bill', 'Charles'))
         
Likes = (Men >> (Men >> Bool))('Likes')
x, y, z = Men('x y z')
    
s = Z3_Solver()
s.add(Likes(x, Bill))
print 'Check: ', s.check()
print 'Model: ', s.z3_model()


    

    




Check:  sat
Model:  [x = Alex, Likes = [(Alex, Bill) -> True, else -> True]]

In [3]:

    

x = Real('x')
p = x ** 2 + 1.01
q = 0.1 * x ** 3
print p
print q

s = Z3_Solver()
s.add(q > p)
print 'Check: ', s.check()
print 'Model: ', s.z3_model()


    

    




((x ** 2) + 1.01)
(0.1 × (x ** 3))
Check:  sat
Model:  [x = 11]

In [4]:

    

Men, (Alec, Bill, Carl, Dave) = \
    defenum('Men', ('Alec', 'Bill', 'Carl', 'Dave'))
tall, dark, handsome = (Men >> Int)('tall, dark, handsome')
ideal = Men('ideal')
x = Men('x')
    
s = Z3_Solver()
s.add(forall(x, Or(tall(x) == 0, tall(x) == 1)))
s.add(forall(x, Or(dark(x) == 0, dark(x) == 1)))
s.add(forall(x, Or(handsome(x) == 0, handsome(x) == 1)))
s.add(tall(Alec) + tall(Bill) + tall(Carl) + tall(Dave) == 3)
s.add(dark(Alec) + dark(Bill) + dark(Carl) + dark(Dave) == 2)
s.add(handsome(Alec) + handsome(Bill) + handsome(Carl) + handsome(Dave) == 1)
s.add(forall(x, Or(tall(x) == 1, dark(x) == 1, handsome(x) == 1)))
s.add(dark(Alec) == dark(Dave))   
s.add(tall(Bill) == tall(Carl))
s.add(tall(Carl) != tall(Dave))
s.add(And(tall(ideal) == 1, dark(ideal) == 1, handsome(ideal) == 1))
    
print 'Check:', s.check()
print 'Model: ', s.z3_model()


    

    




Check: sat
Model:  [ideal = Alec,
 tall = [Alec -> 1, Bill -> 1, Carl -> 1, else -> 0],
 dark = [Alec -> 1, Dave -> 1, else -> 0],
 handsome = [Bill -> 0, Carl -> 0, Dave -> 0, else -> 1]]

In [5]:

    

local_ctxt.show()


    

    




decls:

  Div_int : Div(Int, divide_int)
  Le : Π([X, pred], Bool)
  false : Bool
  Minus_real : Minus(Real, minus_real)
  divide_int : (Int) → (Int) → Int
  Add_int : Add(Int, add_int)
  Mul_int : Mul(Int, mul_int)
  <= : Π([X, pred, le_ev], (X) → (X) → Bool)
  Lt_real : Lt(Real, lt_real)
  uminus_real : (Real) → Real
  Add : Π([X, op], Bool)
  Abs : Π([X, uop], Bool)
  lt_int : (Int) → (Int) → Bool
  abs_int : (Int) → Int
  le_int : (Int) → (Int) → Bool
  Mul : Π([X, op], Bool)
  uminus_int : (Int) → Int
  divide_real : (Real) → (Real) → Real
  Abs_real : Abs(Real, abs_real)
  Real : Type
  minus_int : (Int) → (Int) → Int
  % : (Int) → (Int) → Int
  le_real : (Real) → (Real) → Bool
  + : Π([X, op, add_ev], (X) → (X) → X)
  * : Π([X, op, mul_ev], (X) → (X) → X)
  - : Π([X, op, minus_ev], (X) → (X) → X)
  int_sub_real : Int ≤ Real
  / : Π([X, op, div_ev], (X) → (X) → X)
  Or : (Bool) → (Bool) → Bool
  Uminus : Π([X, uop], Bool)
  Dave : Men
  abs : Π([X, uop, abs_ev], (X) → X)
  Lt_int : Lt(Int, lt_int)
  Abs_int : Abs(Int, abs_int)
  Carl : Men
  Not : (Bool) → Bool
  < : Π([X, pred, lt_ev], (X) → (X) → Bool)
  Div_real : Div(Real, divide_real)
  Minus_int : Minus(Int, minus_int)
  Alex : Men
  Le_real : Le(Real, lt_real)
  == : Π(X, (X) → (X) → Bool)
  Bill : Men
  Uminus_int : Uminus(Int, uminus_int)
  uminus : Π([X, uop, uminus_ev], (X) → X)
  ** : (Real) → (Real) → Real
  add_real : (Real) → (Real) → Real
  X : Type
  Div : Π([X, op], Bool)
  true : Bool
  Minus : Π([X, op], Bool)
  Alec : Men
  And : (Bool) → (Bool) → Bool
  Uminus_real : Uminus(Real, uminus_real)
  implies : (Bool) → (Bool) → Bool
  minus_real : (Real) → (Real) → Real
  Int : Type
  Charles : Men
  Lt : Π([X, pred], Bool)
  lt_real : (Real) → (Real) → Bool
  add_int : (Int) → (Int) → Int
  mul_int : (Int) → (Int) → Int
  Mul_real : Mul(Real, mul_real)
  Men : Type
  Add_real : Add(Real, add_real)
  Le_int : Le(Int, le_int)
  mul_real : (Real) → (Real) → Real
  abs_real : (Real) → Real

defs:

  Div_int : triv()
  Le : λ([X, pred], true)
  Minus_real : triv()
  Add_int : triv()
  <= : λ([X, pred, le_ev], pred)
  Lt_real : triv()
  Lt : λ([X, pred], true)
  Mul_int : triv()
  Mul : λ([X, op], true)
  Mul_real : triv()
  Abs_real : triv()
  Uminus_real : triv()
  + : λ([X, op, add_ev], op)
  * : λ([X, op, mul_ev], op)
  - : λ([X, op, minus_ev], op)
  / : λ([X, op, div_ev], op)
  Uminus : λ([X, uop], true)
  abs : λ([X, uop, abs_ev], uop)
  Lt_int : triv()
  Abs_int : triv()
  < : λ([X, pred, lt_ev], pred)
  Div_real : triv()
  Minus_int : triv()
  Le_real : triv()
  == : λ([X, x, y], And(Sub(x, y), Sub(y, x)))
  Uminus_int : triv()
  uminus : λ([X, uop, uminus_ev], uop)
  Div : λ([X, op], true)
  Minus : λ([X, op], true)
  implies : λ([p, q], Sub(p, q))
  Add : λ([X, op], true)
  Abs : λ([X, uop], true)
  Add_real : triv()
  Le_int : triv()

hyps:

  Div_real : Div(Real, divide_real)
  Div_int : Div(Int, divide_int)
  Minus_int : Minus(Int, minus_int)
  Minus_real : Minus(Real, minus_real)
  Le_real : Le(Real, lt_real)
  Add_int : Add(Int, add_int)
  Uminus_int : Uminus(Int, uminus_int)
  Lt_real : Lt(Real, lt_real)
  Uminus_real : Uminus(Real, uminus_real)
  int_sub_real : Int ≤ Real
  Lt_int : Lt(Int, lt_int)
  Abs_int : Abs(Int, abs_int)
  Add_real : Add(Real, add_real)
  Le_int : Le(Int, le_int)
  Mul_int : Mul(Int, mul_int)
  Mul_real : Mul(Real, mul_real)
  Abs_real : Abs(Real, abs_real)