void IntegerEncodingTransform::orderIntegerEncodingSATEncoder(BooleanOrder *boolOrder) {
- IntegerEncodingRecord* ierec = orderIntegerEncoding->get(order);
- //getting two elements and using SATC_LT predicate ...
+ IntegerEncodingRecord* ierec = orderIntEncoding->get(currOrder);
+ //getting two elements and using LT predicate ...
Element *elem1 = ierec->getOrderIntegerElement(solver, boolOrder->first);
Element *elem2 = ierec->getOrderIntegerElement(solver, boolOrder->second);
- Set *sarray[] = {ierec->set, ierec->set};
+ Set *sarray[] = {ierec->getSecondarySet(), ierec->getSecondarySet()};
- Predicate *predicate = solver->createPredicateOperator(LT, sarray, 2);
+ Predicate *predicate = solver->createPredicateOperator(SATC_LT, sarray, 2);
Element *parray[] = {elem1, elem2};
Boolean *boolean = solver->applyPredicate(predicate, parray, 2);
solver->addConstraint(boolean);
#include "orderelement.h"
IntegerEncodingRecord::IntegerEncodingRecord(Set* _set):
- set(_set)
+ secondarySet(_set)
{
- elementTable = new HashSetOrderElement();
+ elementTable = new HashsetOrderElement();
}
IntegerEncodingRecord::~IntegerEncodingRecord(){
IntegerEncodingRecord(Set* set);
~IntegerEncodingRecord();
Element* getOrderIntegerElement(CSolver *This, uint64_t item);
- MEMALLOC;
+ inline Set* getSecondarySet() { return secondarySet; }
+ CMEMALLOC;
+
private:
- HashSetOrderElement *elementTable;
+ Set* secondarySet;
+ HashsetOrderElement *elementTable;
};
#endif /* INTEGERENCODINGRECORD_H */
--- /dev/null
- if (order->type == PARTIAL) {
+#include "transformer.h"
+#include "common.h"
+#include "order.h"
+#include "boolean.h"
+#include "ordergraph.h"
+#include "ordernode.h"
+#include "rewriter.h"
+#include "orderedge.h"
+#include "mutableset.h"
+#include "ops.h"
+#include "csolver.h"
+#include "orderanalysis.h"
+#include "tunable.h"
+#include "transform.h"
+#include "element.h"
+#include "integerencoding.h"
+#include "decomposeordertransform.h"
+
+Transformer::Transformer(CSolver *_solver):
+ integerEncoding(new IntegerEncodingTransform(_solver)),
+ solver(_solver)
+{
+}
+
+Transformer::~Transformer(){
+ delete integerEncoding;
+}
+
+void Transformer::orderAnalysis() {
+ Vector<Order *> *orders = solver->getOrders();
+ uint size = orders->getSize();
+ for (uint i = 0; i < size; i++) {
+ Order *order = orders->get(i);
+ DecomposeOrderTransform* decompose = new DecomposeOrderTransform(solver, order);
+ if (!decompose->canExecuteTransform()){
+ delete decompose;
+ continue;
+ }
+
+ OrderGraph *graph = buildOrderGraph(order);
- //solver pair of analysis is also optional
- if (order->type == PARTIAL) {
++ if (order->type == SATC_PARTIAL) {
+ //Required to do SCC analysis for partial order graphs. It
+ //makes sure we don't incorrectly optimize graphs with negative
+ //polarity edges
+ completePartialOrderGraph(graph);
+ }
+
+
+ bool mustReachGlobal = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHGLOBAL, &onoff);
+
+ if (mustReachGlobal)
+ reachMustAnalysis(solver, graph, false);
+
+ bool mustReachLocal = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHLOCAL, &onoff);
+
+ if (mustReachLocal) {
++ //This pair of analysis is also optional
++ if (order->type == SATC_PARTIAL) {
+ localMustAnalysisPartial(solver, graph);
+ } else {
+ localMustAnalysisTotal(solver, graph);
+ }
+ }
+
+ bool mustReachPrune = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
+
+ if (mustReachPrune)
+ removeMustBeTrueNodes(solver, graph);
+
+ //This is needed for splitorder
+ computeStronglyConnectedComponentGraph(graph);
+ decompose->setOrderGraph(graph);
+ decompose->doTransform();
+ delete decompose;
+ delete graph;
+
+ integerEncoding->setCurrentOrder(order);
+ if(!integerEncoding->canExecuteTransform()){
+ continue;
+ }
+ integerEncoding->doTransform();
+ }
+}
+
+
class OrderElement {
public:
OrderElement(uint64_t item, Element *elem);
- MEMALLOC;
+ inline uint getHash() {return (uint) item;}
+ inline bool equals(OrderElement* oe){ return item == oe->item;}
+ inline Element* getElement() { return elem; }
++ CMEMALLOC;
+private:
uint64_t item;
Element *elem;
- CMEMALLOC;
};
bool order_element_equals(OrderElement *key1, OrderElement *key2);
unsigned int order_pair_hash_function(OrderPair *This);
bool order_pair_equals(OrderPair *key1, OrderPair *key2);
- unsigned int order_hash_function(Order *This);
- bool order_pair_equals(Order *key1, Order *key2);
- typedef HashSet<Boolean *, uintptr_t, 4> HashSetBoolean;
- typedef HashSet<TableEntry *, uintptr_t, 4, table_entry_hash_function, table_entry_equals> HashSetTableEntry;
- typedef HashSet<OrderNode *, uintptr_t, 4, order_node_hash_function, order_node_equals> HashSetOrderNode;
- typedef HashSet<OrderEdge *, uintptr_t, 4, order_edge_hash_function, order_edge_equals> HashSetOrderEdge;
- typedef HashSet<OrderElement *, uintptr_t, 4, order_element_hash_function, order_element_equals> HashSetOrderElement;
-
+ typedef Hashset<TableEntry *, uintptr_t, 4, table_entry_hash_function, table_entry_equals> HashsetTableEntry;
+ typedef Hashset<OrderNode *, uintptr_t, 4, order_node_hash_function, order_node_equals> HashsetOrderNode;
+ typedef Hashset<OrderEdge *, uintptr_t, 4, order_edge_hash_function, order_edge_equals> HashsetOrderEdge;
+ typedef Hashset<OrderElement *, uintptr_t, 4, order_element_hash_function, order_element_equals> HashsetOrderElement;
+
- typedef HashTable<OrderNode *, HashSetOrderNode *, uintptr_t, 4> HashTableNodeToNodeSet;
- typedef HashTable<OrderPair *, OrderPair *, uintptr_t, 4, order_pair_hash_function, order_pair_equals> HashTableOrderPair;
- typedef HashTable<void *, void *, uintptr_t, 4> CloneMap;
- typedef HashTable<Order* , IntegerEncodingRecord*, uintptr_t, 4, order_hash_function, order_pair_equals> HashTableOrderIntEncoding;
+ typedef Hashtable<OrderNode *, HashsetOrderNode *, uintptr_t, 4> HashtableNodeToNodeSet;
+ typedef Hashtable<OrderPair *, OrderPair *, uintptr_t, 4, order_pair_hash_function, order_pair_equals> HashtableOrderPair;
+ typedef Hashtable<void *, void *, uintptr_t, 4> CloneMap;
-typedef Hashtable<Order* , IntegerEncodingRecord*, uintptr_t, 4> HashtableOrderIntegerEncoding;
++typedef Hashtable<Order* , IntegerEncodingRecord*, uintptr_t, 4> HashTableOrderIntEncoding;
- typedef HSIterator<TableEntry *, uintptr_t, 4, table_entry_hash_function, table_entry_equals> HSIteratorTableEntry;
- typedef HSIterator<Boolean *, uintptr_t, 4> HSIteratorBoolean;
- typedef HSIterator<OrderEdge *, uintptr_t, 4, order_edge_hash_function, order_edge_equals> HSIteratorOrderEdge;
- typedef HSIterator<OrderNode *, uintptr_t, 4, order_node_hash_function, order_node_equals> HSIteratorOrderNode;
- typedef HSIterator<OrderElement *, uintptr_t, 4, order_element_hash_function, order_element_equals> HSIteratorOrderElement;
+ typedef SetIterator<TableEntry *, uintptr_t, 4, table_entry_hash_function, table_entry_equals> SetIteratorTableEntry;
+ typedef SetIterator<OrderEdge *, uintptr_t, 4, order_edge_hash_function, order_edge_equals> SetIteratorOrderEdge;
+ typedef SetIterator<OrderNode *, uintptr_t, 4, order_node_hash_function, order_node_equals> SetIteratorOrderNode;
-
++typedef SetIterator<OrderElement *, uintptr_t, 4, order_element_hash_function, order_element_equals> SetIteratorOrderElement;
#endif
--- /dev/null
+ /* Copyright (c) 2015 Regents of the University of California
+ *
+ * Author: Brian Demsky <bdemsky@uci.edu>
+ *
+ * This program is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * version 2 as published by the Free Software Foundation.
+ */
+
+ #ifndef CLASSES_H
+ #define CLASSES_H
+
+ #include "mymemory.h"
+ #include <inttypes.h>
+
+ class SATEncoder;
+ class CSolver;
+ class Boolean;
+ class Element;
+ class Predicate;
+ class Table;
+ class Order;
+ class MutableSet;
+ class Function;
+ class Tuner;
++class Transformer;
+ class Set;
+ class BooleanLogic;
+ typedef uint64_t VarType;
+ typedef unsigned int uint;
+
+ #endif
#include "sattranslator.h"
#include "tunable.h"
#include "polarityassignment.h"
-#include "analyzer.h"
+#include "transformer.h"
#include "autotuner.h"
+ #include "astops.h"
+ #include "structs.h"
CSolver::CSolver() :
+ boolTrue(new BooleanConst(true)),
+ boolFalse(new BooleanConst(false)),
unsat(false),
tuner(NULL),
elapsedTime(0)
delete allFunctions.get(i);
}
+ delete boolTrue;
+ delete boolFalse;
delete satEncoder;
+ delete transformer;
}
CSolver *CSolver::clone() {
Vector<Order *> *getOrders() { return &allOrders;}
Tuner *getTuner() { return tuner; }
+ Transformer* getTransformer() {return transformer;}
- HSIteratorBoolean *getConstraints() { return constraints.iterator(); }
+ SetIteratorBoolean *getConstraints() { return constraints.iterator(); }
SATEncoder *getSATEncoder() {return satEncoder;}
CSolver *clone();
void autoTune(uint budget);
- void setTuner(Transformer * _transformer) { transformer = _transformer; }
++ void setTransformer(Transformer * _transformer) { transformer = _transformer; }
void setTuner(Tuner * _tuner) { tuner = _tuner; }
long long getElapsedTime() { return elapsedTime; }
long long getEncodeTime();