From b7d8ca816a513565a36f83be7f9c7dc9566204f0 Mon Sep 17 00:00:00 2001 From: bdemsky Date: Thu, 24 Aug 2017 16:02:57 -0700 Subject: [PATCH] Add LTE function for completeness and fix bug in LT --- src/Backend/constraint.c | 16 ++++++++++++++-- src/Backend/constraint.h | 1 + 2 files changed, 15 insertions(+), 2 deletions(-) diff --git a/src/Backend/constraint.c b/src/Backend/constraint.c index 3e0d0a8..c7cac98 100644 --- a/src/Backend/constraint.c +++ b/src/Backend/constraint.c @@ -883,7 +883,7 @@ Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) { Edge generateLTConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2){ if(numvars == 0 ) - return E_True; + return E_False; Edge result =constraintAND2(cnf, constraintNegate( var1[0]), var2[0]); for (uint i = 1; i < numvars; i++) { Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]); @@ -891,4 +891,16 @@ Edge generateLTConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2){ result = constraintOR2(cnf, lt, eq); } return result; -} \ No newline at end of file +} + +Edge generateLTEConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2){ + if(numvars == 0 ) + return E_True; + Edge result =constraintIMPLIES(cnf, var1[0], var2[0]); + for (uint i = 1; i < numvars; i++) { + Edge lt = constraintAND2(cnf, constraintNegate( var1[i]), var2[i]); + Edge eq = constraintAND2(cnf, constraintIFF(cnf, var1[i], var2[i]), result); + result = constraintOR2(cnf, lt, eq); + } + return result; +} diff --git a/src/Backend/constraint.h b/src/Backend/constraint.h index 772f6c8..02fe3da 100644 --- a/src/Backend/constraint.h +++ b/src/Backend/constraint.h @@ -212,6 +212,7 @@ Edge generateBinaryConstraint(CNF *cnf, uint numvars, Edge *vars, uint value); Edge generateLTValueConstraint(CNF *cnf, uint numvars, Edge *vars, uint value); Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2); Edge generateLTConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2); +Edge generateLTEConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2); extern Edge E_True; extern Edge E_False; -- 2.34.1