From 683070a175eb6d9621d7464f7cbb013897df07a4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 5 Feb 2024 10:44:41 -0800 Subject: [PATCH] finish encoding of n'th root Signed-off-by: Nikolaj Bjorner --- src/nlsat/nlsat_solver.cpp | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 79a42e6786a..1b4924c6a2e 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -3182,10 +3182,24 @@ namespace nlsat { std::string y2 = std::string("y") + std::to_string(j+1); out << "(< " << y1 << " " << y2 << ")\n"; } + + std::string yn = "y" + std::to_string(a.i() - 1); + // TODO we need (forall z : z < yn . p(z) => z = y1 or ... z = y_{n-1}) // to say y1, .., yn are the first n distinct roots. // - std::string yn = "y" + std::to_string(a.i() - 1); + out << "(forall ((z Real)) (=> (and (< z " << yn << ") "; display_poly_root(out, "z", a, proc) << ") "; + if (a.i() == 1) { + out << "false))\n"; + } + else { + out << "(or "; + for (unsigned j = 0; j + 1 < a.i(); ++j) { + std::string y1 = std::string("y") + std::to_string(j); + out << "(= z " << y1 << ") "; + } + out << ")))\n"; + } switch (a.get_kind()) { case atom::ROOT_LT: out << "(< "; proc(out, a.x()); out << " " << yn << ")"; break; case atom::ROOT_GT: out << "(> "; proc(out, a.x()); out << " " << yn << ")"; break;