check_ast_cu.cpp

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

void check_ast_cu(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(" +x or ( +y)- -z",  +x|( +y)- -z);
    CHECK_AST(" +x or  +(y)- -z",  +x| +(y)- -z);
    CHECK_AST("( +x) or  +y- not z", ( +x)| +y- not z);
    CHECK_AST("( +x or  +y)- not z", ( +x| +y)- not z);
    CHECK_AST(" +(x) or  +y- not z",  +(x)| +y- not z);
    CHECK_AST(" +(x or  +y)- not z",  +(x| +y)- not z);
    CHECK_AST(" +x or ( +y)- not z",  +x|( +y)- not z);
    CHECK_AST(" +x or  +(y)- not z",  +x| +(y)- not z);
    CHECK_AST("( +x) or  -y-z", ( +x)| -y-z);
    CHECK_AST("( +x or  -y)-z", ( +x| -y)-z);
    CHECK_AST(" +(x) or  -y-z",  +(x)| -y-z);
    CHECK_AST(" +(x or  -y)-z",  +(x| -y)-z);
    CHECK_AST(" +x or ( -y)-z",  +x|( -y)-z);
    CHECK_AST(" +x or  -(y)-z",  +x| -(y)-z);
    CHECK_AST("( +x) or  -y- +z", ( +x)| -y- +z);
    CHECK_AST("( +x or  -y)- +z", ( +x| -y)- +z);
    CHECK_AST(" +(x) or  -y- +z",  +(x)| -y- +z);
    CHECK_AST(" +(x or  -y)- +z",  +(x| -y)- +z);
    CHECK_AST(" +x or ( -y)- +z",  +x|( -y)- +z);
    CHECK_AST(" +x or  -(y)- +z",  +x| -(y)- +z);
    CHECK_AST("( +x) or  -y- -z", ( +x)| -y- -z);
    CHECK_AST("( +x or  -y)- -z", ( +x| -y)- -z);
    CHECK_AST(" +(x) or  -y- -z",  +(x)| -y- -z);
    CHECK_AST(" +(x or  -y)- -z",  +(x| -y)- -z);
    CHECK_AST(" +x or ( -y)- -z",  +x|( -y)- -z);
    CHECK_AST(" +x or  -(y)- -z",  +x| -(y)- -z);
    CHECK_AST("( +x) or  -y- not z", ( +x)| -y- not z);
    CHECK_AST("( +x or  -y)- not z", ( +x| -y)- not z);
    CHECK_AST(" +(x) or  -y- not z",  +(x)| -y- not z);
    CHECK_AST(" +(x or  -y)- not z",  +(x| -y)- not z);
    CHECK_AST(" +x or ( -y)- not z",  +x|( -y)- not z);
    CHECK_AST(" +x or  -(y)- not z",  +x| -(y)- not z);
    CHECK_AST("( +x) or  not y-z", ( +x)| not y-z);
    CHECK_AST("( +x or  not y)-z", ( +x| not y)-z);
    CHECK_AST(" +(x) or  not y-z",  +(x)| not y-z);
    CHECK_AST(" +(x or  not y)-z",  +(x| not y)-z);
    CHECK_AST(" +x or ( not y)-z",  +x|( not y)-z);
    CHECK_AST(" +x or  not (y)-z",  +x| not (y)-z);
    CHECK_AST("( +x) or  not y- +z", ( +x)| not y- +z);
    CHECK_AST("( +x or  not y)- +z", ( +x| not y)- +z);
    CHECK_AST(" +(x) or  not y- +z",  +(x)| not y- +z);
    CHECK_AST(" +(x or  not y)- +z",  +(x| not y)- +z);
    CHECK_AST(" +x or ( not y)- +z",  +x|( not y)- +z);
    CHECK_AST(" +x or  not (y)- +z",  +x| not (y)- +z);
    CHECK_AST("( +x) or  not y- -z", ( +x)| not y- -z);
    CHECK_AST("( +x or  not y)- -z", ( +x| not y)- -z);
    CHECK_AST(" +(x) or  not y- -z",  +(x)| not y- -z);
    CHECK_AST(" +(x or  not y)- -z",  +(x| not y)- -z);
    CHECK_AST(" +x or ( not y)- -z",  +x|( not y)- -z);
    CHECK_AST(" +x or  not (y)- -z",  +x| not (y)- -z);
    CHECK_AST("( +x) or  not y- not z", ( +x)| not y- not z);
    CHECK_AST("( +x or  not y)- not z", ( +x| not y)- not z);
    CHECK_AST(" +(x) or  not y- not z",  +(x)| not y- not z);
    CHECK_AST(" +(x or  not y)- not z",  +(x| not y)- not z);
    CHECK_AST(" +x or ( not y)- not z",  +x|( not y)- not z);
    CHECK_AST(" +x or  not (y)- not z",  +x| not (y)- not z);
    CHECK_AST("( -x) or y-z", ( -x)|y-z);
    CHECK_AST("( -x or y)-z", ( -x|y)-z);
    CHECK_AST(" -(x) or y-z",  -(x)|y-z);
    CHECK_AST(" -(x or y)-z",  -(x|y)-z);
    CHECK_AST(" -x or (y)-z",  -x|(y)-z);
    CHECK_AST("( -x) or y- +z", ( -x)|y- +z);
    CHECK_AST("( -x or y)- +z", ( -x|y)- +z);
    CHECK_AST(" -(x) or y- +z",  -(x)|y- +z);
    CHECK_AST(" -(x or y)- +z",  -(x|y)- +z);
    CHECK_AST(" -x or (y)- +z",  -x|(y)- +z);
    CHECK_AST("( -x) or y- -z", ( -x)|y- -z);
    CHECK_AST("( -x or y)- -z", ( -x|y)- -z);
    CHECK_AST(" -(x) or y- -z",  -(x)|y- -z);
    CHECK_AST(" -(x or y)- -z",  -(x|y)- -z);
    CHECK_AST(" -x or (y)- -z",  -x|(y)- -z);
    CHECK_AST("( -x) or y- not z", ( -x)|y- not z);
    CHECK_AST("( -x or y)- not z", ( -x|y)- not z);
    CHECK_AST(" -(x) or y- not z",  -(x)|y- not z);
    CHECK_AST(" -(x or y)- not z",  -(x|y)- not z);
    CHECK_AST(" -x or (y)- not z",  -x|(y)- not z);
    CHECK_AST("( -x) or  +y-z", ( -x)| +y-z);
    CHECK_AST("( -x or  +y)-z", ( -x| +y)-z);
    CHECK_AST(" -(x) or  +y-z",  -(x)| +y-z);
    CHECK_AST(" -(x or  +y)-z",  -(x| +y)-z);
    CHECK_AST(" -x or ( +y)-z",  -x|( +y)-z);
    CHECK_AST(" -x or  +(y)-z",  -x| +(y)-z);
    CHECK_AST("( -x) or  +y- +z", ( -x)| +y- +z);
    CHECK_AST("( -x or  +y)- +z", ( -x| +y)- +z);
    CHECK_AST(" -(x) or  +y- +z",  -(x)| +y- +z);
    CHECK_AST(" -(x or  +y)- +z",  -(x| +y)- +z);
    CHECK_AST(" -x or ( +y)- +z",  -x|( +y)- +z);
    CHECK_AST(" -x or  +(y)- +z",  -x| +(y)- +z);
    CHECK_AST("( -x) or  +y- -z", ( -x)| +y- -z);
    CHECK_AST("( -x or  +y)- -z", ( -x| +y)- -z);
    CHECK_AST(" -(x) or  +y- -z",  -(x)| +y- -z);
    CHECK_AST(" -(x or  +y)- -z",  -(x| +y)- -z);
    CHECK_AST(" -x or ( +y)- -z",  -x|( +y)- -z);
    CHECK_AST(" -x or  +(y)- -z",  -x| +(y)- -z);
    CHECK_AST("( -x) or  +y- not z", ( -x)| +y- not z);
    CHECK_AST("( -x or  +y)- not z", ( -x| +y)- not z);
    CHECK_AST(" -(x) or  +y- not z",  -(x)| +y- not z);
    CHECK_AST(" -(x or  +y)- not z",  -(x| +y)- not z);
    CHECK_AST(" -x or ( +y)- not z",  -x|( +y)- not z);
    CHECK_AST(" -x or  +(y)- not z",  -x| +(y)- not z);
    CHECK_AST("( -x) or  -y-z", ( -x)| -y-z);
    CHECK_AST("( -x or  -y)-z", ( -x| -y)-z);
    CHECK_AST(" -(x) or  -y-z",  -(x)| -y-z);
    CHECK_AST(" -(x or  -y)-z",  -(x| -y)-z);
    CHECK_AST(" -x or ( -y)-z",  -x|( -y)-z);
    CHECK_AST(" -x or  -(y)-z",  -x| -(y)-z);
    CHECK_AST("( -x) or  -y- +z", ( -x)| -y- +z);
    CHECK_AST("( -x or  -y)- +z", ( -x| -y)- +z);
    CHECK_AST(" -(x) or  -y- +z",  -(x)| -y- +z);
    CHECK_AST(" -(x or  -y)- +z",  -(x| -y)- +z);
    CHECK_AST(" -x or ( -y)- +z",  -x|( -y)- +z);
    CHECK_AST(" -x or  -(y)- +z",  -x| -(y)- +z);
    CHECK_AST("( -x) or  -y- -z", ( -x)| -y- -z);
    CHECK_AST("( -x or  -y)- -z", ( -x| -y)- -z);
    CHECK_AST(" -(x) or  -y- -z",  -(x)| -y- -z);
    CHECK_AST(" -(x or  -y)- -z",  -(x| -y)- -z);
    CHECK_AST(" -x or ( -y)- -z",  -x|( -y)- -z);
    CHECK_AST(" -x or  -(y)- -z",  -x| -(y)- -z);
    CHECK_AST("( -x) or  -y- not z", ( -x)| -y- not z);
    CHECK_AST("( -x or  -y)- not z", ( -x| -y)- not z);
    CHECK_AST(" -(x) or  -y- not z",  -(x)| -y- not z);
    CHECK_AST(" -(x or  -y)- not z",  -(x| -y)- not z);
    CHECK_AST(" -x or ( -y)- not z",  -x|( -y)- not z);
    CHECK_AST(" -x or  -(y)- not z",  -x| -(y)- not z);
    CHECK_AST("( -x) or  not y-z", ( -x)| not y-z);
    CHECK_AST("( -x or  not y)-z", ( -x| not y)-z);
    CHECK_AST(" -(x) or  not y-z",  -(x)| not y-z);
    CHECK_AST(" -(x or  not y)-z",  -(x| not y)-z);
    CHECK_AST(" -x or ( not y)-z",  -x|( not y)-z);
    CHECK_AST(" -x or  not (y)-z",  -x| not (y)-z);
    CHECK_AST("( -x) or  not y- +z", ( -x)| not y- +z);
    CHECK_AST("( -x or  not y)- +z", ( -x| not y)- +z);
    CHECK_AST(" -(x) or  not y- +z",  -(x)| not y- +z);
    CHECK_AST(" -(x or  not y)- +z",  -(x| not y)- +z);
    CHECK_AST(" -x or ( not y)- +z",  -x|( not y)- +z);
    CHECK_AST(" -x or  not (y)- +z",  -x| not (y)- +z);
    CHECK_AST("( -x) or  not y- -z", ( -x)| not y- -z);
    CHECK_AST("( -x or  not y)- -z", ( -x| not y)- -z);
    CHECK_AST(" -(x) or  not y- -z",  -(x)| not y- -z);
    CHECK_AST(" -(x or  not y)- -z",  -(x| not y)- -z);
    CHECK_AST(" -x or ( not y)- -z",  -x|( not y)- -z);
    CHECK_AST(" -x or  not (y)- -z",  -x| not (y)- -z);
    CHECK_AST("( -x) or  not y- not z", ( -x)| not y- not z);
    CHECK_AST("( -x or  not y)- not z", ( -x| not y)- not z);
    CHECK_AST(" -(x) or  not y- not z",  -(x)| not y- not z);
    CHECK_AST(" -(x or  not y)- not z",  -(x| not y)- not z);
    CHECK_AST(" -x or ( not y)- not z",  -x|( not y)- not z);
    CHECK_AST(" -x or  not (y)- not z",  -x| not (y)- not z);
    CHECK_AST("( not x) or y-z", ( not x)|y-z);
    CHECK_AST("( not x or y)-z", ( not x|y)-z);
    CHECK_AST(" not (x) or y-z",  not (x)|y-z);
    CHECK_AST(" not (x or y)-z",  not (x|y)-z);
    CHECK_AST(" not x or (y)-z",  not x|(y)-z);
    CHECK_AST("( not x) or y- +z", ( not x)|y- +z);
    CHECK_AST("( not x or y)- +z", ( not x|y)- +z);
    CHECK_AST(" not (x) or y- +z",  not (x)|y- +z);
    CHECK_AST(" not (x or y)- +z",  not (x|y)- +z);
    CHECK_AST(" not x or (y)- +z",  not x|(y)- +z);
    CHECK_AST("( not x) or y- -z", ( not x)|y- -z);
    CHECK_AST("( not x or y)- -z", ( not x|y)- -z);
    CHECK_AST(" not (x) or y- -z",  not (x)|y- -z);
    CHECK_AST(" not (x or y)- -z",  not (x|y)- -z);
    CHECK_AST(" not x or (y)- -z",  not x|(y)- -z);
    CHECK_AST("( not x) or y- not z", ( not x)|y- not z);
    CHECK_AST("( not x or y)- not z", ( not x|y)- not z);
    CHECK_AST(" not (x) or y- not z",  not (x)|y- not z);
    CHECK_AST(" not (x or y)- not z",  not (x|y)- not z);
    CHECK_AST(" not x or (y)- not z",  not x|(y)- not z);
    CHECK_AST("( not x) or  +y-z", ( not x)| +y-z);
    CHECK_AST("( not x or  +y)-z", ( not x| +y)-z);
    CHECK_AST(" not (x) or  +y-z",  not (x)| +y-z);
    CHECK_AST(" not (x or  +y)-z",  not (x| +y)-z);
    CHECK_AST(" not x or ( +y)-z",  not x|( +y)-z);
    CHECK_AST(" not x or  +(y)-z",  not x| +(y)-z);
    CHECK_AST("( not x) or  +y- +z", ( not x)| +y- +z);
    CHECK_AST("( not x or  +y)- +z", ( not x| +y)- +z);
    CHECK_AST(" not (x) or  +y- +z",  not (x)| +y- +z);
    CHECK_AST(" not (x or  +y)- +z",  not (x| +y)- +z);
    CHECK_AST(" not x or ( +y)- +z",  not x|( +y)- +z);
    CHECK_AST(" not x or  +(y)- +z",  not x| +(y)- +z);
    CHECK_AST("( not x) or  +y- -z", ( not x)| +y- -z);
    CHECK_AST("( not x or  +y)- -z", ( not x| +y)- -z);
    CHECK_AST(" not (x) or  +y- -z",  not (x)| +y- -z);
    CHECK_AST(" not (x or  +y)- -z",  not (x| +y)- -z);
    CHECK_AST(" not x or ( +y)- -z",  not x|( +y)- -z);
    CHECK_AST(" not x or  +(y)- -z",  not x| +(y)- -z);
    CHECK_AST("( not x) or  +y- not z", ( not x)| +y- not z);
    CHECK_AST("( not x or  +y)- not z", ( not x| +y)- not z);
    CHECK_AST(" not (x) or  +y- not z",  not (x)| +y- not z);
    CHECK_AST(" not (x or  +y)- not z",  not (x| +y)- not z);
    CHECK_AST(" not x or ( +y)- not z",  not x|( +y)- not z);
    CHECK_AST(" not x or  +(y)- not z",  not x| +(y)- not z);
    CHECK_AST("( not x) or  -y-z", ( not x)| -y-z);
    CHECK_AST("( not x or  -y)-z", ( not x| -y)-z);
    CHECK_AST(" not (x) or  -y-z",  not (x)| -y-z);
    CHECK_AST(" not (x or  -y)-z",  not (x| -y)-z);
    CHECK_AST(" not x or ( -y)-z",  not x|( -y)-z);
    CHECK_AST(" not x or  -(y)-z",  not x| -(y)-z);
    CHECK_AST("( not x) or  -y- +z", ( not x)| -y- +z);
    CHECK_AST("( not x or  -y)- +z", ( not x| -y)- +z);
    CHECK_AST(" not (x) or  -y- +z",  not (x)| -y- +z);
    CHECK_AST(" not (x or  -y)- +z",  not (x| -y)- +z);
    CHECK_AST(" not x or ( -y)- +z",  not x|( -y)- +z);
    CHECK_AST(" not x or  -(y)- +z",  not x| -(y)- +z);
    CHECK_AST("( not x) or  -y- -z", ( not x)| -y- -z);
    CHECK_AST("( not x or  -y)- -z", ( not x| -y)- -z);
    CHECK_AST(" not (x) or  -y- -z",  not (x)| -y- -z);
    CHECK_AST(" not (x or  -y)- -z",  not (x| -y)- -z);
    CHECK_AST(" not x or ( -y)- -z",  not x|( -y)- -z);
    CHECK_AST(" not x or  -(y)- -z",  not x| -(y)- -z);
    CHECK_AST("( not x) or  -y- not z", ( not x)| -y- not z);
    CHECK_AST("( not x or  -y)- not z", ( not x| -y)- not z);
    CHECK_AST(" not (x) or  -y- not z",  not (x)| -y- not z);
    CHECK_AST(" not (x or  -y)- not z",  not (x| -y)- not z);
    CHECK_AST(" not x or ( -y)- not z",  not x|( -y)- not z);
    CHECK_AST(" not x or  -(y)- not z",  not x| -(y)- not z);
    CHECK_AST("( not x) or  not y-z", ( not x)| not y-z);
    CHECK_AST("( not x or  not y)-z", ( not x| not y)-z);
    CHECK_AST(" not (x) or  not y-z",  not (x)| not y-z);
    CHECK_AST(" not (x or  not y)-z",  not (x| not y)-z);
    CHECK_AST(" not x or ( not y)-z",  not x|( not y)-z);
    CHECK_AST(" not x or  not (y)-z",  not x| not (y)-z);
    CHECK_AST("( not x) or  not y- +z", ( not x)| not y- +z);
    CHECK_AST("( not x or  not y)- +z", ( not x| not y)- +z);
    CHECK_AST(" not (x) or  not y- +z",  not (x)| not y- +z);
    CHECK_AST(" not (x or  not y)- +z",  not (x| not y)- +z);
    CHECK_AST(" not x or ( not y)- +z",  not x|( not y)- +z);
    CHECK_AST(" not x or  not (y)- +z",  not x| not (y)- +z);
    CHECK_AST("( not x) or  not y- -z", ( not x)| not y- -z);
    CHECK_AST("( not x or  not y)- -z", ( not x| not y)- -z);
    CHECK_AST(" not (x) or  not y- -z",  not (x)| not y- -z);
    CHECK_AST(" not (x or  not y)- -z",  not (x| not y)- -z);
    CHECK_AST(" not x or ( not y)- -z",  not x|( not y)- -z);
    CHECK_AST(" not x or  not (y)- -z",  not x| not (y)- -z);
    CHECK_AST("( not x) or  not y- not z", ( not x)| not y- not z);
    CHECK_AST("( not x or  not y)- not z", ( not x| not y)- not z);
    CHECK_AST(" not (x) or  not y- not z",  not (x)| not y- not z);
    CHECK_AST(" not (x or  not y)- not z",  not (x| not y)- not z);
    CHECK_AST(" not x or ( not y)- not z",  not x|( not y)- not z);
    CHECK_AST(" not x or  not (y)- not z",  not x| not (y)- not z);
    CHECK_AST("(x) or y<z", (x)|y<z);
    CHECK_AST("(x or y)<z", (x|y)<z);
    CHECK_AST("x or (y)<z", x|(y)<z);
    CHECK_AST("(x) or y< +z", (x)|y< +z);
    CHECK_AST("(x or y)< +z", (x|y)< +z);
    CHECK_AST("x or (y)< +z", x|(y)< +z);
    CHECK_AST("(x) or y< -z", (x)|y< -z);
    CHECK_AST("(x or y)< -z", (x|y)< -z);
    CHECK_AST("x or (y)< -z", x|(y)< -z);
    CHECK_AST("(x) or y< not z", (x)|y< not z);
    CHECK_AST("(x or y)< not z", (x|y)< not z);
    CHECK_AST("x or (y)< not z", x|(y)< not z);
    CHECK_AST("(x) or  +y<z", (x)| +y<z);
    CHECK_AST("(x or  +y)<z", (x| +y)<z);
    CHECK_AST("x or ( +y)<z", x|( +y)<z);
    CHECK_AST("x or  +(y)<z", x| +(y)<z);
    CHECK_AST("(x) or  +y< +z", (x)| +y< +z);
    CHECK_AST("(x or  +y)< +z", (x| +y)< +z);
    CHECK_AST("x or ( +y)< +z", x|( +y)< +z);
    CHECK_AST("x or  +(y)< +z", x| +(y)< +z);
    CHECK_AST("(x) or  +y< -z", (x)| +y< -z);
    CHECK_AST("(x or  +y)< -z", (x| +y)< -z);
    CHECK_AST("x or ( +y)< -z", x|( +y)< -z);
    CHECK_AST("x or  +(y)< -z", x| +(y)< -z);
    CHECK_AST("(x) or  +y< not z", (x)| +y< not z);
    CHECK_AST("(x or  +y)< not z", (x| +y)< not z);
    CHECK_AST("x or ( +y)< not z", x|( +y)< not z);
    CHECK_AST("x or  +(y)< not z", x| +(y)< not z);
    CHECK_AST("(x) or  -y<z", (x)| -y<z);
    CHECK_AST("(x or  -y)<z", (x| -y)<z);
    CHECK_AST("x or ( -y)<z", x|( -y)<z);
    CHECK_AST("x or  -(y)<z", x| -(y)<z);
    CHECK_AST("(x) or  -y< +z", (x)| -y< +z);
    CHECK_AST("(x or  -y)< +z", (x| -y)< +z);
    CHECK_AST("x or ( -y)< +z", x|( -y)< +z);
    CHECK_AST("x or  -(y)< +z", x| -(y)< +z);
    CHECK_AST("(x) or  -y< -z", (x)| -y< -z);
    CHECK_AST("(x or  -y)< -z", (x| -y)< -z);
    CHECK_AST("x or ( -y)< -z", x|( -y)< -z);
    CHECK_AST("x or  -(y)< -z", x| -(y)< -z);
    CHECK_AST("(x) or  -y< not z", (x)| -y< not z);
    CHECK_AST("(x or  -y)< not z", (x| -y)< not z);
    CHECK_AST("x or ( -y)< not z", x|( -y)< not z);
    CHECK_AST("x or  -(y)< not z", x| -(y)< not z);
    CHECK_AST("(x) or  not y<z", (x)| not y<z);
    CHECK_AST("(x or  not y)<z", (x| not y)<z);
    CHECK_AST("x or ( not y)<z", x|( not y)<z);
    CHECK_AST("x or  not (y)<z", x| not (y)<z);
    CHECK_AST("(x) or  not y< +z", (x)| not y< +z);
    CHECK_AST("(x or  not y)< +z", (x| not y)< +z);
    CHECK_AST("x or ( not y)< +z", x|( not y)< +z);
    CHECK_AST("x or  not (y)< +z", x| not (y)< +z);
    CHECK_AST("(x) or  not y< -z", (x)| not y< -z);
    CHECK_AST("(x or  not y)< -z", (x| not y)< -z);
    CHECK_AST("x or ( not y)< -z", x|( not y)< -z);
    CHECK_AST("x or  not (y)< -z", x| not (y)< -z);
    CHECK_AST("(x) or  not y< not z", (x)| not y< not z);
    CHECK_AST("(x or  not y)< not z", (x| not y)< not z);
    CHECK_AST("x or ( not y)< not z", x|( not y)< not z);
    CHECK_AST("x or  not (y)< not z", x| not (y)< not z);
    CHECK_AST("( +x) or y<z", ( +x)|y<z);
    CHECK_AST("( +x or y)<z", ( +x|y)<z);
    CHECK_AST(" +(x) or y<z",  +(x)|y<z);
    CHECK_AST(" +(x or y)<z",  +(x|y)<z);
    CHECK_AST(" +x or (y)<z",  +x|(y)<z);
    CHECK_AST("( +x) or y< +z", ( +x)|y< +z);
    CHECK_AST("( +x or y)< +z", ( +x|y)< +z);
    CHECK_AST(" +(x) or y< +z",  +(x)|y< +z);
    CHECK_AST(" +(x or y)< +z",  +(x|y)< +z);
    CHECK_AST(" +x or (y)< +z",  +x|(y)< +z);
    CHECK_AST("( +x) or y< -z", ( +x)|y< -z);
    CHECK_AST("( +x or y)< -z", ( +x|y)< -z);
    CHECK_AST(" +(x) or y< -z",  +(x)|y< -z);
    CHECK_AST(" +(x or y)< -z",  +(x|y)< -z);
    CHECK_AST(" +x or (y)< -z",  +x|(y)< -z);
    CHECK_AST("( +x) or y< not z", ( +x)|y< not z);
    CHECK_AST("( +x or y)< not z", ( +x|y)< not z);
    CHECK_AST(" +(x) or y< not z",  +(x)|y< not z);
    CHECK_AST(" +(x or y)< not z",  +(x|y)< not z);
    CHECK_AST(" +x or (y)< not z",  +x|(y)< not z);
    CHECK_AST("( +x) or  +y<z", ( +x)| +y<z);
    CHECK_AST("( +x or  +y)<z", ( +x| +y)<z);
    CHECK_AST(" +(x) or  +y<z",  +(x)| +y<z);
    CHECK_AST(" +(x or  +y)<z",  +(x| +y)<z);
    CHECK_AST(" +x or ( +y)<z",  +x|( +y)<z);
    CHECK_AST(" +x or  +(y)<z",  +x| +(y)<z);
    CHECK_AST("( +x) or  +y< +z", ( +x)| +y< +z);
    CHECK_AST("( +x or  +y)< +z", ( +x| +y)< +z);
    CHECK_AST(" +(x) or  +y< +z",  +(x)| +y< +z);
    CHECK_AST(" +(x or  +y)< +z",  +(x| +y)< +z);
    CHECK_AST(" +x or ( +y)< +z",  +x|( +y)< +z);
    CHECK_AST(" +x or  +(y)< +z",  +x| +(y)< +z);
    CHECK_AST("( +x) or  +y< -z", ( +x)| +y< -z);
    CHECK_AST("( +x or  +y)< -z", ( +x| +y)< -z);
    CHECK_AST(" +(x) or  +y< -z",  +(x)| +y< -z);
    CHECK_AST(" +(x or  +y)< -z",  +(x| +y)< -z);
    CHECK_AST(" +x or ( +y)< -z",  +x|( +y)< -z);
    CHECK_AST(" +x or  +(y)< -z",  +x| +(y)< -z);
    CHECK_AST("( +x) or  +y< not z", ( +x)| +y< not z);
    CHECK_AST("( +x or  +y)< not z", ( +x| +y)< not z);
    CHECK_AST(" +(x) or  +y< not z",  +(x)| +y< not z);
    CHECK_AST(" +(x or  +y)< not z",  +(x| +y)< not z);
    CHECK_AST(" +x or ( +y)< not z",  +x|( +y)< not z);
    CHECK_AST(" +x or  +(y)< not z",  +x| +(y)< not z);
    CHECK_AST("( +x) or  -y<z", ( +x)| -y<z);
    CHECK_AST("( +x or  -y)<z", ( +x| -y)<z);
    CHECK_AST(" +(x) or  -y<z",  +(x)| -y<z);
    CHECK_AST(" +(x or  -y)<z",  +(x| -y)<z);
    CHECK_AST(" +x or ( -y)<z",  +x|( -y)<z);
    CHECK_AST(" +x or  -(y)<z",  +x| -(y)<z);
    CHECK_AST("( +x) or  -y< +z", ( +x)| -y< +z);
    CHECK_AST("( +x or  -y)< +z", ( +x| -y)< +z);
    CHECK_AST(" +(x) or  -y< +z",  +(x)| -y< +z);
    CHECK_AST(" +(x or  -y)< +z",  +(x| -y)< +z);
    CHECK_AST(" +x or ( -y)< +z",  +x|( -y)< +z);
    CHECK_AST(" +x or  -(y)< +z",  +x| -(y)< +z);
    CHECK_AST("( +x) or  -y< -z", ( +x)| -y< -z);
    CHECK_AST("( +x or  -y)< -z", ( +x| -y)< -z);
    CHECK_AST(" +(x) or  -y< -z",  +(x)| -y< -z);
    CHECK_AST(" +(x or  -y)< -z",  +(x| -y)< -z);
    CHECK_AST(" +x or ( -y)< -z",  +x|( -y)< -z);
    CHECK_AST(" +x or  -(y)< -z",  +x| -(y)< -z);
    CHECK_AST("( +x) or  -y< not z", ( +x)| -y< not z);
    CHECK_AST("( +x or  -y)< not z", ( +x| -y)< not z);
    CHECK_AST(" +(x) or  -y< not z",  +(x)| -y< not z);
    CHECK_AST(" +(x or  -y)< not z",  +(x| -y)< not z);
    CHECK_AST(" +x or ( -y)< not z",  +x|( -y)< not z);
    CHECK_AST(" +x or  -(y)< not z",  +x| -(y)< not z);
    CHECK_AST("( +x) or  not y<z", ( +x)| not y<z);
    CHECK_AST("( +x or  not y)<z", ( +x| not y)<z);
    CHECK_AST(" +(x) or  not y<z",  +(x)| not y<z);
    CHECK_AST(" +(x or  not y)<z",  +(x| not y)<z);
    CHECK_AST(" +x or ( not y)<z",  +x|( not y)<z);
    CHECK_AST(" +x or  not (y)<z",  +x| not (y)<z);
    CHECK_AST("( +x) or  not y< +z", ( +x)| not y< +z);
    CHECK_AST("( +x or  not y)< +z", ( +x| not y)< +z);
    CHECK_AST(" +(x) or  not y< +z",  +(x)| not y< +z);
    CHECK_AST(" +(x or  not y)< +z",  +(x| not y)< +z);
    CHECK_AST(" +x or ( not y)< +z",  +x|( not y)< +z);
    CHECK_AST(" +x or  not (y)< +z",  +x| not (y)< +z);
    CHECK_AST("( +x) or  not y< -z", ( +x)| not y< -z);
    CHECK_AST("( +x or  not y)< -z", ( +x| not y)< -z);
    CHECK_AST(" +(x) or  not y< -z",  +(x)| not y< -z);
    CHECK_AST(" +(x or  not y)< -z",  +(x| not y)< -z);
    CHECK_AST(" +x or ( not y)< -z",  +x|( not y)< -z);
    CHECK_AST(" +x or  not (y)< -z",  +x| not (y)< -z);
    CHECK_AST("( +x) or  not y< not z", ( +x)| not y< not z);
    CHECK_AST("( +x or  not y)< not z", ( +x| not y)< not z);
    CHECK_AST(" +(x) or  not y< not z",  +(x)| not y< not z);
    CHECK_AST(" +(x or  not y)< not z",  +(x| not y)< not z);
    CHECK_AST(" +x or ( not y)< not z",  +x|( not y)< not z);
    CHECK_AST(" +x or  not (y)< not z",  +x| not (y)< not z);
    CHECK_AST("( -x) or y<z", ( -x)|y<z);
    CHECK_AST("( -x or y)<z", ( -x|y)<z);
    CHECK_AST(" -(x) or y<z",  -(x)|y<z);
    CHECK_AST(" -(x or y)<z",  -(x|y)<z);
    CHECK_AST(" -x or (y)<z",  -x|(y)<z);
    CHECK_AST("( -x) or y< +z", ( -x)|y< +z);
    CHECK_AST("( -x or y)< +z", ( -x|y)< +z);
    CHECK_AST(" -(x) or y< +z",  -(x)|y< +z);
    CHECK_AST(" -(x or y)< +z",  -(x|y)< +z);
    CHECK_AST(" -x or (y)< +z",  -x|(y)< +z);
    CHECK_AST("( -x) or y< -z", ( -x)|y< -z);
    CHECK_AST("( -x or y)< -z", ( -x|y)< -z);
    CHECK_AST(" -(x) or y< -z",  -(x)|y< -z);
    CHECK_AST(" -(x or y)< -z",  -(x|y)< -z);
    CHECK_AST(" -x or (y)< -z",  -x|(y)< -z);
    CHECK_AST("( -x) or y< not z", ( -x)|y< not z);
    CHECK_AST("( -x or y)< not z", ( -x|y)< not z);
    CHECK_AST(" -(x) or y< not z",  -(x)|y< not z);
    CHECK_AST(" -(x or y)< not z",  -(x|y)< not z);
    CHECK_AST(" -x or (y)< not z",  -x|(y)< not z);
    CHECK_AST("( -x) or  +y<z", ( -x)| +y<z);
    CHECK_AST("( -x or  +y)<z", ( -x| +y)<z);
    CHECK_AST(" -(x) or  +y<z",  -(x)| +y<z);
    CHECK_AST(" -(x or  +y)<z",  -(x| +y)<z);
    CHECK_AST(" -x or ( +y)<z",  -x|( +y)<z);
    CHECK_AST(" -x or  +(y)<z",  -x| +(y)<z);
    CHECK_AST("( -x) or  +y< +z", ( -x)| +y< +z);
    CHECK_AST("( -x or  +y)< +z", ( -x| +y)< +z);
    CHECK_AST(" -(x) or  +y< +z",  -(x)| +y< +z);
    CHECK_AST(" -(x or  +y)< +z",  -(x| +y)< +z);
    CHECK_AST(" -x or ( +y)< +z",  -x|( +y)< +z);
    CHECK_AST(" -x or  +(y)< +z",  -x| +(y)< +z);
    CHECK_AST("( -x) or  +y< -z", ( -x)| +y< -z);
    CHECK_AST("( -x or  +y)< -z", ( -x| +y)< -z);
    CHECK_AST(" -(x) or  +y< -z",  -(x)| +y< -z);
    CHECK_AST(" -(x or  +y)< -z",  -(x| +y)< -z);
    CHECK_AST(" -x or ( +y)< -z",  -x|( +y)< -z);
    CHECK_AST(" -x or  +(y)< -z",  -x| +(y)< -z);
    CHECK_AST("( -x) or  +y< not z", ( -x)| +y< not z);
    CHECK_AST("( -x or  +y)< not z", ( -x| +y)< not z);
    CHECK_AST(" -(x) or  +y< not z",  -(x)| +y< not z);
    CHECK_AST(" -(x or  +y)< not z",  -(x| +y)< not z);
    CHECK_AST(" -x or ( +y)< not z",  -x|( +y)< not z);
    CHECK_AST(" -x or  +(y)< not z",  -x| +(y)< not z);
    CHECK_AST("( -x) or  -y<z", ( -x)| -y<z);
    CHECK_AST("( -x or  -y)<z", ( -x| -y)<z);
    CHECK_AST(" -(x) or  -y<z",  -(x)| -y<z);
    CHECK_AST(" -(x or  -y)<z",  -(x| -y)<z);
    CHECK_AST(" -x or ( -y)<z",  -x|( -y)<z);
    CHECK_AST(" -x or  -(y)<z",  -x| -(y)<z);
    CHECK_AST("( -x) or  -y< +z", ( -x)| -y< +z);
    CHECK_AST("( -x or  -y)< +z", ( -x| -y)< +z);
    CHECK_AST(" -(x) or  -y< +z",  -(x)| -y< +z);
    CHECK_AST(" -(x or  -y)< +z",  -(x| -y)< +z);
    CHECK_AST(" -x or ( -y)< +z",  -x|( -y)< +z);
    CHECK_AST(" -x or  -(y)< +z",  -x| -(y)< +z);
    CHECK_AST("( -x) or  -y< -z", ( -x)| -y< -z);
    CHECK_AST("( -x or  -y)< -z", ( -x| -y)< -z);
    CHECK_AST(" -(x) or  -y< -z",  -(x)| -y< -z);
    CHECK_AST(" -(x or  -y)< -z",  -(x| -y)< -z);
    CHECK_AST(" -x or ( -y)< -z",  -x|( -y)< -z);
    CHECK_AST(" -x or  -(y)< -z",  -x| -(y)< -z);
    CHECK_AST("( -x) or  -y< not z", ( -x)| -y< not z);
    CHECK_AST("( -x or  -y)< not z", ( -x| -y)< not z);
    CHECK_AST(" -(x) or  -y< not z",  -(x)| -y< not z);
    CHECK_AST(" -(x or  -y)< not z",  -(x| -y)< not z);
    CHECK_AST(" -x or ( -y)< not z",  -x|( -y)< not z);
    CHECK_AST(" -x or  -(y)< not z",  -x| -(y)< not z);
    CHECK_AST("( -x) or  not y<z", ( -x)| not y<z);
    CHECK_AST("( -x or  not y)<z", ( -x| not y)<z);
    CHECK_AST(" -(x) or  not y<z",  -(x)| not y<z);
    CHECK_AST(" -(x or  not y)<z",  -(x| not y)<z);
    CHECK_AST(" -x or ( not y)<z",  -x|( not y)<z);
    CHECK_AST(" -x or  not (y)<z",  -x| not (y)<z);
    CHECK_AST("( -x) or  not y< +z", ( -x)| not y< +z);
    CHECK_AST("( -x or  not y)< +z", ( -x| not y)< +z);
    CHECK_AST(" -(x) or  not y< +z",  -(x)| not y< +z);
    CHECK_AST(" -(x or  not y)< +z",  -(x| not y)< +z);
    CHECK_AST(" -x or ( not y)< +z",  -x|( not y)< +z);
    CHECK_AST(" -x or  not (y)< +z",  -x| not (y)< +z);
    CHECK_AST("( -x) or  not y< -z", ( -x)| not y< -z);
    CHECK_AST("( -x or  not y)< -z", ( -x| not y)< -z);
    CHECK_AST(" -(x) or  not y< -z",  -(x)| not y< -z);
    CHECK_AST(" -(x or  not y)< -z",  -(x| not y)< -z);
    CHECK_AST(" -x or ( not y)< -z",  -x|( not y)< -z);
    CHECK_AST(" -x or  not (y)< -z",  -x| not (y)< -z);
    CHECK_AST("( -x) or  not y< not z", ( -x)| not y< not z);
    CHECK_AST("( -x or  not y)< not z", ( -x| not y)< not z);
    CHECK_AST(" -(x) or  not y< not z",  -(x)| not y< not z);
    CHECK_AST(" -(x or  not y)< not z",  -(x| not y)< not z);
    CHECK_AST(" -x or ( not y)< not z",  -x|( not y)< not z);
    CHECK_AST(" -x or  not (y)< not z",  -x| not (y)< not z);
    CHECK_AST("( not x) or y<z", ( not x)|y<z);
    CHECK_AST("( not x or y)<z", ( not x|y)<z);
    CHECK_AST(" not (x) or y<z",  not (x)|y<z);
    CHECK_AST(" not (x or y)<z",  not (x|y)<z);
    CHECK_AST(" not x or (y)<z",  not x|(y)<z);
    CHECK_AST("( not x) or y< +z", ( not x)|y< +z);
    CHECK_AST("( not x or y)< +z", ( not x|y)< +z);
    CHECK_AST(" not (x) or y< +z",  not (x)|y< +z);
    CHECK_AST(" not (x or y)< +z",  not (x|y)< +z);
    CHECK_AST(" not x or (y)< +z",  not x|(y)< +z);
    CHECK_AST("( not x) or y< -z", ( not x)|y< -z);
    CHECK_AST("( not x or y)< -z", ( not x|y)< -z);
    CHECK_AST(" not (x) or y< -z",  not (x)|y< -z);
    CHECK_AST(" not (x or y)< -z",  not (x|y)< -z);
    CHECK_AST(" not x or (y)< -z",  not x|(y)< -z);
    CHECK_AST("( not x) or y< not z", ( not x)|y< not z);
    CHECK_AST("( not x or y)< not z", ( not x|y)< not z);
    CHECK_AST(" not (x) or y< not z",  not (x)|y< not z);
    CHECK_AST(" not (x or y)< not z",  not (x|y)< not z);
    CHECK_AST(" not x or (y)< not z",  not x|(y)< not z);
    CHECK_AST("( not x) or  +y<z", ( not x)| +y<z);
    CHECK_AST("( not x or  +y)<z", ( not x| +y)<z);
    CHECK_AST(" not (x) or  +y<z",  not (x)| +y<z);
    CHECK_AST(" not (x or  +y)<z",  not (x| +y)<z);
    CHECK_AST(" not x or ( +y)<z",  not x|( +y)<z);
    CHECK_AST(" not x or  +(y)<z",  not x| +(y)<z);
    CHECK_AST("( not x) or  +y< +z", ( not x)| +y< +z);
    CHECK_AST("( not x or  +y)< +z", ( not x| +y)< +z);
    CHECK_AST(" not (x) or  +y< +z",  not (x)| +y< +z);
    CHECK_AST(" not (x or  +y)< +z",  not (x| +y)< +z);
    CHECK_AST(" not x or ( +y)< +z",  not x|( +y)< +z);
    CHECK_AST(" not x or  +(y)< +z",  not x| +(y)< +z);
    CHECK_AST("( not x) or  +y< -z", ( not x)| +y< -z);
    CHECK_AST("( not x or  +y)< -z", ( not x| +y)< -z);
    CHECK_AST(" not (x) or  +y< -z",  not (x)| +y< -z);
    CHECK_AST(" not (x or  +y)< -z",  not (x| +y)< -z);
    CHECK_AST(" not x or ( +y)< -z",  not x|( +y)< -z);
    CHECK_AST(" not x or  +(y)< -z",  not x| +(y)< -z);
    CHECK_AST("( not x) or  +y< not z", ( not x)| +y< not z);
    CHECK_AST("( not x or  +y)< not z", ( not x| +y)< not z);
    CHECK_AST(" not (x) or  +y< not z",  not (x)| +y< not z);
    CHECK_AST(" not (x or  +y)< not z",  not (x| +y)< not z);
    CHECK_AST(" not x or ( +y)< not z",  not x|( +y)< not z);
    CHECK_AST(" not x or  +(y)< not z",  not x| +(y)< not z);
    CHECK_AST("( not x) or  -y<z", ( not x)| -y<z);
    CHECK_AST("( not x or  -y)<z", ( not x| -y)<z);
    CHECK_AST(" not (x) or  -y<z",  not (x)| -y<z);
    CHECK_AST(" not (x or  -y)<z",  not (x| -y)<z);
    CHECK_AST(" not x or ( -y)<z",  not x|( -y)<z);
    CHECK_AST(" not x or  -(y)<z",  not x| -(y)<z);
    CHECK_AST("( not x) or  -y< +z", ( not x)| -y< +z);
    CHECK_AST("( not x or  -y)< +z", ( not x| -y)< +z);
    CHECK_AST(" not (x) or  -y< +z",  not (x)| -y< +z);
    CHECK_AST(" not (x or  -y)< +z",  not (x| -y)< +z);
    CHECK_AST(" not x or ( -y)< +z",  not x|( -y)< +z);
    CHECK_AST(" not x or  -(y)< +z",  not x| -(y)< +z);
    CHECK_AST("( not x) or  -y< -z", ( not x)| -y< -z);
    CHECK_AST("( not x or  -y)< -z", ( not x| -y)< -z);
    CHECK_AST(" not (x) or  -y< -z",  not (x)| -y< -z);
    CHECK_AST(" not (x or  -y)< -z",  not (x| -y)< -z);
    CHECK_AST(" not x or ( -y)< -z",  not x|( -y)< -z);
    CHECK_AST(" not x or  -(y)< -z",  not x| -(y)< -z);
    CHECK_AST("( not x) or  -y< not z", ( not x)| -y< not z);
    CHECK_AST("( not x or  -y)< not z", ( not x| -y)< not z);
    CHECK_AST(" not (x) or  -y< not z",  not (x)| -y< not z);
    CHECK_AST(" not (x or  -y)< not z",  not (x| -y)< not z);
    CHECK_AST(" not x or ( -y)< not z",  not x|( -y)< not z);
    CHECK_AST(" not x or  -(y)< not z",  not x| -(y)< not z);
    CHECK_AST("( not x) or  not y<z", ( not x)| not y<z);
    CHECK_AST("( not x or  not y)<z", ( not x| not y)<z);
    CHECK_AST(" not (x) or  not y<z",  not (x)| not y<z);
    CHECK_AST(" not (x or  not y)<z",  not (x| not y)<z);
    CHECK_AST(" not x or ( not y)<z",  not x|( not y)<z);
    CHECK_AST(" not x or  not (y)<z",  not x| not (y)<z);
    CHECK_AST("( not x) or  not y< +z", ( not x)| not y< +z);
    CHECK_AST("( not x or  not y)< +z", ( not x| not y)< +z);
    CHECK_AST(" not (x) or  not y< +z",  not (x)| not y< +z);
    CHECK_AST(" not (x or  not y)< +z",  not (x| not y)< +z);
    CHECK_AST(" not x or ( not y)< +z",  not x|( not y)< +z);
    CHECK_AST(" not x or  not (y)< +z",  not x| not (y)< +z);
    CHECK_AST("( not x) or  not y< -z", ( not x)| not y< -z);
    CHECK_AST("( not x or  not y)< -z", ( not x| not y)< -z);
    CHECK_AST(" not (x) or  not y< -z",  not (x)| not y< -z);
    CHECK_AST(" not (x or  not y)< -z",  not (x| not y)< -z);
    CHECK_AST(" not x or ( not y)< -z",  not x|( not y)< -z);
    CHECK_AST(" not x or  not (y)< -z",  not x| not (y)< -z);
    CHECK_AST("( not x) or  not y< not z", ( not x)| not y< not z);
    CHECK_AST("( not x or  not y)< not z", ( not x| not y)< not z);
    CHECK_AST(" not (x) or  not y< not z",  not (x)| not y< not z);
    CHECK_AST(" not (x or  not y)< not z",  not (x| not y)< not z);
    CHECK_AST(" not x or ( not y)< not z",  not x|( not y)< not z);
    CHECK_AST(" not x or  not (y)< not z",  not x| not (y)< not z);
    CHECK_AST("(x) or y<=z", (x)|y<=z);
    CHECK_AST("(x or y)<=z", (x|y)<=z);
    CHECK_AST("x or (y)<=z", x|(y)<=z);
    CHECK_AST("(x) or y<= +z", (x)|y<= +z);
    CHECK_AST("(x or y)<= +z", (x|y)<= +z);
    CHECK_AST("x or (y)<= +z", x|(y)<= +z);
    CHECK_AST("(x) or y<= -z", (x)|y<= -z);
    CHECK_AST("(x or y)<= -z", (x|y)<= -z);
    CHECK_AST("x or (y)<= -z", x|(y)<= -z);
    CHECK_AST("(x) or y<= not z", (x)|y<= not z);
    CHECK_AST("(x or y)<= not z", (x|y)<= not z);
    CHECK_AST("x or (y)<= not z", x|(y)<= not z);
    CHECK_AST("(x) or  +y<=z", (x)| +y<=z);
    CHECK_AST("(x or  +y)<=z", (x| +y)<=z);
    CHECK_AST("x or ( +y)<=z", x|( +y)<=z);
    CHECK_AST("x or  +(y)<=z", x| +(y)<=z);
    CHECK_AST("(x) or  +y<= +z", (x)| +y<= +z);
    CHECK_AST("(x or  +y)<= +z", (x| +y)<= +z);
    CHECK_AST("x or ( +y)<= +z", x|( +y)<= +z);
    CHECK_AST("x or  +(y)<= +z", x| +(y)<= +z);
    CHECK_AST("(x) or  +y<= -z", (x)| +y<= -z);
    CHECK_AST("(x or  +y)<= -z", (x| +y)<= -z);
    CHECK_AST("x or ( +y)<= -z", x|( +y)<= -z);
    CHECK_AST("x or  +(y)<= -z", x| +(y)<= -z);
    CHECK_AST("(x) or  +y<= not z", (x)| +y<= not z);
    CHECK_AST("(x or  +y)<= not z", (x| +y)<= not z);
    CHECK_AST("x or ( +y)<= not z", x|( +y)<= not z);
    CHECK_AST("x or  +(y)<= not z", x| +(y)<= not z);
    CHECK_AST("(x) or  -y<=z", (x)| -y<=z);
    CHECK_AST("(x or  -y)<=z", (x| -y)<=z);
    CHECK_AST("x or ( -y)<=z", x|( -y)<=z);
    CHECK_AST("x or  -(y)<=z", x| -(y)<=z);
    CHECK_AST("(x) or  -y<= +z", (x)| -y<= +z);
    CHECK_AST("(x or  -y)<= +z", (x| -y)<= +z);
    CHECK_AST("x or ( -y)<= +z", x|( -y)<= +z);
    CHECK_AST("x or  -(y)<= +z", x| -(y)<= +z);
    CHECK_AST("(x) or  -y<= -z", (x)| -y<= -z);
    CHECK_AST("(x or  -y)<= -z", (x| -y)<= -z);
    CHECK_AST("x or ( -y)<= -z", x|( -y)<= -z);
    CHECK_AST("x or  -(y)<= -z", x| -(y)<= -z);
    CHECK_AST("(x) or  -y<= not z", (x)| -y<= not z);
    CHECK_AST("(x or  -y)<= not z", (x| -y)<= not z);
    CHECK_AST("x or ( -y)<= not z", x|( -y)<= not z);
    CHECK_AST("x or  -(y)<= not z", x| -(y)<= not z);
    CHECK_AST("(x) or  not y<=z", (x)| not y<=z);
    CHECK_AST("(x or  not y)<=z", (x| not y)<=z);
    CHECK_AST("x or ( not y)<=z", x|( not y)<=z);
    CHECK_AST("x or  not (y)<=z", x| not (y)<=z);
    CHECK_AST("(x) or  not y<= +z", (x)| not y<= +z);
    CHECK_AST("(x or  not y)<= +z", (x| not y)<= +z);
    CHECK_AST("x or ( not y)<= +z", x|( not y)<= +z);
    CHECK_AST("x or  not (y)<= +z", x| not (y)<= +z);
    CHECK_AST("(x) or  not y<= -z", (x)| not y<= -z);
    CHECK_AST("(x or  not y)<= -z", (x| not y)<= -z);
    CHECK_AST("x or ( not y)<= -z", x|( not y)<= -z);
    CHECK_AST("x or  not (y)<= -z", x| not (y)<= -z);
    CHECK_AST("(x) or  not y<= not z", (x)| not y<= not z);
    CHECK_AST("(x or  not y)<= not z", (x| not y)<= not z);
    CHECK_AST("x or ( not y)<= not z", x|( not y)<= not z);
    CHECK_AST("x or  not (y)<= not z", x| not (y)<= not z);
    CHECK_AST("( +x) or y<=z", ( +x)|y<=z);
    CHECK_AST("( +x or y)<=z", ( +x|y)<=z);
    CHECK_AST(" +(x) or y<=z",  +(x)|y<=z);
    CHECK_AST(" +(x or y)<=z",  +(x|y)<=z);
    CHECK_AST(" +x or (y)<=z",  +x|(y)<=z);
    CHECK_AST("( +x) or y<= +z", ( +x)|y<= +z);
    CHECK_AST("( +x or y)<= +z", ( +x|y)<= +z);
    CHECK_AST(" +(x) or y<= +z",  +(x)|y<= +z);
    CHECK_AST(" +(x or y)<= +z",  +(x|y)<= +z);
    CHECK_AST(" +x or (y)<= +z",  +x|(y)<= +z);
    CHECK_AST("( +x) or y<= -z", ( +x)|y<= -z);
    CHECK_AST("( +x or y)<= -z", ( +x|y)<= -z);
    CHECK_AST(" +(x) or y<= -z",  +(x)|y<= -z);
    CHECK_AST(" +(x or y)<= -z",  +(x|y)<= -z);
    CHECK_AST(" +x or (y)<= -z",  +x|(y)<= -z);
    CHECK_AST("( +x) or y<= not z", ( +x)|y<= not z);
    CHECK_AST("( +x or y)<= not z", ( +x|y)<= not z);
    CHECK_AST(" +(x) or y<= not z",  +(x)|y<= not z);
    CHECK_AST(" +(x or y)<= not z",  +(x|y)<= not z);
    CHECK_AST(" +x or (y)<= not z",  +x|(y)<= not z);
    CHECK_AST("( +x) or  +y<=z", ( +x)| +y<=z);
    CHECK_AST("( +x or  +y)<=z", ( +x| +y)<=z);
    CHECK_AST(" +(x) or  +y<=z",  +(x)| +y<=z);
    CHECK_AST(" +(x or  +y)<=z",  +(x| +y)<=z);
    CHECK_AST(" +x or ( +y)<=z",  +x|( +y)<=z);
    CHECK_AST(" +x or  +(y)<=z",  +x| +(y)<=z);
    CHECK_AST("( +x) or  +y<= +z", ( +x)| +y<= +z);
    CHECK_AST("( +x or  +y)<= +z", ( +x| +y)<= +z);
    CHECK_AST(" +(x) or  +y<= +z",  +(x)| +y<= +z);
    CHECK_AST(" +(x or  +y)<= +z",  +(x| +y)<= +z);
    CHECK_AST(" +x or ( +y)<= +z",  +x|( +y)<= +z);
    CHECK_AST(" +x or  +(y)<= +z",  +x| +(y)<= +z);
    CHECK_AST("( +x) or  +y<= -z", ( +x)| +y<= -z);
    CHECK_AST("( +x or  +y)<= -z", ( +x| +y)<= -z);
    CHECK_AST(" +(x) or  +y<= -z",  +(x)| +y<= -z);
    CHECK_AST(" +(x or  +y)<= -z",  +(x| +y)<= -z);
    CHECK_AST(" +x or ( +y)<= -z",  +x|( +y)<= -z);
    CHECK_AST(" +x or  +(y)<= -z",  +x| +(y)<= -z);
    CHECK_AST("( +x) or  +y<= not z", ( +x)| +y<= not z);
    CHECK_AST("( +x or  +y)<= not z", ( +x| +y)<= not z);
    CHECK_AST(" +(x) or  +y<= not z",  +(x)| +y<= not z);
    CHECK_AST(" +(x or  +y)<= not z",  +(x| +y)<= not z);
    CHECK_AST(" +x or ( +y)<= not z",  +x|( +y)<= not z);
    CHECK_AST(" +x or  +(y)<= not z",  +x| +(y)<= not z);
    CHECK_AST("( +x) or  -y<=z", ( +x)| -y<=z);
    CHECK_AST("( +x or  -y)<=z", ( +x| -y)<=z);
    CHECK_AST(" +(x) or  -y<=z",  +(x)| -y<=z);
    CHECK_AST(" +(x or  -y)<=z",  +(x| -y)<=z);
    CHECK_AST(" +x or ( -y)<=z",  +x|( -y)<=z);
    CHECK_AST(" +x or  -(y)<=z",  +x| -(y)<=z);
    CHECK_AST("( +x) or  -y<= +z", ( +x)| -y<= +z);
    CHECK_AST("( +x or  -y)<= +z", ( +x| -y)<= +z);
    CHECK_AST(" +(x) or  -y<= +z",  +(x)| -y<= +z);
    CHECK_AST(" +(x or  -y)<= +z",  +(x| -y)<= +z);
    CHECK_AST(" +x or ( -y)<= +z",  +x|( -y)<= +z);
    CHECK_AST(" +x or  -(y)<= +z",  +x| -(y)<= +z);
    CHECK_AST("( +x) or  -y<= -z", ( +x)| -y<= -z);
    CHECK_AST("( +x or  -y)<= -z", ( +x| -y)<= -z);
    CHECK_AST(" +(x) or  -y<= -z",  +(x)| -y<= -z);
    CHECK_AST(" +(x or  -y)<= -z",  +(x| -y)<= -z);
    CHECK_AST(" +x or ( -y)<= -z",  +x|( -y)<= -z);
    CHECK_AST(" +x or  -(y)<= -z",  +x| -(y)<= -z);
    CHECK_AST("( +x) or  -y<= not z", ( +x)| -y<= not z);
    CHECK_AST("( +x or  -y)<= not z", ( +x| -y)<= not z);
    CHECK_AST(" +(x) or  -y<= not z",  +(x)| -y<= not z);
    CHECK_AST(" +(x or  -y)<= not z",  +(x| -y)<= not z);
    CHECK_AST(" +x or ( -y)<= not z",  +x|( -y)<= not z);
    CHECK_AST(" +x or  -(y)<= not z",  +x| -(y)<= not z);
    CHECK_AST("( +x) or  not y<=z", ( +x)| not y<=z);
    CHECK_AST("( +x or  not y)<=z", ( +x| not y)<=z);
    CHECK_AST(" +(x) or  not y<=z",  +(x)| not y<=z);
    CHECK_AST(" +(x or  not y)<=z",  +(x| not y)<=z);
    CHECK_AST(" +x or ( not y)<=z",  +x|( not y)<=z);
    CHECK_AST(" +x or  not (y)<=z",  +x| not (y)<=z);
    CHECK_AST("( +x) or  not y<= +z", ( +x)| not y<= +z);
    CHECK_AST("( +x or  not y)<= +z", ( +x| not y)<= +z);
    CHECK_AST(" +(x) or  not y<= +z",  +(x)| not y<= +z);
    CHECK_AST(" +(x or  not y)<= +z",  +(x| not y)<= +z);
    CHECK_AST(" +x or ( not y)<= +z",  +x|( not y)<= +z);
    CHECK_AST(" +x or  not (y)<= +z",  +x| not (y)<= +z);
    CHECK_AST("( +x) or  not y<= -z", ( +x)| not y<= -z);
    CHECK_AST("( +x or  not y)<= -z", ( +x| not y)<= -z);
    CHECK_AST(" +(x) or  not y<= -z",  +(x)| not y<= -z);
    CHECK_AST(" +(x or  not y)<= -z",  +(x| not y)<= -z);
    CHECK_AST(" +x or ( not y)<= -z",  +x|( not y)<= -z);
    CHECK_AST(" +x or  not (y)<= -z",  +x| not (y)<= -z);
    CHECK_AST("( +x) or  not y<= not z", ( +x)| not y<= not z);
    CHECK_AST("( +x or  not y)<= not z", ( +x| not y)<= not z);
    CHECK_AST(" +(x) or  not y<= not z",  +(x)| not y<= not z);
    CHECK_AST(" +(x or  not y)<= not z",  +(x| not y)<= not z);
    CHECK_AST(" +x or ( not y)<= not z",  +x|( not y)<= not z);
    CHECK_AST(" +x or  not (y)<= not z",  +x| not (y)<= not z);
    CHECK_AST("( -x) or y<=z", ( -x)|y<=z);
    CHECK_AST("( -x or y)<=z", ( -x|y)<=z);
    CHECK_AST(" -(x) or y<=z",  -(x)|y<=z);
    CHECK_AST(" -(x or y)<=z",  -(x|y)<=z);
    CHECK_AST(" -x or (y)<=z",  -x|(y)<=z);
    CHECK_AST("( -x) or y<= +z", ( -x)|y<= +z);
    CHECK_AST("( -x or y)<= +z", ( -x|y)<= +z);
    CHECK_AST(" -(x) or y<= +z",  -(x)|y<= +z);
    CHECK_AST(" -(x or y)<= +z",  -(x|y)<= +z);
    CHECK_AST(" -x or (y)<= +z",  -x|(y)<= +z);
    CHECK_AST("( -x) or y<= -z", ( -x)|y<= -z);
    CHECK_AST("( -x or y)<= -z", ( -x|y)<= -z);
    CHECK_AST(" -(x) or y<= -z",  -(x)|y<= -z);
    CHECK_AST(" -(x or y)<= -z",  -(x|y)<= -z);
    CHECK_AST(" -x or (y)<= -z",  -x|(y)<= -z);
    CHECK_AST("( -x) or y<= not z", ( -x)|y<= not z);
    CHECK_AST("( -x or y)<= not z", ( -x|y)<= not z);
    CHECK_AST(" -(x) or y<= not z",  -(x)|y<= not z);
    CHECK_AST(" -(x or y)<= not z",  -(x|y)<= not z);
    CHECK_AST(" -x or (y)<= not z",  -x|(y)<= not z);
    CHECK_AST("( -x) or  +y<=z", ( -x)| +y<=z);
    CHECK_AST("( -x or  +y)<=z", ( -x| +y)<=z);
    CHECK_AST(" -(x) or  +y<=z",  -(x)| +y<=z);
    CHECK_AST(" -(x or  +y)<=z",  -(x| +y)<=z);
    CHECK_AST(" -x or ( +y)<=z",  -x|( +y)<=z);
    CHECK_AST(" -x or  +(y)<=z",  -x| +(y)<=z);
    CHECK_AST("( -x) or  +y<= +z", ( -x)| +y<= +z);
    CHECK_AST("( -x or  +y)<= +z", ( -x| +y)<= +z);
    CHECK_AST(" -(x) or  +y<= +z",  -(x)| +y<= +z);
    CHECK_AST(" -(x or  +y)<= +z",  -(x| +y)<= +z);
    CHECK_AST(" -x or ( +y)<= +z",  -x|( +y)<= +z);
    CHECK_AST(" -x or  +(y)<= +z",  -x| +(y)<= +z);
    CHECK_AST("( -x) or  +y<= -z", ( -x)| +y<= -z);
    CHECK_AST("( -x or  +y)<= -z", ( -x| +y)<= -z);
    CHECK_AST(" -(x) or  +y<= -z",  -(x)| +y<= -z);
    CHECK_AST(" -(x or  +y)<= -z",  -(x| +y)<= -z);
    CHECK_AST(" -x or ( +y)<= -z",  -x|( +y)<= -z);
    CHECK_AST(" -x or  +(y)<= -z",  -x| +(y)<= -z);
    CHECK_AST("( -x) or  +y<= not z", ( -x)| +y<= not z);
    CHECK_AST("( -x or  +y)<= not z", ( -x| +y)<= not z);
    CHECK_AST(" -(x) or  +y<= not z",  -(x)| +y<= not z);
    CHECK_AST(" -(x or  +y)<= not z",  -(x| +y)<= not z);
    CHECK_AST(" -x or ( +y)<= not z",  -x|( +y)<= not z);
    CHECK_AST(" -x or  +(y)<= not z",  -x| +(y)<= not z);
    CHECK_AST("( -x) or  -y<=z", ( -x)| -y<=z);
    CHECK_AST("( -x or  -y)<=z", ( -x| -y)<=z);
    CHECK_AST(" -(x) or  -y<=z",  -(x)| -y<=z);
    CHECK_AST(" -(x or  -y)<=z",  -(x| -y)<=z);
    CHECK_AST(" -x or ( -y)<=z",  -x|( -y)<=z);
    CHECK_AST(" -x or  -(y)<=z",  -x| -(y)<=z);
    CHECK_AST("( -x) or  -y<= +z", ( -x)| -y<= +z);
    CHECK_AST("( -x or  -y)<= +z", ( -x| -y)<= +z);
    CHECK_AST(" -(x) or  -y<= +z",  -(x)| -y<= +z);
    CHECK_AST(" -(x or  -y)<= +z",  -(x| -y)<= +z);
    CHECK_AST(" -x or ( -y)<= +z",  -x|( -y)<= +z);
    CHECK_AST(" -x or  -(y)<= +z",  -x| -(y)<= +z);
    CHECK_AST("( -x) or  -y<= -z", ( -x)| -y<= -z);
    CHECK_AST("( -x or  -y)<= -z", ( -x| -y)<= -z);
    CHECK_AST(" -(x) or  -y<= -z",  -(x)| -y<= -z);
    CHECK_AST(" -(x or  -y)<= -z",  -(x| -y)<= -z);
    CHECK_AST(" -x or ( -y)<= -z",  -x|( -y)<= -z);
    CHECK_AST(" -x or  -(y)<= -z",  -x| -(y)<= -z);
    CHECK_AST("( -x) or  -y<= not z", ( -x)| -y<= not z);
    CHECK_AST("( -x or  -y)<= not z", ( -x| -y)<= not z);
    CHECK_AST(" -(x) or  -y<= not z",  -(x)| -y<= not z);
    CHECK_AST(" -(x or  -y)<= not z",  -(x| -y)<= not z);
    CHECK_AST(" -x or ( -y)<= not z",  -x|( -y)<= not z);
    CHECK_AST(" -x or  -(y)<= not z",  -x| -(y)<= not z);
    CHECK_AST("( -x) or  not y<=z", ( -x)| not y<=z);
    CHECK_AST("( -x or  not y)<=z", ( -x| not y)<=z);
    CHECK_AST(" -(x) or  not y<=z",  -(x)| not y<=z);
    CHECK_AST(" -(x or  not y)<=z",  -(x| not y)<=z);
    CHECK_AST(" -x or ( not y)<=z",  -x|( not y)<=z);
    CHECK_AST(" -x or  not (y)<=z",  -x| not (y)<=z);
    CHECK_AST("( -x) or  not y<= +z", ( -x)| not y<= +z);
    CHECK_AST("( -x or  not y)<= +z", ( -x| not y)<= +z);
    CHECK_AST(" -(x) or  not y<= +z",  -(x)| not y<= +z);
    CHECK_AST(" -(x or  not y)<= +z",  -(x| not y)<= +z);
    CHECK_AST(" -x or ( not y)<= +z",  -x|( not y)<= +z);
    CHECK_AST(" -x or  not (y)<= +z",  -x| not (y)<= +z);
    CHECK_AST("( -x) or  not y<= -z", ( -x)| not y<= -z);
    CHECK_AST("( -x or  not y)<= -z", ( -x| not y)<= -z);
    CHECK_AST(" -(x) or  not y<= -z",  -(x)| not y<= -z);
    CHECK_AST(" -(x or  not y)<= -z",  -(x| not y)<= -z);
    CHECK_AST(" -x or ( not y)<= -z",  -x|( not y)<= -z);
    CHECK_AST(" -x or  not (y)<= -z",  -x| not (y)<= -z);
    CHECK_AST("( -x) or  not y<= not z", ( -x)| not y<= not z);
    CHECK_AST("( -x or  not y)<= not z", ( -x| not y)<= not z);
    CHECK_AST(" -(x) or  not y<= not z",  -(x)| not y<= not z);
    CHECK_AST(" -(x or  not y)<= not z",  -(x| not y)<= not z);
    CHECK_AST(" -x or ( not y)<= not z",  -x|( not y)<= not z);
    CHECK_AST(" -x or  not (y)<= not z",  -x| not (y)<= not z);
    CHECK_AST("( not x) or y<=z", ( not x)|y<=z);
    CHECK_AST("( not x or y)<=z", ( not x|y)<=z);
    CHECK_AST(" not (x) or y<=z",  not (x)|y<=z);
    CHECK_AST(" not (x or y)<=z",  not (x|y)<=z);
    CHECK_AST(" not x or (y)<=z",  not x|(y)<=z);
    CHECK_AST("( not x) or y<= +z", ( not x)|y<= +z);
    CHECK_AST("( not x or y)<= +z", ( not x|y)<= +z);
    CHECK_AST(" not (x) or y<= +z",  not (x)|y<= +z);
    CHECK_AST(" not (x or y)<= +z",  not (x|y)<= +z);
    CHECK_AST(" not x or (y)<= +z",  not x|(y)<= +z);
    CHECK_AST("( not x) or y<= -z", ( not x)|y<= -z);
    CHECK_AST("( not x or y)<= -z", ( not x|y)<= -z);
    CHECK_AST(" not (x) or y<= -z",  not (x)|y<= -z);
    CHECK_AST(" not (x or y)<= -z",  not (x|y)<= -z);
    CHECK_AST(" not x or (y)<= -z",  not x|(y)<= -z);
    CHECK_AST("( not x) or y<= not z", ( not x)|y<= not z);
    CHECK_AST("( not x or y)<= not z", ( not x|y)<= not z);
    CHECK_AST(" not (x) or y<= not z",  not (x)|y<= not z);
    CHECK_AST(" not (x or y)<= not z",  not (x|y)<= not z);
    CHECK_AST(" not x or (y)<= not z",  not x|(y)<= not z);
    CHECK_AST("( not x) or  +y<=z", ( not x)| +y<=z);
    CHECK_AST("( not x or  +y)<=z", ( not x| +y)<=z);
    CHECK_AST(" not (x) or  +y<=z",  not (x)| +y<=z);
    CHECK_AST(" not (x or  +y)<=z",  not (x| +y)<=z);
    CHECK_AST(" not x or ( +y)<=z",  not x|( +y)<=z);
    CHECK_AST(" not x or  +(y)<=z",  not x| +(y)<=z);
    CHECK_AST("( not x) or  +y<= +z", ( not x)| +y<= +z);
    CHECK_AST("( not x or  +y)<= +z", ( not x| +y)<= +z);
    CHECK_AST(" not (x) or  +y<= +z",  not (x)| +y<= +z);
    CHECK_AST(" not (x or  +y)<= +z",  not (x| +y)<= +z);
    CHECK_AST(" not x or ( +y)<= +z",  not x|( +y)<= +z);
    CHECK_AST(" not x or  +(y)<= +z",  not x| +(y)<= +z);
    CHECK_AST("( not x) or  +y<= -z", ( not x)| +y<= -z);
    CHECK_AST("( not x or  +y)<= -z", ( not x| +y)<= -z);
    CHECK_AST(" not (x) or  +y<= -z",  not (x)| +y<= -z);
    CHECK_AST(" not (x or  +y)<= -z",  not (x| +y)<= -z);
    CHECK_AST(" not x or ( +y)<= -z",  not x|( +y)<= -z);
    CHECK_AST(" not x or  +(y)<= -z",  not x| +(y)<= -z);
    CHECK_AST("( not x) or  +y<= not z", ( not x)| +y<= not z);
    CHECK_AST("( not x or  +y)<= not z", ( not x| +y)<= not z);
    CHECK_AST(" not (x) or  +y<= not z",  not (x)| +y<= not z);
    CHECK_AST(" not (x or  +y)<= not z",  not (x| +y)<= not z);
    CHECK_AST(" not x or ( +y)<= not z",  not x|( +y)<= not z);
    CHECK_AST(" not x or  +(y)<= not z",  not x| +(y)<= not z);
    CHECK_AST("( not x) or  -y<=z", ( not x)| -y<=z);
    CHECK_AST("( not x or  -y)<=z", ( not x| -y)<=z);
    CHECK_AST(" not (x) or  -y<=z",  not (x)| -y<=z);
    CHECK_AST(" not (x or  -y)<=z",  not (x| -y)<=z);
    CHECK_AST(" not x or ( -y)<=z",  not x|( -y)<=z);
    CHECK_AST(" not x or  -(y)<=z",  not x| -(y)<=z);
    CHECK_AST("( not x) or  -y<= +z", ( not x)| -y<= +z);
    CHECK_AST("( not x or  -y)<= +z", ( not x| -y)<= +z);
    CHECK_AST(" not (x) or  -y<= +z",  not (x)| -y<= +z);
    CHECK_AST(" not (x or  -y)<= +z",  not (x| -y)<= +z);
    CHECK_AST(" not x or ( -y)<= +z",  not x|( -y)<= +z);
    CHECK_AST(" not x or  -(y)<= +z",  not x| -(y)<= +z);
    CHECK_AST("( not x) or  -y<= -z", ( not x)| -y<= -z);
    CHECK_AST("( not x or  -y)<= -z", ( not x| -y)<= -z);
    CHECK_AST(" not (x) or  -y<= -z",  not (x)| -y<= -z);
    CHECK_AST(" not (x or  -y)<= -z",  not (x| -y)<= -z);
    CHECK_AST(" not x or ( -y)<= -z",  not x|( -y)<= -z);
    CHECK_AST(" not x or  -(y)<= -z",  not x| -(y)<= -z);
    CHECK_AST("( not x) or  -y<= not z", ( not x)| -y<= not z);
    CHECK_AST("( not x or  -y)<= not z", ( not x| -y)<= not z);
    CHECK_AST(" not (x) or  -y<= not z",  not (x)| -y<= not z);
    CHECK_AST(" not (x or  -y)<= not z",  not (x| -y)<= not z);
    CHECK_AST(" not x or ( -y)<= not z",  not x|( -y)<= not z);
    CHECK_AST(" not x or  -(y)<= not z",  not x| -(y)<= not z);
    CHECK_AST("( not x) or  not y<=z", ( not x)| not y<=z);
    CHECK_AST("( not x or  not y)<=z", ( not x| not y)<=z);
    CHECK_AST(" not (x) or  not y<=z",  not (x)| not y<=z);
    CHECK_AST(" not (x or  not y)<=z",  not (x| not y)<=z);
    CHECK_AST(" not x or ( not y)<=z",  not x|( not y)<=z);
    CHECK_AST(" not x or  not (y)<=z",  not x| not (y)<=z);
    CHECK_AST("( not x) or  not y<= +z", ( not x)| not y<= +z);
    CHECK_AST("( not x or  not y)<= +z", ( not x| not y)<= +z);
    CHECK_AST(" not (x) or  not y<= +z",  not (x)| not y<= +z);
    CHECK_AST(" not (x or  not y)<= +z",  not (x| not y)<= +z);
    CHECK_AST(" not x or ( not y)<= +z",  not x|( not y)<= +z);
    CHECK_AST(" not x or  not (y)<= +z",  not x| not (y)<= +z);
    CHECK_AST("( not x) or  not y<= -z", ( not x)| not y<= -z);
    CHECK_AST("( not x or  not y)<= -z", ( not x| not y)<= -z);
    CHECK_AST(" not (x) or  not y<= -z",  not (x)| not y<= -z);
    CHECK_AST(" not (x or  not y)<= -z",  not (x| not y)<= -z);
    CHECK_AST(" not x or ( not y)<= -z",  not x|( not y)<= -z);
    CHECK_AST(" not x or  not (y)<= -z",  not x| not (y)<= -z);
    CHECK_AST("( not x) or  not y<= not z", ( not x)| not y<= not z);
    CHECK_AST("( not x or  not y)<= not z", ( not x| not y)<= not z);
    CHECK_AST(" not (x) or  not y<= not z",  not (x)| not y<= not z);
    CHECK_AST(" not (x or  not y)<= not z",  not (x| not y)<= not z);
    CHECK_AST(" not x or ( not y)<= not z",  not x|( not y)<= not z);
    CHECK_AST(" not x or  not (y)<= not z",  not x| not (y)<= not z);
    CHECK_AST("(x) or y>z", (x)|y>z);
    CHECK_AST("(x or y)>z", (x|y)>z);
    CHECK_AST("x or (y)>z", x|(y)>z);
    CHECK_AST("(x) or y> +z", (x)|y> +z);
    CHECK_AST("(x or y)> +z", (x|y)> +z);
    CHECK_AST("x or (y)> +z", x|(y)> +z);
    CHECK_AST("(x) or y> -z", (x)|y> -z);
    CHECK_AST("(x or y)> -z", (x|y)> -z);
    CHECK_AST("x or (y)> -z", x|(y)> -z);
    CHECK_AST("(x) or y> not z", (x)|y> not z);
    CHECK_AST("(x or y)> not z", (x|y)> not z);
    CHECK_AST("x or (y)> not z", x|(y)> not z);
    CHECK_AST("(x) or  +y>z", (x)| +y>z);
    CHECK_AST("(x or  +y)>z", (x| +y)>z);
    CHECK_AST("x or ( +y)>z", x|( +y)>z);
    CHECK_AST("x or  +(y)>z", x| +(y)>z);
    CHECK_AST("(x) or  +y> +z", (x)| +y> +z);
    CHECK_AST("(x or  +y)> +z", (x| +y)> +z);
    CHECK_AST("x or ( +y)> +z", x|( +y)> +z);
    CHECK_AST("x or  +(y)> +z", x| +(y)> +z);
    CHECK_AST("(x) or  +y> -z", (x)| +y> -z);
    CHECK_AST("(x or  +y)> -z", (x| +y)> -z);
    CHECK_AST("x or ( +y)> -z", x|( +y)> -z);
    CHECK_AST("x or  +(y)> -z", x| +(y)> -z);
    CHECK_AST("(x) or  +y> not z", (x)| +y> not z);
    CHECK_AST("(x or  +y)> not z", (x| +y)> not z);
    CHECK_AST("x or ( +y)> not z", x|( +y)> not z);
    CHECK_AST("x or  +(y)> not z", x| +(y)> not z);
    CHECK_AST("(x) or  -y>z", (x)| -y>z);
    CHECK_AST("(x or  -y)>z", (x| -y)>z);
    CHECK_AST("x or ( -y)>z", x|( -y)>z);
    CHECK_AST("x or  -(y)>z", x| -(y)>z);
    CHECK_AST("(x) or  -y> +z", (x)| -y> +z);
    CHECK_AST("(x or  -y)> +z", (x| -y)> +z);
    CHECK_AST("x or ( -y)> +z", x|( -y)> +z);
    CHECK_AST("x or  -(y)> +z", x| -(y)> +z);
    CHECK_AST("(x) or  -y> -z", (x)| -y> -z);
    CHECK_AST("(x or  -y)> -z", (x| -y)> -z);
    CHECK_AST("x or ( -y)> -z", x|( -y)> -z);
    CHECK_AST("x or  -(y)> -z", x| -(y)> -z);
    CHECK_AST("(x) or  -y> not z", (x)| -y> not z);
    CHECK_AST("(x or  -y)> not z", (x| -y)> not z);
    CHECK_AST("x or ( -y)> not z", x|( -y)> not z);
    CHECK_AST("x or  -(y)> not z", x| -(y)> not z);
    CHECK_AST("(x) or  not y>z", (x)| not y>z);
    CHECK_AST("(x or  not y)>z", (x| not y)>z);
    CHECK_AST("x or ( not y)>z", x|( not y)>z);
    CHECK_AST("x or  not (y)>z", x| not (y)>z);
    CHECK_AST("(x) or  not y> +z", (x)| not y> +z);
    CHECK_AST("(x or  not y)> +z", (x| not y)> +z);
    CHECK_AST("x or ( not y)> +z", x|( not y)> +z);
    CHECK_AST("x or  not (y)> +z", x| not (y)> +z);
    CHECK_AST("(x) or  not y> -z", (x)| not y> -z);
    CHECK_AST("(x or  not y)> -z", (x| not y)> -z);
    CHECK_AST("x or ( not y)> -z", x|( not y)> -z);
    CHECK_AST("x or  not (y)> -z", x| not (y)> -z);
    CHECK_AST("(x) or  not y> not z", (x)| not y> not z);
    CHECK_AST("(x or  not y)> not z", (x| not y)> not z);
    CHECK_AST("x or ( not y)> not z", x|( not y)> not z);
    CHECK_AST("x or  not (y)> not z", x| not (y)> not z);
    CHECK_AST("( +x) or y>z", ( +x)|y>z);
    CHECK_AST("( +x or y)>z", ( +x|y)>z);
    CHECK_AST(" +(x) or y>z",  +(x)|y>z);
    CHECK_AST(" +(x or y)>z",  +(x|y)>z);
    CHECK_AST(" +x or (y)>z",  +x|(y)>z);
    CHECK_AST("( +x) or y> +z", ( +x)|y> +z);
    CHECK_AST("( +x or y)> +z", ( +x|y)> +z);
    CHECK_AST(" +(x) or y> +z",  +(x)|y> +z);
    CHECK_AST(" +(x or y)> +z",  +(x|y)> +z);
    CHECK_AST(" +x or (y)> +z",  +x|(y)> +z);
    CHECK_AST("( +x) or y> -z", ( +x)|y> -z);
    CHECK_AST("( +x or y)> -z", ( +x|y)> -z);
    CHECK_AST(" +(x) or y> -z",  +(x)|y> -z);
    CHECK_AST(" +(x or y)> -z",  +(x|y)> -z);
    CHECK_AST(" +x or (y)> -z",  +x|(y)> -z);
    CHECK_AST("( +x) or y> not z", ( +x)|y> not z);
    CHECK_AST("( +x or y)> not z", ( +x|y)> not z);
    CHECK_AST(" +(x) or y> not z",  +(x)|y> not z);
    CHECK_AST(" +(x or y)> not z",  +(x|y)> not z);
    CHECK_AST(" +x or (y)> not z",  +x|(y)> not z);
    CHECK_AST("( +x) or  +y>z", ( +x)| +y>z);
    CHECK_AST("( +x or  +y)>z", ( +x| +y)>z);
    CHECK_AST(" +(x) or  +y>z",  +(x)| +y>z);
    CHECK_AST(" +(x or  +y)>z",  +(x| +y)>z);
    CHECK_AST(" +x or ( +y)>z",  +x|( +y)>z);
    CHECK_AST(" +x or  +(y)>z",  +x| +(y)>z);
    CHECK_AST("( +x) or  +y> +z", ( +x)| +y> +z);
    CHECK_AST("( +x or  +y)> +z", ( +x| +y)> +z);

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