Z3, C ++: освобожденный указатель не выделен - PullRequest
Новая
       6

Z3, C ++: освобожденный указатель не выделен

0 голосов
/ 27 августа 2018

Я решил использовать Z3 с C ++ и установил последнюю версию из git.При попытке выполнить пример git (следующий код является упрощенным примером) 

#include "z3++.h"
#include <iostream>
using namespace z3;
using namespace std;

int main() {
    context c;
    expr x = c.bool_const("x");
    expr y = c.bool_const("y");
    expr conjunction = (!(x && y)) == (!x|| !y);
    solver s(c);

    s.add(!conjunction);
    cout << s << "\n";
    cout << s.to_smt2() << "\n";
    switch (s.check()) {
        case unsat:   std::cout << "de-Morgan is valid\n"; break;
        case sat:     std::cout << "de-Morgan is not valid\n"; break;
        case unknown: std::cout << "unknown\n"; break;
    }
    return 0;
}

Я мог бы получить этот результат. 

(declare-fun y () Bool)
(declare-fun x () Bool)
(assert (not (= (not (and x y)) (or (not x) (not y)))))

;
(set-info :status unknown)
(declare-fun y () Bool)
(declare-fun x () Bool)
(assert
 (not (= (not (and x y)) (or (not x) (not y)))))
(check-sat)

de-Morgan is valid

Но я получил эту ошибку. 

a.out(92870,0x7fff9182c380) malloc: *** error for object 0x7f7fdc6217f8: pointer being freed was not allocated
*** set a breakpoint in malloc_error_break to debug
Abort trap: 6

Из этого выяснилось, что эта ошибка произошла после завершения программы.Мы также обнаружили, что эта ошибка возникает при обращении к уже выпущенному конструктору, но мы не видим такой точки в этом примере.

Благодарю тех, кто является экспертом.

Ответы [ 2 ]

0 голосов
/ 27 августа 2018

С точки зрения C ++ вы, кажется, делаете все правильно.Кроме того, вы скопировали непосредственно из Z ++ example.cpp .

ПРЕДЛОЖЕНИЕ:

Даже если это не должно иметь значение ...пожалуйста попробуйте это:

a) скопируйте свой код OUT из main() и в отдельную функцию, demorgan()

b) Завершите ваш звонок с "main () "into" demorgan () "из блока try {} catch()

Или даже лучше ... попробуйте запустить весь example.cpp как есть, без изменений.

Сбой всего остального, один (глупый!) обходной путь: context *c = new context();: вместо «auto» попробуйте «new» и посмотрите, что произойдет.

Q: Какой компилятор вы используете?На какой платформе вы строите?

0 голосов
/ 27 августа 2018

Я думаю, что лучший способ начать - это изучить файл примера cpp * Z3 и постепенно создавать примеры "Hello Z3 world".Просто зайдите в каталог build и запустите make examples.как только make успешно завершится, просто запустите ./cpp_example.Я вижу, что ваш пример взят из их первой функции demorgan, поэтому, если она не работает для вас, возможно, лучше опубликовать ее в их выпусках .

РЕДАКТИРОВАТЬ:

Я только что проверил это, и он отлично работает.Может, расскажете, как вы собрали свой пример?

...