convertQEtoRC := proc( expr, $ )
# Converts a Tarski formula (unquantified or otherwise) in QuantifierElimination
# format to RegularChains:-SemiAlgebraicSetTools:-QuantifierElimination amenable
# format
# note input expr MUST be prenex!

local oper;

if type( ( oper := op( 0, expr ) ), identical( :-exists ) ) then

    return &E( `if`( type( op( 1, expr ), 'list' ),
                     op( 1, expr ), [ op( 1, expr ) ] ) ),
               procname( op( 2, expr ) );

elif type( oper, identical( :-forall ) ) then

    return &A( `if`( type( op( 1, expr ), 'list' ),
                     op( 1, expr ), [ op( 1, expr ) ] ) ),
               procname( op( 2, expr ) );

else # should always be prenex, unquantified and/or

    return eval( expr, [ ':-And' = ':-`&and`', ':-Or' = ':-`&or`' ] );

end if;

end proc:

###############################################################################

convertQEtoSyNRAC := proc( expr, $ )
# Converts a Tarski formula (unquantified or otherwise) in QuantifierElimination
# format to SyNRAC amenable format
# input need not be prenex BUT SyNRAC will only accept prenex input

return eval( expr, [ ':-exists' = ':-Ex', ':-forall' = ':-All' ] );

end proc:

###############################################################################

convertQEtoQEPCAD := proc( expr, ECs :: truefalse := true, $ ) :: string;
# again, expr must be in prenex form
# produces a string that can be written to a file that can be redirected into
# QEPCAD

local out :: string := "[ Maple Formula ]\n",
      expri := expr,
      allVars :: MutableSet,
      i :: posint,
      x :: name,
      quants :: Array := Array([]),
      quantvars :: Array := Array([]);

while type( expri, 'specfunc'( { ':-forall', ':-exists' } ) ) do

    for x in op( 1, expri ) do

        quantvars ,= x;

        quants ,= op( 0, expri );

    end do;

    expri := op( 2, expri );

end do;

allVars := MutableSet( op( indets( expr, 'name' ) ) );

for x in quantvars do

    delete( allVars, x );

end do;

out := cat( out, sprintf( "( %q )\n", seq( x, x in allVars ),
                                      seq( quantvars[ -i ],
                                           i in 1..numelems( quantvars ) ) ) );


out := cat( out, sprintf( "%d\n", numelems( allVars ) ) );

for i to numelems( quants ) do

    out := cat( out, sprintf( "( %c %s )",
                              `if`( quants[ -i ] = ':-forall', "A", "E" ),
                              quantvars[ -i ] ) );

end do;

out := cat( out, "\n[ " );

out := cat( out, StringTools:-SubstituteAll( QEPCADFormulaUnquantified( expri ),
                                             "*", " " ) );

out := cat( out, " ].\n" );

if ECs then

    out := cat( out, "prop-eqn-const\n" );

end if;

out := cat( out, "finish\n" );

return out;

end proc:

###############################################################################

QEPCADFormulaUnquantified := proc( expr, $ ) :: string;

local infix :: string,
      i :: posint,
      out :: string;

if type( expr, 'specop'( { ':-And', ':-Or' } ) ) then

    ( out, infix ) := "[ ", `if`( op( 0 , expr ) = ':-And', " /\\ ", " \\/ " );

    for i to numelems( expr ) - 1 do

        out := cat( out, procname( op( i, expr ), infix ) );

    end do;

    return cat( out, procname( op( -1, expr ) ), " ]" );

elif type( expr, 'specop'( `<>` ) ) then # need to print this specially

    return sprintf( "%a /= 0", lhs( expr ) );

else

    return sprintf( "%a", expr );

end if;

end proc: