267 for(
int a=1; a<pf.
arity(); a++ ){
293 }
else if( e.
arity()==1 ){
295 }
else if( e.
arity()>0 ){
297 for(
int a=e.
arity()-2; a>=0; a-- ){
324 ose <<
"Unexpected non-discharged assumption " << ce;
330 for(
int a=1; a<e.
arity(); a++ ){
350 for(
int a=0; a<e.
arity(); a++ ){
375 }
else if( e[0].isFalse() ){
379 return Expr(
get_not( e[0].getKind() ), e[0][1], e[0][0] );
400 print_error(
"WARNING: uninitialized e in query", cout );
406 return val*(neg ? -1 : 1 );
423 os <<
"ERROR: cannot make polynomial normalization for " << ce <<
std::endl;
463 ose <<
"Can't pnorm " << ea[0] <<
" " << ea[1] <<
std::endl;
473 if(
getY( e[1], pe2,
false ) ){
490 if(
getY( e[1], pe2,
false,
false ) ){
491 if(
getY( e[0], pe1,
false,
false ) ){
549 pe =
Expr(
EQ, pf[1], pf[2] );
562 pe =
Expr(
IFF, pf[1], pf[3] );
572 pe =
Expr(
EQ, pf[2], pf[4] );
577 pe =
Expr(
EQ, pf[3], pf[2] );
586 pe =
Expr(
IFF, pf[1], pf[2] );
595 if( pf[1].getKind()==
UMINUS ){
596 pe =
Expr(
EQ, pf[1], pf[2] );
598 }
else if( pf[1].getKind()==
NOT ){
599 pe =
Expr(
IFF, pf[1], pf[2] );
611 pe =
Expr( ( pf[1].getKind()==
LE && pf[2].getKind()==
LE ) ?
LE :
LT, pf[1][0], pf[2][1] );
615 pe =
Expr(
EQ, pf[2][0], pf[2][1]);
620 if( pf[1].getKind()==
AND || pf[1].getKind()==
OR || pf[1].getKind()==
IFF ||
is_eq_kind( pf[1].getKind() ) ||
622 pe =
Expr(
IFF, pf[1], pf[2] );
624 }
else if( pf[1].getKind()==
ITE || pf[1].getKind()==
PLUS || pf[1].getKind()==
MINUS || pf[1].getKind()==
MULT ){
625 pe =
Expr(
EQ, pf[1], pf[2] );
669 pe =
Expr(
IFF, pf[1], pf[1] );
671 pe =
Expr(
EQ, pf[1], pf[1] );
700 pe =
Expr(
IFF, pf[1],
Expr(
get_not( pf[1][0].getKind() ), pf[1][0][0], pf[1][0][1] ) );
771 if(pf[1] == e_false){
776 if(pf[1].isNot() && pf[1][0] == pf[2]){
777 pe = e.
iffExpr(pf[2].negate());
786 if(pf[2] == e_false){
791 if(pf[2].isNot() && pf[2][0] == pf[1]){
792 pe = e.
iffExpr(pf[1].negate());
811 ose <<
"What_is_proven, unknown: (" <<
d_rules[pf[0]] <<
"): " << pf[0];
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.
ExprManager * getEM() const
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
Rational getNumerator() const
static Expr d_canon_mult_str
static ExprMap< bool > d_assump_map
static Expr d_not_to_iff_str
bool isInitialized() const
const Rational & getRational() const
Get the Rational value out of RATIONAL_EXPR.
static Expr d_rewrite_not_true_str
iterator find(const Expr &e)
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
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
int get_normalized(int knd, bool isnot)
static Expr d_rewrite_iff_str
static void print_error(const char *c, std::ostream &s)
static Expr queryAtomic(const Expr &expr, bool getBase=false)
Expr impExpr(const Expr &right) const
static Expr d_flip_inequality_str
static Expr d_basic_subst_op1_str
bool is_opposite(int knd)
static void collect_vars(const Expr &e, bool readPred=true)
Expr newStringExpr(const std::string &s)
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
Expr iffExpr(const Expr &right) const
static ExprMap< int > nnode_map
const Expr & falseExpr()
FALSE Expr.
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
const Expr & trueExpr()
TRUE Expr.
static Expr d_rewrite_ite_same_str
Expr newRatExpr(const Rational &r)
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
bool is_comparison(int knd)
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
Expr newVarExpr(const std::string &s)
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