simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 11:15:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

easier list of known logic

Browse source
This commit is contained in:
Simon Cruanes 2022-01-31 15:28:02 -05:00
parent 3c41ab2484
commit cb369ec68d
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 14 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/smtlib/Process.ml
View file

@ -210,6 +210,16 @@ let solve
Format.printf "Unknown (:reason %a)" Solver.Unknown.pp reas
end
let known_logics = [
"QF_UF";
"QF_LRA";
"QF_UFLRA";
"QF_DT";
"QF_UFDT";
"QF_LIA";
"QF_UFLIA";
]
(* process a single statement *)
let process_stmt
?gc ?restarts ?(pp_cnf=false)
@ -231,10 +241,10 @@ let process_stmt
in
begin match stmt with
| Statement.Stmt_set_logic ("QF_UF"|"QF_LRA"|"QF_UFLRA"|"QF_DT"|"QF_UFDT") ->
E.return ()
| Statement.Stmt_set_logic s ->
Log.debugf 0 (fun k->k "warning: unknown logic `%s`" s);
| Statement.Stmt_set_logic logic ->
if not @@ List.mem logic known_logics then (
Log.debugf 0 (fun k->k "warning: unknown logic `%s`" logic);
);
E.return ()
| Statement.Stmt_set_option l ->
Log.debugf 0 (fun k->k "warning: unknown option `%a`" (Util.pp_list Fmt.string) l);