CVC3
|
#include "Util.h"
Go to the source code of this file.
Functions | |
void | ajr_debug_print (const Expr &pf) |
string | kind_to_str (int knd) |
bool | is_eq_kind (int knd) |
bool | is_smt_kind (int knd) |
bool | is_opposite (int knd) |
bool | is_comparison (int knd) |
int | get_not (int knd) |
int | get_knd_order (int knd) |
int | get_normalized (int knd, bool isnot) |
int | get_knd_result (int knd1, int knd2) |
void | print_mpq (int num, int den, std::ostream &s) |
void | print_rational (const Rational &r, std::ostream &s) |
void | print_rational_divide (const Rational &n, const Rational &d, std::ostream &s) |
bool | getRat (const Expr &e, Rational &r) |
bool | isFlat (const Expr &e) |
void | make_flatten_expr_h (const Expr &e, Expr &pe, const Expr &pec, bool pecDef, int knd) |
void | make_flatten_expr (const Expr &e, Expr &pe, int knd) |
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 AND, DISTINCT, EQ, CVC3::GE, CVC3::GT, IFF, ITE, CVC3::LE, CVC3::LT, CVC3::MINUS, CVC3::MULT, NOT, OR, CVC3::PLUS, Obj::print_error(), and CVC3::UMINUS.
Referenced by LFSCConvert::cvc3_to_lfsc(), LFSCConvert::do_bso(), get_knd_result(), LFSCPrinter::print_formula_h(), LFSCPrinter::print_LFSC(), LFSCLraAdd::print_pf(), LFSCLraAxiom::print_pf(), LFSCLraMulC::print_pf(), LFSCLraSub::print_pf(), LFSCLraPoly::print_pf(), LFSCLraContra::print_pf(), LFSCPrinter::print_poly_norm(), and LFSCPrinter::print_terms_h().
bool is_eq_kind | ( | int | knd | ) |
Definition at line 47 of file Util.cpp.
References DISTINCT, EQ, CVC3::GE, CVC3::GT, CVC3::LE, and CVC3::LT.
Referenced by LFSCObj::can_pnorm(), LFSCObj::collect_vars(), LFSCConvert::cvc3_to_lfsc(), LFSCConvert::do_bso(), LFSCObj::getY(), LFSCObj::isFormula(), LFSCLraPoly::Make(), TReturn::normalize_tr(), LFSCPrinter::print_formula_h(), LFSCObj::queryAtomic(), and LFSCObj::what_is_proven().
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 DISTINCT, CVC3::LE, and CVC3::LT.
Referenced by LFSCConvert::do_bso(), LFSCObj::getY(), and LFSCLraPoly::Make().
bool is_comparison | ( | int | knd | ) |
Definition at line 70 of file Util.cpp.
References CVC3::GE, CVC3::GT, CVC3::LE, and CVC3::LT.
Referenced by LFSCConvert::cvc3_to_lfsc(), LFSCObj::getY(), TReturn::normalize_to_tf(), and TReturn::normalize_tr().
int get_not | ( | int | knd | ) |
Definition at line 75 of file Util.cpp.
References DISTINCT, EQ, CVC3::GE, CVC3::GT, CVC3::LE, and CVC3::LT.
Referenced by LFSCConvert::cvc3_to_lfsc(), get_normalized(), LFSCLraPoly::print_pf(), LFSCObj::queryAtomic(), and LFSCObj::what_is_proven().
int get_knd_order | ( | int | knd | ) |
int get_normalized | ( | int | knd, |
bool | isnot | ||
) |
Definition at line 100 of file Util.cpp.
References CVC3::GE, get_normalized(), get_not(), CVC3::GT, CVC3::LE, and CVC3::LT.
Referenced by LFSCLraPoly::checkOp(), LFSCConvert::cvc3_to_lfsc(), get_normalized(), LFSCObj::getY(), LFSCLraPoly::Make(), TReturn::normalize_to_tf(), TReturn::normalize_tr(), and LFSCLraPoly::print_pf().
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 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().
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::DIVIDE, CVC3::Expr::getKind(), getRat(), CVC3::Expr::getRational(), CVC3::Expr::isRational(), and CVC3::UMINUS.
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().