main.go

package main

import (
	"fmt"
	"strconv"

	"github.com/mitchellh/go-z3"
)

func main() {
	config := z3.NewConfig()
	ctx := z3.NewContext(config)
	config.Close()
	defer ctx.Close()

	// Logic:
	// x400 * 2 = x800
	// x800 - x400 = 400

	// Create the solver
	s := ctx.NewSolver()
	defer s.Close()

	// Vars
	x400 := ctx.Const(ctx.Symbol("x400"), ctx.IntSort())
	x800 := ctx.Const(ctx.Symbol("x800"), ctx.IntSort())

	// x400 * 2 = x800
	s.Assert(x400.Mul(ctx.Int(2, ctx.IntSort())).Eq(x800))

	// x800 - x400 = 400
	s.Assert(x800.Sub(x400).Eq(ctx.Int(400, ctx.IntSort())))

	if v := s.Check(); v != z3.True {
		fmt.Println("Unsolveable")
		return
	}

	// Get the resulting model:
	m := s.Model()
	assignments := m.Assignments()
	m.Close()

	v400, _ := strconv.Atoi(assignments["x400"].String())
	v800, _ := strconv.Atoi(assignments["x800"].String())
	ss := "低い"
	if v800 > v400 {
		ss = "高い"
	}
	fmt.Printf("年収800万は年収400万よりも%s\n", ss)
}