1use std::fmt::{self, Write};
2
3use itertools::Itertools;
4
5use crate::{
6 BinOp, BinRel, ConstDecl, Constant, Constraint, DataCtor, DataDecl, DataField, Expr,
7 FixpointFmt, FunDef, Identifier, KVarDecl, Pred, Qualifier, Sort, SortCtor, Task, Types,
8};
9
10pub(crate) fn fmt_constraint<T: Types>(
11 cstr: &Constraint<T>,
12 f: &mut fmt::Formatter<'_>,
13) -> fmt::Result {
14 let mut cx = ConstraintFormatter::default();
15 write!(f, "(constraint")?;
16 cx.incr();
17 cx.newline(f)?;
18 cx.fmt_constraint(f, cstr)?;
19 cx.decr();
20 writeln!(f, ")")
21}
22
23impl<T: Types> fmt::Display for Task<T> {
24 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
25 if self.scrape_quals {
26 writeln!(f, "(fixpoint \"--scrape=both\")")?;
27 }
28 for line in &self.comments {
29 writeln!(f, ";; {line}")?;
30 }
31 writeln!(f)?;
32
33 for data_decl in &self.data_decls {
34 writeln!(f, "{data_decl}")?;
35 }
36
37 for qualif in &self.qualifiers {
38 writeln!(f, "{qualif}")?;
39 }
40
41 for cinfo in &self.constants {
42 writeln!(f, "{cinfo}")?;
43 }
44
45 for fun_decl in &self.define_funs {
46 writeln!(f, "{fun_decl}")?;
47 }
48
49 for kvar in &self.kvars {
50 writeln!(f, "{kvar}")?;
51 }
52
53 writeln!(f)?;
54 fmt_constraint(&self.constraint, f)
55 }
56}
57
58impl<T: Types> fmt::Display for KVarDecl<T> {
59 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
60 write!(
61 f,
62 "(var ${} ({})) ;; {}",
63 self.kvid.display(),
64 self.sorts.iter().format(" "),
65 self.comment
66 )
67 }
68}
69
70impl<T: Types> fmt::Display for ConstDecl<T> {
71 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
72 write!(f, "(constant {} {})", self.name.display(), self.sort)?;
73 if let Some(comment) = &self.comment {
74 write!(f, " ;; {comment}")?;
75 }
76 Ok(())
77 }
78}
79
80impl<T: Types> fmt::Debug for Task<T> {
81 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
82 fmt::Display::fmt(self, f)
83 }
84}
85
86#[derive(Default)]
87struct ConstraintFormatter {
88 level: u32,
89}
90
91impl ConstraintFormatter {
92 fn fmt_constraint<T: Types>(
93 &mut self,
94 f: &mut fmt::Formatter<'_>,
95 cstr: &Constraint<T>,
96 ) -> fmt::Result {
97 match cstr {
98 Constraint::Pred(pred, tag) => self.fmt_pred_in_head_position(pred, tag.as_ref(), f),
99 Constraint::Conj(cstrs) => {
100 match &cstrs[..] {
101 [] => write!(f, "((true))"),
102 [cstr] => self.fmt_constraint(f, cstr),
103 cstrs => {
104 write!(f, "(and")?;
105 for cstr in cstrs {
106 self.incr();
107 self.newline(f)?;
108 self.fmt_constraint(f, cstr)?;
109 self.decr();
110 }
111 f.write_char(')')
112 }
113 }
114 }
115 Constraint::ForAll(bind, head) => {
116 write!(f, "(forall (({} {}) {})", bind.name.display(), bind.sort, bind.pred)?;
117
118 self.incr();
119 self.newline(f)?;
120 self.fmt_constraint(f, head)?;
121 self.decr();
122
123 f.write_str(")")
124 }
125 }
126 }
127
128 fn fmt_pred_in_head_position<T: Types>(
129 &mut self,
130 pred: &Pred<T>,
131 tag: Option<&T::Tag>,
132 f: &mut fmt::Formatter<'_>,
133 ) -> fmt::Result {
134 match pred {
135 Pred::And(preds) => {
136 match &preds[..] {
137 [] => write!(f, "((true))"),
138 [pred] => self.fmt_pred_in_head_position(pred, tag, f),
139 _ => {
140 write!(f, "(and")?;
141 for pred in preds {
142 self.incr();
143 self.newline(f)?;
144 self.fmt_pred_in_head_position(pred, tag, f)?;
145 self.decr();
146 }
147 write!(f, ")")
148 }
149 }
150 }
151 Pred::Expr(_) | Pred::KVar(..) => {
152 if let Some(tag) = tag {
153 write!(f, "(tag {pred} \"{tag}\")")
154 } else {
155 write!(f, "{pred}")
156 }
157 }
158 }
159 }
160
161 fn incr(&mut self) {
162 self.level += 1;
163 }
164
165 fn decr(&mut self) {
166 self.level -= 1;
167 }
168
169 fn newline(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
170 f.write_char('\n')?;
171 self.padding(f)
172 }
173
174 fn padding(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
175 for _ in 0..self.level {
176 f.write_str(" ")?;
177 }
178 Ok(())
179 }
180}
181
182impl<T: Types> fmt::Display for DataDecl<T> {
183 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
184 write!(
185 f,
186 "(datatype ({} {}) ({}))",
187 self.name.display(),
188 self.vars,
189 self.ctors.iter().format(" ")
190 )
191 }
192}
193
194impl<T: Types> fmt::Display for DataCtor<T> {
195 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
196 write!(f, "({} ({}))", self.name.display(), self.fields.iter().format(" "))
197 }
198}
199
200impl<T: Types> fmt::Display for DataField<T> {
201 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
202 write!(f, "({} {})", self.name.display(), self.sort)
203 }
204}
205
206impl<T: Types> fmt::Display for SortCtor<T> {
207 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
208 match self {
209 SortCtor::Set => write!(f, "Set_Set"),
210 SortCtor::Map => write!(f, "Map_t"),
211 SortCtor::Data(name) => write!(f, "{}", name.display()),
212 }
213 }
214}
215
216impl<T: Types> fmt::Display for Sort<T> {
217 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
218 match self {
219 Sort::Int => write!(f, "int"),
220 Sort::Bool => write!(f, "bool"),
221 Sort::Real => write!(f, "real"),
222 Sort::Str => write!(f, "Str"),
223 Sort::Var(i) => write!(f, "@({i})"),
224 Sort::BitVec(size) => write!(f, "(BitVec {size})"),
225 Sort::BvSize(size) => write!(f, "Size{size}"),
226 Sort::Abs(..) => {
227 let (params, sort) = self.peel_out_abs();
228 fmt_func(params, sort, f)
229 }
230 Sort::Func(..) => fmt_func(0, self, f),
231 Sort::App(ctor, args) => {
232 write!(f, "({ctor}")?;
233 for arg in args {
234 write!(f, " {arg}")?;
235 }
236 write!(f, ")")
237 }
238 }
239 }
240}
241
242fn fmt_func<T: Types>(params: usize, sort: &Sort<T>, f: &mut fmt::Formatter<'_>) -> fmt::Result {
243 write!(f, "(func {params} (")?;
244 let mut curr = sort;
245 while let Sort::Func(input_and_output) = curr {
246 let [input, output] = &**input_and_output;
247 write!(f, "{input} ")?;
248 curr = output;
249 }
250 write!(f, ") {curr})")
251}
252
253impl<T: Types> fmt::Display for Pred<T> {
254 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
255 match self {
256 Pred::And(preds) => {
257 match &preds[..] {
258 [] => write!(f, "((true))"),
259 [pred] => write!(f, "{pred}"),
260 preds => write!(f, "(and {})", preds.iter().join(" ")),
261 }
262 }
263 Pred::KVar(kvid, vars) => {
264 write!(
265 f,
266 "(${} {})",
267 kvid.display(),
268 vars.iter().map(Identifier::display).format(" ")
269 )
270 }
271 Pred::Expr(expr) => write!(f, "({expr})"),
272 }
273 }
274}
275
276impl<T: Types> fmt::Display for Expr<T> {
277 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
278 match self {
279 Expr::Constant(c) => write!(f, "{c}"),
280 Expr::Var(x) => write!(f, "{}", x.display()),
281 Expr::App(func, args) => {
282 write!(f, "({func} {})", args.iter().format(" "))
283 }
284 Expr::Neg(e) => {
285 write!(f, "(- {e})")
286 }
287 Expr::BinaryOp(op, exprs) => {
288 let [e1, e2] = &**exprs;
289 write!(f, "({op} {e1} {e2})")
290 }
291 Expr::IfThenElse(exprs) => {
292 let [p, e1, e2] = &**exprs;
293 write!(f, "(if {p} {e1} {e2})")
294 }
295 Expr::And(exprs) => {
296 write!(f, "(and {})", exprs.iter().format(" "))
297 }
298 Expr::Or(exprs) => {
299 write!(f, "(or {})", exprs.iter().format(" "))
300 }
301 Expr::Not(e) => {
302 write!(f, "(not {e})")
303 }
304 Expr::Imp(exprs) => {
305 let [e1, e2] = &**exprs;
306 write!(f, "(=> {e1} {e2})")
307 }
308 Expr::Iff(exprs) => {
309 let [e1, e2] = &**exprs;
310 write!(f, "(<=> {e1} {e2})")
311 }
312 Expr::Atom(rel, exprs) => {
313 let [e1, e2] = &**exprs;
314 write!(f, "({rel} {e1} {e2})")
315 }
316 Expr::Let(name, exprs) => {
317 let [e1, e2] = &**exprs;
320 write!(f, "(let (({} {e1})) {e2})", name.display())
321 }
322 Expr::ThyFunc(thy_func) => write!(f, "{}", thy_func),
323 Expr::IsCtor(ctor, e) => {
324 write!(f, "(is${} {})", ctor.display(), e)
325 }
326 }
327 }
328}
329
330impl<T: Types> fmt::Display for Constant<T> {
331 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
332 match self {
333 Constant::Numeral(n) => write!(f, "{n}"),
334 Constant::Real(n) => write!(f, "{n}.0"),
335 Constant::Boolean(b) => write!(f, "{b}"),
336 Constant::String(s) => write!(f, "{}", s.display()),
337 Constant::BitVec(i, sz) => {
338 if sz.is_multiple_of(4) {
339 write!(f, "(lit \"#x{i:00$x}\" (BitVec Size{sz}))", (sz / 4) as usize)
340 } else {
341 write!(f, "(lit \"#b{i:00$x}\" (BitVec Size{sz}))", *sz as usize)
342 }
343 }
344 }
345 }
346}
347
348impl<T: Types> fmt::Display for Qualifier<T> {
349 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
350 write!(
351 f,
352 "(qualif {} ({}) ({}))",
353 self.name,
354 self.args.iter().format_with(" ", |(name, sort), f| {
355 f(&format_args!("({} {sort})", name.display()))
356 }),
357 self.body
358 )
359 }
360}
361
362impl<T: Types> fmt::Display for FunDef<T> {
363 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
364 write!(
365 f,
366 "(define_fun {} ({}) {} ({}))",
367 self.name.display(),
368 self.args.iter().format_with(" ", |(name, sort), f| {
369 f(&format_args!("({} {sort})", name.display()))
370 }),
371 self.out,
372 self.body
373 )?;
374 if let Some(comment) = &self.comment {
375 write!(f, " ;; {comment}")?;
376 }
377 Ok(())
378 }
379}
380
381impl fmt::Display for BinOp {
382 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
383 match self {
384 BinOp::Add => write!(f, "+"),
385 BinOp::Sub => write!(f, "-"),
386 BinOp::Mul => write!(f, "*"),
387 BinOp::Div => write!(f, "/"),
388 BinOp::Mod => write!(f, "mod"),
389 }
390 }
391}
392
393impl fmt::Display for BinRel {
394 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
395 match self {
396 BinRel::Eq => write!(f, "="),
397 BinRel::Ne => write!(f, "!="),
398 BinRel::Gt => write!(f, ">"),
399 BinRel::Ge => write!(f, ">="),
400 BinRel::Lt => write!(f, "<"),
401 BinRel::Le => write!(f, "<="),
402 }
403 }
404}
405
406impl fmt::Debug for BinOp {
407 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
408 fmt::Display::fmt(self, f)
409 }
410}