Check if two "simple" 'if statements' in C are equivalent

Question

I have 'if statements' from two different sources, which try to implement the same condition possibly in a different way. The 'if statements' are C. If at all possible I need a python script that can decide whether pairs of conditions are equivalent or not. A basic example:

source1: ((op1 != v1) || ((op2 != v2) || (op3 != v3)))

source2: ((op2 != v2) || (op1 != v1) || (op3 != v3))

Of course any operator is allowed, function calls and of course parentheses.

Any ideas are welcome.

Edit 1: The function calls have no side effects.

Answer 1

Here's the thing, the problem may (or may not) be NP-complete but unless this is within the inner-loop of something important (and the number of variable are small), build the entire truth table! It's extremely easy to do. It obviously grows as 2^n, but for small n this is completely feasible. Like the comments suggest, I'm assuming that the function calls have no side effects and simply output True or False.

I've posted a mockup example that solves your stated problem, adapt as needed. I rely on pythons parser to handle the evaluation of the expression.

import pyparsing as pypar
import itertools

def python_equiv(s):
    return s.replace('||',' or ').replace('&&',' and ')

def substitute(s,truth_table, VARS):
    for v,t in zip(VARS,truth_table):
        s = s.replace(v,t)
    return s

def check_statements(A1,A2):  
    VARS = set()
    maths    = pypar.oneOf("( ! = | & )")
    keywords = pypar.oneOf("and or")
    variable = pypar.Word(pypar.alphanums)
    variable.setParseAction(lambda x: VARS.add(x[0]))
    grammar  = pypar.OneOrMore(maths | keywords | variable)

    # Determine the variable names
    grammar.parseString(A1)
    grammar.parseString(A2)

    A1 = python_equiv(A1)
    A2 = python_equiv(A2)

    bool_vals = map(str, [False,True])

    for table in itertools.product(bool_vals,repeat=len(VARS)):
        T1 = substitute(A1,table,VARS)
        T2 = substitute(A2,table,VARS)
        if eval(T1) != eval(T2):
            print "FAIL AT ", table,
            return False

    print "Statements equiv:",

    return True


# Original example
A1 = '''((op1 != v1) || ((op2 != v2) || (op3 != v3)))'''
A2 = '''((op2 != v2) ||  (op1 != v1) || (op3 != v3))'''
print check_statements(A1,A2)

# Example with a failure
A1 = '''((op1 != v1) || ((op2 != v2) || (op3 != v3)))'''
A2 = '''((op2 != v2) ||  (op1 != v1) && (op3 != v3))'''
print check_statements(A1,A2)

Gives as output:

Statements equiv: True
FAIL AT  ('False', 'False', 'False', 'False', 'False', 'True') False