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::exprs 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 porquecompno es solamente un valor booleano sino un objetoz3::exprque representa la comparación(a < b). Para extraer el valor booleano decomp, se necesita un solucionador o un contexto.Si necesitas comparar objetos
z3::exprfrecuentemente, 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.