* Test file generator for mul, div, rem.

* Speed up the signed div, signed mod & signed rem encodings.

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

diff --git a/src/AST/Transform.cpp b/src/AST/Transform.cpp
index 771e25c3479cb08113f58fe534bda51df766aa76..e8f6accfdffa3aa36fecd376c11b2de6bcdf0ead 100644 (file)
--- a/src/AST/Transform.cpp
+++ b/src/AST/Transform.cpp
@@ -36,22 +36,19 @@ ASTNode BeevMgr::TranslateSignedDivModRem(const ASTNode& in)
 
        if (SBVREM == in.GetKind())
        {
-               //if(TopBit(dividend)==1)
-               //
-               //then -BVMOD(-dividend,abs(divisor))
-               //
-               //else BVMOD(dividend,abs(divisor))
+               //BVMOD is an expensive operation. So have the fewest bvmods possible. Just one.
+
+               //Take absolute value.
+               ASTNode pos_dividend = CreateTerm(ITE, len, cond_dividend, CreateTerm(BVUMINUS, len, dividend), dividend);
+               ASTNode pos_divisor =  CreateTerm(ITE, len, cond_divisor,  CreateTerm(BVUMINUS, len, divisor), divisor);
 
-               //create the condition and conditional for the divisor
-               ASTNode pos_divisor = CreateTerm(ITE, len, cond_divisor, CreateTerm(BVUMINUS, len, divisor), divisor);
+               //create the modulus term
+               ASTNode modnode = CreateTerm(BVMOD, len, pos_dividend, pos_divisor);
 
-               //create the modulus term for each case
-               ASTNode modnode = CreateTerm(BVMOD, len, dividend, pos_divisor);
-               ASTNode minus_modnode = CreateTerm(BVMOD, len, CreateTerm(BVUMINUS, len, dividend), pos_divisor);
-               minus_modnode = CreateTerm(BVUMINUS, len, minus_modnode);
+               //If the dividend is <0 take the unary minus.
+               ASTNode n = CreateTerm(ITE, len, cond_dividend, CreateTerm(BVUMINUS, len, modnode), modnode);
 
                //put everything together, simplify, and return
-               ASTNode n = CreateTerm(ITE, len, cond_dividend, minus_modnode, modnode);
                return SimplifyTerm_TopLevel(n);
        }
 
@@ -69,33 +66,21 @@ ASTNode BeevMgr::TranslateSignedDivModRem(const ASTNode& in)
                // (ite (and (= ?msb_s bit0) (= ?msb_t bit1))
                //      (bvadd (bvurem s (bvneg t)) t)
                //      (bvneg (bvurem (bvneg s) (bvneg t)))))))
-               ASTNode & s = dividend;
-               ASTNode & t = divisor;
 
-               ASTNode isSNeg = cond_dividend; // (= ?msb_s bit1)
-               ASTNode isSPos = CreateNode(NOT, isSNeg); // (= ?msb_s bit0)
+               //Take absolute value.
+               ASTNode pos_dividend = CreateTerm(ITE, len, cond_dividend, CreateTerm(BVUMINUS, len, dividend), dividend);
+               ASTNode pos_divisor =  CreateTerm(ITE, len, cond_divisor,  CreateTerm(BVUMINUS, len, divisor), divisor);
 
-               ASTNode isTNeg = cond_divisor; // (= ?msb_t bit1)
-               ASTNode isTPos = CreateNode(NOT, isTNeg); // (= ?msb_t bit0)
+               ASTNode urem_node = CreateTerm(BVMOD, len, pos_dividend, pos_divisor);
 
+               // If the dividend is <0, then we negate the whole thing.
+               ASTNode rev_node =  CreateTerm(ITE, len, cond_dividend, CreateTerm(BVUMINUS, len, urem_node), urem_node);
 
-               ASTNode negS = CreateTerm(BVUMINUS, len, s); // (bvneg s)
-               ASTNode negT = CreateTerm(BVUMINUS, len, t); // (bvneg t)
+               // if It's XOR <0 then add t (not its absolute value).
+               ASTNode xor_node = CreateNode(XOR, cond_dividend, cond_divisor);
+               ASTNode n = CreateTerm(ITE, len, xor_node, CreateTerm(BVPLUS, len, rev_node, divisor), rev_node);
 
-               // (bvneg (bvurem (bvneg s) (bvneg t)))
-               ASTNode branch4 = CreateTerm(BVUMINUS, len, CreateTerm(BVMOD, len, negS, negT));
-               // (bvadd (bvurem s (bvneg t)) t)
-               ASTNode branch3 = CreateTerm(BVPLUS, len, CreateTerm(BVMOD, len, s, negT), t);
-               // (bvadd (bvneg (bvurem (bvneg s) t)) t)
-               ASTNode branch2 = CreateTerm(BVPLUS, len, CreateTerm(BVUMINUS, len, CreateTerm(BVMOD, len, negS, t)), t);
-               // (bvurem s t)
-               ASTNode branch1 = CreateTerm(BVMOD, len, s, t);
-
-               ASTNode ite3 = CreateTerm(ITE, len, CreateNode(AND, isSPos, isTNeg), branch3, branch4);
-               ASTNode ite2 = CreateTerm(ITE, len, CreateNode(AND, isSNeg, isTPos), branch2, ite3);
-               ASTNode ite1 = CreateTerm(ITE, len, CreateNode(AND, isSPos, isTPos), branch1, ite2);
-
-               return SimplifyTerm_TopLevel(ite1);
+               return SimplifyTerm_TopLevel(n);
        }
        else if (SBVDIV == in.GetKind())
        {
@@ -114,23 +99,16 @@ ASTNode BeevMgr::TranslateSignedDivModRem(const ASTNode& in)
                //
                //else simply output BVDIV(dividend,divisor)
 
-               ASTNode divnode = CreateTerm(BVDIV, len, dividend, divisor);
+               //Take absolute value.
+               ASTNode pos_dividend = CreateTerm(ITE, len, cond_dividend, CreateTerm(BVUMINUS, len, dividend), dividend);
+               ASTNode pos_divisor =  CreateTerm(ITE, len, cond_divisor,  CreateTerm(BVUMINUS, len, divisor), divisor);
 
-               ASTNode cond1 = CreateNode(AND, CreateNode(EQ, zero, CreateTerm(BVEXTRACT, 1, dividend, hi1, hi1)), CreateNode(EQ, one, CreateTerm(BVEXTRACT,
-                               1, divisor, hi1, hi1)));
-               ASTNode minus_divnode1 = CreateTerm(BVDIV, len, dividend, CreateTerm(BVUMINUS, len, divisor));
-               minus_divnode1 = CreateTerm(BVUMINUS, len, minus_divnode1);
+               ASTNode divnode = CreateTerm(BVDIV, len, pos_dividend, pos_divisor);
 
-               ASTNode cond2 = CreateNode(AND, CreateNode(EQ, one, CreateTerm(BVEXTRACT, 1, dividend, hi1, hi1)), CreateNode(EQ, zero, CreateTerm(BVEXTRACT,
-                               1, divisor, hi1, hi1)));
-               ASTNode minus_divnode2 = CreateTerm(BVDIV, len, CreateTerm(BVUMINUS, len, dividend), divisor);
-               minus_divnode2 = CreateTerm(BVUMINUS, len, minus_divnode2);
+               // A little confusing. Only negate the result if they are XOR <0.
+               ASTNode xor_node = CreateNode(XOR, cond_dividend, cond_divisor);
+               ASTNode n = CreateTerm(ITE, len, xor_node, CreateTerm(BVUMINUS, len, divnode), divnode);
 
-               ASTNode cond3 = CreateNode(AND, CreateNode(EQ, one, CreateTerm(BVEXTRACT, 1, dividend, hi1, hi1)), CreateNode(EQ, one, CreateTerm(BVEXTRACT,
-                               1, divisor, hi1, hi1)));
-               ASTNode minus_divnode3 = CreateTerm(BVDIV, len, CreateTerm(BVUMINUS, len, dividend), CreateTerm(BVUMINUS, len, divisor));
-               ASTNode n = CreateTerm(ITE, len, cond1, minus_divnode1, CreateTerm(ITE, len, cond2, minus_divnode2, CreateTerm(ITE, len, cond3,
-                               minus_divnode3, divnode)));
                return SimplifyTerm_TopLevel(n);
        }
 

diff --git a/tests/generated_tests/mulDivRem.cpp b/tests/generated_tests/mulDivRem.cpp
new file mode 100644 (file)
index 0000000..13b204e
--- /dev/null
+++ b/tests/generated_tests/mulDivRem.cpp
@@ -0,0 +1,177 @@
+#include <cstdint>
+#include <iostream>
+#include <cstdlib>
+#include <cassert>
+#include <cmath>
+#include "../constantbv/constantbv.h"
+#include "../AST/AST.h"
+
+/*
+ * Generates random (a op b = c) triples to check that solver.
+ * Only for complicated instructions like modulus, remainder and divide.
+ */
+
+using std::endl;
+using std::cout;
+using std::cerr;
+using namespace BEEV;
+using namespace CONSTANTBV;
+
+int width = 16;
+typedef uint16_t uns;
+typedef int16_t sig;
+
+const bool debug = false;
+
+uns getUnsignedResult(uns a, Kind k, uns b)
+{
+       uns gold;
+
+       if (BVMULT == k)
+       {
+               return a * b;
+       }
+       else if (BVMOD == k)
+       {
+               return a % b;
+       }
+       else if (BVDIV == k)
+       {
+               return a / b;
+       }
+       cerr << "not implemetned" << endl;
+       exit(2);
+
+}
+
+sig getSignedResult(sig a, Kind k, sig b)
+{
+       sig gold;
+
+       if (SBVMOD == k)
+       {
+               sig Q_prime = (sig) (trunc((double) a / (double) b));
+               if ((a < 0) != (b < 0))
+               {
+                       Q_prime = Q_prime - 1;
+               }
+
+               gold = a - Q_prime * b;
+               if (debug)
+                       fprintf(stderr, "a=%d; b=%d; Q_prime=%d\n", a, b, Q_prime);
+       }
+       else if (SBVREM == k)
+       {
+               gold = a % b;
+       }
+       else if (SBVDIV == k)
+       {
+               gold = a / b;
+       }
+       else
+       {
+               cerr << "not implemetned" << endl;
+               exit(2);
+       }
+       return gold;
+
+}
+
+void go(int count, uns a, uns b, uns result, char* name)
+{
+       cout << ":extrafuns ((a" << count << " BitVec[" << width << "])) " << endl;
+       cout << ":extrafuns ((b" << count << " BitVec[" << width << "])) " << endl;
+       cout << ":extrafuns ((op" << count << " BitVec[" << width << "])) " << endl;
+
+       cout << ":assumption (= ";
+       cout << "(" << name << " ";
+       if ((rand() % 3) == 0)
+               cout << "a" << count << " ";
+       else
+               cout << "bv" << a << "[" << width << "] ";
+
+       if ((rand() % 3) == 0)
+               cout << "b" << count << " ";
+       else
+               cout << "bv" << b << "[" << width << "]";
+       cout << " ) ";
+
+       if ((rand() % 3) == 0)
+               cout << "op" << count << " ";
+       else
+               cout << "bv" << result << "[" << width << "]";
+
+       cout << ")" << endl;
+}
+
+void testSolver(void)
+{
+       cout << "(" << endl;
+       cout << "benchmark blah" << endl;
+       cout << ":logic QF_BV" << endl;
+       cout << ":source {automatically generated}" << endl;
+       cout << ":status sat" << endl;
+
+       uns a, b;
+       sig aS, bS;
+
+       do
+       {
+               a = rand();
+               b = rand();
+               aS = rand();
+               bS = rand();
+       } while (bS == 0 || b == 0);
+
+       switch (rand() % 6)
+       {
+               case 0:
+                       go(0, a, b, getUnsignedResult(a, BVMULT, b), "bvmul");
+                       break;
+               case 1:
+                       go(1, a, b, getUnsignedResult(a, BVDIV, b), "bvudiv");
+                       break;
+               case 2:
+                       go(2, a, b, getUnsignedResult(a, BVMOD, b), "bvurem");
+                       break;
+               case 3:
+                       go(3, aS, bS, getSignedResult(aS, SBVDIV, bS), "bvsdiv");
+                       break;
+               case 4:
+                       go(4, aS, bS, getSignedResult(aS, SBVREM, bS), "bvsrem");
+                       break;
+               case 5:
+                       go(5, aS, bS, getSignedResult(aS, SBVMOD, bS), "bvsmod");
+                       break;
+
+       }
+       cout << ")" << endl;
+}
+
+int main(int argc, char**argv)
+{
+       int nonce;
+       if (argc >= 2)
+               nonce = atoi(argv[1]);
+       else
+               nonce = 1;
+       int seed = time(0) * nonce;
+       if (debug)
+       {
+               cerr << "Seed = " << seed << endl;
+       }
+       srand(seed);
+
+       BitVector_Boot();
+
+       if (false)
+       {
+               testConstEval(SBVMOD);
+               testConstEval(SBVREM);
+               testConstEval(SBVDIV);
+       }
+       testSolver();
+
+       return 0;
+}
+