More graph building

diff --git a/src/AST/boolean.h b/src/AST/boolean.h
index 8be1d30626c93f6c3612ab0447157bb3f4825dc1..9d7e9ab16df375e9fc5a2cc4d2708abf75bba99e 100644 (file)
--- a/src/AST/boolean.h
+++ b/src/AST/boolean.h
@@ -61,15 +61,15 @@ class BooleanPredicate : public Boolean {
 public:
        BooleanPredicate(Predicate *_predicate, Element **_inputs, uint _numInputs, BooleanEdge _undefinedStatus);
        Boolean *clone(CSolver *solver, CloneMap *map);
-
+       Predicate *getPredicate() {return predicate;}
+       FunctionEncoding *getFunctionEncoding() {return &encoding;}
+       void updateParents();
+       CMEMALLOC;
+       
        Predicate *predicate;
        FunctionEncoding encoding;
        Array<Element *> inputs;
        BooleanEdge undefStatus;
-       FunctionEncoding *getFunctionEncoding() {return &encoding;}
-       void updateParents();
-
-       CMEMALLOC;
 };
 
 class BooleanLogic : public Boolean {

diff --git a/src/AST/predicate.cc b/src/AST/predicate.cc
index d359811663dedab5d83ecb35c7fb84db889548d7..f37d4cdc72d1dde709325c76b57cec300d4d4356 100644 (file)
--- a/src/AST/predicate.cc
+++ b/src/AST/predicate.cc
@@ -4,7 +4,7 @@
 #include "table.h"
 #include "csolver.h"
 
-PredicateOperator::PredicateOperator(CompOp _op, Set **domain, uint numDomain) : Predicate(OPERATORPRED), op(_op), domains(domain, numDomain) {
+PredicateOperator::PredicateOperator(CompOp _op, Set **domain, uint numDomain) : Predicate(OPERATORPRED), domains(domain, numDomain), op(_op) {
 }
 
 PredicateTable::PredicateTable(Table *_table, UndefinedBehavior _undefBehavior) : Predicate(TABLEPRED), table(_table), undefinedbehavior(_undefBehavior) {

diff --git a/src/AST/predicate.h b/src/AST/predicate.h
index 183a96099c9d69157f8a63dc7d4c6bd323a91f36..80515fa9e06a75968ae1e53507bcd7c1577f2db4 100644 (file)
--- a/src/AST/predicate.h
+++ b/src/AST/predicate.h
@@ -21,9 +21,11 @@ public:
        PredicateOperator(CompOp op, Set **domain, uint numDomain);
        bool evalPredicateOperator(uint64_t *inputs);
        Predicate *clone(CSolver *solver, CloneMap *map);
-       CompOp op;
+       CompOp getOp() {return op;}
        Array<Set *> domains;
        CMEMALLOC;
+ private:
+       CompOp op;
 };
 
 class PredicateTable : public Predicate {

diff --git a/src/ASTAnalyses/Encoding/encodinggraph.cc b/src/ASTAnalyses/Encoding/encodinggraph.cc
index a329e6b316aed6d3071d05d03f23680a8a3d000f..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) {
@@ -58,6 +60,33 @@ void EncodingGraph::processFunction(ElementFunction *ef) {
        }
 }
 
+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);
+               }
+       }
+}
+
 EncodingEdge * EncodingGraph::getEdge(EncodingNode *left, EncodingNode *right, EncodingNode *dst) {
        EncodingEdge e(left, right, dst);
        EncodingEdge *result = edgeMap.get(&e);
@@ -68,14 +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;

diff --git a/src/ASTAnalyses/Encoding/encodinggraph.h b/src/ASTAnalyses/Encoding/encodinggraph.h
index 12994da28fd657a91a5a58d1d17fd951507e6cf4..7f7b8b41b6d43f9083c5727a8d57f4793577f118 100644 (file)
--- a/src/ASTAnalyses/Encoding/encodinggraph.h
+++ b/src/ASTAnalyses/Encoding/encodinggraph.h
@@ -30,6 +30,7 @@ class EncodingNode {
  public:
        EncodingNode(Set *_s);
        void addElement(Element *e);
+       uint getSize();
        CMEMALLOC;
  private:
        Set *s;
@@ -52,6 +53,6 @@ class EncodingEdge {
        uint numComparisons;
        friend uint hashEncodingEdge(EncodingEdge *edge);
        friend bool equalsEncodingEdge(EncodingEdge *e1, EncodingEdge *e2);
-       fiend class EncodingGraph;
+       friend class EncodingGraph;
 };
 #endif

diff --git a/src/Backend/satfuncopencoder.cc b/src/Backend/satfuncopencoder.cc
index 7e6a67d239def78348bb3d4443b1a683735e4354..9fc3c4124f4f1187836fc93b9ebaf59c458ab055 100644 (file)
--- a/src/Backend/satfuncopencoder.cc
+++ b/src/Backend/satfuncopencoder.cc
@@ -204,7 +204,7 @@ Edge SATEncoder::encodeCircuitOperatorPredicateEncoder(BooleanPredicate *constra
        ElementEncoding *ee1 = getElementEncoding(elem1);
        ASSERT(ee0->numVars == ee1->numVars);
        uint numVars = ee0->numVars;
-       switch (predicate->op) {
+       switch (predicate->getOp()) {
        case SATC_EQUALS:
                return generateEquivNVConstraint(cnf, numVars, ee0->variables, ee1->variables);
        case SATC_LT: