From d29f6bd493fddf50aa85f058938cb3dad979e490 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Thu, 2 Nov 2023 16:24:32 +0100 Subject: [PATCH] Removing the optimization support in the native language The current implementation of `maximize` and `minimize` isn't satisfying in the native language. As this feature have never been released and MERCE prefers using the SMT-LIB format, we remove the support of optimization in the native language. --- src/parsers/native_lexer.mll | 2 -- src/parsers/native_parser.mly | 1 - 2 files changed, 3 deletions(-) diff --git a/src/parsers/native_lexer.mll b/src/parsers/native_lexer.mll index e282e95d66..1090e63299 100644 --- a/src/parsers/native_lexer.mll +++ b/src/parsers/native_lexer.mll @@ -79,8 +79,6 @@ "match" , MATCH; "with" , WITH; "of" , OF; - "maximize" , MAXIMIZE; - "minimize" , MINIMIZE; ] in List.iter (fun (s, kw) -> Hashtbl.add tbl s kw) kw_list; diff --git a/src/parsers/native_parser.mly b/src/parsers/native_parser.mly index 0e4664b6eb..dd96f92163 100644 --- a/src/parsers/native_parser.mly +++ b/src/parsers/native_parser.mly @@ -54,7 +54,6 @@ %token RIGHTPAR RIGHTSQ RIGHTBR %token SLASH POW POWDOT %token THEN TIMES TRUE TYPE -%token MAXIMIZE MINIMIZE /* Precedences */