[프로그램합성] 해당 함수와 동일한 함수 합성하기

해당 함수와 하는일은 같지만, 

간단한 함수를 원할 때

합성을 이용하여 만들어 낼수 있다.

 

일단 sygus 포맷을 사용한다.

 

; 참고 링크 : https://github.com/SyGuS-Org/benchmarks/blob/5ccf14c9040ddd749f237dc6d40b79438effedff/lib/General_Track/from_2018/parity-AIG-d1.sl
; how to run :  /home/wslee/utils/CVC4/cvc4 --lang=sygus --no-checking --no-interactive --dump-synth --default-dag-thresh=0 basic.sl 
(set-logic BV)

(define-fun watf ( (a (BitVec 64)) (b (BitVec 64)) ) (BitVec 64)
  (bvadd a b)) 
; wat 파일에 표기된 함수 적기

(synth-fun synf ( (a (BitVec 64)) (b (BitVec 64)) ) (BitVec 64))

; 합성할 함수 적기
(declare-var a (BitVec 64))
(declare-var b (BitVec 64))

(constraint (= (watf a b) (synf a b)))
; wat에 적힌 함수와 합성할 함수는 똑같은 일을 해야한다.

(check-synth)

지금은 기존에 원하는 해당함수가 매우 간단하기 때문에

synf 또한 똑같이 나오지만, 원한다면 watf 의 함수 내용을 바꾸어서

커스터 마이징이  가능하다.

; 합성 결과
(define-fun synf ((a (BitVec 64)) (b (BitVec 64))) (BitVec 64) (bvadd a b))