Support for solving constraints on reals

gmhwxi · June 23, 2016, 5:51pm

I have recently added support for generating constraints on reals in ATS.

The generated constraints can be exported for solving via Z3:

https://github.com/githwxi/ATS-Postiats-contrib/blob/master/projects/MEDIUM/ATS-extsolve-z3/

Here is an example verifying the two solutions to a quadratic equation:

https://github.com/githwxi/ATS-Postiats-contrib/blob/master/projects/MEDIUM/ATS-extsolve-z3/TEST/quadratic.dats

There are a few lines in the following script showing how patsolve_z3 can
be built:

github.com

ats-lang/ats-lang.github.io/blob/master/SCRIPT/C9-ATS2-install-cs520-z3.sh

#!/usr/bin/env sh

######
#
# A shell script for
# installing ATS-Postiats + utils
#
# This is mainly for teaching CS520
#
######
#
# Author: Hongwei Xi
# Authoremail: gmhwxiATgmailDOTcom
#
######

sudo apt-get update
#
# Installing gcc
# sudo apt-get install -y gcc

This file has been truncated. show original

Cheers!

–Hongwei

Topic		Replies	Views
Ats + z3 Google Group	12	569	June 13, 2015
Patsolve_smt2 Google Group	1	427	June 26, 2016
Ats2-0.2.0 Google Group	7	498	June 13, 2015
Quantifed constraints Google Group	12	561	June 16, 2015
ATS2-0.2.1 released Google Group	0	280	July 12, 2015

Support for solving constraints on reals

Related topics