39 std::vector< int >
br;
64 if( lambdaMap[p]==0 ){
70 void print( std::ostream& s,
int ind = 0 );
71 virtual void print_pf( std::ostream& s,
int ind = 0 )=0;
87 static int psCounter = 0;
88 s <<
"P" << psCounter;
94 void calcL( std::vector< int >& lget, std::vector< int >& lgetu );
void print_structure(std::ostream &s, int ind=0)
Data structure of expressions in CVC3.
virtual int getNumChildren()
long int get_string_length()
static LFSCProof * Make_CNF(const Expr &form, const Expr &reason, int pos)
virtual LFSCLraMulC * AsLFSCLraMulC()
virtual long int get_length()
virtual LFSCLraPoly * AsLFSCLraPoly()
virtual LFSCClausify * AsLFSCClausify()
virtual LFSCBoolRes * AsLFSCBoolRes()
virtual LFSCPfLet * AsLFSCPfLet()
static int get_proof_counter()
static std::map< LFSCProof *, LFSCProof * > lambdaPrintMap
virtual LFSCAssume * AsLFSCAssume()
static LFSCProof * Make_and_elim(const Expr &form, LFSCProof *p, int n, const Expr &expected)
virtual LFSCPfVar * AsLFSCPfVar()
virtual int checkBoolRes(std::vector< int > &clause)
virtual LFSCPfLambda * AsLFSCPfLambda()
virtual void print_struct(std::ostream &s, int ind=0)
virtual LFSCProof * clone()=0
virtual LFSCProof * getChild(int n)
void print(std::ostream &s, int ind=0)
virtual LFSCLraSub * AsLFSCLraSub()
virtual LFSCProofGeneric * AsLFSCProofGeneric()
virtual LFSCProofExpr * AsLFSCProofExpr()
virtual LFSCLraAxiom * AsLFSCLraAxiom()
virtual void print_pf(std::ostream &s, int ind=0)=0
static LFSCProof * Make_not_not_elim(const Expr &pf, LFSCProof *p)
virtual LFSCLraContra * AsLFSCLraContra()
static std::map< LFSCProof *, int > lambdaMap
static int make_lambda(LFSCProof *p)
void setRplProof(LFSCProof *p)
virtual LFSCLem * AsLFSCLem()
static LFSCProof * Make_mimic(const Expr &pf, LFSCProof *p, int numHoles)
virtual LFSCLraAdd * AsLFSCLraAdd()