CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
search
Util.h
Go to the documentation of this file.
1
#ifndef UTIL_H_
2
#define UTIL_H_
3
4
#include "
Object.h
"
5
6
// helper utility functions
7
void
ajr_debug_print
(
const
Expr
& pf );
8
string
kind_to_str
(
int
knd );
9
bool
is_eq_kind
(
int
knd );
10
bool
is_smt_kind
(
int
knd );
11
12
//equation types ( a ~ b ) that are normalized to (b-a) ~' 0
13
bool
is_opposite
(
int
knd );
14
bool
is_comparison
(
int
knd );
15
int
get_not
(
int
knd );
16
17
//order in LFSC signature for rules when order does not matter (such as lra_add)
18
int
get_knd_order
(
int
knd );
19
int
get_normalized
(
int
knd,
bool
isnot =
false
);
20
21
//should only be called on normalized ops
22
int
get_knd_result
(
int
knd1,
int
knd2 );
23
24
//print helpers
25
void
print_mpq
(
int
num,
int
den, std::ostream& s );
26
void
print_rational
(
const
Rational
& r, std::ostream& s );
27
void
print_rational_divide
(
const
Rational
& n,
const
Rational
& d, std::ostream& s );
28
29
bool
getRat
(
const
Expr
& e,
Rational
& r );
30
bool
isFlat
(
const
Expr
& e );
31
void
make_flatten_expr
(
const
Expr
& e,
Expr
& pe,
int
knd );
32
33
#endif
Generated on Mon Aug 6 2012 09:40:09 for CVC3 by
1.8.1.1