projects
/
satune.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Don't reencode expressions that are already encoded
[satune.git]
/
src
/
csolver.h
diff --git
a/src/csolver.h
b/src/csolver.h
index b27e3c00038d586908d6d17bb80f79a774b7eaed..5ef235d3d8ce9b26032380b30c4cea82c85bd0f2 100644
(file)
--- a/
src/csolver.h
+++ b/
src/csolver.h
@@
-103,6
+103,9
@@
public:
/** This exactly one element of array can be true! (i.e. a1 + a2 + a3 + ... + an = 1)*/
BooleanEdge applyExactlyOneConstraint (BooleanEdge *array, uint asize);
/** This exactly one element of array can be true! (i.e. a1 + a2 + a3 + ... + an = 1)*/
BooleanEdge applyExactlyOneConstraint (BooleanEdge *array, uint asize);
+
+ /** This exactly one element of array can be true! (i.e. a1 => !a2 & !a3 & ... & !an)*/
+ BooleanEdge applyAtMostOneConstraint (BooleanEdge *array, uint asize);
/** This function applies a logical operation to the Booleans in its input. */
/** This function applies a logical operation to the Booleans in its input. */
@@
-141,7
+144,7
@@
public:
uint64_t getElementValue(Element *element);
void freezeElement(Element *e);
uint64_t getElementValue(Element *element);
void freezeElement(Element *e);
-
+ void turnoffOptimizations(){optimizationsOff = true;}
/** After getting the solution from the SAT solver, client can get the value of a boolean via this function*/
bool getBooleanValue(BooleanEdge boolean);
/** After getting the solution from the SAT solver, client can get the value of a boolean via this function*/
bool getBooleanValue(BooleanEdge boolean);
@@
-237,10
+240,12
@@
private:
bool unsat;
bool booleanVarUsed;
bool incrementalMode;
bool unsat;
bool booleanVarUsed;
bool incrementalMode;
+ bool optimizationsOff;
Tuner *tuner;
long long elapsedTime;
long satsolverTimeout;
Interpreter *interpreter;
Tuner *tuner;
long long elapsedTime;
long satsolverTimeout;
Interpreter *interpreter;
+ bool noOptimization;
friend class ElementOpt;
friend class VarOrderingOpt;
};
friend class ElementOpt;
friend class VarOrderingOpt;
};