Speedup. Add bvconcat normalisation. Break bvconcat apart sometimes.

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

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index ec8c31301e6c6c4f1964bec0b710b71fc1f8d194..52f999749cfb5da6f864b4bdc42ed0a74c24879e 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -967,6 +967,14 @@ namespace BEEV
                        return ASTFalse;
        }
 
+    // If both the children are concats split them apart.
+    // nb. This doesn't cover the case when the children are organised differently:
+    // (concat (concat A B) C) == (concat A (concat B C))
+    if (k1 == BVCONCAT && k2 == BVCONCAT && in1[0].GetValueWidth() == in2[0].GetValueWidth())
+    {
+      return nf->CreateNode(AND, nf->CreateNode(EQ, in1[0], in2[0]), nf->CreateNode(EQ, in1[1], in2[1]));
+    }
+
 
     //last resort is to CreateNode
     return nf->CreateNode(EQ, in1, in2);
@@ -2627,6 +2635,15 @@ namespace BEEV
                   output = nf->CreateTerm(BVCONCAT, inputValueWidth, t, u);
                 }
             }
+          else if (t.GetKind() == BVCONCAT && t[0].GetKind() != BVCONCAT && false)
+            {
+
+              /// This makes the left hand child of every concat not a concat.
+              ASTNode left= t[0];
+              ASTNode bottom = nf->CreateTerm(BVCONCAT, t[1].GetValueWidth() + u.GetValueWidth(), t[1], u);
+              output = nf->CreateTerm(BVCONCAT, inputValueWidth, left, bottom);
+              assert(BVTypeCheck(output));
+            }
           else
             {
               output = nf->CreateTerm(BVCONCAT, inputValueWidth, t, u);

diff --git a/unit_test/bvconcat.smt2 b/unit_test/bvconcat.smt2
new file mode 100644 (file)
index 0000000..d3bdbf3
--- /dev/null
+++ b/unit_test/bvconcat.smt2
@@ -0,0 +1,16 @@
+(set-logic QF_BV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "check")
+(set-info :status sat)
+(declare-fun v0 () (_ BitVec 2))
+(declare-fun v1 () (_ BitVec 2))
+(declare-fun v2 () (_ BitVec 2))
+(declare-fun v3 () (_ BitVec 2))
+(declare-fun v4 () (_ BitVec 2))
+(declare-fun v5 () (_ BitVec 2))
+(declare-fun v6 () (_ BitVec 2))
+(declare-fun v7 () (_ BitVec 2))
+
+(assert (= (concat (concat v4 v5) v1) (concat (concat v6 v7) v2 ) ))
+(check-sat)
+(exit)

diff --git a/unit_test/bvconcat2.smt2 b/unit_test/bvconcat2.smt2
new file mode 100644 (file)
index 0000000..4c18160
--- /dev/null
+++ b/unit_test/bvconcat2.smt2
@@ -0,0 +1,16 @@
+(set-logic QF_BV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "check")
+(set-info :status sat)
+(declare-fun v0 () (_ BitVec 2))
+(declare-fun v1 () (_ BitVec 2))
+(declare-fun v2 () (_ BitVec 2))
+(declare-fun v3 () (_ BitVec 2))
+(declare-fun v4 () (_ BitVec 2))
+(declare-fun v5 () (_ BitVec 2))
+(declare-fun v6 () (_ BitVec 2))
+(declare-fun v7 () (_ BitVec 2))
+
+(assert (= (concat v1 (concat v4 v5)) (concat (concat v6 v7) v2 ) ))
+(check-sat)
+(exit)

diff --git a/unit_test/bvconcat3.smt2 b/unit_test/bvconcat3.smt2
new file mode 100644 (file)
index 0000000..1e141be
--- /dev/null
+++ b/unit_test/bvconcat3.smt2
@@ -0,0 +1,16 @@
+(set-logic QF_BV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "check")
+(set-info :status sat)
+(declare-fun v0 () (_ BitVec 2))
+(declare-fun v1 () (_ BitVec 2))
+(declare-fun v2 () (_ BitVec 2))
+(declare-fun v3 () (_ BitVec 2))
+(declare-fun v4 () (_ BitVec 2))
+(declare-fun v5 () (_ BitVec 2))
+(declare-fun v6 () (_ BitVec 2))
+(declare-fun v7 () (_ BitVec 2))
+
+(assert (= (concat v1 (concat v2 v3)) (concat (concat v1 v2) v3 ) ))
+(check-sat)
+(exit)