mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

add note that the encoding is a first approximation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-02-04 19:11:35 -08:00
parent b9528b1c56
commit d743e1b47c
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/nlsat/nlsat_solver.cpp
View file

@ -3163,6 +3163,7 @@ namespace nlsat {
if (a.i() == 1 && m_pm.degree(a.p(), a.x()) == 1) if (a.i() == 1 && m_pm.degree(a.p(), a.x()) == 1)
return display_linear_root_smt2(out, a, proc); return display_linear_root_smt2(out, a, proc);
#if 1 #if 1
// A first approximation: this encoding assumes roots are distinct
out << "(exists ("; out << "(exists (";
for (unsigned j = 0; j < a.i(); ++j) { for (unsigned j = 0; j < a.i(); ++j) {
std::string y = std::string("y") + std::to_string(j); std::string y = std::string("y") + std::to_string(j);