mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
add pdd_interval to evaluate intervals of pdd expressions
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
parent
fffd764226
commit
1d217595c8
72
src/math/dd/pdd_interval.h
Normal file
72
src/math/dd/pdd_interval.h
Normal file
|
@ -0,0 +1,72 @@
|
|||
/*++
|
||||
Copyright (c) 2019 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
dd_pdd.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
Poly DD package
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2019-12-24
|
||||
Lev Nachmanson (levnach) 2019-12-24
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
#include "math/dd/dd_pdd.h"
|
||||
#include "math/interval/dep_intervals.h"
|
||||
|
||||
namespace dd {
|
||||
typedef dep_intervals::interval interval;
|
||||
typedef dep_intervals::with_deps_t w_dep;
|
||||
// calculates the interval of a pdd expression based on the given intervals of the variables
|
||||
class pdd_interval {
|
||||
pdd_manager& m;
|
||||
dep_intervals m_dep_intervals;
|
||||
std::function<interval (unsigned, bool)> m_var2interval;
|
||||
|
||||
public:
|
||||
|
||||
pdd_interval(pdd_manager& m, reslimit& lim): m(m), m_dep_intervals(lim) {}
|
||||
|
||||
std::function<interval (unsigned, bool)>& var2interval() { return m_var2interval; } // setter
|
||||
const std::function<interval (unsigned, bool)>& var2interval() const { return m_var2interval; } // getter
|
||||
|
||||
template <w_dep wd>
|
||||
interval get_interval(pdd const& p) {
|
||||
interval k;
|
||||
if (p.is_val()) {
|
||||
m_dep_intervals.set_interval_for_scalar(k, p.val());
|
||||
return k;
|
||||
}
|
||||
bool deps = (wd == w_dep::with_deps);
|
||||
interval a = m_var2interval(p.var(), deps);
|
||||
interval hi = get_interval<wd>(p.hi());
|
||||
interval la = get_interval<wd>(p.lo());
|
||||
interval t;
|
||||
interval ret;
|
||||
if (deps) {
|
||||
interval_deps_combine_rule combine_rule;
|
||||
m_dep_intervals.add(hi, a, t, combine_rule);
|
||||
m_dep_intervals.combine_deps(hi, a, combine_rule, t);
|
||||
combine_rule.reset();
|
||||
m_dep_intervals.add(t, la, ret, combine_rule);
|
||||
m_dep_intervals.combine_deps(t, la, combine_rule, ret);
|
||||
return ret;
|
||||
} else {
|
||||
m_dep_intervals.mul(hi, a, t);
|
||||
m_dep_intervals.add(t, la, ret);
|
||||
return ret;
|
||||
}
|
||||
}
|
||||
|
||||
bool separated_from_zero(pdd const& p, u_dependency*& dep) {
|
||||
return m_dep_intervals.check_interval_for_conflict_on_zero((*this)(p), dep);
|
||||
}
|
||||
|
||||
};
|
||||
}
|
|
@ -332,5 +332,4 @@ public:
|
|||
|
||||
copy_upper_bound<wd>(b, i);
|
||||
}
|
||||
|
||||
};
|
||||
|
|
|
@ -107,6 +107,9 @@ inline deps_combine_rule dep1_to_dep2(deps_combine_rule d) {
|
|||
struct interval_deps_combine_rule {
|
||||
deps_combine_rule m_lower_combine;
|
||||
deps_combine_rule m_upper_combine;
|
||||
void reset() {
|
||||
m_lower_combine = m_upper_combine = 0;
|
||||
}
|
||||
};
|
||||
|
||||
template<typename C>
|
||||
|
|
|
@ -1,5 +1,6 @@
|
|||
#include "math/dd/dd_pdd.h"
|
||||
#include "math/dd/pdd_eval.h"
|
||||
#include "math/dd/pdd_interval.h"
|
||||
|
||||
namespace dd {
|
||||
static void test1() {
|
||||
|
|
Loading…
Reference in a new issue