# simple-program-synthesis

**Repository Path**: rpgszj2019/simple-program-synthesis

## Basic Information

- **Project Name**: simple-program-synthesis
- **Description**: 程序分析技术 课程 大作业：简易程序综合
- **Primary Language**: Python
- **License**: Not specified
- **Default Branch**: master
- **Homepage**: None
- **GVP Project**: No

## Statistics

- **Stars**: 1
- **Forks**: 2
- **Created**: 2019-12-16
- **Last Updated**: 2022-12-27

## Categories & Tags

**Categories**: Uncategorized

**Tags**: None

## README

# 程序分析技术课程大作业：简易程序综合

## 说明

一个简易的SyGuS（syntax-guided synthesis）问题求解器。

纯搜索实现（对于“数组reduce”类问题有优化），目前只能求解一些简单的程序综合（program synthesis）问题。

## 依赖
```bash
pip install z3-solver
```

## 使用方法
```bash
python main.py <specification file>
```

输入格式为[SyGuS-IF 1.0](https://sygus.org/language_1.0/)，只支持`LIA`类型的问题。

以下是一个示例问题`max2`：
```scheme
;; The background theory is linear integer arithmetic
(set-logic LIA)

;; Name and signature of the function to be synthesized
(synth-fun max2 ((x Int) (y Int)) Int

    ;; Define the grammar for allowed implementations of max2
    ((Start Int (x y 0 1
                 (+ Start Start)
                 (- Start Start)
                 (ite StartBool Start Start)))
    (StartBool Bool ((and StartBool StartBool)
                     (or StartBool StartBool)
                     (not StartBool)
                     (<= Start Start)
                     (= Start Start)
                     (>= Start Start))))
)

(declare-var x Int)
(declare-var y Int)

;; Define the semantic constraints on the function
(constraint (>= (max2 x y) x))
(constraint (>= (max2 x y) y))
(constraint (or (= x (max2 x y)) (= y (max2 x y))))

(check-synth)
```

一个可行的答案：
```scheme
(define-fun max2 ((x Int) (y Int)) Int (ite (>= x y) x y))
```