CVC3
LFSCObject.h
Go to the documentation of this file.
1 #ifndef LFSC_OBJ_H_
2 #define LFSC_OBJ_H_
3 
4 #include "Object.h"
5 #include "Util.h"
6 
7 class LFSCPrinter;
8 
9 class LFSCObj : public Obj
10 {
11 public:
12  LFSCObj(){}
13  static void initialize( const Expr& pf_expr, int lfscm );
14 protected:
15  //the printer object
17  //counters
18  static int formula_i;
19  static int trusted_i;
20  static int term_i;
21  static int tnorm_i;
22  //options for the conversion
23  static int lfsc_mode;
24  static bool debug_conv;
25  static bool debug_var;
26  static bool cvc3_mimic;
27  static bool cvc3_mimic_input;
28  //null rational
29  static Rational nullRat;
30  //get number of nodes
32  static int getNumNodes( const Expr& pf, bool recount = false );
33  //cascade expr
35  static Expr cascade_expr( const Expr& e );
36  //skolem variables
37  static ExprMap< Expr > skolem_vars; //with the expr they point to
39  static void define_skolem_vars( const Expr& e );
40  //is variable
41  static bool isVar( const Expr& e );
42  //collect free variables
43  static void collect_vars( const Expr& e, bool readPred = true );
44 protected:
45  // this is actually the M map <formula, int> where M = {v_i -> non-negated formula}
47  //trusted formulas
49  // this is the M_t map <term, int> where M_t = { v_i -> term }
51  //this is the equations that will use the d_pn map. They are mapped to the index of the pn_i they will use
53  //similar to m, but with terms
55  //input variables
57  //input predicates
59  //pnt that are needed to print
60  static std::map< int, bool > pntNeeded;
61  //atoms that must be printed
63  //original proof expression
64  static Expr d_pf_expr;
65  //assumptions
67 protected:
68  //eliminate not not
69  static Expr queryElimNotNot(const Expr& expr);
70  //get base will get you the base formula, i.e. ~( a = b ) returns ( a = b )
71  //get base = false will get you the equivalent atomic, i.e. ~( a = b ) returns ( b != a )
72  static Expr queryAtomic(const Expr& expr, bool getBase = false );
73  //returns a integer v, +v means M( v ) = expr, -v means M( v ) = expr', where expr := NOT expr'
74  //add is whether or not to add it to M, or just query
75  static int queryM(const Expr& expr, bool add = true, bool trusted = false);
76  //returns an integer v, where M_t( v ) = expr
77  static int queryMt(const Expr& expr);
78  //similar to m, but this time it is with terms
79  static int queryT( const Expr& e );
80  //get Y
81  static bool getY( const Expr& e, Expr& pe, bool doIff = true, bool doLogic = true );
82  //is this expr a formula
83  static bool isFormula( const Expr& e );
84  //can this expr be polynomial normalized
85  static bool can_pnorm( const Expr& e );
86  //what is proven
87  static bool what_is_proven( const Expr& pf, Expr& pe );
88 protected:
89  // differentiate between variables and rules
91  // boolean resultion rules
94  // arithmetic rules
107  static Expr d_refl_str;
150  static Expr d_andE_str;
153  //CNF rules
154  static Expr d_CNF_str;
157  //reasons for CNF
160  static Expr d_ite_s;
161  static Expr d_iff_s;
162  static Expr d_imp_s;
163  static Expr d_or_mid_s;
165 };
166 
167 #endif