Tarski is a system that provides an
interface to a number of functions for computing with Tarski formulas and
semi-algebraic sets. Right now, the system and its functionality are in an
early stage of development, but the goal is to provide a an environment for
creating and testing new algorithms and, ultimately, to produce a system that
is flexibly able to choose efficient solution strategies for a wide range of
Tarski formula problems.

In its current stage, some of the primary pieces of functionality it offers are:;

- fast simplification and UNSAT cores for Tarski formulas
- problem formulation for QepcadB
- Open NuCAD constuction and projection
- read and write in smtlib syntax

~/$tarski>(def F1 [ y > -x (x - 1) /\ (x - 1/3)^2 + y^2 < (1/2)^2 ]); define F1 as a formula :void >(def R1 (SAT-NuCADConjunction F1)); determine (open) satisfiability of F1 :void >(head R1)( ( x:sym y:sym ) ( 0:num 1/8:num ) ) >(def F2 [ y > -x (x - 1) /\ (x - 1/3)^2 + y^2 < (1/8)^2 ]); define F2 as a formula :void >(def R2 (SAT-NuCADConjunction F2)); determine (open) satisfiability of F2 :void >(head R2)false:boo >(def F [ y > -x (x - 1) /\ (x - c)^2 + y^2 < r^2 /\ r > 0 ]); F generalizes with parameters :void >(def D (make-NuCADConjunction '(c r x y) '(0 0 0 0) F)); construct an open NuCAD for F :void >(msg D 'project 2); project onto (c,r)-space :void >(msg D 'plot-leaves "-1 1 -1 1 500 500" "C" "/tmp/foo.svg"); produce a plot :void >(msg D 'negate); swap true/false labels on the cells of D :void >(msg D 'def-form); get a defining formula for D "[ [ r < _root_1 r ] \/ [ r > _root_1 r /\ r < _root_2 16 r^6 - 48 c^2 r^4 + 48 c r^4 - 13 r^4 + 48 c^4 r^2 - 96 c^3 r^2 + 92 c^2 r^2 - 44 c r^2 + 8 r^2 - 16 c^6 + 48 c^5 - 52 c^4 + 24 c^3 - 4 c^2 /\ c > _root_1 c /\ c < _root_1 2 c - 1 ] \/ [ r > _root_1 r /\ r < _root_2 16 r^6 - 48 c^2 r^4 + 48 c r^4 - 13 r^4 + 48 c^4 r^2 - 96 c^3 r^2 + 92 c^2 r^2 - 44 c r^2 + 8 r^2 - 16 c^6 + 48 c^5 - 52 c^4 + 24 c^3 - 4 c^2 /\ c > _root_1 2 c - 1 /\ c < _root_1 c - 1 ] ]":str >(quit)~/$