3ca5a8d21a
Z3 expression translator fixes: - implies(x, y) now preserves both arguments (was dropping both → (=> true true)) - Multi-level field access m.price.amount → m_price_amount (was m_price.(>= amount 0)) - len() now handled same as length() (was left as bare len()) - nil/null translated to speckl_nil sentinel constant - != now properly converts to (distinct X Y) via convertToPrefix (was bare 'distinct') - Added 'distinct' as binary operator in convertToPrefix - speckl_nil declared as Int constant in output All 8 product spec constraints now produce valid SMT-LIB2. 57/57 tests pass.
16 lines
469 B
JavaScript
16 lines
469 B
JavaScript
import { parseSpeckFile } from './dist/parser.js';
|
|
import fs from 'fs';
|
|
|
|
const ast = parseSpeckFile('/home/sscoble/speckl/examples/Raft.speck');
|
|
for (const speck of ast.specks) {
|
|
for (const m of speck.members) {
|
|
if (m.type === 'action') {
|
|
for (const s of (m.statements || [])) {
|
|
if (s.type === 'ifblock') {
|
|
console.log('--- ifblock in', m.name, '---');
|
|
console.log('raw:', s.raw.substring(0, 200));
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|