/* * This file is part of the Yices SMT Solver. * Copyright (C) 2017 SRI International. * * Yices is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by * the Free Software Foundation, either version 3 of the License, or * (at your option) any later version. * * Yices is distributed in the hope that it will be useful, * but WITHOUT ANY WARRANTY; without even the implied warranty of * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the * GNU General Public License for more details. * * You should have received a copy of the GNU General Public License * along with Yices. If not, see . */ The SMT tokens are enum smt_token { // separators SMT_TK_LP, SMT_TK_RP, SMT_TK_LB, SMT_TK_RB, SMT_TK_COLON, SMT_TK_EOS, // strings, symbols, variables, attributes SMT_TK_STRING, SMT_TK_SYMBOL, SMT_TK_VAR, SMT_TK_FVAR, SMT_TK_ATTRIBUTE, SMT_TK_USER_VALUE, // numerals: more permissive than SMT LIB, we allow // rationals as or / // floats as . SMT_TK_RATIONAL, SMT_TK_FLOAT, // bitvector constants "bv" (size is determined by the theory (e.g., QF_UFBV[32]) // New bitvector theory: size is appended in the format "bv[i]" SMT_TK_BV_CONSTANT, // bitvector constants in binary "bvbin" and hexadecimal "bvhex" SMT_TK_BV_BINCONSTANT, SMT_TK_BV_HEXCONSTANT, // SMT-LIB keywords (independent of the logic and theories) SMT_TK_DISTINCT, SMT_TK_ITE, SMT_TK_EQ, SMT_TK_TRUE, SMT_TK_FALSE, SMT_TK_NOT, SMT_TK_IMPLIES, SMT_TK_IF_THEN_ELSE, SMT_TK_AND, SMT_TK_OR, SMT_TK_XOR, SMT_TK_IFF, SMT_TK_EXISTS, SMT_TK_FORALL, SMT_TK_LET, SMT_TK_FLET, // attribute for patterns SMT_TK_PAT, SMT_TK_NOPAT, // benchmark attributes and keywords SMT_TK_BENCHMARK, SMT_TK_SAT, SMT_TK_UNSAT, SMT_TK_UNKNOWN, SMT_TK_LOGIC, SMT_TK_ASSUMPTION, SMT_TK_FORMULA, SMT_TK_STATUS, SMT_TK_EXTRASORTS, SMT_TK_EXTRAFUNS, SMT_TK_EXTRAPREDS, SMT_TK_NOTES, // theories: sort symbols. removed SMT_TK_U SMT_TK_INDEX, SMT_TK_ELEMENT, SMT_TK_ARRAY, SMT_TK_INT, SMT_TK_REAL, SMT_TK_ARRAY1, SMT_TK_ARRAY2, SMT_TK_BITVEC, // theories: function symbols SMT_TK_ADD, SMT_TK_SUB, SMT_TK_MUL, SMT_TK_DIV, SMT_TK_TILDE, SMT_TK_LT, SMT_TK_LE, SMT_TK_GT, SMT_TK_GE, SMT_TK_SELECT, SMT_TK_STORE, // old bitvector functions SMT_TK_BVADD, SMT_TK_BVSUB, SMT_TK_BVMUL, SMT_TK_BVNEG, SMT_TK_BVOR, SMT_TK_BVAND, SMT_TK_BVXOR, SMT_TK_BVNOT, SMT_TK_BVLT, SMT_TK_BVLEQ, SMT_TK_BVGT, SMT_TK_BVGEQ, SMT_TK_BVSLT, SMT_TK_BVSLEQ, SMT_TK_BVSGT, SMT_TK_BVSGEQ, SMT_TK_CONCAT, SMT_TK_EXTRACT, SMT_TK_SIGN_EXTEND, SMT_TK_SHIFT_LEFT0, SMT_TK_SHIFT_LEFT1, SMT_TK_SHIFT_RIGHT0, SMT_TK_SHIFT_RIGHT1, SMT_TK_BIT0, SMT_TK_BIT1, // new bitvector functions SMT_TK_BVUDIV, SMT_TK_BVUREM, SMT_TK_BVSDIV, SMT_TK_BVSREM, SMT_TK_BVSMOD, SMT_TK_BVSHL, SMT_TK_BVLSHR, SMT_TK_BVASHR, SMT_TK_BVNAND, SMT_TK_BVNOR, SMT_TK_BVXNOR, SMT_TK_BVREDOR, SMT_TK_BVREDAND, SMT_TK_BVCOMP, SMT_TK_REPEAT, SMT_TK_ZERO_EXTEND, SMT_TK_ROTATE_LEFT, SMT_TK_ROTATE_RIGHT, // new names of bitvector predicates SMT_TK_BVULT, SMT_TK_BVULE, SMT_TK_BVUGT, SMT_TK_BVUGE, SMT_TK_BVSLE, SMT_TK_BVSGE, // errors SMT_TK_OPEN_STRING, SMT_TK_OPEN_USER_VAL, SMT_TK_ZERO_DIVISOR, SMT_TK_INVALID_NUMBER, SMT_TK_INVALID_BITVEC, SMT_TK_INVALID_EXTRACT, SMT_TK_ERROR, } Tokens that can be atomic terms or formulas ------------------------------------------- SMT_TK_VAR SMT_TK_RATIONALS SMT_TK_BV_BINCONSTANT SMT_TK_FALSE SMK_TK_FVAR SMT_TK_FLOAT SMT_TK_BV_HEXCONSTANT SMT_TK_BIT0 SMT_TK_SYMBOL SMT_TK_BV_CONSTANTS SMT_TK_TRUE SMT_TK_BIT1 Tokens that represent simple functions or connectors ---------------------------------------------------- SMT_TK_DISTINCT SMT_TK_EQ SMT_TK_NOT SMT_TK_IMPLIES SMT_TK_IF_THEN_ELSE SMT_TK_AND SMT_TK_OR SMT_TK_XOR SMT_TK_IFF SMT_TK_ITE SMT_TK_ADD SMT_TK_SUB SMT_TK_MUL SMT_TK_DIV SMT_TK_TILDE SMT_TK_LT SMT_TK_LE SMT_TK_GT SMT_TK_GE SMT_TK_SELECT SMT_TK_STORE SMT_TK_BVADD SMT_TK_BVSUB SMT_TK_BVMUL SMT_TK_BVNEG SMT_TK_BVOR SMT_TK_BVAND SMT_TK_BVXOR SMT_TK_BVNOT SMT_TK_BVLT SMT_TK_BVLEQ SMT_TK_BVGT SMT_TK_BVGEQ SMT_TK_BVSLT SMT_TK_BVSLEQ SMT_TK_BVSGT SMT_TK_BVSGEQ SMT_TK_CONCAT SMT_TK_SHIFT_LEFT0 SMT_TK_SHIFT_RIGHT0 SMT_TK_SHIFT_LEFT1 SMT_TK_SHIFT_RIGHT1 SMT_TK_BVUDIV SMT_TK_BVUREM SMT_TK_BVSDIV SMT_TK_BVSREM SMT_TK_BVSMOD SMT_TK_BVSHL SMT_TK_BVLSHR SMT_TK_BVASHR SMT_TK_BVNAND SMT_TK_BVNOR SMT_TK_BVXNOR SMT_TK_BVREDOR SMT_TK_BVREDAND SMT_TK_BVCOMP SMT_TK_BVULT SMT_TK_BVULE SMT_TK_BVUGT SMT_TK_BVUGE SMT_TK_BVSLE SMT_TK_BVSGE Tokens that need special treatment ---------------------------------- SMT_TK_EXTRACT SMT_TK_SIGN_EXTEND SMT_TK_REPEAT SMT_TK_ZERO_EXTEND SMT_TK_ROTATE_LEFT SMT_TK_ROTATE_RIGHT Ordinary sort symbols --------------------- SMT_TK_INT SMT_TK_REAL SMT_TK_ARRAY1 SMT_TK_ARRAY2 Sort symbols that need special treatment ---------------------------------------- SMT_TK_BITVEC SMT_TK_ARRAY Parsing transitions ------------------- list of annotations (possibly empty) an0 next; goto an1 - return (do not consume the token) an1 next; goto an1 next; goto an0 - return (do not consume the token) basic term or atoms (excluding ) bt0 next; return next; return next; return next; return next; return next; return true next; return false next; return bit0 next; return bit1 next; return next; goto bt1 bt1 [ next; goto bt2 _ return bt2 next; goto bt3 // bitvector size bt3 ] next; return // used to include // s0 U next; return // removed: U is no longer a keyword sort s0 Int next; return Real next; return Array1 next; return Array2 next; return next; return BitVec next; goto s1 Array next; goto s4 s1 [ next; goto s2 s2 next; goto s3 // bitvector size s3 ] next; return s4 [ next; goto s5 - return s5 next; goto s6 s6 : next; goto s7 s7 next; goto s8 s8 ] next; return annotated term of formula f0 next; return ( next; goto f1 - goto bt0 f1 simple kw next; push f3; goto f0 next; goto f4 extract next; goto f6 rotate_left next; goto f9 rotate_right next; goto f9 repeat next; goto f9 zero_extend next; goto f9 sign_extend next; goto f14 let next; goto f16 flet next; goto f16 exists next; goto f20 forall next; goto f20 - push f5; goto bt0 // function applications or annotated base-term or annotated symbol f3 ) next; return next; push f26; goto an1 - push f3; goto f0 f4 next; push f27; goto an1 - push f3; goto f0 f5 next; push f27; goto an1 f27 ) next; return // no eval // f6: read 2 square bracketed rationals f6 [ next; goto f7 f7 next; goto f8 f8 : next; goto f10 // f9: read 1 square bracketed rational f9 [ next; goto f10 f10 next; goto f11 f11 ] next; push f26; push an0; goto f0 // f13: ) f13 _ push f26; goto an0 // removed f26 ) next return // f14: either [] term ) // or term rational ) f14 [ next; goto f10 _ push f15; goto f0 f15 next; goto f13 // deal with let/flet f16 ( next; goto f17 f17 var next; push f19; goto f0 fvar next; push f19; goto f0 f19 ) next; push f13; goto f0 // quantifiers f20 ( next; goto f21 f21 var next; push f23; goto s0 f23 ) next; goto f24 f24 ( next; goto f25 next; goto f13 _ push f13; goto bt0 f25 var next; push f23; goto s0 _ push f13; goto f1 // recursive parse term, omitting opening ( benchmark b0 ( next; goto b1 b1 benchmark next; goto b2 b2 next; goto b3 b3 :notes next; goto b4 :status next; goto b5 :assumption next; push b3; goto f0 :formula next; push b3; goto f0 :logic next; goto b7 :extrasorts next; goto b11 :extrapreds next; goto b14 :extrafuns next; goto b20 next; push b3; goto an1 ) next; return // done! b4 next; goto b3 b5 sat next; goto b3 unsat next; goto b3 unknown next; goto b3 b7 next; goto b8 b8 [ next; goto b9 - goto b3 b9 next; goto b10 b10 ] next; goto b3 // extrasorts b11 ( next; goto b12 b12 next; goto b13 b13 ) next; goto b3 next; goto b13 // extrapreds b14 ( next; goto b15 b15 ( next; goto b16 b16 next; goto b17 b17 ) next; goto b19 next; push b18; goto an1 _ push b17; goto s0 b18 ) next; goto b19 b19 ( next; goto b16 ) next; goto b3 // extrafuns b20 ( next; goto b21 b21 ( next; goto b22 b22 next; push b24; goto s0 b24 ) next; goto b25 next; push b27; goto an1 _ push b24; goto s0 b25 ( next; goto b22 ) next; goto b3 b27 ) next; goto b25