Incremental solver works and the test case passes

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

diff --git a/src/Backend/constraint.h b/src/Backend/constraint.h
index 8d2666ca2e17464c8023fccbc3a5ac5c6e594228..f623571bad97c6bda47c9790573bd51060a2e56c 100644 (file)
--- a/src/Backend/constraint.h
+++ b/src/Backend/constraint.h
@@ -182,6 +182,7 @@ void outputCNF(CNF *cnf, Edge cnfform);
 void outputCNFOR(CNF *cnf, Edge cnfform, Edge eorvar);
 void generateProxy(CNF *cnf, Edge expression, Edge proxy, Polarity p);
 void addClause(CNF *cnf, uint numliterals, int *literals);
+void freezeVariable(CNF *cnf, Edge e);
 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);