search

usi-verification-and-security / golem

Solver for Constrained Horn Clauses
MIT License
34 stars 7 forks source link

Engines: Refactor computation of witnesses for transition systems #33

Closed blishko closed 1 year ago

blishko commented 1 year ago

This refactoring prepares the code for transformation of general linear CHC system to a transition system. The plan is that there will be no CHC graph corresponding to a transition system, but we go to directly to our inner TS representation. For this reason, we refactor the methods so they do not require both representation of a transition system.

To support witness production, we add a simple wrapper for a witness for our inner TS representation.

blishko commented 1 year ago

I need the separation of the concepts for the transformation that I want to implement. Basically, I need a witness for a transition system without a ChcDirectedGraph, which is not possible in current implementation.

If the functions would be joined, then I would have to call the translation method on every return statement, here there is only one invocation.