Rename declare-fun to let-const

formalsec · Jan 20, 2024 · c2b0537 · c2b0537
1 parent ef2e962
commit c2b0537
Show file tree

Hide file tree

Showing 6 changed files with 16 additions and 15 deletions.
diff --git a/lib/ast.ml b/lib/ast.ml
@@ -1,14 +1,14 @@
 type t =
-  | Declare of Symbol.t
+  | Let_const of Symbol.t
   | Assert of Expr.t
   | CheckSat
   | GetModel
 
 let pp fmt (instr : t) =
   match instr with
-  | Declare s ->
+  | Let_const s ->
     let ty = Symbol.type_of s in
-    Format.fprintf fmt "(declare-fun %a %a)" Symbol.pp s Ty.pp ty
+    Format.fprintf fmt "(let-const %a %a)" Symbol.pp s Ty.pp ty
   | Assert e -> Format.fprintf fmt "(assert @[<h 2>%a@])" Expr.pp e
   | CheckSat -> Format.pp_print_string fmt "(check-sat)"
   | GetModel -> Format.pp_print_string fmt "(get-model)"

diff --git a/lib/ast.mli b/lib/ast.mli
@@ -1,5 +1,5 @@
 type t =
-  | Declare of Symbol.t
+  | Let_const of Symbol.t
   | Assert of Expr.t
   | CheckSat
   | GetModel

diff --git a/lib/interpret.ml b/lib/interpret.ml
@@ -20,7 +20,7 @@ module Make (Solver : Solver_intf.S) = struct
     let { solver; pc; _ } = state in
     let st pc = { state with pc } in
     match stmt with
-    | Declare _x -> st pc
+    | Let_const _x -> st pc
     | Assert e ->
       Solver.add solver [ e ];
       st (e :: pc)

diff --git a/lib/lexer.mll b/lib/lexer.mll
@@ -63,7 +63,8 @@ let keywords =
      ; ("bool.and", BINARY (Ty_bool, And))
      ; ("bool.or", BINARY (Ty_bool, Or))
      ; ("bool.xor", BINARY (Ty_bool, Xor))
-     ; ("bool.eq", RELOP (Ty_bool, Eq))
+     ; ("=", RELOP (Ty_bool, Eq))
+     ; ("bool.eq", RELOP (Ty_bool, Ne))
      ; ("bool.ne", RELOP (Ty_bool, Ne))
      ; ("bool.ite", TERNARY (Ty_bool, Ite))
      ; ("str.len", UNARY (Ty_str, Len))
@@ -187,8 +188,8 @@ let keywords =
      ; ("f64.reinterpret_i64", CVTOP (Ty_fp S64, Reinterpret_int))
      ; ("Ptr", PTR)
      ; ("assert", ASSERT)
+     ; ("let-const", LET_CONST)
      ; ("check-sat", CHECK_SAT)
-     ; ("declare-fun", DECLARE_FUN)
      ; ("get-model", GET_MODEL)
     |];
   tbl

diff --git a/lib/parser.mly b/lib/parser.mly
@@ -13,7 +13,7 @@ let get_bind x = Hashtbl.find varmap x
 %token LPAREN
 %token RPAREN
 %token ASSERT
-%token DECLARE_FUN CHECK_SAT GET_MODEL
+%token LET_CONST CHECK_SAT GET_MODEL
 (*%token HOLE*)
 %token EOF
 
@@ -35,12 +35,12 @@ let get_bind x = Hashtbl.find varmap x
 let script := stmts = list(stmt); EOF; { stmts }
 
 let stmt :=
-  | LPAREN; DECLARE_FUN; x = SYMBOL; t = TYPE; RPAREN;
+  | LPAREN; LET_CONST; x = SYMBOL; t = TYPE; RPAREN;
     {
       add_bind x t;
-      Ast.Declare (Symbol.mk_symbol t x)
+      Ast.Let_const (Symbol.mk_symbol t x)
     }
-  | LPAREN; ASSERT; e = s_expr; RPAREN; { Ast.Assert e }
+  | LPAREN; ASSERT; ~ = s_expr; RPAREN; <Ast.Assert>
   | LPAREN; CHECK_SAT; RPAREN; { Ast.CheckSat }
   | LPAREN; GET_MODEL; RPAREN; { Ast.GetModel }
 

diff --git a/test/test_parser.ml b/test/test_parser.ml
@@ -6,10 +6,10 @@ let () =
   (* FIXME: when y = 2.0 this fails in Z3! *)
   let script =
     {|
-    (declare-fun x real)
-    (declare-fun y real)
-    (assert (real.eq y (real.mul x x)))
-    (assert (real.eq y 4.0))
+    (let-const x real)
+    (let-const y real)
+    (assert (= y (real.mul x x)))
+    (assert (= y 4.0))
     (check-sat)
     (get-model)
     |}