1 #ifndef LFSC_BOOL_PROOF_H_
2 #define LFSC_BOOL_PROOF_H_
23 void print_pf( std::ostream& s,
int ind = 0 );
48 void print_pf( std::ostream& s,
int ind = 0 ){ s <<
"(lem _ _ @a" <<
abs( d_var ) <<
")"; }
49 void print_struct( std::ostream& s,
int ind = 0 ){ s <<
"(lem " << d_var <<
")"; }
54 clause.push_back( -d_var );
55 clause.push_back( d_var );
73 void print_pf( std::ostream& s,
int ind = 0 );
74 void print_struct( std::ostream& s,
int ind = 0 ){ s <<
"(clausify " << d_var <<
")"; }
85 clause.push_back( d_var );
101 void print_pf( std::ostream& s,
int ind = 0 );
113 clause.push_back( -d_var );
void print_struct(std::ostream &s, int ind=0)
LFSCClausify(int v, LFSCProof *pf)
Data structure of expressions in CVC3.
LFSCBoolRes(LFSCProof *pf1, LFSCProof *pf2, int v, bool col)
int checkBoolRes(std::vector< int > &clause)
virtual LFSCLem * AsLFSCLem()
void print_pf(std::ostream &s, int ind=0)
long int get_string_length()
void print_struct(std::ostream &s, int ind=0)
LFSCAssume(int v, LFSCProof *pf, bool assm, int type)
void print_struct(std::ostream &s, int ind=0)
void print_pf(std::ostream &s, int ind=0)
int checkBoolRes(std::vector< int > &clause)
virtual LFSCAssume * AsLFSCAssume()
static LFSCProof * Make(LFSCProof *pf1, LFSCProof *pf2, int v, bool col)
static LFSCProof * Make_i(const Expr &e, LFSCProof *p, std::vector< Expr > &exprs, const Expr &end)
void print_pf(std::ostream &s, int ind=0)
virtual int checkBoolRes(std::vector< int > &clause)
void print_struct(std::ostream &s, int ind=0)
static LFSCProof * Make(int v, LFSCProof *pf)
RefPtr< LFSCProof > d_children[2]
virtual LFSCBoolRes * AsLFSCBoolRes()
void print_pf(std::ostream &s, int ind=0)
LFSCProof * getChild(int n)
int checkBoolRes(std::vector< int > &clause)
LFSCProof * getChild(int n)
int checkBoolRes(std::vector< int > &clause)
static LFSCProof * Make(int v)
LFSCProof * getChild(int n)
virtual LFSCClausify * AsLFSCClausify()
static LFSCProof * Make(int v, LFSCProof *pf, bool assm=true, int type=3)
static LFSCProof * MakeC(LFSCProof *p, const Expr &res)