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

spacer: print all lemmas in json

Browse source
This commit is contained in:
Arie Gurfinkel 2018-05-30 09:04:39 -07:00
parent bfa472faec
commit fce68536d3
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/muz/spacer/spacer_json.cpp
View file

@ -119,9 +119,10 @@ void json_marshaller::marshal_lemmas_new(std::ostream &out) const {
for (auto &pob_map:m_relations) { for (auto &pob_map:m_relations) {
std::ostringstream pob_lemmas; std::ostringstream pob_lemmas;
pob *n = pob_map.first; pob *n = pob_map.first;
unsigned i = 0;
for (auto *l : n->lemmas()) { for (auto *l : n->lemmas()) {
pob_lemmas << ((unsigned)pob_lemmas.tellp() == 0 ? "" : ",") pob_lemmas << ((unsigned)pob_lemmas.tellp() == 0 ? "" : ",")
<< "\"0\":"; << "\"" << i++ << "\":";
lemma_ref_vector lemmas_vec; lemma_ref_vector lemmas_vec;
lemmas_vec.push_back(l); lemmas_vec.push_back(l);
json_marshal(pob_lemmas, lemmas_vec); json_marshal(pob_lemmas, lemmas_vec);