Advanced Problem Definition Techniques [WORK IN PROGRESS]¶
Using Theories¶
[1]:
import tarski
# 1. Create language equipped with the Arithmetic theory
bw = tarski.language(theories=['equality', 'arithmetic'])
# 2. Define sorts
place = bw.sort('place')
block = bw.sort('block', place)
# 3. Define functions
loc = bw.function( 'loc', block, place )
width = bw.function('width', block, bw.Real)
# 4. Define predicates
clear = bw.predicate( 'clear', block)
[2]:
b1, b2, b3, b4 = [ bw.constant( 'b_{}'.format(k), block) for k in (1,2,3,4) ]
[3]:
table = bw.constant('table', place)
[4]:
import tarski.model
import tarski.evaluators
s = tarski.model.create(bw)
s.evaluator = tarski.evaluators.get_entry_point('simple')
[5]:
s.set( loc(b1), table)
[6]:
s.set(loc(b2), table) # block b2 is on the table
s.set(loc(b3), b2) # block b3 is on block 2
s.set(width(b1), 3.0) # block b1 has a width of 3.0 units
s.set(width(b2), 3.0) # block b2 has a width of 3.0 units
s.set(width(b3), 4.0) # block b3 has a width of 4.0 units
Builtin Function Symbols¶
A number of functions are already defined for the builtin sorts Real
, Integer
and Natural
, in order to facilitate the definition of terms that model arithmetic operators, algebraic and transcendental functions
Name 
Syntax 
Notes 
Name 
Syntax 
Notes 

Addition 

Power 


Subtraction 


Multiplication 


Division 


Modulo 

Examples¶
We can write crazy stuff like:
[7]:
expr1 = width(b1) + width(b2)
[8]:
print(expr1)
+(width(b_1), width(b_2))
[9]:
expr2 = width(b1) * width(b2)
[10]:
print(expr2)
*(width(b_1), width(b_2))
and evaluate it with the \(\sigma\) operator, which is implemented by the eval
method of our language
[11]:
s[expr1]
[11]:
6.0 (Real)
[12]:
s[expr2]
[12]:
9.0 (Real)
Giving Meaning to Predicates¶
Tarski languages represent \(P^{\cal M}\) either extensionally, as tables of tuples of constants for which the predicate is defined, or intensionally as a procedure that maps a tuple of constants into either \(\top\) or \(\bot\).
We can add a new tuple of constants to the extension of predicate \(P\) using the method add
[13]:
my_blocks = [ b1, b2, b3, b4]
[14]:
for b in my_blocks :
s.add(clear, b)
Evaluating the satisfiability of a predicate \(P\) under a given interpretation of its arguments can be done via the satisifed
method
[15]:
print(s[clear(b1)])
True
[16]:
print(s[clear(b2)])
True
Relational operators like \(>\), \(=\) etc. are represented always procedurally when the sorts of the arguments are builtin sorts such as Real
.
NB: It may be interesting to highlight that predicates are actually constraints that we use to define states.
Formula evaluation¶
Example: Nested functions for compact preconditions¶
[17]:
looking_at = bw.function('looking_at', block)
s.set(looking_at(), b1)
precondition = (width(looking_at()) <= width(b2)) & (clear(b2))
s[precondition]
[17]:
True