結果の検証

今回の QE ツールにおける入出力（に対応した論理式）の等価性の検証は，いつもお世話になっている qepmax（https://github.com/YasuakiHonda/qepmax）を介して QEPCAD B で行なっています．具体的には，次のように出力のリストを論理結合に変換する関数 F2G（内部で QEPCAD B を繰り返し呼んでいます）で処理したのち，QEPCAD B の出力と等価であるかをチェックしています．

(%i1) (qvpeds ([all],[c,b,a,x],0,h1,r11,0 ),G1:qe( bfpcad(ext( '(  x^4+a*x^2+b*x+c>=0  ) )))  )$
Evaluation took 6.6300 seconds (6.7100 elapsed) using 828.758 MB.

(%i2) G1:F2G(G1);
Evaluation took 17.2500 seconds (20.6700 elapsed) using 2096.781 MB.
(%o2) (((a >= 0) %and (c > 0)) %or ((a >= 0) %and (4096*c^3+27*b^4 = 0))
                               %or ((c > 0)
                                %and ((-64*a*c^2)+36*b^2*c+16*a^3*c-3*a^2*b^2
                                 >= 0)))
  %and (c >= 0)
  %and (256*c^3-128*a^2*c^2+144*a*b^2*c+16*a^4*c-27*b^4-4*a^3*b^2 >= 0)

(%i3) qex([],G1 %eq qex([[A,x]],x^4+a*x^2+b*x+c>=0));
Evaluation took 3.2500 seconds (3.6800 elapsed) using 438.299 MB.
(%o3) true

ただし，well-oriented という条件を満たさない入力の場合，QEPCAD B のデフォルトの projection では正当性が保証されないので，Hong's projection operator を併用するコマンドを挟むよう qepmax の qe コマンドの定義（https://github.com/YasuakiHonda/qepmax/blob/master/qepmax.mac）の 214 行目を

    if length(varlist)>1 then
     ( printf(ost, "[ ~a ].~%proj-operator (m", writeLogicalExp(formula,varlist)),
       if length(varlist)>2 then printf(ost, ",m"),
       for i:1 thru length(varlist)-3 do printf(ost, ",h"),
       printf(ost, ")~%finish~%")
     )
    else printf(ost, "[ ~a ].~%finish~%", writeLogicalExp(formula,varlist)),

のように改変し qex（以前公開した同名の関数とは別物）として使わせて頂いています．