solutionViaInterpolation

gapt.cutintro.solutionViaInterpolation

Solution finding algorithm for Π₁-cut-introduction based on the Duality algorithm for constrained Horn clause verification[1].

[1] K. L. McMillan, A. Rybalchenko, Solving Constrained Horn Clauses using Interpolation, technical report MSR-TR-2013-6, available at https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/MSR-TR-2013-6.pdf

Attributes

Source
solutionViaInterpolation.scala
Graph
Supertypes
class Object
trait Matchable
class Any
Self type

Members list

Value members

Concrete methods