mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 05:13:39 +00:00
Code Activity

working on pb solver

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-11-14 18:04:55 -08:00
commit e034331f2e
3 changed files with 13 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/opt/opt_solver.cpp
View file

@ -109,9 +109,11 @@ namespace opt {
lbool r = m_context.check(num_assumptions, assumptions); lbool r = m_context.check(num_assumptions, assumptions);
if (m_is_dump) { if (m_is_dump) {
std::stringstream buffer; std::stringstream file_name;
buffer << "opt_solver" << ++g_checksat_count << ".smt2"; file_name << "opt_solver" << ++g_checksat_count << ".smt2";
to_smt2_benchmark(buffer.str().c_str(), "benchmark", "QF_BV"); std::ofstream buffer(file_name.str().c_str());
to_smt2_benchmark(buffer, "opt_solver", "QF_BV");
buffer.close();
} }
if (r == l_true && m_objective_enabled) { if (r == l_true && m_objective_enabled) {
m_objective_values.reset(); m_objective_values.reset();
@ -212,9 +214,8 @@ namespace opt {
return dynamic_cast<opt_solver&>(s); return dynamic_cast<opt_solver&>(s);
} }
void opt_solver::to_smt2_benchmark(char const * file_name, char const * name, char const * logic, void opt_solver::to_smt2_benchmark(std::ofstream & buffer, char const * name, char const * logic,
char const * status, char const * attributes) { char const * status, char const * attributes) {
std::ofstream buffer(file_name);
ast_smt_pp pp(m); ast_smt_pp pp(m);
pp.set_benchmark_name(name); pp.set_benchmark_name(name);
pp.set_logic(logic); pp.set_logic(logic);
@ -225,8 +226,7 @@ namespace opt {
for (unsigned i = 0; i < get_num_assertions(); ++i) { for (unsigned i = 0; i < get_num_assertions(); ++i) {
pp.add_assumption(to_expr(get_assertion(i))); pp.add_assumption(to_expr(get_assertion(i)));
} }
pp.display_smt2(buffer, to_expr(m.mk_true())); pp.display_smt2(buffer, to_expr(m.mk_true()));
buffer.close();
} }
opt_solver::toggle_objective::toggle_objective(opt_solver& s, bool new_value): s(s), m_old_value(s.m_objective_enabled) { opt_solver::toggle_objective::toggle_objective(opt_solver& s, bool new_value): s(s), m_old_value(s.m_objective_enabled) {

4
src/opt/opt_solver.h
View file

@ -90,8 +90,8 @@ namespace opt {
smt::theory_opt& get_optimizer(); smt::theory_opt& get_optimizer();
void to_smt2_benchmark(char const * file_name, char const * name = "benchmarks", void to_smt2_benchmark(std::ofstream & buffer, char const * name = "benchmarks",
char const * logic = "", char const * status = "unknown", char const * attributes = ""); char const * logic = "", char const * status = "unknown", char const * attributes = "");
}; };
} }

11
src/smt/theory_card.cpp
View file

@ -133,15 +133,10 @@ namespace smt {
} }
static unsigned gcd(unsigned a, unsigned b) { static unsigned gcd(unsigned a, unsigned b) {
if (a == 0) return b;
if (b == 0) return a;
while (a != b) { while (a != b) {
if (a == 0) { if (a == 0) return b;
return b; if (b == 0) return a;
} SASSERT(a != 0 && b != 0);
if (b == 0) {
return a;
}
if (a < b) { if (a < b) {
b %= a; b %= a;
} }