From 6cde6bda109b2005faa01650a50a74eafa557c20 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Mon, 4 Dec 2017 10:43:40 -0800 Subject: [PATCH] Fix side condition for BITVECTOR_MULT. (#1422) --- src/theory/quantifiers/bv_inverter.cpp | 36 ++++++++++++++++++++++---- 1 file changed, 31 insertions(+), 5 deletions(-) diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp index d777dc4f8..b5d36eae4 100644 --- a/src/theory/quantifiers/bv_inverter.cpp +++ b/src/theory/quantifiers/bv_inverter.cpp @@ -281,6 +281,8 @@ Node BvInverter::solve_bv_lit(Node sv, sc = nm->mkNode(NOT, nm->mkNode(k, t, x)); } } + Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc + << std::endl; status.d_conds.push_back(sc); /* t = skv (fresh skolem constant) */ Node skv = getInversionNode(sc, solve_tn, m); @@ -337,6 +339,8 @@ Node BvInverter::solve_bv_lit(Node sv, sc = nm->mkNode(NOT, nm->mkNode(k, t, x)); } } + Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc + << std::endl; status.d_conds.push_back(sc); /* t = skv (fresh skolem constant) */ Node skv = getInversionNode(sc, solve_tn, m); @@ -370,6 +374,8 @@ Node BvInverter::solve_bv_lit(Node sv, nm->mkNode(DISTINCT, t, bv::utils::mkOnes(w))); Node scr = nm->mkNode(DISTINCT, x, t); Node sc = nm->mkNode(IMPLIES, scl, scr); + Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc + << std::endl; status.d_conds.push_back(sc); /* t = skv (fresh skolem constant) */ Node skv = getInversionNode(sc, solve_tn, m); @@ -452,18 +458,25 @@ Node BvInverter::solve_bv_lit(Node sv, /* with side condition: * ctz(t) >= ctz(s) <-> x * s = t * where - * ctz(t) >= ctz(s) -> (t & -t) >= (s & -s) */ + * ctz(t) >= ctz(s) -> t = 0 \/ ((t & -t) >= (s & -s) /\ s != 0) */ TypeNode solve_tn = sv_t[index].getType(); Node x = getSolveVariable(solve_tn); + Node zero = bv::utils::mkZero(bv::utils::getSize(s)); /* left hand side of side condition */ - Node scl = nm->mkNode( - BITVECTOR_UGE, - nm->mkNode(BITVECTOR_AND, t, nm->mkNode(BITVECTOR_NEG, t)), - nm->mkNode(BITVECTOR_AND, s, nm->mkNode(BITVECTOR_NEG, s))); + Node t_uge_s = nm->mkNode( + BITVECTOR_UGE, + nm->mkNode(BITVECTOR_AND, t, nm->mkNode(BITVECTOR_NEG, t)), + nm->mkNode(BITVECTOR_AND, s, nm->mkNode(BITVECTOR_NEG, s))); + Node scl = + nm->mkNode(OR, + t.eqNode(zero), + nm->mkNode(AND, t_uge_s, s.eqNode(zero).notNode())); /* right hand side of side condition */ Node scr = nm->mkNode(EQUAL, nm->mkNode(BITVECTOR_MULT, x, s), t); /* overall side condition */ Node sc = nm->mkNode(IMPLIES, scl, scr); + Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc + << std::endl; /* add side condition */ status.d_conds.push_back(sc); @@ -510,6 +523,8 @@ Node BvInverter::solve_bv_lit(Node sv, scr = nm->mkNode(EQUAL, nm->mkNode(BITVECTOR_UREM_TOTAL, s, x), t); } Node sc = nm->mkNode(IMPLIES, scl, scr); + Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc + << std::endl; status.d_conds.push_back(sc); Node skv = getInversionNode(sc, solve_tn, m); t = skv; @@ -559,6 +574,9 @@ Node BvInverter::solve_bv_lit(Node sv, /* overall side condition */ Node sc = nm->mkNode(IMPLIES, scl, scr); + Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc + << std::endl; + status.d_conds.push_back(sc); /* add side condition */ status.d_conds.push_back(sc); @@ -581,6 +599,8 @@ Node BvInverter::solve_bv_lit(Node sv, Node scl = nm->mkNode(EQUAL, t, nm->mkNode(k, t, s)); Node scr = nm->mkNode(EQUAL, nm->mkNode(k, x, s), t); Node sc = nm->mkNode(IMPLIES, scl, scr); + Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc + << std::endl; status.d_conds.push_back(sc); /* t = skv (fresh skolem constant) */ Node skv = getInversionNode(sc, solve_tn, m); @@ -617,6 +637,8 @@ Node BvInverter::solve_bv_lit(Node sv, nm->mkNode(EQUAL, ext, z)); scr = nm->mkNode(EQUAL, nm->mkNode(BITVECTOR_LSHR, x, s), t); Node sc = nm->mkNode(IMPLIES, scl, scr); + Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc + << std::endl; status.d_conds.push_back(sc); /* t = skv (fresh skolem constant) */ Node skv = getInversionNode(sc, solve_tn, m); @@ -661,6 +683,8 @@ Node BvInverter::solve_bv_lit(Node sv, nm->mkNode(EQUAL, ext, s2)); scr = nm->mkNode(EQUAL, nm->mkNode(BITVECTOR_LSHR, x, s), t); Node sc = nm->mkNode(IMPLIES, scl, scr); + Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc + << std::endl; status.d_conds.push_back(sc); /* t = skv (fresh skolem constant) */ Node skv = getInversionNode(sc, solve_tn, m); @@ -728,6 +752,8 @@ Node BvInverter::solve_bv_lit(Node sv, /* overall side condition */ Node sc = nm->mkNode(IMPLIES, scl, scr); + Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc + << std::endl; /* add side condition */ status.d_conds.push_back(sc); -- 2.30.2