Boolector: implement direct BV rotation by constant.

Author: kfriedberger

lib/native/source/libboolector/interface_wrap.c

@@ -1976,6 +1976,42 @@ SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_
 }
 
 
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1rori(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jint jarg3) {
+  jlong jresult = 0 ;
+  Btor *arg1 = (Btor *) 0 ;
+  BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+  uint32_t arg3 = 0 ;
+  BoolectorNode *result = 0 ;
+
+  (void)jenv;
+  (void)jcls;
+  arg1 = *(Btor **)&jarg1;
+  arg2 = *(BoolectorNode **)&jarg2;
+  arg3 = (uint32_t)jarg3;
+  result = (BoolectorNode *)boolector_rori(arg1,arg2,arg3);
+  *(BoolectorNode **)&jresult = result;
+  return jresult;
+}
+
+
+SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1roli(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jint jarg3) {
+  jlong jresult = 0 ;
+  Btor *arg1 = (Btor *) 0 ;
+  BoolectorNode *arg2 = (BoolectorNode *) 0 ;
+  uint32_t arg3 = 0 ;
+  BoolectorNode *result = 0 ;
+
+  (void)jenv;
+  (void)jcls;
+  arg1 = *(Btor **)&jarg1;
+  arg2 = *(BoolectorNode **)&jarg2;
+  arg3 = (uint32_t)jarg3;
+  result = (BoolectorNode *)boolector_roli(arg1,arg2,arg3);
+  *(BoolectorNode **)&jresult = result;
+  return jresult;
+}
+
+
 SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1sub(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jlong jarg3) {
   jlong jresult = 0 ;
   Btor *arg1 = (Btor *) 0 ;
@@ -3495,41 +3531,6 @@ SWIGEXPORT jint JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_b
 }
 
 
-SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1rori(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jint jarg3) {
-  jlong jresult = 0 ;
-  Btor *arg1 = (Btor *) 0 ;
-  BoolectorNode *arg2 = (BoolectorNode *) 0 ;
-  uint32_t arg3 = 0 ;
-  BoolectorNode *result = 0 ;
-
-  (void)jenv;
-  (void)jcls;
-  arg1 = *(Btor **)&jarg1;
-  arg2 = *(BoolectorNode **)&jarg2;
-  arg3 = (uint32_t)jarg3;
-  result = (BoolectorNode *)boolector_rori(arg1,arg2,arg3);
-  *(BoolectorNode **)&jresult = result;
-  return jresult;
-}
-
-SWIGEXPORT jlong JNICALL Java_org_sosy_1lab_java_1smt_solvers_boolector_BtorJNI_boolector_1roli(JNIEnv *jenv, jclass jcls, jlong jarg1, jlong jarg2, jint jarg3) {
-  jlong jresult = 0 ;
-  Btor *arg1 = (Btor *) 0 ;
-  BoolectorNode *arg2 = (BoolectorNode *) 0 ;
-  uint32_t arg3 = 0 ;
-  BoolectorNode *result = 0 ;
-
-  (void)jenv;
-  (void)jcls;
-  arg1 = *(Btor **)&jarg1;
-  arg2 = *(BoolectorNode **)&jarg2;
-  arg3 = (uint32_t)jarg3;
-  result = (BoolectorNode *)boolector_roli(arg1,arg2,arg3);
-  *(BoolectorNode **)&jresult = result;
-  return jresult;
-}
-
-
 //helpmethods
 
 //Returns the int value of BOOLECTOR_PARSE_ERROR

src/org/sosy_lab/java_smt/solvers/boolector/BoolectorBitvectorFormulaManager.java

@@ -17,7 +17,9 @@
 import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_not;
 import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_or;
 import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_rol;
+import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_roli;
 import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_ror;
+import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_rori;
 import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_sdiv;
 import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_sext;
 import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_sgt;
@@ -195,11 +197,21 @@ public Long shiftLeft(Long bitVec, Long toShift) {
     return boolector_sll(btor, bitVec, toShift);
   }
 
+  @Override
+  public Long rotateLeftByConstant(Long bitVec, int toRotate) {
+    return boolector_roli(btor, bitVec, toRotate);
+  }
+
   @Override
   public Long rotateLeft(Long bitVec, Long toRotate) {
     return boolector_rol(btor, bitVec, toRotate);
   }
 
+  @Override
+  public Long rotateRightByConstant(Long bitVec, int toRotate) {
+    return boolector_rori(btor, bitVec, toRotate);
+  }
+
   @Override
   public Long rotateRight(Long bitVec, Long toRotate) {
     return boolector_ror(btor, bitVec, toRotate);

src/org/sosy_lab/java_smt/solvers/boolector/BtorJNI.java

@@ -221,6 +221,10 @@ private BtorJNI() {}
 
   protected static native long boolector_ror(long jarg1, long jarg2, long jarg3);
 
+  protected static native long boolector_roli(long btor, long node, int nbits);
+
+  protected static native long boolector_rori(long btor, long node, int nbits);
+
   protected static native long boolector_sub(long jarg1, long jarg2, long jarg3);
 
   protected static native long boolector_usubo(long jarg1, long jarg2, long jarg3);
@@ -414,10 +418,6 @@ protected static native int boolector_parse_smt2(
 
   protected static native int boolector_bitvec_sort_get_width(long jarg1, long jarg2);
 
-  protected static native long boolector_roli(long btor, long node, int nbits);
-
-  protected static native long boolector_rori(long btor, long node, int nbits);
-
   protected static native long boolector_get_value(long btor, long node);
 
   /**