mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

add special procedures for UTVPI and horn arithmetic

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-04-28 13:37:03 -07:00
parent e6d6c55df0
commit be64e4b238
2 changed files with 7 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

24
src/smt/theory_horn_ineq.h
View file

@ -6,30 +6,16 @@ Module Name:
theory_horn_ineq.h theory_horn_ineq.h
Abstract: Abstract:
A*x <= b + D*x, coefficients to A and D are non-negative, A*x <= weight + D*x, coefficients to A and D are non-negative,
D is a diagonal matrix. D is a diagonal matrix.
Coefficients to b may have both signs. Coefficients to weight may have both signs.
Ford-Fulkerson variant:
Label variables by weight. Label variables by weight.
Select inequality that is not satisfied. Select inequality that is not satisfied.
Set gamma(LHS) := 0 Set delta(LHS) := 0
Set gamma(RHS(x)) := weight(x) - b Set delta(RHS(x)) := weight(x) - b
Propagate gamma through inequalities. Propagate weight increment through inequalities.
Gamma is the increment.
Maintain Heap of variables weighted by gamma.
When processing inequality,
then update gamma of variables by gamma := A(gamma + weight) - b
If some variable in the premise of the original rule gets
relabeled (assignment is increased), then the set of
inequalities is unsatisfiable.
Propagation updates lower bounds on gamma by taking into
account integer inequalities. The greatest lower bound
is computable by taking integer floor/ceilings.
Author: Author:

6
src/smt/theory_horn_ineq_def.h
View file

@ -937,10 +937,8 @@ namespace smt {
template<typename Ext> template<typename Ext>
void theory_horn_ineq<Ext>::collect_statistics(::statistics& st) const { void theory_horn_ineq<Ext>::collect_statistics(::statistics& st) const {
st.update("hi conflicts", m_stats.m_num_conflicts); st.update("horn ineq conflicts", m_stats.m_num_conflicts);
// st.update("hi propagations", m_stats.m_num_th2core_prop); st.update("horn ineq assertions", m_stats.m_num_assertions);
// st.update("hi asserts", m_stats.m_num_assertions);
// st.update("core->hi eqs", m_stats.m_num_core2th_eqs);
m_arith_eq_adapter.collect_statistics(st); m_arith_eq_adapter.collect_statistics(st);
m_graph->collect_statistics(st); m_graph->collect_statistics(st);
} }