From c1238f1fc66a42dd1a05f0564eac1a1618d4d782 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Mon, 11 Apr 2011 15:09:31 +0000 Subject: [PATCH] Add an extra simplification rule to the simplifying node factory. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1265 e59a4935-1847-0410-ae03-e826735625c1 --- .../NodeFactory/SimplifyingNodeFactory.cpp | 10 +++++++++ unit_test/bvge1.smt2 | 22 +++++++++++++++++++ 2 files changed, 32 insertions(+) create mode 100644 unit_test/bvge1.smt2 diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp index 1cd2d52..85ec1d1 100644 --- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp +++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp @@ -340,6 +340,16 @@ ASTNode SimplifyingNodeFactory::CreateSimpleEQ(const ASTVec& children) if (k2 == BEEV::BVUMINUS && k1 == BEEV::BVCONST || (k2 == BEEV::BVNEG && k1 == BEEV::BVCONST)) return NodeFactory::CreateNode(BEEV::EQ, in2[0], NodeFactory::CreateTerm(k2,width, in1 )); + if ((k1 == BEEV::BVNEG && in1[0] == in2) || (k2 == BEEV::BVNEG && in2[0] == in1)) + return in1.GetSTPMgr()->ASTFalse; + + if (k2 == BEEV::BVDIV && k1 == BEEV::BVCONST && (in1 == bm.CreateZeroConst(width))) + return NodeFactory::CreateNode(BEEV::BVGT, in2[1], in2[0]); + + if (k1 == BEEV::BVDIV && k2 == BEEV::BVCONST && (in2 == bm.CreateZeroConst(width))) + return NodeFactory::CreateNode(BEEV::BVGT, in1[1], in1[0]); + + // This increases the number of nodes. So disable for now. if (false && BEEV::BVCONCAT == k1 && BEEV::BVCONCAT == k2 && in1[0].GetValueWidth() == in2[0].GetValueWidth()) { diff --git a/unit_test/bvge1.smt2 b/unit_test/bvge1.smt2 new file mode 100644 index 0000000..35afd3e --- /dev/null +++ b/unit_test/bvge1.smt2 @@ -0,0 +1,22 @@ +(set-logic QF_BV) +(set-info :smt-lib-version 2.0) +(set-info :category "check") +(set-info :status unsat) +(declare-fun x () (_ BitVec 10)) +(declare-fun y () (_ BitVec 10)) + + +; +(assert + (bvult + (bvudiv x y ) + (_ bv1 10) + ) +) + +(assert (not (bvult x y))) + + +(check-sat) +(exit) + -- 2.47.3