More graph building

[satune.git] / src / ASTAnalyses / Encoding / encodinggraph.cc

diff --git a/src/ASTAnalyses/Encoding/encodinggraph.cc b/src/ASTAnalyses/Encoding/encodinggraph.cc
index 070f639e447e4a6966dea797396dd706d00683a9..87799756ab0544e87063f76b93b502caa58eb59c 100644 (file)
--- a/src/ASTAnalyses/Encoding/encodinggraph.cc
+++ b/src/ASTAnalyses/Encoding/encodinggraph.cc
@@ -2,6 +2,8 @@
 #include "iterator.h"
 #include "element.h"
 #include "function.h"
+#include "predicate.h"
+#include "set.h"
 
 EncodingGraph::EncodingGraph(CSolver * _solver) :
        solver(_solver) {
@@ -54,6 +56,34 @@ void EncodingGraph::processFunction(ElementFunction *ef) {
                        return;
                EncodingNode *dst=createNode(ef);
                EncodingEdge *edge=getEdge(left, right, dst);
+               edge->numArithOps++;
+       }
+}
+
+void EncodingGraph::processPredicate(BooleanPredicate *b) {
+       Predicate *p=b->getPredicate();
+       if (p->type==OPERATORPRED) {
+               PredicateOperator *po=(PredicateOperator *)p;
+               ASSERT(b->inputs.getSize()==2);
+               EncodingNode *left=createNode(b->inputs.get(0));
+               EncodingNode *right=createNode(b->inputs.get(1));
+               if (left == NULL || right == NULL)
+                       return;
+               EncodingEdge *edge=getEdge(left, right, NULL);
+               CompOp op=po->getOp();
+               switch(op) {
+               case SATC_EQUALS:
+                       edge->numEquals++;
+                       break;
+               case SATC_LT:
+               case SATC_LTE:
+               case SATC_GT:
+               case SATC_GTE:
+                       edge->numComparisons++;
+                       break;
+               default:
+                       ASSERT(0);
+               }
        }
 }
 
@@ -67,15 +97,15 @@ EncodingEdge * EncodingGraph::getEdge(EncodingNode *left, EncodingNode *right, E
        return result;
 }
 
-void EncodingGraph::processPredicate(BooleanPredicate *b) {
-
-}
-
 EncodingNode::EncodingNode(Set *_s) :
        s(_s),
        numElements(0) {
 }
 
+uint EncodingNode::getSize() {
+       return s->getSize();
+}
+
 EncodingNode * EncodingGraph::createNode(Element *e) {
        if (e->type == ELEMCONST)
                return NULL;