mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
This commit is contained in:
parent
833dd62623
commit
d50bfc6a50
|
@ -717,6 +717,8 @@ namespace datatype {
|
|||
todo.pop_back();
|
||||
continue;
|
||||
}
|
||||
if (!is_declared(s))
|
||||
return true;
|
||||
already_found.insert(datatype_name(s), GRAY);
|
||||
def const& d = get_def(s);
|
||||
bool can_process = true;
|
||||
|
|
|
@ -342,9 +342,7 @@ namespace sat {
|
|||
clause* solver::mk_clause(unsigned num_lits, literal * lits, sat::status st) {
|
||||
m_model_is_current = false;
|
||||
|
||||
for (unsigned i = 0; i < num_lits; i++)
|
||||
VERIFY(!was_eliminated(lits[i]));
|
||||
|
||||
|
||||
DEBUG_CODE({
|
||||
for (unsigned i = 0; i < num_lits; i++) {
|
||||
CTRACE("sat", was_eliminated(lits[i]), tout << lits[i] << " was eliminated\n";);
|
||||
|
|
|
@ -22,6 +22,7 @@ namespace sat {
|
|||
m_solver(m_params, l)
|
||||
{
|
||||
SASSERT(!m_solver.get_config().m_drat);
|
||||
m_solver.set_incremental(true);
|
||||
}
|
||||
|
||||
void dual_solver::flush() {
|
||||
|
@ -104,10 +105,10 @@ namespace sat {
|
|||
root = ext2lit(clause[0]);
|
||||
else {
|
||||
root = literal(m_solver.mk_var(), false);
|
||||
m_solver.set_external(root.var());
|
||||
for (unsigned i = 0; i < sz; ++i)
|
||||
m_solver.mk_clause(root, ~ext2lit(clause[i]), status::input());
|
||||
}
|
||||
}
|
||||
m_solver.set_external(root.var());
|
||||
m_roots.push_back(~root);
|
||||
TRACE("dual", tout << "root: " << ~root << " => " << literal_vector(sz, clause) << "\n";);
|
||||
}
|
||||
|
|
|
@ -23,7 +23,13 @@ Author:
|
|||
namespace sat {
|
||||
|
||||
class dual_solver {
|
||||
no_drat_params m_params;
|
||||
class dual_params : public no_drat_params {
|
||||
public:
|
||||
dual_params() {
|
||||
set_bool("core.minimize", false);
|
||||
}
|
||||
};
|
||||
dual_params m_params;
|
||||
solver m_solver;
|
||||
lim_svector<literal> m_units, m_roots;
|
||||
lim_svector<bool_var> m_tracked_vars;
|
||||
|
|
Loading…
Reference in a new issue