X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2FBackend%2Forderpair.cc;h=e778247a22915252422c671cf2fb5aae0de041e1;hb=457ee300c637089a095444672c9d4628faf901e7;hp=9501af5dcc437f232c686395765e4be271a2820c;hpb=4216901871798182a3574865d6aa4f3ff3130a54;p=satune.git

diff --git a/src/Backend/orderpair.cc b/src/Backend/orderpair.cc
index 9501af5..e778247 100644
--- a/src/Backend/orderpair.cc
+++ b/src/Backend/orderpair.cc
@@ -1,14 +1,35 @@
 #include "orderpair.h"
+#include "constraint.h"
+#include "csolver.h"
+#include "satencoder.h"
 
+OrderPair::OrderPair(uint64_t _first, uint64_t _second, Edge _constraint) :
+	first(_first),
+	second(_second),
+	constraint(_constraint) {
+}
+
+OrderPair::OrderPair() :
+	first(0),
+	second(0),
+	constraint(E_NULL) {
+}
+
+OrderPair::~OrderPair() {
+}
+
+Edge OrderPair::getConstraint() {
+	return constraint;
+}
+
+Edge OrderPair::getNegatedConstraint() {
+	return constraintNegate(constraint);
+}
 
-OrderPair *allocOrderPair(uint64_t first, uint64_t second, Edge constraint) {
-	OrderPair *pair = (OrderPair *) ourmalloc(sizeof(OrderPair));
-	pair->first = first;
-	pair->second = second;
-	pair->constraint = constraint;
-	return pair;
+bool OrderPair::getConstraintValue(CSolver *solver) {
+	return getValueCNF(solver->getSATEncoder()->getCNF(), constraint);
 }
 
-void deleteOrderPair(OrderPair *pair) {
-	ourfree(pair);
+bool OrderPair::getNegatedConstraintValue(CSolver *solver) {
+	return getValueCNF(solver->getSATEncoder()->getCNF(), constraintNegate(constraint));
 }