projects
/
satune.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
7f34f47
)
Give vector more specific type
author
bdemsky
<bdemsky@uci.edu>
Wed, 16 Aug 2017 07:22:07 +0000
(
00:22
-0700)
committer
bdemsky
<bdemsky@uci.edu>
Wed, 16 Aug 2017 07:22:07 +0000
(
00:22
-0700)
src/AST/boolean.c
patch
|
blob
|
history
src/AST/order.c
patch
|
blob
|
history
src/AST/order.h
patch
|
blob
|
history
src/Collections/structs.c
patch
|
blob
|
history
src/Collections/structs.h
patch
|
blob
|
history
src/Encoders/orderencoder.c
patch
|
blob
|
history
src/Encoders/orderencoder.h
patch
|
blob
|
history
src/Encoders/ordergraph.c
patch
|
blob
|
history
src/Encoders/ordergraph.h
patch
|
blob
|
history
src/Encoders/ordernode.c
patch
|
blob
|
history
src/Encoders/ordernode.h
patch
|
blob
|
history
diff --git
a/src/AST/boolean.c
b/src/AST/boolean.c
index 591bfe61ac0a8de6a56c6ef2b6943914f3675349..3ce75e4ad432bc071ebca41adde714877c99656c 100644
(file)
--- a/
src/AST/boolean.c
+++ b/
src/AST/boolean.c
@@
-23,7
+23,7
@@
Boolean* allocBooleanOrder(Order* order, uint64_t first, uint64_t second) {
This->order=order;
This->first=first;
This->second=second;
This->order=order;
This->first=first;
This->second=second;
- pushVectorBoolean
(&order->constraints, &This->base
);
+ pushVectorBoolean
Order(&order->constraints, This
);
initDefVectorBoolean(GETBOOLEANPARENTS(This));
return & This -> base;
}
initDefVectorBoolean(GETBOOLEANPARENTS(This));
return & This -> base;
}
diff --git
a/src/AST/order.c
b/src/AST/order.c
index 92c52ae64069a575a64d538284333fa924fd4c9c..054de91ce833b9247a9b6fab80f74fcd2469dbaf 100644
(file)
--- a/
src/AST/order.c
+++ b/
src/AST/order.c
@@
-6,7
+6,7
@@
Order* allocOrder(OrderType type, Set * set){
Order* This = (Order*)ourmalloc(sizeof(Order));
This->set=set;
Order* allocOrder(OrderType type, Set * set){
Order* This = (Order*)ourmalloc(sizeof(Order));
This->set=set;
- initDefVectorBoolean(& This->constraints);
+ initDefVectorBoolean
Order
(& This->constraints);
This->type=type;
initOrderEncoding(& This->order, This);
This->orderPairTable = NULL;
This->type=type;
initOrderEncoding(& This->order, This);
This->orderPairTable = NULL;
@@
-18,7
+18,7
@@
void initializeOrderHashTable(Order* This){
}
void addOrderConstraint(Order* This, BooleanOrder* constraint){
}
void addOrderConstraint(Order* This, BooleanOrder* constraint){
- pushVectorBoolean
( &This->constraints, (Boolean*)
constraint);
+ pushVectorBoolean
Order( &This->constraints,
constraint);
}
void setOrderEncodingType(Order* This, OrderEncodingType type){
}
void setOrderEncodingType(Order* This, OrderEncodingType type){
@@
-26,7
+26,7
@@
void setOrderEncodingType(Order* This, OrderEncodingType type){
}
void deleteOrder(Order* This){
}
void deleteOrder(Order* This){
- deleteVectorArrayBoolean(& This->constraints);
+ deleteVectorArrayBoolean
Order
(& This->constraints);
deleteOrderEncoding(& This->order);
if(This->orderPairTable != NULL) {
resetAndDeleteHashTableOrderPair(This->orderPairTable);
deleteOrderEncoding(& This->order);
if(This->orderPairTable != NULL) {
resetAndDeleteHashTableOrderPair(This->orderPairTable);
diff --git
a/src/AST/order.h
b/src/AST/order.h
index bb35603069b3bb857da0a46223cb24d7e890baa0..7a173b90f2bf73c26b106792683ac6641be0b8e9 100644
(file)
--- a/
src/AST/order.h
+++ b/
src/AST/order.h
@@
-11,7
+11,7
@@
struct Order {
OrderType type;
Set * set;
HashTableOrderPair * orderPairTable;
OrderType type;
Set * set;
HashTableOrderPair * orderPairTable;
- VectorBoolean constraints;
+ VectorBoolean
Order
constraints;
OrderEncoding order;
};
OrderEncoding order;
};
diff --git
a/src/Collections/structs.c
b/src/Collections/structs.c
index 9c44ea7a66ffc43f7dbd2352e9a4be2d8ee13be5..459edd1498d6fe2416b957e5c894686893a0dc33 100644
(file)
--- a/
src/Collections/structs.c
+++ b/
src/Collections/structs.c
@@
-9,6
+9,7
@@
VectorImpl(Table, Table *, 4);
VectorImpl(Set, Set *, 4);
VectorImpl(Boolean, Boolean *, 4);
VectorImpl(Table, Table *, 4);
VectorImpl(Set, Set *, 4);
VectorImpl(Boolean, Boolean *, 4);
+VectorImpl(BooleanOrder, BooleanOrder *, 4);
VectorImpl(Function, Function *, 4);
VectorImpl(Predicate, Predicate *, 4);
VectorImpl(Element, Element *, 4);
VectorImpl(Function, Function *, 4);
VectorImpl(Predicate, Predicate *, 4);
VectorImpl(Element, Element *, 4);
diff --git
a/src/Collections/structs.h
b/src/Collections/structs.h
index 4343d34302178b2e45bd183f456f6f40d1984393..5713e89178749aeabfb5232ce54a0dcd093a520e 100644
(file)
--- a/
src/Collections/structs.h
+++ b/
src/Collections/structs.h
@@
-13,6
+13,7
@@
ArrayDef(Set, Set *);
VectorDef(Table, Table *);
VectorDef(Set, Set *);
VectorDef(Boolean, Boolean *);
VectorDef(Table, Table *);
VectorDef(Set, Set *);
VectorDef(Boolean, Boolean *);
+VectorDef(BooleanOrder, BooleanOrder *);
VectorDef(Function, Function *);
VectorDef(Predicate, Predicate *);
VectorDef(Element, Element *);
VectorDef(Function, Function *);
VectorDef(Predicate, Predicate *);
VectorDef(Element, Element *);
diff --git
a/src/Encoders/orderencoder.c
b/src/Encoders/orderencoder.c
index b87a982da0820f203b91c3ed6ff585a7872a29af..d15592132c65b3d3d59528b92a3a80f7c9bd003e 100644
(file)
--- a/
src/Encoders/orderencoder.c
+++ b/
src/Encoders/orderencoder.c
@@
-9,9
+9,9
@@
OrderGraph* buildOrderGraph(Order *order) {
OrderGraph* orderGraph = allocOrderGraph(order);
OrderGraph* buildOrderGraph(Order *order) {
OrderGraph* orderGraph = allocOrderGraph(order);
- uint constrSize = getSizeVectorBoolean(&order->constraints);
+ uint constrSize = getSizeVectorBoolean
Order
(&order->constraints);
for(uint j=0; j<constrSize; j++){
for(uint j=0; j<constrSize; j++){
- addOrderConstraintToOrderGraph(orderGraph, getVectorBoolean(&order->constraints, j));
+ addOrderConstraintToOrderGraph(orderGraph, getVectorBoolean
Order
(&order->constraints, j));
}
return orderGraph;
}
}
return orderGraph;
}
@@
-22,7
+22,7
@@
void DFS(OrderGraph* graph, VectorOrderNode* finishNodes) {
OrderNode* node = nextOrderNode(iterator);
if(node->status == NOTVISITED){
node->status = VISITED;
OrderNode* node = nextOrderNode(iterator);
if(node->status == NOTVISITED){
node->status = VISITED;
- DFSNodeVisit(node, finishNodes, false);
+ DFSNodeVisit(node, finishNodes, false
, 0
);
node->status = FINISHED;
pushVectorOrderNode(finishNodes, node);
}
node->status = FINISHED;
pushVectorOrderNode(finishNodes, node);
}
@@
-32,18
+32,20
@@
void DFS(OrderGraph* graph, VectorOrderNode* finishNodes) {
void DFSReverse(OrderGraph* graph, VectorOrderNode* finishNodes) {
uint size = getSizeVectorOrderNode(finishNodes);
void DFSReverse(OrderGraph* graph, VectorOrderNode* finishNodes) {
uint size = getSizeVectorOrderNode(finishNodes);
+ uint sccNum=1;
for(int i=size-1; i>=0; i--){
OrderNode* node = getVectorOrderNode(finishNodes, i);
if(node->status == NOTVISITED){
node->status = VISITED;
for(int i=size-1; i>=0; i--){
OrderNode* node = getVectorOrderNode(finishNodes, i);
if(node->status == NOTVISITED){
node->status = VISITED;
- DFSNodeVisit(node, NULL, true);
+ DFSNodeVisit(node, NULL, true, sccNum);
+ node->sccNum = sccNum;
node->status = FINISHED;
node->status = FINISHED;
- pushVectorOrderNode(&graph->scc, node);
+ sccNum++;
}
}
}
}
}
}
-void DFSNodeVisit(OrderNode* node, VectorOrderNode* finishNodes, bool isReverse) {
+void DFSNodeVisit(OrderNode* node, VectorOrderNode* finishNodes, bool isReverse
, uint sccNum
) {
HSIteratorOrderEdge* iterator = isReverse?iteratorOrderEdge(node->inEdges):iteratorOrderEdge(node->outEdges);
while(hasNextOrderEdge(iterator)){
OrderEdge* edge = nextOrderEdge(iterator);
HSIteratorOrderEdge* iterator = isReverse?iteratorOrderEdge(node->inEdges):iteratorOrderEdge(node->outEdges);
while(hasNextOrderEdge(iterator)){
OrderEdge* edge = nextOrderEdge(iterator);
@@
-52,12
+54,14
@@
void DFSNodeVisit(OrderNode* node, VectorOrderNode* finishNodes, bool isReverse)
OrderNode* child = isReverse? edge->source: edge->sink;
OrderNode* child = isReverse? edge->source: edge->sink;
- if(child->status == NOTVISITED){
+ if(child->status == NOTVISITED)
{
child->status = VISITED;
child->status = VISITED;
- DFSNodeVisit(child, finishNodes, isReverse);
+ DFSNodeVisit(child, finishNodes, isReverse
, sccNum
);
child->status = FINISHED;
if(!isReverse)
pushVectorOrderNode(finishNodes, child);
child->status = FINISHED;
if(!isReverse)
pushVectorOrderNode(finishNodes, child);
+ else
+ child->sccNum = sccNum;
}
}
deleteIterOrderEdge(iterator);
}
}
deleteIterOrderEdge(iterator);
@@
-246,6
+250,12
@@
void localMustAnalysisPartial(OrderGraph *graph) {
deleteIterOrderEdge(iterator);
}
deleteIterOrderEdge(iterator);
}
+void decomposeOrder(Order *order, OrderGraph *graph) {
+ uint size=getSizeVectorBooleanOrder(&order->constraints);
+ for(uint i=0;i<size;i++) {
+ }
+}
+
void orderAnalysis(CSolver* This) {
uint size = getSizeVectorOrder(This->allOrders);
for(uint i=0; i<size; i++){
void orderAnalysis(CSolver* This) {
uint size = getSizeVectorOrder(This->allOrders);
for(uint i=0; i<size; i++){
@@
-268,10
+278,14
@@
void orderAnalysis(CSolver* This) {
localMustAnalysisTotal(graph);
}
localMustAnalysisTotal(graph);
}
- //This
analysis
is completely optional
+ //This
optimization
is completely optional
removeMustBeTrueNodes(graph);
removeMustBeTrueNodes(graph);
+ //This is needed for splitorder
computeStronglyConnectedComponentGraph(graph);
computeStronglyConnectedComponentGraph(graph);
+
+ decomposeOrder(order, graph);
+
deleteOrderGraph(graph);
}
}
deleteOrderGraph(graph);
}
}
diff --git
a/src/Encoders/orderencoder.h
b/src/Encoders/orderencoder.h
index ca3e415c0c687660beaf5c86e536d97e8c8f555f..e25ee42994973bb46b6ec8f9f1e38b974ec62185 100644
(file)
--- a/
src/Encoders/orderencoder.h
+++ b/
src/Encoders/orderencoder.h
@@
-15,7
+15,7
@@
OrderGraph* buildOrderGraph(Order *order);
void computeStronglyConnectedComponentGraph(OrderGraph* graph);
void orderAnalysis(CSolver* solver);
void initializeNodeInfoSCC(OrderGraph* graph);
void computeStronglyConnectedComponentGraph(OrderGraph* graph);
void orderAnalysis(CSolver* solver);
void initializeNodeInfoSCC(OrderGraph* graph);
-void DFSNodeVisit(OrderNode* node, VectorOrderNode* finishNodes, bool isReverse);
+void DFSNodeVisit(OrderNode* node, VectorOrderNode* finishNodes, bool isReverse
, uint sccNum
);
void DFS(OrderGraph* graph, VectorOrderNode* finishNodes);
void DFSReverse(OrderGraph* graph, VectorOrderNode* finishNodes);
void completePartialOrderGraph(OrderGraph* graph);
void DFS(OrderGraph* graph, VectorOrderNode* finishNodes);
void DFSReverse(OrderGraph* graph, VectorOrderNode* finishNodes);
void completePartialOrderGraph(OrderGraph* graph);
@@
-30,6
+30,7
@@
void reachMustAnalysis(OrderGraph *graph);
void localMustAnalysisTotal(OrderGraph *graph);
void localMustAnalysisPartial(OrderGraph *graph);
void orderAnalysis(CSolver* This);
void localMustAnalysisTotal(OrderGraph *graph);
void localMustAnalysisPartial(OrderGraph *graph);
void orderAnalysis(CSolver* This);
+void decomposeOrder(Order *order, OrderGraph *graph);
#endif /* ORDERGRAPHBUILDER_H */
#endif /* ORDERGRAPHBUILDER_H */
diff --git
a/src/Encoders/ordergraph.c
b/src/Encoders/ordergraph.c
index 2510fab7a15c29744ff2d0f6ada155159387b77e..e6cb64e1ba3016dc3a4bd7ffd4ec5ca3a258fd39 100644
(file)
--- a/
src/Encoders/ordergraph.c
+++ b/
src/Encoders/ordergraph.c
@@
-9,13
+9,12
@@
OrderGraph* allocOrderGraph(Order *order) {
OrderGraph* This = (OrderGraph*) ourmalloc(sizeof(OrderGraph));
This->nodes = allocHashSetOrderNode(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
This->order = order;
OrderGraph* This = (OrderGraph*) ourmalloc(sizeof(OrderGraph));
This->nodes = allocHashSetOrderNode(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
This->order = order;
- initDefVectorOrderNode(&This->scc);
return This;
}
return This;
}
-void addOrderEdge(OrderGraph* graph, OrderNode* node1, OrderNode* node2, Boolean* constr) {
- Polarity polarity=constr->polarity;
- BooleanValue mustval=constr->boolVal;
+void addOrderEdge(OrderGraph* graph, OrderNode* node1, OrderNode* node2, Boolean
Order
* constr) {
+ Polarity polarity=constr->
base.
polarity;
+ BooleanValue mustval=constr->b
ase.b
oolVal;
Order* order=graph->order;
switch(polarity) {
case P_BOTHTRUEFALSE:
Order* order=graph->order;
switch(polarity) {
case P_BOTHTRUEFALSE:
@@
-26,7
+25,7
@@
void addOrderEdge(OrderGraph* graph, OrderNode* node1, OrderNode* node2, Boolean
_1to2->polPos = true;
addNewOutgoingEdge(node1, _1to2);
addNewIncomingEdge(node2, _1to2);
_1to2->polPos = true;
addNewOutgoingEdge(node1, _1to2);
addNewIncomingEdge(node2, _1to2);
- if(constr->polarity == P_TRUE)
+ if(constr->
base.
polarity == P_TRUE)
break;
}
case P_FALSE:{
break;
}
case P_FALSE:{
@@
-83,11
+82,10
@@
OrderEdge* getInverseOrderEdge(OrderGraph* graph, OrderEdge *edge) {
return tmp;
}
return tmp;
}
-void addOrderConstraintToOrderGraph(OrderGraph* graph, Boolean* constr) {
- BooleanOrder* bOrder = (BooleanOrder*) constr;
+void addOrderConstraintToOrderGraph(OrderGraph* graph, BooleanOrder* bOrder) {
OrderNode* from = getOrderNodeFromOrderGraph(graph, bOrder->first);
OrderNode* to = getOrderNodeFromOrderGraph(graph, bOrder->second);
OrderNode* from = getOrderNodeFromOrderGraph(graph, bOrder->first);
OrderNode* to = getOrderNodeFromOrderGraph(graph, bOrder->second);
- addOrderEdge(graph, from, to,
const
r);
+ addOrderEdge(graph, from, to,
bOrde
r);
}
void deleteOrderGraph(OrderGraph* graph){
}
void deleteOrderGraph(OrderGraph* graph){
diff --git
a/src/Encoders/ordergraph.h
b/src/Encoders/ordergraph.h
index 1848d2e7c197c6fc941b31c56d745b75ec6cbdf8..a30c9f94d302981874987d95a061e572202173ca 100644
(file)
--- a/
src/Encoders/ordergraph.h
+++ b/
src/Encoders/ordergraph.h
@@
-15,14
+15,13
@@
struct OrderGraph {
HashSetOrderNode* nodes;
HashSetOrderEdge* edges;
Order* order;
HashSetOrderNode* nodes;
HashSetOrderEdge* edges;
Order* order;
- VectorOrderNode scc;
};
OrderGraph* allocOrderGraph(Order *order);
};
OrderGraph* allocOrderGraph(Order *order);
-void addOrderConstraintToOrderGraph(OrderGraph* graph, Boolean
* const
r);
+void addOrderConstraintToOrderGraph(OrderGraph* graph, Boolean
Order* bOrde
r);
OrderNode* getOrderNodeFromOrderGraph(OrderGraph* graph, uint64_t id);
OrderEdge* getOrderEdgeFromOrderGraph(OrderGraph* graph, OrderNode* begin, OrderNode* end);
OrderNode* getOrderNodeFromOrderGraph(OrderGraph* graph, uint64_t id);
OrderEdge* getOrderEdgeFromOrderGraph(OrderGraph* graph, OrderNode* begin, OrderNode* end);
-void addOrderEdge(OrderGraph* graph, OrderNode* node1, OrderNode* node2, Boolean* constr);
+void addOrderEdge(OrderGraph* graph, OrderNode* node1, OrderNode* node2, Boolean
Order
* constr);
void deleteOrderGraph(OrderGraph* graph);
OrderEdge* getInverseOrderEdge(OrderGraph* graph, OrderEdge *edge);
#endif /* ORDERGRAPH_H */
void deleteOrderGraph(OrderGraph* graph);
OrderEdge* getInverseOrderEdge(OrderGraph* graph, OrderEdge *edge);
#endif /* ORDERGRAPH_H */
diff --git
a/src/Encoders/ordernode.c
b/src/Encoders/ordernode.c
index 9f86b2be00ba36a5f15f448cb7c6d8d7bf1ce6d3..072e54c150a6b56fd284b7d64758807a2a5a4ff4 100644
(file)
--- a/
src/Encoders/ordernode.c
+++ b/
src/Encoders/ordernode.c
@@
-7,6
+7,7
@@
OrderNode* allocOrderNode(uint64_t id) {
This->inEdges = allocHashSetOrderEdge(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
This->outEdges = allocHashSetOrderEdge(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
This->status=NOTVISITED;
This->inEdges = allocHashSetOrderEdge(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
This->outEdges = allocHashSetOrderEdge(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
This->status=NOTVISITED;
+ This->sccNum=0;
return This;
}
return This;
}
diff --git
a/src/Encoders/ordernode.h
b/src/Encoders/ordernode.h
index 2e2ce9d4df3419acab89f8375d06ed62dc2db1c4..359b5bfee8f934f30eb6caf52866cfa8a9231fd0 100644
(file)
--- a/
src/Encoders/ordernode.h
+++ b/
src/Encoders/ordernode.h
@@
-22,6
+22,7
@@
struct OrderNode {
HashSetOrderEdge* inEdges;
HashSetOrderEdge* outEdges;
NodeStatus status;
HashSetOrderEdge* inEdges;
HashSetOrderEdge* outEdges;
NodeStatus status;
+ uint sccNum;
};
OrderNode* allocOrderNode(uint64_t id);
};
OrderNode* allocOrderNode(uint64_t id);