結果の検証

今回の 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(以前公開した同名の関数とは別物)として使わせて頂いています.