import sys
from satispi import *
from example.program import *
from example.symabs import *

program = Program.from_file(sys.argv[1])
worklist = [State(program, 0, [], None)]
while worklist:
    state = worklist.pop(0)

    # Process state
    print("Processing state ...")
    exprs = [state.reg(reg) for reg in program.registers]
    types = ["(_ BitVec 32)" for _ in program.registers]
    cutoffs = [5 for _ in exprs]
    possible = symabs(state.smtlib, exprs, types, cutoffs)
    for reg, values in zip(program.registers, possible):
        print("\t", reg, "\t->\t", values)

    # Execute
    for next_state in state.step():
        if next_state.has_model():
            worklist.append(next_state)