From 43b7885a8ff46375c13dc141c63fd69e60d7b21a Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Mon, 1 Feb 2010 12:51:01 +0000 Subject: [PATCH] NodeFactory classes that are used to build functions. The HashingNodeFactory uses existing code to perform structural hashing. The SimplifyingNodeFactory applies straight forward simplifications. The TypeCheck wraps around another node factory to type check each node after it's created. Classes that currently take an STPManager as a parameter, but just use it to create nodes will over time be changed to instead take a node factory. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@581 e59a4935-1847-0410-ae03-e826735625c1 --- scripts/Makefile.common | 2 +- src/AST/AST.h | 2 + src/AST/ASTInterior.h | 1 + src/AST/ASTNode.h | 31 ++ src/AST/ASTmisc.cpp | 26 + src/AST/Makefile | 3 +- src/AST/NodeFactory/HashingNodeFactory.cpp | 47 ++ src/AST/NodeFactory/HashingNodeFactory.h | 27 + src/AST/NodeFactory/NodeFactory.cpp | 105 ++++ src/AST/NodeFactory/NodeFactory.h | 58 ++ .../NodeFactory/SimplifyingNodeFactory.cpp | 497 ++++++++++++++++++ src/AST/NodeFactory/SimplifyingNodeFactory.h | 77 +++ src/AST/NodeFactory/TypeChecker.cpp | 27 + src/AST/NodeFactory/TypeChecker.h | 32 ++ src/AST/genkinds.pl | 1 + src/STPManager/STPManager.cpp | 113 ---- src/STPManager/STPManager.h | 86 +-- src/main/Globals.h | 1 + src/printer/Makefile | 2 +- tests/c-api-tests/Makefile | 45 +- 20 files changed, 1013 insertions(+), 170 deletions(-) create mode 100644 src/AST/NodeFactory/HashingNodeFactory.cpp create mode 100644 src/AST/NodeFactory/HashingNodeFactory.h create mode 100644 src/AST/NodeFactory/NodeFactory.cpp create mode 100644 src/AST/NodeFactory/NodeFactory.h create mode 100644 src/AST/NodeFactory/SimplifyingNodeFactory.cpp create mode 100644 src/AST/NodeFactory/SimplifyingNodeFactory.h create mode 100644 src/AST/NodeFactory/TypeChecker.cpp create mode 100644 src/AST/NodeFactory/TypeChecker.h diff --git a/scripts/Makefile.common b/scripts/Makefile.common index fd03be4..7573f09 100644 --- a/scripts/Makefile.common +++ b/scripts/Makefile.common @@ -74,7 +74,7 @@ ifeq ($(shell uname -s), DarwinX) 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 diff --git a/src/AST/AST.h b/src/AST/AST.h index 7d12dcb..09e5446 100644 --- a/src/AST/AST.h +++ b/src/AST/AST.h @@ -25,6 +25,8 @@ namespace BEEV 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 diff --git a/src/AST/ASTInterior.h b/src/AST/ASTInterior.h index b003959..a6e6044 100644 --- a/src/AST/ASTInterior.h +++ b/src/AST/ASTInterior.h @@ -29,6 +29,7 @@ namespace BEEV friend class STPMgr; friend class ASTNodeHasher; friend class ASTNodeEqual; + friend class HashingNodeFactory; private: /****************************************************************** diff --git a/src/AST/ASTNode.h b/src/AST/ASTNode.h index c0ecbc6..5e83aa5 100644 --- a/src/AST/ASTNode.h +++ b/src/AST/ASTNode.h @@ -8,6 +8,7 @@ ********************************************************************/ #ifndef ASTNODE_H #define ASTNODE_H +#include "../AST/NodeFactory/HashingNodeFactory.h" /******************************************************************** * This file gives the class description of the ASTNode class * @@ -27,6 +28,7 @@ namespace BEEV friend class CNFMgr; friend class ASTInterior; friend class vector; + friend BEEV::ASTNode HashingNodeFactory::CreateNode(const Kind kind, const BEEV::ASTVec & back_children); private: /**************************************************************** @@ -139,6 +141,35 @@ namespace BEEV } } //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; diff --git a/src/AST/ASTmisc.cpp b/src/AST/ASTmisc.cpp index 65238d7..5a9f928 100644 --- a/src/AST/ASTmisc.cpp +++ b/src/AST/ASTmisc.cpp @@ -16,6 +16,32 @@ namespace BEEV * 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) diff --git a/src/AST/Makefile b/src/AST/Makefile index ce1c4fc..46e8cad 100644 --- a/src/AST/Makefile +++ b/src/AST/Makefile @@ -1,6 +1,7 @@ include ../../scripts/Makefile.common SRCS=$(wildcard *.cpp) +SRCS+=$(wildcard NodeFactory/*.cpp) OBJS = $(SRCS:.cpp=.o) OBJS+= ASTKind.o CFLAGS += -I$(MTL) @@ -17,7 +18,7 @@ ASTKind.h ASTKind.cpp: ASTKind.kinds genkinds.pl .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". diff --git a/src/AST/NodeFactory/HashingNodeFactory.cpp b/src/AST/NodeFactory/HashingNodeFactory.cpp new file mode 100644 index 0000000..8034834 --- /dev/null +++ b/src/AST/NodeFactory/HashingNodeFactory.cpp @@ -0,0 +1,47 @@ +#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; +} + + diff --git a/src/AST/NodeFactory/HashingNodeFactory.h b/src/AST/NodeFactory/HashingNodeFactory.h new file mode 100644 index 0000000..809826c --- /dev/null +++ b/src/AST/NodeFactory/HashingNodeFactory.h @@ -0,0 +1,27 @@ +// 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_ */ diff --git a/src/AST/NodeFactory/NodeFactory.cpp b/src/AST/NodeFactory/NodeFactory.cpp new file mode 100644 index 0000000..756191a --- /dev/null +++ b/src/AST/NodeFactory/NodeFactory.cpp @@ -0,0 +1,105 @@ +#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; +} + diff --git a/src/AST/NodeFactory/NodeFactory.h b/src/AST/NodeFactory/NodeFactory.h new file mode 100644 index 0000000..1317ad9 --- /dev/null +++ b/src/AST/NodeFactory/NodeFactory.h @@ -0,0 +1,58 @@ +// Abstract base class for all the node factories. +#ifndef NODEFACTORY_H +#define NODEFACTORY_H + +#include +#include "ASTKind.h" + +namespace BEEV +{ +class ASTNode; +typedef std::vector 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 diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp new file mode 100644 index 0000000..345ba25 --- /dev/null +++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp @@ -0,0 +1,497 @@ +// nb. Some of the simplifications are duplicated with minor differences in the STPManager class. + +#include "../../AST/AST.h" +#include +#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; + +} diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.h b/src/AST/NodeFactory/SimplifyingNodeFactory.h new file mode 100644 index 0000000..f2f8d0b --- /dev/null +++ b/src/AST/NodeFactory/SimplifyingNodeFactory.h @@ -0,0 +1,77 @@ +/* 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 diff --git a/src/AST/NodeFactory/TypeChecker.cpp b/src/AST/NodeFactory/TypeChecker.cpp new file mode 100644 index 0000000..2ef2afc --- /dev/null +++ b/src/AST/NodeFactory/TypeChecker.cpp @@ -0,0 +1,27 @@ +#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; +} + diff --git a/src/AST/NodeFactory/TypeChecker.h b/src/AST/NodeFactory/TypeChecker.h new file mode 100644 index 0000000..dd23762 --- /dev/null +++ b/src/AST/NodeFactory/TypeChecker.h @@ -0,0 +1,32 @@ +/* + 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_ */ diff --git a/src/AST/genkinds.pl b/src/AST/genkinds.pl index 1eaa407..672e14e 100755 --- a/src/AST/genkinds.pl +++ b/src/AST/genkinds.pl @@ -59,6 +59,7 @@ sub gen_h_file { "#define TESTKINDS_H\n", "// Generated automatically by genkinds.pl from ASTKind.kinds $now.\n", "// Do not edit\n", + "#include \n", "namespace BEEV {\n typedef enum {\n"; for (@kindnames) { diff --git a/src/STPManager/STPManager.cpp b/src/STPManager/STPManager.cpp index c74637d..a1b92a8 100644 --- a/src/STPManager/STPManager.cpp +++ b/src/STPManager/STPManager.cpp @@ -43,58 +43,6 @@ namespace BEEV - //////////////////////////////////////////////////////////////// - // 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 @@ -393,67 +341,6 @@ namespace BEEV } } - // 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. diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h index 4f9b412..c5a53b1 100644 --- a/src/STPManager/STPManager.h +++ b/src/STPManager/STPManager.h @@ -13,6 +13,7 @@ #include "UserDefinedFlags.h" #include "../AST/AST.h" #include "../parser/let-funcs.h" +#include "../AST/NodeFactory/HashingNodeFactory.h" namespace BEEV { @@ -20,12 +21,14 @@ 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: /**************************************************************** @@ -70,8 +73,13 @@ namespace BEEV 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 @@ -175,6 +183,10 @@ namespace BEEV 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); @@ -268,44 +280,52 @@ namespace BEEV ****************************************************************/ // 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); + } /**************************************************************** @@ -404,6 +424,8 @@ namespace BEEV _interior_unique_table.clear(); _bvconst_unique_table.clear(); _symbol_unique_table.clear(); + + delete hashingNodeFactory; } };//End of Class STPMgr };//end of namespace diff --git a/src/main/Globals.h b/src/main/Globals.h index 235f139..847c7dd 100644 --- a/src/main/Globals.h +++ b/src/main/Globals.h @@ -92,6 +92,7 @@ namespace BEEV // Function that computes various kinds of statistics for the phases // of STP void CountersAndStats(const char * functionname, STPMgr * bm); + }; //end of namespace BEEV #endif diff --git a/src/printer/Makefile b/src/printer/Makefile index 0c1030d..c3e0baa 100644 --- a/src/printer/Makefile +++ b/src/printer/Makefile @@ -17,5 +17,5 @@ clean: depend: $(SRCS) @$(CXX) -MM -MG $(CXXFLAGS) $(SRCS) > $@ -#-include ./depend +-include ./depend diff --git a/tests/c-api-tests/Makefile b/tests/c-api-tests/Makefile index 01447da..23c3da0 100644 --- a/tests/c-api-tests/Makefile +++ b/tests/c-api-tests/Makefile @@ -1,7 +1,8 @@ # 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)" "" @@ -15,70 +16,70 @@ all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18 19 20 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: -- 2.47.3