check_ast_ad.cpp

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

void check_ast_ad(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>=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);
    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);
    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_ad: " << good << " out of " << total
        << " (" << std::setprecision(1) << std::fixed << (100.0*good/total) << "%)\n";
}