From b23c5096c91068a2ca86384d38a0afdab70020b0 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sun, 12 Sep 2010 13:55:09 +0000 Subject: [PATCH] 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 --- src/simplifier/simplifier.cpp | 17 +++++++++++++++++ unit_test/bvconcat.smt2 | 16 ++++++++++++++++ unit_test/bvconcat2.smt2 | 16 ++++++++++++++++ unit_test/bvconcat3.smt2 | 16 ++++++++++++++++ 4 files changed, 65 insertions(+) create mode 100644 unit_test/bvconcat.smt2 create mode 100644 unit_test/bvconcat2.smt2 create mode 100644 unit_test/bvconcat3.smt2 diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index ec8c313..52f9997 100644 --- 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 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 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 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) -- 2.47.3