Могу ли я прочитать файл SMT2 в решатель через интерфейс z3 C++?

Question

У меня проблема, когда код z3, встроенный в более крупную систему, не находит решение для определенного набора ограничений (добавленных через интерфейс C++), несмотря на довольно длительные таймауты. Когда я сбрасываю ограничения на файл (используя метод to_smt2() на решателе, перед вызовом check()) и запускает файл через автономный исполняемый файл z3, он решает систему примерно через 4 секунды (возвращение сидит). Для чего это стоит, файл имеет длину 476 587 строк, поэтому довольно большой набор ограничений.

Есть ли способ, чтобы я мог прочитать этот файл обратно в встроенный решатель с помощью интерфейса C++, заменив существующие ограничения, чтобы узнать, может ли встроенная версия решить, начиная с той же начальной точки, что и автономный решатель? (По сути, как я мог создать соответствующий метод from_smt2 (stream) в классе solver?)

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

Дальнейшее примечание: похоже, что у другого пользователя возникают аналогичные проблемы here. В отличие от этого пользователя, моя проблема использует все битовые векторы, и единственным неизвестным результатом является тот, что из встроенного кода. Есть ли способ вызвать (get-info: reason-unknown) из интерфейса C++, как предлагается там, чтобы выяснить, почему проблема с встроенной версией?

Answer 1

Вы можете использовать метод «solver :: reason_unknown()» для получения объяснений отказа поиска. Существуют методы для разбора файлов и строк в одном выражении. В случае набора утверждений выражение представляет собой конъюнкцию. Возможно, полезно добавить такой метод непосредственно в класс решателя для удобства. Было бы:

void from_smt2_string(char const* smt2benchmark) { 
     expr fml = ctx().parse_string(smt2benchmark); 
     add(fml); 
    } 

Так что, если вы напишете его вне класса решателя вам нужно:

 expr fml = solver.ctx().parse_string(smt2benchmark); 
     solver.add(fml);