mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
fix regression reported in #1159
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
49f88d9d90
commit
70f6280bf1
|
@ -431,6 +431,7 @@ format_ns::format * smt2_pp_environment::pp_sort(sort * s) {
|
|||
fs.push_back(pp_sort(to_sort(s->get_parameter(0).get_ast())));
|
||||
return mk_seq1(m, fs.begin(), fs.end(), f2f(), get_sutil().is_seq(s)?"Seq":"Re");
|
||||
}
|
||||
#if 0
|
||||
if (get_dtutil().is_datatype(s)) {
|
||||
ptr_buffer<format> fs;
|
||||
unsigned sz = get_dtutil().get_datatype_num_parameter_sorts(s);
|
||||
|
@ -439,6 +440,7 @@ format_ns::format * smt2_pp_environment::pp_sort(sort * s) {
|
|||
}
|
||||
return mk_seq1(m, fs.begin(), fs.end(), f2f(), s->get_name().str().c_str());
|
||||
}
|
||||
#endif
|
||||
return format_ns::mk_string(get_manager(), s->get_name().str().c_str());
|
||||
}
|
||||
|
||||
|
|
|
@ -366,13 +366,14 @@ class smt_printer {
|
|||
return;
|
||||
}
|
||||
else if (s->is_sort_of(m_dt_fid, DATATYPE_SORT)) {
|
||||
m_out << m_renaming.get_symbol(s->get_name());
|
||||
#if 0
|
||||
datatype_util util(m_manager);
|
||||
unsigned num_sorts = util.get_datatype_num_parameter_sorts(s);
|
||||
if (num_sorts > 0) {
|
||||
m_out << "(";
|
||||
}
|
||||
|
||||
m_out << m_renaming.get_symbol(s->get_name());
|
||||
if (num_sorts > 0) {
|
||||
for (unsigned i = 0; i < num_sorts; ++i) {
|
||||
m_out << " ";
|
||||
|
@ -380,6 +381,7 @@ class smt_printer {
|
|||
}
|
||||
m_out << ")";
|
||||
}
|
||||
#endif
|
||||
return;
|
||||
}
|
||||
else {
|
||||
|
|
|
@ -2,8 +2,8 @@
|
|||
Copyright (c) 2017 Microsoft Corporation
|
||||
Author: Lev Nachmanson
|
||||
*/
|
||||
#include "util/vector.h"
|
||||
#include <memory>
|
||||
#include "util/vector.h"
|
||||
#include "util/lp/lp_settings.hpp"
|
||||
template bool lean::vectors_are_equal<double>(vector<double> const&, vector<double> const&);
|
||||
template bool lean::vectors_are_equal<lean::mpq>(vector<lean::mpq > const&, vector<lean::mpq> const&);
|
||||
|
|
|
@ -2,8 +2,8 @@
|
|||
Copyright (c) 2017 Microsoft Corporation
|
||||
Author: Lev Nachmanson
|
||||
*/
|
||||
#include "util/vector.h"
|
||||
#include <memory>
|
||||
#include "util/vector.h"
|
||||
#include "util/lp/row_eta_matrix.hpp"
|
||||
#include "util/lp/lu.h"
|
||||
namespace lean {
|
||||
|
|
Loading…
Reference in a new issue