Authors: Andreas Dolzmann and Thomas Sturm
QEPCAD is a package to be used in combination with the package REDLOG. It provides access to the real quantifier elimination software QEPCAD B by C. Brown via process communication. In addition, it provides access to the simplifier SLFQ by C. Bown.
For using the QEPCAD package, the software QEPCAD B and SLFQ have to be installed independently of Reduce. It is recommended to Install also Singular and make sure QEPCAD uses this. Check that all programs work in your shell and that the corresponding executables are in your path. Note that QEPCAD requires an environment variable qe to be setup.
Create a QEPCAD input file:
Eliminate quantifiers in QEPCAD and reimport the result to Redlog:
psi := rlqepcad phi;
The same for SLFQ:
rlslfq(phi,"hugo.slfq"); psi := rlslfq phi;
Use QEPCAD as the fallback QE with
rlqepcadn(100*10^6); % The number of cells used by QEPCAD/SLFQ. The % default is (only) 1 * 10^6.
rlqepcadl(200*10^3); % The size of the prime list used by QEPCAD/SLFQ. The % default is (only) 2 * 10^3.
on rlqefbslfq; % use also SLFQ before QEPCAD in the fallback QE
on rlslfqvb; % dump all slfq messages to the screen. You usually want that.
Note that the quantities specified via rlqepcadn/rlqepcadl are used also for SLFQ, although the format and scaling of the options differs on the command line. The interface abstracts these differences.