0

I try to resolve the circuit satisfiability problem reading the circuit from file (in the form presented in text visualizer-somehow dynamic). If my circuit is small my resolver work smooth (small means like <16-18 wires). If i get to 25-30 wires so 2^25-30 possibilities i encountered a problem with a violation of access. I tried to free memory every time i can. I tried to create a new pointer of my expression every time, but the access violation always occur. Circuit Satisfiability Bug

^ How is this possible ?

int evalBoolExprForBinaryVector(char *expr, int n, int binaryVector[]){

    // create boolean expression from logical expression
    char* expression = (char*) malloc(sizeof(char) * strlen(expr) + 1);
    strcpy(expression, expr);

    for(int binaryVectorCounter=0; binaryVectorCounter<n; binaryVectorCounter++){
        char* currentSearchedIdentifier = (char*) malloc(sizeof(char) * 10);
        char* index =(char*) malloc(sizeof(char) * 10);
        char* valueOfIndex = (char*) malloc(sizeof(char)*2);
        strcpy(currentSearchedIdentifier,"v[");
        sprintf(index, "%d", binaryVectorCounter);
        strcat(currentSearchedIdentifier, index);
        strcat(currentSearchedIdentifier, "]");
        sprintf(valueOfIndex, "%d", binaryVector[binaryVectorCounter]);
        expression = str_replace(expression,currentSearchedIdentifier,valueOfIndex);
        free(currentSearchedIdentifier);
        free(index);
        free(valueOfIndex);
    }
    // here my expression will be something like 
    // ( 0 | 1 ) & (!0 | !1) & ...
    // evaluate this
    return evalBoolExpr(expression);
};

Here is my code for better understanding.

The program breaks with this exception in strlen.asm at:

main_loop:
        mov     eax,dword ptr [ecx]     ; read 4 bytes

Thanks in advance for any thoughts.

Razvan Dumitru
  • 11,815
  • 5
  • 34
  • 54
  • What is Circuit Satisfiability Solver? – Prof. Falken Feb 06 '15 at 11:02
  • Sorry, i try to explain (in general) what my program does. I check every possibility in 2^n (n - no. of wires) and try to satisfy the circuit - to get true value at output. – Razvan Dumitru Feb 06 '15 at 11:03
  • 1
    By the way, ***always*** check return value of `malloc`. Also, use `snprintf()` if you have it, or use `_snprintf()` if you must, but be aware of its pitfalls: http://stackoverflow.com/a/13067917/193892 Also check tools like http://stackoverflow.com/a/6580332/193892 – Prof. Falken Feb 06 '15 at 11:03
  • 1
    Don't use C string handling vOv. – Bartek Banachewicz Feb 06 '15 at 11:08
  • And by that u mean to use std::string always ? – Razvan Dumitru Feb 06 '15 at 11:13
  • 1
    Do you ever release the memory you're allocating for `expression`? If you're using C++: use `std::string`, avoid manual memory management. – molbdnilo Feb 06 '15 at 11:45
  • Yes i release the memory for expression after i parse and evaluate. I will use C++, i need some modifications, i will try that and come with a response. – Razvan Dumitru Feb 06 '15 at 12:05
  • I checked the return value of malloc and use the handling from C++. I observe a small delay ( 20% ), but everything work smooth now. Thanks for advices. – Razvan Dumitru Feb 06 '15 at 21:22

1 Answers1

0

I rewrite this part in c++ manner and everything worked smooth (some delay but at least it can finish with success)

void replaceAll(std::string& str, const std::string& from, const std::string& to) {
    if(from.empty())
        return;
    size_t start_pos = 0;
    while((start_pos = str.find(from, start_pos)) != std::string::npos) {
        str.replace(start_pos, from.length(), to);
        start_pos += to.length();
    }
}

int evalBoolExprForBinaryVector(char *expr, int n, int binaryVector[]){

    std::string expression(expr);

    for(int binaryVectorCounter=0; binaryVectorCounter<n; binaryVectorCounter++){
        std::string currentSearchedIdentifier, valueOfIndex;    
        currentSearchedIdentifier = "v[" + std::to_string(binaryVectorCounter) + "]";
        valueOfIndex = std::to_string(binaryVector[binaryVectorCounter]);
        replaceAll(expression,currentSearchedIdentifier,valueOfIndex);
    }

    char *cstr = new char[expression.length() + 1];
    strcpy(cstr, expression.c_str());

    return evalBoolExpr(cstr);
};
Razvan Dumitru
  • 11,815
  • 5
  • 34
  • 54