projects
/
satune.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Interpreter abstraction and memory bug fixes
[satune.git]
/
src
/
csolver.cc
diff --git
a/src/csolver.cc
b/src/csolver.cc
index c81e2f3e1c1941789dc0259467dc1f206881193e..14f902b85e846c5f7c6e0a7e1bc76eb03705a9a3 100644
(file)
--- a/
src/csolver.cc
+++ b/
src/csolver.cc
@@
-39,7
+39,7
@@
CSolver::CSolver() :
tuner(NULL),
elapsedTime(0),
satsolverTimeout(NOTIMEOUT),
tuner(NULL),
elapsedTime(0),
satsolverTimeout(NOTIMEOUT),
-
alloyEncod
er(NULL)
+
interpret
er(NULL)
{
satEncoder = new SATEncoder(this);
}
{
satEncoder = new SATEncoder(this);
}
@@
-82,6
+82,10
@@
CSolver::~CSolver() {
for (uint i = 0; i < size; i++) {
delete allFunctions.get(i);
}
for (uint i = 0; i < size; i++) {
delete allFunctions.get(i);
}
+
+ if(interpreter != NULL){
+ delete interpreter;
+ }
delete boolTrue.getBoolean();
delete satEncoder;
delete boolTrue.getBoolean();
delete satEncoder;
@@
-606,9
+610,9
@@
int CSolver::solve() {
}
int result = IS_INDETER;
if(useAlloyCompiler()){
}
int result = IS_INDETER;
if(useAlloyCompiler()){
-
alloyEncod
er->encode();
+
interpret
er->encode();
model_print("Problem encoded in Alloy\n");
model_print("Problem encoded in Alloy\n");
- result =
alloyEncod
er->solve();
+ result =
interpret
er->solve();
model_print("Problem solved by Alloy\n");
} else{
model_print("Problem solved by Alloy\n");
} else{
@@
-676,8
+680,8
@@
int CSolver::solve() {
}
void CSolver::setAlloyEncoder(){
}
void CSolver::setAlloyEncoder(){
- if(
alloyEncod
er == NULL){
-
alloyEncod
er = new AlloyEnc(this);
+ if(
interpret
er == NULL){
+
interpret
er = new AlloyEnc(this);
}
}
}
}
@@
-699,7
+703,7
@@
uint64_t CSolver::getElementValue(Element *element) {
case ELEMSET:
case ELEMCONST:
case ELEMFUNCRETURN:
case ELEMSET:
case ELEMCONST:
case ELEMFUNCRETURN:
- return useAlloyCompiler()?
alloyEncod
er->getValue(element):
+ return useAlloyCompiler()?
interpret
er->getValue(element):
getElementValueSATTranslator(this, element);
default:
ASSERT(0);
getElementValueSATTranslator(this, element);
default:
ASSERT(0);
@@
-711,7
+715,7
@@
bool CSolver::getBooleanValue(BooleanEdge bedge) {
Boolean *boolean = bedge.getBoolean();
switch (boolean->type) {
case BOOLEANVAR:
Boolean *boolean = bedge.getBoolean();
switch (boolean->type) {
case BOOLEANVAR:
- return useAlloyCompiler()?
alloyEncod
er->getBooleanValue(boolean):
+ return useAlloyCompiler()?
interpret
er->getBooleanValue(boolean):
getBooleanVariableValueSATTranslator(this, boolean);
default:
ASSERT(0);
getBooleanVariableValueSATTranslator(this, boolean);
default:
ASSERT(0);