1 #ifndef LFSC_CONVERT_H_
2 #define LFSC_CONVERT_H_
Data structure of expressions in CVC3.
bool ignore_theory_lemmas
ExprMap< bool > d_th_trans
LFSCProof * make_let_proof(LFSCProof *p)
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)
void convert(const Expr &pf)
RefPtr< LFSCProof > pfinal
bool isTrivialTheoryAxiom(const Expr &expr, bool checkBody=false)
bool isIgnoredRule(const Expr &expr)
TReturn * cvc3_to_lfsc(const Expr &pf, bool beneath_lc=false, bool rev_pol=false)
std::map< TReturn *, bool > d_th_trans_lam[2]
ExprMap< TReturn * > d_th_trans_map[2]
bool isTrivialBooleanAxiom(const Expr &expr)
TReturn * make_trusted(const Expr &pf)
int get_proof_pattern(const Expr &pf, Expr &modE)
LFSCProof * getLFSCProof()