1

Closed

"simplify" tactic applied for "true" gives "false"

description

Hi,

Consider the method goal::as_expr (z3++.h, unstable branch)
expr as_expr() const {
            unsigned n = size();
            if (n == 0) 
                return ctx().bool_val(false);
            else if (n == 1)
                return operator[](0);
            else {
                array<Z3_ast> args(n);
                for (unsigned i = 0; i < n; i++)
                    args[i] = operator[](i);
                return expr(ctx(), Z3_mk_and(ctx(), n, args.ptr()));
            }
        }
Is that correct that for an empty set of goals "false" value shall be returned? It also gives a strange result on the following example:
   context ctx; 
   expr e(ctx);
   e = ctx.bool_val(true);
   
   cout << "Input formula: " << e << endl;
   tactic t_sim(ctx, "simplify");

   goal g(ctx);
   g.add(e);

   apply_result result= t_sim.apply(g);
   cout << "Goals after simplification:" << result << endl;
   goal result_goal = result[0];
    
   cout << "Simplfication result: " << result_goal.as_expr() << endl;
Ouptut:
Input formula: true
Goals after simplification:(goals
(goal)
)
Simplfication result: false
Thanks,
Valentyn
Closed Jul 9, 2013 at 3:22 PM by leodemoura
Fixed in the unstable (work-in-progress) branch

comments

leodemoura wrote Jul 9, 2013 at 3:20 PM

Thanks for catching that. You are correct. It should return ctx().bool_val(true)

Thanks,
Leo