mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Nikolaj Bjorner 2013-03-18 21:46:48 -07:00
parent 7e9f4e264d d4d3ba104e
commit b8b73077a9
7 changed files with 50 additions and 73 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

73
src/muz_qe/dl_base.cpp
View file

@ -325,9 +325,20 @@ namespace datalog {
return res;
}
/**
\brief Default method for complementation.
It assumes that the compiler creates only tables with
at most one column (0 or 1 columns).
Complementation of tables with more than one columns
is transformed into a cross product of complements and/or
difference.
*/
table_base * table_base::complement(func_decl* p, const table_element * func_columns) const {
const table_signature & sig = get_signature();
SASSERT(sig.functional_columns()==0 || func_columns!=0);
SASSERT(sig.first_functional() <= 1);
table_base * res = get_plugin().mk_empty(sig);
@ -335,16 +346,14 @@ namespace datalog {
fact.resize(sig.first_functional());
fact.append(sig.functional_columns(), func_columns);
if(sig.first_functional()==0) {
if(empty()) {
if (sig.first_functional() == 0) {
if (empty()) {
res->add_fact(fact);
}
return res;
}
if(sig.first_functional()!=1) { //now we support only tables with one non-functional column
NOT_IMPLEMENTED_YET();
}
VERIFY(sig.first_functional() == 1);
uint64 upper_bound = get_signature()[0];
bool empty_table = empty();
@ -356,51 +365,13 @@ namespace datalog {
warning_msg(buffer.str().c_str());
}
for(table_element i=0; i<upper_bound; i++) {
fact[0]=i;
for(table_element i = 0; i < upper_bound; i++) {
fact[0] = i;
if(empty_table || !contains_fact(fact)) {
res->add_fact(fact);
}
}
return res;
#if 0
svector<unsigned> var_arg_indexes(arity);
var_arg_indexes.fill(0);
svector<unsigned> var_arg_domain_sizes = s;
unsigned var_cnt=var_arg_indexes.size();
table_fact fact;
fact.resize(arity);
fact.fill(0);
unsigned depth=arity;
while(true) {
if(depth==arity) {
SASSERT(!res->contains_fact(fact));
if(empty_table || !contains_fact(fact)) {
res->add_fact(fact);
}
depth--;
}
else if(fact[depth]==s[depth]-1) {
val_indexes[depth]=0;
if(depth==0) {
break;
}
depth--;
}
else {
SASSERT(val_indexes[depth]<var_arg_domain_sizes[depth]);
unsigned arg_idx = var_arg_indexes[depth];
unsigned val_idx = val_indexes[depth]++;
head_args[arg_idx]=ctx.get_arith().mk_numeral(rational(val_idx), true);
depth++;
}
}
return res;
#endif
}
void table_base::display(std::ostream & out) const {
@ -468,23 +439,21 @@ namespace datalog {
expr_ref_vector disjs(m);
expr_ref_vector conjs(m);
dl_decl_util util(m);
bool_rewriter brw(m);
table_fact fact;
iterator it = begin();
iterator iend = end();
for(; it!=iend; ++it) {
for(; it != iend; ++it) {
const row_interface & r = *it;
r.get_fact(fact);
conjs.reset();
for (unsigned i = 0; i < fact.size(); ++i) {
conjs.push_back(m.mk_eq(m.mk_var(i, sig[i]), util.mk_numeral(fact[i], sig[i])));
}
switch(conjs.size()) {
case 0: disjs.push_back(m.mk_true()); break;
case 1: disjs.push_back(conjs[0].get()); break;
default: disjs.push_back(m.mk_and(conjs.size(), conjs.c_ptr())); break;
}
brw.mk_and(conjs.size(), conjs.c_ptr(), fml);
disjs.push_back(fml);
}
bool_rewriter(m).mk_or(disjs.size(), disjs.c_ptr(), fml);
brw.mk_or(disjs.size(), disjs.c_ptr(), fml);
}
}

2
src/muz_qe/dl_mk_karr_invariants.cpp
View file

@ -325,7 +325,6 @@ namespace datalog {
TRACE("dl", m_hb.display(tout););
SASSERT(is_sat == l_true);
unsigned basis_size = m_hb.get_basis_size();
bool first_initial = true;
for (unsigned i = 0; i < basis_size; ++i) {
bool is_initial;
vector<rational> soln;
@ -378,7 +377,6 @@ namespace datalog {
}
void mk_karr_invariants::update_body(rule_set& rules, rule& r){
func_decl* p = r.get_decl();
unsigned utsz = r.get_uninterpreted_tail_size();
unsigned tsz = r.get_tail_size();
app_ref_vector tail(m);

15
src/muz_qe/dl_relation_manager.cpp
View file

@ -243,15 +243,14 @@ namespace datalog {
relation_plugin & relation_manager::get_appropriate_plugin(const relation_signature & s) {
relation_plugin * res = try_get_appropriate_plugin(s);
if(!res) {
if (!res) {
throw default_exception("no suitable plugin found for given relation signature");
throw 0;
}
return *res;
}
table_plugin * relation_manager::try_get_appropriate_plugin(const table_signature & t) {
if(m_favourite_table_plugin && m_favourite_table_plugin->can_handle_signature(t)) {
if (m_favourite_table_plugin && m_favourite_table_plugin->can_handle_signature(t)) {
return m_favourite_table_plugin;
}
table_plugin_vector::iterator tpit = m_table_plugins.begin();
@ -346,7 +345,7 @@ namespace datalog {
return p->mk_empty(s);
}
if(mk_empty_table_relation(s, res)) {
if (mk_empty_table_relation(s, res)) {
return res;
}
@ -884,10 +883,10 @@ namespace datalog {
SASSERT(plugin->can_handle_signature(res_sign));
table_base * res = plugin->mk_empty(res_sign);
unsigned t1cols=t1.get_signature().size();
unsigned t2cols=t2.get_signature().size();
unsigned t1first_func=t1.get_signature().first_functional();
unsigned t2first_func=t2.get_signature().first_functional();
unsigned t1cols = t1.get_signature().size();
unsigned t2cols = t2.get_signature().size();
unsigned t1first_func = t1.get_signature().first_functional();
unsigned t2first_func = t2.get_signature().first_functional();
table_base::iterator els1it = t1.begin();
table_base::iterator els1end = t1.end();

1
src/muz_qe/horn_tactic.cpp
View file

@ -169,7 +169,6 @@ class horn_tactic : public tactic {
SASSERT(g->is_well_sorted());
mc = 0; pc = 0; core = 0;
tactic_report report("horn", *g);
bool produce_models = g->models_enabled();
bool produce_proofs = g->proofs_enabled();
if (produce_proofs) {

11
src/muz_qe/rel_context.cpp
View file

@ -31,9 +31,6 @@ Revision History:
#include"dl_sparse_table.h"
#include"dl_table.h"
#include"dl_table_relation.h"
#ifndef _EXTERNAL_RELEASE
#include"dl_skip_table.h"
#endif
namespace datalog {
@ -44,16 +41,16 @@ namespace datalog {
m_answer(m),
m_cancel(false),
m_last_result_relation(0) {
// register plugins for builtin tables
get_rmanager().register_plugin(alloc(sparse_table_plugin, get_rmanager()));
get_rmanager().register_plugin(alloc(hashtable_table_plugin, get_rmanager()));
get_rmanager().register_plugin(alloc(bitvector_table_plugin, get_rmanager()));
get_rmanager().register_plugin(alloc(equivalence_table_plugin, get_rmanager()));
#ifndef _EXTERNAL_RELEASE
get_rmanager().register_plugin(alloc(skip_table_plugin, get_rmanager()));
#endif
//register plugins for builtin relations
// register plugins for builtin relations
get_rmanager().register_plugin(alloc(bound_relation_plugin, get_rmanager()));
get_rmanager().register_plugin(alloc(interval_relation_plugin, get_rmanager()));

19
src/smt/smt_model_finder.cpp
View file

@ -1535,8 +1535,23 @@ namespace smt {
n1->insert_exception(m_t);
}
virtual void populate_inst_sets(quantifier * q, auf_solver & s, context * ctx) {
// do nothing...
virtual void populate_inst_sets(quantifier * q, auf_solver & slv, context * ctx) {
unsigned num_vars = q->get_num_decls();
ast_manager & m = ctx->get_manager();
sort * s = q->get_decl_sort(num_vars - m_var_i - 1);
if (m.is_uninterp(s)) {
// For uninterpreted sorst, we add all terms in the context.
// See Section 4.1 in the paper "Complete Quantifier Instantiation"
node * S_q_i = slv.get_uvar(q, m_var_i);
ptr_vector<enode>::const_iterator it = ctx->begin_enodes();
ptr_vector<enode>::const_iterator end = ctx->end_enodes();
for (; it != end; ++it) {
enode * n = *it;
if (ctx->is_relevant(n) && get_sort(n->get_owner()) == s) {
S_q_i->insert(n->get_owner(), n->get_generation());
}
}
}
}
};

2
src/util/bit_vector.h
View file

@ -106,7 +106,7 @@ public:
}
bool empty() const {
return m_num_bits != 0;
return m_num_bits == 0;
}
unsigned num_words() const {