mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-08-24 02:20:30 -07:00
parent 6beec7b642
commit e46ad45968
4 changed files with 8 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/lp_bound_propagator.h
View file

@ -190,7 +190,7 @@ public:
void try_add_equation_with_lp_fixed_tables(const vertex *v) { void try_add_equation_with_lp_fixed_tables(const vertex *v) {
SASSERT(m_fixed_vertex); SASSERT(m_fixed_vertex);
unsigned v_j = v->column(); unsigned v_j = v->column();
unsigned j; unsigned j = null_lpvar;
if (!lp().find_in_fixed_tables(val(v_j), is_int(v_j), j)) if (!lp().find_in_fixed_tables(val(v_j), is_int(v_j), j))
return; return;
TRACE("cheap_eq", tout << "found j=" << j << " for v="; TRACE("cheap_eq", tout << "found j=" << j << " for v=";

7
src/smt/smt_quantifier.cpp
View file

@ -206,9 +206,9 @@ namespace smt {
} }
void log_causality( void log_causality(
fingerprint* f, fingerprint* f,
app * pat, app * pat,
vector<std::tuple<enode *, enode *>> & used_enodes) { vector<std::tuple<enode *, enode *>> & used_enodes) {
if (pat != nullptr) { if (pat != nullptr) {
if (used_enodes.size() > 0) { if (used_enodes.size() > 0) {
@ -219,6 +219,7 @@ namespace smt {
for (auto n : used_enodes) { for (auto n : used_enodes) {
enode *orig = std::get<0>(n); enode *orig = std::get<0>(n);
enode *substituted = std::get<1>(n); enode *substituted = std::get<1>(n);
(void) substituted;
if (orig == nullptr) { if (orig == nullptr) {
STRACE("causality", tout << " #" << substituted->get_owner_id();); STRACE("causality", tout << " #" << substituted->get_owner_id(););
} }

1
src/smt/theory_bv.cpp
View file

@ -1139,7 +1139,6 @@ namespace smt {
bool_var watch_var = null_bool_var; bool_var watch_var = null_bool_var;
it1 = bits1.begin(); it1 = bits1.begin();
it2 = bits2.begin(); it2 = bits2.begin();
unsigned h = hash_u_u(v1, v2);
unsigned act = m_diseq_activity[hash_u_u(v1, v2) & 0xFF]++; unsigned act = m_diseq_activity[hash_u_u(v1, v2) & 0xFF]++;
for (; it1 != end1 && ((act & 0x3) != 0x3); ++it1, ++it2) { for (; it1 != end1 && ((act & 0x3) != 0x3); ++it1, ++it2) {

5
src/test/egraph.cpp
View file

@ -3,6 +3,7 @@ Copyright (c) 2020 Microsoft Corporation
--*/ --*/
#include "util/util.h"
#include "util/timer.h" #include "util/timer.h"
#include "ast/euf/euf_egraph.h" #include "ast/euf/euf_egraph.h"
#include "ast/reg_decl_plugins.h" #include "ast/reg_decl_plugins.h"
@ -15,13 +16,13 @@ static expr_ref mk_const(ast_manager& m, char const* name, sort* s) {
static expr_ref mk_app(char const* name, expr_ref const& arg, sort* s) { static expr_ref mk_app(char const* name, expr_ref const& arg, sort* s) {
ast_manager& m = arg.m(); ast_manager& m = arg.m();
func_decl_ref f(m.mk_func_decl(symbol(name), m.get_sort(arg), s), m); func_decl_ref f(m.mk_func_decl(symbol(name), m.get_sort(arg), s), m);
return expr_ref(m.mk_app(f, arg), m); return expr_ref(m.mk_app(f, arg.get()), m);
} }
static expr_ref mk_app(char const* name, expr_ref const& arg1, expr_ref const& arg2, sort* s) { static expr_ref mk_app(char const* name, expr_ref const& arg1, expr_ref const& arg2, sort* s) {
ast_manager& m = arg1.m(); ast_manager& m = arg1.m();
func_decl_ref f(m.mk_func_decl(symbol(name), m.get_sort(arg1), m.get_sort(arg2), s), m); func_decl_ref f(m.mk_func_decl(symbol(name), m.get_sort(arg1), m.get_sort(arg2), s), m);
return expr_ref(m.mk_app(f, arg1, arg2), m); return expr_ref(m.mk_app(f, arg1.get(), arg2.get()), m);
} }
static void test1() { static void test1() {