mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2017-01-25 18:09:37 -08:00
parent 777091e653 4782e19086
commit 6e6c5935d7
4 changed files with 31 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/api/python/z3/z3.py
View file

@ -2662,6 +2662,12 @@ class RatNumRef(ArithRef):
return self.denominator().as_long()
def is_int(self):
return False
def is_real(self):
return True
def is_int_value(self):
return self.denominator().is_int() and self.denominator_as_long() == 1
def as_long(self):

25
src/sat/sat_simplifier.cpp
View file

@ -896,7 +896,7 @@ namespace sat {
unsigned idx = l.index();
if (m_queue.contains(idx))
m_queue.decreased(idx);
else
else
m_queue.insert(idx);
}
literal next() { SASSERT(!empty()); return to_literal(m_queue.erase_min()); }
@ -918,16 +918,19 @@ namespace sat {
}
void insert(literal l) {
bool_var v = l.var();
if (s.is_external(v) || s.was_eliminated(v))
return;
m_queue.insert(l);
}
bool process_var(bool_var v) {
return !s.is_external(v) && !s.was_eliminated(v);
}
void operator()(unsigned num_vars) {
for (bool_var v = 0; v < num_vars; v++) {
insert(literal(v, false));
insert(literal(v, true));
if (process_var(v)) {
insert(literal(v, false));
insert(literal(v, true));
}
}
while (!m_queue.empty()) {
s.checkpoint();
@ -941,9 +944,9 @@ namespace sat {
void process(literal l) {
TRACE("blocked_clause", tout << "processing: " << l << "\n";);
model_converter::entry * new_entry = 0;
if (s.is_external(l.var()) || s.was_eliminated(l.var()))
if (!process_var(l.var())) {
return;
}
{
m_to_remove.reset();
{
@ -963,8 +966,10 @@ namespace sat {
mc.insert(*new_entry, c);
unsigned sz = c.size();
for (unsigned i = 0; i < sz; i++) {
if (c[i] != l)
m_queue.decreased(~c[i]);
literal lit = c[i];
if (lit != l && process_var(lit.var())) {
m_queue.decreased(~lit);
}
}
}
s.unmark_all(c);

3
src/smt/params/smt_params_helper.pyg
View file

@ -63,5 +63,6 @@ def_module_params(module_name='smt',
('dack.threshold', UINT, 10, ' number of times the congruence rule must be used before Leibniz\'s axiom is expanded'),
('core.validate', BOOL, False, 'validate unsat core produced by SMT context'),
('core.minimize', BOOL, False, 'minimize unsat core produced by SMT context'),
('core.extend_patterns', BOOL, False, 'extend unsat core with literals that trigger (potential) quantifier instances')
('core.extend_patterns', BOOL, False, 'extend unsat core with literals that trigger (potential) quantifier instances'),
('core.extend_patterns.max_distance', UINT, UINT_MAX, 'limits the distance of a pattern-extended unsat core')
))

11
src/smt/smt_solver.cpp
View file

@ -37,6 +37,7 @@ namespace smt {
symbol m_logic;
bool m_minimizing_core;
bool m_core_extend_patterns;
unsigned m_core_extend_patterns_max_distance;
obj_map<expr, expr*> m_name2assertion;
public:
@ -46,12 +47,14 @@ namespace smt {
m_params(p),
m_context(m, m_smt_params),
m_minimizing_core(false),
m_core_extend_patterns(false) {
m_core_extend_patterns(false),
m_core_extend_patterns_max_distance(UINT_MAX) {
m_logic = l;
if (m_logic != symbol::null)
m_context.set_logic(m_logic);
smt_params_helper smth(p);
m_core_extend_patterns = smth.core_extend_patterns();
m_core_extend_patterns_max_distance = smth.core_extend_patterns_max_distance();
}
virtual solver * translate(ast_manager & m, params_ref const & p) {
@ -283,7 +286,7 @@ namespace smt {
func_decl_set pattern_fds;
vector<func_decl_set> assrtn_fds;
do {
for (unsigned d = 0; d < m_core_extend_patterns_max_distance; d++) {
new_core_literals.reset();
unsigned sz = core.size();
@ -308,8 +311,10 @@ namespace smt {
}
core.append(new_core_literals.size(), new_core_literals.c_ptr());
if (new_core_literals.empty())
break;
}
while (!new_core_literals.empty());
}
};
};