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

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-01-31 16:36:55 -08:00
parent 46f754c43d
commit 4dfdabc80f
3 changed files with 2 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/smt/q_ematch.h
View file

@ -127,7 +127,7 @@ namespace q {
void on_binding(quantifier* q, app* pat, euf::enode* const* binding, unsigned max_generation, unsigned min_gen, unsigned max_gen); void on_binding(quantifier* q, app* pat, euf::enode* const* binding, unsigned max_generation, unsigned min_gen, unsigned max_gen);
// callback from queue // callback from queue
lbool eval(euf::enode* const* binding, clause& c) { return m_eval(binding, c); } lbool evaluate(euf::enode* const* binding, clause& c) { return m_eval(binding, c); }
void add_instantiation(clause& c, binding& b, sat::literal lit); void add_instantiation(clause& c, binding& b, sat::literal lit);
bool propagate(euf::enode* const* binding, unsigned max_generation, clause& c); bool propagate(euf::enode* const* binding, unsigned max_generation, clause& c);

3
src/sat/smt/q_queue.cpp
View file

@ -137,7 +137,6 @@ namespace q {
void queue::instantiate(entry& ent) { void queue::instantiate(entry& ent) {
fingerprint & f = *ent.m_qb; fingerprint & f = *ent.m_qb;
quantifier * q = f.q(); quantifier * q = f.q();
unsigned generation = f.m_max_generation;
unsigned num_bindings = f.size(); unsigned num_bindings = f.size();
euf::enode * const * bindings = f.nodes(); euf::enode * const * bindings = f.nodes();
q::quantifier_stat * stat = f.c->m_stat; q::quantifier_stat * stat = f.c->m_stat;
@ -181,7 +180,7 @@ namespace q {
if (curr.m_cost <= m_eager_cost_threshold) if (curr.m_cost <= m_eager_cost_threshold)
instantiate(curr); instantiate(curr);
else if (m_params.m_qi_promote_unsat && l_false == em.eval(f.nodes(), *f.c)) { else if (m_params.m_qi_promote_unsat && l_false == em.evaluate(f.nodes(), *f.c)) {
// do not delay instances that produce a conflict. // do not delay instances that produce a conflict.
TRACE("q", tout << "promoting instance that produces a conflict\n" << mk_pp(f.q(), m) << "\n";); TRACE("q", tout << "promoting instance that produces a conflict\n" << mk_pp(f.q(), m) << "\n";);
instantiate(curr); instantiate(curr);

8
src/util/zstring.cpp
View file

@ -33,14 +33,6 @@ static bool is_hex_digit(char ch, unsigned& d) {
return false; return false;
} }
static bool is_octal_digit(char ch, unsigned& d) {
if ('0' <= ch && ch <= '7') {
d = ch - '0';
return true;
}
return false;
}
bool zstring::is_escape_char(char const *& s, unsigned& result) { bool zstring::is_escape_char(char const *& s, unsigned& result) {
unsigned d; unsigned d;
if (*s == '\\' && *(s+1) == 'u' && *(s+2) == '{') { if (*s == '\\' && *(s+1) == 'u' && *(s+2) == '{') {