Z3: utilizar operadores de comparación (<,<=,...) en z3::expr
Almaceno números como z3::expr
y quiero compararlos. Intenté lo siguiente:
z3::context c;
z3::expr a = c.real_val("0");
z3::expr b = c.real_val("1");
z3::expr comp = (a < b);
std::cout << comp.is_bool() << std::endl;
std::cout << comp.bool_value() << std::endl;
Estoy un poco confundido, ¿por qué es comp.bool_value()
falso?
Si uso un solucionador, todo funciona como se esperaba:
z3::solver s(c);
s.add(comp);
std::cout << s.check() << std::endl;
Tengo que comparar z3::expr
s con bastante frecuencia, ¿cuál sería el método más rápido para hacerlo? El uso de un solucionador me parece como si tuviera mucha sobrecarga.
davy.ai
La razón por la que
comp.bool_value()
es falsa es porquecomp
no es solamente un valor booleano sino un objetoz3::expr
que representa la comparación(a < b)
. Para extraer el valor booleano decomp
, se necesita un solucionador o un contexto.Si necesitas comparar objetos
z3::expr
frecuentemente, se recomienda utilizar un solucionador para mayor eficiencia ya que está diseñado específicamente para manejar esta tarea. Utilizar un solucionador no se considera sobrecarga sino que es la forma estándar de comprobar la satisfacibilidad y resolver las restricciones en Z3.