Skip to content

Commit

Permalink
Reserve proxy names of SatML (#836)
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 authored Sep 26, 2023
1 parent 4f9c03a commit 0e10c6a
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 0e10c6a

Please sign in to comment.