Currently (model ...) declarations in ISLE are ignored. This PR implements processing for them, and replaces hard-coded types in add_isle_constraints with equivalent model declarations.
Tests pass:
mbm@m1p ~/D/v/v/c/i/v/veri_engine (mbm/use-models)> cargo test
...
running 182 tests
test test_broken_band_fits_in_32 ... ok
test test_broken_bor_fits_in_32 ... ok
test test_broken_cls_8 ... ok
...
test test_named_urem ... ok
test test_named_x64_to_amode_add_const_fold_iadd_lhs_rhs ... ok
test test_named_x64_to_amode_add_const_fold_iadd_rhs_rhs ... ok
test test_named_x64_to_amode_add_const_fold_iadd_lhs_lhs ... ok
test test_named_x64_to_amode_add_const_fold_iadd_rhs_lhs ... ok
test test_named_srem ... ok
test result: ok. 172 passed; 0 failed; 10 ignored; 0 measured; 0 filtered out; finished in 49.93s
...
Currently
(model ...)
declarations in ISLE are ignored. This PR implements processing for them, and replaces hard-coded types inadd_isle_constraints
with equivalent model declarations.Tests pass: