CVC3
Functions

Util.cpp File Reference

#include "Util.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 DISTINCT, and EQ.

Referenced by LFSCPrinter::print_formula_h().

bool is_opposite ( int  knd)

Definition at line 66 of file Util.cpp.

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

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

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 DISTINCT, EQ, CVC3::GE, and CVC3::GT.

Referenced by LFSCLraAdd::Make().

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

Definition at line 111 of file Util.cpp.

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

Referenced by LFSCLraSub::checkOp(), and LFSCLraAdd::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_h ( const Expr e,
Expr pe,
const Expr pec,
bool  pecDef,
int  knd 
)

Definition at line 185 of file Util.cpp.

References CVC3::Expr::getKind().

Referenced by make_flatten_expr().

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().