mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

display dimacs

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-03-14 18:22:42 -07:00
parent e19c119496
commit 7b50fca02c
1 changed files with 52 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

60
src/ast/display_dimacs.cpp
View file

@ -26,6 +26,7 @@ std::ostream& display_dimacs(std::ostream& out, expr_ref_vector const& fmls) {
ptr_vector<expr> exprs;
unsigned num_vars = 0;
unsigned num_cls = fmls.size();
bool is_from_dimacs = true;
for (expr * f : fmls) {
unsigned num_lits;
expr * const * lits;
@ -41,10 +42,51 @@ std::ostream& display_dimacs(std::ostream& out, expr_ref_vector const& fmls) {
expr * l = lits[j];
if (m.is_not(l))
l = to_app(l)->get_arg(0);
if (expr2var.get(l->get_id(), UINT_MAX) == UINT_MAX) {
num_vars++;
expr2var.setx(l->get_id(), num_vars, UINT_MAX);
exprs.setx(l->get_id(), l, nullptr);
if (!is_uninterp_const(l)) {
is_from_dimacs = false;
break;
}
symbol const& s = to_app(l)->get_decl()->get_name();
if (s.is_numerical() && s.get_num() > 0) {
if (expr2var.get(l->get_id(), UINT_MAX) == UINT_MAX) {
++num_vars;
expr2var.setx(l->get_id(), s.get_num(), UINT_MAX);
exprs.setx(l->get_id(), l, nullptr);
}
continue;
}
is_from_dimacs = false;
break;
}
if (!is_from_dimacs) {
num_vars = 0;
expr2var.reset();
exprs.reset();
break;
}
}
if (!is_from_dimacs) {
for (expr * f : fmls) {
unsigned num_lits;
expr * const * lits;
if (m.is_or(f)) {
num_lits = to_app(f)->get_num_args();
lits = to_app(f)->get_args();
}
else {
num_lits = 1;
lits = &f;
}
for (unsigned j = 0; j < num_lits; j++) {
expr * l = lits[j];
if (m.is_not(l))
l = to_app(l)->get_arg(0);
if (expr2var.get(l->get_id(), UINT_MAX) == UINT_MAX) {
num_vars++;
expr2var.setx(l->get_id(), num_vars, UINT_MAX);
exprs.setx(l->get_id(), l, nullptr);
}
}
}
}
@ -71,10 +113,12 @@ std::ostream& display_dimacs(std::ostream& out, expr_ref_vector const& fmls) {
}
out << "0\n";
}
for (expr* e : exprs) {
if (e && is_app(e)) {
symbol const& n = to_app(e)->get_decl()->get_name();
out << "c " << expr2var[e->get_id()] << " " << n << "\n";
if (!is_from_dimacs) {
for (expr* e : exprs) {
if (e && is_app(e)) {
symbol const& n = to_app(e)->get_decl()->get_name();
out << "c " << expr2var[e->get_id()] << " " << n << "\n";
}
}
}
return out;