X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2FBackend%2Forderpair.cc;h=e778247a22915252422c671cf2fb5aae0de041e1;hb=02df685ced0f69f14934c0cbebdbd694f199d341;hp=89913bbfe00e5d34025c16b529c9ad65d473d13b;hpb=7c10dbd982d74cf1e96c06b3078e329c62e6a3e8;p=satune.git

diff --git a/src/Backend/orderpair.cc b/src/Backend/orderpair.cc
index 89913bb..e778247 100644
--- a/src/Backend/orderpair.cc
+++ b/src/Backend/orderpair.cc
@@ -1,5 +1,7 @@
 #include "orderpair.h"
-
+#include "constraint.h"
+#include "csolver.h"
+#include "satencoder.h"
 
 OrderPair::OrderPair(uint64_t _first, uint64_t _second, Edge _constraint) :
 	first(_first),
@@ -12,3 +14,22 @@ OrderPair::OrderPair() :
 	second(0),
 	constraint(E_NULL) {
 }
+
+OrderPair::~OrderPair() {
+}
+
+Edge OrderPair::getConstraint() {
+	return constraint;
+}
+
+Edge OrderPair::getNegatedConstraint() {
+	return constraintNegate(constraint);
+}
+
+bool OrderPair::getConstraintValue(CSolver *solver) {
+	return getValueCNF(solver->getSATEncoder()->getCNF(), constraint);
+}
+
+bool OrderPair::getNegatedConstraintValue(CSolver *solver) {
+	return getValueCNF(solver->getSATEncoder()->getCNF(), constraintNegate(constraint));
+}