Convert first-order formulas
After installing golang
and setting up your GOPATH
, execute follows:
go get github.com/hiwane/qeconv/qeconv
qeconv
will be installed to the ${GOPATH}/bin
directory.
For convenience, add the ${GOPATH}/bin
to your PATH
.
To update qeconv
, execute follows:
go get -u github.com/hiwane/qeconv/qeconv
Usage: qeconv [-f {from}][-t {to}][-i {inputfile}][-o {outputfile}][-s][-n {{index}]
-f: Use {from} for input format [syn]
-t: Use {to} for output format [syn]
syn: SyNRAC format
tex: LaTeX format
math: MATHEMATICA format
qep: QEPCAD format
red: Redlog format
rc: RegularChains format
smt2: SMT2 format (-n option is reguired)
-i: Use {inputfile} for input [stdin]
-o: Use {outputfile} for output [stdout]
-s: Remove duplicate formulas
-n: Use {index}th formula [0]
0: Use all formula
-1: Get the number of first-order formulas in input
% echo "x>0:" | qeconv
0 < x:
% echo "And(x<>0,y>=0):" | qconv
And(x <> 0,0 <= y):
% echo "Ex([y],And(x>0,y>=0)):" | qconv
Ex([y],And(0 < x,0 <= y)):
% echo "x>0:" | qeconv -t tex
0 < x
% echo "And(x<>0,y>=0):" | qeconv -t tex
x \neq 0 \land 0 \leq y
% echo "Ex([y],And(x>0,y>=0)):" | qeconv -t tex
\exists y(0 < x \land 0 \leq y)
% echo "x>0:" | qeconv -t math
0 < x
% echo "And(x<>0,y>=0):" | qeconv -t math
x != 0 && 0 <= y
% echo "Ex([y],And(x>0,y>=0)):" | qeconv -t math
Exists[{y},0 < x && 0 <= y]
% echo "x>0:" | qeconv -t qep
0 < x
% echo "And(x<>0,y>=0):" | qeconv -t qep
x /= 0 /\ 0 <= y
% echo "Ex([y],And(x>0,y>=0)):" | qeconv -t qep
(E y)[0 < x /\ 0 <= y]
% echo "x>0:" | qeconv -t red
0 < x
% echo "And(x<>0,y>=0):" | qeconv -t red
x <> 0 and 0 <= y
% echo "Ex([y],And(x>0,y>=0)):" | qeconv -t red
ex([y],0 < x and 0 <= y)
% echo "x>0:" | qeconv -t rc
0 < x
% echo "And(x<>0,y>=0):" | qeconv -t rc
`&and`(x <> 0, 0 <= y)
% echo "Ex([y],And(x>0,y>=0)):" | qeconv -t rc
`&E`([y]), `&and`(0 < x,0 <= y)