4

jSIMLIBチェッカーは本質的にlispコードである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)
4

2 に答える 2

9

このpp関数は物事をうまく印刷できますが、希望するフォーマットと正確に一致しない場合があります。

これがあなたの質問からの1行です：

(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)))))))
于 2012-10-20T16:26:50.377 に答える
8

GNU Emacsでは、を使用できますindent-pp-sexp。

s-expressionの前のカーソルをpretty-printに設定し、と入力しc-u m-x indent-pp-sexpます。

于 2012-10-20T18:40:52.953 に答える