mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

Add accessor for lower/upper bounds of algebraic numerals #3245

Browse source 
The pretty printer for algebraic numerals prints a polynomial root expression, however, polynomial root expressions are not exposed over the API. The C API contains methods for approximating root objects from above and below with arbitrary precision. These functions are now exposed over the C++ API.
Note that algebraic numbers are also disjoint from rcf (real closed field) objects.
Thus, z3 doesn't support adding "pi" as an extension field to algebraic numbers that are used by the nlsat solver. It operats on algebraic numbers formed by roots over polynomial with rational coefficients
This commit is contained in:
Nikolaj Bjorner 2020-03-12 14:23:45 -07:00
parent 356a9bb9ed
commit a6fcdecfd7
3 changed files with 25 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/smt/smt_context.cpp
View file

@ -3364,10 +3364,13 @@ namespace smt {
r = l_undef;
}
if (r == l_true && gparams::get_value("model_validate") == "true") {
model_ref mdl;
get_model(mdl);
for (theory* t : m_theory_set) {
t->validate_model(*mdl);
recfun::util u(m);
if (u.get_rec_funs().empty()) {
model_ref mdl;
get_model(mdl);
for (theory* t : m_theory_set) {
t->validate_model(*mdl);
}
}
#if 0
for (literal lit : m_assigned_literals) {

1
src/smt/theory_seq.cpp
View file

@ -4412,6 +4412,7 @@ app* theory_seq::mk_value(app* e) {
void theory_seq::validate_model(model& mdl) {
return;
for (auto const& eq : m_eqs) {
expr_ref_vector ls = eq.ls();
expr_ref_vector rs = eq.rs();