else
LDFLAGS = $(LDFLAGS_BASE)
CFLAGS = $(CFLAGS_BASE)
- CFLAGS = $(CFLAGS_BASE) $(CFLAGS_M32)
+ CFLAGS = $(CFLAGS_BASE) $(CFLAGS_M32) -I../AST
endif
#CXXFLAGS = $(CFLAGS) -Wall -Wextra -DEXT_HASH_MAP -Wno-deprecated
bool exprless(const ASTNode n1, const ASTNode n2);
bool arithless(const ASTNode n1, const ASTNode n2);
bool isAtomic(Kind k);
+ bool isCommutative(const Kind k);
+
// If (a > b) in the termorder, then return 1 elseif (a < b) in the
// termorder, then return -1 else return 0
friend class STPMgr;
friend class ASTNodeHasher;
friend class ASTNodeEqual;
+ friend class HashingNodeFactory;
private:
/******************************************************************
********************************************************************/
#ifndef ASTNODE_H
#define ASTNODE_H
+#include "../AST/NodeFactory/HashingNodeFactory.h"
/********************************************************************
* This file gives the class description of the ASTNode class *
friend class CNFMgr;
friend class ASTInterior;
friend class vector<ASTNode>;
+ friend BEEV::ASTNode HashingNodeFactory::CreateNode(const Kind kind, const BEEV::ASTVec & back_children);
private:
/****************************************************************
}
} //end of arithless
+ bool isConstant() const
+ {
+ const Kind k = GetKind();
+ return (k == BVCONST || k == TRUE || k == FALSE);
+ }
+
+ bool isITE() const
+ {
+ bool result;
+
+ Kind k = GetKind();
+ switch (k)
+ {
+ case ITE:
+ {
+ result = true;
+ break;
+ }
+ default:
+ {
+ result = false;
+ break;
+ }
+ }
+
+ return result;
+ }
+
+
// For lisp DAG printing. Has it been printed already, so we can
// just print the node number?
bool IsAlreadyPrinted() const;
* Universal Helper Functions *
****************************************************************/
+ bool isCommutative(const Kind k) {
+ switch (k) {
+ case BVOR:
+ case BVAND:
+ case BVXOR:
+ case BVNAND:
+ case BVNOR:
+ case BVXNOR:
+ case BVPLUS:
+ case BVMULT:
+ case EQ:
+ case AND:
+ case OR:
+ case NAND:
+ case NOR:
+ case XOR:
+ case IFF:
+ return true;
+ default:
+ return false;
+ }
+
+ return false;
+}
+
+
void FatalError(const char * str, const ASTNode& a, int w)
{
if (a.GetKind() != UNDEFINED)
include ../../scripts/Makefile.common
SRCS=$(wildcard *.cpp)
+SRCS+=$(wildcard NodeFactory/*.cpp)
OBJS = $(SRCS:.cpp=.o)
OBJS+= ASTKind.o
CFLAGS += -I$(MTL)
.PHONY: clean
clean:
- rm -rf *.o *~ *.a ASTKind.cpp ASTKind.h depend .#*
+ rm -rf NodeFactory/*.o *.o *~ *.a ASTKind.cpp ASTKind.h depend .#*
#If this depended on ASTKind.h & ASTKind.cpp, then ./genkinds.pl
#would be called each "clean".
--- /dev/null
+#include "HashingNodeFactory.h"
+#include "AST.h"
+#include "../STPManager/STP.h"
+
+using BEEV::Kind;
+using BEEV::ASTInterior;
+using BEEV::ASTVec;
+using BEEV::ASTNode;
+
+
+HashingNodeFactory::~HashingNodeFactory()
+{
+}
+
+// Get structurally hashed version of the node.
+BEEV::ASTNode HashingNodeFactory::CreateNode(const Kind kind, const BEEV::ASTVec & back_children)
+{
+ // create a new node. Children will be modified.
+ ASTInterior *n_ptr = new ASTInterior(kind);
+
+ ASTVec children(back_children);
+ // The Bitvector solver seems to expect constants on the RHS, variables on the LHS.
+ // We leave the order of equals children as we find them.
+ if (BEEV::isCommutative(kind) && kind != BEEV::EQ && kind != BEEV::AND)
+ {
+ SortByArith(children);
+ }
+
+ // insert all of children at end of new_children.
+ ASTNode n(bm.CreateInteriorNode(kind, n_ptr, children));
+ return n;
+}
+
+// Create and return an ASTNode for a term
+ASTNode HashingNodeFactory::CreateTerm(Kind kind, unsigned int width,const ASTVec &children)
+{
+
+ ASTNode n = CreateNode(kind, children);
+ n.SetValueWidth(width);
+
+ //by default we assume that the term is a Bitvector. If
+ //necessary the indexwidth can be changed later
+ n.SetIndexWidth(0);
+ return n;
+}
+
+
--- /dev/null
+// A Node factory that only does structural hashing.
+#ifndef HASHINGNODEFACTORY_H_
+#define HASHINGNODEFACTORY_H_
+
+#include "NodeFactory.h"
+#include "ASTKind.h"
+namespace BEEV
+{
+ class STPMgr;
+}
+
+class HashingNodeFactory : public NodeFactory
+{
+ BEEV::STPMgr& bm;
+public:
+ HashingNodeFactory(BEEV::STPMgr& bm_)
+ : bm(bm_)
+ {
+ }
+
+ virtual ~HashingNodeFactory();
+ BEEV::ASTNode CreateNode(const BEEV::Kind kind, const BEEV::ASTVec & back_children);
+ BEEV::ASTNode CreateTerm(BEEV::Kind kind, unsigned int width,const BEEV::ASTVec &children);
+
+};
+
+#endif /* HASHINGNODEFACTORY_H_ */
--- /dev/null
+#include "ASTKind.h"
+#include "AST.h"
+
+NodeFactory::~NodeFactory()
+{
+}
+
+BEEV::ASTNode NodeFactory::CreateTerm(BEEV::Kind kind, unsigned int width,
+ const BEEV::ASTVec &children)
+{
+ return CreateTerm(kind, width, children);
+}
+
+ASTNode NodeFactory::CreateTerm(Kind kind, unsigned int width,
+ const ASTNode& child0, const ASTVec &children)
+{
+ ASTVec child;
+ child.reserve(children.size() + 1);
+ child.push_back(child0);
+ child.insert(child.end(), children.begin(), children.end());
+ return CreateTerm(kind, width, child);
+}
+
+ASTNode NodeFactory::CreateTerm(Kind kind, unsigned int width,
+ const ASTNode& child0, const ASTNode& child1, const ASTVec &children)
+{
+ ASTVec child;
+ child.reserve(children.size() + 2);
+ child.push_back(child0);
+ child.push_back(child1);
+ child.insert(child.end(), children.begin(), children.end());
+ return CreateTerm(kind, width, child);
+}
+
+ASTNode NodeFactory::CreateTerm(Kind kind, unsigned int width,
+ const ASTNode& child0, const ASTNode& child1, const ASTNode& child2,
+ const ASTVec &children)
+{
+ ASTVec child;
+ child.reserve(children.size() + 3);
+ child.push_back(child0);
+ child.push_back(child1);
+ child.push_back(child2);
+ child.insert(child.end(), children.begin(), children.end());
+ return CreateTerm(kind, width, child);
+}
+
+ASTNode NodeFactory::CreateNode(Kind kind, const ASTNode& child0,
+ const ASTVec & back_children)
+{
+ ASTVec front_children;
+ front_children.reserve(1 + back_children.size());
+ front_children.push_back(child0);
+ front_children.insert(front_children.end(), back_children.begin(),
+ back_children.end());
+ return CreateNode(kind, front_children);
+}
+
+ASTNode NodeFactory::CreateNode(Kind kind, const ASTNode& child0,
+ const ASTNode& child1, const ASTVec & back_children)
+{
+ ASTVec front_children;
+ front_children.reserve(2 + back_children.size());
+ front_children.push_back(child0);
+ front_children.push_back(child1);
+ front_children.insert(front_children.end(), back_children.begin(),
+ back_children.end());
+ return CreateNode(kind, front_children);
+}
+
+ASTNode NodeFactory::CreateNode(Kind kind, const ASTNode& child0,
+ const ASTNode& child1, const ASTNode& child2,
+ const ASTVec & back_children)
+{
+ ASTVec front_children;
+ front_children.reserve(3 + back_children.size());
+ front_children.push_back(child0);
+ front_children.push_back(child1);
+ front_children.push_back(child2);
+ front_children.insert(front_children.end(), back_children.begin(),
+ back_children.end());
+ return CreateNode(kind, front_children);
+}
+
+ASTNode NodeFactory::CreateArrayTerm(Kind kind, unsigned int index, unsigned int width,
+ const ASTNode& child0, const ASTNode& child1, const ASTNode& child2,
+ const ASTVec &children)
+{
+ ASTVec child;
+ child.reserve(children.size() + 3);
+ child.push_back(child0);
+ child.push_back(child1);
+ child.push_back(child2);
+ child.insert(child.end(), children.begin(), children.end());
+ return CreateArrayTerm(kind, index, width, child);
+}
+
+BEEV::ASTNode NodeFactory::CreateArrayTerm(Kind kind, unsigned int index,
+ unsigned int width, const BEEV::ASTVec &children)
+{
+ ASTNode result = CreateTerm(kind, width, children);
+ result.SetIndexWidth(index);
+ return result;
+}
+
--- /dev/null
+// Abstract base class for all the node factories.
+#ifndef NODEFACTORY_H
+#define NODEFACTORY_H
+
+#include <vector>
+#include "ASTKind.h"
+
+namespace BEEV
+{
+class ASTNode;
+typedef std::vector<ASTNode> ASTVec;
+extern ASTVec _empty_ASTVec;
+}
+
+using BEEV::ASTNode;
+using BEEV::Kind;
+using BEEV::ASTVec;
+using BEEV::_empty_ASTVec;
+
+class NodeFactory
+{
+public:
+ virtual ~NodeFactory();
+
+ virtual BEEV::ASTNode CreateTerm(Kind kind, unsigned int width,
+ const BEEV::ASTVec &children) =0;
+
+ virtual BEEV::ASTNode CreateArrayTerm(Kind kind, unsigned int index, unsigned int width,
+ const BEEV::ASTVec &children);
+
+ virtual BEEV::ASTNode CreateNode(Kind kind,
+ const BEEV::ASTVec& children) =0;
+
+
+ ASTNode CreateTerm(Kind kind, unsigned int width, const ASTNode& child0,
+ const ASTVec &children = _empty_ASTVec);
+ ASTNode CreateTerm(Kind kind, unsigned int width, const ASTNode& child0,
+ const ASTNode& child1, const ASTVec &children = _empty_ASTVec);
+ ASTNode CreateTerm(Kind kind, unsigned int width, const ASTNode& child0,
+ const ASTNode& child1, const ASTNode& child2,
+ const ASTVec &children = _empty_ASTVec);
+
+ ASTNode CreateNode(Kind kind, const ASTNode& child0,
+ const ASTVec & back_children = _empty_ASTVec);
+ ASTNode CreateNode(Kind kind, const ASTNode& child0, const ASTNode& child1,
+ const ASTVec & back_children = _empty_ASTVec);
+ ASTNode CreateNode(Kind kind, const ASTNode& child0, const ASTNode& child1,
+ const ASTNode& child2, const ASTVec & back_children =
+ _empty_ASTVec);
+
+
+ ASTNode CreateArrayTerm(Kind kind, unsigned int index, unsigned int width, const ASTNode& child0,
+ const ASTNode& child1, const ASTNode& child2,
+ const ASTVec &children = _empty_ASTVec);
+
+};
+
+#endif
--- /dev/null
+// nb. Some of the simplifications are duplicated with minor differences in the STPManager class.
+
+#include "../../AST/AST.h"
+#include <cassert>
+#include "SimplifyingNodeFactory.h"
+
+using BEEV::Kind;
+
+static bool debug_simplifyingNodeFactory = false;
+
+ASTNode SimplifyingNodeFactory::CreateNode(Kind kind, const ASTVec & children)
+{
+ // If all the parameters are constant, return the constant value.
+ // The bitblaster calls CreateNode with a boolean vector. We don't try to simplify those.
+ if (kind != BEEV::BOOLVEC && kind != BEEV::UNDEFINED)
+ {
+ bool allConstant = true;
+
+ for (unsigned i = 0; i < children.size(); i++)
+ if (!children[i].isConstant())
+ {
+ allConstant = false;
+ break;
+ }
+
+ if (allConstant)
+ {
+ const ASTNode& hash = hashing.CreateNode(kind, children);
+ const ASTNode& c = simplifier->BVConstEvaluator(hash);
+ return c;
+ }
+ }
+
+ ASTNode result;
+
+ switch (kind)
+ {
+
+ case BEEV::BVLT:
+ assert(children.size() ==2);
+ result = NodeFactory::CreateNode(BEEV::BVGT, children[1], children[0]);
+ break;
+
+ case BEEV::BVLE:
+ assert(children.size() ==2);
+ result = NodeFactory::CreateNode(BEEV::BVGE, children[1], children[0]);
+ break;
+
+ case BEEV::BVSLT:
+ assert(children.size() ==2);
+ result = NodeFactory::CreateNode(BEEV::BVSGT, children[1], children[0]);
+ break;
+
+ case BEEV::BVSLE:
+ assert(children.size() ==2);
+ result = NodeFactory::CreateNode(BEEV::BVSGE, children[1], children[0]);
+ break;
+
+ case BEEV::NOT:
+ result = CreateSimpleNot(children);
+ break;
+ case BEEV::AND:
+ result = CreateSimpleAndOr(1, children);
+ break;
+ case BEEV::OR:
+ result = CreateSimpleAndOr(0, children);
+ break;
+ case BEEV::NAND:
+ result = CreateSimpleNot(CreateSimpleAndOr(1, children));
+ break;
+ case BEEV::NOR:
+ result = CreateSimpleNot(CreateSimpleAndOr(0, children));
+ break;
+ case BEEV::XOR:
+ result = CreateSimpleXor(children);
+ break;
+ case BEEV::ITE:
+ result = CreateSimpleFormITE(children);
+ break;
+ case BEEV::EQ:
+ result = CreateSimpleEQ(children);
+ break;
+ default:
+ result = hashing.CreateNode(kind, children);
+ }
+
+ return result;
+}
+
+ASTNode SimplifyingNodeFactory::CreateSimpleNot(const ASTNode& form)
+{
+ const Kind k = form.GetKind();
+ switch (k)
+ {
+ case BEEV::FALSE:
+ {
+ return form.GetSTPMgr()->ASTTrue;
+ }
+ case BEEV::TRUE:
+ {
+ return form.GetSTPMgr()->ASTFalse;
+ }
+ case BEEV::NOT:
+ {
+ return form[0];
+ } // NOT NOT cancellation
+ default:
+ {
+ ASTVec children;
+ children.push_back(form);
+ return hashing.CreateNode(BEEV::NOT, children);
+ }
+ }
+}
+
+ASTNode SimplifyingNodeFactory::CreateSimpleNot(const ASTVec& children)
+{
+ const Kind k = children[0].GetKind();
+ switch (k)
+ {
+ case BEEV::FALSE:
+ {
+ return children[0].GetSTPMgr()->ASTTrue;
+ }
+ case BEEV::TRUE:
+ {
+ return children[0].GetSTPMgr()->ASTFalse;
+ }
+ case BEEV::NOT:
+ {
+ return children[0][0];
+ } // NOT NOT cancellation
+ default:
+ {
+ return hashing.CreateNode(BEEV::NOT, children);
+ }
+ }
+}
+
+ASTNode SimplifyingNodeFactory::CreateSimpleAndOr(bool IsAnd,
+ const ASTNode& form1, const ASTNode& form2)
+{
+ ASTVec children;
+ children.push_back(form1);
+ children.push_back(form2);
+ return CreateSimpleAndOr(IsAnd, children);
+}
+
+// FIXME: Could also handle (AND ... (NOT (OR ...) ...)
+ASTNode SimplifyingNodeFactory::CreateSimpleAndOr(bool IsAnd,
+ const ASTVec &children)
+{
+ const Kind k = IsAnd ? BEEV::AND : BEEV::OR;
+
+ // Copy so that it can be sorted. Sort so that identical nodes
+ // occur in sequential runs, followed by their negations.
+
+ ASTVec children_copy = children;
+ SortByExprNum(children_copy);
+
+ assert(children.size() == children_copy.size());
+
+ if (debug_simplifyingNodeFactory)
+ {
+ cout << "========" << endl << "CreateSimpAndOr " << k << " ";
+ lpvec(children_copy);
+ cout << endl;
+ }
+
+ const ASTNode& annihilator = (IsAnd ? ASTFalse : ASTTrue);
+ const ASTNode& identity = (IsAnd ? ASTTrue : ASTFalse);
+
+ ASTNode retval;
+ ASTVec new_children;
+
+ const ASTVec::const_iterator it_end = children_copy.end();
+ for (ASTVec::const_iterator it = children_copy.begin(); it != it_end; it++)
+ {
+ ASTVec::const_iterator next_it;
+
+ bool nextexists = (it + 1 < it_end);
+ if (nextexists)
+ next_it = it + 1;
+ else
+ next_it = it_end;
+
+ if (*it == annihilator)
+ {
+ retval = annihilator;
+ if (debug_simplifyingNodeFactory)
+ {
+ cout << "Annihilator" << endl;
+ }
+ return retval;
+ }
+ else if (*it == identity || (nextexists && (*next_it == *it)))
+ {
+ // just drop it
+ }
+ else if (nextexists && (next_it->GetKind() == BEEV::NOT)
+ && ((*next_it)[0] == *it))
+ {
+ // form and negation -- return FALSE for AND, TRUE for OR.
+ retval = annihilator;
+ // cout << "X and/or NOT X" << endl;
+ if (debug_simplifyingNodeFactory)
+ {
+ cout << "Annihilator. Not and Equals" << retval << endl;
+ }
+ return retval;
+ }
+ else
+ {
+ // add to children
+ new_children.push_back(*it);
+ }
+ }
+
+ // If we get here, we saw no annihilators, and children should
+ // be only the non-True nodes.
+ if (new_children.size() < 2)
+ {
+ if (0 == new_children.size())
+ {
+ retval = identity;
+ }
+ else
+ {
+ // there is just one child
+ retval = new_children[0];
+ }
+ }
+ else
+ {
+ // 2 or more children. Create a new node.
+ retval = hashing.CreateNode(IsAnd ? BEEV::AND : BEEV::OR, new_children);
+ }
+ if (debug_simplifyingNodeFactory)
+ {
+ cout << "returns " << retval << endl;
+ }
+ return retval;
+}
+
+//Tries to simplify the input to TRUE/FALSE. if it fails, then
+//return the constructed equality
+ASTNode SimplifyingNodeFactory::CreateSimpleEQ(const ASTVec& children)
+{
+ const ASTNode& in1 = children[0];
+ const ASTNode& in2 = children[1];
+ const Kind k1 = in1.GetKind();
+ const Kind k2 = in2.GetKind();
+
+ if (in1 == in2)
+ //terms are syntactically the same
+ return in1.GetSTPMgr()->ASTTrue;
+
+ //here the terms are definitely not syntactically equal but may be
+ //semantically equal.
+ if (BEEV::BVCONST == k1 && BEEV::BVCONST == k2)
+ return in1.GetSTPMgr()->ASTFalse;
+
+ //last resort is to CreateNode
+ return hashing.CreateNode(BEEV::EQ, children);
+}
+
+// Constant children are accumulated in "accumconst".
+ASTNode SimplifyingNodeFactory::CreateSimpleXor(const ASTVec &children)
+{
+ if (debug_simplifyingNodeFactory)
+ {
+ cout << "========" << endl << "CreateSimpXor ";
+ lpvec(children);
+ cout << endl;
+ }
+
+ ASTVec flat_children; // empty vector
+ flat_children = children;
+
+ // sort so that identical nodes occur in sequential runs, followed by
+ // their negations.
+ SortByExprNum(flat_children);
+
+ // This is the C Boolean value of all constant args seen. It is initially
+ // 0. TRUE children cause it to change value.
+ bool accumconst = 0;
+
+ ASTVec new_children;
+ new_children.reserve(children.size());
+
+ const ASTVec::const_iterator it_end = flat_children.end();
+ ASTVec::iterator next_it;
+ for (ASTVec::iterator it = flat_children.begin(); it != it_end; it++)
+ {
+ next_it = it + 1;
+ bool nextexists = (next_it < it_end);
+
+ if (ASTTrue == *it)
+ {
+ accumconst = !accumconst;
+ }
+ else if (ASTFalse == *it)
+ {
+ // Ignore it
+ }
+ else if (nextexists && (*next_it == *it))
+ {
+ // x XOR x = FALSE. Skip current, write "false" into next_it
+ // so that it gets tossed, too.
+ *next_it = ASTFalse;
+ }
+ else if (nextexists && (next_it->GetKind() == BEEV::NOT)
+ && ((*next_it)[0] == *it))
+ {
+ // x XOR NOT x = TRUE. Skip current, write "true" into next_it
+ // so that it gets tossed, too.
+ *next_it = ASTTrue;
+ }
+ else if (BEEV::NOT == it->GetKind())
+ {
+ // If child is (NOT alpha), we can flip accumconst and use alpha.
+ // This is ok because (NOT alpha) == TRUE XOR alpha
+ accumconst = !accumconst;
+ // CreateSimpNot just takes child of not.
+ new_children.push_back(CreateSimpleNot(*it));
+ }
+ else
+ {
+ new_children.push_back(*it);
+ }
+ }
+
+ ASTNode retval;
+
+ // Children should be non-constant.
+ if (new_children.size() < 2)
+ {
+ if (0 == new_children.size())
+ {
+ // XOR(TRUE, FALSE) -- accumconst will be 1.
+ if (accumconst)
+ {
+ retval = ASTTrue;
+ }
+ else
+ {
+ retval = ASTFalse;
+ }
+ }
+ else
+ {
+ // there is just one child
+ // XOR(x, TRUE) -- accumconst will be 1.
+ if (accumconst)
+ {
+ retval = CreateSimpleNot(new_children[0]);
+ }
+ else
+ {
+ retval = new_children[0];
+ }
+ }
+ }
+ else
+ {
+ // negate first child if accumconst == 1
+ if (accumconst)
+ {
+ new_children[0] = CreateSimpleNot(new_children[0]);
+ }
+ retval = hashing.CreateNode(BEEV::XOR, new_children);
+ }
+
+ if (debug_simplifyingNodeFactory)
+ {
+ cout << "returns " << retval << endl;
+ }
+ return retval;
+}
+
+// FIXME: How do I know whether ITE is a formula or not?
+ASTNode SimplifyingNodeFactory::CreateSimpleFormITE(const ASTVec& children)
+{
+
+ const ASTNode& child0 = children[0];
+ const ASTNode& child1 = children[1];
+ const ASTNode& child2 = children[2];
+
+ ASTNode retval;
+
+ if (debug_simplifyingNodeFactory)
+ {
+ cout << "========" << endl << "CreateSimpleFormITE " << child0
+ << child1 << child2 << endl;
+ }
+
+ if (ASTTrue == child0)
+ {
+ retval = child1;
+ }
+ else if (ASTFalse == child0)
+ {
+ retval = child2;
+ }
+ else if (child1 == child2)
+ {
+ retval = child1;
+ }
+ // ITE(x, TRUE, y ) == x OR y
+ else if (ASTTrue == child1)
+ {
+ retval = CreateSimpleAndOr(0, child0, child2);
+ }
+ // ITE(x, FALSE, y ) == (!x AND y)
+ else if (ASTFalse == child1)
+ {
+ retval = CreateSimpleAndOr(1, CreateSimpleNot(child0), child2);
+ }
+ // ITE(x, y, TRUE ) == (!x OR y)
+ else if (ASTTrue == child2)
+ {
+ retval = CreateSimpleAndOr(0, CreateSimpleNot(child0), child1);
+ }
+ // ITE(x, y, FALSE ) == (x AND y)
+ else if (ASTFalse == child2)
+ {
+ retval = CreateSimpleAndOr(1, child0, child1);
+ }
+ else
+ {
+ retval = hashing.CreateNode(BEEV::ITE, children);
+ }
+
+ if (debug_simplifyingNodeFactory)
+ {
+ cout << "returns " << retval << endl;
+ }
+
+ return retval;
+}
+
+ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width,
+ const ASTVec &children)
+{
+
+ if (!is_Term_kind(kind))
+ FatalError("CreateTerm: Illegal kind to CreateTerm:", ASTUndefined,
+ kind);
+
+ // If all the parameters are constant, return the constant value.
+ bool allConstant = true;
+ for (unsigned i = 0; i < children.size(); i++)
+ if (!children[i].isConstant())
+ {
+ allConstant = false;
+ break;
+ }
+
+ assert(bm.hashingNodeFactory == &hashing);
+
+ if (allConstant)
+ {
+ const ASTNode& hash = hashing.CreateTerm(kind, width, children);
+ const ASTNode& c = simplifier->BVConstEvaluator(hash);
+ return c;
+ }
+
+ ASTNode result;
+
+ switch (kind)
+ {
+
+ case BEEV::BVNEG:
+ {
+ switch (children[0].GetKind())
+ {
+
+ case BEEV::BVNEG:
+ result = children[0][0];
+ break;
+ default: // quieten compiler.
+ break;
+
+ }
+ }
+ break;
+ default: // quieten compiler.
+ break;
+
+ }
+
+ if (result.IsNull())
+ result = hashing.CreateTerm(kind, width, children);
+
+ return result;
+
+}
--- /dev/null
+/* A node factory that:
+ * * Sorts children to increases sharing,
+ * * Performs constant evaluation,
+ * * performs simplify boolean simplifications,
+ * * converts less thans to greater thans.
+ *
+ * NOTE: CreateNode doesn't necessary return a node with the same Kind as what it was called
+ * with. For example: (AND TRUE FALSE) will return FALSE. Which isn't an AND node.
+ *
+ * The intention is to never create nodes that will later be simplified by single level
+ * re-write rules. So we will never create the node (NOT(NOT x)). This is and example of
+ * a multi-level rule that never increases the global number of nodes.
+ *
+ * These rules never increase the total number of nodes. They are complimented by
+ * multi-level re-write rules that consider the global reference count when simplifying.
+ *
+ */
+
+#ifndef SIMPLIFYINGNODEFACTORY_H
+#define SIMPLIFYINGNODEFACTORY_H
+
+#include "NodeFactory.h"
+#include "../../STPManager/STPManager.h"
+#include "../../simplifier/simplifier.h"
+
+using BEEV::ASTNode;
+using BEEV::ASTVec;
+using BEEV::Simplifier;
+
+class SimplifyingNodeFactory: public NodeFactory
+{
+
+private:
+ HashingNodeFactory& hashing;
+ BEEV::STPMgr& bm; // Only here until the const evaluator is pulled out.
+
+ const ASTNode& ASTTrue;
+ const ASTNode& ASTFalse;
+ const ASTNode& ASTUndefined;
+
+ ASTNode CreateSimpleFormITE(const ASTVec &children);
+ ASTNode CreateSimpleXor(const ASTVec &children);
+ ASTNode CreateSimpleAndOr(bool IsAnd, const ASTVec &children);
+ ASTNode CreateSimpleAndOr(bool IsAnd, const ASTNode& form1,
+ const ASTNode& form2);
+ ASTNode CreateSimpleNot(const ASTNode& form);
+ ASTNode CreateSimpleNot(const ASTVec& children);
+
+ ASTNode CreateSimpleEQ(const ASTVec& children);
+
+ SimplifyingNodeFactory(const SimplifyingNodeFactory& );
+ SimplifyingNodeFactory& operator=(const SimplifyingNodeFactory&);
+
+ // Just here to access the Constant Evaluator.
+ Simplifier * simplifier;
+
+
+public:
+
+ virtual BEEV::ASTNode CreateNode(BEEV::Kind kind, const BEEV::ASTVec & children);
+ virtual BEEV::ASTNode CreateTerm(BEEV::Kind kind, unsigned int width, const BEEV::ASTVec &children);
+
+
+ SimplifyingNodeFactory(HashingNodeFactory& raw_, BEEV::STPMgr& bm_)
+ :hashing(raw_), bm(bm_), ASTTrue(bm.ASTTrue), ASTFalse(bm.ASTFalse), ASTUndefined(bm.ASTUndefined)
+ {
+ simplifier = new Simplifier(&bm);
+ }
+ ;
+ ~SimplifyingNodeFactory()
+ {
+ delete simplifier;
+ }
+
+};
+
+#endif
--- /dev/null
+#include "TypeChecker.h"
+#include "../AST.h"
+
+BEEV::ASTNode TypeChecker::CreateTerm(BEEV::Kind kind, unsigned int width, const BEEV::ASTVec &children)
+{
+ BEEV::ASTNode r = f.CreateTerm(kind,width,children);
+ BVTypeCheck(r);
+ return r;
+}
+
+//virtual BEEV::ASTNode CreateNode(BEEV::Kind kind, const BEEV::ASTVec& children);
+BEEV::ASTNode TypeChecker::CreateNode(BEEV::Kind kind, const BEEV::ASTVec& children)
+{
+ BEEV::ASTNode r = f.CreateNode(kind,children);
+ BVTypeCheck(r);
+ return r;
+}
+
+BEEV::ASTNode TypeChecker::CreateArrayTerm(Kind kind, unsigned int index,
+ unsigned int width, const BEEV::ASTVec &children)
+{
+ ASTNode r = f.CreateTerm(kind, width, children);
+ r.SetIndexWidth(index);
+ BVTypeCheck(r);
+ return r;
+}
+
--- /dev/null
+/*
+ A decorator pattern, which calls some base node factory, then type checks each of the results.
+ */
+
+#ifndef TYPECHECKER_H_
+#define TYPECHECKER_H_
+
+#include "NodeFactory.h"
+#include "../STPManager/STPManager.h"
+
+namespace BEEV
+{
+class BeevMgr;
+}
+using BEEV::STPMgr;
+
+class TypeChecker : public NodeFactory
+{
+NodeFactory& f;
+STPMgr& bm;
+
+public:
+ TypeChecker(NodeFactory& f_, STPMgr& bm_) : f(f_), bm(bm_)
+ {}
+
+ BEEV::ASTNode CreateTerm(BEEV::Kind kind, unsigned int width, const BEEV::ASTVec &children);
+ BEEV::ASTNode CreateNode(BEEV::Kind kind, const BEEV::ASTVec& children);
+ BEEV::ASTNode CreateArrayTerm(Kind kind, unsigned int index,unsigned int width, const BEEV::ASTVec &children);
+
+};
+
+#endif /* TYPECHECKER_H_ */
"#define TESTKINDS_H\n",
"// Generated automatically by genkinds.pl from ASTKind.kinds $now.\n",
"// Do not edit\n",
+ "#include <iostream>\n",
"namespace BEEV {\n typedef enum {\n";
for (@kindnames) {
- ////////////////////////////////////////////////////////////////
- // STPMgr members
- ////////////////////////////////////////////////////////////////
- ASTNode STPMgr::CreateNode(Kind kind, const ASTVec & back_children)
- {
- // create a new node. Children will be modified.
- ASTInterior *n_ptr = new ASTInterior(kind);
-
- // insert all of children at end of new_children.
- ASTNode n(CreateInteriorNode(kind, n_ptr, back_children));
- return n;
- }
-
- ASTNode STPMgr::CreateNode(Kind kind,
- const ASTNode& child0,
- const ASTVec & back_children)
- {
-
- ASTInterior *n_ptr = new ASTInterior(kind);
- ASTVec &front_children = n_ptr->_children;
- front_children.push_back(child0);
- ASTNode n(CreateInteriorNode(kind, n_ptr, back_children));
- return n;
- }
-
- ASTNode STPMgr::CreateNode(Kind kind,
- const ASTNode& child0,
- const ASTNode& child1,
- const ASTVec & back_children)
- {
- ASTInterior *n_ptr = new ASTInterior(kind);
- ASTVec &front_children = n_ptr->_children;
- front_children.push_back(child0);
- front_children.push_back(child1);
- ASTNode n(CreateInteriorNode(kind, n_ptr, back_children));
- return n;
- }
-
- ASTNode STPMgr::CreateNode(Kind kind,
- const ASTNode& child0,
- const ASTNode& child1,
- const ASTNode& child2,
- const ASTVec & back_children)
- {
- ASTInterior *n_ptr = new ASTInterior(kind);
- ASTVec &front_children = n_ptr->_children;
- front_children.push_back(child0);
- front_children.push_back(child1);
- front_children.push_back(child2);
- ASTNode n(CreateInteriorNode(kind, n_ptr, back_children));
- return n;
- }
ASTInterior *STPMgr::CreateInteriorNode(Kind kind,
// children array of this
}
}
- // Create and return an ASTNode for a term
- ASTNode STPMgr::CreateTerm(Kind kind,
- unsigned int width,
- const ASTVec &children)
- {
- if (!is_Term_kind(kind))
- FatalError("CreateTerm: Illegal kind to CreateTerm:",
- ASTUndefined, kind);
- ASTNode n = CreateNode(kind, children);
- n.SetValueWidth(width);
-
- //by default we assume that the term is a Bitvector. If
- //necessary the indexwidth can be changed later
- n.SetIndexWidth(0);
- return n;
- }
-
- ASTNode STPMgr::CreateTerm(Kind kind,
- unsigned int width,
- const ASTNode& child0,
- const ASTVec &children)
- {
- if (!is_Term_kind(kind))
- FatalError("CreateTerm: Illegal kind to CreateTerm:",
- ASTUndefined, kind);
- ASTNode n = CreateNode(kind, child0, children);
- n.SetValueWidth(width);
- BVTypeCheck(n);
- return n;
- }
-
- ASTNode STPMgr::CreateTerm(Kind kind,
- unsigned int width,
- const ASTNode& child0,
- const ASTNode& child1,
- const ASTVec &children)
- {
- if (!is_Term_kind(kind))
- FatalError("CreateTerm: Illegal kind to CreateTerm:",
- ASTUndefined, kind);
- ASTNode n = CreateNode(kind, child0, child1, children);
- n.SetValueWidth(width);
- return n;
- }
-
- ASTNode STPMgr::CreateTerm(Kind kind,
- unsigned int width,
- const ASTNode& child0,
- const ASTNode& child1,
- const ASTNode& child2,
- const ASTVec &children)
- {
- if (!is_Term_kind(kind))
- FatalError("CreateTerm: Illegal kind to CreateTerm:",
- ASTUndefined, kind);
- ASTNode n = CreateNode(kind, child0, child1, child2, children);
- n.SetValueWidth(width);
- return n;
- }
-
-
////////////////////////////////////////////////////////////////
//
// IO manipulators for Lisp format printing of AST.
#include "UserDefinedFlags.h"
#include "../AST/AST.h"
#include "../parser/let-funcs.h"
+#include "../AST/NodeFactory/HashingNodeFactory.h"
namespace BEEV
{
* Class STPMgr. This holds all "global" variables for the system,
* such as unique tables for the various kinds of nodes.
*****************************************************************/
+
class STPMgr
{
friend class ASTNode;
friend class ASTInterior;
friend class ASTBVConst;
friend class ASTSymbol;
+ friend BEEV::ASTNode HashingNodeFactory::CreateNode(const Kind kind, const BEEV::ASTVec & back_children);
private:
/****************************************************************
ASTNode dummy_node;
+ public:
+ HashingNodeFactory* hashingNodeFactory;
+ NodeFactory *defaultNodeFactory;
+
//frequently used nodes
ASTNode ASTFalse, ASTTrue, ASTUndefined;
+ private:
// Stack of Logical Context. each entry in the stack is a logical
// context. A logical context is a vector of assertions. The
Begin_RemoveWrites = false;
SimplifyWrites_InPlace_Flag = false;
+ // Need to initiate the node factories before any nodes are created.
+ hashingNodeFactory = new HashingNodeFactory(*this);
+ defaultNodeFactory= hashingNodeFactory;
+
ASTFalse = CreateNode(FALSE);
ASTTrue = CreateNode(TRUE);
ASTUndefined = CreateNode(UNDEFINED);
****************************************************************/
// Create and return an interior ASTNode
- ASTNode CreateNode(Kind kind,
- const ASTVec &children = _empty_ASTVec);
- ASTNode CreateNode(Kind kind,
- const ASTNode& child0,
- const ASTVec &children = _empty_ASTVec);
- ASTNode CreateNode(Kind kind,
- const ASTNode& child0,
- const ASTNode& child1,
- const ASTVec &children = _empty_ASTVec);
- ASTNode CreateNode(Kind kind,
- const ASTNode& child0,
- const ASTNode& child1,
- const ASTNode& child2,
- const ASTVec &children = _empty_ASTVec);
+ inline BEEV::ASTNode CreateNode(BEEV::Kind kind, const BEEV::ASTVec& children = _empty_ASTVec)
+ {
+ return defaultNodeFactory->CreateNode(kind,children);
+ }
+
+ inline ASTNode CreateNode(Kind kind, const ASTNode& child0, const ASTVec & back_children = _empty_ASTVec)
+ {
+ return defaultNodeFactory->CreateNode(kind, child0, back_children);
+ }
+
+ inline ASTNode CreateNode(Kind kind, const ASTNode& child0, const ASTNode& child1, const ASTVec & back_children = _empty_ASTVec)
+ {
+ return defaultNodeFactory->CreateNode(kind, child0, child1, back_children);
+ }
+
+ inline ASTNode CreateNode(Kind kind, const ASTNode& child0, const ASTNode& child1, const ASTNode& child2, const ASTVec & back_children = _empty_ASTVec)
+ {
+ return defaultNodeFactory->CreateNode(kind, child0, child1, child2, back_children);
+
+ }
/****************************************************************
* Create Term functions *
****************************************************************/
// Create and return an ASTNode for a term
- ASTNode CreateTerm(Kind kind,
- unsigned int width,
- const ASTVec &children = _empty_ASTVec);
- ASTNode CreateTerm(Kind kind,
- unsigned int width,
- const ASTNode& child0,
- const ASTVec &children = _empty_ASTVec);
- ASTNode CreateTerm(Kind kind,
- unsigned int width,
- const ASTNode& child0,
- const ASTNode& child1,
- const ASTVec &children = _empty_ASTVec);
- ASTNode CreateTerm(Kind kind,
- unsigned int width,
- const ASTNode& child0,
- const ASTNode& child1,
- const ASTNode& child2,
- const ASTVec &children = _empty_ASTVec);
+ inline BEEV::ASTNode CreateTerm(BEEV::Kind kind, unsigned int width, const BEEV::ASTVec &children =_empty_ASTVec)
+ {
+ return defaultNodeFactory->CreateTerm(kind,width,children);
+ }
+
+ inline ASTNode CreateTerm(Kind kind, unsigned int width,
+ const ASTNode& child0, const ASTVec &children = _empty_ASTVec) {
+ return defaultNodeFactory->CreateTerm(kind, width, child0, children);
+ }
+
+ inline ASTNode CreateTerm(Kind kind, unsigned int width,
+ const ASTNode& child0, const ASTNode& child1, const ASTVec &children = _empty_ASTVec) {
+ return defaultNodeFactory->CreateTerm(kind,width, child0, child1,children);
+ }
+
+ inline ASTNode CreateTerm(Kind kind, unsigned int width,
+ const ASTNode& child0, const ASTNode& child1, const ASTNode& child2,
+ const ASTVec &children = _empty_ASTVec) {
+ return defaultNodeFactory->CreateTerm(kind, width, child0, child1, child2);
+ }
/****************************************************************
_interior_unique_table.clear();
_bvconst_unique_table.clear();
_symbol_unique_table.clear();
+
+ delete hashingNodeFactory;
}
};//End of Class STPMgr
};//end of namespace
// Function that computes various kinds of statistics for the phases
// of STP
void CountersAndStats(const char * functionname, STPMgr * bm);
+
}; //end of namespace BEEV
#endif
depend: $(SRCS)
@$(CXX) -MM -MG $(CXXFLAGS) $(SRCS) > $@
-#-include ./depend
+-include ./depend
# Tests that run under valgrind will return a non-zero error code on
# either leak, or use of unitialised values.
include ../../scripts/Makefile.common
-CXXFLAGS= -DEXT_HASH_MAP $(CFLAGS) -I../../src/c_interface -L../../lib
+CXXFLAGS= -DEXT_HASH_MAP $(CFLAGS) -I../../src/c_interface -L../../lib -L../../src/AST
+LIBS= -lstp -last
VALGRINDPATH=`which valgrind`
ifeq "$(VALGRINDPATH)" ""
rm -rf *.out
0:
- g++ $(CXXFLAGS) array-cvcl-02.c -o a0.out -lstp
+ g++ $(CXXFLAGS) array-cvcl-02.c -o a0.out $(LIBS)
./a0.out
1:
- g++ $(CXXFLAGS) b4-c.c -lstp -o a1.out
+ g++ $(CXXFLAGS) b4-c.c -lstp -o a1.out $(LIBS)
./a1.out
2:
- g++ $(CXXFLAGS) b4-c2.c -lstp -o a2.out
+ g++ $(CXXFLAGS) b4-c2.c -lstp -o a2.out $(LIBS)
./a2.out
3:
- g++ $(CXXFLAGS) getbvunsignedlonglong-check.c -lstp -o a3.out
+ g++ $(CXXFLAGS) getbvunsignedlonglong-check.c -o a3.out $(LIBS)
$(VALGRIND) ./a3.out
4:
- g++ $(CXXFLAGS) multiple-queries.c -lstp -o a4.out
+ g++ $(CXXFLAGS) multiple-queries.c -o a4.out $(LIBS)
./a4.out
5:
- g++ $(CXXFLAGS) parsefile-using-cinterface.c -lstp -o a5.out
+ g++ $(CXXFLAGS) parsefile-using-cinterface.c -o a5.out $(LIBS)
./a5.out
6:
- g++ $(CXXFLAGS) print.c -lstp -o a6.out
+ g++ $(CXXFLAGS) print.c -o a6.out $(LIBS)
./a6.out
7:
- g++ $(CXXFLAGS) push-pop-1.c -lstp -o a7.out
+ g++ $(CXXFLAGS) push-pop-1.c -o a7.out $(LIBS)
./a7.out
8:
- g++ $(CXXFLAGS) sbvmod.c -lstp -o a8.out
+ g++ $(CXXFLAGS) sbvmod.c -o a8.out $(LIBS)
./a8.out
9:
- g++ $(CXXFLAGS) simplify.c -o a9.out -lstp
+ g++ $(CXXFLAGS) simplify.c -o a9.out $(LIBS)
./a9.out
10:
- g++ $(CXXFLAGS) simplify1.c -lstp -o a10.out
+ g++ $(CXXFLAGS) simplify1.c -o a10.out $(LIBS)
./a10.out
11:
- g++ $(CXXFLAGS) squares-leak.c -lstp -o a11.out
+ g++ $(CXXFLAGS) squares-leak.c -o a11.out $(LIBS)
$(VALGRIND) ./a11.out
12:
- g++ $(CXXFLAGS) stp-counterex.c -lstp -o a12.out
+ g++ $(CXXFLAGS) stp-counterex.c -o a12.out $(LIBS)
./a12.out
13:
- g++ $(CXXFLAGS) stp-div-001.c -lstp -o a13.out
+ g++ $(CXXFLAGS) stp-div-001.c -o a13.out $(LIBS)
./a13.out
14:
- g++ $(CXXFLAGS) stpcheck.c -o a14.out -lstp
+ g++ $(CXXFLAGS) stpcheck.c -o a14.out $(LIBS)
./a14.out
15:
- g++ $(CXXFLAGS) x.c -lstp -o a15.out
+ g++ $(CXXFLAGS) x.c -o a15.out $(LIBS)
$(VALGRIND) ./a15.out
16:
- g++ $(CXXFLAGS) y.c -lstp -o a16.out
+ g++ $(CXXFLAGS) y.c -lstp -o a16.out $(LIBS)
./a16.out
17:
- g++ $(CXXFLAGS) push-pop.c -lstp -o a17.out
+ g++ $(CXXFLAGS) push-pop.c -o a17.out $(LIBS)
./a17.out
18:
- g++ $(CXXFLAGS) cvc-to-c.cpp -lstp -o a18.out
+ g++ $(CXXFLAGS) cvc-to-c.cpp -o a18.out $(LIBS)
#./a18.out ./t.cvc
19:
- g++ -g $(CXXFLAGS) biosat-rna.cpp -lstp -o a19.out
+ g++ -g $(CXXFLAGS) biosat-rna.cpp -o a19.out $(LIBS)
./a19.out AUUGGUAUGUAAGCUACUUCUUCCAAGACCA 800
20:
- g++ -g $(CXXFLAGS) leak.c -lstp -o a20.out
+ g++ -g $(CXXFLAGS) leak.c -o a20.out $(LIBS)
$(VALGRIND) ./a20.out
clean:
projects / francis / stp.git / commitdiff