--- /dev/null
+#include "analyzer.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 "orderencoder.h"
+#include "tunable.h"
+#include "transform.h"
+#include "element.h"
+#include "integerencoding.h"
+#include "decomposeordertransform.h"
+
+void orderAnalysis(CSolver *This) {
+ Vector<Order *> *orders = This->getOrders();
+ uint size = orders->getSize();
+ for (uint i = 0; i < size; i++) {
+ Order *order = orders->get(i);
+ DecomposeOrderTransform* decompose = new DecomposeOrderTransform(This, order, DECOMPOSEORDER, &onoff);
+ if (!decompose->canExecuteTransform())
+ continue;
+
+ OrderGraph *graph = buildOrderGraph(order);
+ if (order->type == 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(This->getTuner(), order->type, MUSTREACHGLOBAL, &onoff);
+
+ if (mustReachGlobal)
+ reachMustAnalysis(This, graph, false);
+
+ bool mustReachLocal = GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHLOCAL, &onoff);
+
+ if (mustReachLocal) {
+ //This pair of analysis is also optional
+ if (order->type == PARTIAL) {
+ localMustAnalysisPartial(This, graph);
+ } else {
+ localMustAnalysisTotal(This, graph);
+ }
+ }
+
+ bool mustReachPrune = GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
+
+ if (mustReachPrune)
+ removeMustBeTrueNodes(This, graph);
+
+ //This is needed for splitorder
+ computeStronglyConnectedComponentGraph(graph);
+ decompose->doTransform();
+ delete decompose;
+ delete graph;
+
+
+ IntegerEncodingTransform* integerEncoding = new IntegerEncodingTransform(This, order, ORDERINTEGERENCODING, &offon);
+ if(!integerEncoding->canExecuteTransform())
+ continue;
+ integerEncoding->doTransform();
+ delete integerEncoding;
+ }
+}
+
+
--- /dev/null
+/*
+ * File: analyzer.h
+ * Author: hamed
+ *
+ * Created on August 24, 2017, 5:33 PM
+ */
+
+#ifndef ORDERDECOMPOSE_H
+#define ORDERDECOMPOSE_H
+#include "classlist.h"
+#include "structs.h"
+
+void orderAnalysis(CSolver *This);
+
+#endif/* ORDERDECOMPOSE_H */
+
--- /dev/null
+/*
+ * File: ordertransform.cc
+ * Author: hamed
+ *
+ * Created on August 28, 2017, 10:35 AM
+ */
+
+#include "decomposeordertransform.h"
+#include "order.h"
+#include "orderedge.h"
+#include "ordernode.h"
+#include "boolean.h"
+#include "mutableset.h"
+#include "ordergraph.h"
+#include "csolver.h"
+
+
+DecomposeOrderTransform::DecomposeOrderTransform(CSolver* _solver, Order* _order, Tunables _tunable, TunableDesc* _desc)
+ :Transform(_solver, _tunable, _desc),
+ order(_order)
+{
+}
+
+DecomposeOrderTransform::~DecomposeOrderTransform() {
+}
+
+bool DecomposeOrderTransform::canExecuteTransform(){
+ return canExecutePass(solver, order->type);
+}
+
+void DecomposeOrderTransform::doTransform(){
+ Vector<Order *> ordervec;
+ Vector<Order *> partialcandidatevec;
+ uint size = order->constraints.getSize();
+ for (uint i = 0; i < size; i++) {
+ BooleanOrder *orderconstraint = order->constraints.get(i);
+ OrderNode *from = graph->getOrderNodeFromOrderGraph(orderconstraint->first);
+ OrderNode *to = graph->getOrderNodeFromOrderGraph(orderconstraint->second);
+ model_print("from->sccNum:%u\tto->sccNum:%u\n", from->sccNum, to->sccNum);
+ if (from->sccNum != to->sccNum) {
+ OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to);
+ if (edge->polPos) {
+ solver->replaceBooleanWithTrue(orderconstraint);
+ } else if (edge->polNeg) {
+ solver->replaceBooleanWithFalse(orderconstraint);
+ } else {
+ //This case should only be possible if constraint isn't in AST
+ ASSERT(0);
+ }
+ } else {
+ //Build new order and change constraint's order
+ Order *neworder = NULL;
+ if (ordervec.getSize() > from->sccNum)
+ neworder = ordervec.get(from->sccNum);
+ if (neworder == NULL) {
+ MutableSet *set = solver->createMutableSet(order->set->type);
+ neworder = solver->createOrder(order->type, set);
+ ordervec.setExpand(from->sccNum, neworder);
+ if (order->type == PARTIAL)
+ partialcandidatevec.setExpand(from->sccNum, neworder);
+ else
+ partialcandidatevec.setExpand(from->sccNum, NULL);
+ }
+ if (from->status != ADDEDTOSET) {
+ from->status = ADDEDTOSET;
+ ((MutableSet *)neworder->set)->addElementMSet(from->id);
+ }
+ if (to->status != ADDEDTOSET) {
+ to->status = ADDEDTOSET;
+ ((MutableSet *)neworder->set)->addElementMSet(to->id);
+ }
+ if (order->type == PARTIAL) {
+ OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to);
+ if (edge->polNeg)
+ partialcandidatevec.setExpand(from->sccNum, NULL);
+ }
+ orderconstraint->order = neworder;
+ neworder->addOrderConstraint(orderconstraint);
+ }
+ }
+
+ uint pcvsize = partialcandidatevec.getSize();
+ for (uint i = 0; i < pcvsize; i++) {
+ Order *neworder = partialcandidatevec.get(i);
+ if (neworder != NULL) {
+ neworder->type = TOTAL;
+ model_print("i=%u\t", i);
+ }
+ }
+}
--- /dev/null
+/*
+ * File: ordertransform.h
+ * Author: hamed
+ *
+ * Created on August 28, 2017, 10:35 AM
+ */
+
+#ifndef ORDERTRANSFORM_H
+#define ORDERTRANSFORM_H
+#include "classlist.h"
+#include "transform.h"
+
+
+class DecomposeOrderTransform : public Transform {
+public:
+ DecomposeOrderTransform(CSolver* _solver, Order* order, Tunables _tunable, TunableDesc* _desc);
+ virtual ~DecomposeOrderTransform();
+ void doTransform();
+ void setOrderGraph(OrderGraph* _graph){
+ graph = _graph;
+ }
+ bool canExecuteTransform();
+private:
+ Order* order;
+ OrderGraph* graph;
+};
+
+#endif /* ORDERTRANSFORM_H */
+
--- /dev/null
+
+#include "integerencoding.h"
+#include "set.h"
+#include "order.h"
+#include "satencoder.h"
+#include "csolver.h"
+#include "integerencodingrecord.h"
+
+HashTableOrderIntegerEncoding* IntegerEncodingTransform::orderIntegerEncoding = new HashTableOrderIntegerEncoding();
+
+IntegerEncodingTransform::IntegerEncodingTransform(CSolver* _solver, Order* _order, Tunables _tunable, TunableDesc* _desc)
+ :Transform(_solver, _tunable, _desc),
+ order(_order)
+
+{
+}
+
+IntegerEncodingTransform::~IntegerEncodingTransform(){
+}
+
+bool IntegerEncodingTransform::canExecuteTransform(){
+ return canExecutePass(solver, order->type);
+}
+
+void IntegerEncodingTransform::doTransform(){
+ if (!orderIntegerEncoding->contains(order)) {
+ orderIntegerEncoding->put(order, new IntegerEncodingRecord(
+ solver->createRangeSet(order->set->type, 0, (uint64_t) order->set->getSize()-1)));
+ }
+ uint size = order->constraints.getSize();
+ for(uint i=0; i<size; i++){
+ orderIntegerEncodingSATEncoder(order->constraints.get(i));
+ }
+}
+
+
+void IntegerEncodingTransform::orderIntegerEncodingSATEncoder(BooleanOrder *boolOrder) {
+ IntegerEncodingRecord* ierec = orderIntegerEncoding->get(order);
+ //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};
+ Predicate *predicate = solver->createPredicateOperator(LT, sarray, 2);
+ Element *parray[] = {elem1, elem2};
+ Boolean *boolean = solver->applyPredicate(predicate, parray, 2);
+ solver->addConstraint(boolean);
+ solver->replaceBooleanWithBoolean(boolOrder, boolean);
+}
+
--- /dev/null
+/*
+ * File: integerencoding.h
+ * Author: hamed
+ *
+ * Created on August 27, 2017, 4:36 PM
+ */
+
+#ifndef INTEGERENCODING_H
+#define INTEGERENCODING_H
+#include "classlist.h"
+#include "transform.h"
+#include "order.h"
+
+class IntegerEncodingTransform : public Transform{
+public:
+ IntegerEncodingTransform(CSolver* solver, Order* order, Tunables _tunable, TunableDesc* _desc);
+ void orderIntegerEncodingSATEncoder(BooleanOrder *boolOrder);
+ void doTransform();
+ bool canExecuteTransform();
+ ~IntegerEncodingTransform();
+private:
+ Order* order;
+ // In future we can use a singleton class instead of static variable for keeping data that needed
+ // for translating back result
+ static HashTableOrderIntegerEncoding* orderIntegerEncoding;
+};
+
+
+#endif /* INTEGERENCODING_H */
+
+++ /dev/null
-#include "orderdecompose.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 "orderencoder.h"
-#include "tunable.h"
-#include "transform.h"
-#include "element.h"
-
-void orderAnalysis(CSolver *This) {
- Transform* transform = new Transform();
- Vector<Order *> *orders = This->getOrders();
- uint size = orders->getSize();
- for (uint i = 0; i < size; i++) {
- Order *order = orders->get(i);
- bool doDecompose = GETVARTUNABLE(This->getTuner(), order->type, DECOMPOSEORDER, &onoff);
- if (!doDecompose)
- continue;
-
- OrderGraph *graph = buildOrderGraph(order);
- if (order->type == 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(This->getTuner(), order->type, MUSTREACHGLOBAL, &onoff);
-
- if (mustReachGlobal)
- reachMustAnalysis(This, graph, false);
-
- bool mustReachLocal = GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHLOCAL, &onoff);
-
- if (mustReachLocal) {
- //This pair of analysis is also optional
- if (order->type == PARTIAL) {
- localMustAnalysisPartial(This, graph);
- } else {
- localMustAnalysisTotal(This, graph);
- }
- }
-
- bool mustReachPrune = GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
-
- if (mustReachPrune)
- removeMustBeTrueNodes(This, graph);
-
- //This is needed for splitorder
- computeStronglyConnectedComponentGraph(graph);
- decomposeOrder(This, order, graph);
- delete graph;
-
-
- bool doIntegerEncoding = GETVARTUNABLE(This->getTuner(), order->order.type, ORDERINTEGERENCODING, &offon );
- if(!doIntegerEncoding)
- continue;
- uint size = order->constraints.getSize();
- for(uint i=0; i<size; i++){
- transform->orderIntegerEncodingSATEncoder(This, order->constraints.get(i));
- }
-
- }
- delete transform;
-}
-
-void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) {
- Vector<Order *> ordervec;
- Vector<Order *> partialcandidatevec;
- uint size = order->constraints.getSize();
- for (uint i = 0; i < size; i++) {
- BooleanOrder *orderconstraint = order->constraints.get(i);
- OrderNode *from = graph->getOrderNodeFromOrderGraph(orderconstraint->first);
- OrderNode *to = graph->getOrderNodeFromOrderGraph(orderconstraint->second);
- model_print("from->sccNum:%u\tto->sccNum:%u\n", from->sccNum, to->sccNum);
- if (from->sccNum != to->sccNum) {
- OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to);
- if (edge->polPos) {
- This->replaceBooleanWithTrue(orderconstraint);
- } else if (edge->polNeg) {
- This->replaceBooleanWithFalse(orderconstraint);
- } else {
- //This case should only be possible if constraint isn't in AST
- ASSERT(0);
- }
- } else {
- //Build new order and change constraint's order
- Order *neworder = NULL;
- if (ordervec.getSize() > from->sccNum)
- neworder = ordervec.get(from->sccNum);
- if (neworder == NULL) {
- MutableSet *set = This->createMutableSet(order->set->type);
- neworder = This->createOrder(order->type, set);
- ordervec.setExpand(from->sccNum, neworder);
- if (order->type == PARTIAL)
- partialcandidatevec.setExpand(from->sccNum, neworder);
- else
- partialcandidatevec.setExpand(from->sccNum, NULL);
- }
- if (from->status != ADDEDTOSET) {
- from->status = ADDEDTOSET;
- ((MutableSet *)neworder->set)->addElementMSet(from->id);
- }
- if (to->status != ADDEDTOSET) {
- to->status = ADDEDTOSET;
- ((MutableSet *)neworder->set)->addElementMSet(to->id);
- }
- if (order->type == PARTIAL) {
- OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to);
- if (edge->polNeg)
- partialcandidatevec.setExpand(from->sccNum, NULL);
- }
- orderconstraint->order = neworder;
- neworder->addOrderConstraint(orderconstraint);
- }
- }
-
- uint pcvsize = partialcandidatevec.getSize();
- for (uint i = 0; i < pcvsize; i++) {
- Order *neworder = partialcandidatevec.get(i);
- if (neworder != NULL) {
- neworder->type = TOTAL;
- model_print("i=%u\t", i);
- }
- }
-}
-
+++ /dev/null
-/*
- * To change this license header, choose License Headers in Project Properties.
- * To change this template file, choose Tools | Templates
- * and open the template in the editor.
- */
-
-/*
- * File: orderdecompose.h
- * Author: hamed
- *
- * Created on August 24, 2017, 5:33 PM
- */
-
-#ifndef ORDERDECOMPOSE_H
-#define ORDERDECOMPOSE_H
-#include "classlist.h"
-#include "structs.h"
-
-void orderAnalysis(CSolver *This);
-void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph);
-
-#endif/* ORDERDECOMPOSE_H */
-
--- /dev/null
+#include "pass.h"
+#include "tunable.h"
+#include "csolver.h"
+
+Pass::Pass(Tunables _tunable, TunableDesc* _desc):
+ tunable(_tunable),
+ tunableDesc(_desc)
+{
+
+}
+
+Pass::~Pass(){
+
+}
--- /dev/null
+/*
+ * File: pass.h
+ * Author: hamed
+ *
+ * Created on August 28, 2017, 6:23 PM
+ */
+
+#ifndef PASS_H
+#define PASS_H
+#include "classlist.h"
+#include "mymemory.h"
+#include "structs.h"
+#include "tunable.h"
+#include "csolver.h"
+
+class Pass{
+public:
+ Pass(Tunables _tunable, TunableDesc* _desc);
+ virtual ~Pass();
+ virtual inline bool canExecutePass(CSolver* This, uint type=0){
+ return GETVARTUNABLE(This->getTuner(), type, tunable, tunableDesc);
+ }
+ MEMALLOC;
+protected:
+ Tunables tunable;
+ TunableDesc* tunableDesc;
+};
+
+
+#endif /* PASS_H */
+
-/*
- * To change this license header, choose License Headers in Project Properties.
- * To change this template file, choose Tools | Templates
- * and open the template in the editor.
- */
-
/*
* File: transform.cc
* Author: hamed
*/
#include "transform.h"
-#include "set.h"
-#include "order.h"
-#include "satencoder.h"
-#include "csolver.h"
-#include "integerencodingrecord.h"
-
-Transform::Transform() {
- orderIntegerEncoding = new HashTableOrderIntegerEncoding;
-}
-void Transform:: orderIntegerEncodingSATEncoder(CSolver *This, BooleanOrder *boolOrder) {
- Order *order = boolOrder->order;
- if (!orderIntegerEncoding->contains(order)) {
- orderIntegerEncoding->put(order, new IntegerEncodingRecord(
- This->createRangeSet(order->set->type, 0, (uint64_t) order->set->getSize()-1)));
- }
- IntegerEncodingRecord* ierec = orderIntegerEncoding->get(order);
- //getting two elements and using LT predicate ...
- Element *elem1 = ierec->getOrderIntegerElement(This, boolOrder->first);
- Element *elem2 = ierec->getOrderIntegerElement(This, boolOrder->second);
- Set *sarray[] = {ierec->set, ierec->set};
- Predicate *predicate = This->createPredicateOperator(LT, sarray, 2);
- Element *parray[] = {elem1, elem2};
- Boolean *boolean = This->applyPredicate(predicate, parray, 2);
- This->addConstraint(boolean);
- This->replaceBooleanWithBoolean(boolOrder, boolean);
+Transform::Transform(CSolver* _solver, Tunables _tunable, TunableDesc* _desc):
+ Pass(_tunable, _desc)
+{
+ solver = _solver;
}
Transform::~Transform(){
- delete orderIntegerEncoding;
}
#include "classlist.h"
#include "mymemory.h"
#include "structs.h"
+#include "pass.h"
-class Transform {
+class Transform : public Pass{
public:
- Transform();
- ~Transform();
- void orderIntegerEncodingSATEncoder(CSolver *This, BooleanOrder *boolOrder);
- MEMALLOC;
-private:
- HashTableOrderIntegerEncoding* orderIntegerEncoding;
+ Transform(CSolver* _solver,Tunables _tunable, TunableDesc* _desc);
+ virtual ~Transform();
+ virtual bool canExecuteTransform() = 0;
+ virtual void doTransform() = 0;
+protected:
+ // Need solver for translating back the result ...
+ CSolver* solver;
};
#endif /* TRANSFORM_H */
class OrderNode;
class OrderEdge;
+class Pass;
+class Transform;
struct IncrementalSolver;
typedef struct IncrementalSolver IncrementalSolver;
#include "sattranslator.h"
#include "tunable.h"
#include "polarityassignment.h"
-#include "orderdecompose.h"
+#include "analyzer.h"
CSolver::CSolver() : unsat(false) {
tuner = new Tuner();
projects / satune.git / commitdiff