Module Search

module Search: sig .. end

In this module, find the correct body of given Ast by iterative search

exception LoopOut

module WorklistBFS: sig .. end

val synthFuncByBFS : Ast.cmd list ->
       Ast.symbol ->
       Ast.sorted_var list ->
       Ast.sort ->
       Ast.term ->
       Ast.term list IntermediateTypes.TransitionMap.t -> Ast.term list -> string

val searchByBFS : Ast.cmd list -> IntermediateTypes.funcIngredient list -> 'a -> string

Find the synth-fun list body by BFS

Returns the sygus string which have correct body of synth-fun

ast : parsed sygus string

funcIngredients : function ingredient list of synth-fun list

costFunc : cost function

type heapterm =

`\|`	`Node of Ast.term * int`

module OrderedType: sig .. end

module Heap: BatHeap.Make(OrderedType)

val synthFuncByHeap : Ast.cmd list ->
       Ast.symbol ->
       Ast.sorted_var list ->
       Ast.sort ->
       Ast.term ->
       Ast.term list IntermediateTypes.TransitionMap.t ->
       Ast.term list -> (Ast.term -> Ast.term list -> int) -> string

val searchByHeap : Ast.cmd list ->
       IntermediateTypes.funcIngredient list ->
       (Ast.term -> Ast.term list -> int) -> string

Find the synth-fun list body by using heap

Returns the sygus string which have correct body of synth-fun

ast : parsed sygus string

funcIngredients : function ingredient list of synth-fun list

costFunc : cost function