let yyact = [|
(fun _ -> failwith "parser")
; (fun parser_env ->
let _1 = (peek_val parser_env 1 : 'term) in
Obj.repr((
# 127 "../../src/parser.mly"
_1 ) : Term.t))
; (fun parser_env ->
let _1 = (peek_val parser_env 1 : 'atom) in
Obj.repr((
# 128 "../../src/parser.mly"
_1 ) : Atom.t))
; (fun parser_env ->
let _1 = (peek_val parser_env 1 : 'command) in
Obj.repr((
# 129 "../../src/parser.mly"
_1 ) : Result.t))
; (fun parser_env ->
let _1 = (peek_val parser_env 1 : 'command) in
Obj.repr((
# 131 "../../src/parser.mly"
_1 ) : Result.t))
; (fun parser_env ->
Obj.repr((
# 132 "../../src/parser.mly"
raise End_of_file ) : Result.t))
; (fun parser_env ->
let _1 = (peek_val parser_env 2 : 'command) in
let _3 = (peek_val parser_env 0 : unit) in
Obj.repr((
# 135 "../../src/parser.mly"
lastresult := _1 ) : unit))
; (fun parser_env ->
let _1 = (peek_val parser_env 2 : 'command) in
Obj.repr((
# 136 "../../src/parser.mly"
lastresult := _1; raise(Result.Result(!lastresult)) ) : unit))
; (fun parser_env ->
let _1 = (peek_val parser_env 0 : int) in
Obj.repr((
# 140 "../../src/parser.mly"
_1 ) : 'int))
; (fun parser_env ->
let _1 = (peek_val parser_env 0 : 'int) in
Obj.repr((
# 143 "../../src/parser.mly"
Q.of_int _1 ) : 'rat))
; (fun parser_env ->
let _1 = (peek_val parser_env 0 : Mpa.Q.t) in
Obj.repr((
# 144 "../../src/parser.mly"
_1 ) : 'rat))
; (fun parser_env ->
let _1 = (peek_val parser_env 0 : string) in
Obj.repr((
# 148 "../../src/parser.mly"
Name.of_string _1 ) : 'name))
; (fun parser_env ->
let _1 = (peek_val parser_env 0 : 'name) in
Obj.repr((
# 150 "../../src/parser.mly"
[_1] ) : 'namelist))
; (fun parser_env ->
let _1 = (peek_val parser_env 2 : 'namelist) in
let _3 = (peek_val parser_env 0 : 'name) in
Obj.repr((
# 151 "../../src/parser.mly"
_3 :: _1 ) : 'namelist))
; (fun parser_env ->
let _1 = (peek_val parser_env 0 : 'name) in
Obj.repr((
# 154 "../../src/parser.mly"
Sym.Uninterp(_1) ) : 'funsym))
; (fun parser_env ->
Obj.repr((
# 155 "../../src/parser.mly"
Sym.Arith(Sym.Add) ) : 'funsym))
; (fun parser_env ->
Obj.repr((
# 156 "../../src/parser.mly"
Sym.Pp(Sym.Mult) ) : 'funsym))
; (fun parser_env ->
let _3 = (peek_val parser_env 1 : 'int) in
Obj.repr((
# 157 "../../src/parser.mly"
Sym.Pp(Sym.Expt(_3)) ) : 'funsym))
; (fun parser_env ->
Obj.repr((
# 158 "../../src/parser.mly"
Sym.Pair(Sym.Cons) ) : 'funsym))
; (fun parser_env ->
Obj.repr((
# 159 "../../src/parser.mly"
Sym.Pair(Sym.Car) ) : 'funsym))
; (fun parser_env ->
Obj.repr((
# 160 "../../src/parser.mly"
Sym.Pair(Sym.Cdr) ) : 'funsym))
; (fun parser_env ->
Obj.repr((
# 161 "../../src/parser.mly"
Sym.Bvarith(Sym.Unsigned) ) : 'funsym))
; (fun parser_env ->
let _3 = (peek_val parser_env 3 : int) in
let _5 = (peek_val parser_env 1 : int) in
Obj.repr((
# 162 "../../src/parser.mly"
Sym.Bv(Sym.Conc(_3, _5)) ) : 'funsym))
; (fun parser_env ->
let _3 = (peek_val parser_env 5 : int) in
let _5 = (peek_val parser_env 3 : int) in
let _7 = (peek_val parser_env 1 : int) in
Obj.repr((
# 163 "../../src/parser.mly"
Sym.Bv(Sym.Sub(_3, _5, _7)) ) : 'funsym))
; (fun parser_env ->
let _3 = (peek_val parser_env 1 : int) in
Obj.repr((
# 164 "../../src/parser.mly"
Sym.Bv(Sym.Bitwise(_3)) ) : 'funsym))
; (fun parser_env ->
let _2 = (peek_val parser_env 0 : 'range) in
Obj.repr((
# 165 "../../src/parser.mly"
Sym.Fun(Sym.Apply(_2)) ) : 'funsym))
; (fun parser_env ->
Obj.repr((
# 166 "../../src/parser.mly"
Sym.Fun(Sym.Abs) ) : 'funsym))
; (fun parser_env ->
Obj.repr((
# 169 "../../src/parser.mly"
None ) : 'range))
; (fun parser_env ->
let _1 = (peek_val parser_env 0 : 'rat) in
Obj.repr((
# 172 "../../src/parser.mly"
Sym.Arith(Sym.Num(_1)) ) : 'constsym))
; (fun parser_env ->
Obj.repr((
# 173 "../../src/parser.mly"
Sym.Bv(Sym.Const(Bitv.from_string "1")) ) : 'constsym))
; (fun parser_env ->
Obj.repr((
# 174 "../../src/parser.mly"
Sym.Bv(Sym.Const(Bitv.from_string "0")) ) : 'constsym))
; (fun parser_env ->
let _1 = (peek_val parser_env 0 : string) in
Obj.repr((
# 175 "../../src/parser.mly"
Sym.Bv(Sym.Const(Bitv.from_string _1)) ) : 'constsym))
; (fun parser_env ->
let _1 = (peek_val parser_env 0 : 'var) in
Obj.repr((
# 181 "../../src/parser.mly"
_1 ) : 'term))
; (fun parser_env ->
let _1 = (peek_val parser_env 0 : 'app) in
Obj.repr((
# 182 "../../src/parser.mly"
_1 ) : 'term))
; (fun parser_env ->
let _2 = (peek_val parser_env 1 : 'term) in
Obj.repr((
# 183 "../../src/parser.mly"
_2 ) : 'term))
; (fun parser_env ->
let _1 = (peek_val parser_env 0 : 'arith) in
Obj.repr((
# 184 "../../src/parser.mly"
_1 ) : 'term))
; (fun parser_env ->
let _1 = (peek_val parser_env 0 : 'array) in
Obj.repr((
# 185 "../../src/parser.mly"
_1 ) : 'term))
; (fun parser_env ->
let _1 = (peek_val parser_env 0 : 'bv) in
Obj.repr((
# 186 "../../src/parser.mly"
_1 ) : 'term))
; (fun parser_env ->
let _1 = (peek_val parser_env 0 : 'coproduct) in
Obj.repr((
# 187 "../../src/parser.mly"
_1 ) : 'term))
; (fun parser_env ->
let _1 = (peek_val parser_env 0 : 'list) in
Obj.repr((
# 188 "../../src/parser.mly"
_1 ) : 'term))
; (fun parser_env ->
let _1 = (peek_val parser_env 0 : 'apply) in
Obj.repr((
# 189 "../../src/parser.mly"
_1 ) : 'term))
; (fun parser_env ->
let _1 = (peek_val parser_env 0 : 'name) in
Obj.repr((
# 193 "../../src/parser.mly"
try
match Symtab.lookup _1 (Istate.symtab()) with
| Symtab.Def(Symtab.Term(a)) -> a
| Symtab.Type(d) -> Term.mk_var _1 (Some(d))
| _ -> Term.mk_var _1 None
with
Not_found -> Term.mk_var _1 None ) : 'var))
; (fun parser_env ->
let _1 = (peek_val parser_env 3 : 'name) in
let _3 = (peek_val parser_env 1 : 'dom) in
Obj.repr((
# 200 "../../src/parser.mly"
Term.mk_var _1 (Some(_3))) : 'var))
; (fun parser_env ->
let _1 = (peek_val parser_env 1 : string * int) in
let _2 = (peek_val parser_env 0 : 'optdom) in
Obj.repr((
# 201 "../../src/parser.mly"
let (x, k) = _1 in
let n = Name.of_string x in
if Name.eq n name_of_strict_slack then
Term.mk_slack (Some(k)) false _2
else if Name.eq n name_of_nonstrict_slack then
Term.mk_slack (Some(k)) true _2
else
Term.mk_rename n (Some(k)) _2 ) : 'var))
; (fun parser_env ->
let _1 = (peek_val parser_env 0 : int) in
Obj.repr((
# 209 "../../src/parser.mly"
Term.Var(Var.mk_free _1) ) : 'var))
; (fun parser_env ->
let _1 = (peek_val parser_env 0 : 'var) in
Obj.repr((
# 212 "../../src/parser.mly"
[_1] ) : 'varlist))
; (fun parser_env ->
let _1 = (peek_val parser_env 2 : 'varlist) in
let _3 = (peek_val parser_env 0 : 'var) in
Obj.repr((
# 213 "../../src/parser.mly"
_3 :: _1 ) : 'varlist))
; (fun parser_env ->
Obj.repr((
# 216 "../../src/parser.mly"
None ) : 'optdom))
; (fun parser_env ->
let _2 = (peek_val parser_env 1 : 'dom) in
Obj.repr((
# 217 "../../src/parser.mly"
Some(_2) ) : 'optdom))
; (fun parser_env ->
let _1 = (peek_val parser_env 3 : 'funsym) in
let _3 = (peek_val parser_env 1 : 'termlist) in
Obj.repr((
# 221 "../../src/parser.mly"
Th.sigma _1 (List.rev _3) ) : 'app))
; (fun parser_env ->
let _1 = (peek_val parser_env 0 : 'constsym) in
Obj.repr((
# 222 "../../src/parser.mly"
Th.sigma _1 [] ) : 'app))
; (fun parser_env ->
let _1 = (peek_val parser_env 2 : 'term) in
let _3 = (peek_val parser_env 0 : 'term) in
Obj.repr((
# 225 "../../src/parser.mly"
Coproduct.mk_inj 1 (Pair.mk_cons _1 _3) ) : 'list))
; (fun parser_env ->
let _3 = (peek_val parser_env 1 : 'term) in
Obj.repr((
# 226 "../../src/parser.mly"
Pair.mk_car (Coproduct.mk_out 1 _3) ) : 'list))
; (fun parser_env ->
let _3 = (peek_val parser_env 1 : 'term) in
Obj.repr((
# 227 "../../src/parser.mly"
Pair.mk_cdr (Coproduct.mk_out 1 _3) ) : 'list))
; (fun parser_env ->
Obj.repr((
# 228 "../../src/parser.mly"
Coproduct.mk_inj 0 (Bitvector.mk_eps) ) : 'list))
; (fun parser_env ->
let _1 = (peek_val parser_env 2 : 'term) in
let _3 = (peek_val parser_env 0 : 'term) in
Obj.repr((
# 231 "../../src/parser.mly"
Apply.mk_apply
Th.sigma
None _1 [_3] ) : 'apply))
; (fun parser_env ->
let _1 = (peek_val parser_env 2 : 'term) in
let _3 = (peek_val parser_env 0 : 'term) in
Obj.repr((
# 237 "../../src/parser.mly"
Arith.mk_add _1 _3 ) : 'arith))
; (fun parser_env ->
let _1 = (peek_val parser_env 2 : 'term) in
let _3 = (peek_val parser_env 0 : 'term) in
Obj.repr((
# 238 "../../src/parser.mly"
Arith.mk_sub _1 _3 ) : 'arith))
; (fun parser_env ->
let _2 = (peek_val parser_env 0 : 'term) in
Obj.repr((
# 239 "../../src/parser.mly"
Arith.mk_neg _2 ) : 'arith))
; (fun parser_env ->
let _1 = (peek_val parser_env 2 : 'term) in
let _3 = (peek_val parser_env 0 : 'term) in
Obj.repr((
# 240 "../../src/parser.mly"
Sig.mk_mult _1 _3 ) : 'arith))
; (fun parser_env ->
let _1 = (peek_val parser_env 2 : 'term) in
let _3 = (peek_val parser_env 0 : 'term) in
Obj.repr((
# 241 "../../src/parser.mly"
Sig.mk_div _1 _3 ) : 'arith))
; (fun parser_env ->
let _1 = (peek_val parser_env 2 : 'term) in
let _3 = (peek_val parser_env 0 : 'int) in
Obj.repr((
# 242 "../../src/parser.mly"
Sig.mk_expt _3 _1 ) : 'arith))
; (fun parser_env ->
let _3 = (peek_val parser_env 1 : 'term) in
Obj.repr((
# 246 "../../src/parser.mly"
Coproduct.mk_inl _3 ) : 'coproduct))
; (fun parser_env ->
let _3 = (peek_val parser_env 1 : 'term) in
Obj.repr((
# 247 "../../src/parser.mly"
Coproduct.mk_inr _3 ) : 'coproduct))
; (fun parser_env ->
let _3 = (peek_val parser_env 1 : 'term) in
Obj.repr((
# 248 "../../src/parser.mly"
Coproduct.mk_outl _3 ) : 'coproduct))
; (fun parser_env ->
let _3 = (peek_val parser_env 1 : 'term) in
Obj.repr((
# 249 "../../src/parser.mly"
Coproduct.mk_outr _3 ) : 'coproduct))
; (fun parser_env ->
let _3 = (peek_val parser_env 4 : int) in
let _6 = (peek_val parser_env 1 : 'term) in
Obj.repr((
# 250 "../../src/parser.mly"
Coproduct.mk_inj _3 _6 ) : 'coproduct))
; (fun parser_env ->
let _3 = (peek_val parser_env 4 : int) in
let _6 = (peek_val parser_env 1 : 'term) in
Obj.repr((
# 251 "../../src/parser.mly"
Coproduct.mk_out _3 _6 ) : 'coproduct))
; (fun parser_env ->
let _3 = (peek_val parser_env 1 : 'term) in
Obj.repr((
# 255 "../../src/parser.mly"
Arr.mk_create _3 ) : 'array))
; (fun parser_env ->
let _1 = (peek_val parser_env 5 : 'term) in
let _3 = (peek_val parser_env 3 : 'term) in
let _5 = (peek_val parser_env 1 : 'term) in
Obj.repr((
# 256 "../../src/parser.mly"
Arr.mk_update Istate.is_equal _1 _3 _5 ) : 'array))
; (fun parser_env ->
let _1 = (peek_val parser_env 3 : 'term) in
let _3 = (peek_val parser_env 1 : 'term) in
Obj.repr((
# 257 "../../src/parser.mly"
Arr.mk_select Istate.is_equal _1 _3 ) : 'array))
; (fun parser_env ->
let _1 = (peek_val parser_env 2 : 'term) in
let _3 = (peek_val parser_env 0 : 'term) in
Obj.repr((
# 262 "../../src/parser.mly"
match Istate.width_of _1, Istate.width_of _3 with
| Some(n), Some(m) ->
if n < 0 then
raise (Invalid_argument ("Negative length of " ^ Term.to_string _1))
else if m < 0 then
raise (Invalid_argument ("Negative length of " ^ Term.to_string _3))
else
Bitvector.mk_conc n m _1 _3
| Some _, _ ->
raise (Invalid_argument (Term.to_string _3 ^ " not a bitvector."))
| _ ->
raise (Invalid_argument (Term.to_string _1 ^ " not a bitvector.")) ) : 'bv))
; (fun parser_env ->
let _1 = (peek_val parser_env 5 : 'term) in
let _3 = (peek_val parser_env 3 : int) in
let _5 = (peek_val parser_env 1 : int) in
Obj.repr((
# 275 "../../src/parser.mly"
match Istate.width_of _1 with
| Some(n) ->
if n < 0 then
raise(Invalid_argument ("Negative length of " ^ Term.to_string _1))
else if not(0 <= _3 && _3 <= _5 && _5 < n) then
raise(Invalid_argument ("Invalid extraction from " ^ Term.to_string _1))
else
Bitvector.mk_sub n _3 _5 _1
| None ->
raise (Invalid_argument (Term.to_string _1 ^ " not a bitvector.")) ) : 'bv))
; (fun parser_env ->
let _1 = (peek_val parser_env 2 : 'term) in
let _3 = (peek_val parser_env 0 : 'term) in
Obj.repr((
# 285 "../../src/parser.mly"
Bitvector.mk_bwconj (equal_width_of _1 _3) _1 _3 ) : 'bv))
; (fun parser_env ->
let _1 = (peek_val parser_env 2 : 'term) in
let _3 = (peek_val parser_env 0 : 'term) in
Obj.repr((
# 286 "../../src/parser.mly"
Bitvector.mk_bwdisj (equal_width_of _1 _3) _1 _3 ) : 'bv))
; (fun parser_env ->
let _1 = (peek_val parser_env 2 : 'term) in
let _3 = (peek_val parser_env 0 : 'term) in
Obj.repr((
# 287 "../../src/parser.mly"
Bitvector.mk_bwimp (equal_width_of _1 _3) _1 _3 ) : 'bv))
; (fun parser_env ->
let _1 = (peek_val parser_env 2 : 'term) in
let _3 = (peek_val parser_env 0 : 'term) in
Obj.repr((
# 288 "../../src/parser.mly"
Bitvector.mk_bwiff (equal_width_of _1 _3) _1 _3 ) : 'bv))
; (fun parser_env ->
let _2 = (peek_val parser_env 1 : 'prop) in
Obj.repr((
# 292 "../../src/parser.mly"
_2 ) : 'prop))
; (fun parser_env ->
let _2 = (peek_val parser_env 1 : 'prop) in
Obj.repr((
# 293 "../../src/parser.mly"
_2 ) : 'prop))
; (fun parser_env ->
let _1 = (peek_val parser_env 0 : 'name) in
Obj.repr((
# 294 "../../src/parser.mly"
try
match Symtab.lookup _1 (Istate.symtab()) with
| Symtab.Def(Symtab.Prop(p)) -> p
| _ -> Prop.mk_var _1
with
Not_found -> Prop.mk_var _1 ) : 'prop))
; (fun parser_env ->
let _1 = (peek_val parser_env 0 : 'atom) in
Obj.repr((
# 300 "../../src/parser.mly"
Prop.mk_poslit _1 ) : 'prop))
; (fun parser_env ->
let _1 = (peek_val parser_env 2 : 'prop) in
let _3 = (peek_val parser_env 0 : 'prop) in
Obj.repr((
# 301 "../../src/parser.mly"
Prop.mk_conj [_1; _3] ) : 'prop))
; (fun parser_env ->
let _1 = (peek_val parser_env 2 : 'prop) in
let _3 = (peek_val parser_env 0 : 'prop) in
Obj.repr((
# 302 "../../src/parser.mly"
Prop.mk_disj [_1; _3] ) : 'prop))
; (fun parser_env ->
let _1 = (peek_val parser_env 2 : 'prop) in
let _3 = (peek_val parser_env 0 : 'prop) in
Obj.repr((
# 303 "../../src/parser.mly"
Prop.mk_iff _1 _3 ) : 'prop))
; (fun parser_env ->
let _1 = (peek_val parser_env 2 : 'prop) in
let _3 = (peek_val parser_env 0 : 'prop) in
Obj.repr((
# 304 "../../src/parser.mly"
Prop.mk_neg (Prop.mk_iff _1 _3) ) : 'prop))
; (fun parser_env ->
let _1 = (peek_val parser_env 2 : 'prop) in
let _3 = (peek_val parser_env 0 : 'prop) in
Obj.repr((
# 305 "../../src/parser.mly"
Prop.mk_disj [Prop.mk_neg _1; _3] ) : 'prop))
; (fun parser_env ->
let _2 = (peek_val parser_env 0 : 'prop) in
Obj.repr((
# 306 "../../src/parser.mly"
Prop.mk_neg _2 ) : 'prop))
; (fun parser_env ->
let _2 = (peek_val parser_env 5 : 'prop) in
let _4 = (peek_val parser_env 3 : 'prop) in
let _6 = (peek_val parser_env 1 : 'prop) in
Obj.repr((
# 307 "../../src/parser.mly"
Prop.mk_ite _2 _4 _6 ) : 'prop))
; (fun parser_env ->
Obj.repr((
# 311 "../../src/parser.mly"
Atom.mk_false ) : 'atom))
; (fun parser_env ->
Obj.repr((
# 312 "../../src/parser.mly"
Atom.mk_true ) : 'atom))
; (fun parser_env ->
let _1 = (peek_val parser_env 2 : 'term) in
let _3 = (peek_val parser_env 0 : 'term) in
Obj.repr((
# 313 "../../src/parser.mly"
Atom.mk_equal(_1, _3)) : 'atom))
; (fun parser_env ->
let _1 = (peek_val parser_env 2 : 'term) in
let _3 = (peek_val parser_env 0 : 'term) in
Obj.repr((
# 314 "../../src/parser.mly"
Atom.mk_diseq(_1, _3) ) : 'atom))
; (fun parser_env ->
let _1 = (peek_val parser_env 2 : 'term) in
let _3 = (peek_val parser_env 0 : 'term) in
Obj.repr((
# 315 "../../src/parser.mly"
Atom.mk_lt (_1, _3) ) : 'atom))
; (fun parser_env ->
let _1 = (peek_val parser_env 2 : 'term) in
let _3 = (peek_val parser_env 0 : 'term) in
Obj.repr((
# 316 "../../src/parser.mly"
Atom.mk_gt (_1, _3) ) : 'atom))
; (fun parser_env ->
let _1 = (peek_val parser_env 2 : 'term) in
let _3 = (peek_val parser_env 0 : 'term) in
Obj.repr((
# 317 "../../src/parser.mly"
Atom.mk_le (_1, _3) ) : 'atom))
; (fun parser_env ->
let _1 = (peek_val parser_env 2 : 'term) in
let _3 = (peek_val parser_env 0 : 'term) in
Obj.repr((
# 318 "../../src/parser.mly"
Atom.mk_ge (_1, _3) ) : 'atom))
; (fun parser_env ->
Obj.repr((
# 322 "../../src/parser.mly"
Dom.Int ) : 'dom))
; (fun parser_env ->
Obj.repr((
# 323 "../../src/parser.mly"
Dom.Real ) : 'dom))
; (fun parser_env ->
Obj.repr((
# 327 "../../src/parser.mly"
[] ) : 'termlist))
; (fun parser_env ->
let _1 = (peek_val parser_env 0 : 'term) in
Obj.repr((
# 328 "../../src/parser.mly"
[_1] ) : 'termlist))
; (fun parser_env ->
let _1 = (peek_val parser_env 2 : 'termlist) in
let _3 = (peek_val parser_env 0 : 'term) in
Obj.repr((
# 329 "../../src/parser.mly"
_3 :: _1 ) : 'termlist))
; (fun parser_env ->
let _3 = (peek_val parser_env 1 : int) in
Obj.repr((
# 333 "../../src/parser.mly"
_3 ) : 'signature))
; (fun parser_env ->
let _2 = (peek_val parser_env 0 : 'term) in
Obj.repr((
# 337 "../../src/parser.mly"
Result.Term(Istate.can _2) ) : 'command))
; (fun parser_env ->
let _2 = (peek_val parser_env 1 : 'optname) in
let _3 = (peek_val parser_env 0 : 'atom) in
Obj.repr((
# 338 "../../src/parser.mly"
Result.Process(Istate.process _2 _3) ) : 'command))
; (fun parser_env ->
let _2 = (peek_val parser_env 2 : 'name) in
let _4 = (peek_val parser_env 0 : 'term) in
Obj.repr((
# 339 "../../src/parser.mly"
Result.Unit(Istate.def _2 (Symtab.Term(_4))) ) : 'command))
; (fun parser_env ->
let _2 = (peek_val parser_env 2 : 'name) in
let _4 = (peek_val parser_env 0 : 'prop) in
Obj.repr((
# 340 "../../src/parser.mly"
Result.Unit(Istate.def _2 (Symtab.Prop(_4))) ) : 'command))
; (fun parser_env ->
let _2 = (peek_val parser_env 2 : 'name) in
let _4 = (peek_val parser_env 0 : 'dom) in
Obj.repr((
# 341 "../../src/parser.mly"
Result.Unit(Istate.typ [_2] _4) ) : 'command))
; (fun parser_env ->
let _2 = (peek_val parser_env 2 : 'name) in
let _4 = (peek_val parser_env 0 : 'signature) in
Obj.repr((
# 342 "../../src/parser.mly"
Result.Unit(Istate.sgn _2 _4) ) : 'command))
; (fun parser_env ->
Obj.repr((
# 343 "../../src/parser.mly"
Result.Unit(Istate.reset ()) ) : 'command))
; (fun parser_env ->
let _2 = (peek_val parser_env 0 : 'name) in
Obj.repr((
# 344 "../../src/parser.mly"
Result.Name(Istate.save(Some(_2))) ) : 'command))
; (fun parser_env ->
Obj.repr((
# 345 "../../src/parser.mly"
Result.Name(Istate.save(None)) ) : 'command))
; (fun parser_env ->
let _2 = (peek_val parser_env 0 : 'name) in
Obj.repr((
# 346 "../../src/parser.mly"
Result.Unit(Istate.restore _2) ) : 'command))
; (fun parser_env ->
let _2 = (peek_val parser_env 0 : 'name) in
Obj.repr((
# 347 "../../src/parser.mly"
Result.Unit(Istate.remove _2) ) : 'command))
; (fun parser_env ->
Obj.repr((
# 348 "../../src/parser.mly"
Result.Unit(Istate.forget()) ) : 'command))
; (fun parser_env ->
let _2 = (peek_val parser_env 1 : 'optname) in
let _3 = (peek_val parser_env 0 : 'atom) in
Obj.repr((
# 349 "../../src/parser.mly"
Result.Bool(Istate.valid _2 _3) ) : 'command))
; (fun parser_env ->
let _2 = (peek_val parser_env 1 : 'optname) in
let _3 = (peek_val parser_env 0 : 'atom) in
Obj.repr((
# 350 "../../src/parser.mly"
Result.Bool(Istate.unsat _2 _3) ) : 'command))
; (fun parser_env ->
Obj.repr((
# 351 "../../src/parser.mly"
raise End_of_file ) : 'command))
; (fun parser_env ->
Obj.repr((
# 352 "../../src/parser.mly"
failwith "drop" ) : 'command))
; (fun parser_env ->
Obj.repr((
# 353 "../../src/parser.mly"
Result.Symtab(Istate.symtab()) ) : 'command))
; (fun parser_env ->
let _2 = (peek_val parser_env 0 : 'name) in
Obj.repr((
# 354 "../../src/parser.mly"
match Istate.entry_of _2 with
| Some(e) -> Result.Entry(e)
| None -> raise (Invalid_argument (Name.to_string _2 ^ "not in symbol table")) ) : 'command))
; (fun parser_env ->
let _2 = (peek_val parser_env 0 : 'optname) in
Obj.repr((
# 357 "../../src/parser.mly"
Result.Atoms(Istate.ctxt_of _2) ) : 'command))
; (fun parser_env ->
let _2 = (peek_val parser_env 0 : 'term) in
Obj.repr((
# 358 "../../src/parser.mly"
Result.Term(_2) ) : 'command))
; (fun parser_env ->
let _1 = (peek_val parser_env 2 : 'term) in
let _3 = (peek_val parser_env 0 : 'term) in
Obj.repr((
# 359 "../../src/parser.mly"
Result.Int(Term.cmp _1 _3) ) : 'command))
; (fun parser_env ->
let _2 = (peek_val parser_env 0 : 'optname) in
Obj.repr((
# 360 "../../src/parser.mly"
Result.Context(Istate.get_context _2) ) : 'command))
; (fun parser_env ->
let _2 = (peek_val parser_env 2 : 'optname) in
let _3 = (peek_val parser_env 1 : 'th) in
let _4 = (peek_val parser_env 0 : 'term) in
Obj.repr((
# 361 "../../src/parser.mly"
Result.Term(Istate.find _2 _3 _4) ) : 'command))
; (fun parser_env ->
let _2 = (peek_val parser_env 2 : 'optname) in
let _3 = (peek_val parser_env 1 : 'th) in
let _4 = (peek_val parser_env 0 : 'term) in
Obj.repr((
# 362 "../../src/parser.mly"
try Result.Optterm(Some(Istate.inv _2 _3 _4))
with Not_found -> Result.Optterm(None) ) : 'command))
; (fun parser_env ->
let _2 = (peek_val parser_env 2 : 'optname) in
let _3 = (peek_val parser_env 1 : 'th) in
let _4 = (peek_val parser_env 0 : 'term) in
Obj.repr((
# 364 "../../src/parser.mly"
Result.Terms(Istate.use _2 _3 _4) ) : 'command))
; (fun parser_env ->
let _2 = (peek_val parser_env 1 : 'optname) in
let _3 = (peek_val parser_env 0 : 'term) in
Obj.repr((
# 365 "../../src/parser.mly"
Result.Cnstrnt(Istate.sign _2 _3) ) : 'command))
; (fun parser_env ->
let _2 = (peek_val parser_env 1 : 'optname) in
let _3 = (peek_val parser_env 0 : 'term) in
Obj.repr((
# 366 "../../src/parser.mly"
Result.Dom(Istate.dom _2 _3) ) : 'command))
; (fun parser_env ->
let _2 = (peek_val parser_env 1 : 'optname) in
let _3 = (peek_val parser_env 0 : 'term) in
Obj.repr((
# 367 "../../src/parser.mly"
Result.Terms(Istate.diseq _2 _3) ) : 'command))
; (fun parser_env ->
let _2 = (peek_val parser_env 0 : 'optname) in
Obj.repr((
# 368 "../../src/parser.mly"
Result.Atoms(Istate.split()) ) : 'command))
; (fun parser_env ->
let _2 = (peek_val parser_env 3 : 'th) in
let _3 = (peek_val parser_env 2 : 'term) in
let _5 = (peek_val parser_env 0 : 'term) in
Obj.repr((
# 369 "../../src/parser.mly"
Result.Solution(Istate.solve _2 (_3, _5)) ) : 'command))
; (fun parser_env ->
let _2 = (peek_val parser_env 0 : 'identlist) in
Obj.repr((
# 370 "../../src/parser.mly"
Result.Unit(List.iter Trace.add _2) ) : 'command))
; (fun parser_env ->
Obj.repr((
# 371 "../../src/parser.mly"
Result.Unit(Trace.reset ()) ) : 'command))
; (fun parser_env ->
let _2 = (peek_val parser_env 0 : 'prop) in
Obj.repr((
# 372 "../../src/parser.mly"
Result.Sat(Istate.sat _2) ) : 'command))
; (fun parser_env ->
let _2 = (peek_val parser_env 1 : 'optname) in
let _3 = (peek_val parser_env 0 : 'varlist) in
Obj.repr((
# 373 "../../src/parser.mly"
Result.Solution(Istate.model _2 _3) ) : 'command))
; (fun parser_env ->
let _2 = (peek_val parser_env 0 : string) in
Obj.repr((
# 374 "../../src/parser.mly"
Result.Unit(Format.eprintf "%s@." _2) ) : 'command))
; (fun parser_env ->
let _1 = (peek_val parser_env 0 : 'help) in
Obj.repr((
# 375 "../../src/parser.mly"
Result.Unit(_1) ) : 'command))
; (fun parser_env ->
let _1 = (peek_val parser_env 0 : string) in
Obj.repr((
# 380 "../../src/parser.mly"
[_1] ) : 'identlist))
; (fun parser_env ->
let _1 = (peek_val parser_env 2 : 'identlist) in
let _3 = (peek_val parser_env 0 : string) in
Obj.repr((
# 381 "../../src/parser.mly"
_3 :: _1 ) : 'identlist))
; (fun parser_env ->
let _1 = (peek_val parser_env 0 : string) in
Obj.repr((
# 384 "../../src/parser.mly"
Th.of_string _1 ) : 'th))
; (fun parser_env ->
Obj.repr((
# 387 "../../src/parser.mly"
Help.on_help () ) : 'help))
; (fun parser_env ->
Obj.repr((
# 388 "../../src/parser.mly"
Help.syntax () ) : 'help))
; (fun parser_env ->
Obj.repr((
# 389 "../../src/parser.mly"
Help.commands () ) : 'help))
; (fun parser_env ->
Obj.repr((
# 393 "../../src/parser.mly"
None ) : 'optname))
; (fun parser_env ->
let _2 = (peek_val parser_env 0 : 'name) in
Obj.repr((
# 394 "../../src/parser.mly"
Some(_2) ) : 'optname))
; (fun parser_env -> raise (YYexit (peek_val parser_env 0)))
; (fun parser_env -> raise (YYexit (peek_val parser_env 0)))
; (fun parser_env -> raise (YYexit (peek_val parser_env 0)))
; (fun parser_env -> raise (YYexit (peek_val parser_env 0)))
; (fun parser_env -> raise (YYexit (peek_val parser_env 0)))
|]