mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 04:48:45 +00:00
Code Activity

fix build

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-02-21 22:18:47 +09:00
parent b3fa5d7978
commit 7b6f51941c
3 changed files with 10 additions and 19 deletions
src
api/python/z3
z3.py
muz/transforms
dl_mk_rule_inliner.cpp
util/lp
permutation_matrix.h

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

@ -7453,7 +7453,7 @@ def WithParams(t, p):
>>> x, y = Ints('x y')
>>> p = ParamsRef()
>>> p.set("som", True)
>>> t = With(Tactic('simplify'), p)
>>> t = WithParams(Tactic('simplify'), p)
>>> t((x + 1)*(y + 2) == 0)
[[2*x + y + x*y == -2]]
"""

17
src/muz/transforms/dl_mk_rule_inliner.cpp
View file

@ -210,8 +210,7 @@ namespace datalog {
}
rule_set::iterator rend = orig.end();
for (rule_set::iterator rit = orig.begin(); rit!=rend; ++rit) {
rule * r = *rit;
for (rule * r : orig) {
func_decl * head_pred = r->get_decl();
m_head_pred_ctr.inc(head_pred);
@ -283,9 +282,7 @@ namespace datalog {
const rule_stratifier::comp_vector& comps = r.get_stratifier().get_strats();
rule_stratifier::comp_vector::const_iterator cend = comps.end();
for (rule_stratifier::comp_vector::const_iterator it = comps.begin(); it!=cend; ++it) {
rule_stratifier::item_set * stratum = *it;
for (rule_stratifier::item_set * stratum : comps) {
if (stratum->size()==1) {
continue;
}
@ -307,9 +304,7 @@ namespace datalog {
const rule_stratifier::comp_vector& comps =
proposed_inlined_rules.get_stratifier().get_strats();
rule_stratifier::comp_vector::const_iterator cend = comps.end();
for (rule_stratifier::comp_vector::const_iterator it = comps.begin(); it!=cend; ++it) {
rule_stratifier::item_set * stratum = *it;
for (rule_stratifier::item_set * stratum : comps) {
SASSERT(stratum->size()==1);
func_decl * head_pred = *stratum->begin();
@ -318,10 +313,7 @@ namespace datalog {
bool is_multi_occurrence_pred = m_tail_pred_ctr.get(head_pred)>1;
const rule_vector& pred_rules = proposed_inlined_rules.get_predicate_rules(head_pred);
rule_vector::const_iterator iend = pred_rules.end();
for (rule_vector::const_iterator iit = pred_rules.begin(); iit!=iend; ++iit) {
rule * r = *iit;
for (rule * r : pred_rules) {
unsigned pt_len = r->get_positive_tail_size();
for (unsigned ti = 0; ti<pt_len; ++ti) {
func_decl * tail_pred = r->get_decl(ti);
@ -409,7 +401,6 @@ namespace datalog {
const rule_stratifier::comp_vector& comps = candidate_inlined_set->get_stratifier().get_strats();
rule_stratifier::comp_vector::const_iterator cend = comps.end();
for (rule_stratifier::item_set * stratum : comps) {
SASSERT(stratum->size()==1);
func_decl * pred = *stratum->begin();

10
src/util/lp/permutation_matrix.h
View file

@ -109,13 +109,13 @@ class permutation_matrix : public tail_matrix<T, X> {
void transpose_from_right(unsigned i, unsigned j);
#ifdef Z3DEBUG
T get_elem(unsigned i, unsigned j) const{
T get_elem(unsigned i, unsigned j) const override {
return m_permutation[i] == j? numeric_traits<T>::one() : numeric_traits<T>::zero();
}
unsigned row_count() const{ return size(); }
unsigned column_count() const { return size(); }
virtual void set_number_of_rows(unsigned /*m*/) { }
virtual void set_number_of_columns(unsigned /*n*/) { }
unsigned row_count() const override { return size(); }
unsigned column_count() const override { return size(); }
void set_number_of_rows(unsigned /*m*/) override { }
void set_number_of_columns(unsigned /*n*/) override { }
#endif
void multiply_by_permutation_from_left(permutation_matrix<T, X> & p);