CVC3  2.4.1
Functions
Util.h File Reference
#include "Object.h"

Go to the source code of this file.

Functions


Function Documentation

void ajr_debug_print ( const Expr pf)

Definition at line 8 of file Util.cpp.

References CVC3::Expr::arity(), and CVC3::Expr::print().

string kind_to_str ( int  knd)
bool is_eq_kind ( int  knd)
bool is_smt_kind ( int  knd)

Definition at line 60 of file Util.cpp.

References EQ, and DISTINCT.

Referenced by LFSCPrinter::print_formula_h().

bool is_opposite ( int  knd)

Definition at line 66 of file Util.cpp.

References CVC3::LE, CVC3::LT, and DISTINCT.

Referenced by LFSCConvert::do_bso(), LFSCLraPoly::Make(), and LFSCObj::getY().

bool is_comparison ( int  knd)
int get_not ( int  knd)
int get_knd_order ( int  knd)

Definition at line 89 of file Util.cpp.

References EQ, CVC3::GT, CVC3::GE, and DISTINCT.

Referenced by LFSCLraAdd::Make().

int get_normalized ( int  knd,
bool  isnot = false 
)
int get_knd_result ( int  knd1,
int  knd2 
)

Definition at line 111 of file Util.cpp.

References EQ, DISTINCT, CVC3::GT, CVC3::GE, kind_to_str(), std::endl(), and Obj::print_error().

Referenced by LFSCLraAdd::checkOp(), and LFSCLraSub::checkOp().

void print_mpq ( int  num,
int  den,
std::ostream s 
)

Definition at line 127 of file Util.cpp.

References CVC3::abs().

void print_rational ( const Rational r,
std::ostream s 
)
void print_rational_divide ( const Rational n,
const Rational d,
std::ostream s 
)

Definition at line 149 of file Util.cpp.

Referenced by LFSCPrinter::print_poly_norm(), and LFSCPrinter::print_terms_h().

bool getRat ( const Expr e,
Rational r 
)
bool isFlat ( const Expr e)

Definition at line 173 of file Util.cpp.

References CVC3::Expr::arity(), CVC3::Expr::getKind(), and isFlat().

Referenced by LFSCConvert::cvc3_to_lfsc(), and isFlat().

void make_flatten_expr ( const Expr e,
Expr pe,
int  knd 
)

Definition at line 203 of file Util.cpp.

References make_flatten_expr_h().

Referenced by LFSCConvert::cvc3_to_lfsc().