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

fix #1762, #1764, #1768

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-07-26 20:29:26 +01:00
parent 259d4c4e43
commit d74978c277
15 changed files with 32 additions and 42 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1675,7 +1675,6 @@ def Or(*args):
class PatternRef(ExprRef):
"""Patterns are hints for quantifier instantiation.
See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
"""
def as_ast(self):
return Z3_pattern_to_ast(self.ctx_ref(), self.ast)
@ -1686,8 +1685,6 @@ class PatternRef(ExprRef):
def is_pattern(a):
"""Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation.
See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
>>> f = Function('f', IntSort(), IntSort())
>>> x = Int('x')
>>> q = ForAll(x, f(x) == 0, patterns = [ f(x) ])
@ -1705,8 +1702,6 @@ def is_pattern(a):
def MultiPattern(*args):
"""Create a Z3 multi-pattern using the given expressions `*args`
See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
>>> f = Function('f', IntSort(), IntSort())
>>> g = Function('g', IntSort(), IntSort())
>>> x = Int('x')
@ -1966,8 +1961,6 @@ def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations.
See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
>>> f = Function('f', IntSort(), IntSort(), IntSort())
>>> x = Int('x')
>>> y = Int('y')
@ -1985,7 +1978,6 @@ def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations.
See http://rise4fun.com/Z3Py/tutorial/advanced for more details.
>>> f = Function('f', IntSort(), IntSort(), IntSort())
>>> x = Int('x')

8
src/opt/opt_context.cpp
View file

@ -1012,8 +1012,7 @@ namespace opt {
}
}
// fix types of objectives:
for (unsigned i = 0; i < m_objectives.size(); ++i) {
objective & obj = m_objectives[i];
for (objective & obj : m_objectives) {
expr* t = obj.m_term;
switch(obj.m_type) {
case O_MINIMIZE:
@ -1189,13 +1188,12 @@ namespace opt {
void context::update_bound(bool is_lower) {
expr_ref val(m);
if (!m_model.get()) return;
for (unsigned i = 0; i < m_objectives.size(); ++i) {
objective const& obj = m_objectives[i];
for (objective const& obj : m_objectives) {
rational r;
switch(obj.m_type) {
case O_MINIMIZE: {
val = (*m_model)(obj.m_term);
TRACE("opt", tout << obj.m_term << " " << val << " " << is_numeral(val, r) << "\n";);
TRACE("opt", tout << obj.m_term << " " << val << "\n";);
if (is_numeral(val, r)) {
inf_eps val = inf_eps(obj.m_adjust_value(r));
TRACE("opt", tout << "adjusted value: " << val << "\n";);

24
src/smt/mam.cpp
View file

@ -405,7 +405,7 @@ namespace smt {
unsigned m_num_regs;
unsigned m_num_choices;
instruction * m_root;
obj_hashtable<enode> m_candidates;
enode_vector m_candidates;
#ifdef Z3DEBUG
context * m_context;
ptr_vector<app> m_patterns;
@ -539,7 +539,7 @@ namespace smt {
}
void add_candidate(enode * n) {
m_candidates.insert(n);
m_candidates.push_back(n);
}
bool has_candidates() const {
@ -550,7 +550,7 @@ namespace smt {
m_candidates.reset();
}
obj_hashtable<enode> const & get_candidates() const {
enode_vector const & get_candidates() const {
return m_candidates;
}
@ -1978,10 +1978,10 @@ namespace smt {
#define INIT_ARGS_SIZE 16
public:
interpreter(context & ctx, mam & m, bool use_filters):
interpreter(context & ctx, mam & ma, bool use_filters):
m_context(ctx),
m_ast_manager(ctx.get_manager()),
m_mam(m),
m_mam(ma),
m_use_filters(use_filters) {
m_args.resize(INIT_ARGS_SIZE);
}
@ -2001,7 +2001,6 @@ namespace smt {
TRACE("trigger_bug", tout << "execute for code tree:\n"; t->display(tout););
init(t);
if (t->filter_candidates()) {
//t->display(std::cout << "ncf: " << t->get_candidates().size() << "\n");
for (enode* app : t->get_candidates()) {
TRACE("trigger_bug", tout << "candidate\n" << mk_ismt2_pp(app->get_owner(), m_ast_manager) << "\n";);
if (!app->is_marked() && app->is_cgr()) {
@ -2016,9 +2015,6 @@ namespace smt {
}
}
else {
//t->display(std::cout << "ncu: " << t->get_candidates().size() << "\n");
//for (enode* app : t->get_candidates()) { std::cout << expr_ref(app->get_owner(), m_ast_manager) << "\n"; }
//std::cout.flush();
for (enode* app : t->get_candidates()) {
TRACE("trigger_bug", tout << "candidate\n" << mk_ismt2_pp(app->get_owner(), m_ast_manager) << "\n";);
if (app->is_cgr()) {
@ -2842,7 +2838,7 @@ namespace smt {
mk_tree_trail(ptr_vector<code_tree> & t, unsigned id):m_trees(t), m_lbl_id(id) {}
void undo(mam_impl & m) override {
dealloc(m_trees[m_lbl_id]);
m_trees[m_lbl_id] = 0;
m_trees[m_lbl_id] = nullptr;
}
};
@ -2875,8 +2871,8 @@ namespace smt {
app * p = to_app(mp->get_arg(first_idx));
func_decl * lbl = p->get_decl();
unsigned lbl_id = lbl->get_decl_id();
m_trees.reserve(lbl_id+1, 0);
if (m_trees[lbl_id] == 0) {
m_trees.reserve(lbl_id+1, nullptr);
if (m_trees[lbl_id] == nullptr) {
m_trees[lbl_id] = m_compiler.mk_tree(qa, mp, first_idx, false);
SASSERT(m_trees[lbl_id]->expected_num_args() == p->get_num_args());
DEBUG_CODE(m_trees[lbl_id]->set_context(m_context););
@ -2961,7 +2957,7 @@ namespace smt {
m_ground_arg(ground_arg),
m_pattern_idx(pat_idx),
m_child(child) {
SASSERT(ground_arg != 0 || ground_arg_idx == 0);
SASSERT(ground_arg != nullptr || ground_arg_idx == 0);
}
};
@ -3228,7 +3224,7 @@ namespace smt {
path_tree * mk_path_tree(path * p, quantifier * qa, app * mp) {
SASSERT(m_ast_manager.is_pattern(mp));
SASSERT(p != 0);
SASSERT(p != nullptr);
unsigned pat_idx = p->m_pattern_idx;
path_tree * head = nullptr;
path_tree * curr = nullptr;

2
src/smt/params/theory_arith_params.h
View file

@ -19,7 +19,7 @@ Revision History:
#ifndef THEORY_ARITH_PARAMS_H_
#define THEORY_ARITH_PARAMS_H_
#include<limits.h>
#include<climits>
#include "util/params.h"
enum arith_solver_id {

5
src/smt/theory_lra.cpp
View file

@ -2648,6 +2648,7 @@ public:
else {
rational r = get_value(v);
TRACE("arith", tout << "v" << v << " := " << r << "\n";);
SASSERT(!a.is_int(o) || r.is_int());
if (a.is_int(o) && !r.is_int()) r = floor(r);
return alloc(expr_wrapper_proc, m_factory->mk_value(r, m.get_sort(o)));
}
@ -2797,6 +2798,7 @@ public:
lp::var_index vi = m_theory_var2var_index[v];
st = m_solver->maximize_term(vi, term_max);
}
TRACE("arith", display(tout << st << " v" << v << "\n"););
switch (st) {
case lp::lp_status::OPTIMAL: {
inf_rational val(term_max.x, term_max.y);
@ -2804,13 +2806,12 @@ public:
return inf_eps(rational::zero(), val);
}
case lp::lp_status::FEASIBLE: {
inf_rational val(term_max.x, term_max.y);
inf_rational val = get_value(v);
blocker = mk_gt(v);
return inf_eps(rational::zero(), val);
}
default:
SASSERT(st == lp::lp_status::UNBOUNDED);
TRACE("arith", tout << "Unbounded v" << v << "\n";);
has_shared = false;
blocker = m.mk_false();
return inf_eps(rational::one(), inf_rational());

2
src/util/approx_nat.h
View file

@ -21,7 +21,7 @@ Notes:
#define APPROX_NAT_H_
#include<iostream>
#include<limits.h>
#include<limits>
class approx_nat {
unsigned m_value;

2
src/util/bit_vector.cpp
View file

@ -16,7 +16,7 @@ Author:
Revision History:
--*/
#include<limits.h>
#include<climits>
#include "util/bit_vector.h"
#include "util/trace.h"

2
src/util/fixed_bit_vector.cpp
View file

@ -19,7 +19,7 @@ Revision History:
--*/
#include<limits.h>
#include<climits>
#include "util/fixed_bit_vector.h"
#include "util/trace.h"
#include "util/hash.h"

4
src/util/hashtable.h
View file

@ -19,9 +19,9 @@ Revision History:
#ifndef HASHTABLE_H_
#define HASHTABLE_H_
#include "util/debug.h"
#include<ostream>
#include <ostream>
#include "util/util.h"
#include<limits.h>
#include <climits>
#include "util/memory_manager.h"
#include "util/hash.h"
#include "util/vector.h"

8
src/util/lp/lar_solver.cpp
View file

@ -538,12 +538,16 @@ lp_status lar_solver::maximize_term(unsigned ext_j,
if (column_value_is_integer(j))
continue;
if (m_int_solver->is_base(j)) {
if (!remove_from_basis(j)) // consider a special version of remove_from_basis that would not remove inf_int columns
if (!remove_from_basis(j)) { // consider a special version of remove_from_basis that would not remove inf_int columns
m_mpq_lar_core_solver.m_r_x = backup;
return lp_status::FEASIBLE; // it should not happen
}
}
m_int_solver->patch_nbasic_column(j, false);
if (!column_value_is_integer(j))
if (!column_value_is_integer(j)) {
m_mpq_lar_core_solver.m_r_x = backup;
return lp_status::FEASIBLE;
}
change = true;
}
if (change) {

2
src/util/memory_manager.cpp
View file

@ -6,7 +6,7 @@ Copyright (c) 2015 Microsoft Corporation
#include<iostream>
#include<stdlib.h>
#include<limits.h>
#include<climits>
#include "util/trace.h"
#include "util/memory_manager.h"
#include "util/error_codes.h"

1
src/util/mpz.h
View file

@ -19,7 +19,6 @@ Revision History:
#ifndef MPZ_H_
#define MPZ_H_
#include<limits.h>
#include<string>
#include "util/util.h"
#include "util/small_object_allocator.h"

2
src/util/nat_set.h
View file

@ -19,7 +19,7 @@ Revision History:
#ifndef NAT_SET_H_
#define NAT_SET_H_
#include<limits.h>
#include <climits>
#include "util/vector.h"
class nat_set {

2
src/util/scoped_timer.cpp
View file

@ -50,7 +50,7 @@ Revision History:
#undef max
#endif
#include "util/util.h"
#include<limits.h>
#include<climits>
#include "util/z3_omp.h"
struct scoped_timer::imp {

2
src/util/symbol.h
View file

@ -19,7 +19,7 @@ Revision History:
#ifndef SYMBOL_H_
#define SYMBOL_H_
#include<ostream>
#include<limits.h>
#include<climits>
#include "util/util.h"
#include "util/tptr.h"