mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-09 04:35:35 -05:00
Added smtlib input option
This commit is contained in:
Guillaume Bury
parent
a28cf4098c
commit
4c040ccbde
22 changed files with 947 additions and 78 deletions
2
Makefile
2
Makefile
|
|
@ -3,7 +3,7 @@
|
|||
LOG=build.log
|
||||
COMP=ocamlbuild -log $(LOG) -use-ocamlfind -classic-display
|
||||
FLAGS=
|
||||
DIRS=-Is sat,smt,util
|
||||
DIRS=-Is sat,smt,util,util/smtlib
|
||||
DOC=msat.docdir/index.html
|
||||
TEST=sat_solve.native
|
||||
|
||||
|
|
|
|||
39
sat/sat.ml
39
sat/sat.ml
|
|
@ -1,22 +1,23 @@
|
|||
(* Copyright 2014 Guillaume Bury *)
|
||||
|
||||
module Fsat = struct
|
||||
exception Dummy
|
||||
exception Out_of_int
|
||||
exception Dummy of int
|
||||
|
||||
(* Until the constant true_ and false_ are not needed anymore,
|
||||
* wa can't simply use sigend integers to represent literals *)
|
||||
type t = int
|
||||
|
||||
let max_lit = min max_int (- min_int)
|
||||
let max_lit = max_int
|
||||
let max_fresh = ref (-1)
|
||||
let max_index = ref 0
|
||||
|
||||
let make i =
|
||||
if i <> 0 then begin
|
||||
max_index := max !max_index (abs i);
|
||||
i
|
||||
let _make i =
|
||||
if i <> 0 && (abs i) < max_lit then begin
|
||||
max_index := max !max_index (abs i);
|
||||
i
|
||||
end else
|
||||
raise Dummy
|
||||
(Format.printf "Warning : %d/%d@." i max_lit;
|
||||
raise (Dummy i))
|
||||
|
||||
let dummy = 0
|
||||
|
||||
|
|
@ -31,12 +32,11 @@ module Fsat = struct
|
|||
let label a = _str
|
||||
let add_label _ _ = ()
|
||||
|
||||
let create, iter =
|
||||
let make i = _make (2 * i)
|
||||
let fresh, iter =
|
||||
let create () =
|
||||
if !max_index <> max_lit then
|
||||
(incr max_index; !max_index)
|
||||
else
|
||||
raise Out_of_int
|
||||
incr max_fresh;
|
||||
_make (2 * !max_fresh + 1)
|
||||
in
|
||||
let iter: (t -> unit) -> unit = fun f ->
|
||||
for j = 1 to !max_index do
|
||||
|
|
@ -45,10 +45,11 @@ module Fsat = struct
|
|||
in
|
||||
create, iter
|
||||
|
||||
let fresh = create
|
||||
|
||||
let print fmt a =
|
||||
Format.fprintf fmt "%s%d" (if a < 0 then "~" else "") (abs a)
|
||||
Format.fprintf fmt "%s%s%d"
|
||||
(if a < 0 then "~" else "")
|
||||
(if a mod 2 = 0 then "v" else "f")
|
||||
((abs a) / 2)
|
||||
|
||||
end
|
||||
|
||||
|
|
@ -90,14 +91,14 @@ module Make(Dummy : sig end) = struct
|
|||
|
||||
let new_atom () =
|
||||
try
|
||||
Fsat.create ()
|
||||
with Fsat.Out_of_int ->
|
||||
Fsat.fresh ()
|
||||
with Fsat.Dummy _ ->
|
||||
raise Bad_atom
|
||||
|
||||
let make i =
|
||||
try
|
||||
Fsat.make i
|
||||
with Fsat.Dummy ->
|
||||
with Fsat.Dummy _ ->
|
||||
raise Bad_atom
|
||||
|
||||
let neg = Fsat.neg
|
||||
|
|
|
|||
|
|
@ -44,50 +44,14 @@ module Make (F : Formula_intf.S) = struct
|
|||
else if List.mem (make Not [c]) env then Some false
|
||||
else None
|
||||
|
||||
(*
|
||||
let rec lift_ite env op l =
|
||||
try
|
||||
let left, (c, t1, t2), right = Term.first_ite l in
|
||||
begin
|
||||
match value env c with
|
||||
| Some true ->
|
||||
lift_ite (c::env) op (left@(t1::right))
|
||||
| Some false ->
|
||||
lift_ite ((make Not [c])::env) op (left@(t2::right))
|
||||
| None ->
|
||||
Comb
|
||||
(And,
|
||||
[Comb
|
||||
(Imp, [c; lift_ite (c::env) op (left@(t1::right))]);
|
||||
Comb (Imp,
|
||||
[(make Not [c]);
|
||||
lift_ite
|
||||
((make Not [c])::env) op (left@(t2::right))])])
|
||||
end
|
||||
with Not_found ->
|
||||
begin
|
||||
let lit =
|
||||
match op, l with
|
||||
| Eq, [Term.T t1; Term.T t2] ->
|
||||
Literal.Eq (t1, t2)
|
||||
| Neq, ts ->
|
||||
let ts =
|
||||
List.rev_map (function Term.T x -> x | _ -> assert false) ts in
|
||||
Literal.Distinct (false, ts)
|
||||
| Le, [Term.T t1; Term.T t2] ->
|
||||
Literal.Builtin (true, Hstring.make "<=", [t1; t2])
|
||||
| Lt, [Term.T t1; Term.T t2] ->
|
||||
Literal.Builtin (true, Hstring.make "<", [t1; t2])
|
||||
| _ -> assert false
|
||||
in
|
||||
Lit (F.make lit)
|
||||
end
|
||||
|
||||
let make_lit op l = lift_ite [] op l
|
||||
*)
|
||||
|
||||
let make_atom p = Lit p
|
||||
|
||||
let atomic_true = F.fresh ()
|
||||
let atomic_false = F.neg atomic_true
|
||||
|
||||
let f_true = make_atom atomic_true
|
||||
let f_false = make_atom atomic_false
|
||||
|
||||
let make_not f = make Not [f]
|
||||
let make_and l = make And l
|
||||
let make_imply f1 f2 = make Imp [f1; f2]
|
||||
|
|
@ -95,6 +59,11 @@ module Make (F : Formula_intf.S) = struct
|
|||
let make_xor f1 f2 = make Or [ make And [ make Not [f1]; f2 ];
|
||||
make And [ f1; make Not [f2] ] ]
|
||||
|
||||
let make_or = function
|
||||
| [] -> raise Empty_Or
|
||||
| [a] -> a
|
||||
| l -> Comb (Or, l)
|
||||
|
||||
(* simplify formula *)
|
||||
let rec sform = function
|
||||
| Comb (Not, [Lit a]) -> Lit (F.neg a)
|
||||
|
|
@ -116,15 +85,26 @@ module Make (F : Formula_intf.S) = struct
|
|||
| Comb ((Imp | Not), _) -> assert false
|
||||
| Lit _ as f -> f
|
||||
|
||||
let rec simplify_clause acc = function
|
||||
| [] -> Some acc
|
||||
| a :: r when F.equal atomic_true a -> None
|
||||
| a :: r when F.equal atomic_false a ->
|
||||
simplify_clause acc r
|
||||
| a :: r -> simplify_clause (a :: acc) r
|
||||
|
||||
let rec rev_opt_map f acc = function
|
||||
| [] -> acc
|
||||
| a :: r -> begin match f a with
|
||||
| None -> rev_opt_map f acc r
|
||||
| Some b -> rev_opt_map f (b :: acc) r
|
||||
end
|
||||
|
||||
let simplify_cnf = rev_opt_map (simplify_clause []) []
|
||||
|
||||
let ( @@ ) l1 l2 = List.rev_append l1 l2
|
||||
let ( @ ) = `Use_rev_append_instead (* prevent use of non-tailrec append *)
|
||||
|
||||
let make_or = function
|
||||
| [] -> raise Empty_Or
|
||||
| [a] -> a
|
||||
| l -> Comb (Or, l)
|
||||
|
||||
(*
|
||||
let distrib l_and l_or =
|
||||
let l =
|
||||
if l_or = [] then l_and
|
||||
|
|
@ -218,18 +198,9 @@ module Make (F : Formula_intf.S) = struct
|
|||
let make_cnf f =
|
||||
let sfnc = cnf (sform f) in
|
||||
init [] sfnc
|
||||
*)
|
||||
|
||||
let mk_proxy = F.fresh
|
||||
(*
|
||||
let cpt = ref 0 in
|
||||
fun () ->
|
||||
let t = AETerm.make
|
||||
(Symbols.name (Hstring.make ("PROXY__"^(string_of_int !cpt))))
|
||||
[] Ty.Tbool
|
||||
in
|
||||
incr cpt;
|
||||
F.make (Literal.Eq (t, AETerm.true_))
|
||||
*)
|
||||
|
||||
let acc_or = ref []
|
||||
let acc_and = ref []
|
||||
|
|
|
|||
|
|
@ -16,6 +16,9 @@ module type S = sig
|
|||
type t
|
||||
type atom
|
||||
|
||||
val f_true : t
|
||||
val f_false : t
|
||||
|
||||
val make_atom : atom -> t
|
||||
(** [make_pred p] builds the atomic formula [p = true].
|
||||
@param sign the polarity of the atomic formula *)
|
||||
|
|
@ -32,6 +35,10 @@ module type S = sig
|
|||
list (which is a conjunction) of lists (which are disjunctions) of
|
||||
literals. *)
|
||||
|
||||
val simplify_cnf : atom list list -> atom list list
|
||||
(** Simplifies the cnf given as argument : eliminates 'false' atoms, and eliminates clauses
|
||||
with the 'true' atom *)
|
||||
|
||||
val print : Format.formatter -> t -> unit
|
||||
(** [print fmt f] prints the formula on the formatter [fmt].*)
|
||||
|
||||
|
|
|
|||
4
tests/sat/test-002.smt2
Normal file
4
tests/sat/test-002.smt2
Normal file
|
|
@ -0,0 +1,4 @@
|
|||
(declare-fun a () Bool)
|
||||
(declare-fun b () Bool)
|
||||
(assert (or a b))
|
||||
(check-sat)
|
||||
5
tests/unsat/test-000.cnf
Normal file
5
tests/unsat/test-000.cnf
Normal file
|
|
@ -0,0 +1,5 @@
|
|||
c First test
|
||||
p cnf 0 0
|
||||
1 0
|
||||
-1 2 0
|
||||
-1 -2 0
|
||||
4
tests/unsat/test-003.smt2
Normal file
4
tests/unsat/test-003.smt2
Normal file
|
|
@ -0,0 +1,4 @@
|
|||
(declare-fun a () Bool)
|
||||
(declare-fun b () Bool)
|
||||
(assert (and (or a b) (and (not a) (not b))))
|
||||
(check-sat)
|
||||
4
tests/unsat/test-004.smt2
Normal file
4
tests/unsat/test-004.smt2
Normal file
|
|
@ -0,0 +1,4 @@
|
|||
(declare-fun a () Bool)
|
||||
(declare-fun b () Bool)
|
||||
(assert (and (or a b) (not a) (not b)))
|
||||
(check-sat)
|
||||
|
|
@ -1,9 +1,11 @@
|
|||
S ./
|
||||
S ./smtlib/
|
||||
S ../sat/
|
||||
S ../common/
|
||||
|
||||
B ../_build/
|
||||
B ../_build/util/
|
||||
B ../_build/util/smtlib/
|
||||
B ../_build/sat/
|
||||
B ../_build/smt/
|
||||
B ../_build/common/
|
||||
|
|
|
|||
|
|
@ -8,6 +8,7 @@ exception Out_of_space
|
|||
(* Types for input/output languages *)
|
||||
type sat_input =
|
||||
| Dimacs
|
||||
| Smtlib
|
||||
|
||||
type sat_output =
|
||||
| Standard (* Only output problem status *)
|
||||
|
|
@ -18,6 +19,7 @@ let output = ref Standard
|
|||
|
||||
let input_list = [
|
||||
"dimacs", Dimacs;
|
||||
"smtlib", Smtlib;
|
||||
]
|
||||
let output_list = [
|
||||
"dot", Dot;
|
||||
|
|
@ -38,8 +40,13 @@ let set_input s = set_io "Input" s input input_list
|
|||
let set_output s = set_io "Output" s output output_list
|
||||
|
||||
(* Input Parsing *)
|
||||
let rec rev_flat_map f acc = function
|
||||
| [] -> acc
|
||||
| a :: r -> rev_flat_map f (List.rev_append (f a) acc) r
|
||||
|
||||
let parse_input file = match !input with
|
||||
| Dimacs -> List.rev_map (List.rev_map S.make) (Parser.parse file)
|
||||
| Dimacs -> List.rev_map (List.rev_map S.make) (Parsedimacs.parse file)
|
||||
| Smtlib -> Sat.Tseitin.simplify_cnf (rev_flat_map Sat.Tseitin.make_cnf [] (Smtlib.parse file))
|
||||
|
||||
(* Printing wrappers *)
|
||||
let std = Format.std_formatter
|
||||
|
|
|
|||
9
util/smtlib/.merlin
Normal file
9
util/smtlib/.merlin
Normal file
|
|
@ -0,0 +1,9 @@
|
|||
S ./
|
||||
S ../
|
||||
S ../../sat/
|
||||
|
||||
B ../../_build/
|
||||
B ../../_build/util/
|
||||
B ../../_build/util/smtlib/
|
||||
B ../../_build/sat/
|
||||
B ../../_build/smt/
|
||||
3
util/smtlib/lexsmtlib.mli
Normal file
3
util/smtlib/lexsmtlib.mli
Normal file
|
|
@ -0,0 +1,3 @@
|
|||
(* Copyright 2014 INIA *)
|
||||
|
||||
val token : Lexing.lexbuf -> Parsesmtlib.token
|
||||
48
util/smtlib/lexsmtlib.mll
Normal file
48
util/smtlib/lexsmtlib.mll
Normal file
|
|
@ -0,0 +1,48 @@
|
|||
{
|
||||
(* auto-generated by gt *)
|
||||
|
||||
open Parsesmtlib;;
|
||||
}
|
||||
|
||||
rule token = parse
|
||||
| ['\t' ' ' ]+ { token lexbuf }
|
||||
| ';' (_ # '\n')* { token lexbuf }
|
||||
| ['\n']+ as str { Smtlib_util.line := (!Smtlib_util.line + (String.length str)); token lexbuf }
|
||||
| "_" { UNDERSCORE }
|
||||
| "(" { LPAREN }
|
||||
| ")" { RPAREN }
|
||||
| "as" { AS }
|
||||
| "let" { LET }
|
||||
| "forall" { FORALL }
|
||||
| "exists" { EXISTS }
|
||||
| "!" { EXCLIMATIONPT }
|
||||
| "set-logic" { SETLOGIC }
|
||||
| "set-option" { SETOPTION }
|
||||
| "set-info" { SETINFO }
|
||||
| "declare-sort" { DECLARESORT }
|
||||
| "define-sort" { DEFINESORT }
|
||||
| "declare-fun" { DECLAREFUN }
|
||||
| "define-fun" { DEFINEFUN }
|
||||
| "push" { PUSH }
|
||||
| "pop" { POP }
|
||||
| "assert" { ASSERT }
|
||||
| "check-sat" { CHECKSAT }
|
||||
| "get-assertions" { GETASSERT }
|
||||
| "get-proof" { GETPROOF }
|
||||
| "get-unsat-core" { GETUNSATCORE }
|
||||
| "get-value" { GETVALUE }
|
||||
| "get-assignment" { GETASSIGN }
|
||||
| "get-option" { GETOPTION }
|
||||
| "get-info" { GETINFO }
|
||||
| "exit" { EXIT }
|
||||
| '#' 'x' ['0'-'9' 'A'-'F' 'a'-'f']+ as str { HEXADECIMAL(str) }
|
||||
| '#' 'b' ['0'-'1']+ as str { BINARY(str) }
|
||||
| '|' ([ '!'-'~' ' ' '\n' '\t' '\r'] # ['\\' '|'])* '|' as str { ASCIIWOR(str) }
|
||||
| ':' ['a'-'z' 'A'-'Z' '0'-'9' '+' '-' '/' '*' '=' '%' '?' '!' '.' '$' '_' '~' '&' '^' '<' '>' '@']+ as str { KEYWORD(str) }
|
||||
| ['a'-'z' 'A'-'Z' '+' '-' '/' '*' '=''%' '?' '!' '.' '$' '_' '~' '&' '^' '<' '>' '@'] ['a'-'z' 'A'-'Z' '0'-'9' '+' '-' '/' '*' '=''%' '?' '!' '.' '$' '_' '~' '&' '^' '<' '>' '@']* as str { SYMBOL(str) }
|
||||
| '"' (([ '!'-'~' ' ' '\n' '\t' '\r' ] # ['\\' '"']) | ('\\' ['!'-'~' ' ' '\n' '\t' '\r'] ))* '"' as str { STRINGLIT(str) }
|
||||
| ( '0' | ['1'-'9'] ['0'-'9']* ) as str { NUMERAL(str) }
|
||||
| ( '0' | ['1'-'9'] ['0'-'9']* ) '.' ['0'-'9']+ as str { DECIMAL(str) }
|
||||
| eof { EOF }
|
||||
| _ {failwith((Lexing.lexeme lexbuf) ^
|
||||
": lexing error on line "^(string_of_int !Smtlib_util.line))}{}
|
||||
330
util/smtlib/parsesmtlib.mly
Normal file
330
util/smtlib/parsesmtlib.mly
Normal file
|
|
@ -0,0 +1,330 @@
|
|||
%{
|
||||
(* auto-generated by gt *)
|
||||
|
||||
open Smtlib_syntax;;
|
||||
let parse_error s =
|
||||
print_string s;
|
||||
print_string " on line ";
|
||||
print_int !Smtlib_util.line;
|
||||
print_string "\n";;
|
||||
|
||||
%}
|
||||
|
||||
%start main
|
||||
|
||||
%token EOF AS ASSERT CHECKSAT DECLAREFUN DECLARESORT DEFINEFUN DEFINESORT EXCLIMATIONPT EXISTS EXIT FORALL GETASSERT GETASSIGN GETINFO GETOPTION GETPROOF GETUNSATCORE GETVALUE LET LPAREN POP PUSH RPAREN SETINFO SETLOGIC SETOPTION UNDERSCORE
|
||||
%token <string> ASCIIWOR BINARY DECIMAL HEXADECIMAL KEYWORD NUMERAL STRINGLIT SYMBOL
|
||||
|
||||
%type <Smtlib_syntax.commands option> main
|
||||
|
||||
%type <Smtlib_syntax.an_option> an_option
|
||||
|
||||
%type <Smtlib_syntax.attribute> attribute
|
||||
|
||||
%type <Smtlib_syntax.attributevalsexpr_attributevalue_sexpr5> attributevalsexpr_attributevalue_sexpr5
|
||||
|
||||
%type <Smtlib_syntax.attributevalue> attributevalue
|
||||
|
||||
%type <Smtlib_syntax.command> command
|
||||
|
||||
%type <Smtlib_syntax.commanddeclarefun_command_sort13> commanddeclarefun_command_sort13
|
||||
|
||||
%type <Smtlib_syntax.commanddefinefun_command_sortedvar15> commanddefinefun_command_sortedvar15
|
||||
|
||||
%type <Smtlib_syntax.commanddefinesort_command_symbol11> commanddefinesort_command_symbol11
|
||||
|
||||
%type <Smtlib_syntax.commandgetvalue_command_term24> commandgetvalue_command_term24
|
||||
|
||||
%type <Smtlib_syntax.commands> commands
|
||||
|
||||
%type <Smtlib_syntax.commands_commands_command30> commands_commands_command30
|
||||
|
||||
%type <Smtlib_syntax.identifier> identifier
|
||||
|
||||
%type <Smtlib_syntax.idunderscoresymnum_identifier_numeral33> idunderscoresymnum_identifier_numeral33
|
||||
|
||||
%type <Smtlib_syntax.infoflag> infoflag
|
||||
|
||||
%type <Smtlib_syntax.qualidentifier> qualidentifier
|
||||
|
||||
%type <Smtlib_syntax.sexpr> sexpr
|
||||
|
||||
%type <Smtlib_syntax.sexprinparen_sexpr_sexpr41> sexprinparen_sexpr_sexpr41
|
||||
|
||||
%type <Smtlib_syntax.sort> sort
|
||||
|
||||
%type <Smtlib_syntax.sortedvar> sortedvar
|
||||
|
||||
%type <Smtlib_syntax.sortidsortmulti_sort_sort44> sortidsortmulti_sort_sort44
|
||||
|
||||
%type <Smtlib_syntax.specconstant> specconstant
|
||||
|
||||
%type <Smtlib_syntax.symbol> symbol
|
||||
|
||||
%type <Smtlib_syntax.term> term
|
||||
|
||||
%type <Smtlib_syntax.termexclimationpt_term_attribute64> termexclimationpt_term_attribute64
|
||||
|
||||
%type <Smtlib_syntax.termexiststerm_term_sortedvar62> termexiststerm_term_sortedvar62
|
||||
|
||||
%type <Smtlib_syntax.termforallterm_term_sortedvar60> termforallterm_term_sortedvar60
|
||||
|
||||
%type <Smtlib_syntax.termletterm_term_varbinding58> termletterm_term_varbinding58
|
||||
|
||||
%type <Smtlib_syntax.termqualidterm_term_term56> termqualidterm_term_term56
|
||||
|
||||
%type <Smtlib_syntax.varbinding> varbinding
|
||||
|
||||
%type <Smtlib_util.pd> cur_position
|
||||
|
||||
%%
|
||||
|
||||
main:
|
||||
| commands { Some($1) }
|
||||
| EOF { None }
|
||||
|
||||
cur_position:
|
||||
| { Smtlib_util.cur_pd() }
|
||||
|
||||
an_option:
|
||||
| attribute { AnOptionAttribute(pd_attribute $1, $1) }
|
||||
|
||||
attribute:
|
||||
| cur_position KEYWORD { AttributeKeyword($1, $2) }
|
||||
|
||||
attribute:
|
||||
| cur_position KEYWORD attributevalue { AttributeKeywordValue($1, $2, $3) }
|
||||
|
||||
attributevalue:
|
||||
| specconstant { AttributeValSpecConst(pd_specconstant $1, $1) }
|
||||
|
||||
attributevalue:
|
||||
| symbol { AttributeValSymbol(pd_symbol $1, $1) }
|
||||
|
||||
attributevalue:
|
||||
| cur_position LPAREN attributevalsexpr_attributevalue_sexpr5 RPAREN { AttributeValSexpr($1, $3) }
|
||||
|
||||
command:
|
||||
| cur_position LPAREN SETLOGIC symbol RPAREN { CommandSetLogic($1, $4) }
|
||||
|
||||
command:
|
||||
| cur_position LPAREN SETOPTION an_option RPAREN { CommandSetOption($1, $4) }
|
||||
|
||||
command:
|
||||
| cur_position LPAREN SETINFO attribute RPAREN { CommandSetInfo($1, $4) }
|
||||
|
||||
command:
|
||||
| cur_position LPAREN DECLARESORT symbol NUMERAL RPAREN { CommandDeclareSort($1, $4, $5) }
|
||||
|
||||
command:
|
||||
| cur_position LPAREN DEFINESORT symbol LPAREN commanddefinesort_command_symbol11 RPAREN sort RPAREN { CommandDefineSort($1, $4, $6, $8) }
|
||||
|
||||
command:
|
||||
| cur_position LPAREN DECLAREFUN symbol LPAREN commanddeclarefun_command_sort13 RPAREN sort RPAREN { CommandDeclareFun($1, $4, $6, $8) }
|
||||
|
||||
command:
|
||||
| cur_position LPAREN DEFINEFUN symbol LPAREN commanddefinefun_command_sortedvar15 RPAREN sort term RPAREN { CommandDefineFun($1, $4, $6, $8, $9) }
|
||||
|
||||
command:
|
||||
| cur_position LPAREN PUSH NUMERAL RPAREN { CommandPush($1, $4) }
|
||||
|
||||
command:
|
||||
| cur_position LPAREN POP NUMERAL RPAREN { CommandPop($1, $4) }
|
||||
|
||||
command:
|
||||
| cur_position LPAREN ASSERT term RPAREN { CommandAssert($1, $4) }
|
||||
|
||||
command:
|
||||
| cur_position LPAREN CHECKSAT RPAREN { CommandCheckSat($1) }
|
||||
|
||||
command:
|
||||
| cur_position LPAREN GETASSERT RPAREN { CommandGetAssert($1) }
|
||||
|
||||
command:
|
||||
| cur_position LPAREN GETPROOF RPAREN { CommandGetProof($1) }
|
||||
|
||||
command:
|
||||
| cur_position LPAREN GETUNSATCORE RPAREN { CommandGetUnsatCore($1) }
|
||||
|
||||
command:
|
||||
| cur_position LPAREN GETVALUE LPAREN commandgetvalue_command_term24 RPAREN RPAREN { CommandGetValue($1, $5) }
|
||||
|
||||
command:
|
||||
| cur_position LPAREN GETASSIGN RPAREN { CommandGetAssign($1) }
|
||||
|
||||
command:
|
||||
| cur_position LPAREN GETOPTION KEYWORD RPAREN { CommandGetOption($1, $4) }
|
||||
|
||||
command:
|
||||
| cur_position LPAREN GETINFO infoflag RPAREN { CommandGetInfo($1, $4) }
|
||||
|
||||
command:
|
||||
| cur_position LPAREN EXIT RPAREN { CommandExit($1) }
|
||||
|
||||
commands:
|
||||
| commands_commands_command30 { Commands(pd_commands_commands_command30 $1, $1) }
|
||||
|
||||
identifier:
|
||||
| symbol { IdSymbol(pd_symbol $1, $1) }
|
||||
|
||||
identifier:
|
||||
| cur_position LPAREN UNDERSCORE symbol idunderscoresymnum_identifier_numeral33 RPAREN { IdUnderscoreSymNum($1, $4, $5) }
|
||||
|
||||
infoflag:
|
||||
| cur_position KEYWORD { InfoFlagKeyword($1, $2) }
|
||||
|
||||
qualidentifier:
|
||||
| identifier { QualIdentifierId(pd_identifier $1, $1) }
|
||||
|
||||
qualidentifier:
|
||||
| cur_position LPAREN AS identifier sort RPAREN { QualIdentifierAs($1, $4, $5) }
|
||||
|
||||
sexpr:
|
||||
| specconstant { SexprSpecConst(pd_specconstant $1, $1) }
|
||||
|
||||
sexpr:
|
||||
| symbol { SexprSymbol(pd_symbol $1, $1) }
|
||||
|
||||
sexpr:
|
||||
| cur_position KEYWORD { SexprKeyword($1, $2) }
|
||||
|
||||
sexpr:
|
||||
| cur_position LPAREN sexprinparen_sexpr_sexpr41 RPAREN { SexprInParen($1, $3) }
|
||||
|
||||
sort:
|
||||
| identifier { SortIdentifier(pd_identifier $1, $1) }
|
||||
|
||||
sort:
|
||||
| cur_position LPAREN identifier sortidsortmulti_sort_sort44 RPAREN { SortIdSortMulti($1, $3, $4) }
|
||||
|
||||
sortedvar:
|
||||
| cur_position LPAREN symbol sort RPAREN { SortedVarSymSort($1, $3, $4) }
|
||||
|
||||
specconstant:
|
||||
| cur_position DECIMAL { SpecConstsDec($1, $2) }
|
||||
|
||||
specconstant:
|
||||
| cur_position NUMERAL { SpecConstNum($1, $2) }
|
||||
|
||||
specconstant:
|
||||
| cur_position STRINGLIT { SpecConstString($1, $2) }
|
||||
|
||||
specconstant:
|
||||
| cur_position HEXADECIMAL { SpecConstsHex($1, $2) }
|
||||
|
||||
specconstant:
|
||||
| cur_position BINARY { SpecConstsBinary($1, $2) }
|
||||
|
||||
symbol:
|
||||
| cur_position SYMBOL { Symbol($1, $2) }
|
||||
|
||||
symbol:
|
||||
| cur_position ASCIIWOR { SymbolWithOr($1, $2) }
|
||||
|
||||
term:
|
||||
| specconstant { TermSpecConst(pd_specconstant $1, $1) }
|
||||
|
||||
term:
|
||||
| qualidentifier { TermQualIdentifier(pd_qualidentifier $1, $1) }
|
||||
|
||||
term:
|
||||
| cur_position LPAREN qualidentifier termqualidterm_term_term56 RPAREN { TermQualIdTerm($1, $3, $4) }
|
||||
|
||||
term:
|
||||
| cur_position LPAREN LET LPAREN termletterm_term_varbinding58 RPAREN term RPAREN { TermLetTerm($1, $5, $7) }
|
||||
|
||||
term:
|
||||
| cur_position LPAREN FORALL LPAREN termforallterm_term_sortedvar60 RPAREN term RPAREN { TermForAllTerm($1, $5, $7) }
|
||||
|
||||
term:
|
||||
| cur_position LPAREN EXISTS LPAREN termexiststerm_term_sortedvar62 RPAREN term RPAREN { TermExistsTerm($1, $5, $7) }
|
||||
|
||||
term:
|
||||
| cur_position LPAREN EXCLIMATIONPT term termexclimationpt_term_attribute64 RPAREN { TermExclimationPt($1, $4, $5) }
|
||||
|
||||
varbinding:
|
||||
| cur_position LPAREN symbol term RPAREN { VarBindingSymTerm($1, $3, $4) }
|
||||
|
||||
termexclimationpt_term_attribute64:
|
||||
| attribute { (pd_attribute $1, ($1)::[]) }
|
||||
|
||||
termexclimationpt_term_attribute64:
|
||||
| attribute termexclimationpt_term_attribute64 { let (p, ( l1 )) = $2 in (pd_attribute $1, ($1)::(l1)) }
|
||||
|
||||
termexiststerm_term_sortedvar62:
|
||||
| sortedvar { (pd_sortedvar $1, ($1)::[]) }
|
||||
|
||||
termexiststerm_term_sortedvar62:
|
||||
| sortedvar termexiststerm_term_sortedvar62 { let (p, ( l1 )) = $2 in (pd_sortedvar $1, ($1)::(l1)) }
|
||||
|
||||
termforallterm_term_sortedvar60:
|
||||
| sortedvar { (pd_sortedvar $1, ($1)::[]) }
|
||||
|
||||
termforallterm_term_sortedvar60:
|
||||
| sortedvar termforallterm_term_sortedvar60 { let (p, ( l1 )) = $2 in (pd_sortedvar $1, ($1)::(l1)) }
|
||||
|
||||
termletterm_term_varbinding58:
|
||||
| varbinding { (pd_varbinding $1, ($1)::[]) }
|
||||
|
||||
termletterm_term_varbinding58:
|
||||
| varbinding termletterm_term_varbinding58 { let (p, ( l1 )) = $2 in (pd_varbinding $1, ($1)::(l1)) }
|
||||
|
||||
termqualidterm_term_term56:
|
||||
| term { (pd_term $1, ($1)::[]) }
|
||||
|
||||
termqualidterm_term_term56:
|
||||
| term termqualidterm_term_term56 { let (p, ( l1 )) = $2 in (pd_term $1, ($1)::(l1)) }
|
||||
|
||||
sortidsortmulti_sort_sort44:
|
||||
| sort { (pd_sort $1, ($1)::[]) }
|
||||
|
||||
sortidsortmulti_sort_sort44:
|
||||
| sort sortidsortmulti_sort_sort44 { let (p, ( l1 )) = $2 in (pd_sort $1, ($1)::(l1)) }
|
||||
|
||||
sexprinparen_sexpr_sexpr41:
|
||||
| cur_position { ($1, []) }
|
||||
|
||||
sexprinparen_sexpr_sexpr41:
|
||||
| sexpr sexprinparen_sexpr_sexpr41 { let (p, ( l1 )) = $2 in (pd_sexpr $1, ($1)::(l1)) }
|
||||
|
||||
idunderscoresymnum_identifier_numeral33:
|
||||
| cur_position NUMERAL { ($1, ($2)::[]) }
|
||||
|
||||
idunderscoresymnum_identifier_numeral33:
|
||||
| cur_position NUMERAL idunderscoresymnum_identifier_numeral33 { let (p, ( l1 )) = $3 in ($1, ($2)::(l1)) }
|
||||
|
||||
commands_commands_command30:
|
||||
| cur_position { ($1, []) }
|
||||
|
||||
commands_commands_command30:
|
||||
| command commands_commands_command30 { let (p, ( l1 )) = $2 in (pd_command $1, ($1)::(l1)) }
|
||||
|
||||
commandgetvalue_command_term24:
|
||||
| term { (pd_term $1, ($1)::[]) }
|
||||
|
||||
commandgetvalue_command_term24:
|
||||
| term commandgetvalue_command_term24 { let (p, ( l1 )) = $2 in (pd_term $1, ($1)::(l1)) }
|
||||
|
||||
commanddefinefun_command_sortedvar15:
|
||||
| cur_position { ($1, []) }
|
||||
|
||||
commanddefinefun_command_sortedvar15:
|
||||
| sortedvar commanddefinefun_command_sortedvar15 { let (p, ( l1 )) = $2 in (pd_sortedvar $1, ($1)::(l1)) }
|
||||
|
||||
commanddeclarefun_command_sort13:
|
||||
| cur_position { ($1, []) }
|
||||
|
||||
commanddeclarefun_command_sort13:
|
||||
| sort commanddeclarefun_command_sort13 { let (p, ( l1 )) = $2 in (pd_sort $1, ($1)::(l1)) }
|
||||
|
||||
commanddefinesort_command_symbol11:
|
||||
| cur_position { ($1, []) }
|
||||
|
||||
commanddefinesort_command_symbol11:
|
||||
| symbol commanddefinesort_command_symbol11 { let (p, ( l1 )) = $2 in (pd_symbol $1, ($1)::(l1)) }
|
||||
|
||||
attributevalsexpr_attributevalue_sexpr5:
|
||||
| cur_position { ($1, []) }
|
||||
|
||||
attributevalsexpr_attributevalue_sexpr5:
|
||||
| sexpr attributevalsexpr_attributevalue_sexpr5 { let (p, ( l1 )) = $2 in (pd_sexpr $1, ($1)::(l1)) }
|
||||
103
util/smtlib/smtlib.ml
Normal file
103
util/smtlib/smtlib.ml
Normal file
|
|
@ -0,0 +1,103 @@
|
|||
(* Copyright 2014 INRIA **)
|
||||
|
||||
open Smtlib_syntax
|
||||
|
||||
module F = Sat.Fsat
|
||||
module T = Sat.Tseitin
|
||||
|
||||
exception Bad_arity of string
|
||||
exception Unknown_command
|
||||
exception Incomplete_translation
|
||||
|
||||
(* Environment *)
|
||||
let env : (string, T.t) Hashtbl.t = Hashtbl.create 57;;
|
||||
Hashtbl.add env "true" T.f_true;;
|
||||
Hashtbl.add env "false" T.f_false;;
|
||||
|
||||
let get_var =
|
||||
fun s ->
|
||||
try
|
||||
Hashtbl.find env s
|
||||
with Not_found ->
|
||||
let f = T.make_atom (F.fresh ()) in
|
||||
Hashtbl.add env s f;
|
||||
f
|
||||
|
||||
(* Term translation *)
|
||||
let translate_const = function
|
||||
| SpecConstsDec(_, s)
|
||||
| SpecConstNum(_, s)
|
||||
| SpecConstString(_, s)
|
||||
| SpecConstsHex(_, s)
|
||||
| SpecConstsBinary(_, s) -> get_var s
|
||||
|
||||
let translate_symbol = function
|
||||
| Symbol(_, s)
|
||||
| SymbolWithOr(_, s) -> s
|
||||
|
||||
let translate_id = function
|
||||
| IdSymbol(_, s) -> translate_symbol s
|
||||
| IdUnderscoreSymNum(_, s, n) -> raise Incomplete_translation
|
||||
|
||||
let translate_sort = function
|
||||
| SortIdentifier(_, id) ->
|
||||
let s = translate_id id in
|
||||
if s <> "Bool" then raise Incomplete_translation
|
||||
| _ -> raise Incomplete_translation
|
||||
|
||||
let translate_qualid = function
|
||||
| QualIdentifierId(_, id) -> translate_id id
|
||||
| QualIdentifierAs(_, id, s) -> raise Incomplete_translation
|
||||
|
||||
let left_assoc s f = function
|
||||
| x :: r -> List.fold_left f x r
|
||||
| _ -> raise (Bad_arity s)
|
||||
|
||||
let right_assoc s f = function
|
||||
| x :: r -> List.fold_right f r x
|
||||
| _ -> raise (Bad_arity s)
|
||||
|
||||
let rec translate_term = function
|
||||
| TermSpecConst(_, const) -> translate_const const
|
||||
| TermQualIdentifier(_, id) -> get_var (translate_qualid id)
|
||||
| TermQualIdTerm(_, f, (_, l)) ->
|
||||
begin match (translate_qualid f), (List.map translate_term l) with
|
||||
(* CORE theory translation - '=', 'distinct','ite' not yet implemented *)
|
||||
| "not", [e] -> T.make_not e
|
||||
| "not", _ -> raise (Bad_arity "not")
|
||||
| "and" as s, l -> T.make_and l
|
||||
| "or" as s, l -> T.make_or l
|
||||
| "xor" as s, l -> left_assoc s T.make_xor l
|
||||
| "=>" as s, l -> right_assoc s T.make_imply l
|
||||
| _ -> raise Unknown_command
|
||||
end
|
||||
| _ -> raise Incomplete_translation
|
||||
|
||||
(* Command Translation *)
|
||||
let translate_command = function
|
||||
| CommandDeclareFun(_, s, (_, []), ret) ->
|
||||
ignore (translate_sort ret);
|
||||
ignore (get_var (translate_symbol s));
|
||||
None
|
||||
| CommandAssert(_, t) ->
|
||||
Some (translate_term t)
|
||||
| _ -> None
|
||||
|
||||
let rec translate_command_list acc = function
|
||||
| [] -> acc
|
||||
| c :: r ->
|
||||
begin match translate_command c with
|
||||
| None -> translate_command_list acc r
|
||||
| Some t -> translate_command_list (t :: acc) r
|
||||
end
|
||||
|
||||
let translate = function
|
||||
| Some Commands (_, (_, l)) -> List.rev (translate_command_list [] l)
|
||||
| None -> []
|
||||
|
||||
let parse file =
|
||||
let f = open_in file in
|
||||
let lexbuf = Lexing.from_channel f in
|
||||
let commands = Parsesmtlib.main Lexsmtlib.token lexbuf in
|
||||
close_in f;
|
||||
translate commands
|
||||
3
util/smtlib/smtlib.mli
Normal file
3
util/smtlib/smtlib.mli
Normal file
|
|
@ -0,0 +1,3 @@
|
|||
(* Copyright 2014 INRIA *)
|
||||
|
||||
val parse : string -> Sat.Tseitin.t list
|
||||
229
util/smtlib/smtlib_syntax.ml
Normal file
229
util/smtlib/smtlib_syntax.ml
Normal file
|
|
@ -0,0 +1,229 @@
|
|||
(* auto-generated by gt *)
|
||||
|
||||
open Smtlib_util;;
|
||||
|
||||
type dummy = Dummy
|
||||
and an_option = | AnOptionAttribute of pd * attribute
|
||||
and attribute = | AttributeKeyword of pd * string | AttributeKeywordValue of pd * string * attributevalue
|
||||
and attributevalue = | AttributeValSpecConst of pd * specconstant | AttributeValSymbol of pd * symbol | AttributeValSexpr of pd * attributevalsexpr_attributevalue_sexpr5
|
||||
and command = | CommandSetLogic of pd * symbol | CommandSetOption of pd * an_option | CommandSetInfo of pd * attribute | CommandDeclareSort of pd * symbol * string | CommandDefineSort of pd * symbol * commanddefinesort_command_symbol11 * sort | CommandDeclareFun of pd * symbol * commanddeclarefun_command_sort13 * sort | CommandDefineFun of pd * symbol * commanddefinefun_command_sortedvar15 * sort * term | CommandPush of pd * string | CommandPop of pd * string | CommandAssert of pd * term | CommandCheckSat of pd | CommandGetAssert of pd | CommandGetProof of pd | CommandGetUnsatCore of pd | CommandGetValue of pd * commandgetvalue_command_term24 | CommandGetAssign of pd | CommandGetOption of pd * string | CommandGetInfo of pd * infoflag | CommandExit of pd
|
||||
and commands = | Commands of pd * commands_commands_command30
|
||||
and identifier = | IdSymbol of pd * symbol | IdUnderscoreSymNum of pd * symbol * idunderscoresymnum_identifier_numeral33
|
||||
and infoflag = | InfoFlagKeyword of pd * string
|
||||
and qualidentifier = | QualIdentifierId of pd * identifier | QualIdentifierAs of pd * identifier * sort
|
||||
and sexpr = | SexprSpecConst of pd * specconstant | SexprSymbol of pd * symbol | SexprKeyword of pd * string | SexprInParen of pd * sexprinparen_sexpr_sexpr41
|
||||
and sort = | SortIdentifier of pd * identifier | SortIdSortMulti of pd * identifier * sortidsortmulti_sort_sort44
|
||||
and sortedvar = | SortedVarSymSort of pd * symbol * sort
|
||||
and specconstant = | SpecConstsDec of pd * string | SpecConstNum of pd * string | SpecConstString of pd * string | SpecConstsHex of pd * string | SpecConstsBinary of pd * string
|
||||
and symbol = | Symbol of pd * string | SymbolWithOr of pd * string
|
||||
and term = | TermSpecConst of pd * specconstant | TermQualIdentifier of pd * qualidentifier | TermQualIdTerm of pd * qualidentifier * termqualidterm_term_term56 | TermLetTerm of pd * termletterm_term_varbinding58 * term | TermForAllTerm of pd * termforallterm_term_sortedvar60 * term | TermExistsTerm of pd * termexiststerm_term_sortedvar62 * term | TermExclimationPt of pd * term * termexclimationpt_term_attribute64
|
||||
and varbinding = | VarBindingSymTerm of pd * symbol * term
|
||||
and termexclimationpt_term_attribute64 = pd * ( attribute) list
|
||||
and termexiststerm_term_sortedvar62 = pd * ( sortedvar) list
|
||||
and termforallterm_term_sortedvar60 = pd * ( sortedvar) list
|
||||
and termletterm_term_varbinding58 = pd * ( varbinding) list
|
||||
and termqualidterm_term_term56 = pd * ( term) list
|
||||
and sortidsortmulti_sort_sort44 = pd * ( sort) list
|
||||
and sexprinparen_sexpr_sexpr41 = pd * ( sexpr) list
|
||||
and idunderscoresymnum_identifier_numeral33 = pd * ( string) list
|
||||
and commands_commands_command30 = pd * ( command) list
|
||||
and commandgetvalue_command_term24 = pd * ( term) list
|
||||
and commanddefinefun_command_sortedvar15 = pd * ( sortedvar) list
|
||||
and commanddeclarefun_command_sort13 = pd * ( sort) list
|
||||
and commanddefinesort_command_symbol11 = pd * ( symbol) list
|
||||
and attributevalsexpr_attributevalue_sexpr5 = pd * ( sexpr) list;;
|
||||
|
||||
(* pd stands for pos (position) and extradata *)
|
||||
let rec dummy () = ()
|
||||
and pd_an_option = function
|
||||
| AnOptionAttribute(d,_) -> d
|
||||
|
||||
and pd_attribute = function
|
||||
| AttributeKeyword(d,_) -> d
|
||||
|
||||
| AttributeKeywordValue(d,_,_) -> d
|
||||
|
||||
and pd_attributevalue = function
|
||||
| AttributeValSpecConst(d,_) -> d
|
||||
|
||||
| AttributeValSymbol(d,_) -> d
|
||||
|
||||
| AttributeValSexpr(d,_) -> d
|
||||
|
||||
and pd_command = function
|
||||
| CommandSetLogic(d,_) -> d
|
||||
|
||||
| CommandSetOption(d,_) -> d
|
||||
|
||||
| CommandSetInfo(d,_) -> d
|
||||
|
||||
| CommandDeclareSort(d,_,_) -> d
|
||||
|
||||
| CommandDefineSort(d,_,_,_) -> d
|
||||
|
||||
| CommandDeclareFun(d,_,_,_) -> d
|
||||
|
||||
| CommandDefineFun(d,_,_,_,_) -> d
|
||||
|
||||
| CommandPush(d,_) -> d
|
||||
|
||||
| CommandPop(d,_) -> d
|
||||
|
||||
| CommandAssert(d,_) -> d
|
||||
|
||||
| CommandCheckSat(d) -> d
|
||||
|
||||
| CommandGetAssert(d) -> d
|
||||
|
||||
| CommandGetProof(d) -> d
|
||||
|
||||
| CommandGetUnsatCore(d) -> d
|
||||
|
||||
| CommandGetValue(d,_) -> d
|
||||
|
||||
| CommandGetAssign(d) -> d
|
||||
|
||||
| CommandGetOption(d,_) -> d
|
||||
|
||||
| CommandGetInfo(d,_) -> d
|
||||
|
||||
| CommandExit(d) -> d
|
||||
|
||||
and pd_commands = function
|
||||
| Commands(d,_) -> d
|
||||
|
||||
and pd_identifier = function
|
||||
| IdSymbol(d,_) -> d
|
||||
|
||||
| IdUnderscoreSymNum(d,_,_) -> d
|
||||
|
||||
and pd_infoflag = function
|
||||
| InfoFlagKeyword(d,_) -> d
|
||||
|
||||
and pd_qualidentifier = function
|
||||
| QualIdentifierId(d,_) -> d
|
||||
|
||||
| QualIdentifierAs(d,_,_) -> d
|
||||
|
||||
and pd_sexpr = function
|
||||
| SexprSpecConst(d,_) -> d
|
||||
|
||||
| SexprSymbol(d,_) -> d
|
||||
|
||||
| SexprKeyword(d,_) -> d
|
||||
|
||||
| SexprInParen(d,_) -> d
|
||||
|
||||
and pd_sort = function
|
||||
| SortIdentifier(d,_) -> d
|
||||
|
||||
| SortIdSortMulti(d,_,_) -> d
|
||||
|
||||
and pd_sortedvar = function
|
||||
| SortedVarSymSort(d,_,_) -> d
|
||||
|
||||
and pd_specconstant = function
|
||||
| SpecConstsDec(d,_) -> d
|
||||
|
||||
| SpecConstNum(d,_) -> d
|
||||
|
||||
| SpecConstString(d,_) -> d
|
||||
|
||||
| SpecConstsHex(d,_) -> d
|
||||
|
||||
| SpecConstsBinary(d,_) -> d
|
||||
|
||||
and pd_symbol = function
|
||||
| Symbol(d,_) -> d
|
||||
|
||||
| SymbolWithOr(d,_) -> d
|
||||
|
||||
and pd_term = function
|
||||
| TermSpecConst(d,_) -> d
|
||||
|
||||
| TermQualIdentifier(d,_) -> d
|
||||
|
||||
| TermQualIdTerm(d,_,_) -> d
|
||||
|
||||
| TermLetTerm(d,_,_) -> d
|
||||
|
||||
| TermForAllTerm(d,_,_) -> d
|
||||
|
||||
| TermExistsTerm(d,_,_) -> d
|
||||
|
||||
| TermExclimationPt(d,_,_) -> d
|
||||
|
||||
and pd_varbinding = function
|
||||
| VarBindingSymTerm(d,_,_) -> d
|
||||
|
||||
and pd_termexclimationpt_term_attribute64 = function
|
||||
| (d,[]) -> d
|
||||
|
||||
| (d,( _ )::f1239o2) -> d
|
||||
|
||||
and pd_termexiststerm_term_sortedvar62 = function
|
||||
| (d,[]) -> d
|
||||
|
||||
| (d,( _ )::f1239o2) -> d
|
||||
|
||||
and pd_termforallterm_term_sortedvar60 = function
|
||||
| (d,[]) -> d
|
||||
|
||||
| (d,( _ )::f1239o2) -> d
|
||||
|
||||
and pd_termletterm_term_varbinding58 = function
|
||||
| (d,[]) -> d
|
||||
|
||||
| (d,( _ )::f1239o2) -> d
|
||||
|
||||
and pd_termqualidterm_term_term56 = function
|
||||
| (d,[]) -> d
|
||||
|
||||
| (d,( _ )::f1239o2) -> d
|
||||
|
||||
and pd_sortidsortmulti_sort_sort44 = function
|
||||
| (d,[]) -> d
|
||||
|
||||
| (d,( _ )::f1239o2) -> d
|
||||
|
||||
and pd_sexprinparen_sexpr_sexpr41 = function
|
||||
| (d,[]) -> d
|
||||
|
||||
| (d,( _ )::f1239o2) -> d
|
||||
|
||||
and pd_idunderscoresymnum_identifier_numeral33 = function
|
||||
| (d,[]) -> d
|
||||
|
||||
| (d,( _ )::f1239o2) -> d
|
||||
|
||||
and pd_commands_commands_command30 = function
|
||||
| (d,[]) -> d
|
||||
|
||||
| (d,( _ )::f1239o2) -> d
|
||||
|
||||
and pd_commandgetvalue_command_term24 = function
|
||||
| (d,[]) -> d
|
||||
|
||||
| (d,( _ )::f1239o2) -> d
|
||||
|
||||
and pd_commanddefinefun_command_sortedvar15 = function
|
||||
| (d,[]) -> d
|
||||
|
||||
| (d,( _ )::f1239o2) -> d
|
||||
|
||||
and pd_commanddeclarefun_command_sort13 = function
|
||||
| (d,[]) -> d
|
||||
|
||||
| (d,( _ )::f1239o2) -> d
|
||||
|
||||
and pd_commanddefinesort_command_symbol11 = function
|
||||
| (d,[]) -> d
|
||||
|
||||
| (d,( _ )::f1239o2) -> d
|
||||
|
||||
and pd_attributevalsexpr_attributevalue_sexpr5 = function
|
||||
| (d,[]) -> d
|
||||
|
||||
| (d,( _ )::f1239o2) -> d
|
||||
;;
|
||||
let pd e = pd_commands e;;
|
||||
119
util/smtlib/smtlib_syntax.mli
Normal file
119
util/smtlib/smtlib_syntax.mli
Normal file
|
|
@ -0,0 +1,119 @@
|
|||
(* Copyright 2014 INRIA *)
|
||||
|
||||
type dummy = Dummy
|
||||
and an_option = AnOptionAttribute of Smtlib_util.pd * attribute
|
||||
and attribute =
|
||||
AttributeKeyword of Smtlib_util.pd * string
|
||||
| AttributeKeywordValue of Smtlib_util.pd * string * attributevalue
|
||||
and attributevalue =
|
||||
AttributeValSpecConst of Smtlib_util.pd * specconstant
|
||||
| AttributeValSymbol of Smtlib_util.pd * symbol
|
||||
| AttributeValSexpr of Smtlib_util.pd *
|
||||
attributevalsexpr_attributevalue_sexpr5
|
||||
and command =
|
||||
CommandSetLogic of Smtlib_util.pd * symbol
|
||||
| CommandSetOption of Smtlib_util.pd * an_option
|
||||
| CommandSetInfo of Smtlib_util.pd * attribute
|
||||
| CommandDeclareSort of Smtlib_util.pd * symbol * string
|
||||
| CommandDefineSort of Smtlib_util.pd * symbol *
|
||||
commanddefinesort_command_symbol11 * sort
|
||||
| CommandDeclareFun of Smtlib_util.pd * symbol *
|
||||
commanddeclarefun_command_sort13 * sort
|
||||
| CommandDefineFun of Smtlib_util.pd * symbol *
|
||||
commanddefinefun_command_sortedvar15 * sort * term
|
||||
| CommandPush of Smtlib_util.pd * string
|
||||
| CommandPop of Smtlib_util.pd * string
|
||||
| CommandAssert of Smtlib_util.pd * term
|
||||
| CommandCheckSat of Smtlib_util.pd
|
||||
| CommandGetAssert of Smtlib_util.pd
|
||||
| CommandGetProof of Smtlib_util.pd
|
||||
| CommandGetUnsatCore of Smtlib_util.pd
|
||||
| CommandGetValue of Smtlib_util.pd * commandgetvalue_command_term24
|
||||
| CommandGetAssign of Smtlib_util.pd
|
||||
| CommandGetOption of Smtlib_util.pd * string
|
||||
| CommandGetInfo of Smtlib_util.pd * infoflag
|
||||
| CommandExit of Smtlib_util.pd
|
||||
and commands = Commands of Smtlib_util.pd * commands_commands_command30
|
||||
and identifier =
|
||||
IdSymbol of Smtlib_util.pd * symbol
|
||||
| IdUnderscoreSymNum of Smtlib_util.pd * symbol *
|
||||
idunderscoresymnum_identifier_numeral33
|
||||
and infoflag = InfoFlagKeyword of Smtlib_util.pd * string
|
||||
and qualidentifier =
|
||||
QualIdentifierId of Smtlib_util.pd * identifier
|
||||
| QualIdentifierAs of Smtlib_util.pd * identifier * sort
|
||||
and sexpr =
|
||||
SexprSpecConst of Smtlib_util.pd * specconstant
|
||||
| SexprSymbol of Smtlib_util.pd * symbol
|
||||
| SexprKeyword of Smtlib_util.pd * string
|
||||
| SexprInParen of Smtlib_util.pd * sexprinparen_sexpr_sexpr41
|
||||
and sort =
|
||||
SortIdentifier of Smtlib_util.pd * identifier
|
||||
| SortIdSortMulti of Smtlib_util.pd * identifier *
|
||||
sortidsortmulti_sort_sort44
|
||||
and sortedvar = SortedVarSymSort of Smtlib_util.pd * symbol * sort
|
||||
and specconstant =
|
||||
SpecConstsDec of Smtlib_util.pd * string
|
||||
| SpecConstNum of Smtlib_util.pd * string
|
||||
| SpecConstString of Smtlib_util.pd * string
|
||||
| SpecConstsHex of Smtlib_util.pd * string
|
||||
| SpecConstsBinary of Smtlib_util.pd * string
|
||||
and symbol =
|
||||
Symbol of Smtlib_util.pd * string
|
||||
| SymbolWithOr of Smtlib_util.pd * string
|
||||
and term =
|
||||
TermSpecConst of Smtlib_util.pd * specconstant
|
||||
| TermQualIdentifier of Smtlib_util.pd * qualidentifier
|
||||
| TermQualIdTerm of Smtlib_util.pd * qualidentifier *
|
||||
termqualidterm_term_term56
|
||||
| TermLetTerm of Smtlib_util.pd * termletterm_term_varbinding58 * term
|
||||
| TermForAllTerm of Smtlib_util.pd * termforallterm_term_sortedvar60 * term
|
||||
| TermExistsTerm of Smtlib_util.pd * termexiststerm_term_sortedvar62 * term
|
||||
| TermExclimationPt of Smtlib_util.pd * term *
|
||||
termexclimationpt_term_attribute64
|
||||
and varbinding = VarBindingSymTerm of Smtlib_util.pd * symbol * term
|
||||
and termexclimationpt_term_attribute64 = Smtlib_util.pd * attribute list
|
||||
and termexiststerm_term_sortedvar62 = Smtlib_util.pd * sortedvar list
|
||||
and termforallterm_term_sortedvar60 = Smtlib_util.pd * sortedvar list
|
||||
and termletterm_term_varbinding58 = Smtlib_util.pd * varbinding list
|
||||
and termqualidterm_term_term56 = Smtlib_util.pd * term list
|
||||
and sortidsortmulti_sort_sort44 = Smtlib_util.pd * sort list
|
||||
and sexprinparen_sexpr_sexpr41 = Smtlib_util.pd * sexpr list
|
||||
and idunderscoresymnum_identifier_numeral33 = Smtlib_util.pd * string list
|
||||
and commands_commands_command30 = Smtlib_util.pd * command list
|
||||
and commandgetvalue_command_term24 = Smtlib_util.pd * term list
|
||||
and commanddefinefun_command_sortedvar15 = Smtlib_util.pd * sortedvar list
|
||||
and commanddeclarefun_command_sort13 = Smtlib_util.pd * sort list
|
||||
and commanddefinesort_command_symbol11 = Smtlib_util.pd * symbol list
|
||||
and attributevalsexpr_attributevalue_sexpr5 = Smtlib_util.pd * sexpr list
|
||||
val dummy : unit -> unit
|
||||
val pd_an_option : an_option -> Smtlib_util.pd
|
||||
val pd_attribute : attribute -> Smtlib_util.pd
|
||||
val pd_attributevalue : attributevalue -> Smtlib_util.pd
|
||||
val pd_command : command -> Smtlib_util.pd
|
||||
val pd_commands : commands -> Smtlib_util.pd
|
||||
val pd_identifier : identifier -> Smtlib_util.pd
|
||||
val pd_infoflag : infoflag -> Smtlib_util.pd
|
||||
val pd_qualidentifier : qualidentifier -> Smtlib_util.pd
|
||||
val pd_sexpr : sexpr -> Smtlib_util.pd
|
||||
val pd_sort : sort -> Smtlib_util.pd
|
||||
val pd_sortedvar : sortedvar -> Smtlib_util.pd
|
||||
val pd_specconstant : specconstant -> Smtlib_util.pd
|
||||
val pd_symbol : symbol -> Smtlib_util.pd
|
||||
val pd_term : term -> Smtlib_util.pd
|
||||
val pd_varbinding : varbinding -> Smtlib_util.pd
|
||||
val pd_termexclimationpt_term_attribute64 : 'a * 'b list -> 'a
|
||||
val pd_termexiststerm_term_sortedvar62 : 'a * 'b list -> 'a
|
||||
val pd_termforallterm_term_sortedvar60 : 'a * 'b list -> 'a
|
||||
val pd_termletterm_term_varbinding58 : 'a * 'b list -> 'a
|
||||
val pd_termqualidterm_term_term56 : 'a * 'b list -> 'a
|
||||
val pd_sortidsortmulti_sort_sort44 : 'a * 'b list -> 'a
|
||||
val pd_sexprinparen_sexpr_sexpr41 : 'a * 'b list -> 'a
|
||||
val pd_idunderscoresymnum_identifier_numeral33 : 'a * 'b list -> 'a
|
||||
val pd_commands_commands_command30 : 'a * 'b list -> 'a
|
||||
val pd_commandgetvalue_command_term24 : 'a * 'b list -> 'a
|
||||
val pd_commanddefinefun_command_sortedvar15 : 'a * 'b list -> 'a
|
||||
val pd_commanddeclarefun_command_sort13 : 'a * 'b list -> 'a
|
||||
val pd_commanddefinesort_command_symbol11 : 'a * 'b list -> 'a
|
||||
val pd_attributevalsexpr_attributevalue_sexpr5 : 'a * 'b list -> 'a
|
||||
val pd : commands -> Smtlib_util.pd
|
||||
12
util/smtlib/smtlib_util.ml
Normal file
12
util/smtlib/smtlib_util.ml
Normal file
|
|
@ -0,0 +1,12 @@
|
|||
(* auto-generated by gt *)
|
||||
|
||||
(* no extra data from grammar file. *)
|
||||
type extradata = unit;;
|
||||
let initial_data() = ();;
|
||||
|
||||
let file = ref "stdin";;
|
||||
let line = ref 1;;
|
||||
type pos = int;;
|
||||
let string_of_pos p = "line "^(string_of_int p);;
|
||||
let cur_pd() = (!line, initial_data());; (* "pd": pos + extradata *)
|
||||
type pd = pos * extradata;;
|
||||
8
util/smtlib/smtlib_util.mli
Normal file
8
util/smtlib/smtlib_util.mli
Normal file
|
|
@ -0,0 +1,8 @@
|
|||
type extradata = unit
|
||||
val initial_data : unit -> unit
|
||||
val file : string ref
|
||||
val line : int ref
|
||||
type pos = int
|
||||
val string_of_pos : int -> string
|
||||
val cur_pd : unit -> int * unit
|
||||
type pd = pos * extradata
|
||||
Loading…
Add table
Reference in a new issue