1 #ifndef LFSC_LRA_PROOF_H_
2 #define LFSC_LRA_PROOF_H_
24 void print_pf( std::ostream& s,
int ind = 0 );
48 void print_pf( std::ostream& s,
int ind = 0 );
74 void print_pf( std::ostream& s,
int ind = 0 );
102 void print_pf( std::ostream& s,
int ind = 0 );
126 void print_pf( std::ostream& s,
int ind = 0 );
156 d_pf->
print( s, ind+1 );
static LFSCProof * MakeEq()
Data structure of expressions in CVC3.
LFSCProof * getChild(int n)
LFSCLraContra(LFSCProof *pf, int op)
static LFSCProof * Make(LFSCProof *pf1, LFSCProof *pf2, int op1, int op2)
virtual LFSCLraAdd * AsLFSCLraAdd()
void print_pf(std::ostream &s, int ind=0)
static LFSCProof * Make(LFSCProof *pf, int op)
void print_pf(std::ostream &s, int ind=0)
long int get_string_length()
LFSCProof * getChild(int n)
LFSCLraAdd(LFSCProof *pf1, LFSCProof *pf2, int op1, int op2)
LFSCLraAxiom(int op, Rational r)
LFSCLraSub(LFSCProof *pf1, LFSCProof *pf2, int op1, int op2)
virtual LFSCLraSub * AsLFSCLraSub()
int get_normalized(int knd, bool isnot)
LFSCProof * getChild(int n)
void print_pf(std::ostream &s, int ind=0)
LFSCLraPoly(LFSCProof *pf, int var, int op)
static LFSCProof * Make(Rational r, int op)
virtual LFSCLraAxiom * AsLFSCLraAxiom()
void print_pf(std::ostream &s, int ind=0)
void print_pf(std::ostream &s, int ind=0)
static LFSCProof * Make(LFSCProof *pf, Rational r, int op)
virtual LFSCLraContra * AsLFSCLraContra()
LFSCLraMulC(LFSCProof *pf, Rational r, int op)
string kind_to_str(int knd)
LFSCProof * getChild(int n)
static RefPtr< LFSCProof > eq
void print(std::ostream &s, int ind=0)
static LFSCProof * Make(LFSCProof *pf, int var, int op)
void print_pf(std::ostream &s, int ind=0)
static LFSCProof * Make(LFSCProof *pf1, LFSCProof *pf2, int op1, int op2)
RefPtr< LFSCProof > d_children[2]
RefPtr< LFSCProof > d_children[2]
int get_knd_result(int knd1, int knd2)
virtual LFSCLraMulC * AsLFSCLraMulC()
LFSCProof * getChild(int n)
virtual LFSCLraPoly * AsLFSCLraPoly()