Refactor and fix solveBvLit for CBQI BV. (#1526)

This refactors and simplifies solveBvLit() and fixes the following:

- generate side conditions for BITVECTOR_NEG, BITVECTOR_NOT, BITVECTOR_PLUS,
BITVECTOR_XOR over inequalities and disequality
- fix CONCAT handling (generate side conditions rather then computing an inverse which was incorrect)
- fix SIGN_EXTEND handling (same as with CONCATs)

1 files changed, 304 insertions, 1 deletions

diff --git a/test/unit/theory/theory_quantifiers_bv_inverter_white.h b/test/unit/theory/theory_quantifiers_bv_inverter_white.h
index ba8dd1668..99595a543 100644
--- a/test/unit/theory/theory_quantifiers_bv_inverter_white.h
+++ b/test/unit/theory/theory_quantifiers_bv_inverter_white.h
@@ -126,6 +126,100 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite
     TS_ASSERT(res.d_sat == Result::UNSAT);
   }
 
+  void runTestConcat(bool pol, Kind litk, unsigned idx)
+  {
+    Node s1, s2, sv_t;
+    Node x, t, sk;
+    Node sc;
+
+    if (idx == 0)
+    {
+      s2 = d_nm->mkVar("s2", d_nm->mkBitVectorType(4));
+      x = d_nm->mkBoundVar(s2.getType());
+      sk = d_nm->mkSkolem("sk", s2.getType());
+      t = d_nm->mkVar("t", d_nm->mkBitVectorType(8));
+      sv_t = d_nm->mkNode(BITVECTOR_CONCAT, x, s2);
+      sc = getScBvConcat(pol, litk, 0, sk, sv_t, t);
+    }
+    else if (idx == 1)
+    {
+      s1 = d_nm->mkVar("s1", d_nm->mkBitVectorType(4));
+      x = d_nm->mkBoundVar(s1.getType());
+      sk = d_nm->mkSkolem("sk", s1.getType());
+      t = d_nm->mkVar("t", d_nm->mkBitVectorType(8));
+      sv_t = d_nm->mkNode(BITVECTOR_CONCAT, s1, x);
+      sc = getScBvConcat(pol, litk, 1, sk, sv_t, t);
+    }
+    else
+    {
+      Assert(idx == 2);
+      s1 = d_nm->mkVar("s1", d_nm->mkBitVectorType(4));
+      s2 = d_nm->mkVar("s2", d_nm->mkBitVectorType(4));
+      x = d_nm->mkBoundVar(s2.getType());
+      sk = d_nm->mkSkolem("sk", s1.getType());
+      t = d_nm->mkVar("t", d_nm->mkBitVectorType(12));
+      sv_t = d_nm->mkNode(BITVECTOR_CONCAT, s1, x, s2);
+      sc = getScBvConcat(pol, litk, 1, sk, sv_t, t);
+    }
+
+    TS_ASSERT(!sc.isNull());
+    Kind ksc = sc.getKind();
+    TS_ASSERT((litk == kind::EQUAL && pol == false)
+              || ksc == IMPLIES);
+    Node scl = ksc == IMPLIES ? sc[0] : bv::utils::mkTrue();
+    Node body = d_nm->mkNode(litk, sv_t, t);
+    Node bvarlist = d_nm->mkNode(BOUND_VAR_LIST, { x });
+    Node scr = d_nm->mkNode(EXISTS, bvarlist, pol ? body : body.notNode());
+    Expr a = d_nm->mkNode(DISTINCT, scl, scr).toExpr();
+    Result res = d_smt->checkSat(a);
+    if (res.d_sat == Result::SAT)
+    {
+      std::cout << std::endl;
+      if (!s1.isNull())
+        std::cout << "s1 " << d_smt->getValue(s1.toExpr()) << std::endl;
+      if (!s2.isNull())
+        std::cout << "s2 " << d_smt->getValue(s2.toExpr()) << std::endl;
+      std::cout << "t " << d_smt->getValue(t.toExpr()) << std::endl;
+      std::cout << "x " << d_smt->getValue(x.toExpr()) << std::endl;
+    }
+    TS_ASSERT(res.d_sat == Result::UNSAT);
+  }
+
+  void runTestSext(bool pol, Kind litk)
+  {
+    unsigned ws = 3;
+    unsigned wx = 5;
+    unsigned w = 8;
+
+    Node x = d_nm->mkVar("x", d_nm->mkBitVectorType(wx));
+    Node sk = d_nm->mkSkolem("sk", x.getType());
+    x = d_nm->mkBoundVar(x.getType());
+
+    Node t = d_nm->mkVar("t", d_nm->mkBitVectorType(w));
+    Node sv_t = bv::utils::mkSignExtend(x, ws);
+    Node sc = getScBvSext(pol, litk, 0, sk, sv_t, t);
+
+    TS_ASSERT(!sc.isNull());
+    Kind ksc = sc.getKind();
+    TS_ASSERT((litk == kind::EQUAL && pol == false)
+              || (litk == kind::BITVECTOR_ULT && pol == false)
+              || (litk == kind::BITVECTOR_UGT && pol == false)
+              || ksc == IMPLIES);
+    Node scl = ksc == IMPLIES ? sc[0] : bv::utils::mkTrue();
+    Node body = d_nm->mkNode(litk, sv_t, t);
+    Node bvarlist = d_nm->mkNode(BOUND_VAR_LIST, { x });
+    Node scr = d_nm->mkNode(EXISTS, bvarlist, pol ? body : body.notNode());
+    Expr a = d_nm->mkNode(DISTINCT, scl, scr).toExpr();
+    Result res = d_smt->checkSat(a);
+    if (res.d_sat == Result::SAT)
+    {
+      std::cout << std::endl;
+      std::cout << "t " << d_smt->getValue(t.toExpr()) << std::endl;
+      std::cout << "x " << d_smt->getValue(x.toExpr()) << std::endl;
+    }
+    TS_ASSERT(res.d_sat == Result::UNSAT);
+  }
+
  public:
   TheoryQuantifiersBvInverter() {}
 
@@ -134,7 +228,7 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite
     d_em = new ExprManager();
     d_nm = NodeManager::fromExprManager(d_em);
     d_smt = new SmtEngine(d_em);
-    d_smt->setOption("cbqi-bv", CVC4::SExpr(false));
+    d_smt->setOption("cbqi-full", CVC4::SExpr(true));
     d_smt->setOption("produce-models", CVC4::SExpr(true));
     d_scope = new SmtScope(d_smt);
 
@@ -376,6 +470,50 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite
     runTest(false, EQUAL, BITVECTOR_SHL, 1, getScBvShl);
   }
 
+  /* Concat */
+
+  void testGetScBvConcatEqTrue0()
+  {
+    runTestConcat(true, EQUAL, 0);
+  }
+
+  void testGetScBvConcatEqTrue1()
+  {
+    runTestConcat(true, EQUAL, 1);
+  }
+
+  void testGetScBvConcatEqTrue2()
+  {
+    runTestConcat(true, EQUAL, 2);
+  }
+
+  void testGetScBvConcatEqFalse0()
+  {
+    runTestConcat(false, EQUAL, 0);
+  }
+
+  void testGetScBvConcatEqFalse1()
+  {
+    runTestConcat(false, EQUAL, 1);
+  }
+
+  void testGetScBvConcatEqFalse2()
+  {
+    runTestConcat(false, EQUAL, 2);
+  }
+
+  /* Sext */
+
+  void testGetScBvSextEqTrue()
+  {
+    runTestSext(true, EQUAL);
+  }
+
+  void testGetScBvSextEqFalse()
+  {
+    runTestSext(false, EQUAL);
+  }
+
   /* Inequality ------------------------------------------------------------  */
 
   /* Mult */
@@ -1033,4 +1171,169 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite
   {
     runTest(false, BITVECTOR_SGT, BITVECTOR_SHL, 1, getScBvShl);
   }
+
+  /* Concat */
+
+  void testGetScBvConcatUltTrue0()
+  {
+    runTestConcat(true, BITVECTOR_ULT, 0);
+  }
+
+  void testGetScBvConcatUltTrue1()
+  {
+    runTestConcat(true, BITVECTOR_ULT, 1);
+  }
+
+  void testGetScBvConcatUltTrue2()
+  {
+    runTestConcat(true, BITVECTOR_ULT, 2);
+  }
+
+  void testGetScBvConcatUltFalse0()
+  {
+    runTestConcat(false, BITVECTOR_ULT, 0);
+  }
+
+  void testGetScBvConcatUltFalse1()
+  {
+    runTestConcat(false, BITVECTOR_ULT, 1);
+  }
+
+  void testGetScBvConcatUltFalse2()
+  {
+    runTestConcat(false, BITVECTOR_ULT, 2);
+  }
+
+  void testGetScBvConcatUgtTrue0()
+  {
+    runTestConcat(true, BITVECTOR_UGT, 0);
+  }
+
+  void testGetScBvConcatUgtTrue1()
+  {
+    runTestConcat(true, BITVECTOR_UGT, 1);
+  }
+
+  void testGetScBvConcatUgtTrue2()
+  {
+    runTestConcat(true, BITVECTOR_UGT, 2);
+  }
+
+  void testGetScBvConcatUgtFalse0()
+  {
+    runTestConcat(false, BITVECTOR_UGT, 0);
+  }
+
+  void testGetScBvConcatUgtFalse1()
+  {
+    runTestConcat(false, BITVECTOR_UGT, 1);
+  }
+
+  void testGetScBvConcatUgtFalse2()
+  {
+    runTestConcat(false, BITVECTOR_UGT, 2);
+  }
+
+  void testGetScBvConcatSltTrue0()
+  {
+    runTestConcat(true, BITVECTOR_SLT, 0);
+  }
+
+  void testGetScBvConcatSltTrue1()
+  {
+    runTestConcat(true, BITVECTOR_SLT, 1);
+  }
+
+  void testGetScBvConcatSltTrue2()
+  {
+    runTestConcat(true, BITVECTOR_SLT, 2);
+  }
+
+  void testGetScBvConcatSltFalse0()
+  {
+    runTestConcat(false, BITVECTOR_SLT, 0);
+  }
+
+  void testGetScBvConcatSltFalse1()
+  {
+    runTestConcat(false, BITVECTOR_SLT, 1);
+  }
+
+  void testGetScBvConcatSltFalse2()
+  {
+    runTestConcat(false, BITVECTOR_SLT, 2);
+  }
+
+  void testGetScBvConcatSgtTrue0()
+  {
+    runTestConcat(true, BITVECTOR_SGT, 0);
+  }
+
+  void testGetScBvConcatSgtTrue1()
+  {
+    runTestConcat(true, BITVECTOR_SGT, 1);
+  }
+
+  void testGetScBvConcatSgtTrue2()
+  {
+    runTestConcat(true, BITVECTOR_SGT, 2);
+  }
+
+  void testGetScBvConcatSgtFalse0()
+  {
+    runTestConcat(false, BITVECTOR_SGT, 0);
+  }
+
+  void testGetScBvConcatSgtFalse1()
+  {
+    runTestConcat(false, BITVECTOR_SGT, 1);
+  }
+
+  void testGetScBvConcatSgtFalse2()
+  {
+    runTestConcat(false, BITVECTOR_SGT, 2);
+  }
+
+  /* Sext */
+
+  void testGetScBvSextUltTrue()
+  {
+    runTestSext(true, BITVECTOR_ULT);
+  }
+
+  void testGetScBvSextUltFalse()
+  {
+    runTestSext(false, BITVECTOR_ULT);
+  }
+
+  void testGetScBvSextUgtTrue()
+  {
+    runTestSext(true, BITVECTOR_UGT);
+  }
+
+  void testGetScBvSextUgtFalse()
+  {
+    runTestSext(false, BITVECTOR_UGT);
+  }
+
+  void testGetScBvSextSltTrue()
+  {
+    runTestSext(true, BITVECTOR_SLT);
+  }
+
+  void testGetScBvSextSltFalse()
+  {
+    runTestSext(false, BITVECTOR_SLT);
+  }
+
+  void testGetScBvSextSgtTrue()
+  {
+    runTestSext(true, BITVECTOR_SGT);
+  }
+
+  void testGetScBvSextSgtFalse()
+  {
+    runTestSext(false, BITVECTOR_SGT);
+  }
+
 };