CVC3
2.4.1
|
#include "Util.h"
Go to the source code of this file.
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 | ) |
Definition at line 17 of file Util.cpp.
References EQ, CVC3::LE, CVC3::LT, CVC3::GE, CVC3::GT, DISTINCT, CVC3::PLUS, CVC3::MINUS, CVC3::MULT, AND, OR, NOT, ITE, IFF, CVC3::UMINUS, and Obj::print_error().
Referenced by LFSCConvert::cvc3_to_lfsc(), LFSCConvert::do_bso(), LFSCLraAdd::print_pf(), LFSCLraAxiom::print_pf(), LFSCLraMulC::print_pf(), LFSCLraSub::print_pf(), LFSCLraPoly::print_pf(), LFSCLraContra::print_pf(), LFSCPrinter::print_LFSC(), LFSCPrinter::print_poly_norm(), LFSCPrinter::print_terms_h(), LFSCPrinter::print_formula_h(), and get_knd_result().
bool is_eq_kind | ( | int | knd | ) |
Definition at line 47 of file Util.cpp.
References EQ, CVC3::LE, CVC3::LT, CVC3::GE, CVC3::GT, and DISTINCT.
Referenced by LFSCConvert::cvc3_to_lfsc(), LFSCConvert::do_bso(), LFSCLraPoly::Make(), LFSCObj::collect_vars(), LFSCObj::queryAtomic(), LFSCObj::getY(), LFSCObj::isFormula(), LFSCObj::can_pnorm(), LFSCObj::what_is_proven(), LFSCPrinter::print_formula_h(), and TReturn::normalize_tr().
bool is_smt_kind | ( | int | knd | ) |
Definition at line 60 of file Util.cpp.
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 | ) |
Definition at line 70 of file Util.cpp.
References CVC3::LE, CVC3::LT, CVC3::GE, and CVC3::GT.
Referenced by LFSCConvert::cvc3_to_lfsc(), LFSCObj::getY(), TReturn::normalize_tr(), and TReturn::normalize_to_tf().
int get_not | ( | int | knd | ) |
Definition at line 75 of file Util.cpp.
References EQ, DISTINCT, CVC3::LE, CVC3::GT, CVC3::LT, and CVC3::GE.
Referenced by LFSCConvert::cvc3_to_lfsc(), LFSCLraPoly::print_pf(), LFSCObj::queryAtomic(), LFSCObj::what_is_proven(), and get_normalized().
int get_knd_order | ( | int | knd | ) |
int get_normalized | ( | int | knd, |
bool | isnot | ||
) |
Definition at line 100 of file Util.cpp.
References get_normalized(), get_not(), CVC3::LE, CVC3::GE, CVC3::LT, and CVC3::GT.
Referenced by LFSCConvert::cvc3_to_lfsc(), LFSCLraPoly::print_pf(), LFSCLraPoly::Make(), LFSCLraPoly::checkOp(), LFSCObj::getY(), TReturn::normalize_tr(), TReturn::normalize_to_tf(), and get_normalized().
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 | ||
) |
Definition at line 136 of file Util.cpp.
Referenced by LFSCConvert::cvc3_to_lfsc(), LFSCLraAxiom::print_pf(), LFSCLraMulC::print_pf(), LFSCPrinter::print_poly_norm(), and LFSCPrinter::print_terms_h().
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().
Definition at line 158 of file Util.cpp.
References CVC3::Expr::isRational(), CVC3::Expr::getRational(), CVC3::Expr::getKind(), CVC3::DIVIDE, CVC3::UMINUS, and getRat().
Referenced by LFSCConvert::cvc3_to_lfsc(), LFSCConvert::do_bso(), and getRat().
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().
Definition at line 185 of file Util.cpp.
References CVC3::Expr::getKind().
Referenced by make_flatten_expr().
Definition at line 203 of file Util.cpp.
References make_flatten_expr_h().
Referenced by LFSCConvert::cvc3_to_lfsc().