As a preparation for producing witnesses for nonlinear systems (from Spacer engine), we change the format of the invalidity witness. The new style is similar to what Eldarica prints out. The proof is a sequence of steps where each step is a derived fact (instantiation of an uninterpreted predicate with constants as the arguments). Moreover, we remember the indices for the premises of each derivation step and the edge that was used for this derivation step.
The validator has been updated to validate this new format. It also meant that we removed the distinction between Graph- and System- invalidity witness.
Unfortunately, we now require the corresponding ChcDirectedHyperGraph to validate InvalidityWitness, which means that we have to keep around a copy of the original graph, if we are making any transformation passes.
Maybe we will have to re-introduce a format for proof for normalized system in the future again. But I need to understand precisely the representation of the normalized system and how can we keep references to clauses in the system in the InvalidityWitness.
As a preparation for producing witnesses for nonlinear systems (from Spacer engine), we change the format of the invalidity witness. The new style is similar to what Eldarica prints out. The proof is a sequence of steps where each step is a derived fact (instantiation of an uninterpreted predicate with constants as the arguments). Moreover, we remember the indices for the premises of each derivation step and the edge that was used for this derivation step.
The validator has been updated to validate this new format. It also meant that we removed the distinction between Graph- and System- invalidity witness.
Unfortunately, we now require the corresponding ChcDirectedHyperGraph to validate InvalidityWitness, which means that we have to keep around a copy of the original graph, if we are making any transformation passes.
Maybe we will have to re-introduce a format for proof for normalized system in the future again. But I need to understand precisely the representation of the normalized system and how can we keep references to clauses in the system in the InvalidityWitness.