From bd774376780f6cc7a52e50a62a8aa6de59de26d2 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Wed, 29 Jul 2009 04:03:44 +0000 Subject: [PATCH] Pull up ITEs when two ITEs with the same conditional are arguments to a binary operation. e.g. turns (bvslt (ite a b c) (ite a d e)) INTO (ite a (bvslt b d) (bvslt c e) git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@97 e59a4935-1847-0410-ae03-e826735625c1 --- AST/AST.h | 2 + Makefile.common | 2 +- simplifier/simplifier.cpp | 84 ++++++++++++++++++++++++++++++++++++++- 3 files changed, 85 insertions(+), 3 deletions(-) diff --git a/AST/AST.h b/AST/AST.h index d8862c4..a170dc5 100644 --- a/AST/AST.h +++ b/AST/AST.h @@ -1580,6 +1580,8 @@ public: ASTNode SimplifyAtomicFormula(const ASTNode& a, bool pushNeg); ASTNode CreateSimplifiedEQ(const ASTNode& t1, const ASTNode& t2); ASTNode ITEOpt_InEqs(const ASTNode& in1); + ASTNode PullUpITE(const ASTNode& in); + ASTNode RemoveContradictionsFromAND(const ASTNode& in); ASTNode CreateSimplifiedTermITE(const ASTNode& t1, const ASTNode& t2, const ASTNode& t3); ASTNode CreateSimplifiedFormulaITE(const ASTNode& in0, const ASTNode& in1, const ASTNode& in2); ASTNode CreateSimplifiedINEQ(Kind k, const ASTNode& a0, const ASTNode& a1, bool pushNeg); diff --git a/Makefile.common b/Makefile.common index d160e62..fcc665a 100644 --- a/Makefile.common +++ b/Makefile.common @@ -9,7 +9,7 @@ #OPTIMIZE = -g -pg # Debugging and gprof-style profiling #OPTIMIZE = -g # Debugging -OPTIMIZE = -O3 # Maximum optimization +OPTIMIZE = -O3 -DNDEBUG # Maximum optimization CFLAGS_BASE = $(OPTIMIZE) $(OPTIONS1) $(OPTIONS2) # You can compile using make STATIC=true to compile a statically linked executable diff --git a/simplifier/simplifier.cpp b/simplifier/simplifier.cpp index 90b49c8..4a6b7af 100644 --- a/simplifier/simplifier.cpp +++ b/simplifier/simplifier.cpp @@ -227,6 +227,9 @@ ASTNode BeevMgr::SimplifyFormula(const ASTNode& b, bool pushNeg) if (CheckSimplifyMap(a, output, pushNeg)) return output; + a = PullUpITE(a); + kind = a.GetKind(); // pullUpITE can change the Kind of the node. + switch (kind) { case AND: @@ -476,6 +479,72 @@ ASTNode BeevMgr::CreateSimplifiedINEQ(Kind k, const ASTNode& left, const ASTNode return output; } +//Look through the AND Node for terms that contradict. +//Should be made significantly more general.. +ASTNode BeevMgr::RemoveContradictionsFromAND(const ASTNode& in) +{ + assert(AND == in.GetKind()); + const int childrenSize = in.GetChildren().size(); + + for (int i = 0; i < childrenSize; i++) + { + if (BVLT != in[i].GetKind()) + continue; + + for (int j = i + 1; j < childrenSize; j++) + { + if (BVLT != in[j].GetKind()) + continue; + if (in[i][0] == in[j][1] && in[i][1] == in[j][0]) // parameters are swapped. + return ASTFalse; + } + } + return in; +} + +// turns say (bvslt (ite a b c) (ite a d e)) INTO (ite a (bvslt b d) (bvslt c e)) +// Expensive. But makes some other simplifications possible. +ASTNode BeevMgr::PullUpITE(const ASTNode& in) +{ + if (2 != in.GetChildren().size()) + return in; + if (ITE != in[0].GetKind()) + return in; + if (ITE != in[1].GetKind()) + return in; + if (in[0][0] != in[1][0]) // if the conditional is not equal. + return in; + + // Consider equals. It takes bitvectors and returns a boolean. + // Consider add. It takes bitvectors and returns bitvectors. + // Consider concat. The bitwidth of each side could vary. + + ASTNode l1; + ASTNode l2; + ASTNode result; + + if (in.GetType() == BOOLEAN_TYPE) + { + l1 = CreateNode(in.GetKind(), in[0][1], in[1][1]); + l2 = CreateNode(in.GetKind(), in[0][2], in[1][2]); + result = CreateNode(ITE, in[0][0], l1, l2); + } + else + { + l1 = CreateTerm(in.GetKind(), in.GetValueWidth(), in[0][1], in[1][1]); + l2 = CreateTerm(in.GetKind(), in.GetValueWidth(), in[0][2], in[1][2]); + result = CreateTerm(ITE, in.GetValueWidth(), in[0][0], l1, l2); + } + + assert(result.GetType() == in.GetType()); + assert(result.GetValueWidth() == in.GetValueWidth()); + assert(result.GetIndexWidth() == in.GetIndexWidth()); + assert(BVTypeCheck(result)); + + return result; +} + + //takes care of some simple ITE Optimizations in the context of equations ASTNode BeevMgr::ITEOpt_InEqs(const ASTNode& in) { @@ -753,6 +822,11 @@ ASTNode BeevMgr::SimplifyAndOrFormula(const ASTNode& a, bool pushNeg) break; } } + + // I haven't verified this is useful. + //if (output.GetKind() == AND) + // output = RemoveContradictionsFromAND(output); + //memoize UpdateSimplifyMap(a, output, pushNeg); //cerr << "output:\n" << output << endl; @@ -1162,8 +1236,10 @@ ASTNode BeevMgr::SimplifyTerm_TopLevel(const ASTNode& b) } //This function simplifies terms based on their kind -ASTNode BeevMgr::SimplifyTerm(const ASTNode& inputterm) +ASTNode BeevMgr::SimplifyTerm(const ASTNode& actualInputterm) { + ASTNode inputterm(actualInputterm); // mutable local copy. + //cout << "SimplifyTerm: input: " << a << endl; if (!optimize) { @@ -1197,6 +1273,10 @@ ASTNode BeevMgr::SimplifyTerm(const ASTNode& inputterm) } unsigned int inputValueWidth = inputterm.GetValueWidth(); + + inputterm = PullUpITE(inputterm); + k = inputterm.GetKind(); // pull up ITE can change the kind of the node + switch (k) { case BVCONST: @@ -3075,7 +3155,7 @@ ASTNode BeevMgr::ConvertBVSXToITE(const ASTNode& a) ASTNode BeevMgr::RemoveWrites_TopLevel(const ASTNode& term) { - if (READ != term.GetKind() && WRITE != term[0].GetKind()) + if (READ != term.GetKind() || WRITE != term[0].GetKind()) { FatalError("RemovesWrites: Input must be a READ over a WRITE", term); } -- 2.47.3