From ddbf95c937091b95b742502b760767d757c7cf13 Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Wed, 27 Sep 2017 13:45:27 -0700
Subject: [PATCH] CEGQI for BV: Add inverse for BITVECTOR_MULT. (#1153)

This implements side conditions and the instantiation via word-level inversion for operator BITVECTOR_MULT.
---
 src/theory/quantifiers/ceg_t_instantiator.cpp | 29 ++++++++++++++++---
 src/theory/quantifiers/ceg_t_instantiator.h   | 11 +++++++
 2 files changed, 36 insertions(+), 4 deletions(-)

diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp
index 6f94249ef..88aeacb1d 100644
--- a/src/theory/quantifiers/ceg_t_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_t_instantiator.cpp
@@ -885,18 +885,39 @@ Node BvInverter::getPathToPv( Node lit, Node pv, Node sv, Node pvs, std::vector<
 
 Node BvInverter::solve_bv_constraint( Node sv, Node sv_t, Node t, Kind rk, bool pol, std::vector< unsigned >& path,
                                       BvInverterModelQuery * m, BvInverterStatus& status ) {
+  NodeManager *nm = NodeManager::currentNM();
   while( !path.empty() ){
     unsigned index = path.back();
+    Assert (sv_t.getNumChildren() <= 2);
     Assert( index<sv_t.getNumChildren() );
     path.pop_back();
     Kind k = sv_t.getKind();
     // inversions
     if( k==BITVECTOR_PLUS ){
-      t = NodeManager::currentNM()->mkNode( BITVECTOR_SUB, t, sv_t[1-index] );
+      t = nm->mkNode( BITVECTOR_SUB, t, sv_t[1-index] );
     }else if( k==BITVECTOR_SUB ){
-      t = NodeManager::currentNM()->mkNode( BITVECTOR_PLUS, t, sv_t[1-index] );
-    //}else if( k==BITVECTOR_MULT ){
-      // TODO
+      t = nm->mkNode( BITVECTOR_PLUS, t, sv_t[1-index] );
+    }else if( k==BITVECTOR_MULT ){
+      // t = skv (fresh skolem constant)
+      // with side condition:
+      // ctz(t) >= ctz(s) <-> skv * s = t
+      // where
+      // ctz(t) >= ctz(s) -> (t & -t) >= (s & -s)
+      Node s = sv_t[1-index];
+      Node skv = nm->mkSkolem ("skvinv", t.getType(), "created for BvInverter");
+      // cache for substitution
+      BvInverterSkData d = BvInverterSkData (sv_t, t, k);
+      d_sk_inv.emplace(skv,d);
+      // 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)));
+      // right hand side of side condition
+      Node scr = nm->mkNode (EQUAL, nm->mkNode (BITVECTOR_MULT, skv, s), t);
+      // add side condition
+      status.d_conds.push_back (nm->mkNode (EQUAL, scl, scr));
+      t = skv;
+
     }else if( k==BITVECTOR_NEG || k==BITVECTOR_NOT ){
       t = NodeManager::currentNM()->mkNode( k, t );
     //}else if( k==BITVECTOR_AND || k==BITVECTOR_OR ){
diff --git a/src/theory/quantifiers/ceg_t_instantiator.h b/src/theory/quantifiers/ceg_t_instantiator.h
index a24878caf..51142f77d 100644
--- a/src/theory/quantifiers/ceg_t_instantiator.h
+++ b/src/theory/quantifiers/ceg_t_instantiator.h
@@ -95,11 +95,22 @@ public:
   std::vector< Node > d_conds;
 };
 
+// class for storing mapped data for fresh skolem constants
+class BvInverterSkData {
+public:
+  BvInverterSkData (Node sv_t, Node t, Kind op)
+    : d_sv_t(sv_t), d_t(t), d_op(op) {}
+  Node d_sv_t;
+  Node d_t;
+  Kind d_op;
+};
+
 // inverter class
 // TODO : move to theory/bv/ if generally useful?
 class BvInverter {
 private:
   std::map< TypeNode, Node > d_solve_var;
+  std::unordered_map< Node, BvInverterSkData, NodeHashFunction > d_sk_inv;
   Node getPathToPv( Node lit, Node pv, Node sv, std::vector< unsigned >& path, std::unordered_set< TNode, TNodeHashFunction >& visited );
 public:
   // get dummy fresh variable of type tn, used as argument for sv 
-- 
2.30.2