GaNRAC

Getting started

Requirements

• ox-asir or
• SageMath

install ox-asir

CentOS

# yum install libX11-devel libXt-devel libXaw-devel
> curl -O "http://www.math.sci.kobe-u.ac.jp/pub/OpenXM/Head/openxm-head.tar.gz"
> tar xf openxm-head.tar.gz
> (cd OpenXM/src; make install)
> (cd OpenXM/rc; make install)
> while :; do ox -ox ox_asir -control 1234 -data 4321; done

Ubuntu

# apt install build-essential m4 bison
# apt install libx11-dev libxt-dev libxaw7-dev
> curl -O "http://www.math.sci.kobe-u.ac.jp/pub/OpenXM/Head/openxm-head.tar.gz"
> tar xf openxm-head.tar.gz
> (cd OpenXM/src; make install)
> (cd OpenXM/rc; make install)
> while :; do ox -ox ox_asir -control 1234 -data 4321; done

Installation

downloading the binary

See https://github.com/hiwane/ganrac/releases

compiling from source code

Required: go (1.18 or newer)

ox-asir version

> go install github.com/hiwane/ganrac/cmd/ganrac-ox@latest
> # go get github.com/hiwane/ganrac/cmd/ganrac-ox

SageMath version

> go install github.com/hiwane/ganrac/cmd/ganrac-sage@latest
> # go get github.com/hiwane/ganrac/cmd/ganrac-sage

Demo

real Quantifier Elimination

See qe.md for details.

F = ex([x], a*x^2+b*x+c==0);
qe(F);
G = example("quad");
H = time(qe(G[0]));
qe(all([x,y,z], equiv(G[1], H)));

real QE by Cylindrical Algebraic Decomposition

See cad.md for details.

vars(c,b,a,x);
F = ex([x], a*x^2+b*x+c <= 0);
F;
C = cadinit(F);
cadproj(C);
print(C, "proj");
print(C, "proj", 3, 0);
cadlift(C);
print(C, "sig");
print(C, "sig", 0);
print(C, "cell", 0, 1);
cadsfc(C);
print(C, "stat");