Skip to content

Commit

Permalink
Reserve proxy names of SatML
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
Halbaroth committed Sep 23, 2023
1 parent 2d7d271 commit 8cfe247
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions src/lib/structures/satml_types.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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) =
Expand Down

0 comments on commit 8cfe247

Please sign in to comment.