CVC3  2.4.1
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
static Expr d_right_minus_left_str
Definition: LFSCObject.h:103
static int tnorm_i
Definition: LFSCObject.h:21
static Expr d_or_final_s
Definition: LFSCObject.h:158
static Expr d_cnf_convert_str
Definition: LFSCObject.h:108
static ExprMap< bool > d_formulas_printed
Definition: LFSCObject.h:62
Data structure of expressions in CVC3.
Definition: expr.h:133
static Expr d_andE_str
Definition: LFSCObject.h:150
static std::map< int, bool > pntNeeded
Definition: LFSCObject.h:60
static ExprMap< bool > temp_visited
Definition: LFSCObject.h:38
static Expr d_CNF_str
Definition: LFSCObject.h:154
static void define_skolem_vars(const Expr &e)
Definition: LFSCObject.cpp:308
static bool cvc3_mimic_input
Definition: LFSCObject.h:27
static Expr d_mult_ineqn_str
Definition: LFSCObject.h:102
static Expr d_rewrite_not_not_str
Definition: LFSCObject.h:136
static Expr cascade_expr(const Expr &e)
Definition: LFSCObject.cpp:281
static Expr d_iff_true_elim_str
Definition: LFSCObject.h:115
static Expr d_canon_mult_str
Definition: LFSCObject.h:118
static Expr d_ite_s
Definition: LFSCObject.h:160
static ExprMap< bool > d_assump_map
Definition: LFSCObject.h:66
static Expr d_not_to_iff_str
Definition: LFSCObject.h:133
static Expr d_rewrite_not_true_str
Definition: LFSCObject.h:137
static int queryM(const Expr &expr, bool add=true, bool trusted=false)
Definition: LFSCObject.cpp:386
static Expr d_mult_eqn_str
Definition: LFSCObject.h:121
static Expr d_iff_not_false_str
Definition: LFSCObject.h:130
LFSCObj()
Definition: LFSCObject.h:12
static Expr d_const_predicate_str
Definition: LFSCObject.h:135
static Expr d_rewrite_and_str
Definition: LFSCObject.h:128
static Expr d_lessThan_To_LE_rhs_rwr_str
Definition: LFSCObject.h:148
static Expr d_CNFITE_str
Definition: LFSCObject.h:140
static void initialize()
Definition: Object.h:111
static int queryT(const Expr &e)
Definition: LFSCObject.cpp:436
static bool cvc3_mimic
Definition: LFSCObject.h:26
static int queryMt(const Expr &expr)
Definition: LFSCObject.cpp:418
static Expr d_assump_str
Definition: LFSCObject.h:93
static Expr d_minus_to_plus_str
Definition: LFSCObject.h:110
static int lfsc_mode
Definition: LFSCObject.h:23
static Expr d_or_mid_s
Definition: LFSCObject.h:163
static Expr d_iff_false_str
Definition: LFSCObject.h:131
static Expr d_var_intro_str
Definition: LFSCObject.h:141
static Expr d_plus_predicate_str
Definition: LFSCObject.h:111
static Expr d_iff_true_str
Definition: LFSCObject.h:120
Definition: Object.h:63
static Expr d_rewrite_not_false_str
Definition: LFSCObject.h:138
static Expr d_uminus_to_mult_str
Definition: LFSCObject.h:147
static LFSCPrinter * printer
Definition: LFSCObject.h:16
static Expr d_rewrite_iff_str
Definition: LFSCObject.h:145
static Expr queryAtomic(const Expr &expr, bool getBase=false)
Definition: LFSCObject.cpp:365
static Expr d_flip_inequality_str
Definition: LFSCObject.h:113
static Expr d_basic_subst_op1_str
Definition: LFSCObject.h:116
static void collect_vars(const Expr &e, bool readPred=true)
Definition: LFSCObject.cpp:342
static Expr d_implyWeakerInequalityDiffLogic_str
Definition: LFSCObject.h:124
static Expr d_implyWeakerInequality_str
Definition: LFSCObject.h:123
static Expr d_and_final_s
Definition: LFSCObject.h:159
static int getNumNodes(const Expr &pf, bool recount=false)
Definition: LFSCObject.cpp:263
static bool what_is_proven(const Expr &pf, Expr &pe)
Definition: LFSCObject.cpp:539
static ExprMap< int > d_terms
Definition: LFSCObject.h:54
static Expr d_if_lift_rule_str
Definition: LFSCObject.h:139
static ExprMap< int > nnode_map
Definition: LFSCObject.h:31
static Expr d_iff_symm_str
Definition: LFSCObject.h:144
static Expr d_rewrite_eq_symm_str
Definition: LFSCObject.h:122
static ExprMap< int > d_formulas
Definition: LFSCObject.h:46
static Expr d_learned_clause_str
Definition: LFSCObject.h:109
static bool can_pnorm(const Expr &e)
Definition: LFSCObject.cpp:520
static Expr d_rewrite_or_str
Definition: LFSCObject.h:127
static bool getY(const Expr &e, Expr &pe, bool doIff=true, bool doLogic=true)
Definition: LFSCObject.cpp:448
static Expr d_rewrite_eq_refl_str
Definition: LFSCObject.h:143
static Expr d_iff_s
Definition: LFSCObject.h:161
static ExprMap< int > d_pn
Definition: LFSCObject.h:50
static Expr d_rewrite_ite_same_str
Definition: LFSCObject.h:149
static Expr d_pf_expr
Definition: LFSCObject.h:64
static ExprMap< Expr > cas_map
Definition: LFSCObject.h:34
static Expr d_cnf_add_unit_str
Definition: LFSCObject.h:155
static bool debug_conv
Definition: LFSCObject.h:24
static Expr d_rewrite_implies_str
Definition: LFSCObject.h:126
static Expr d_implyNegatedInequality_str
Definition: LFSCObject.h:146
static Expr d_eq_symm_str
Definition: LFSCObject.h:105
static int trusted_i
Definition: LFSCObject.h:19
static Expr d_int_const_eq_str
Definition: LFSCObject.h:142
static Expr d_iff_trans_str
Definition: LFSCObject.h:97
static bool isFormula(const Expr &e)
Definition: LFSCObject.cpp:514
static Expr d_imp_mp_str
Definition: LFSCObject.h:125
static bool debug_var
Definition: LFSCObject.h:25
static Expr d_real_shadow_str
Definition: LFSCObject.h:98
static Expr d_canon_plus_str
Definition: LFSCObject.h:106
static Expr d_imp_s
Definition: LFSCObject.h:162
static ExprMap< bool > input_vars
Definition: LFSCObject.h:56
static Expr d_and_mid_s
Definition: LFSCObject.h:164
static Expr queryElimNotNot(const Expr &expr)
Definition: LFSCObject.cpp:356
static Expr d_rewrite_iff_symm_str
Definition: LFSCObject.h:129
static int formula_i
Definition: LFSCObject.h:18
static Expr d_iff_false_elim_str
Definition: LFSCObject.h:132
static ExprMap< bool > input_preds
Definition: LFSCObject.h:58
static Expr d_bool_res_str
Definition: LFSCObject.h:92
static int term_i
Definition: LFSCObject.h:20
static ExprMap< int > d_trusted
Definition: LFSCObject.h:48
static Expr d_canon_invert_divide_str
Definition: LFSCObject.h:119
static Expr d_iff_mp_str
Definition: LFSCObject.h:95
static Expr d_impl_mp_str
Definition: LFSCObject.h:96
static Expr d_optimized_subst_op_str
Definition: LFSCObject.h:114
static ExprMap< Expr > skolem_vars
Definition: LFSCObject.h:37
static Expr d_not_not_elim_str
Definition: LFSCObject.h:134
static Expr d_basic_subst_op0_str
Definition: LFSCObject.h:117
static Expr d_implyEqualities_str
Definition: LFSCObject.h:151
static Expr d_eq_trans_str
Definition: LFSCObject.h:104
static ExprMap< bool > d_rules
Definition: LFSCObject.h:90
static Expr d_real_shadow_eq_str
Definition: LFSCObject.h:100
static Rational nullRat
Definition: LFSCObject.h:29
static Expr d_basic_subst_op_str
Definition: LFSCObject.h:101
static Expr d_refl_str
Definition: LFSCObject.h:107
static Expr d_minisat_proof_str
Definition: LFSCObject.h:156
static ExprMap< int > d_pn_form
Definition: LFSCObject.h:52
static Expr d_cycle_conflict_str
Definition: LFSCObject.h:99
static Expr d_negated_inequality_str
Definition: LFSCObject.h:112
static bool isVar(const Expr &e)
Definition: LFSCObject.cpp:337
static Expr d_addInequalities_str
Definition: LFSCObject.h:152