Merge pull request #64 from sankalpgambhir/model-printing-fix2

Print models according to SMTLIB standard

regression-tests/horn-accel/Answers

@@ -311,9 +311,13 @@ unsat
 booleans.smt2
 Warning: ignoring exit
 sat
-(define-fun main_1 ((A Int) (B Int) (C Int) (D Int) (E Bool) (F Int)) Bool (or (= A 0) (and (= A 1) (and (= E true) (and (and (and (and (and (and (and (and (>= (+ (* 2 C) (+ (* (- 2) D) F)) B) (<= B 999999)) (>= B 0)) (<= C 499998)) (<= D 499999)) (>= D 1)) (<= F 999999)) (>= F 4)) (or (>= (- F B) 3) (and (= (+ B (+ (* (- 2) C) (- (* 2 D) F))) 0) (>= (- D C) 1))))))))
+(
+    (define-fun main_1 ((A Int) (B Int) (C Int) (D Int) (E Bool) (F Int)) Bool (or (= A 0) (and (= A 1) (and (= E true) (and (and (and (and (and (and (and (and (>= (+ (* 2 C) (+ (* (- 2) D) F)) B) (<= B 999999)) (>= B 0)) (<= C 499998)) (<= D 499999)) (>= D 1)) (<= F 999999)) (>= F 4)) (or (>= (- F B) 3) (and (= (+ B (+ (* (- 2) C) (- (* 2 D) F))) 0) (>= (- D C) 1))))))))
+)
 
 chc-LIA-Lin_421.smt2
 Warning: ignoring exit
 sat
-(define-fun predh11_1 ((A Int) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) (T Int) (U Int) (V Int) (W Int) (X Int) (Y Int) (Z Int) (A1 Int) (B1 Int) (C1 Int) (D1 Int) (E1 Int) (F1 Int) (G1 Int) (H1 Int) (I1 Int) (J1 Int) (K1 Int) (L1 Int) (M1 Int) (N1 Int) (O1 Int) (P1 Int) (Q1 Int) (R1 Int) (S1 Int) (T1 Int) (U1 Int) (V1 Int) (W1 Int) (X1 Int) (Y1 Int) (Z1 Int) (A2 Int) (B2 Int) (C2 Int) (D2 Int) (E2 Int) (F2 Int) (G2 Int) (H2 Int)) Bool (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= H2 D1) (= G2 C1)) (= (- F2 F) 1)) (= E2 1)) (= D2 F)) (= C2 1)) (= (- B2 F) 1)) (= A2 1)) (= Z1 F)) (= Y1 1)) (= X1 F)) (= W1 1)) (= V1 R)) (= U1 Q)) (= T1 P)) (= (+ S1 (- L R1)) 0)) (= Q1 1)) (= P1 L)) (= O1 K)) (= N1 J)) (= M1 I)) (= L1 H)) (= K1 G)) (= J1 F)) (= I1 E)) (= H1 D)) (= G1 C)) (= F1 B)) (= E1 A)) (and (>= (- F J) (- 1)) (>= J 1))))
+(
+    (define-fun predh11_1 ((A Int) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int) (I Int) (J Int) (K Int) (L Int) (M Int) (N Int) (O Int) (P Int) (Q Int) (R Int) (S Int) (T Int) (U Int) (V Int) (W Int) (X Int) (Y Int) (Z Int) (A1 Int) (B1 Int) (C1 Int) (D1 Int) (E1 Int) (F1 Int) (G1 Int) (H1 Int) (I1 Int) (J1 Int) (K1 Int) (L1 Int) (M1 Int) (N1 Int) (O1 Int) (P1 Int) (Q1 Int) (R1 Int) (S1 Int) (T1 Int) (U1 Int) (V1 Int) (W1 Int) (X1 Int) (Y1 Int) (Z1 Int) (A2 Int) (B2 Int) (C2 Int) (D2 Int) (E2 Int) (F2 Int) (G2 Int) (H2 Int)) Bool (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= H2 D1) (= G2 C1)) (= (- F2 F) 1)) (= E2 1)) (= D2 F)) (= C2 1)) (= (- B2 F) 1)) (= A2 1)) (= Z1 F)) (= Y1 1)) (= X1 F)) (= W1 1)) (= V1 R)) (= U1 Q)) (= T1 P)) (= (+ S1 (- L R1)) 0)) (= Q1 1)) (= P1 L)) (= O1 K)) (= N1 J)) (= M1 I)) (= L1 H)) (= K1 G)) (= J1 F)) (= I1 E)) (= H1 D)) (= G1 C)) (= F1 B)) (= E1 A)) (and (>= (- F J) (- 1)) (>= J 1))))
+)

regression-tests/horn-adt/Answers

@@ -1,12 +1,16 @@
 
 simple-adt-horn.smt2
 sat
-(define-fun I1 ((A Pair)) Bool (and (= (right A) true) (>= (left A) 0)))
-(define-fun I2 ((A Pair)) Bool (and (not (= (right A) true)) (>= (left A) 1)))
+(
+    (define-fun I1 ((A Pair)) Bool (and (= (right A) true) (>= (left A) 0)))
+    (define-fun I2 ((A Pair)) Bool (and (not (= (right A) true)) (>= (left A) 1)))
+)
 
 bool.smt2
 sat
-(define-fun Inv ((A Bool) (B Bool)) Bool (or (and (= A true) (= B true)) (and (not (= A true)) (not (= B true)))))
+(
+    (define-fun Inv ((A Bool) (B Bool)) Bool (or (and (= A true) (= B true)) (and (not (= A true)) (not (= B true)))))
+)
 
 bool-unsat.smt2
 unsat
@@ -17,10 +21,14 @@ unsat
 
 list-synasc.smt2
 sat
-(define-fun Concat ((A IList) (B IList) (C IList)) Bool (or (and (and (= (+ (_size A) (- (_size B) (_size C))) 1) (and (>= (_size C) (_size B)) (>= (_size B) 1))) (= (head C) (head A))) (and (and (and (and (= (_size A) 1) (or (and (is-Nil B) (is-Nil C)) (and (is-Cons B) (is-Cons C)))) (= (_size B) (_size C))) (>= (_size C) 1)) (or (not (is-Cons C)) (= (head C) (head B))))))
+(
+    (define-fun Concat ((A IList) (B IList) (C IList)) Bool (or (and (and (= (+ (_size A) (- (_size B) (_size C))) 1) (and (>= (_size C) (_size B)) (>= (_size B) 1))) (= (head C) (head A))) (and (and (and (and (= (_size A) 1) (or (and (is-Nil B) (is-Nil C)) (and (is-Cons B) (is-Cons C)))) (= (_size B) (_size C))) (>= (_size C) 1)) (or (not (is-Cons C)) (= (head C) (head B))))))
+)
 
 unbounded-tree.smt2
 sat
+(
+)
 
 record-cex.smt2
 unsat
@@ -58,11 +66,15 @@ unsat
 
 testers.smt2
 sat
-(define-fun p1 ((A XS)) Bool (is-XS_cons A))
+(
+    (define-fun p1 ((A XS)) Bool (is-XS_cons A))
+)
 
 tuple.smt2
 sat
-(define-fun p1 ((A Pair) (B Int)) Bool (and (and (>= (first A) 1) (<= (second A) 2)) (>= B 42)))
+(
+    (define-fun p1 ((A Pair) (B Int)) Bool (and (and (>= (first A) 1) (<= (second A) 2)) (>= B 42)))
+)
 
 tuple2.smt2
 unsat
@@ -77,17 +89,23 @@ unsat
 
 polymorphicTuple.smt2
 sat
-(define-fun p1 ((A (Pair Int Int)) (B Int)) Bool (and (and (>= (first A) 1) (<= (second A) 2)) (>= B 42)))
+(
+    (define-fun p1 ((A (Pair Int Int)) (B Int)) Bool (and (and (>= (first A) 1) (<= (second A) 2)) (>= B 42)))
+)
 
 adt-bug.smt2
 sat
-(define-fun pred1 ((A Int) (B abi_type) (C f_type) (D f_type)) Bool (or (not (= B a)) (and (= D C) (= A 0))))
+(
+    (define-fun pred1 ((A Int) (B abi_type) (C f_type) (D f_type)) Bool (or (not (= B a)) (and (= D C) (= A 0))))
+)
 
 de-brujin-bug.smt2
 sat
-(define-fun mmin ((A f)) Bool (= (h 0 g) A))
-(define-fun n ((A f)) Bool (= (_size A) 1))
-(define-fun p ((A f) (B d1) (C f)) Bool (or (or (and (and (= (_size A) (_size C)) (= (_size B) 1)) (>= (_size C) 1)) (and (and (and (is-b B) (= (_size B) 3)) (and (>= (_size A) 1) (>= (_size C) 1))) (is-b B))) (and (and (and (is-b B) (and (and (and (and (or (and (is-g A) (>= (_size B) 4)) (and (is-h A) (>= (+ (- 1) (_size B)) 4))) (or (and (is-g A) (>= (_size B) 5)) (and (is-h A) (>= (+ 1 (_size B)) 5)))) (>= (+ (_size A) (_size B)) 6)) (>= (_size A) 1)) (>= (_size C) 1))) (is-b B)) (= (mod (+ 1 (_size B)) 2) 0))))
+(
+    (define-fun mmin ((A f)) Bool (= (h 0 g) A))
+    (define-fun n ((A f)) Bool (= (_size A) 1))
+    (define-fun p ((A f) (B d1) (C f)) Bool (or (or (and (and (= (_size A) (_size C)) (= (_size B) 1)) (>= (_size C) 1)) (and (and (and (is-b B) (= (_size B) 3)) (and (>= (_size A) 1) (>= (_size C) 1))) (is-b B))) (and (and (and (is-b B) (and (and (and (and (or (and (is-g A) (>= (_size B) 4)) (and (is-h A) (>= (+ (- 1) (_size B)) 4))) (or (and (is-g A) (>= (_size B) 5)) (and (is-h A) (>= (+ 1 (_size B)) 5)))) (>= (+ (_size A) (_size B)) 6)) (>= (_size A) 1)) (>= (_size C) 1))) (is-b B)) (= (mod (+ 1 (_size B)) 2) 0))))
+)
 
 list-synasc-unsat.smt2
 unsat