CODEWITHSUNDEEP
z3python-3.5z3pysat
So S
So S

Reputation: 591

Z3-solver throws 'model is not available' exception on python 3

For solving a SAT-problem I decided to use the Z3-solver from Microsoft and Python 3. The aim is to take a long model (up to 500,000 features) and find all possible solutions. To find them I want to add the first solution S1 to the initial equation and exclude S1 it and so forth. I will do it using a while-loop. Solving a SAT-problem is important for me, because I wanna analyse feature models.

But I'm facing a problem with adding sth to the initial equation. I will share a minimal example:

# Import statements
import sys 
sys.path.insert(0,'/.../z3/bin')
from z3 import *        # https://github.com/Z3Prover/z3/wiki

def main():

    '''
    Solves after transformation a given boolean equation by using the Z3-Solver from Microsoft.
    '''

    fd = dict()
    fd['_r'] = Bool('_r')
    fd['_r_1'] = Bool('_r_1')

    equation = '''And(fd.get("_r"),Or(Not(fd.get("_r")),fd.get("_r_1")))'''

    # Solve the equation
    s = Solver()
    exec('s.add(' + equation + ')')
    s.check()
    print(s.model())

    ###################################
    # Successfull until here.
    ###################################

    s.add(Or(fd['_r'] != bool(s.model()[fd.get('_r')])))
    # s.add(Or(fd['_r'] != False))

    s.check()
    print(s.model())


if __name__=='__main__':
    main()

The first coded line after # Successfull... throws an z3types.Z3Exception: model is not available error. So i tried the line above adding simply false to the model. That works just fine.

I'm stucked here. I believe the error is easy to solve, but I don't see the solution. Does one of you? Thanks!

Upvotes: 0

Views: 1761

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

Models become available only after s.check() returns 'sat'. The model maps Boolean propositions to {True, False} and generally maps constants and functions to fixed values. The requirement is that the model provides an interpretation that satisfies the formula that is added to the solver 's'. We don't know whether the solver state is satisfiable before we have called 's.check()'.

Suppose you want to say:

s.add(Or(fd['_r'] != bool(s.model()[fd.get('_r')])))

meaning that in the model that satisfies the constraint should have the property that if '_r' is true under the model, then fd['_r'] != True, and if '_r' is false under the model, then fd['_r'] != False. This is equivalent to saying fd['_r'] != '_r'. So it isn't really necessary to access the value of '_r' in whatever model may evaluate '_r' in order to say something about the evaluation of it.

Upvotes: 2

Related Questions