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

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 d67a0f247b1515aa2d860c66b87edf612d46e837..ab83d3b86e96e7eb7b880320353f64b1ba820c22 100644 (file)
--- 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 62492a3b136e34f4541b096f64821f0c2e6ee969..c1b42f64a727429ced3a93adfaeee1f3154f522d 100644 (file)
--- 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 */