1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
|
/*======================================================================
QEPCAD(Fs; t,F_e,F_n,F_s)
Quantifier Elimination by Partial Cylindrical Algebraic Decomposition.
\Input
\parm{F*} $=(Q_{f+1} x_{f+1})\cdots(Q_r x_r)\hat{F}(x_1,\ldots,x_r)$,
$0\leq f < r$, is a quantified formula.
\Output
\parm{t} is either \c{EQU} or \c{INEQU}.
\parm{Fe} is a quantifier-free formula equivalent to~\v{F*}
if \v{t} is \c{EQU}, otherwise \v{Fe} is undefined.
\parm{Fn} is a quantifier-free formula necssary for~\v{F*}
if \v{t} is \c{INEQU}, otherwise \v{Fn} is undefined.
\parm{Fs} is a quantifier-free formula sufficient for~\v{F*}
if \v{t} is \c{INEQU}, otherwise \v{Fs} is undefined.
======================================================================*/
#include "qepcad.h"
void QepcadCls::QEPCADauto(Word Fs, Word *t_, Word *F_e_, Word *F_n_, Word *F_s_)
{
Word A,D,F,F_e,F_n,F_s,Fh,J,P,Q,f,r,t;
/* hide t; */
Step1: /* Normalize. */
t = -1;
F_e = F_n = F_s = NIL;
FIRST4(Fs,&r,&f,&Q,&Fh);
F = NORMQFF(Fh);
if (GVUA != NIL) GVNA = NORMQFF(GVUA);
GVNQFF = F;
if (TYPEQFF(F) != UNDET) { t = EQU; F_e = F; goto Return; }
Step2: /* Projection. */
if (GVUA != NIL) F = LIST3(ANDOP,GVNA,F);
A = EXTRACT(r,F);
if (GVUA != NIL) {
GVNA = SECOND(F);
F = THIRD(F); }
GVNIP = A;
GVPF = LLCOPY(A);
GVLV = r;
PROJECTauto(r,A,&P,&J);
Step3: /* Truth-invariant CAD. */
if (PCTRACKUNSATCORE) { UNSATCORE.prepareForLift(); }
D = TICADauto(Q,F,f,P,A);
Step4: /* Solution. */
GVPC = D;
if (!PCMZERROR)
SFC3(GVPC,GVPF,GVPJ,GVNFV,LIST10(0,0,0,1,0,3,2,4,1,-1));
else
SFCFULLD(GVPC,GVPF,GVPJ,GVNFV);
Return: /* Prepare for return. */
*t_ = t;
*F_e_ = F_e;
*F_n_ = F_n;
*F_s_ = F_s;
return;
}
|
