CVC3  2.4.1
LFSCProof.h
Go to the documentation of this file.
1 #ifndef LFSC_PROOF_H_
2 #define LFSC_PROOF_H_
3 
4 #include "LFSCObject.h"
5 
6 //////////////////////////////////
7 /// LFSC Proof Class & subclasses
8 //////////////////////////////////
9 
10 class LFSCProofExpr;
11 class LFSCLraAdd;
12 class LFSCLraSub;
13 class LFSCLraMulC;
14 class LFSCLraAxiom;
15 class LFSCLraContra;
16 class LFSCLraPoly;
17 class LFSCBoolRes;
18 class LFSCLem;
19 class LFSCClausify;
20 class LFSCAssume;
21 class LFSCProofGeneric;
22 class LFSCPfVar;
23 class LFSCPfLambda;
24 class LFSCPfLet;
25 
26 class LFSCProof : public LFSCObj{
27 protected:
28  static int pf_counter;
29  static std::map< LFSCProof*, int > lambdaMap;
30  static std::map< LFSCProof*, LFSCProof* > lambdaPrintMap;
33  static int lambdaCounter;
34  long int strLen;
35  int chOp;
36  int assumeVar;
38 
39  std::vector< int > br;
40  bool brComputed;
41 
42  LFSCProof();
43  virtual long int get_length() { return 0; }
44  virtual ~LFSCProof(){}
45 public:
46  virtual LFSCProofExpr* AsLFSCProofExpr(){ return NULL; }
47  virtual LFSCLraAdd* AsLFSCLraAdd(){ return NULL; }
48  virtual LFSCLraSub* AsLFSCLraSub(){ return NULL; }
49  virtual LFSCLraMulC* AsLFSCLraMulC(){ return NULL; }
50  virtual LFSCLraAxiom* AsLFSCLraAxiom(){ return NULL; }
51  virtual LFSCLraContra* AsLFSCLraContra(){ return NULL; }
52  virtual LFSCLraPoly* AsLFSCLraPoly(){ return NULL; }
53  virtual LFSCBoolRes* AsLFSCBoolRes(){ return NULL; }
54  virtual LFSCLem* AsLFSCLem(){ return NULL; }
55  virtual LFSCClausify* AsLFSCClausify(){ return NULL; }
56  virtual LFSCAssume* AsLFSCAssume(){ return NULL; }
57  virtual LFSCProofGeneric* AsLFSCProofGeneric(){ return NULL; }
58  virtual LFSCPfVar* AsLFSCPfVar(){ return NULL; }
59  virtual LFSCPfLambda* AsLFSCPfLambda(){ return NULL; }
60  virtual LFSCPfLet* AsLFSCPfLet(){ return NULL; }
61 
62  virtual bool isLraMulC() { return false; }
63  static int make_lambda( LFSCProof* p ){
64  if( lambdaMap[p]==0 ){
66  lambdaCounter++;
67  }
68  return lambdaMap[p];
69  }
70  void print( std::ostream& s, int ind = 0 );
71  virtual void print_pf( std::ostream& s, int ind = 0 )=0;
72  virtual bool isTrivial() { return false; }
73  long int get_string_length() {
74  if( strLen<0 ){
75  strLen = get_length();
76  //to prevent overflow
77  for( int a=0; a<getNumChildren(); a++ ){
78  if( strLen<getChild( a )->get_string_length() ){
80  }
81  }
82  }
83  return strLen;
84  }
85  void print_structure( std::ostream& s, int ind = 0 );
86  virtual void print_struct( std::ostream& s, int ind = 0 ){
87  static int psCounter = 0;
88  s << "P" << psCounter;
89  psCounter++;
90  }
91  void setRplProof( LFSCProof* p ) { rplProof = p; }
92  virtual void fillHoles();
93 #ifdef OPTIMIZE
94  void calcL( std::vector< int >& lget, std::vector< int >& lgetu );
95 #endif
96 
97  friend class LFSCPrinter;
98 
99  virtual LFSCProof* clone() = 0;
100  virtual int getNumChildren() { return 0; }
101  virtual LFSCProof* getChild( int n ) { return NULL; }
102  virtual int checkOp();
103  int getChOp(){ return chOp; }
104  void setChOp( int c ) { chOp = c; }
105  virtual int checkBoolRes( std::vector< int >& clause ){ return 0; }
106 
107 //proof making methods
108 public:
109  static LFSCProof* Make_CNF( const Expr& form, const Expr& reason, int pos );
110  static LFSCProof* Make_not_not_elim( const Expr& pf, LFSCProof* p );
111  static LFSCProof* Make_mimic( const Expr& pf, LFSCProof* p, int numHoles );
112  static LFSCProof* Make_and_elim( const Expr& form, LFSCProof* p, int n, const Expr& expected );
113 
114  static int get_proof_counter() { return pf_counter; }
115 };
116 
117 
118 #endif
void print_structure(std::ostream &s, int ind=0)
Definition: LFSCProof.cpp:43
Data structure of expressions in CVC3.
Definition: expr.h:133
static int pf_counter
Definition: LFSCProof.h:28
virtual bool isTrivial()
Definition: LFSCProof.h:72
virtual int getNumChildren()
Definition: LFSCProof.h:100
long int get_string_length()
Definition: LFSCProof.h:73
int chOp
Definition: LFSCProof.h:35
virtual bool isLraMulC()
Definition: LFSCProof.h:62
static LFSCProof * Make_CNF(const Expr &form, const Expr &reason, int pos)
Definition: LFSCProof.cpp:104
int assumeVar
Definition: LFSCProof.h:36
virtual LFSCLraMulC * AsLFSCLraMulC()
Definition: LFSCProof.h:49
virtual long int get_length()
Definition: LFSCProof.h:43
virtual LFSCLraPoly * AsLFSCLraPoly()
Definition: LFSCProof.h:52
virtual LFSCClausify * AsLFSCClausify()
Definition: LFSCProof.h:55
virtual LFSCBoolRes * AsLFSCBoolRes()
Definition: LFSCProof.h:53
virtual LFSCPfLet * AsLFSCPfLet()
Definition: LFSCProof.h:60
long int strLen
Definition: LFSCProof.h:34
bool brComputed
Definition: LFSCProof.h:40
static int get_proof_counter()
Definition: LFSCProof.h:114
static std::map< LFSCProof *, LFSCProof * > lambdaPrintMap
Definition: LFSCProof.h:30
virtual LFSCAssume * AsLFSCAssume()
Definition: LFSCProof.h:56
static LFSCProof * Make_and_elim(const Expr &form, LFSCProof *p, int n, const Expr &expected)
Definition: LFSCProof.cpp:397
int printCounter
Definition: LFSCProof.h:31
virtual ~LFSCProof()
Definition: LFSCProof.h:44
virtual LFSCPfVar * AsLFSCPfVar()
Definition: LFSCProof.h:58
virtual int checkBoolRes(std::vector< int > &clause)
Definition: LFSCProof.h:105
virtual LFSCPfLambda * AsLFSCPfLambda()
Definition: LFSCProof.h:59
std::vector< int > br
Definition: LFSCProof.h:39
virtual void print_struct(std::ostream &s, int ind=0)
Definition: LFSCProof.h:86
virtual void fillHoles()
Definition: LFSCProof.cpp:61
static int lambdaCounter
Definition: LFSCProof.h:33
virtual LFSCProof * clone()=0
virtual LFSCProof * getChild(int n)
Definition: LFSCProof.h:101
LFSCProof * rplProof
Definition: LFSCProof.h:32
void print(std::ostream &s, int ind=0)
Definition: LFSCProof.cpp:23
virtual LFSCLraSub * AsLFSCLraSub()
Definition: LFSCProof.h:48
virtual LFSCProofGeneric * AsLFSCProofGeneric()
Definition: LFSCProof.h:57
virtual LFSCProofExpr * AsLFSCProofExpr()
Definition: LFSCProof.h:46
virtual LFSCLraAxiom * AsLFSCLraAxiom()
Definition: LFSCProof.h:50
virtual void print_pf(std::ostream &s, int ind=0)=0
static LFSCProof * Make_not_not_elim(const Expr &pf, LFSCProof *p)
Definition: LFSCProof.cpp:372
int assumeVarUsed
Definition: LFSCProof.h:37
virtual int checkOp()
Definition: LFSCProof.cpp:83
virtual LFSCLraContra * AsLFSCLraContra()
Definition: LFSCProof.h:51
void setChOp(int c)
Definition: LFSCProof.h:104
static std::map< LFSCProof *, int > lambdaMap
Definition: LFSCProof.h:29
static int make_lambda(LFSCProof *p)
Definition: LFSCProof.h:63
void setRplProof(LFSCProof *p)
Definition: LFSCProof.h:91
virtual LFSCLem * AsLFSCLem()
Definition: LFSCProof.h:54
static LFSCProof * Make_mimic(const Expr &pf, LFSCProof *p, int numHoles)
Definition: LFSCProof.cpp:384
virtual LFSCLraAdd * AsLFSCLraAdd()
Definition: LFSCProof.h:47
int getChOp()
Definition: LFSCProof.h:103