From 8cfe247250bf45cbf2d1a15f450960882d8e6ff9 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Sat, 23 Sep 2023 18:19:15 +0200 Subject: [PATCH] Reserve proxy names of SatML The SAT solver SatML produces proxy terms while building the CNF form of an expression. These terms have top symbols `Sy.Name` whose the string is prefixed by `PROXY_`. I replace the prefix by `.PROXY_` as names starting by a dot are reserved in the SMT-LIB standard. --- src/lib/structures/satml_types.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/lib/structures/satml_types.ml b/src/lib/structures/satml_types.ml index e2081a907..31f174f68 100644 --- a/src/lib/structures/satml_types.ml +++ b/src/lib/structures/satml_types.ml @@ -925,7 +925,7 @@ module Flat_Formula : FLAT_FORMULA = struct if is_neg then a.Atom.neg,l else a,l let mk_new_proxy n = - let hs = Hs.make ("PROXY__" ^ (string_of_int n)) in + let hs = Hs.make (".PROXY__" ^ (string_of_int n)) in (* TODO: we should use a smart constructor here. *) let sy = Symbols.Name (hs, Symbols.Other, false) in E.mk_term sy [] Ty.Tbool @@ -995,7 +995,7 @@ module Proxy_formula = struct if is_neg then a.Atom.neg,l else a,l let mk_new_proxy n = - let sy = Symbols.name @@ "PROXY__" ^ (string_of_int n) in + let sy = Symbols.name @@ ".PROXY__" ^ (string_of_int n) in E.mk_term sy [] Ty.Tbool let rec mk_cnf hcons f ((proxies, inv_proxies, new_vars, cnf) as accu) =