edits

[satune.git] / src / Backend / constraint.h

diff --git a/src/Backend/constraint.h b/src/Backend/constraint.h
index b2488178134bc82bc50ee5680dd9622154dca1ad..2f61d72a41e31d86acd1ca814a7eb3df43ff38e5 100644 (file)
--- a/src/Backend/constraint.h
+++ b/src/Backend/constraint.h
@@ -63,6 +63,8 @@ struct CNF {
        IncrementalSolver *solver;
        VectorEdge constraints;
        VectorEdge args;
+       long long solveTime;
+       long long encodeTime;
 };
 
 typedef struct CNF CNF;
@@ -209,8 +211,10 @@ Literal introProxy(CNF *cnf, Edge e, CNFExpr *exp, bool isNeg);
 void outputCNF(CNF *cnf, CNFExpr *expr);
 
 Edge generateBinaryConstraint(CNF *cnf, uint numvars, Edge *vars, uint value);
-Edge generateLTConstraint(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;