Проверьте, эквивалентны ли два "простых" "оператора if" в C

У меня есть "если утверждения" из двух разных источников, которые пытаются реализовать одно и то же условие, возможно, по-разному. "Операторы if" - это C. Если это вообще возможно, мне нужен скрипт на python, который может решить, эквивалентны ли пары условий или нет. Основной пример:

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

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

Разумеется, разрешен любой оператор, вызовы функций и, конечно, круглые скобки.

Любые идеи приветствуются.

Редактировать 1: вызовы функций не имеют побочных эффектов.

Источник

2 ответа

Решение

Здесь дело в том, что проблема может (или не может) быть NP-полной, но если это не входит во внутренний цикл чего-то важного (а число переменных невелико), создайте всю таблицу истинности! Это очень легко сделать. Очевидно, он растет как 2^n, но для малых n это вполне выполнимо. Как и в комментариях, я предполагаю, что вызовы функций не имеют побочных эффектов и просто выводят True или же False,

Я опубликовал пример макета, который решает вашу заявленную проблему, адаптируется по мере необходимости. Я полагаюсь на синтаксический анализатор питонов для обработки оценки выражения.

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)

Дает в качестве вывода:

Statements equiv: True
FAIL AT  ('False', 'False', 'False', 'False', 'False', 'True') False
Источник

Для этого вам необходим анализ потока управления, чтобы определить, имеют ли два условия одинаковую зависимость управления (в противном случае они не выполняются в одном и том же контексте данных), полный анализ потока данных, включая точечный анализ кода C, -эффектный анализ функций, возможность обратного среза от корня условия до листьев выражения при вызовах функций, а затем логическое сопоставление эквивалентности, которое учитывает семантику C (например, короткое замыкание, переполнение, ...)

Это далеко за пределы того, что вы получаете от синтаксического анализатора Си.

Источник
Другие вопросы по тегам