Basic Tutorial

Because this module can be somewhat daunting at times, here is a (hopefully) comprehensible tutorial of all that it has to offer.

If this still isn’t enough, or it’s missing something, let me know. Until then, you could read through the Examples using the Pyidp3 API to see if it’s covered there. And if it isn’t, check out the The Pyidp3 API reference.

Requirements

IDP:

The IDP system needs to be installed somewhere on your system. To do this, go to this link, and download the offline version.

Open it using a filemanager or by using the “tar” command in terminal.

tar -xf ipd-version-tar.gz

This will extract the files from the tarball archive.

You can move the idp folder to anywhere you like, as long as the permissions are correct. I usually place my personal installation in my $HOME folder.

Pyidp3: Next up we need the Pyidp3 module. This can be done easily by using the following command:

python3 pip install pyidp3

If you used this command, proceed to the next step.

You could also download the sourcecode over at gitlab and clone it to your machine.

Next, you can run

python3 setup.py install

to install the package globally.

Tutorial

With the requirements done, let’s start simple: to begin programming using Pyidp3 you need to import it. This is done as such:

from pyidp3.typedIDP import IDP

As a user, all you need is this import. The IDP object is the most top-level object there is. It will allow you to do everything you need to do.

This is a list of what the IDP object offers:

  • Constant
  • Constraint
  • Define
  • Function
  • Predicate
  • Type
  • check_sat
  • minimize
  • model_expand

Say for instance, we’d like implement the following .idp file as a .py file, to be used in an application later. This example solves a simple letterpuzzle, where we try to assign values to each letter, so “AI + BA = CDE”. No two letters can have the same value, none of the letters can be zero and all vowels need to be an even number, all consonants uneven.

vocabulary V {
    type Decimal isa int
	A: Decimal
    B: Decimal
    C: Decimal
    I: Decimal
    D: Decimal
    E: Decimal
    
    Even(Decimal)
} 
structure S : V {
    Decimal = {0..9}
    Even = {0;2;4;6;8;}
}
theory T : V {
	A ~= B & A ~= C & A ~= I & A ~= D & A ~= E & B ~= C & B ~= I 
	& B ~= D & B ~= E & C ~= I & C ~= D & C ~= E & I ~= D & I ~= E 
	& D ~= E.
    
    A ~= 0.
    B ~= 0.
    C ~= 0.
    
    Even(A).
    Even(E).
    Even(I).
    
    ~Even(B).
    ~Even(C).
    ~Even(D).
    
    I + A + 10*A + 10*B = E + 10 * D + 100 * C.
}
procedure main() {	
    stdoptions.nbmodels = 3
    printmodels(modelexpand(T, S))	
}

First of all, we need to instantiate our IDP object. This can be done as follows:

idp = IDP('path/to/IDP/exec')

Make sure to set the path to your IDP executable, or it won’t work.

Next up, we’ll add the type Decimal.

idp.Type("Decimal", (0, 9))

Normally, when the Type uses the isa keyword, we’d have to explicitly tell this to the Type() method. But, by default Pyidp3 will find if it’s an int and add this automatically.

Now we should add the constants. This is also fairly easy:

idp.Constant("A: Decimal")
idp.Constant("B: Decimal")
idp.Constant("C: Decimal")
idp.Constant("I: Decimal")
idp.Constant("D: Decimal")
idp.Constant("E: Decimal")

Now for the Predicate Even, where we define what numbers are even.

idp.Predicate("Even(Decimal)", [0, 2, 4, 6, 8])

All that’s left now are the constraints in our theory. Because these are already in their IDP form, we need to set the last variable to True. These are also fairly easy to create, but take some time to type out:

# No two letters can be the same.
idp.Constraint("A ~= B & A ~= C & A ~= I & A ~= D & A ~= E & B ~= C & B ~= I
                & B ~= D & B ~= E & C ~= I & C ~= D & C ~= E & I ~= D & I ~= E
                & D ~= E.", True)

# No letter can be zero.
idp.Constraint("A ~= 0.", True)
idp.Constraint("B ~= 0.", True)
idp.Constraint("C ~= 0.", True)
idp.Constraint("I ~= 0.", True)
idp.Constraint("D ~= 0.", True)
idp.Constraint("E ~= 0.", True)

# Vowels have to be an even number.
idp.Constraint("Even(A).", True)
idp.Constraint("Even(E).", True)
idp.Constraint("Even(I).", True)

# Consonants have to be an uneven number.
idp.Constraint("~Even(B).", True)
idp.Constraint("~Even(C).", True)
idp.Constraint("~Even(D).", True)

# The formula to solve.
idp.Constraint("I + A + 10*A + 10*B = E + 10 * D + 100 * C.", True)
idp.Constraint("satisfiable()", True)

Note how we add satisfiable() as a constraint: otherwise IDP might return models that aren’t satisfiable. This has it’s applications, but for now we only want models that are satisfiable.

But say we’d like to extend this puzzle, with more letters and a harder to solve formula. This would be a pain, because for each n’th letter we’d have to add n-1 + 1 + 1 constraints. This is where the power of Pyidp3 (and Python) comes in. Because this is Python, we could also write something along the lines of:

idp.Type("Decimal", (0,9))
idp.Predicate("Even(Decimal)", [0, 2, 4, 6, 8])

even_letters = ['A', 'E', 'I']
uneven_letters = ['B', 'C', 'D']
letters = even_letters + uneven_letters
for i, letter in enumerate(letters):
    idp.Constant(letter+": Decimal")  # Define a type for every letter.

    for j, letter2 in enumerate(letters):  # Iterate over all the letters again
        if i < j and letter != letter2:  # No letters can have the same value
            idp.Constraint(letter + " ~= " + letter2)

    if letter in even_letters:
        idp.Constraint("Even(" + letter + ")")
    else:
        idp.Constraint("~Even(" + letter + ")")

    idp.Constraint(letter + " ~= 0")

idp.Constraint("I + A + 10*A + 10*B = E + 10 * D + 100 * C.", True)
idp.Constraint("satisfiable()", True)

Now if we want to add letters, all we need to do is append them to either the even_letters list or the uneven_letters list, and Pyidp3 will sort out the rest. In other words, our implementation is a lot more scalable than a direct implementation in IDP.

Last but not least, we still need to model expand! In the main block, stdoptions.nbmodels is set to three, after which it model expands. This can be done like so:

idp.nbmodels = 3
solutions = idp.model_expand()

print("Total amount of solutions:", len(solutions))
for i, sol in solutions:
    print("Solution {:d}".format(i), sol)

Every option in the IDP system can be used by giving a value to IDP.optionname. For a list of these options, see the usermanual. One thing to note however, is that all the verbosityoptions need to be used as IDP.verbosity_optionname.

When there are multiple solutions and a lot of data, it can sometimes be hard to see the difference between two solutions. To help remedy this, you could use the compare function in the IDP class. Although currently, this only works on functions.

This is just the tip of the iceberg, but currently I don’t have the time to add more to this tutorial. Luckily, there’s a whole bunch of examplefiles you can read and try to reverse-engineer from. These can be found here: Examples using the Pyidp3 API.