Obtenir le noyau non saturé en utilisant Z3_solver_get_unsat_core

Question

Supposons que l'ensemble des contraintes sur l'arithmétique réelle non linéaire soit le suivant

pred1 = (> (- (* (- v2_x v0_x) (- v1_y v0_y)) (* (- v2_y v0_y) (- v1_x v0_x))) 0)
pred2 = (> (- (* (- v1_x v0_x) (- v2_y v0_y)) (* (- v1_y v0_y) (- v2_x v0_x))) 0)

En effet, si nous faisons

Z3_solver_assert(ctx,solver,pred1);
Z3_solver_assert(ctx,solver,pred2);
b = Z3_solver_check(ctx, solver);

b serait insatisfaisant. Je veux obtenir le noyau unsat (pour cet exemple, c'est trivial). Ainsi, pour chacun de ces prédicats, j'ai défini une variable de prédicat. Disons qu'elles sont p1 y p2 .

Z3_ast p1 = mk_bool_var(ctx, "P1");
assumptions[i] = Z3_mk_not(ctx, p1);
Z3_ast g[2] = { pred1, p1 };
Z3_solver_assert(ctx,solver,Z3_mk_or(ctx, 2, g));
Z3_ast p2 = mk_bool_var(ctx, "P2");
assumptions[i] = Z3_mk_not(ctx, p2);
Z3_ast g[2] = { pred2, p2 };
Z3_solver_assert(ctx,solver,Z3_mk_or(ctx, 2, g));

puis j'appelle Z3_solver_check_assumptions(ctx, solver, 2 , assumptions);

mais cela renvoie Z3_L_UNDEF et la raison en est (incomplete (theory arithmetic))

Je me demande où je commets une erreur et comment résoudre ce problème.

Voici comment les choses sont initialisées :

  ctx = Z3_mk_context(cfg);
  Z3_symbol logic_symbol = Z3_mk_string_symbol(ctx, "QF_UFNRA");
  solver = Z3_mk_solver_for_logic((Z3_context)ctx, logic_symbol);
  Z3_solver_inc_ref(ctx, solver);
  Z3_params params = Z3_mk_params(ctx);
  Z3_symbol param_symbol = Z3_mk_string_symbol(ctx, "unsat_core");
  Z3_params_set_bool(ctx , params, param_symbol, Z3_L_TRUE);
  Z3_solver_set_params(ctx, solver, params); 

Merci,

Answer 1

Z3 contient de nombreux solveurs. Pour les problèmes arithmétiques non linéaires, il utilise nlsat . L'implémentation de ce solveur se trouve dans le répertoire src/nlsat et l'algorithme est expliqué aquí . Cependant, l'actuelle nlsat ne prend pas en charge l'extraction des noyaux d'insat ni la génération de preuves. Lorsque l'utilisateur demande l'extraction d'un noyau non-sat, Z3 passe à un solveur général qui est incomplet pour l'arithmétique non-linéaire. En d'autres termes, il peut renvoyer unknown pour les problèmes arithmétiques non linéaires. Le solveur général prend en charge de nombreuses théories, des quantificateurs, l'extraction de noyaux d'Unsat et la génération de preuves. Il est complet pour linéaire arithmétique, mais comme je l'ai dit, elle n'est pas complète pour le fragment non linéaire. Dans le plan, Z3 aura une nouvelle version de nlsat qui s'intègre à d'autres théories et prend en charge l'extraction des noyaux d'insat, mais il s'agit là d'un travail futur.