From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 18 Apr 2012 12:38:48 +0000 (+0000)
Subject: Add some operations to the c-interfalce that were previously missing. Thanks to Xu... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=4260f6bdc91dd649213b3bd163a7fdfeb59968a7;p=francis%2Fstp.git

Add some operations to the c-interfalce that were previously missing. Thanks to Xu Zhongxing.:

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1643 e59a4935-1847-0410-ae03-e826735625c1
---

diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
index d67a0f2..ab83d3b 100644
--- a/src/c_interface/c_interface.cpp
+++ b/src/c_interface/c_interface.cpp
@@ -1073,6 +1073,11 @@ Expr vc_sbvModExpr(VC vc, int n_bits, Expr left, Expr right) {
     return createBinaryTerm(vc, n_bits, BEEV::SBVREM, left, right);
 }
 
+Expr vc_sbvRemExpr(VC vc, int n_bits, Expr left, Expr right) {
+    return createBinaryTerm(vc, n_bits, BEEV::SBVMOD, left, right);
+}
+
+
 Expr vc_bv32MultExpr(VC vc, Expr left, Expr right) {
   return vc_bvMultExpr(vc, 32, left, right);
 }
@@ -1119,6 +1124,22 @@ Expr vc_sbvGeExpr(VC vc, Expr left, Expr right) {
     return createBinaryNode(vc,BEEV::BVSGE,left,right);
 }
 
+Expr vc_bvLeftShiftExprExpr(VC vc, int n_bits, Expr left, Expr right)
+{
+  return createBinaryTerm(vc, n_bits,BEEV::BVLEFTSHIFT,left,right);
+}
+
+Expr vc_bvRightShiftExprExpr(VC vc, int n_bits,Expr left, Expr right)
+{
+  return createBinaryTerm(vc, n_bits,BEEV::BVRIGHTSHIFT,left,right);
+}
+
+Expr vc_bvSignedRightShiftExprExpr(VC vc,int n_bits, Expr left, Expr right)
+{
+  return createBinaryTerm(vc, n_bits,BEEV::BVSRSHIFT,left,right);
+}
+
+
 Expr vc_bvUMinusExpr(VC vc, Expr ccc) {
   bmstar b = (bmstar)(((stpstar)vc)->bm);
   nodestar a = (nodestar)ccc;
diff --git a/src/c_interface/c_interface.h b/src/c_interface/c_interface.h
index 62492a3..c1b42f6 100644
--- a/src/c_interface/c_interface.h
+++ b/src/c_interface/c_interface.h
@@ -279,6 +279,7 @@ extern "C" {
   Expr vc_sbvDivExpr(VC vc, int n_bits, Expr left, Expr right);
   // signed left modulo right i.e. left%right
   Expr vc_sbvModExpr(VC vc, int n_bits, Expr left, Expr right);
+  Expr vc_sbvRemExpr(VC vc, int n_bits, Expr left, Expr right);
 
   Expr vc_bvLtExpr(VC vc, Expr left, Expr right);
   Expr vc_bvLeExpr(VC vc, Expr left, Expr right);
@@ -298,6 +299,12 @@ extern "C" {
   Expr vc_bvXorExpr(VC vc, Expr left, Expr right);
   Expr vc_bvNotExpr(VC vc, Expr child);
 
+  // Shift an expression by another expression. This is newstyle.
+  Expr vc_bvLeftShiftExprExpr(VC vc, int n_bits, Expr left, Expr right);
+  Expr vc_bvRightShiftExprExpr(VC vc, int n_bits,  Expr left, Expr right);
+  Expr vc_bvSignedRightShiftExprExpr(VC vc, int n_bits, Expr left, Expr right);
+
+  // These shifts are old-style. Kept for compatability---oldstyle.
   Expr vc_bvLeftShiftExpr(VC vc, int sh_amt, Expr child);
   Expr vc_bvRightShiftExpr(VC vc, int sh_amt, Expr child);
   /* Same as vc_bvLeftShift only that the answer in 32 bits long */