%{ #include #include "smt_lexer.h" %} %struct-type %define slot-name word struct keyword_s; %% *, SMT_TK_MUL +, SMT_TK_ADD -, SMT_TK_SUB /, SMT_TK_DIV :assumption, SMT_TK_ASSUMPTION :extrafuns, SMT_TK_EXTRAFUNS :extrapreds, SMT_TK_EXTRAPREDS :extrasorts, SMT_TK_EXTRASORTS :formula, SMT_TK_FORMULA :logic, SMT_TK_LOGIC :nopat, SMT_TK_NOPAT :notes, SMT_TK_NOTES :pat, SMT_TK_PAT :status, SMT_TK_STATUS <, SMT_TK_LT <=, SMT_TK_LE =, SMT_TK_EQ >, SMT_TK_GT >=, SMT_TK_GE Array, SMT_TK_ARRAY Array1, SMT_TK_ARRAY1 Array2, SMT_TK_ARRAY2 BitVec, SMT_TK_BITVEC Int, SMT_TK_INT Real, SMT_TK_REAL and, SMT_TK_AND benchmark, SMT_TK_BENCHMARK bit0, SMT_TK_BIT0 bit1, SMT_TK_BIT1 bvadd, SMT_TK_BVADD bvand, SMT_TK_BVAND bvashr, SMT_TK_BVASHR bvcomp, SMT_TK_BVCOMP bvgeq, SMT_TK_BVGEQ bvgt, SMT_TK_BVGT bvleq, SMT_TK_BVLEQ bvlshr, SMT_TK_BVLSHR bvlt, SMT_TK_BVLT bvmul, SMT_TK_BVMUL bvnand, SMT_TK_BVNAND bvneg, SMT_TK_BVNEG bvnor, SMT_TK_BVNOR bvnot, SMT_TK_BVNOT bvor, SMT_TK_BVOR bvredand, SMT_TK_BVREDAND bvredor, SMT_TK_BVREDOR bvsdiv, SMT_TK_BVSDIV bvsge, SMT_TK_BVSGE bvsgeq, SMT_TK_BVSGEQ bvsgt, SMT_TK_BVSGT bvshl, SMT_TK_BVSHL bvsle, SMT_TK_BVSLE bvsleq, SMT_TK_BVSLEQ bvslt, SMT_TK_BVSLT bvsmod, SMT_TK_BVSMOD bvsrem, SMT_TK_BVSREM bvsub, SMT_TK_BVSUB bvudiv, SMT_TK_BVUDIV bvuge, SMT_TK_BVUGE bvugt, SMT_TK_BVUGT bvule, SMT_TK_BVULE bvult, SMT_TK_BVULT bvurem, SMT_TK_BVUREM bvxnor, SMT_TK_BVXNOR bvxor, SMT_TK_BVXOR concat, SMT_TK_CONCAT distinct, SMT_TK_DISTINCT exists, SMT_TK_EXISTS extract, SMT_TK_EXTRACT false, SMT_TK_FALSE flet, SMT_TK_FLET forall, SMT_TK_FORALL if_then_else, SMT_TK_IF_THEN_ELSE iff, SMT_TK_IFF implies, SMT_TK_IMPLIES ite, SMT_TK_ITE let, SMT_TK_LET not, SMT_TK_NOT or, SMT_TK_OR repeat, SMT_TK_REPEAT rotate_left, SMT_TK_ROTATE_LEFT rotate_right, SMT_TK_ROTATE_RIGHT sat, SMT_TK_SAT select, SMT_TK_SELECT shift_left0, SMT_TK_SHIFT_LEFT0 shift_left1, SMT_TK_SHIFT_LEFT1 shift_right0, SMT_TK_SHIFT_RIGHT0 shift_right1, SMT_TK_SHIFT_RIGHT1 sign_extend, SMT_TK_SIGN_EXTEND store, SMT_TK_STORE true, SMT_TK_TRUE unknown, SMT_TK_UNKNOWN unsat, SMT_TK_UNSAT xor, SMT_TK_XOR zero_extend, SMT_TK_ZERO_EXTEND ~, SMT_TK_TILDE