CVC3  2.4.1
LFSCConvert.h
Go to the documentation of this file.
1 #ifndef LFSC_CONVERT_H_
2 #define LFSC_CONVERT_H_
3 
4 #include "TReturn.h"
5 
6 class LFSCConvert : public LFSCObj
7 {
8 private:
9  //the converted LFSCProof
11  // translations of proofs for cvc3_to_lfsc : if a proof has already been done,
12  // return the TReturn store for it
15  // these are the current TReturns we need to make into lambdas
16  std::map<TReturn*, bool> d_th_trans_lam[2];
17  //counts for theory/non-theory
18  int nodeCount;
22  //whether to ignore theory lemmas
24 
25  // other helper methods
26  bool isTrivialTheoryAxiom(const Expr& expr, bool checkBody = false );
27  bool isTrivialBooleanAxiom(const Expr& expr);
28  bool isIgnoredRule(const Expr& expr);
29 
30  // main method to implement T transformation:
31  // cvc3 proof syntax tree to lfsc proof syntax tree
32  // beneath_lc is whether you are beneath a learned clause
33  // rev_pol is whether you should prove ~psi2 V psi1 in the provesY = 2 case (reverse the implication)
34  TReturn* cvc3_to_lfsc(const Expr& pf, bool beneath_lc = false, bool rev_pol=false);
35  TReturn* cvc3_to_lfsc_h(const Expr& pf, bool beneath_lc = false, bool rev_pol=false);
36  //do basic subst op procedure
37  TReturn* do_bso( const Expr& pf, bool beneath_lc, bool rev_pol, TReturn* t1, TReturn* t2, ostringstream& ose );
38  //get proof type
39  int get_proof_pattern( const Expr& pf, Expr& modE );
40  //make the let proof
42  //make trusted
43  TReturn* make_trusted( const Expr& pf );
44 
45  virtual ~LFSCConvert(){}
46 public:
47  LFSCConvert( int lfscm );
48  //main conversion function
49  void convert( const Expr& pf );
50  //get the results
51  LFSCProof* getLFSCProof() { return pfinal.get(); }
52 };
53 
54 #endif
Data structure of expressions in CVC3.
Definition: expr.h:133
int unodeCount
Definition: LFSCConvert.h:20
bool ignore_theory_lemmas
Definition: LFSCConvert.h:23
ExprMap< bool > d_th_trans
Definition: LFSCConvert.h:13
LFSCProof * make_let_proof(LFSCProof *p)
int unodeCountTh
Definition: LFSCConvert.h:21
T * get()
Definition: Object.h:56
virtual ~LFSCConvert()
Definition: LFSCConvert.h:45
TReturn * cvc3_to_lfsc_h(const Expr &pf, bool beneath_lc=false, bool rev_pol=false)
TReturn * do_bso(const Expr &pf, bool beneath_lc, bool rev_pol, TReturn *t1, TReturn *t2, ostringstream &ose)
LFSCConvert(int lfscm)
Definition: LFSCConvert.cpp:9
int nodeCountTh
Definition: LFSCConvert.h:19
void convert(const Expr &pf)
Definition: LFSCConvert.cpp:18
RefPtr< LFSCProof > pfinal
Definition: LFSCConvert.h:10
bool isTrivialTheoryAxiom(const Expr &expr, bool checkBody=false)
Definition: LFSCConvert.cpp:57
bool isIgnoredRule(const Expr &expr)
Definition: LFSCConvert.cpp:86
TReturn * cvc3_to_lfsc(const Expr &pf, bool beneath_lc=false, bool rev_pol=false)
Definition: LFSCConvert.cpp:93
std::map< TReturn *, bool > d_th_trans_lam[2]
Definition: LFSCConvert.h:16
ExprMap< TReturn * > d_th_trans_map[2]
Definition: LFSCConvert.h:14
bool isTrivialBooleanAxiom(const Expr &expr)
Definition: LFSCConvert.cpp:79
TReturn * make_trusted(const Expr &pf)
int get_proof_pattern(const Expr &pf, Expr &modE)
LFSCProof * getLFSCProof()
Definition: LFSCConvert.h:51