Lines Matching defs:logic
26 logic, and possibly on local term definitions ("let"). 3. Due to
359 (* returns the SMT-LIB logic name and its type/term dictionaries *)
362 val logic = get_token ()
363 val (tydict, tmdict) = SmtLib_Logics.parsedicts_of_logic logic
366 (logic, tydict, tmdict)
442 (* returns the logic's name, its 'tydict', its 'tmdict' extended with
449 | NONE => raise ERR "parse_commands" (cmd ^ " issued before set-logic")
459 | "set-logic" =>
462 raise ERR "parse_commands" "set-logic issued more than once"
463 val (logic, tydict, tmdict) = parse_set_logic get_token
465 parse_commands get_token (SOME (logic, tydict, tmdict, []))
469 val (logic, tydict, tmdict, asserted) = dest_state "declare-sort"
472 parse_commands get_token (SOME (logic, tydict, tmdict, asserted))
476 val (logic, tydict, tmdict, asserted) = dest_state "declare-fun"
479 parse_commands get_token (SOME (logic, tydict, tmdict, asserted))
483 val (logic, tydict, tmdict, asserted) = dest_state "define-fun"
487 parse_commands get_token (SOME (logic, tydict, tmdict, asserted))
491 val (logic, tydict, tmdict, asserted) = dest_state "assert"
495 parse_commands get_token (SOME (logic, tydict, tmdict, asserted))
513 val (logic, tydict, tmdict, asserted) = dest_state "exit"
516 (logic, tydict, tmdict, List.rev asserted)
535 benchmark's logic, two dictionaries containing all types and
539 (* FIXME: We only parse "set-logic", "declare-sort", "declare-fun",