Lisp代碼（s表達式）格式化

Question

jSIMLIB檢查打印出s表達式代碼，其基本上口齒不清代碼

(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) 

如何我可以格式化代碼，優選用的emacs或TextMate的？例如：

(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

在GNU Emacs的，你可以使用indent-pp-sexp。

在s表達式之前將光標設置爲漂亮打印並鍵入c-u m-x indent-pp-sexp。

Answer 2

的pp功能可以很好地打印東西出來，但可能不是你想要的格式完全匹配。

下面是你的問題的一行：

(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)))))))