#29 Redlog Qepcad Broken.

Thomas Sturm

I've reproduced, for my own purposes, the combination of Reduce-Redlog + Qepcad + Slfq + Singular as
described in the paper "Verification and synthesis using real quantifier elimination" (ISSAC 2011).
I've tested it with the benchmarks from

I have found the following bugs:

1) ".qepcad" files.

The generated "{BENCH}.qepcad" files change from running in CSL and in PSL.
In PSL, it generates a good Qepcad input file.
In CSL, it generates a long list of polynomial expressions (without relationals),
separated by blank lines.

2) the instruction
psi2 := rlqepcad( psi , "{BENCH}.qepcad" )

doesn't seem to work right: it likes as it should assign a value to psi2,
but it only assigns to it an empty string.
Maybe it isn't a bug, i'm not sure what is that function supposed to do.

The bug was noticed with the Trunk's head Revision,
and the last released versions of Qepcad
(and it's companion slfq), saclib 2.2.5, and Singular 3-1-3.


  • Bad qepcad file: generated in Csl mode (not Psl)

  • The Redlog/Qepcad package is developed by Thomas Sturm.

    • assigned_to: nobody --> thomas-sturm
  • Thomas Sturm
    Thomas Sturm

    • status: open --> closed-fixed
  • Thomas Sturm
    Thomas Sturm

    The printing badly interacted with the fancy printing for the CSL GUI. I have fixed this. rlqepcad with the second optional argument is for creating the Qepcad file w/o doing anything else. The idea is to work with the generated file outside Reduce.

    For hard computations note that Redlog is probably considerably faster with PSL than with CSL.

    There are comfortable terminal-based interfaces using the editline library in trunk/generic/redfront. These allow also to increase the memory size for PSL on the command line. A man page is available as trunk/generic/redfront/src/redfront.1