diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-01 12:22:09 -0500 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-08-01 10:22:09 -0700 |
commit | 0aa6e039827750757941751e0829575a55601ace (patch) | |
tree | 25e21dfd16e232e07615791935bfc6c32fc5bcab /src | |
parent | b721666fd7a2dafaaeb112059c2588c99e8020ec (diff) |
Fix issues with bv2nat (#2219)
This includes:
- A missing case in the smt2 printer,
- A bug in an inference of int2bv applied to bv2nat where the types are different.
Diffstat (limited to 'src')
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 1 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 44 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 21 |
3 files changed, 48 insertions, 18 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 0e1df15b5..64a52c23f 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -971,6 +971,7 @@ static string smtKindString(Kind k, Variant v) case kind::BITVECTOR_SLE: return "bvsle"; case kind::BITVECTOR_SGT: return "bvsgt"; case kind::BITVECTOR_SGE: return "bvsge"; + case kind::BITVECTOR_TO_NAT: return "bv2nat"; case kind::BITVECTOR_REDOR: return "bvredor"; case kind::BITVECTOR_REDAND: return "bvredand"; diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index d19378f72..9ecbbc99c 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -477,28 +477,36 @@ bool TheoryBV::doExtfInferences(std::vector<Node>& terms) d_extf_collapse_infer.insert(cterm); Node t = n[0]; - if (n.getKind() == kind::INT_TO_BITVECTOR) + if (t.getType() == parent.getType()) { - Assert(t.getType().isInteger()); - // congruent modulo 2^( bv width ) - unsigned bvs = n.getType().getBitVectorSize(); - Node coeff = nm->mkConst(Rational(Integer(1).multiplyByPow2(bvs))); - Node k = nm->mkSkolem( - "int_bv_cong", t.getType(), "for int2bv/bv2nat congruence"); - t = nm->mkNode(kind::PLUS, t, nm->mkNode(kind::MULT, coeff, k)); - } - Node lem = parent.eqNode(t); + if (n.getKind() == kind::INT_TO_BITVECTOR) + { + Assert(t.getType().isInteger()); + // congruent modulo 2^( bv width ) + unsigned bvs = n.getType().getBitVectorSize(); + Node coeff = nm->mkConst(Rational(Integer(1).multiplyByPow2(bvs))); + Node k = nm->mkSkolem( + "int_bv_cong", t.getType(), "for int2bv/bv2nat congruence"); + t = nm->mkNode(kind::PLUS, t, nm->mkNode(kind::MULT, coeff, k)); + } + Node lem = parent.eqNode(t); - if (parent[0] != n) - { - Assert(ee->areEqual(parent[0], n)); - lem = nm->mkNode(kind::IMPLIES, parent[0].eqNode(n), lem); + if (parent[0] != n) + { + Assert(ee->areEqual(parent[0], n)); + lem = nm->mkNode(kind::IMPLIES, parent[0].eqNode(n), lem); + } + // this handles inferences of the form, e.g.: + // ((_ int2bv w) (bv2nat x)) == x (if x is bit-width w) + // (bv2nat ((_ int2bv w) x)) == x + k*2^w for some k + Trace("bv-extf-lemma") + << "BV extf lemma (collapse) : " << lem << std::endl; + d_out->lemma(lem); + sentLemma = true; } - Trace("bv-extf-lemma") - << "BV extf lemma (collapse) : " << lem << std::endl; - d_out->lemma(lem); - sentLemma = true; } + Trace("bv-extf-lemma-debug") + << "BV extf f collapse based on : " << cterm << std::endl; } } return sentLemma; diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index c48708126..05bb695e5 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -181,7 +181,28 @@ private: bool d_needsLastCallCheck; context::CDHashSet<Node, NodeHashFunction> d_extf_range_infer; context::CDHashSet<Node, NodeHashFunction> d_extf_collapse_infer; + /** do extended function inferences + * + * This method adds lemmas on the output channel of TheoryBV based on + * reasoning about extended functions, such as bv2nat and int2bv. Examples + * of lemmas added by this method include: + * 0 <= ((_ int2bv w) x) < 2^w + * ((_ int2bv w) (bv2nat x)) = x + * (bv2nat ((_ int2bv w) x)) == x + k*2^w + * The purpose of these lemmas is to recognize easy conflicts before fully + * reducing extended functions based on their full semantics. + */ bool doExtfInferences( std::vector< Node >& terms ); + /** do extended function reductions + * + * This method adds lemmas on the output channel of TheoryBV based on + * reducing all extended function applications that are preregistered to + * this theory and have not already been reduced by context-dependent + * simplification (see theory/ext_theory.h). Examples of lemmas added by + * this method include: + * (bv2nat x) = (ite ((_ extract w w-1) x) 2^{w-1} 0) + ... + + * (ite ((_ extract 1 0) x) 1 0) + */ bool doExtfReductions( std::vector< Node >& terms ); bool wasPropagatedBySubtheory(TNode literal) const { |