Lisp code (s-expression) formatter

Question

jSIMLIB checker outputs s-expression code, which is essentially lisp code

(set-option :print-success false) (set-logic QF_LIA) (declare-fun RETURN () Int) (declare-fun refs_1_SYMINT () Int) (declare-fun flags_2_SYMINT () Int) (assert+ ( and ( or ( and (/= flags_2_SYMINT 0) (and (= RETURN flags_2_SYMINT)) ) ( and (/= refs_1_SYMINT 0) (and (= flags_2_SYMINT 0)) (and (= RETURN refs_1_SYMINT)) ) ( and (and (= refs_1_SYMINT 0)) (and (= flags_2_SYMINT 0)) (and (= RETURN 100)) ) ) ( not ( or ( and (/= flags_2_SYMINT 0) (and (= RETURN flags_2_SYMINT)) ) ( and (/= refs_1_SYMINT 0) (and (= flags_2_SYMINT 0)) (and (= RETURN refs_1_SYMINT)) ) ( and (and (= refs_1_SYMINT 0)) (and (= flags_2_SYMINT 0)) (and (= RETURN 10)) ) ) ) ) ) (check) (exit) 

How can I format the code, preferably with emacs or TextMate? For instance:

 (set-option :print-success false) (set-logic QF_LIA) (declare-fun RETURN () Int) (declare-fun refs_1_SYMINT () Int) (declare-fun flags_2_SYMINT () Int) (assert (and (and (and (distinct flags_2_SYMINT 0) (= RETURN flags_2_SYMINT)) (= refs_1_SYMINT refs1_1_SYMINT) (= flags_2_SYMINT flags1_2_SYMINT)) (not (and (distinct flags_2_SYMINT 0) (= RETURN flags_2_SYMINT))))) (check-sat) 

Answer 1

In GNU Emacs, you can use indent-pp-sexp .

Position the cursor before s-expression is printed pretty nicely and type cu mx indent-pp-sexp .

Answer 2

The pp function may print things well, but may not match the exact formatting.

Here is one line from your question:

 (pp '(assert+ ( and ( or ( and (/= flags_2_SYMINT 0) (and (= RETURN flags_2_SYMINT)) ) ( and (/= refs_1_SYMINT 0) (and (= flags_2_SYMINT 0)) (and (= RETURN refs_1_SYMINT)) ) ( and (and (= refs_1_SYMINT 0)) (and (= flags_2_SYMINT 0)) (and (= RETURN 100)) ) ) ( not ( or ( and (/= flags_2_SYMINT 0) (and (= RETURN flags_2_SYMINT)) ) ( and (/= refs_1_SYMINT 0) (and (= flags_2_SYMINT 0)) (and (= RETURN refs_1_SYMINT)) ) ( and (and (= refs_1_SYMINT 0)) (and (= flags_2_SYMINT 0)) (and (= RETURN 10)) ) ) ) ) )) 

:

 (assert+ (and (or (and (/= flags_2_SYMINT 0) (and (= RETURN flags_2_SYMINT))) (and (/= refs_1_SYMINT 0) (and (= flags_2_SYMINT 0)) (and (= RETURN refs_1_SYMINT))) (and (and (= refs_1_SYMINT 0)) (and (= flags_2_SYMINT 0)) (and (= RETURN 100)))) (not (or (and (/= flags_2_SYMINT 0) (and (= RETURN flags_2_SYMINT))) (and (/= refs_1_SYMINT 0) (and (= flags_2_SYMINT 0)) (and (= RETURN refs_1_SYMINT))) (and (and (= refs_1_SYMINT 0)) (and (= flags_2_SYMINT 0)) (and (= RETURN 10)))))))