Boolector: «квантификаторы с функциями, которые еще не поддерживаются» - PullRequest
Новая
       21

Boolector: «квантификаторы с функциями, которые еще не поддерживаются»

0 голосов
/ 30 апреля 2020

Я пытаюсь выполнить синтез asm с помощью Boolector / Python - (хотя я также был бы рад переписать это, чтобы использовать Z3).

Это тривиальный пример - есть набор регистров, и я просто хочу, чтобы он обнаружил, что "rs" должно быть 0.

Другими словами, для всех xx (param), Записать (iregs, rs, xx) приводит к regs [0] == xx.

Однако, это вызывает: 

pyboolector.BoolectorException: [pybtor] [btorcore] btor_check_sat: quantifiers with functions not supported yet

Я не уверен, как бы написать это в по-другому. 

#!/usr/bin/env python3

import sys
from pyboolector import *


b = Boolector()
b.Set_opt( BTOR_OPT_MODEL_GEN, 1 )

# reg selector - we have 4 regs
reg_sel_sort = b.BitVecSort( 2 )

# registers are 32-bit
reg_sort = b.BitVecSort( 32 )

# make a register set sort
reg_array_sort = b.ArraySort( reg_sel_sort, reg_sort )

# make a set of registers
iregs = b.Array( reg_array_sort, "iregs" )

# choose an index into the set
rs = b.Var( reg_sel_sort, "rs" )

# write a parameter's value into the chosen reg
xx = b.Param( reg_sort )
iregs = b.Write( iregs, rs, xx )

# read from iregs[ 0 ]
rr = b.Read( iregs, 0 )

# assert that iregs[ 0 ] == xx
fa = b.Forall( [ xx ], b.Eq( rr, xx ) )
b.Assert( fa )

# I was hoping this would just set rs=0 - but instead, it raises:
# pyboolector.BoolectorException: [pybtor] [btorcore] btor_check_sat: quantifiers with functions not supported yet
if( not b.Sat() ):
    print( "unsat" )
    sys.exit( 0 )

b.Print_model()

print( "done" )
...