diff options
| -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 | ||||
| -rw-r--r-- | test/regress/Makefile.tests | 1 | ||||
| -rw-r--r-- | test/regress/regress1/bv/bv2nat-types.smt2 | 7 |
5 files changed, 56 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 { diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index c15e3d045..0b9e415fa 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1045,6 +1045,7 @@ REG1_TESTS = \ regress1/bv/bv-proof00.smt \ regress1/bv/bv2nat-ground.smt2 \ regress1/bv/bv2nat-simp-range-sat.smt2 \ + regress1/bv/bv2nat-types.smt2 \ regress1/bv/cmu-rdk-3.smt2 \ regress1/bv/decision-weight00.smt2 \ regress1/bv/divtest.smt2 \ diff --git a/test/regress/regress1/bv/bv2nat-types.smt2 b/test/regress/regress1/bv/bv2nat-types.smt2 new file mode 100644 index 000000000..e75ffb3ca --- /dev/null +++ b/test/regress/regress1/bv/bv2nat-types.smt2 @@ -0,0 +1,7 @@ +(set-logic QF_ALL) +(set-info :status sat) +(declare-fun x () (_ BitVec 8)) +(assert +(= (concat #b000000000000000000000000 x) ((_ int2bv 32) (bv2nat x))) +) +(check-sat) |