75 static int queryM(
const Expr& expr,
bool add =
true,
bool trusted =
false);
81 static bool getY(
const Expr& e,
Expr& pe,
bool doIff =
true,
bool doLogic =
true );
static Expr d_right_minus_left_str
static Expr d_cnf_convert_str
static ExprMap< bool > d_formulas_printed
Data structure of expressions in CVC3.
static std::map< int, bool > pntNeeded
static ExprMap< bool > temp_visited
static void define_skolem_vars(const Expr &e)
static bool cvc3_mimic_input
static Expr d_mult_ineqn_str
static Expr d_rewrite_not_not_str
static Expr cascade_expr(const Expr &e)
static Expr d_iff_true_elim_str
static Expr d_canon_mult_str
static ExprMap< bool > d_assump_map
static Expr d_not_to_iff_str
static Expr d_rewrite_not_true_str
static int queryM(const Expr &expr, bool add=true, bool trusted=false)
static Expr d_mult_eqn_str
static Expr d_iff_not_false_str
static Expr d_const_predicate_str
static Expr d_rewrite_and_str
static Expr d_lessThan_To_LE_rhs_rwr_str
static int queryT(const Expr &e)
static int queryMt(const Expr &expr)
static Expr d_minus_to_plus_str
static Expr d_iff_false_str
static Expr d_var_intro_str
static Expr d_plus_predicate_str
static Expr d_iff_true_str
static Expr d_rewrite_not_false_str
static Expr d_uminus_to_mult_str
static LFSCPrinter * printer
static Expr d_rewrite_iff_str
static Expr queryAtomic(const Expr &expr, bool getBase=false)
static Expr d_flip_inequality_str
static Expr d_basic_subst_op1_str
static void collect_vars(const Expr &e, bool readPred=true)
static Expr d_implyWeakerInequalityDiffLogic_str
static Expr d_implyWeakerInequality_str
static Expr d_and_final_s
static int getNumNodes(const Expr &pf, bool recount=false)
static bool what_is_proven(const Expr &pf, Expr &pe)
static ExprMap< int > d_terms
static Expr d_if_lift_rule_str
static ExprMap< int > nnode_map
static Expr d_iff_symm_str
static Expr d_rewrite_eq_symm_str
static ExprMap< int > d_formulas
static Expr d_learned_clause_str
static bool can_pnorm(const Expr &e)
static Expr d_rewrite_or_str
static bool getY(const Expr &e, Expr &pe, bool doIff=true, bool doLogic=true)
static Expr d_rewrite_eq_refl_str
static ExprMap< int > d_pn
static Expr d_rewrite_ite_same_str
static ExprMap< Expr > cas_map
static Expr d_cnf_add_unit_str
static Expr d_rewrite_implies_str
static Expr d_implyNegatedInequality_str
static Expr d_eq_symm_str
static Expr d_int_const_eq_str
static Expr d_iff_trans_str
static bool isFormula(const Expr &e)
static Expr d_real_shadow_str
static Expr d_canon_plus_str
static ExprMap< bool > input_vars
static Expr queryElimNotNot(const Expr &expr)
static Expr d_rewrite_iff_symm_str
static Expr d_iff_false_elim_str
static ExprMap< bool > input_preds
static Expr d_bool_res_str
static ExprMap< int > d_trusted
static Expr d_canon_invert_divide_str
static Expr d_impl_mp_str
static Expr d_optimized_subst_op_str
static ExprMap< Expr > skolem_vars
static Expr d_not_not_elim_str
static Expr d_basic_subst_op0_str
static Expr d_implyEqualities_str
static Expr d_eq_trans_str
static ExprMap< bool > d_rules
static Expr d_real_shadow_eq_str
static Expr d_basic_subst_op_str
static Expr d_minisat_proof_str
static ExprMap< int > d_pn_form
static Expr d_cycle_conflict_str
static Expr d_negated_inequality_str
static bool isVar(const Expr &e)
static Expr d_addInequalities_str