check_ast_bt.cpp

#include "ast.h"
#include "ast_gen.h"
#include "parser.h"

void check_ast_bt(size_t& good, size_t& bad) {
    AstGen::Gen const
        x = Ast::Identifier("x"),
        y = Ast::Identifier("y"),
        z = Ast::Identifier("z");

#define CHECK_AST(expr, ast) ++(Parser::check_ast(expr, ast)?good:bad)

#pragma GCC diagnostic push
#pragma GCC diagnostic ignored "-Wlogical-not-parentheses"
#pragma GCC diagnostic ignored "-Wparentheses"
    CHECK_AST("( not x)>= not y xor z", ( not x)>= not y^z);
    CHECK_AST("( not x>= not y) xor z", ( not x>= not y)^z);
    CHECK_AST(" not (x)>= not y xor z",  not (x)>= not y^z);
    CHECK_AST(" not (x>= not y) xor z",  not (x>= not y)^z);
    CHECK_AST(" not x>=( not y) xor z",  not x>=( not y)^z);
    CHECK_AST(" not x>= not (y) xor z",  not x>= not (y)^z);
    CHECK_AST("( not x)>= not y xor  +z", ( not x)>= not y^ +z);
    CHECK_AST("( not x>= not y) xor  +z", ( not x>= not y)^ +z);
    CHECK_AST(" not (x)>= not y xor  +z",  not (x)>= not y^ +z);
    CHECK_AST(" not (x>= not y) xor  +z",  not (x>= not y)^ +z);
    CHECK_AST(" not x>=( not y) xor  +z",  not x>=( not y)^ +z);
    CHECK_AST(" not x>= not (y) xor  +z",  not x>= not (y)^ +z);
    CHECK_AST("( not x)>= not y xor  -z", ( not x)>= not y^ -z);
    CHECK_AST("( not x>= not y) xor  -z", ( not x>= not y)^ -z);
    CHECK_AST(" not (x)>= not y xor  -z",  not (x)>= not y^ -z);
    CHECK_AST(" not (x>= not y) xor  -z",  not (x>= not y)^ -z);
    CHECK_AST(" not x>=( not y) xor  -z",  not x>=( not y)^ -z);
    CHECK_AST(" not x>= not (y) xor  -z",  not x>= not (y)^ -z);
    CHECK_AST("( not x)>= not y xor  not z", ( not x)>= not y^ not z);
    CHECK_AST("( not x>= not y) xor  not z", ( not x>= not y)^ not z);
    CHECK_AST(" not (x)>= not y xor  not z",  not (x)>= not y^ not z);
    CHECK_AST(" not (x>= not y) xor  not z",  not (x>= not y)^ not z);
    CHECK_AST(" not x>=( not y) xor  not z",  not x>=( not y)^ not z);
    CHECK_AST(" not x>= not (y) xor  not z",  not x>= not (y)^ not z);
    CHECK_AST("(x)>=y or z", (x)>=y|z);
    CHECK_AST("(x>=y) or z", (x>=y)|z);
    CHECK_AST("x>=(y) or z", x>=(y)|z);
    CHECK_AST("(x)>=y or  +z", (x)>=y| +z);
    CHECK_AST("(x>=y) or  +z", (x>=y)| +z);
    CHECK_AST("x>=(y) or  +z", x>=(y)| +z);
    CHECK_AST("(x)>=y or  -z", (x)>=y| -z);
    CHECK_AST("(x>=y) or  -z", (x>=y)| -z);
    CHECK_AST("x>=(y) or  -z", x>=(y)| -z);
    CHECK_AST("(x)>=y or  not z", (x)>=y| not z);
    CHECK_AST("(x>=y) or  not z", (x>=y)| not z);
    CHECK_AST("x>=(y) or  not z", x>=(y)| not z);
    CHECK_AST("(x)>= +y or z", (x)>= +y|z);
    CHECK_AST("(x>= +y) or z", (x>= +y)|z);
    CHECK_AST("x>=( +y) or z", x>=( +y)|z);
    CHECK_AST("x>= +(y) or z", x>= +(y)|z);
    CHECK_AST("(x)>= +y or  +z", (x)>= +y| +z);
    CHECK_AST("(x>= +y) or  +z", (x>= +y)| +z);
    CHECK_AST("x>=( +y) or  +z", x>=( +y)| +z);
    CHECK_AST("x>= +(y) or  +z", x>= +(y)| +z);
    CHECK_AST("(x)>= +y or  -z", (x)>= +y| -z);
    CHECK_AST("(x>= +y) or  -z", (x>= +y)| -z);
    CHECK_AST("x>=( +y) or  -z", x>=( +y)| -z);
    CHECK_AST("x>= +(y) or  -z", x>= +(y)| -z);
    CHECK_AST("(x)>= +y or  not z", (x)>= +y| not z);
    CHECK_AST("(x>= +y) or  not z", (x>= +y)| not z);
    CHECK_AST("x>=( +y) or  not z", x>=( +y)| not z);
    CHECK_AST("x>= +(y) or  not z", x>= +(y)| not z);
    CHECK_AST("(x)>= -y or z", (x)>= -y|z);
    CHECK_AST("(x>= -y) or z", (x>= -y)|z);
    CHECK_AST("x>=( -y) or z", x>=( -y)|z);
    CHECK_AST("x>= -(y) or z", x>= -(y)|z);
    CHECK_AST("(x)>= -y or  +z", (x)>= -y| +z);
    CHECK_AST("(x>= -y) or  +z", (x>= -y)| +z);
    CHECK_AST("x>=( -y) or  +z", x>=( -y)| +z);
    CHECK_AST("x>= -(y) or  +z", x>= -(y)| +z);
    CHECK_AST("(x)>= -y or  -z", (x)>= -y| -z);
    CHECK_AST("(x>= -y) or  -z", (x>= -y)| -z);
    CHECK_AST("x>=( -y) or  -z", x>=( -y)| -z);
    CHECK_AST("x>= -(y) or  -z", x>= -(y)| -z);
    CHECK_AST("(x)>= -y or  not z", (x)>= -y| not z);
    CHECK_AST("(x>= -y) or  not z", (x>= -y)| not z);
    CHECK_AST("x>=( -y) or  not z", x>=( -y)| not z);
    CHECK_AST("x>= -(y) or  not z", x>= -(y)| not z);
    CHECK_AST("(x)>= not y or z", (x)>= not y|z);
    CHECK_AST("(x>= not y) or z", (x>= not y)|z);
    CHECK_AST("x>=( not y) or z", x>=( not y)|z);
    CHECK_AST("x>= not (y) or z", x>= not (y)|z);
    CHECK_AST("(x)>= not y or  +z", (x)>= not y| +z);
    CHECK_AST("(x>= not y) or  +z", (x>= not y)| +z);
    CHECK_AST("x>=( not y) or  +z", x>=( not y)| +z);
    CHECK_AST("x>= not (y) or  +z", x>= not (y)| +z);
    CHECK_AST("(x)>= not y or  -z", (x)>= not y| -z);
    CHECK_AST("(x>= not y) or  -z", (x>= not y)| -z);
    CHECK_AST("x>=( not y) or  -z", x>=( not y)| -z);
    CHECK_AST("x>= not (y) or  -z", x>= not (y)| -z);
    CHECK_AST("(x)>= not y or  not z", (x)>= not y| not z);
    CHECK_AST("(x>= not y) or  not z", (x>= not y)| not z);
    CHECK_AST("x>=( not y) or  not z", x>=( not y)| not z);
    CHECK_AST("x>= not (y) or  not z", x>= not (y)| not z);
    CHECK_AST("( +x)>=y or z", ( +x)>=y|z);
    CHECK_AST("( +x>=y) or z", ( +x>=y)|z);
    CHECK_AST(" +(x)>=y or z",  +(x)>=y|z);
    CHECK_AST(" +(x>=y) or z",  +(x>=y)|z);
    CHECK_AST(" +x>=(y) or z",  +x>=(y)|z);
    CHECK_AST("( +x)>=y or  +z", ( +x)>=y| +z);
    CHECK_AST("( +x>=y) or  +z", ( +x>=y)| +z);
    CHECK_AST(" +(x)>=y or  +z",  +(x)>=y| +z);
    CHECK_AST(" +(x>=y) or  +z",  +(x>=y)| +z);
    CHECK_AST(" +x>=(y) or  +z",  +x>=(y)| +z);
    CHECK_AST("( +x)>=y or  -z", ( +x)>=y| -z);
    CHECK_AST("( +x>=y) or  -z", ( +x>=y)| -z);
    CHECK_AST(" +(x)>=y or  -z",  +(x)>=y| -z);
    CHECK_AST(" +(x>=y) or  -z",  +(x>=y)| -z);
    CHECK_AST(" +x>=(y) or  -z",  +x>=(y)| -z);
    CHECK_AST("( +x)>=y or  not z", ( +x)>=y| not z);
    CHECK_AST("( +x>=y) or  not z", ( +x>=y)| not z);
    CHECK_AST(" +(x)>=y or  not z",  +(x)>=y| not z);
    CHECK_AST(" +(x>=y) or  not z",  +(x>=y)| not z);
    CHECK_AST(" +x>=(y) or  not z",  +x>=(y)| not z);
    CHECK_AST("( +x)>= +y or z", ( +x)>= +y|z);
    CHECK_AST("( +x>= +y) or z", ( +x>= +y)|z);
    CHECK_AST(" +(x)>= +y or z",  +(x)>= +y|z);
    CHECK_AST(" +(x>= +y) or z",  +(x>= +y)|z);
    CHECK_AST(" +x>=( +y) or z",  +x>=( +y)|z);
    CHECK_AST(" +x>= +(y) or z",  +x>= +(y)|z);
    CHECK_AST("( +x)>= +y or  +z", ( +x)>= +y| +z);
    CHECK_AST("( +x>= +y) or  +z", ( +x>= +y)| +z);
    CHECK_AST(" +(x)>= +y or  +z",  +(x)>= +y| +z);
    CHECK_AST(" +(x>= +y) or  +z",  +(x>= +y)| +z);
    CHECK_AST(" +x>=( +y) or  +z",  +x>=( +y)| +z);
    CHECK_AST(" +x>= +(y) or  +z",  +x>= +(y)| +z);
    CHECK_AST("( +x)>= +y or  -z", ( +x)>= +y| -z);
    CHECK_AST("( +x>= +y) or  -z", ( +x>= +y)| -z);
    CHECK_AST(" +(x)>= +y or  -z",  +(x)>= +y| -z);
    CHECK_AST(" +(x>= +y) or  -z",  +(x>= +y)| -z);
    CHECK_AST(" +x>=( +y) or  -z",  +x>=( +y)| -z);
    CHECK_AST(" +x>= +(y) or  -z",  +x>= +(y)| -z);
    CHECK_AST("( +x)>= +y or  not z", ( +x)>= +y| not z);
    CHECK_AST("( +x>= +y) or  not z", ( +x>= +y)| not z);
    CHECK_AST(" +(x)>= +y or  not z",  +(x)>= +y| not z);
    CHECK_AST(" +(x>= +y) or  not z",  +(x>= +y)| not z);
    CHECK_AST(" +x>=( +y) or  not z",  +x>=( +y)| not z);
    CHECK_AST(" +x>= +(y) or  not z",  +x>= +(y)| not z);
    CHECK_AST("( +x)>= -y or z", ( +x)>= -y|z);
    CHECK_AST("( +x>= -y) or z", ( +x>= -y)|z);
    CHECK_AST(" +(x)>= -y or z",  +(x)>= -y|z);
    CHECK_AST(" +(x>= -y) or z",  +(x>= -y)|z);
    CHECK_AST(" +x>=( -y) or z",  +x>=( -y)|z);
    CHECK_AST(" +x>= -(y) or z",  +x>= -(y)|z);
    CHECK_AST("( +x)>= -y or  +z", ( +x)>= -y| +z);
    CHECK_AST("( +x>= -y) or  +z", ( +x>= -y)| +z);
    CHECK_AST(" +(x)>= -y or  +z",  +(x)>= -y| +z);
    CHECK_AST(" +(x>= -y) or  +z",  +(x>= -y)| +z);
    CHECK_AST(" +x>=( -y) or  +z",  +x>=( -y)| +z);
    CHECK_AST(" +x>= -(y) or  +z",  +x>= -(y)| +z);
    CHECK_AST("( +x)>= -y or  -z", ( +x)>= -y| -z);
    CHECK_AST("( +x>= -y) or  -z", ( +x>= -y)| -z);
    CHECK_AST(" +(x)>= -y or  -z",  +(x)>= -y| -z);
    CHECK_AST(" +(x>= -y) or  -z",  +(x>= -y)| -z);
    CHECK_AST(" +x>=( -y) or  -z",  +x>=( -y)| -z);
    CHECK_AST(" +x>= -(y) or  -z",  +x>= -(y)| -z);
    CHECK_AST("( +x)>= -y or  not z", ( +x)>= -y| not z);
    CHECK_AST("( +x>= -y) or  not z", ( +x>= -y)| not z);
    CHECK_AST(" +(x)>= -y or  not z",  +(x)>= -y| not z);
    CHECK_AST(" +(x>= -y) or  not z",  +(x>= -y)| not z);
    CHECK_AST(" +x>=( -y) or  not z",  +x>=( -y)| not z);
    CHECK_AST(" +x>= -(y) or  not z",  +x>= -(y)| not z);
    CHECK_AST("( +x)>= not y or z", ( +x)>= not y|z);
    CHECK_AST("( +x>= not y) or z", ( +x>= not y)|z);
    CHECK_AST(" +(x)>= not y or z",  +(x)>= not y|z);
    CHECK_AST(" +(x>= not y) or z",  +(x>= not y)|z);
    CHECK_AST(" +x>=( not y) or z",  +x>=( not y)|z);
    CHECK_AST(" +x>= not (y) or z",  +x>= not (y)|z);
    CHECK_AST("( +x)>= not y or  +z", ( +x)>= not y| +z);
    CHECK_AST("( +x>= not y) or  +z", ( +x>= not y)| +z);
    CHECK_AST(" +(x)>= not y or  +z",  +(x)>= not y| +z);
    CHECK_AST(" +(x>= not y) or  +z",  +(x>= not y)| +z);
    CHECK_AST(" +x>=( not y) or  +z",  +x>=( not y)| +z);
    CHECK_AST(" +x>= not (y) or  +z",  +x>= not (y)| +z);
    CHECK_AST("( +x)>= not y or  -z", ( +x)>= not y| -z);
    CHECK_AST("( +x>= not y) or  -z", ( +x>= not y)| -z);
    CHECK_AST(" +(x)>= not y or  -z",  +(x)>= not y| -z);
    CHECK_AST(" +(x>= not y) or  -z",  +(x>= not y)| -z);
    CHECK_AST(" +x>=( not y) or  -z",  +x>=( not y)| -z);
    CHECK_AST(" +x>= not (y) or  -z",  +x>= not (y)| -z);
    CHECK_AST("( +x)>= not y or  not z", ( +x)>= not y| not z);
    CHECK_AST("( +x>= not y) or  not z", ( +x>= not y)| not z);
    CHECK_AST(" +(x)>= not y or  not z",  +(x)>= not y| not z);
    CHECK_AST(" +(x>= not y) or  not z",  +(x>= not y)| not z);
    CHECK_AST(" +x>=( not y) or  not z",  +x>=( not y)| not z);
    CHECK_AST(" +x>= not (y) or  not z",  +x>= not (y)| not z);
    CHECK_AST("( -x)>=y or z", ( -x)>=y|z);
    CHECK_AST("( -x>=y) or z", ( -x>=y)|z);
    CHECK_AST(" -(x)>=y or z",  -(x)>=y|z);
    CHECK_AST(" -(x>=y) or z",  -(x>=y)|z);
    CHECK_AST(" -x>=(y) or z",  -x>=(y)|z);
    CHECK_AST("( -x)>=y or  +z", ( -x)>=y| +z);
    CHECK_AST("( -x>=y) or  +z", ( -x>=y)| +z);
    CHECK_AST(" -(x)>=y or  +z",  -(x)>=y| +z);
    CHECK_AST(" -(x>=y) or  +z",  -(x>=y)| +z);
    CHECK_AST(" -x>=(y) or  +z",  -x>=(y)| +z);
    CHECK_AST("( -x)>=y or  -z", ( -x)>=y| -z);
    CHECK_AST("( -x>=y) or  -z", ( -x>=y)| -z);
    CHECK_AST(" -(x)>=y or  -z",  -(x)>=y| -z);
    CHECK_AST(" -(x>=y) or  -z",  -(x>=y)| -z);
    CHECK_AST(" -x>=(y) or  -z",  -x>=(y)| -z);
    CHECK_AST("( -x)>=y or  not z", ( -x)>=y| not z);
    CHECK_AST("( -x>=y) or  not z", ( -x>=y)| not z);
    CHECK_AST(" -(x)>=y or  not z",  -(x)>=y| not z);
    CHECK_AST(" -(x>=y) or  not z",  -(x>=y)| not z);
    CHECK_AST(" -x>=(y) or  not z",  -x>=(y)| not z);
    CHECK_AST("( -x)>= +y or z", ( -x)>= +y|z);
    CHECK_AST("( -x>= +y) or z", ( -x>= +y)|z);
    CHECK_AST(" -(x)>= +y or z",  -(x)>= +y|z);
    CHECK_AST(" -(x>= +y) or z",  -(x>= +y)|z);
    CHECK_AST(" -x>=( +y) or z",  -x>=( +y)|z);
    CHECK_AST(" -x>= +(y) or z",  -x>= +(y)|z);
    CHECK_AST("( -x)>= +y or  +z", ( -x)>= +y| +z);
    CHECK_AST("( -x>= +y) or  +z", ( -x>= +y)| +z);
    CHECK_AST(" -(x)>= +y or  +z",  -(x)>= +y| +z);
    CHECK_AST(" -(x>= +y) or  +z",  -(x>= +y)| +z);
    CHECK_AST(" -x>=( +y) or  +z",  -x>=( +y)| +z);
    CHECK_AST(" -x>= +(y) or  +z",  -x>= +(y)| +z);
    CHECK_AST("( -x)>= +y or  -z", ( -x)>= +y| -z);
    CHECK_AST("( -x>= +y) or  -z", ( -x>= +y)| -z);
    CHECK_AST(" -(x)>= +y or  -z",  -(x)>= +y| -z);
    CHECK_AST(" -(x>= +y) or  -z",  -(x>= +y)| -z);
    CHECK_AST(" -x>=( +y) or  -z",  -x>=( +y)| -z);
    CHECK_AST(" -x>= +(y) or  -z",  -x>= +(y)| -z);
    CHECK_AST("( -x)>= +y or  not z", ( -x)>= +y| not z);
    CHECK_AST("( -x>= +y) or  not z", ( -x>= +y)| not z);
    CHECK_AST(" -(x)>= +y or  not z",  -(x)>= +y| not z);
    CHECK_AST(" -(x>= +y) or  not z",  -(x>= +y)| not z);
    CHECK_AST(" -x>=( +y) or  not z",  -x>=( +y)| not z);
    CHECK_AST(" -x>= +(y) or  not z",  -x>= +(y)| not z);
    CHECK_AST("( -x)>= -y or z", ( -x)>= -y|z);
    CHECK_AST("( -x>= -y) or z", ( -x>= -y)|z);
    CHECK_AST(" -(x)>= -y or z",  -(x)>= -y|z);
    CHECK_AST(" -(x>= -y) or z",  -(x>= -y)|z);
    CHECK_AST(" -x>=( -y) or z",  -x>=( -y)|z);
    CHECK_AST(" -x>= -(y) or z",  -x>= -(y)|z);
    CHECK_AST("( -x)>= -y or  +z", ( -x)>= -y| +z);
    CHECK_AST("( -x>= -y) or  +z", ( -x>= -y)| +z);
    CHECK_AST(" -(x)>= -y or  +z",  -(x)>= -y| +z);
    CHECK_AST(" -(x>= -y) or  +z",  -(x>= -y)| +z);
    CHECK_AST(" -x>=( -y) or  +z",  -x>=( -y)| +z);
    CHECK_AST(" -x>= -(y) or  +z",  -x>= -(y)| +z);
    CHECK_AST("( -x)>= -y or  -z", ( -x)>= -y| -z);
    CHECK_AST("( -x>= -y) or  -z", ( -x>= -y)| -z);
    CHECK_AST(" -(x)>= -y or  -z",  -(x)>= -y| -z);
    CHECK_AST(" -(x>= -y) or  -z",  -(x>= -y)| -z);
    CHECK_AST(" -x>=( -y) or  -z",  -x>=( -y)| -z);
    CHECK_AST(" -x>= -(y) or  -z",  -x>= -(y)| -z);
    CHECK_AST("( -x)>= -y or  not z", ( -x)>= -y| not z);
    CHECK_AST("( -x>= -y) or  not z", ( -x>= -y)| not z);
    CHECK_AST(" -(x)>= -y or  not z",  -(x)>= -y| not z);
    CHECK_AST(" -(x>= -y) or  not z",  -(x>= -y)| not z);
    CHECK_AST(" -x>=( -y) or  not z",  -x>=( -y)| not z);
    CHECK_AST(" -x>= -(y) or  not z",  -x>= -(y)| not z);
    CHECK_AST("( -x)>= not y or z", ( -x)>= not y|z);
    CHECK_AST("( -x>= not y) or z", ( -x>= not y)|z);
    CHECK_AST(" -(x)>= not y or z",  -(x)>= not y|z);
    CHECK_AST(" -(x>= not y) or z",  -(x>= not y)|z);
    CHECK_AST(" -x>=( not y) or z",  -x>=( not y)|z);
    CHECK_AST(" -x>= not (y) or z",  -x>= not (y)|z);
    CHECK_AST("( -x)>= not y or  +z", ( -x)>= not y| +z);
    CHECK_AST("( -x>= not y) or  +z", ( -x>= not y)| +z);
    CHECK_AST(" -(x)>= not y or  +z",  -(x)>= not y| +z);
    CHECK_AST(" -(x>= not y) or  +z",  -(x>= not y)| +z);
    CHECK_AST(" -x>=( not y) or  +z",  -x>=( not y)| +z);
    CHECK_AST(" -x>= not (y) or  +z",  -x>= not (y)| +z);
    CHECK_AST("( -x)>= not y or  -z", ( -x)>= not y| -z);
    CHECK_AST("( -x>= not y) or  -z", ( -x>= not y)| -z);
    CHECK_AST(" -(x)>= not y or  -z",  -(x)>= not y| -z);
    CHECK_AST(" -(x>= not y) or  -z",  -(x>= not y)| -z);
    CHECK_AST(" -x>=( not y) or  -z",  -x>=( not y)| -z);
    CHECK_AST(" -x>= not (y) or  -z",  -x>= not (y)| -z);
    CHECK_AST("( -x)>= not y or  not z", ( -x)>= not y| not z);
    CHECK_AST("( -x>= not y) or  not z", ( -x>= not y)| not z);
    CHECK_AST(" -(x)>= not y or  not z",  -(x)>= not y| not z);
    CHECK_AST(" -(x>= not y) or  not z",  -(x>= not y)| not z);
    CHECK_AST(" -x>=( not y) or  not z",  -x>=( not y)| not z);
    CHECK_AST(" -x>= not (y) or  not z",  -x>= not (y)| not z);
    CHECK_AST("( not x)>=y or z", ( not x)>=y|z);
    CHECK_AST("( not x>=y) or z", ( not x>=y)|z);
    CHECK_AST(" not (x)>=y or z",  not (x)>=y|z);
    CHECK_AST(" not (x>=y) or z",  not (x>=y)|z);
    CHECK_AST(" not x>=(y) or z",  not x>=(y)|z);
    CHECK_AST("( not x)>=y or  +z", ( not x)>=y| +z);
    CHECK_AST("( not x>=y) or  +z", ( not x>=y)| +z);
    CHECK_AST(" not (x)>=y or  +z",  not (x)>=y| +z);
    CHECK_AST(" not (x>=y) or  +z",  not (x>=y)| +z);
    CHECK_AST(" not x>=(y) or  +z",  not x>=(y)| +z);
    CHECK_AST("( not x)>=y or  -z", ( not x)>=y| -z);
    CHECK_AST("( not x>=y) or  -z", ( not x>=y)| -z);
    CHECK_AST(" not (x)>=y or  -z",  not (x)>=y| -z);
    CHECK_AST(" not (x>=y) or  -z",  not (x>=y)| -z);
    CHECK_AST(" not x>=(y) or  -z",  not x>=(y)| -z);
    CHECK_AST("( not x)>=y or  not z", ( not x)>=y| not z);
    CHECK_AST("( not x>=y) or  not z", ( not x>=y)| not z);
    CHECK_AST(" not (x)>=y or  not z",  not (x)>=y| not z);
    CHECK_AST(" not (x>=y) or  not z",  not (x>=y)| not z);
    CHECK_AST(" not x>=(y) or  not z",  not x>=(y)| not z);
    CHECK_AST("( not x)>= +y or z", ( not x)>= +y|z);
    CHECK_AST("( not x>= +y) or z", ( not x>= +y)|z);
    CHECK_AST(" not (x)>= +y or z",  not (x)>= +y|z);
    CHECK_AST(" not (x>= +y) or z",  not (x>= +y)|z);
    CHECK_AST(" not x>=( +y) or z",  not x>=( +y)|z);
    CHECK_AST(" not x>= +(y) or z",  not x>= +(y)|z);
    CHECK_AST("( not x)>= +y or  +z", ( not x)>= +y| +z);
    CHECK_AST("( not x>= +y) or  +z", ( not x>= +y)| +z);
    CHECK_AST(" not (x)>= +y or  +z",  not (x)>= +y| +z);
    CHECK_AST(" not (x>= +y) or  +z",  not (x>= +y)| +z);
    CHECK_AST(" not x>=( +y) or  +z",  not x>=( +y)| +z);
    CHECK_AST(" not x>= +(y) or  +z",  not x>= +(y)| +z);
    CHECK_AST("( not x)>= +y or  -z", ( not x)>= +y| -z);
    CHECK_AST("( not x>= +y) or  -z", ( not x>= +y)| -z);
    CHECK_AST(" not (x)>= +y or  -z",  not (x)>= +y| -z);
    CHECK_AST(" not (x>= +y) or  -z",  not (x>= +y)| -z);
    CHECK_AST(" not x>=( +y) or  -z",  not x>=( +y)| -z);
    CHECK_AST(" not x>= +(y) or  -z",  not x>= +(y)| -z);
    CHECK_AST("( not x)>= +y or  not z", ( not x)>= +y| not z);
    CHECK_AST("( not x>= +y) or  not z", ( not x>= +y)| not z);
    CHECK_AST(" not (x)>= +y or  not z",  not (x)>= +y| not z);
    CHECK_AST(" not (x>= +y) or  not z",  not (x>= +y)| not z);
    CHECK_AST(" not x>=( +y) or  not z",  not x>=( +y)| not z);
    CHECK_AST(" not x>= +(y) or  not z",  not x>= +(y)| not z);
    CHECK_AST("( not x)>= -y or z", ( not x)>= -y|z);
    CHECK_AST("( not x>= -y) or z", ( not x>= -y)|z);
    CHECK_AST(" not (x)>= -y or z",  not (x)>= -y|z);
    CHECK_AST(" not (x>= -y) or z",  not (x>= -y)|z);
    CHECK_AST(" not x>=( -y) or z",  not x>=( -y)|z);
    CHECK_AST(" not x>= -(y) or z",  not x>= -(y)|z);
    CHECK_AST("( not x)>= -y or  +z", ( not x)>= -y| +z);
    CHECK_AST("( not x>= -y) or  +z", ( not x>= -y)| +z);
    CHECK_AST(" not (x)>= -y or  +z",  not (x)>= -y| +z);
    CHECK_AST(" not (x>= -y) or  +z",  not (x>= -y)| +z);
    CHECK_AST(" not x>=( -y) or  +z",  not x>=( -y)| +z);
    CHECK_AST(" not x>= -(y) or  +z",  not x>= -(y)| +z);
    CHECK_AST("( not x)>= -y or  -z", ( not x)>= -y| -z);
    CHECK_AST("( not x>= -y) or  -z", ( not x>= -y)| -z);
    CHECK_AST(" not (x)>= -y or  -z",  not (x)>= -y| -z);
    CHECK_AST(" not (x>= -y) or  -z",  not (x>= -y)| -z);
    CHECK_AST(" not x>=( -y) or  -z",  not x>=( -y)| -z);
    CHECK_AST(" not x>= -(y) or  -z",  not x>= -(y)| -z);
    CHECK_AST("( not x)>= -y or  not z", ( not x)>= -y| not z);
    CHECK_AST("( not x>= -y) or  not z", ( not x>= -y)| not z);
    CHECK_AST(" not (x)>= -y or  not z",  not (x)>= -y| not z);
    CHECK_AST(" not (x>= -y) or  not z",  not (x>= -y)| not z);
    CHECK_AST(" not x>=( -y) or  not z",  not x>=( -y)| not z);
    CHECK_AST(" not x>= -(y) or  not z",  not x>= -(y)| not z);
    CHECK_AST("( not x)>= not y or z", ( not x)>= not y|z);
    CHECK_AST("( not x>= not y) or z", ( not x>= not y)|z);
    CHECK_AST(" not (x)>= not y or z",  not (x)>= not y|z);
    CHECK_AST(" not (x>= not y) or z",  not (x>= not y)|z);
    CHECK_AST(" not x>=( not y) or z",  not x>=( not y)|z);
    CHECK_AST(" not x>= not (y) or z",  not x>= not (y)|z);
    CHECK_AST("( not x)>= not y or  +z", ( not x)>= not y| +z);
    CHECK_AST("( not x>= not y) or  +z", ( not x>= not y)| +z);
    CHECK_AST(" not (x)>= not y or  +z",  not (x)>= not y| +z);
    CHECK_AST(" not (x>= not y) or  +z",  not (x>= not y)| +z);
    CHECK_AST(" not x>=( not y) or  +z",  not x>=( not y)| +z);
    CHECK_AST(" not x>= not (y) or  +z",  not x>= not (y)| +z);
    CHECK_AST("( not x)>= not y or  -z", ( not x)>= not y| -z);
    CHECK_AST("( not x>= not y) or  -z", ( not x>= not y)| -z);
    CHECK_AST(" not (x)>= not y or  -z",  not (x)>= not y| -z);
    CHECK_AST(" not (x>= not y) or  -z",  not (x>= not y)| -z);
    CHECK_AST(" not x>=( not y) or  -z",  not x>=( not y)| -z);
    CHECK_AST(" not x>= not (y) or  -z",  not x>= not (y)| -z);
    CHECK_AST("( not x)>= not y or  not z", ( not x)>= not y| not z);
    CHECK_AST("( not x>= not y) or  not z", ( not x>= not y)| not z);
    CHECK_AST(" not (x)>= not y or  not z",  not (x)>= not y| not z);
    CHECK_AST(" not (x>= not y) or  not z",  not (x>= not y)| not z);
    CHECK_AST(" not x>=( not y) or  not z",  not x>=( not y)| not z);
    CHECK_AST(" not x>= not (y) or  not z",  not x>= not (y)| not z);
    CHECK_AST("(x)=y*z", (x)==y*z);
    CHECK_AST("(x=y)*z", (x==y)*z);
    CHECK_AST("x=(y)*z", x==(y)*z);
    CHECK_AST("(x)=y* +z", (x)==y* +z);
    CHECK_AST("(x=y)* +z", (x==y)* +z);
    CHECK_AST("x=(y)* +z", x==(y)* +z);
    CHECK_AST("(x)=y* -z", (x)==y* -z);
    CHECK_AST("(x=y)* -z", (x==y)* -z);
    CHECK_AST("x=(y)* -z", x==(y)* -z);
    CHECK_AST("(x)=y* not z", (x)==y* not z);
    CHECK_AST("(x=y)* not z", (x==y)* not z);
    CHECK_AST("x=(y)* not z", x==(y)* not z);
    CHECK_AST("(x)= +y*z", (x)== +y*z);
    CHECK_AST("(x= +y)*z", (x== +y)*z);
    CHECK_AST("x=( +y)*z", x==( +y)*z);
    CHECK_AST("x= +(y)*z", x== +(y)*z);
    CHECK_AST("(x)= +y* +z", (x)== +y* +z);
    CHECK_AST("(x= +y)* +z", (x== +y)* +z);
    CHECK_AST("x=( +y)* +z", x==( +y)* +z);
    CHECK_AST("x= +(y)* +z", x== +(y)* +z);
    CHECK_AST("(x)= +y* -z", (x)== +y* -z);
    CHECK_AST("(x= +y)* -z", (x== +y)* -z);
    CHECK_AST("x=( +y)* -z", x==( +y)* -z);
    CHECK_AST("x= +(y)* -z", x== +(y)* -z);
    CHECK_AST("(x)= +y* not z", (x)== +y* not z);
    CHECK_AST("(x= +y)* not z", (x== +y)* not z);
    CHECK_AST("x=( +y)* not z", x==( +y)* not z);
    CHECK_AST("x= +(y)* not z", x== +(y)* not z);
    CHECK_AST("(x)= -y*z", (x)== -y*z);
    CHECK_AST("(x= -y)*z", (x== -y)*z);
    CHECK_AST("x=( -y)*z", x==( -y)*z);
    CHECK_AST("x= -(y)*z", x== -(y)*z);
    CHECK_AST("(x)= -y* +z", (x)== -y* +z);
    CHECK_AST("(x= -y)* +z", (x== -y)* +z);
    CHECK_AST("x=( -y)* +z", x==( -y)* +z);
    CHECK_AST("x= -(y)* +z", x== -(y)* +z);
    CHECK_AST("(x)= -y* -z", (x)== -y* -z);
    CHECK_AST("(x= -y)* -z", (x== -y)* -z);
    CHECK_AST("x=( -y)* -z", x==( -y)* -z);
    CHECK_AST("x= -(y)* -z", x== -(y)* -z);
    CHECK_AST("(x)= -y* not z", (x)== -y* not z);
    CHECK_AST("(x= -y)* not z", (x== -y)* not z);
    CHECK_AST("x=( -y)* not z", x==( -y)* not z);
    CHECK_AST("x= -(y)* not z", x== -(y)* not z);
    CHECK_AST("(x)= not y*z", (x)== not y*z);
    CHECK_AST("(x= not y)*z", (x== not y)*z);
    CHECK_AST("x=( not y)*z", x==( not y)*z);
    CHECK_AST("x= not (y)*z", x== not (y)*z);
    CHECK_AST("(x)= not y* +z", (x)== not y* +z);
    CHECK_AST("(x= not y)* +z", (x== not y)* +z);
    CHECK_AST("x=( not y)* +z", x==( not y)* +z);
    CHECK_AST("x= not (y)* +z", x== not (y)* +z);
    CHECK_AST("(x)= not y* -z", (x)== not y* -z);
    CHECK_AST("(x= not y)* -z", (x== not y)* -z);
    CHECK_AST("x=( not y)* -z", x==( not y)* -z);
    CHECK_AST("x= not (y)* -z", x== not (y)* -z);
    CHECK_AST("(x)= not y* not z", (x)== not y* not z);
    CHECK_AST("(x= not y)* not z", (x== not y)* not z);
    CHECK_AST("x=( not y)* not z", x==( not y)* not z);
    CHECK_AST("x= not (y)* not z", x== not (y)* not z);
    CHECK_AST("( +x)=y*z", ( +x)==y*z);
    CHECK_AST("( +x=y)*z", ( +x==y)*z);
    CHECK_AST(" +(x)=y*z",  +(x)==y*z);
    CHECK_AST(" +(x=y)*z",  +(x==y)*z);
    CHECK_AST(" +x=(y)*z",  +x==(y)*z);
    CHECK_AST("( +x)=y* +z", ( +x)==y* +z);
    CHECK_AST("( +x=y)* +z", ( +x==y)* +z);
    CHECK_AST(" +(x)=y* +z",  +(x)==y* +z);
    CHECK_AST(" +(x=y)* +z",  +(x==y)* +z);
    CHECK_AST(" +x=(y)* +z",  +x==(y)* +z);
    CHECK_AST("( +x)=y* -z", ( +x)==y* -z);
    CHECK_AST("( +x=y)* -z", ( +x==y)* -z);
    CHECK_AST(" +(x)=y* -z",  +(x)==y* -z);
    CHECK_AST(" +(x=y)* -z",  +(x==y)* -z);
    CHECK_AST(" +x=(y)* -z",  +x==(y)* -z);
    CHECK_AST("( +x)=y* not z", ( +x)==y* not z);
    CHECK_AST("( +x=y)* not z", ( +x==y)* not z);
    CHECK_AST(" +(x)=y* not z",  +(x)==y* not z);
    CHECK_AST(" +(x=y)* not z",  +(x==y)* not z);
    CHECK_AST(" +x=(y)* not z",  +x==(y)* not z);
    CHECK_AST("( +x)= +y*z", ( +x)== +y*z);
    CHECK_AST("( +x= +y)*z", ( +x== +y)*z);
    CHECK_AST(" +(x)= +y*z",  +(x)== +y*z);
    CHECK_AST(" +(x= +y)*z",  +(x== +y)*z);
    CHECK_AST(" +x=( +y)*z",  +x==( +y)*z);
    CHECK_AST(" +x= +(y)*z",  +x== +(y)*z);
    CHECK_AST("( +x)= +y* +z", ( +x)== +y* +z);
    CHECK_AST("( +x= +y)* +z", ( +x== +y)* +z);
    CHECK_AST(" +(x)= +y* +z",  +(x)== +y* +z);
    CHECK_AST(" +(x= +y)* +z",  +(x== +y)* +z);
    CHECK_AST(" +x=( +y)* +z",  +x==( +y)* +z);
    CHECK_AST(" +x= +(y)* +z",  +x== +(y)* +z);
    CHECK_AST("( +x)= +y* -z", ( +x)== +y* -z);
    CHECK_AST("( +x= +y)* -z", ( +x== +y)* -z);
    CHECK_AST(" +(x)= +y* -z",  +(x)== +y* -z);
    CHECK_AST(" +(x= +y)* -z",  +(x== +y)* -z);
    CHECK_AST(" +x=( +y)* -z",  +x==( +y)* -z);
    CHECK_AST(" +x= +(y)* -z",  +x== +(y)* -z);
    CHECK_AST("( +x)= +y* not z", ( +x)== +y* not z);
    CHECK_AST("( +x= +y)* not z", ( +x== +y)* not z);
    CHECK_AST(" +(x)= +y* not z",  +(x)== +y* not z);
    CHECK_AST(" +(x= +y)* not z",  +(x== +y)* not z);
    CHECK_AST(" +x=( +y)* not z",  +x==( +y)* not z);
    CHECK_AST(" +x= +(y)* not z",  +x== +(y)* not z);
    CHECK_AST("( +x)= -y*z", ( +x)== -y*z);
    CHECK_AST("( +x= -y)*z", ( +x== -y)*z);
    CHECK_AST(" +(x)= -y*z",  +(x)== -y*z);
    CHECK_AST(" +(x= -y)*z",  +(x== -y)*z);
    CHECK_AST(" +x=( -y)*z",  +x==( -y)*z);
    CHECK_AST(" +x= -(y)*z",  +x== -(y)*z);
    CHECK_AST("( +x)= -y* +z", ( +x)== -y* +z);
    CHECK_AST("( +x= -y)* +z", ( +x== -y)* +z);
    CHECK_AST(" +(x)= -y* +z",  +(x)== -y* +z);
    CHECK_AST(" +(x= -y)* +z",  +(x== -y)* +z);
    CHECK_AST(" +x=( -y)* +z",  +x==( -y)* +z);
    CHECK_AST(" +x= -(y)* +z",  +x== -(y)* +z);
    CHECK_AST("( +x)= -y* -z", ( +x)== -y* -z);
    CHECK_AST("( +x= -y)* -z", ( +x== -y)* -z);
    CHECK_AST(" +(x)= -y* -z",  +(x)== -y* -z);
    CHECK_AST(" +(x= -y)* -z",  +(x== -y)* -z);
    CHECK_AST(" +x=( -y)* -z",  +x==( -y)* -z);
    CHECK_AST(" +x= -(y)* -z",  +x== -(y)* -z);
    CHECK_AST("( +x)= -y* not z", ( +x)== -y* not z);
    CHECK_AST("( +x= -y)* not z", ( +x== -y)* not z);
    CHECK_AST(" +(x)= -y* not z",  +(x)== -y* not z);
    CHECK_AST(" +(x= -y)* not z",  +(x== -y)* not z);
    CHECK_AST(" +x=( -y)* not z",  +x==( -y)* not z);
    CHECK_AST(" +x= -(y)* not z",  +x== -(y)* not z);
    CHECK_AST("( +x)= not y*z", ( +x)== not y*z);
    CHECK_AST("( +x= not y)*z", ( +x== not y)*z);
    CHECK_AST(" +(x)= not y*z",  +(x)== not y*z);
    CHECK_AST(" +(x= not y)*z",  +(x== not y)*z);
    CHECK_AST(" +x=( not y)*z",  +x==( not y)*z);
    CHECK_AST(" +x= not (y)*z",  +x== not (y)*z);
    CHECK_AST("( +x)= not y* +z", ( +x)== not y* +z);
    CHECK_AST("( +x= not y)* +z", ( +x== not y)* +z);
    CHECK_AST(" +(x)= not y* +z",  +(x)== not y* +z);
    CHECK_AST(" +(x= not y)* +z",  +(x== not y)* +z);
    CHECK_AST(" +x=( not y)* +z",  +x==( not y)* +z);
    CHECK_AST(" +x= not (y)* +z",  +x== not (y)* +z);
    CHECK_AST("( +x)= not y* -z", ( +x)== not y* -z);
    CHECK_AST("( +x= not y)* -z", ( +x== not y)* -z);
    CHECK_AST(" +(x)= not y* -z",  +(x)== not y* -z);
    CHECK_AST(" +(x= not y)* -z",  +(x== not y)* -z);
    CHECK_AST(" +x=( not y)* -z",  +x==( not y)* -z);
    CHECK_AST(" +x= not (y)* -z",  +x== not (y)* -z);
    CHECK_AST("( +x)= not y* not z", ( +x)== not y* not z);
    CHECK_AST("( +x= not y)* not z", ( +x== not y)* not z);
    CHECK_AST(" +(x)= not y* not z",  +(x)== not y* not z);
    CHECK_AST(" +(x= not y)* not z",  +(x== not y)* not z);
    CHECK_AST(" +x=( not y)* not z",  +x==( not y)* not z);
    CHECK_AST(" +x= not (y)* not z",  +x== not (y)* not z);
    CHECK_AST("( -x)=y*z", ( -x)==y*z);
    CHECK_AST("( -x=y)*z", ( -x==y)*z);
    CHECK_AST(" -(x)=y*z",  -(x)==y*z);
    CHECK_AST(" -(x=y)*z",  -(x==y)*z);
    CHECK_AST(" -x=(y)*z",  -x==(y)*z);
    CHECK_AST("( -x)=y* +z", ( -x)==y* +z);
    CHECK_AST("( -x=y)* +z", ( -x==y)* +z);
    CHECK_AST(" -(x)=y* +z",  -(x)==y* +z);
    CHECK_AST(" -(x=y)* +z",  -(x==y)* +z);
    CHECK_AST(" -x=(y)* +z",  -x==(y)* +z);
    CHECK_AST("( -x)=y* -z", ( -x)==y* -z);
    CHECK_AST("( -x=y)* -z", ( -x==y)* -z);
    CHECK_AST(" -(x)=y* -z",  -(x)==y* -z);
    CHECK_AST(" -(x=y)* -z",  -(x==y)* -z);
    CHECK_AST(" -x=(y)* -z",  -x==(y)* -z);
    CHECK_AST("( -x)=y* not z", ( -x)==y* not z);
    CHECK_AST("( -x=y)* not z", ( -x==y)* not z);
    CHECK_AST(" -(x)=y* not z",  -(x)==y* not z);
    CHECK_AST(" -(x=y)* not z",  -(x==y)* not z);
    CHECK_AST(" -x=(y)* not z",  -x==(y)* not z);
    CHECK_AST("( -x)= +y*z", ( -x)== +y*z);
    CHECK_AST("( -x= +y)*z", ( -x== +y)*z);
    CHECK_AST(" -(x)= +y*z",  -(x)== +y*z);
    CHECK_AST(" -(x= +y)*z",  -(x== +y)*z);
    CHECK_AST(" -x=( +y)*z",  -x==( +y)*z);
    CHECK_AST(" -x= +(y)*z",  -x== +(y)*z);
    CHECK_AST("( -x)= +y* +z", ( -x)== +y* +z);
    CHECK_AST("( -x= +y)* +z", ( -x== +y)* +z);
    CHECK_AST(" -(x)= +y* +z",  -(x)== +y* +z);
    CHECK_AST(" -(x= +y)* +z",  -(x== +y)* +z);
    CHECK_AST(" -x=( +y)* +z",  -x==( +y)* +z);
    CHECK_AST(" -x= +(y)* +z",  -x== +(y)* +z);
    CHECK_AST("( -x)= +y* -z", ( -x)== +y* -z);
    CHECK_AST("( -x= +y)* -z", ( -x== +y)* -z);
    CHECK_AST(" -(x)= +y* -z",  -(x)== +y* -z);
    CHECK_AST(" -(x= +y)* -z",  -(x== +y)* -z);
    CHECK_AST(" -x=( +y)* -z",  -x==( +y)* -z);
    CHECK_AST(" -x= +(y)* -z",  -x== +(y)* -z);
    CHECK_AST("( -x)= +y* not z", ( -x)== +y* not z);
    CHECK_AST("( -x= +y)* not z", ( -x== +y)* not z);
    CHECK_AST(" -(x)= +y* not z",  -(x)== +y* not z);
    CHECK_AST(" -(x= +y)* not z",  -(x== +y)* not z);
    CHECK_AST(" -x=( +y)* not z",  -x==( +y)* not z);
    CHECK_AST(" -x= +(y)* not z",  -x== +(y)* not z);
    CHECK_AST("( -x)= -y*z", ( -x)== -y*z);
    CHECK_AST("( -x= -y)*z", ( -x== -y)*z);
    CHECK_AST(" -(x)= -y*z",  -(x)== -y*z);
    CHECK_AST(" -(x= -y)*z",  -(x== -y)*z);
    CHECK_AST(" -x=( -y)*z",  -x==( -y)*z);
    CHECK_AST(" -x= -(y)*z",  -x== -(y)*z);
    CHECK_AST("( -x)= -y* +z", ( -x)== -y* +z);
    CHECK_AST("( -x= -y)* +z", ( -x== -y)* +z);
    CHECK_AST(" -(x)= -y* +z",  -(x)== -y* +z);
    CHECK_AST(" -(x= -y)* +z",  -(x== -y)* +z);
    CHECK_AST(" -x=( -y)* +z",  -x==( -y)* +z);
    CHECK_AST(" -x= -(y)* +z",  -x== -(y)* +z);
    CHECK_AST("( -x)= -y* -z", ( -x)== -y* -z);
    CHECK_AST("( -x= -y)* -z", ( -x== -y)* -z);
    CHECK_AST(" -(x)= -y* -z",  -(x)== -y* -z);
    CHECK_AST(" -(x= -y)* -z",  -(x== -y)* -z);
    CHECK_AST(" -x=( -y)* -z",  -x==( -y)* -z);
    CHECK_AST(" -x= -(y)* -z",  -x== -(y)* -z);
    CHECK_AST("( -x)= -y* not z", ( -x)== -y* not z);
    CHECK_AST("( -x= -y)* not z", ( -x== -y)* not z);
    CHECK_AST(" -(x)= -y* not z",  -(x)== -y* not z);
    CHECK_AST(" -(x= -y)* not z",  -(x== -y)* not z);
    CHECK_AST(" -x=( -y)* not z",  -x==( -y)* not z);
    CHECK_AST(" -x= -(y)* not z",  -x== -(y)* not z);
    CHECK_AST("( -x)= not y*z", ( -x)== not y*z);
    CHECK_AST("( -x= not y)*z", ( -x== not y)*z);
    CHECK_AST(" -(x)= not y*z",  -(x)== not y*z);
    CHECK_AST(" -(x= not y)*z",  -(x== not y)*z);
    CHECK_AST(" -x=( not y)*z",  -x==( not y)*z);
    CHECK_AST(" -x= not (y)*z",  -x== not (y)*z);
    CHECK_AST("( -x)= not y* +z", ( -x)== not y* +z);
    CHECK_AST("( -x= not y)* +z", ( -x== not y)* +z);
    CHECK_AST(" -(x)= not y* +z",  -(x)== not y* +z);
    CHECK_AST(" -(x= not y)* +z",  -(x== not y)* +z);
    CHECK_AST(" -x=( not y)* +z",  -x==( not y)* +z);
    CHECK_AST(" -x= not (y)* +z",  -x== not (y)* +z);
    CHECK_AST("( -x)= not y* -z", ( -x)== not y* -z);
    CHECK_AST("( -x= not y)* -z", ( -x== not y)* -z);
    CHECK_AST(" -(x)= not y* -z",  -(x)== not y* -z);
    CHECK_AST(" -(x= not y)* -z",  -(x== not y)* -z);
    CHECK_AST(" -x=( not y)* -z",  -x==( not y)* -z);
    CHECK_AST(" -x= not (y)* -z",  -x== not (y)* -z);
    CHECK_AST("( -x)= not y* not z", ( -x)== not y* not z);
    CHECK_AST("( -x= not y)* not z", ( -x== not y)* not z);
    CHECK_AST(" -(x)= not y* not z",  -(x)== not y* not z);
    CHECK_AST(" -(x= not y)* not z",  -(x== not y)* not z);
    CHECK_AST(" -x=( not y)* not z",  -x==( not y)* not z);
    CHECK_AST(" -x= not (y)* not z",  -x== not (y)* not z);
    CHECK_AST("( not x)=y*z", ( not x)==y*z);
    CHECK_AST("( not x=y)*z", ( not x==y)*z);
    CHECK_AST(" not (x)=y*z",  not (x)==y*z);
    CHECK_AST(" not (x=y)*z",  not (x==y)*z);
    CHECK_AST(" not x=(y)*z",  not x==(y)*z);
    CHECK_AST("( not x)=y* +z", ( not x)==y* +z);
    CHECK_AST("( not x=y)* +z", ( not x==y)* +z);
    CHECK_AST(" not (x)=y* +z",  not (x)==y* +z);
    CHECK_AST(" not (x=y)* +z",  not (x==y)* +z);
    CHECK_AST(" not x=(y)* +z",  not x==(y)* +z);
    CHECK_AST("( not x)=y* -z", ( not x)==y* -z);
    CHECK_AST("( not x=y)* -z", ( not x==y)* -z);
    CHECK_AST(" not (x)=y* -z",  not (x)==y* -z);
    CHECK_AST(" not (x=y)* -z",  not (x==y)* -z);
    CHECK_AST(" not x=(y)* -z",  not x==(y)* -z);
    CHECK_AST("( not x)=y* not z", ( not x)==y* not z);
    CHECK_AST("( not x=y)* not z", ( not x==y)* not z);
    CHECK_AST(" not (x)=y* not z",  not (x)==y* not z);
    CHECK_AST(" not (x=y)* not z",  not (x==y)* not z);
    CHECK_AST(" not x=(y)* not z",  not x==(y)* not z);
    CHECK_AST("( not x)= +y*z", ( not x)== +y*z);
    CHECK_AST("( not x= +y)*z", ( not x== +y)*z);
    CHECK_AST(" not (x)= +y*z",  not (x)== +y*z);
    CHECK_AST(" not (x= +y)*z",  not (x== +y)*z);
    CHECK_AST(" not x=( +y)*z",  not x==( +y)*z);
    CHECK_AST(" not x= +(y)*z",  not x== +(y)*z);
    CHECK_AST("( not x)= +y* +z", ( not x)== +y* +z);
    CHECK_AST("( not x= +y)* +z", ( not x== +y)* +z);
    CHECK_AST(" not (x)= +y* +z",  not (x)== +y* +z);
    CHECK_AST(" not (x= +y)* +z",  not (x== +y)* +z);
    CHECK_AST(" not x=( +y)* +z",  not x==( +y)* +z);
    CHECK_AST(" not x= +(y)* +z",  not x== +(y)* +z);
    CHECK_AST("( not x)= +y* -z", ( not x)== +y* -z);
    CHECK_AST("( not x= +y)* -z", ( not x== +y)* -z);
    CHECK_AST(" not (x)= +y* -z",  not (x)== +y* -z);
    CHECK_AST(" not (x= +y)* -z",  not (x== +y)* -z);
    CHECK_AST(" not x=( +y)* -z",  not x==( +y)* -z);
    CHECK_AST(" not x= +(y)* -z",  not x== +(y)* -z);
    CHECK_AST("( not x)= +y* not z", ( not x)== +y* not z);
    CHECK_AST("( not x= +y)* not z", ( not x== +y)* not z);
    CHECK_AST(" not (x)= +y* not z",  not (x)== +y* not z);
    CHECK_AST(" not (x= +y)* not z",  not (x== +y)* not z);
    CHECK_AST(" not x=( +y)* not z",  not x==( +y)* not z);
    CHECK_AST(" not x= +(y)* not z",  not x== +(y)* not z);
    CHECK_AST("( not x)= -y*z", ( not x)== -y*z);
    CHECK_AST("( not x= -y)*z", ( not x== -y)*z);
    CHECK_AST(" not (x)= -y*z",  not (x)== -y*z);
    CHECK_AST(" not (x= -y)*z",  not (x== -y)*z);
    CHECK_AST(" not x=( -y)*z",  not x==( -y)*z);
    CHECK_AST(" not x= -(y)*z",  not x== -(y)*z);
    CHECK_AST("( not x)= -y* +z", ( not x)== -y* +z);
    CHECK_AST("( not x= -y)* +z", ( not x== -y)* +z);
    CHECK_AST(" not (x)= -y* +z",  not (x)== -y* +z);
    CHECK_AST(" not (x= -y)* +z",  not (x== -y)* +z);
    CHECK_AST(" not x=( -y)* +z",  not x==( -y)* +z);
    CHECK_AST(" not x= -(y)* +z",  not x== -(y)* +z);
    CHECK_AST("( not x)= -y* -z", ( not x)== -y* -z);
    CHECK_AST("( not x= -y)* -z", ( not x== -y)* -z);
    CHECK_AST(" not (x)= -y* -z",  not (x)== -y* -z);
    CHECK_AST(" not (x= -y)* -z",  not (x== -y)* -z);
    CHECK_AST(" not x=( -y)* -z",  not x==( -y)* -z);
    CHECK_AST(" not x= -(y)* -z",  not x== -(y)* -z);
    CHECK_AST("( not x)= -y* not z", ( not x)== -y* not z);
    CHECK_AST("( not x= -y)* not z", ( not x== -y)* not z);
    CHECK_AST(" not (x)= -y* not z",  not (x)== -y* not z);
    CHECK_AST(" not (x= -y)* not z",  not (x== -y)* not z);
    CHECK_AST(" not x=( -y)* not z",  not x==( -y)* not z);
    CHECK_AST(" not x= -(y)* not z",  not x== -(y)* not z);
    CHECK_AST("( not x)= not y*z", ( not x)== not y*z);
    CHECK_AST("( not x= not y)*z", ( not x== not y)*z);
    CHECK_AST(" not (x)= not y*z",  not (x)== not y*z);
    CHECK_AST(" not (x= not y)*z",  not (x== not y)*z);
    CHECK_AST(" not x=( not y)*z",  not x==( not y)*z);
    CHECK_AST(" not x= not (y)*z",  not x== not (y)*z);
    CHECK_AST("( not x)= not y* +z", ( not x)== not y* +z);
    CHECK_AST("( not x= not y)* +z", ( not x== not y)* +z);
    CHECK_AST(" not (x)= not y* +z",  not (x)== not y* +z);
    CHECK_AST(" not (x= not y)* +z",  not (x== not y)* +z);
    CHECK_AST(" not x=( not y)* +z",  not x==( not y)* +z);
    CHECK_AST(" not x= not (y)* +z",  not x== not (y)* +z);
    CHECK_AST("( not x)= not y* -z", ( not x)== not y* -z);
    CHECK_AST("( not x= not y)* -z", ( not x== not y)* -z);
    CHECK_AST(" not (x)= not y* -z",  not (x)== not y* -z);
    CHECK_AST(" not (x= not y)* -z",  not (x== not y)* -z);
    CHECK_AST(" not x=( not y)* -z",  not x==( not y)* -z);
    CHECK_AST(" not x= not (y)* -z",  not x== not (y)* -z);
    CHECK_AST("( not x)= not y* not z", ( not x)== not y* not z);
    CHECK_AST("( not x= not y)* not z", ( not x== not y)* not z);
    CHECK_AST(" not (x)= not y* not z",  not (x)== not y* not z);
    CHECK_AST(" not (x= not y)* not z",  not (x== not y)* not z);
    CHECK_AST(" not x=( not y)* not z",  not x==( not y)* not z);
    CHECK_AST(" not x= not (y)* not z",  not x== not (y)* not z);
    CHECK_AST("(x)=y/z", (x)==y/z);
    CHECK_AST("(x=y)/z", (x==y)/z);
    CHECK_AST("x=(y)/z", x==(y)/z);
    CHECK_AST("(x)=y/ +z", (x)==y/ +z);
    CHECK_AST("(x=y)/ +z", (x==y)/ +z);
    CHECK_AST("x=(y)/ +z", x==(y)/ +z);
    CHECK_AST("(x)=y/ -z", (x)==y/ -z);
    CHECK_AST("(x=y)/ -z", (x==y)/ -z);
    CHECK_AST("x=(y)/ -z", x==(y)/ -z);
    CHECK_AST("(x)=y/ not z", (x)==y/ not z);
    CHECK_AST("(x=y)/ not z", (x==y)/ not z);
    CHECK_AST("x=(y)/ not z", x==(y)/ not z);
    CHECK_AST("(x)= +y/z", (x)== +y/z);
    CHECK_AST("(x= +y)/z", (x== +y)/z);
    CHECK_AST("x=( +y)/z", x==( +y)/z);
    CHECK_AST("x= +(y)/z", x== +(y)/z);
    CHECK_AST("(x)= +y/ +z", (x)== +y/ +z);
    CHECK_AST("(x= +y)/ +z", (x== +y)/ +z);
    CHECK_AST("x=( +y)/ +z", x==( +y)/ +z);
    CHECK_AST("x= +(y)/ +z", x== +(y)/ +z);
    CHECK_AST("(x)= +y/ -z", (x)== +y/ -z);
    CHECK_AST("(x= +y)/ -z", (x== +y)/ -z);
    CHECK_AST("x=( +y)/ -z", x==( +y)/ -z);
    CHECK_AST("x= +(y)/ -z", x== +(y)/ -z);
    CHECK_AST("(x)= +y/ not z", (x)== +y/ not z);
    CHECK_AST("(x= +y)/ not z", (x== +y)/ not z);
    CHECK_AST("x=( +y)/ not z", x==( +y)/ not z);
    CHECK_AST("x= +(y)/ not z", x== +(y)/ not z);
    CHECK_AST("(x)= -y/z", (x)== -y/z);
    CHECK_AST("(x= -y)/z", (x== -y)/z);
    CHECK_AST("x=( -y)/z", x==( -y)/z);
    CHECK_AST("x= -(y)/z", x== -(y)/z);
    CHECK_AST("(x)= -y/ +z", (x)== -y/ +z);
    CHECK_AST("(x= -y)/ +z", (x== -y)/ +z);
    CHECK_AST("x=( -y)/ +z", x==( -y)/ +z);
    CHECK_AST("x= -(y)/ +z", x== -(y)/ +z);
    CHECK_AST("(x)= -y/ -z", (x)== -y/ -z);
    CHECK_AST("(x= -y)/ -z", (x== -y)/ -z);
    CHECK_AST("x=( -y)/ -z", x==( -y)/ -z);
    CHECK_AST("x= -(y)/ -z", x== -(y)/ -z);
    CHECK_AST("(x)= -y/ not z", (x)== -y/ not z);
    CHECK_AST("(x= -y)/ not z", (x== -y)/ not z);
    CHECK_AST("x=( -y)/ not z", x==( -y)/ not z);
    CHECK_AST("x= -(y)/ not z", x== -(y)/ not z);
    CHECK_AST("(x)= not y/z", (x)== not y/z);
    CHECK_AST("(x= not y)/z", (x== not y)/z);
    CHECK_AST("x=( not y)/z", x==( not y)/z);
    CHECK_AST("x= not (y)/z", x== not (y)/z);
    CHECK_AST("(x)= not y/ +z", (x)== not y/ +z);
    CHECK_AST("(x= not y)/ +z", (x== not y)/ +z);
    CHECK_AST("x=( not y)/ +z", x==( not y)/ +z);
    CHECK_AST("x= not (y)/ +z", x== not (y)/ +z);
    CHECK_AST("(x)= not y/ -z", (x)== not y/ -z);
    CHECK_AST("(x= not y)/ -z", (x== not y)/ -z);
    CHECK_AST("x=( not y)/ -z", x==( not y)/ -z);
    CHECK_AST("x= not (y)/ -z", x== not (y)/ -z);
    CHECK_AST("(x)= not y/ not z", (x)== not y/ not z);
    CHECK_AST("(x= not y)/ not z", (x== not y)/ not z);
    CHECK_AST("x=( not y)/ not z", x==( not y)/ not z);
    CHECK_AST("x= not (y)/ not z", x== not (y)/ not z);
    CHECK_AST("( +x)=y/z", ( +x)==y/z);
    CHECK_AST("( +x=y)/z", ( +x==y)/z);
    CHECK_AST(" +(x)=y/z",  +(x)==y/z);
    CHECK_AST(" +(x=y)/z",  +(x==y)/z);
    CHECK_AST(" +x=(y)/z",  +x==(y)/z);
    CHECK_AST("( +x)=y/ +z", ( +x)==y/ +z);
    CHECK_AST("( +x=y)/ +z", ( +x==y)/ +z);
    CHECK_AST(" +(x)=y/ +z",  +(x)==y/ +z);
    CHECK_AST(" +(x=y)/ +z",  +(x==y)/ +z);
    CHECK_AST(" +x=(y)/ +z",  +x==(y)/ +z);
    CHECK_AST("( +x)=y/ -z", ( +x)==y/ -z);
    CHECK_AST("( +x=y)/ -z", ( +x==y)/ -z);
    CHECK_AST(" +(x)=y/ -z",  +(x)==y/ -z);
    CHECK_AST(" +(x=y)/ -z",  +(x==y)/ -z);
    CHECK_AST(" +x=(y)/ -z",  +x==(y)/ -z);
    CHECK_AST("( +x)=y/ not z", ( +x)==y/ not z);
    CHECK_AST("( +x=y)/ not z", ( +x==y)/ not z);
    CHECK_AST(" +(x)=y/ not z",  +(x)==y/ not z);
    CHECK_AST(" +(x=y)/ not z",  +(x==y)/ not z);
    CHECK_AST(" +x=(y)/ not z",  +x==(y)/ not z);
    CHECK_AST("( +x)= +y/z", ( +x)== +y/z);
    CHECK_AST("( +x= +y)/z", ( +x== +y)/z);
    CHECK_AST(" +(x)= +y/z",  +(x)== +y/z);
    CHECK_AST(" +(x= +y)/z",  +(x== +y)/z);
    CHECK_AST(" +x=( +y)/z",  +x==( +y)/z);
    CHECK_AST(" +x= +(y)/z",  +x== +(y)/z);
    CHECK_AST("( +x)= +y/ +z", ( +x)== +y/ +z);
    CHECK_AST("( +x= +y)/ +z", ( +x== +y)/ +z);
    CHECK_AST(" +(x)= +y/ +z",  +(x)== +y/ +z);
    CHECK_AST(" +(x= +y)/ +z",  +(x== +y)/ +z);
    CHECK_AST(" +x=( +y)/ +z",  +x==( +y)/ +z);
    CHECK_AST(" +x= +(y)/ +z",  +x== +(y)/ +z);
    CHECK_AST("( +x)= +y/ -z", ( +x)== +y/ -z);
    CHECK_AST("( +x= +y)/ -z", ( +x== +y)/ -z);
    CHECK_AST(" +(x)= +y/ -z",  +(x)== +y/ -z);
    CHECK_AST(" +(x= +y)/ -z",  +(x== +y)/ -z);
    CHECK_AST(" +x=( +y)/ -z",  +x==( +y)/ -z);
    CHECK_AST(" +x= +(y)/ -z",  +x== +(y)/ -z);
    CHECK_AST("( +x)= +y/ not z", ( +x)== +y/ not z);
    CHECK_AST("( +x= +y)/ not z", ( +x== +y)/ not z);
    CHECK_AST(" +(x)= +y/ not z",  +(x)== +y/ not z);
    CHECK_AST(" +(x= +y)/ not z",  +(x== +y)/ not z);
    CHECK_AST(" +x=( +y)/ not z",  +x==( +y)/ not z);
    CHECK_AST(" +x= +(y)/ not z",  +x== +(y)/ not z);
    CHECK_AST("( +x)= -y/z", ( +x)== -y/z);
    CHECK_AST("( +x= -y)/z", ( +x== -y)/z);
    CHECK_AST(" +(x)= -y/z",  +(x)== -y/z);
    CHECK_AST(" +(x= -y)/z",  +(x== -y)/z);
    CHECK_AST(" +x=( -y)/z",  +x==( -y)/z);
    CHECK_AST(" +x= -(y)/z",  +x== -(y)/z);
    CHECK_AST("( +x)= -y/ +z", ( +x)== -y/ +z);
    CHECK_AST("( +x= -y)/ +z", ( +x== -y)/ +z);
    CHECK_AST(" +(x)= -y/ +z",  +(x)== -y/ +z);
    CHECK_AST(" +(x= -y)/ +z",  +(x== -y)/ +z);
    CHECK_AST(" +x=( -y)/ +z",  +x==( -y)/ +z);
    CHECK_AST(" +x= -(y)/ +z",  +x== -(y)/ +z);
    CHECK_AST("( +x)= -y/ -z", ( +x)== -y/ -z);
    CHECK_AST("( +x= -y)/ -z", ( +x== -y)/ -z);
    CHECK_AST(" +(x)= -y/ -z",  +(x)== -y/ -z);
    CHECK_AST(" +(x= -y)/ -z",  +(x== -y)/ -z);
    CHECK_AST(" +x=( -y)/ -z",  +x==( -y)/ -z);
    CHECK_AST(" +x= -(y)/ -z",  +x== -(y)/ -z);
    CHECK_AST("( +x)= -y/ not z", ( +x)== -y/ not z);
    CHECK_AST("( +x= -y)/ not z", ( +x== -y)/ not z);
    CHECK_AST(" +(x)= -y/ not z",  +(x)== -y/ not z);
    CHECK_AST(" +(x= -y)/ not z",  +(x== -y)/ not z);
    CHECK_AST(" +x=( -y)/ not z",  +x==( -y)/ not z);
    CHECK_AST(" +x= -(y)/ not z",  +x== -(y)/ not z);
    CHECK_AST("( +x)= not y/z", ( +x)== not y/z);
    CHECK_AST("( +x= not y)/z", ( +x== not y)/z);
    CHECK_AST(" +(x)= not y/z",  +(x)== not y/z);
    CHECK_AST(" +(x= not y)/z",  +(x== not y)/z);
    CHECK_AST(" +x=( not y)/z",  +x==( not y)/z);
    CHECK_AST(" +x= not (y)/z",  +x== not (y)/z);
    CHECK_AST("( +x)= not y/ +z", ( +x)== not y/ +z);
    CHECK_AST("( +x= not y)/ +z", ( +x== not y)/ +z);
    CHECK_AST(" +(x)= not y/ +z",  +(x)== not y/ +z);
    CHECK_AST(" +(x= not y)/ +z",  +(x== not y)/ +z);
    CHECK_AST(" +x=( not y)/ +z",  +x==( not y)/ +z);
    CHECK_AST(" +x= not (y)/ +z",  +x== not (y)/ +z);
    CHECK_AST("( +x)= not y/ -z", ( +x)== not y/ -z);
    CHECK_AST("( +x= not y)/ -z", ( +x== not y)/ -z);
    CHECK_AST(" +(x)= not y/ -z",  +(x)== not y/ -z);
    CHECK_AST(" +(x= not y)/ -z",  +(x== not y)/ -z);
    CHECK_AST(" +x=( not y)/ -z",  +x==( not y)/ -z);
    CHECK_AST(" +x= not (y)/ -z",  +x== not (y)/ -z);
    CHECK_AST("( +x)= not y/ not z", ( +x)== not y/ not z);
    CHECK_AST("( +x= not y)/ not z", ( +x== not y)/ not z);
    CHECK_AST(" +(x)= not y/ not z",  +(x)== not y/ not z);
    CHECK_AST(" +(x= not y)/ not z",  +(x== not y)/ not z);
    CHECK_AST(" +x=( not y)/ not z",  +x==( not y)/ not z);
    CHECK_AST(" +x= not (y)/ not z",  +x== not (y)/ not z);
    CHECK_AST("( -x)=y/z", ( -x)==y/z);
    CHECK_AST("( -x=y)/z", ( -x==y)/z);
    CHECK_AST(" -(x)=y/z",  -(x)==y/z);
    CHECK_AST(" -(x=y)/z",  -(x==y)/z);
    CHECK_AST(" -x=(y)/z",  -x==(y)/z);
    CHECK_AST("( -x)=y/ +z", ( -x)==y/ +z);
    CHECK_AST("( -x=y)/ +z", ( -x==y)/ +z);
    CHECK_AST(" -(x)=y/ +z",  -(x)==y/ +z);
    CHECK_AST(" -(x=y)/ +z",  -(x==y)/ +z);
    CHECK_AST(" -x=(y)/ +z",  -x==(y)/ +z);
    CHECK_AST("( -x)=y/ -z", ( -x)==y/ -z);
    CHECK_AST("( -x=y)/ -z", ( -x==y)/ -z);
    CHECK_AST(" -(x)=y/ -z",  -(x)==y/ -z);
    CHECK_AST(" -(x=y)/ -z",  -(x==y)/ -z);
    CHECK_AST(" -x=(y)/ -z",  -x==(y)/ -z);
    CHECK_AST("( -x)=y/ not z", ( -x)==y/ not z);
    CHECK_AST("( -x=y)/ not z", ( -x==y)/ not z);
    CHECK_AST(" -(x)=y/ not z",  -(x)==y/ not z);
    CHECK_AST(" -(x=y)/ not z",  -(x==y)/ not z);
    CHECK_AST(" -x=(y)/ not z",  -x==(y)/ not z);
    CHECK_AST("( -x)= +y/z", ( -x)== +y/z);
    CHECK_AST("( -x= +y)/z", ( -x== +y)/z);
    CHECK_AST(" -(x)= +y/z",  -(x)== +y/z);
    CHECK_AST(" -(x= +y)/z",  -(x== +y)/z);
    CHECK_AST(" -x=( +y)/z",  -x==( +y)/z);
    CHECK_AST(" -x= +(y)/z",  -x== +(y)/z);
    CHECK_AST("( -x)= +y/ +z", ( -x)== +y/ +z);
    CHECK_AST("( -x= +y)/ +z", ( -x== +y)/ +z);
    CHECK_AST(" -(x)= +y/ +z",  -(x)== +y/ +z);
    CHECK_AST(" -(x= +y)/ +z",  -(x== +y)/ +z);
    CHECK_AST(" -x=( +y)/ +z",  -x==( +y)/ +z);
    CHECK_AST(" -x= +(y)/ +z",  -x== +(y)/ +z);
    CHECK_AST("( -x)= +y/ -z", ( -x)== +y/ -z);
    CHECK_AST("( -x= +y)/ -z", ( -x== +y)/ -z);
    CHECK_AST(" -(x)= +y/ -z",  -(x)== +y/ -z);
    CHECK_AST(" -(x= +y)/ -z",  -(x== +y)/ -z);
    CHECK_AST(" -x=( +y)/ -z",  -x==( +y)/ -z);
    CHECK_AST(" -x= +(y)/ -z",  -x== +(y)/ -z);
    CHECK_AST("( -x)= +y/ not z", ( -x)== +y/ not z);
    CHECK_AST("( -x= +y)/ not z", ( -x== +y)/ not z);
    CHECK_AST(" -(x)= +y/ not z",  -(x)== +y/ not z);
    CHECK_AST(" -(x= +y)/ not z",  -(x== +y)/ not z);
    CHECK_AST(" -x=( +y)/ not z",  -x==( +y)/ not z);
    CHECK_AST(" -x= +(y)/ not z",  -x== +(y)/ not z);
    CHECK_AST("( -x)= -y/z", ( -x)== -y/z);
    CHECK_AST("( -x= -y)/z", ( -x== -y)/z);
    CHECK_AST(" -(x)= -y/z",  -(x)== -y/z);
    CHECK_AST(" -(x= -y)/z",  -(x== -y)/z);
    CHECK_AST(" -x=( -y)/z",  -x==( -y)/z);
    CHECK_AST(" -x= -(y)/z",  -x== -(y)/z);
    CHECK_AST("( -x)= -y/ +z", ( -x)== -y/ +z);
    CHECK_AST("( -x= -y)/ +z", ( -x== -y)/ +z);
    CHECK_AST(" -(x)= -y/ +z",  -(x)== -y/ +z);
    CHECK_AST(" -(x= -y)/ +z",  -(x== -y)/ +z);
    CHECK_AST(" -x=( -y)/ +z",  -x==( -y)/ +z);
    CHECK_AST(" -x= -(y)/ +z",  -x== -(y)/ +z);
    CHECK_AST("( -x)= -y/ -z", ( -x)== -y/ -z);
    CHECK_AST("( -x= -y)/ -z", ( -x== -y)/ -z);
    CHECK_AST(" -(x)= -y/ -z",  -(x)== -y/ -z);
    CHECK_AST(" -(x= -y)/ -z",  -(x== -y)/ -z);
    CHECK_AST(" -x=( -y)/ -z",  -x==( -y)/ -z);
    CHECK_AST(" -x= -(y)/ -z",  -x== -(y)/ -z);
    CHECK_AST("( -x)= -y/ not z", ( -x)== -y/ not z);
    CHECK_AST("( -x= -y)/ not z", ( -x== -y)/ not z);
    CHECK_AST(" -(x)= -y/ not z",  -(x)== -y/ not z);
    CHECK_AST(" -(x= -y)/ not z",  -(x== -y)/ not z);
    CHECK_AST(" -x=( -y)/ not z",  -x==( -y)/ not z);
    CHECK_AST(" -x= -(y)/ not z",  -x== -(y)/ not z);
    CHECK_AST("( -x)= not y/z", ( -x)== not y/z);
    CHECK_AST("( -x= not y)/z", ( -x== not y)/z);
    CHECK_AST(" -(x)= not y/z",  -(x)== not y/z);
    CHECK_AST(" -(x= not y)/z",  -(x== not y)/z);
    CHECK_AST(" -x=( not y)/z",  -x==( not y)/z);
    CHECK_AST(" -x= not (y)/z",  -x== not (y)/z);
    CHECK_AST("( -x)= not y/ +z", ( -x)== not y/ +z);
    CHECK_AST("( -x= not y)/ +z", ( -x== not y)/ +z);
    CHECK_AST(" -(x)= not y/ +z",  -(x)== not y/ +z);
    CHECK_AST(" -(x= not y)/ +z",  -(x== not y)/ +z);
    CHECK_AST(" -x=( not y)/ +z",  -x==( not y)/ +z);
    CHECK_AST(" -x= not (y)/ +z",  -x== not (y)/ +z);
    CHECK_AST("( -x)= not y/ -z", ( -x)== not y/ -z);
    CHECK_AST("( -x= not y)/ -z", ( -x== not y)/ -z);
    CHECK_AST(" -(x)= not y/ -z",  -(x)== not y/ -z);
    CHECK_AST(" -(x= not y)/ -z",  -(x== not y)/ -z);
    CHECK_AST(" -x=( not y)/ -z",  -x==( not y)/ -z);
    CHECK_AST(" -x= not (y)/ -z",  -x== not (y)/ -z);
    CHECK_AST("( -x)= not y/ not z", ( -x)== not y/ not z);
    CHECK_AST("( -x= not y)/ not z", ( -x== not y)/ not z);
    CHECK_AST(" -(x)= not y/ not z",  -(x)== not y/ not z);
    CHECK_AST(" -(x= not y)/ not z",  -(x== not y)/ not z);
    CHECK_AST(" -x=( not y)/ not z",  -x==( not y)/ not z);
    CHECK_AST(" -x= not (y)/ not z",  -x== not (y)/ not z);
    CHECK_AST("( not x)=y/z", ( not x)==y/z);
    CHECK_AST("( not x=y)/z", ( not x==y)/z);
    CHECK_AST(" not (x)=y/z",  not (x)==y/z);
    CHECK_AST(" not (x=y)/z",  not (x==y)/z);
    CHECK_AST(" not x=(y)/z",  not x==(y)/z);
    CHECK_AST("( not x)=y/ +z", ( not x)==y/ +z);
    CHECK_AST("( not x=y)/ +z", ( not x==y)/ +z);
    CHECK_AST(" not (x)=y/ +z",  not (x)==y/ +z);
    CHECK_AST(" not (x=y)/ +z",  not (x==y)/ +z);
    CHECK_AST(" not x=(y)/ +z",  not x==(y)/ +z);
    CHECK_AST("( not x)=y/ -z", ( not x)==y/ -z);
    CHECK_AST("( not x=y)/ -z", ( not x==y)/ -z);
    CHECK_AST(" not (x)=y/ -z",  not (x)==y/ -z);
    CHECK_AST(" not (x=y)/ -z",  not (x==y)/ -z);
    CHECK_AST(" not x=(y)/ -z",  not x==(y)/ -z);
    CHECK_AST("( not x)=y/ not z", ( not x)==y/ not z);
    CHECK_AST("( not x=y)/ not z", ( not x==y)/ not z);
    CHECK_AST(" not (x)=y/ not z",  not (x)==y/ not z);
    CHECK_AST(" not (x=y)/ not z",  not (x==y)/ not z);
    CHECK_AST(" not x=(y)/ not z",  not x==(y)/ not z);
    CHECK_AST("( not x)= +y/z", ( not x)== +y/z);
    CHECK_AST("( not x= +y)/z", ( not x== +y)/z);
    CHECK_AST(" not (x)= +y/z",  not (x)== +y/z);
    CHECK_AST(" not (x= +y)/z",  not (x== +y)/z);
    CHECK_AST(" not x=( +y)/z",  not x==( +y)/z);
    CHECK_AST(" not x= +(y)/z",  not x== +(y)/z);
    CHECK_AST("( not x)= +y/ +z", ( not x)== +y/ +z);
    CHECK_AST("( not x= +y)/ +z", ( not x== +y)/ +z);
    CHECK_AST(" not (x)= +y/ +z",  not (x)== +y/ +z);
    CHECK_AST(" not (x= +y)/ +z",  not (x== +y)/ +z);
    CHECK_AST(" not x=( +y)/ +z",  not x==( +y)/ +z);
    CHECK_AST(" not x= +(y)/ +z",  not x== +(y)/ +z);
    CHECK_AST("( not x)= +y/ -z", ( not x)== +y/ -z);
    CHECK_AST("( not x= +y)/ -z", ( not x== +y)/ -z);
    CHECK_AST(" not (x)= +y/ -z",  not (x)== +y/ -z);
    CHECK_AST(" not (x= +y)/ -z",  not (x== +y)/ -z);
    CHECK_AST(" not x=( +y)/ -z",  not x==( +y)/ -z);
    CHECK_AST(" not x= +(y)/ -z",  not x== +(y)/ -z);
    CHECK_AST("( not x)= +y/ not z", ( not x)== +y/ not z);
    CHECK_AST("( not x= +y)/ not z", ( not x== +y)/ not z);
    CHECK_AST(" not (x)= +y/ not z",  not (x)== +y/ not z);
    CHECK_AST(" not (x= +y)/ not z",  not (x== +y)/ not z);
    CHECK_AST(" not x=( +y)/ not z",  not x==( +y)/ not z);
    CHECK_AST(" not x= +(y)/ not z",  not x== +(y)/ not z);
    CHECK_AST("( not x)= -y/z", ( not x)== -y/z);
    CHECK_AST("( not x= -y)/z", ( not x== -y)/z);
    CHECK_AST(" not (x)= -y/z",  not (x)== -y/z);
    CHECK_AST(" not (x= -y)/z",  not (x== -y)/z);
    CHECK_AST(" not x=( -y)/z",  not x==( -y)/z);
    CHECK_AST(" not x= -(y)/z",  not x== -(y)/z);
    CHECK_AST("( not x)= -y/ +z", ( not x)== -y/ +z);
    CHECK_AST("( not x= -y)/ +z", ( not x== -y)/ +z);
    CHECK_AST(" not (x)= -y/ +z",  not (x)== -y/ +z);
    CHECK_AST(" not (x= -y)/ +z",  not (x== -y)/ +z);
    CHECK_AST(" not x=( -y)/ +z",  not x==( -y)/ +z);
    CHECK_AST(" not x= -(y)/ +z",  not x== -(y)/ +z);
    CHECK_AST("( not x)= -y/ -z", ( not x)== -y/ -z);
    CHECK_AST("( not x= -y)/ -z", ( not x== -y)/ -z);
    CHECK_AST(" not (x)= -y/ -z",  not (x)== -y/ -z);
    CHECK_AST(" not (x= -y)/ -z",  not (x== -y)/ -z);

    auto total = good + bad;
    std::cout
        << "check_ast_bt: " << good << " out of " << total
        << " (" << std::setprecision(1) << std::fixed << (100.0*good/total) << "%)\n";
}