mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
parent
99339798ee
commit
44a0dbbc61
|
@ -1976,6 +1976,22 @@ public class Context implements AutoCloseable {
|
|||
{
|
||||
return (SeqExpr) Expr.create(this, Native.mkString(nCtx(), s));
|
||||
}
|
||||
|
||||
/**
|
||||
* Convert an integer expression to a string.
|
||||
*/
|
||||
public SeqExpr intToString(Expr e)
|
||||
{
|
||||
return (SeqExpr) Expr.create(this, Native.Z3_mkIntToStr(nCtx(), e.getNativeObject()));
|
||||
}
|
||||
|
||||
/**
|
||||
* Convert an integer expression to a string.
|
||||
*/
|
||||
public IntExpr stringToInt(Expr e)
|
||||
{
|
||||
return (IntExpr) Expr.create(this, Native.mkStrToInt(nCtx(), e.getNativeObject()));
|
||||
}
|
||||
|
||||
/**
|
||||
* Concatenate sequences.
|
||||
|
|
|
@ -292,7 +292,7 @@ namespace opt {
|
|||
model_updated(m_model.get());
|
||||
}
|
||||
if (is_sat != l_true) {
|
||||
TRACE("opt", tout << m_hard_constraints << "\n";);
|
||||
TRACE("opt", tout << m_hard_constraints << " " << asms << "\n";);
|
||||
if (!asms.empty()) {
|
||||
s.get_unsat_core(m_core);
|
||||
}
|
||||
|
|
|
@ -1412,7 +1412,7 @@ public:
|
|||
}
|
||||
|
||||
final_check_status final_check_eh() {
|
||||
IF_VERBOSE(2, verbose_stream() << "final-check\n");
|
||||
IF_VERBOSE(2, verbose_stream() << "final-check " << m_solver->get_status() << "\n");
|
||||
m_use_nra_model = false;
|
||||
lbool is_sat = l_true;
|
||||
if (m_solver->get_status() != lp::lp_status::OPTIMAL) {
|
||||
|
|
Loading…
Reference in a new issue