CODEWITHSUNDEEP
z3z3py
redfast00
redfast00

Reputation: 1673

Z3: implementing "Model Checking Using SMT and Theory of Lists" solver hanging

I'm trying to implement some code from this paper: Model Checking Using SMT and Theory of Lists to prove facts about a simple machine. I wrote the following code using the Python Z3 API, mirroring the code described in the paper: the code and problem was intentionally simplified in order to show the problem better:

from z3 import *

MachineIntSort = BitVecSort(16)
MachineInt = lambda x: BitVec(x, 16)

def DeclareLinkedList(sort):
    LinkedList = Datatype(f'{sort.name()}_LinkedList')
    LinkedList.declare('nil')
    LinkedList.declare('cons', ('car', sort), ('cdr', LinkedList))
    return LinkedList.create()


State = Datatype('State')
State.declare('state',
    ('A', MachineIntSort),
    ('B', MachineIntSort),
    ('C', MachineIntSort),
    ('D', MachineIntSort))
State = State.create()

StateList = DeclareLinkedList(State)


def transition_condition(initial, next):
    return State.A(next) == State.A(initial) + 1

def final_condition(lst):
    return State.A(StateList.car(lst)) == 2

solver = Solver()
check_execution_trace = Function('check_execution_trace', StateList, BoolSort())
execution_list = Const('execution_list', StateList)


solver.add(ForAll(execution_list, check_execution_trace(execution_list) ==
    If(And(execution_list != StateList.nil, StateList.cdr(execution_list) != StateList.nil),
        And(
            transition_condition(StateList.car(execution_list), StateList.car(StateList.cdr(execution_list))),
            check_execution_trace(StateList.cdr(execution_list)),
            If(final_condition(StateList.cdr(execution_list)),
                StateList.nil == StateList.cdr(StateList.cdr(execution_list)),
                StateList.nil != StateList.cdr(StateList.cdr(execution_list))
            )
        ),
    True), # If False, unsat but incorrect. If True, it hangs
))

states = Const('states', StateList)

# Execution trace cannot be empty
solver.add(StateList.nil != states)

# Initial condition
solver.add(State.A(StateList.car(states)) == 0)

# Transition axiom
solver.add(check_execution_trace(states))

print(solver.check())
print(solver.model())

The problem is that model step hangs instead of giving the (trivial) solution. I think I might not have implemented everything the paper describes: I don't understand what "Finally, it is important to stress the purpose of the instantiation pattern ( PAT: {check tr (lst)} ) in the FORALL clause. This axiom states something about all lists. However, it would be impossible for the SMT solver to try to prove that the statement indeed holds for all possible lists. Instead, the common approach is to provide an instantiation pattern to basically say in which cases the axiom should be instantiated and therefore enforced by the solver." means, so I didn't implement it.

My goal now is not to have pretty code (I know the star-import is ugly, ...) but to have working code.

Upvotes: 1

Views: 631

Answers (1)

alias
alias

Reputation: 30428

Quantified formulas are hard for SMT solvers to deal with, as they make the logic semi-decidable. SMT solvers usually rely on "heuristics" to deal with such problems. Patterns are one way to "help" those heuristics to converge faster, when dealing with quantifiers.

You might want to read Section 13.2 of http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.225.8231&rep=rep1&type=pdf

To see an example of how to add patterns in the z3py bindings, look at this page: https://ericpony.github.io/z3py-tutorial/advanced-examples.htm (Search for "Patterns" when the page comes up.)

Upvotes: 4

Related Questions