TryFor w Z3 nie przestaje sprawdzać po podanym limicie czasu

Question

Używam API .NET API Z3. Kiedy instancji solver pod numerem:

Solver s = ctx.MkSolver(ctx.TryFor(ctx.MkTactic("qflia"), TimeLimit)); 

i nadać mu timeLimit 60 sekund (60000 milisekund) dla niektórych modeli rachunku

s.Check() 

nie powróci po 60 sekundach. W przypadku niektórych modeli powraca kilka sekund później, co w moim przypadku nie stanowiłoby problemu, ale w przypadku niektórych modeli w ogóle się nie zwraca (anulowałem proces po 3 dniach).

Jak zmusić Z3, aby przestał sprawdzać po określonym limicie czasu?

Answer 1

Kombinator TryFor jest realizowany za pomocą flagi "anulowania". Nowa taktyka reaguje bardzo szybko i kończy się bardzo szybko po ustawieniu flagi "anulowania". Niestety, taktyka ogólnego przeznaczenia smt jest opakowaniem po rozwiązaniu ogólnego przeznaczenia. Ten solver ogólnego przeznaczenia nie reaguje zbyt szybko. Może się "zagubić" w kilku kluczowych miejscach: tworzenie kwantyfikatora, Simplex itp. Taktyka qflia jest zbudowana na bazie smt i wielu innych taktyk. Odkąd próbujesz rozwiązać problemy bez kwantyfikatorów. Zakładam, że taktyka smt znajduje się w pętli wewnątrz modułu Simplex. Moduł Simplex w taktyce smt jest zaimplementowany przy użyciu dowolnie wymiernych liczb wymiernych. Tak więc może to być bardzo czasochłonne dla nietrywialnych problemów liniowych rzeczywistych/całkowitych.

Nie można wiele zrobić, aby obejść ten problem. Jeśli naprawdę potrzebujesz silnej gwarancji w czasie działania, jedynym rozwiązaniem, jakie widzę, jest stworzenie oddzielnego procesu z uruchomieniem Z3 i zabicie go, gdy zajmie więcej czasu k sekund, aby rozwiązać problem.

Zgodnie z tym, przyszłe wersje Z3 będą miały kompletny nowy moduł arytmetyczny. Ten nowy moduł (podobnie jak nowa taktyka) zakończy się szybko po ustawieniu flagi anulowania.