From be64e4b238c097f20862502685b01e3f8a0caf88 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 28 Apr 2013 13:37:03 -0700 Subject: [PATCH] add special procedures for UTVPI and horn arithmetic Signed-off-by: Nikolaj Bjorner --- src/smt/theory_horn_ineq.h | 24 +++++------------------- src/smt/theory_horn_ineq_def.h | 6 ++---- 2 files changed, 7 insertions(+), 23 deletions(-) diff --git a/src/smt/theory_horn_ineq.h b/src/smt/theory_horn_ineq.h index f5fb41263..441e46a18 100644 --- a/src/smt/theory_horn_ineq.h +++ b/src/smt/theory_horn_ineq.h @@ -6,30 +6,16 @@ Module Name: theory_horn_ineq.h 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. - Coefficients to b may have both signs. - + Coefficients to weight may have both signs. - Ford-Fulkerson variant: Label variables by weight. Select inequality that is not satisfied. - Set gamma(LHS) := 0 - Set gamma(RHS(x)) := weight(x) - b - Propagate gamma 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. + Set delta(LHS) := 0 + Set delta(RHS(x)) := weight(x) - b + Propagate weight increment through inequalities. Author: diff --git a/src/smt/theory_horn_ineq_def.h b/src/smt/theory_horn_ineq_def.h index b86d45819..1fc51a86c 100644 --- a/src/smt/theory_horn_ineq_def.h +++ b/src/smt/theory_horn_ineq_def.h @@ -937,10 +937,8 @@ namespace smt { template void theory_horn_ineq::collect_statistics(::statistics& st) const { - st.update("hi conflicts", m_stats.m_num_conflicts); -// st.update("hi propagations", m_stats.m_num_th2core_prop); -// st.update("hi asserts", m_stats.m_num_assertions); -// st.update("core->hi eqs", m_stats.m_num_core2th_eqs); + st.update("horn ineq conflicts", m_stats.m_num_conflicts); + st.update("horn ineq assertions", m_stats.m_num_assertions); m_arith_eq_adapter.collect_statistics(st); m_graph->collect_statistics(st); }