return v;
}
+ public int[] getRepairs(boolean negated) {
+ return new int[] {AbstractRepair.MODIFYRELATION};
+ }
+
public void generate(CodeWriter writer, VarDescriptor vd) {
// get (first) value for quantifer.relation ... then do comparison with expr...
// can this be maybe? i guess if quantifer.relation is empty
--- /dev/null
+package MCC.IR;
+import java.util.*;
+
+public class Conjunction {
+
+ Vector predicates;
+ public Conjunction(DNFPredicate pred) {
+ predicates=new Vector();
+ predicates.add(pred);
+ }
+ Conjunction(Vector preds){
+ predicates=preds ;
+ }
+
+ int size() {
+ return predicates.size();
+ }
+
+ DNFPredicate get(int i) {
+ return (DNFPredicate) predicates.get(i);
+ }
+
+ void add(DNFPredicate dp) {
+ predicates.add(dp);
+ }
+
+ public Conjunction append(Conjunction c) {
+ Conjunction copy=copy();
+ for(int i=0;i<c.size();i++) {
+ copy.add(new DNFPredicate(c.get(i)));
+ }
+ return copy;
+ }
+
+ public Conjunction copy() {
+ Vector vector=new Vector();
+ for (int i=0;i<size();i++) {
+ DNFPredicate dp=get(i);
+ vector.add(new DNFPredicate(dp));
+ }
+ return new Conjunction(vector);
+ }
+}
SymbolTable st = new SymbolTable();
Vector quantifiers = new Vector();
LogicStatement logicstatement = null;
-
+ DNFConstraint dnfconstraint;
int num;
public Constraint() {
public void setLogicStatement(LogicStatement ls) {
logicstatement = ls;
+ // Construct DNF form for analysis
+ dnfconstraint=logicstatement.constructDNF();
}
public LogicStatement getLogicStatement() {
--- /dev/null
+package MCC.IR;
+import java.util.*;
+
+public class DNFConstraint {
+ Vector conjunctions;
+
+ public DNFConstraint(Predicate p) {
+ conjunctions=new Vector();
+ conjunctions.add(new Conjunction(new DNFPredicate(true,p)));
+ }
+
+ public DNFConstraint(Conjunction conj) {
+ conjunctions=new Vector();
+ conjunctions.add(conj);
+ }
+
+ public DNFConstraint(Vector conj) {
+ conjunctions=conj;
+ }
+
+ DNFConstraint() {
+ conjunctions=new Vector();
+ }
+
+ int size() {
+ return conjunctions.size();
+ }
+
+ Conjunction get(int i) {
+ return (Conjunction)conjunctions.get(i);
+ }
+
+ void add(Conjunction c) {
+ conjunctions.add(c);
+ }
+
+ public DNFConstraint copy() {
+ Vector vector=new Vector();
+ for (int i=0;i<size();i++) {
+ vector.add(get(i).copy());
+ }
+ return new DNFConstraint(vector);
+ }
+
+ public DNFConstraint and(DNFConstraint c) {
+ DNFConstraint newdnf=new DNFConstraint();
+ for(int i=0;i<size();i++) {
+ for(int j=0;j<c.size();j++) {
+ newdnf.add(get(i).append(c.get(j))); //Cross product
+ }
+ }
+ return newdnf;
+ }
+
+ public DNFConstraint or(DNFConstraint c) {
+ DNFConstraint copy=copy();
+ for(int i=0;i<c.size();i++) {
+ copy.add(c.get(i).copy()); //Add in other conjunctions
+ }
+ return copy;
+ }
+
+ public DNFConstraint not() {
+ DNFConstraint copy=copy();
+ for (int i=0;i<size();i++) {
+ Conjunction conj=get(i);
+ for (int j=0;j<conj.size();j++) {
+ DNFPredicate dp=conj.get(j);
+ dp.negatePred();
+ }
+ }
+ return copy;
+ }
+}
+
+
--- /dev/null
+package MCC.IR;
+
+public class DNFExpr {
+ boolean negate;
+ Expr predicate;
+
+ public DNFExpr(DNFExpr dp) {
+ this.negate=dp.negate;
+ this.predicate=dp.predicate;
+ }
+
+ public DNFExpr(boolean negate,Expr predicate) {
+ this.negate=negate;
+ this.predicate=predicate;
+ }
+ void negatePred() {
+ negate=!negate;
+ }
+}
--- /dev/null
+package MCC.IR;
+
+public class DNFPredicate {
+ boolean negate;
+ Predicate predicate;
+
+ public DNFPredicate(DNFPredicate dp) {
+ this.negate=dp.negate;
+ this.predicate=dp.predicate;
+ }
+ Predicate getPredicate() {
+ return predicate;
+ }
+ public DNFPredicate(boolean negate,Predicate predicate) {
+ this.negate=negate;
+ this.predicate=predicate;
+ }
+ void negatePred() {
+ negate=!negate;
+ }
+}
--- /dev/null
+package MCC.IR;
+import java.util.*;
+
+public class DNFRule {
+ Vector ruleconjunctions;
+
+ public DNFRule(Expr e) {
+ ruleconjunctions=new Vector();
+ ruleconjunctions.add(new RuleConjunction(new DNFExpr(true,e)));
+ }
+
+ public DNFRule(RuleConjunction conj) {
+ ruleconjunctions=new Vector();
+ ruleconjunctions.add(conj);
+ }
+
+ public DNFRule(Vector conj) {
+ ruleconjunctions=conj;
+ }
+
+ DNFRule() {
+ ruleconjunctions=new Vector();
+ }
+
+ int size() {
+ return ruleconjunctions.size();
+ }
+
+ RuleConjunction get(int i) {
+ return (RuleConjunction)ruleconjunctions.get(i);
+ }
+
+ void add(RuleConjunction c) {
+ ruleconjunctions.add(c);
+ }
+
+ public DNFRule copy() {
+ Vector vector=new Vector();
+ for (int i=0;i<size();i++) {
+ vector.add(get(i).copy());
+ }
+ return new DNFRule(vector);
+ }
+
+ public DNFRule and(DNFRule c) {
+ DNFRule newdnf=new DNFRule();
+ for(int i=0;i<size();i++) {
+ for(int j=0;j<c.size();j++) {
+ newdnf.add(get(i).append(c.get(j))); //Cross product
+ }
+ }
+ return newdnf;
+ }
+
+ public DNFRule or(DNFRule c) {
+ DNFRule copy=copy();
+ for(int i=0;i<c.size();i++) {
+ copy.add(c.get(i).copy()); //Add in other conjunctions
+ }
+ return copy;
+ }
+
+ public DNFRule not() {
+ DNFRule copy=copy();
+ for (int i=0;i<size();i++) {
+ RuleConjunction conj=get(i);
+ for (int j=0;j<conj.size();j++) {
+ DNFExpr dp=conj.get(j);
+ dp.negatePred();
+ }
+ }
+ return copy;
+ }
+}
+
+
otherrulenode.addEdge(new GraphNode.Edge(d.getSymbol(), rulenode));
}
}
- }
+ }
}
/* build constraint->rule dependencies */
throw new IRException("unsupported");
}
+ public DNFRule constructDNF() {
+ return new DNFRule(this);
+ }
+
}
public void generate(CodeWriter writer, VarDescriptor dest) {
expr.generate(writer, dest);
}
-
+
+ public int[] getRepairs(boolean negated) {
+ return new int[] {};
+ }
}
--- /dev/null
+package MCC.IR;
+import MCC.State;
+import java.util.*;
+
+public class ImplicitSchema {
+ State state;
+ SetAnalysis setanalysis;
+ public ImplicitSchema(State state) {
+ this.state=state;
+ this.setanalysis=new SetAnalysis(state);
+ }
+
+ public void update() {
+ updaterules();
+ updateconstraints();
+ updaterelationconstraints();
+ }
+
+ void updaterelationconstraints() {
+ Vector reldescriptors=state.stRelations.getAllDescriptors();
+ for(int i=0;i<reldescriptors.size();i++) {
+ RelationDescriptor rd=(RelationDescriptor) reldescriptors.get(i);
+ Constraint c=new Constraint();
+
+ /* Construct quantifier */
+ RelationQuantifier rq=new RelationQuantifier();
+ String varname1=new String("partitionvar1");
+ String varname2=new String("partitionvar2");
+ VarDescriptor var1=new VarDescriptor(varname1);
+ VarDescriptor var2=new VarDescriptor(varname2);
+ c.getSymbolTable().add(var1);
+ c.getSymbolTable().add(var2);
+ var1.setType(rd.getDomain().getType());
+ var2.setType(rd.getRange().getType());
+ rq.setTuple(var1,var2);
+ rq.setRelation(rd);
+ c.addQuantifier(rq);
+
+ VarExpr ve1=new VarExpr(varname1);
+ SetExpr se1=new SetExpr(rd.getDomain());
+ LogicStatement incpred1=new InclusionPredicate(ve1,se1);
+
+ VarExpr ve2=new VarExpr(varname2);
+ SetExpr se2=new SetExpr(rd.getRange());
+ LogicStatement incpred2=new InclusionPredicate(ve2,se2);
+ c.setLogicStatement(new LogicStatement(LogicStatement.AND,incpred1,incpred2));
+ state.vConstraints.add(c);
+ }
+ }
+
+ void updateconstraints() {
+ Vector setdescriptors=state.stSets.getAllDescriptors();
+ for(int i=0;i<setdescriptors.size();i++) {
+ SetDescriptor sd=(SetDescriptor) setdescriptors.get(i);
+ if(sd.isPartition()) {
+ Constraint c=new Constraint();
+
+ /* Construct quantifier */
+ SetQuantifier sq=new SetQuantifier();
+ String varname=new String("partitionvar");
+ VarDescriptor var=new VarDescriptor(varname);
+ c.getSymbolTable().add(var);
+ var.setType(sd.getType());
+ sq.setVar(var);
+ sq.setSet(sd);
+ c.addQuantifier(sq);
+
+ /*Construct logic statement*/
+ LogicStatement ls=null;
+ for(int j=0;j<sd.getSubsets().size();j++) {
+ LogicStatement conj=null;
+ for(int k=0;k<sd.getSubsets().size();k++) {
+ VarExpr ve=new VarExpr(varname);
+ SetExpr se=new SetExpr((SetDescriptor) sd.getSubsets().get(k));
+ LogicStatement incpred=new InclusionPredicate(ve,se);
+ if (j!=k) {
+ incpred=new LogicStatement(LogicStatement.NOT ,incpred);
+ }
+ if (conj==null)
+ conj=incpred;
+ else
+ conj=new LogicStatement(LogicStatement.AND, conj, incpred);
+ }
+ if (ls==null)
+ ls=conj;
+ else
+ ls=new LogicStatement(LogicStatement.OR, ls, conj);
+ }
+ c.setLogicStatement(ls);
+ state.vConstraints.add(c);
+ }
+ }
+ }
+
+ void updaterules() {
+ Vector oldrules=state.vRules;
+ Vector newrules=new Vector();
+ for(int i=0;i<oldrules.size();i++) {
+ Rule r=(Rule)oldrules.get(i);
+ if (r.inclusion instanceof SetInclusion) {
+ SetDescriptor sd=((SetInclusion)r.inclusion).getSet();
+ Set supersets=setanalysis.getSuperset(sd);
+ if (supersets!=null)
+ for(Iterator superit=supersets.iterator();superit.hasNext();) {
+ SetDescriptor sd1=(SetDescriptor)superit.next();
+ Rule nr=new Rule();
+ nr.guard=r.guard;
+ nr.quantifiers=r.quantifiers;
+ nr.isstatic=r.isstatic;
+ nr.isdelay=r.isdelay;
+ nr.inclusion=new SetInclusion(((SetInclusion)r.inclusion).elementexpr,sd1);
+ nr.st=r.st;
+ newrules.add(nr);
+ }
+ }
+ }
+ oldrules.addAll(newrules);
+ }
+}
//set.addAll(expr.getInversedRelations());
//return set;
}
-
+
+ public int[] getRepairs(boolean negated) {
+ if (setexpr instanceof ImageSetExpr) {
+ if (negated)
+ return new int[] {AbstractRepair.REMOVEFROMRELATION};
+ else
+ return new int[] {AbstractRepair.ADDTORELATION};
+ } else {
+ if (negated)
+ return new int[] {AbstractRepair.REMOVEFROMSET};
+ else
+ return new int[] {AbstractRepair.ADDTOSET};
+ }
+ }
}
if (left == null) {
throw new IRException();
}
-
Set set = left.getInversedRelations();
if (right != null) {
set.addAll(right.getInversedRelations());
return set;
}
+ public DNFConstraint constructDNF() {
+ if (op==AND) {
+ DNFConstraint leftd=left.constructDNF();
+ DNFConstraint rightd=right.constructDNF();
+ return leftd.and(rightd);
+ } else if (op==OR) {
+ DNFConstraint leftd=left.constructDNF();
+ DNFConstraint rightd=right.constructDNF();
+ return leftd.or(rightd);
+ } else if (op==NOT) {
+ DNFConstraint leftd=left.constructDNF();
+ return leftd.not();
+ } else throw new Error();
+ }
+
public static class Operation {
private final String name;
private Operation(String opname) { name = opname; }
assert (right == null && opcode == Opcode.NOT) || (right != null);
}
+ public DNFRule constructDNF() {
+ if (opcode==Opcode.AND) {
+ DNFRule leftd=left.constructDNF();
+ DNFRule rightd=right.constructDNF();
+ return leftd.and(rightd);
+ } else if (opcode==Opcode.OR) {
+ DNFRule leftd=left.constructDNF();
+ DNFRule rightd=right.constructDNF();
+ return leftd.or(rightd);
+ } else if (opcode==Opcode.NOT) {
+ DNFRule leftd=left.constructDNF();
+ return leftd.not();
+ } else throw new Error();
+ }
+
+
+
public Set getInversedRelations() {
Set set = left.getInversedRelations();
if (right != null) {
public class Optimizer {
State state;
-
public Optimizer(State s) {
state = s;
}
public abstract class Predicate extends LogicStatement {
protected Predicate() {}
+ public DNFConstraint constructDNF() {
+ return new DNFConstraint(this);
+ }
+ public int[] getRepairs(boolean negated) {}
}
--- /dev/null
+package MCC.IR;
+import java.util.*;
+
+public class RuleConjunction {
+
+ Vector predicates;
+ public RuleConjunction(DNFExpr pred) {
+ predicates=new Vector();
+ predicates.add(pred);
+ }
+ RuleConjunction(Vector preds){
+ predicates=preds ;
+ }
+
+ int size() {
+ return predicates.size();
+ }
+
+ DNFExpr get(int i) {
+ return (DNFExpr) predicates.get(i);
+ }
+
+ void add(DNFExpr dp) {
+ predicates.add(dp);
+ }
+
+ public RuleConjunction append(RuleConjunction c) {
+ RuleConjunction copy=copy();
+ for(int i=0;i<c.size();i++) {
+ copy.add(new DNFExpr(c.get(i)));
+ }
+ return copy;
+ }
+
+ public RuleConjunction copy() {
+ Vector vector=new Vector();
+ for (int i=0;i<=size();i++) {
+ DNFExpr dp=get(i);
+ vector.add(new DNFExpr(dp));
+ }
+ return new RuleConjunction(vector);
+ }
+}
}
/* do any post checks... (type constraints, etc?) */
-
- return ok;
+
+ return ok;
}
private boolean parse_constraint(ParseNode pn) {
} else {
throw new IRException("not supported yet");
}
-
}
private LogicStatement parse_body(ParseNode pn) {
--- /dev/null
+package MCC.IR;
+import java.util.*;
+import MCC.State;
+
+public class SetAnalysis {
+ State state;
+ Hashtable intersection;
+ Hashtable subset;
+ Hashtable superset;
+
+ public SetAnalysis(State state) {
+ this.state=state;
+ intersection=new Hashtable();
+ subset=new Hashtable();
+ superset=new Hashtable();
+ doanalysis();
+ }
+
+ public Set getSuperset(SetDescriptor set1) {
+ return (Set)superset.get(set1);
+ }
+
+ public boolean isSubset(SetDescriptor set1, SetDescriptor set2) {
+ return subset.contains(set1)&&((Set)subset.get(set1)).contains(set2);
+ }
+
+ public boolean noIntersection(SetDescriptor set1, SetDescriptor set2) {
+ return intersection.contains(set1)&&((Set)intersection.get(set1)).contains(set2);
+ }
+
+ void doanalysis() {
+ SymbolTable sets=state.stSets;
+ Vector descriptors=sets.getAllDescriptors();
+ for(int i=0;i<descriptors.size();i++) {
+ SetDescriptor sd=(SetDescriptor)descriptors.get(i);
+ Stack st=new Stack();
+ st.addAll(sd.getSubsets());
+ while(!st.empty()) {
+ SetDescriptor subsetsd=(SetDescriptor)st.pop();
+ System.out.print(subsetsd.toString());
+
+ st.addAll(subsetsd.getSubsets());
+ if (!subset.contains(sd))
+ subset.put(sd,new HashSet());
+ ((HashSet)subset.get(sd)).addAll(subsetsd.getSubsets());
+ for(Iterator it=subsetsd.getSubsets().iterator();it.hasNext();) {
+ SetDescriptor sd2=(SetDescriptor)it.next();
+ if (!superset.contains(sd2))
+ superset.put(sd2,new HashSet());
+ ((HashSet)superset.get(sd2)).add(sd);
+ }
+ }
+ }
+ for(int i=0;i<descriptors.size();i++) {
+ SetDescriptor sd=(SetDescriptor)descriptors.get(i);
+ if (sd.isPartition()) {
+ Vector subst=sd.getSubsets();
+ for(Iterator it1=subst.iterator();it1.hasNext();) {
+ SetDescriptor sd1=(SetDescriptor)it1.next();
+ for(Iterator it2=subst.iterator();it2.hasNext();) {
+ SetDescriptor sd2=(SetDescriptor)it2.next();
+ if (sd1!=sd2) {
+ for(Iterator it3=sd1.allSubsets().iterator();it3.hasNext();) {
+ SetDescriptor sd3=(SetDescriptor)it3.next();
+
+ if (!intersection.contains(sd3))
+ intersection.put(sd3,new HashSet());
+ ((HashSet)intersection.get(sd3)).addAll(sd2.allSubsets());
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+}
this.cardinality = cardinality;
}
+ public int[] getRepairs(boolean negated) {
+ if (setexpr instanceof ImageSetExpr) {
+ if (opcode==Opcode.EQ)
+ return new int[] {AbstractRepair.ADDTORELATION,
+ AbstractRepair.REMOVEFROMRELATION};
+ if (((opcode==Opcode.GE)&&!negated)||
+ ((opcode==Opcode.LE)&&negated))
+ return new int[]{AbstractRepair.ADDTORELATION};
+ else
+ return new int[]{AbstractRepair.REMOVEFROMRELATION};
+ } else {
+ if (opcode==Opcode.EQ)
+ return new int[] {AbstractRepair.ADDTOSET,
+ AbstractRepair.REMOVEFROMSET};
+
+ if (((opcode==Opcode.GE)&&!negated)||
+ ((opcode==Opcode.LE)&&negated))
+ return new int[] {AbstractRepair.ADDTOSET};
+ else
+ return new int[] {AbstractRepair.REMOVEFROMSET};
+ }
+ }
+
public Set getRequiredDescriptors() {
assert setexpr != null;
Set v = setexpr.getRequiredDescriptors();
--- /dev/null
+package MCC.IR;
+import java.util.*;
+
+class Termination {
+ HashSet conjunctions;
+ Hashtable conjunctionmap;
+
+ HashSet abstractrepair;
+
+ State state;
+
+ public Termination(State state) {
+ this.state=state;
+ generateconjunctionnodes();
+ generaterepairnodes();
+ }
+
+ void generateconjunctionnodes() {
+ Vector constraints=state.vConstraints;
+ for(int i=0;i<constraints.size();i++) {
+ Constraint c=(Constraint)constraints.get(i);
+ DNFConstraint dnf=c.dnfconstraint;
+ for(int j=0;j<dnf.size();j++) {
+ TermNode tn=new TermNode(c,dnf.get(j));
+ GraphNode gn=new GraphNode("Conjunction"+i+","+j,tn);
+ conjunctions.add(gn);
+ conjunctionmap.put(c,gn);
+ }
+ }
+ }
+
+ void generaterepairnodes() {
+ for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
+ GraphNode gn=(GraphNode)conjiterator.next();
+ TermNode tn=(TermNode)gn.getOwner();
+ Conjunction conj=tn.getConjunction();
+ for(int i=0;i<conj.size();i++) {
+ DNFPredicate dp=conj.get(i);
+ int[] array=dp.getPredicate().getRepairs();
+ for {int j=0;j<array.length;j++) {
+ AbstractRepair ar=new AbstractRepair(dp,array[j]);
+ TermNode tn=new TermNode(ar);
+ GraphNode gn2=new GraphNode(gn.getLabel()+"-"+i+","+j,tn);
+ Edge e=new Edge("abstract",gn2);
+ gn.addEdge(e);
+ abstractrepair.add(gn2);
+ }
+ }
+ }
+ }
+}
+
+class AbstractRepair {
+ public final static int ADDTOSET=1;
+ public final static int REMOVEFROMSET=2;
+ public final static int ADDTORELATION=3;
+ public final static int REMOVEFROMRELATION=4;
+ public final static int MODIFYRELATION=5;
+
+ DNFPredicate torepair;
+ int type;
+
+ public AbstractRepair(DNFPredicate dp,int typ) {
+ torepair=dp;
+ type=typ;
+ }
+}
+
+class TermNode {
+ public final static int CONJUNCTION=1;
+ public final static int ABSTRACT=2;
+
+ Constraint constr;
+ Conjunction conj;
+ int type;
+ AbstractRepair repair;
+
+ public TermNode(Constraint constr, Conjunction conj) {
+ this.constr=constr;
+ this.conj=conj;
+ type=CONJUNCTION;
+ }
+
+ public TermNode(AbstractRepair ar) {
+ repair=ar;
+ type=ABSTRACT;
+ }
+
+ public Conjunction getConjunction() {
+ return conj;
+ }
+}
+
projects / repair.git / commitdiff