16 std::vector <int>
d_L;
34 void getL( std::vector< int >& lget, std::vector< int >& lgetu );
39 bool hasFv() {
return !d_L_used.empty(); }
41 void calcL( std::vector< int >& lget, std::vector< int >& lgetu );
Data structure of expressions in CVC3.
Rational mult_rational(TReturn *lhs)
static int normalize_tr(const Expr &pf1, TReturn *&t1, int y, bool rev_pol=false, bool printErr=true)
void getL(std::vector< int > &lget, std::vector< int > &lgetu)
LFSCProof * getLFSCProof()
TReturn(LFSCProof *lfsc_pf, std::vector< int > &L, std::vector< int > &Lused, Rational r, bool hasR, int pvY)
std::vector< int > d_L_used
static int normalize_tret(const Expr &pf1, TReturn *&t1, const Expr &pf2, TReturn *&t2, bool rev_pol=false)
RefPtr< LFSCProof > d_lfsc_pf
static void normalize_to_tf(const Expr &pf, TReturn *&t1, int y)