module lang::smtlib2::theory::core::Ast

rascal-0.40.16

Synopsis: AST for the SMTLIBv2 Core theory (boolean logic).

Usage

import lang::smtlib2::theory::core::Ast;

data Sort

data Sort  
     = \bool()
     ;

data Expr

data Expr  
     = \not(Expr val)
     | implies(Expr lhs, Expr rhs)
     | and(Expr lhs, Expr rhs)
     | or(Expr lhs, Expr rhs)
     | xor(Expr lhs, Expr rhs)
     | eq(Expr lhs, Expr rhs)
     | distinct(Expr lhs, Expr rhs)
     | ite(Expr condition, Expr whenTrue, Expr whenFalse)
     ;

data Literal

data Literal  
     = boolVal(bool b)
     ;