mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
fix wcnf front-end and unsat case in pd
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
ee458fa601
commit
149549dd52
|
@ -239,7 +239,12 @@ public:
|
|||
break;
|
||||
case l_false:
|
||||
is_sat = process_unsat();
|
||||
if (is_sat != l_true) return is_sat;
|
||||
if (is_sat == l_false) {
|
||||
m_lower = m_upper;
|
||||
}
|
||||
if (is_sat == l_undef) {
|
||||
return is_sat;
|
||||
}
|
||||
break;
|
||||
case l_undef:
|
||||
return l_undef;
|
||||
|
|
|
@ -42,6 +42,11 @@ public:
|
|||
next();
|
||||
}
|
||||
}
|
||||
void skip_space() {
|
||||
while (ch() != 10 && ((ch() >= 9 && ch() <= 13) || ch() == 32)) {
|
||||
next();
|
||||
}
|
||||
}
|
||||
void skip_line() {
|
||||
while(true) {
|
||||
if (eof()) {
|
||||
|
@ -88,6 +93,19 @@ public:
|
|||
}
|
||||
return neg ? -val : val;
|
||||
}
|
||||
|
||||
unsigned parse_unsigned() {
|
||||
skip_space();
|
||||
if (ch() == '\n') {
|
||||
return UINT_MAX;
|
||||
}
|
||||
unsigned val = 0;
|
||||
while (ch() >= '0' && ch() <= '9') {
|
||||
val = val*10 + (ch() - '0');
|
||||
next();
|
||||
}
|
||||
return val;
|
||||
}
|
||||
};
|
||||
|
||||
class wcnf {
|
||||
|
@ -95,11 +113,10 @@ class wcnf {
|
|||
ast_manager& m;
|
||||
stream_buffer& in;
|
||||
|
||||
app_ref read_clause(int& weight) {
|
||||
app_ref read_clause(unsigned& weight) {
|
||||
int parsed_lit;
|
||||
int var;
|
||||
parsed_lit = in.parse_int();
|
||||
weight = parsed_lit;
|
||||
weight = in.parse_unsigned();
|
||||
app_ref result(m), p(m);
|
||||
expr_ref_vector ors(m);
|
||||
while (true) {
|
||||
|
@ -115,11 +132,11 @@ class wcnf {
|
|||
return result;
|
||||
}
|
||||
|
||||
void parse_spec(int& num_vars, int& num_clauses, int& max_weight) {
|
||||
void parse_spec(unsigned& num_vars, unsigned& num_clauses, unsigned& max_weight) {
|
||||
in.parse_token("wcnf");
|
||||
num_vars = in.parse_int();
|
||||
num_clauses = in.parse_int();
|
||||
max_weight = in.parse_int();
|
||||
num_vars = in.parse_unsigned();
|
||||
num_clauses = in.parse_unsigned();
|
||||
max_weight = in.parse_unsigned();
|
||||
}
|
||||
|
||||
public:
|
||||
|
@ -129,7 +146,7 @@ public:
|
|||
}
|
||||
|
||||
void parse() {
|
||||
int num_vars = 0, num_clauses = 0, max_weight = 0;
|
||||
unsigned num_vars = 0, num_clauses = 0, max_weight = 0;
|
||||
while (true) {
|
||||
in.skip_whitespace();
|
||||
if (in.eof()) {
|
||||
|
@ -141,11 +158,12 @@ public:
|
|||
else if (*in == 'p') {
|
||||
++in;
|
||||
parse_spec(num_vars, num_clauses, max_weight);
|
||||
std::cout << "v " << num_vars << " c " << num_clauses << " w " << max_weight << "\n";
|
||||
}
|
||||
else {
|
||||
int weight = 0;
|
||||
unsigned weight = 0;
|
||||
app_ref cls = read_clause(weight);
|
||||
if (weight == max_weight) {
|
||||
if (weight >= max_weight) {
|
||||
opt.add_hard_constraint(cls);
|
||||
}
|
||||
else {
|
||||
|
|
Loading…
Reference in a new issue