Skip to content

Commit

Permalink
ram lat norm modified
Browse files Browse the repository at this point in the history
  • Loading branch information
@QXG2
QXG2 committed Jan 16, 2020
1 parent 4f6c2f2 commit 642b0d1
Show file tree
Hide file tree
Showing 12 changed files with 1,358 additions and 1,079 deletions.
10 changes: 9 additions & 1 deletion src/AstRelation.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -90,6 +90,9 @@ class AstRelation : public AstNode {

/** Set lattice flag for this relation **/
void setLattice() {
// check if the last variable is enum type variable,
// and the other variables are not

LatticeFlag = true;
}

Expand Down Expand Up @@ -202,7 +205,12 @@ class AstRelation : public AstNode {

/** Print string representation of the relation to a given output stream */
void print(std::ostream& os) const override {
os << ".decl " << this->getName() << "(";
if (LatticeFlag) {
os << ".lat ";
} else {
os << ".decl ";
}
os << this->getName() << "(";
if (!attributes.empty()) {
os << attributes[0]->getAttributeName() << ":" << attributes[0]->getTypeName();

Expand Down
27 changes: 27 additions & 0 deletions src/AstSemanticChecker.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -629,6 +629,33 @@ void AstSemanticChecker::checkRelationDeclaration(ErrorReport& report,
attr->getSrcLoc());
}

/* added by Qing Gong: if it is lattice relation, the last
* variable should be enum, and other variables are not. */
if (relation.isLattice()) {
if (i == relation.getArity() - 1) {
// last variable
if (!isEnumType(typeEnv.getType(typeName))) {
report.addError(
"Last variable must be Enum for lattice relation",
attr->getSrcLoc());
}
} else {
// not the last variable
if (isEnumType(typeEnv.getType(typeName))) {
report.addError(
"Variables other than the last one cannot be Enum for lattice relation",
attr->getSrcLoc());
}
}

} else {
if (isEnumType(typeEnv.getType(typeName))) {
report.addError(
"Variables cannot be Enum for non-lattice relation",
attr->getSrcLoc());
}
}

/* check whether name occurs more than once */
for (size_t j = 0; j < i; j++) {
if (attr->getAttributeName()
Expand Down
105 changes: 89 additions & 16 deletions src/AstTranslator.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -252,14 +252,14 @@ std::unique_ptr<RamRelationReference> AstTranslator::createRelationReference(
const std::string name, const size_t arity,
const std::vector<std::string> attributeNames,
const std::vector<std::string> attributeTypeQualifiers,
const SymbolMask mask, const EnumTypeMask enumTypeMask, const RelationRepresentation representation,
const bool latticeFlag) {
const SymbolMask mask, const EnumTypeMask enumTypeMask,
const RelationRepresentation representation, const bool latticeFlag) {
const RamRelation* ramRel = ramProg->getRelation(name);
if (ramRel == nullptr) {
ramProg->addRelation(
std::make_unique<RamRelation>(name, arity, attributeNames,
attributeTypeQualifiers, mask, enumTypeMask, representation,
latticeFlag));
attributeTypeQualifiers, mask, enumTypeMask,
representation, latticeFlag));
ramRel = ramProg->getRelation(name);
assert(ramRel != nullptr && "cannot find relation");
}
Expand All @@ -268,8 +268,8 @@ std::unique_ptr<RamRelationReference> AstTranslator::createRelationReference(

std::unique_ptr<RamRelationReference> AstTranslator::createRelationReference(
const std::string name, const size_t arity) {
return createRelationReference(name, arity, { }, { }, SymbolMask(arity), EnumTypeMask(arity),
{ });
return createRelationReference(name, arity, { }, { }, SymbolMask(arity),
EnumTypeMask(arity), { });
}

std::unique_ptr<RamRelationReference> AstTranslator::translateRelation(
Expand Down Expand Up @@ -299,7 +299,8 @@ std::unique_ptr<RamRelationReference> AstTranslator::translateRelation(
return createRelationReference(
relationNamePrefix + getRelationName(rel->getName()),
rel->getArity(), attributeNames, attributeTypeQualifiers,
getSymbolMask(*rel), getEnumTypeMask(*rel), rel->getRepresentation(), rel->isLattice());
getSymbolMask(*rel), getEnumTypeMask(*rel),
rel->getRepresentation(), rel->isLattice());
}

std::unique_ptr<RamRelationReference> AstTranslator::translateDeltaRelation(
Expand All @@ -312,6 +313,16 @@ std::unique_ptr<RamRelationReference> AstTranslator::translateNewRelation(
return translateRelation(rel, "@new_");
}

std::unique_ptr<RamRelationReference> AstTranslator::translateOrgLatRelation(
const AstRelation* rel) {
return translateRelation(rel, "@org_lat_");
}

std::unique_ptr<RamRelationReference> AstTranslator::translateNewLatRelation(
const AstRelation* rel) {
return translateRelation(rel, "@new_lat_");
}

std::unique_ptr<RamValue> AstTranslator::translateValue(const AstArgument* arg,
const ValueIndex& index) {
if (arg == nullptr) {
Expand Down Expand Up @@ -1438,6 +1449,10 @@ std::unique_ptr<RamStatement> AstTranslator::translateRecursiveRelation(
std::map<const AstRelation*, std::unique_ptr<RamRelationReference>> relDelta;
std::map<const AstRelation*, std::unique_ptr<RamRelationReference>> relNew;

// extra mappings for lattice relations
std::map<const AstRelation*, std::unique_ptr<RamRelationReference>> rrel_lat;
std::map<const AstRelation*, std::unique_ptr<RamRelationReference>> relNew_lat;

/* Compute non-recursive clauses for relations in scc and push
the results in their delta tables. */
for (const AstRelation* rel : scc) {
Expand All @@ -1447,19 +1462,41 @@ std::unique_ptr<RamStatement> AstTranslator::translateRecursiveRelation(
rrel[rel] = translateRelation(rel);
relDelta[rel] = translateDeltaRelation(rel);
relNew[rel] = translateNewRelation(rel);
if (rrel[rel]->isLattice()) {
rrel_lat[rel] = translateOrgLatRelation(rel);
relNew_lat[rel] = translateNewLatRelation(rel);
}

/* create update statements for fixpoint (even iteration) */
appendStmt(updateRelTable,
std::make_unique<RamMerge>(
std::unique_ptr<RamRelationReference>(
rrel[rel]->clone()),
std::unique_ptr<RamRelationReference>(
relNew[rel]->clone())));

// if there is relation with lattice, need to normalize it.
if (rrel[rel]->isLattice()) {
// added by Qing Gong
// if there is relation with lattice, need to normalize it.
appendStmt(updateRelTable,
std::make_unique<RamLatNorm>(
std::unique_ptr<RamRelationReference>(
rrel[rel]->clone()),
std::unique_ptr<RamRelationReference>(
relNew[rel]->clone()),
std::unique_ptr<RamRelationReference>(
rrel_lat[rel]->clone()),
std::unique_ptr<RamRelationReference>(
relNew_lat[rel]->clone())));
// add swaps for them
appendStmt(updateRelTable,
std::make_unique<RamSwap>(
std::unique_ptr<RamRelationReference>(
rrel[rel]->clone()),
std::unique_ptr<RamRelationReference>(
rrel_lat[rel]->clone())));
appendStmt(updateRelTable,
std::make_unique<RamSwap>(
std::unique_ptr<RamRelationReference>(
relNew[rel]->clone()),
std::unique_ptr<RamRelationReference>(
relNew_lat[rel]->clone())));
} else {
/* create update statements for fixpoint (even iteration) */
appendStmt(updateRelTable,
std::make_unique<RamMerge>(
std::unique_ptr<RamRelationReference>(
rrel[rel]->clone()),
std::unique_ptr<RamRelationReference>(
Expand All @@ -1478,6 +1515,17 @@ std::unique_ptr<RamStatement> AstTranslator::translateRecursiveRelation(
std::unique_ptr<RamRelationReference>(
relNew[rel]->clone())));

if (rrel[rel]->isLattice()) {
appendStmt(updateRelTable,
std::make_unique<RamClear>(
std::unique_ptr<RamRelationReference>(
rrel_lat[rel]->clone())));
appendStmt(updateRelTable,
std::make_unique<RamClear>(
std::unique_ptr<RamRelationReference>(
relNew_lat[rel]->clone())));
}

/* measure update time for each relation */
if (Global::config().has("profile")) {
updateRelTable = std::make_unique<RamLogTimer>(
Expand All @@ -1498,6 +1546,18 @@ std::unique_ptr<RamStatement> AstTranslator::translateRecursiveRelation(
std::unique_ptr<RamRelationReference>(
relNew[rel]->clone()))));

// added by Qing Gong: drop temporary lattice relations
if (rel->isLattice()) {
appendStmt(postamble,
std::make_unique<RamSequence>(
std::make_unique<RamDrop>(
std::unique_ptr<RamRelationReference>(
rrel_lat[rel]->clone())),
std::make_unique<RamDrop>(
std::unique_ptr<RamRelationReference>(
relNew_lat[rel]->clone()))));
}

/* Generate code for non-recursive part of relation */
appendStmt(preamble,
translateNonRecursiveRelation(*rel, recursiveClauses));
Expand Down Expand Up @@ -1875,6 +1935,19 @@ void AstTranslator::translateProgram(
std::make_unique<RamCreate>(
std::unique_ptr<RamRelationReference>(
translateNewRelation(relation))));

if (relation->isLattice()) {
appendStmt(current,
std::make_unique<RamCreate>(
std::unique_ptr<RamRelationReference>(
translateOrgLatRelation(
relation))));
appendStmt(current,
std::make_unique<RamCreate>(
std::unique_ptr<RamRelationReference>(
translateNewLatRelation(
relation))));
}
}
}

Expand Down
Loading

0 comments on commit 642b0d1

Please sign in to comment.