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 {
#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) {
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 {
#include "iterator.h"
#include "element.h"
#include "function.h"
+#include "predicate.h"
+#include "set.h"
EncodingGraph::EncodingGraph(CSolver * _solver) :
solver(_solver) {
}
}
+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);
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;
public:
EncodingNode(Set *_s);
void addElement(Element *e);
+ uint getSize();
CMEMALLOC;
private:
Set *s;
uint numComparisons;
friend uint hashEncodingEdge(EncodingEdge *edge);
friend bool equalsEncodingEdge(EncodingEdge *e1, EncodingEdge *e2);
- fiend class EncodingGraph;
+ friend class EncodingGraph;
};
#endif
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: