QEPCAD

From redlog.eu
Jump to: navigation, search

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.

Installation

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.

Usage

load_package qepcad;

Create a QEPCAD input file:

rlqepcad(phi,"hugo.qepcad"); 

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 rlqe. Remember that rlqefb has to be on in order to get into fallback quantifier elimination at all:

on rlqefbqepcad; 

Use also SLFQ before QEPCAD in the fallback QE:

on rlqefbslfq;

The following functions setup quantities to be passed as command line arguments to the QEPCAD/SLFQ calls. The number of cells used by QEPCAD/SLFQ. The default is (only) 1 * 10^6.:

rlqepcadn(100*10^6);  

The size of the prime list used by QEPCAD/SLFQ. The default is (only) 2 * 10^3:

rlqepcadl(200*10^3);

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.

There is a switch to dump all SLFQ messages to the screen. You usually want that. Note that in addition rlverbose has to be turned on in order to get any verbosity output at all:

on rlslfqvb;

External Links

  • QEPCAD - the QEPCAD B homepage
  • SLFQ - the SLFQ homepage
  • Singular - the Singular homepage