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