Util.cpp File Reference

#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)

---

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

)

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(), LFSCLraContra::print_pf(), LFSCLraPoly::print_pf(), LFSCLraSub::print_pf(), LFSCLraMulC::print_pf(), LFSCLraAxiom::print_pf(), LFSCLraAdd::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.

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

)

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

)

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
	)

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

Definition at line 136 of file Util.cpp.

Referenced by LFSCConvert::cvc3_to_lfsc(), LFSCLraMulC::print_pf(), LFSCLraAxiom::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().

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

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

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