From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 1 Aug 2018 17:22:09 +0000 (-0500)
Subject: Fix issues with bv2nat (#2219)
X-Git-Tag: cvc5-1.0.0~4838
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0aa6e039827750757941751e0829575a55601ace;p=cvc5.git

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.
---

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)