# Ats + z3

**URL:** <https://discourse.ats-lang.org/t/ats-z3/640>\
**Category:** Google Group\
**Created:** [June 6, 2015, 9:26pm UTC](https://discourse.ats-lang.org/t/ats-z3/640 "2015-06-06T21:26:03Z")\
**Posts on this page:** 13\
**Page:** 1

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [June 6, 2015, 9:26pm UTC](https://discourse.ats-lang.org/t/ats-z3/640/1 "2015-06-06T21:26:03Z")

</div>

I would like to bring people’s attention to the following ongoing project:

[https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/ATS-extsolve-z3](https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/ATS-extsolve-z3)

The basic idea is to use Z3 ([https://github.com/Z3Prover/z3](https://github.com/Z3Prover/z3)) to solve the  
constraints generated  
during ATS2-typechecking. I want to first thank Will Blair for his piloting  
work on this project. For more,  
please visit:

[http://www.illtyped.com/projects/patsolve/](http://www.illtyped.com/projects/patsolve/)

The Makefile in the following directory shows how to export constraints  
generated during typechecking  
a program in ATS:

[https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/ATS-extsolve-z3/TEST](https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/ATS-extsolve-z3/TEST)

Basically, it goes like this:

patsopt -tc --constraint-export -o foo\_dats\_constraint.json -d foo.dats

for exporting the generated constraints. And the exported constraints can  
be solved like this:

patsolve\_z3 -i foo\_dats\_constraint.json

where patsolve\_z3 is the main command generated from compiling the  
ATS-extsolve-z3 project.

Patsolve\_z3 starts to be functioning as of now. However, this is really  
just the very beginning and  
there will be a lot more coming gradually. With Z3, ATS is expected to  
reach a much higher level  
in terms of program verification.

Cheers!

–Hongwei

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [June 6, 2015, 11:01pm UTC](https://discourse.ats-lang.org/t/ats-z3/640/2 "2015-06-06T23:01:39Z")

</div>

> I would like to bring people’s attention to the following ongoing project:

[https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/ATS-extsolve-z3](https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/ATS-extsolve-z3)

> The basic idea is to use Z3 ([GitHub - Z3Prover/z3: The Z3 Theorem Prover](https://github.com/Z3Prover/z3)) to solve the  
> constraints generated  
> during ATS2-typechecking.

I did this kind of thing in Felix at one stage, using compiler stuff to emit  
user axioms and theorems in WHY format so WHY should then be  
run to invoke automatic theorem provers.

This added two more processes communicating with text that  
had to be parsed on both output an input and of course provers  
aren’t always fast, so it was done offline.

I eventually removed it because WHY was too experimental and kept  
changing, also getting hold of and configuring the external provers wasn’t  
too hard  
on Linux but on other platforms proved very difficult.

You will also have the tricky problem that the solvers aren’t quite aligned  
with what is actually required by your compiler.

Still, congratulations, I think this is the right way to go.  
Leveraging separate projects is tricky and the loss of control is worrying  
but in the end, a compiler writer simply cannot do everything.  
In the end, you have to delegate most of the library development too.  
And then, split the compiler into modules and delegate parts of that  
as well (eg optimisation, parsing, back end etc).

john skaller  
skaller@…  
[http://felix-lang.org](http://felix-lang.org)

---

<div class="post-metadata">

**Author:** ![William\_Blair](https://avatars.discourse-cdn.com/v4/letter/w/c68b51/32.png) [@William\_Blair](https://discourse.ats-lang.org/u/William_Blair)\
**Post date:** [June 13, 2015, 9:22pm UTC](https://discourse.ats-lang.org/t/ats-z3/640/3 "2015-06-13T21:22:29Z")

</div>

> > What do you mean with “Z3 crashed”?

In Z3’s C API, whenever you get an object you need to increase its  
reference count, and then decrease its reference count when you are  
finished with it. With my first prototype, I never decreased any reference  
counts so Z3 eventually ran out of memory and stopped with an “out of  
memory” error.Am Samstag, 13. Juni 2015 04:07:42 UTC-4 schrieb Yannick Duchêne:

> Le vendredi 12 juin 2015 17:26:57 UTC+2, William Blair a écrit :
> 
> > When I first worked on a prototype, all of Z3’s objects were non-linear  
> > and I didn’t try to manage resources. Eventually, type checking large  
> > programs consumed so much memory **Z3 crashed**. Fixing this issue was  
> > pretty straightforward. After I made Z3 objects linear and described how  
> > the API produced and consumed objects, the type checker specified every  
> > place where memory could be leaked.
> 
> What do you mean with “Z3 crashed”? Do you mean it suddenly stopped  
> it‑self or do you mean it was stopped after it tried to execute invalid  
> instructions?

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [June 8, 2015, 6:14am UTC](https://discourse.ats-lang.org/t/ats-z3/640/4 "2015-06-08T06:14:42Z")

</div>

I made significant progress today regarding the ATS-extsolve-z3  
project. Now the generated command patsolve\_z3 can be used to  
compile ATSLIB/prelude and ATSLIB/libats.

Following is an example that cannot be handled by patsopt but can be  
by patsolve\_z3. Note that ‘fact’ is introduced as a “foreign” static  
function  
in this example.

At this stage, I do not really have a good feel as to what can or cannot be  
proven in Z3. However, I do feel that Z3 is very flexible and can become a  
very powerful too if one knows how to use it properly.

Cheers!

( \*\*\*\*\*\* \*\*\*\*\*\* _)  
//  
stacst fact: int → int  
//  
(_ \*\*\*\*\*\* \*\*\*\*\*\* _)  
//  
extern  
praxi  
fact\_bas(): [fact(0)==1] void  
extern  
praxi  
fact\_ind{n:pos}(): [fact(n)==n_fact(n-1)] void  
//  
(\* \*\*\*\*\*\* \*\*\*\*\*\* _)  
//  
fun  
fact  
{n:nat}  
(n: int(n))  
: int(fact(n)) = let  
//  
fun  
loop  
{n:nat}  
{r:int} ..  
(  
n: int(n), r: int(r)  
) : int(fact(n)r) = (  
//  
if  
n = 0  
then let  
prval () = fact\_bas() in (r)  
end // end of [then]  
else let  
prval () = fact\_ind{n}() in loop(n-1, nr)  
end // end of [else]  
//  
) (_ end of [loop] \*)  
//  
in  
loop(n, 1)  
end // end of [fact]

(\* \*\*\*\*\*\* \*\*\*\*\*\* \*)On Saturday, June 6, 2015 at 5:26:03 PM UTC-4, gmhwxi wrote:

> I would like to bring people’s attention to the following ongoing project:
> 
> [https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/ATS-extsolve-z3](https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/ATS-extsolve-z3)
> 
> The basic idea is to use Z3 ([GitHub - Z3Prover/z3: The Z3 Theorem Prover](https://github.com/Z3Prover/z3)) to solve the  
> constraints generated  
> during ATS2-typechecking. I want to first thank Will Blair for his  
> piloting work on this project. For more,  
> please visit:
> 
> [http://www.illtyped.com/projects/patsolve/](http://www.illtyped.com/projects/patsolve/)
> 
> The Makefile in the following directory shows how to export constraints  
> generated during typechecking  
> a program in ATS:
> 
> [https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/ATS-extsolve-z3/TEST](https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/ATS-extsolve-z3/TEST)
> 
> Basically, it goes like this:
> 
> patsopt -tc --constraint-export -o foo\_dats\_constraint.json -d foo.dats
> 
> for exporting the generated constraints. And the exported constraints can  
> be solved like this:
> 
> patsolve\_z3 -i foo\_dats\_constraint.json
> 
> where patsolve\_z3 is the main command generated from compiling the  
> ATS-extsolve-z3 project.
> 
> Patsolve\_z3 starts to be functioning as of now. However, this is really  
> just the very beginning and  
> there will be a lot more coming gradually. With Z3, ATS is expected to  
> reach a much higher level  
> in terms of program verification.
> 
> Cheers!
> 
> –Hongwei

---

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [June 8, 2015, 8:07am UTC](https://discourse.ats-lang.org/t/ats-z3/640/5 "2015-06-08T08:07:14Z")

</div>

> At this stage, I do not really have a good feel as to what can or cannot be  
> proven in Z3. However, I do feel that Z3 is very flexible and can become a  
> very powerful too _if one knows how to use it properly._

Isn’t it entirely transparent from an ATS user point of view?

Also, will this become the default in the future? (the question may raise,  
if using Z3 makes so much difference)

---

<div class="post-metadata">

**Author:** ![john\_skaller](https://avatars.discourse-cdn.com/v4/letter/j/58956e/32.png) [@john\_skaller](https://discourse.ats-lang.org/u/john_skaller)\
**Post date:** [June 8, 2015, 9:43am UTC](https://discourse.ats-lang.org/t/ats-z3/640/6 "2015-06-08T09:43:42Z")

</div>

> I made significant progress today regarding the ATS-extsolve-z3  
> project. Now the generated command patsolve\_z3 can be used to  
> compile ATSLIB/prelude and ATSLIB/libats.

Curious are you using direct C interface or LIB-SMT language text?

john skaller  
[ska...@users.sourceforge.net](mailto:ska...@users.sourceforge.net)  
[http://felix-lang.org](http://felix-lang.org)

---

<div class="post-metadata">

**Author:** ![William\_Blair](https://avatars.discourse-cdn.com/v4/letter/w/c68b51/32.png) [@William\_Blair](https://discourse.ats-lang.org/u/William_Blair)\
**Post date:** [June 12, 2015, 3:26pm UTC](https://discourse.ats-lang.org/t/ats-z3/640/7 "2015-06-12T15:26:57Z")

</div>

> Curious are you using direct C interface or LIB-SMT language text?

Right now, it uses the C API for Z3. You could have the constraint solver  
generate smt-lib text without too much trouble though.

Since Z3 requires the programmer manage reference counting for all of its  
objects, the C api can be difficult to use. In the constraint solver, all  
these objects are linear, so the typechecker can make the process a lot  
easier.

When I first worked on a prototype, all of Z3’s objects were non-linear and  
I didn’t try to manage resources. Eventually, type checking large programs  
consumed so much memory Z3 crashed. Fixing this issue was pretty  
straightforward. After I made Z3 objects linear and described how the API  
produced and consumed objects, the type checker specified every place where  
memory could be leaked.

I think this process of program refinement is a great example of how linear  
types can simplify working with low level interfaces.Am Montag, 8. Juni 2015 05:44:18 UTC-4 schrieb John Skaller:

> On 08/06/2015, at 4:14 PM, gmhwxi wrote:
> 
> > I made significant progress today regarding the ATS-extsolve-z3  
> > project. Now the generated command patsolve\_z3 can be used to  
> > compile ATSLIB/prelude and ATSLIB/libats.
> 
> Curious are you using direct C interface or LIB-SMT language text?
> 
> –  
> john skaller  
> [ska...@users.sourceforge.net](mailto:ska...@users.sourceforge.net) \<javascript:\>  
> [http://felix-lang.org](http://felix-lang.org)

---

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [June 13, 2015, 8:07am UTC](https://discourse.ats-lang.org/t/ats-z3/640/8 "2015-06-13T08:07:42Z")

</div>

> When I first worked on a prototype, all of Z3’s objects were non-linear  
> and I didn’t try to manage resources. Eventually, type checking large  
> programs consumed so much memory **Z3 crashed**. Fixing this issue was  
> pretty straightforward. After I made Z3 objects linear and described how  
> the API produced and consumed objects, the type checker specified every  
> place where memory could be leaked.

What do you mean with “Z3 crashed”? Do you mean it suddenly stopped it‑self  
or do you mean it was stopped after it tried to execute invalid  
instructions?

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [June 8, 2015, 9:24pm UTC](https://discourse.ats-lang.org/t/ats-z3/640/9 "2015-06-08T21:24:08Z")

</div>

I updated ATS2-C9-install.sh:

> <https://gist.github.com/githwxi/7e31f4fd4df92125b73c>

which shows how patsolve\_z3 can be built on Ubuntu  
(assuming that Z3 is already installed).On Saturday, June 6, 2015 at 5:26:03 PM UTC-4, gmhwxi wrote:

> I would like to bring people’s attention to the following ongoing project:
> 
> [https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/ATS-extsolve-z3](https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/ATS-extsolve-z3)
> 
> The basic idea is to use Z3 ([GitHub - Z3Prover/z3: The Z3 Theorem Prover](https://github.com/Z3Prover/z3)) to solve the  
> constraints generated  
> during ATS2-typechecking. I want to first thank Will Blair for his  
> piloting work on this project. For more,  
> please visit:
> 
> [http://www.illtyped.com/projects/patsolve/](http://www.illtyped.com/projects/patsolve/)
> 
> The Makefile in the following directory shows how to export constraints  
> generated during typechecking  
> a program in ATS:
> 
> [https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/ATS-extsolve-z3/TEST](https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/ATS-extsolve-z3/TEST)
> 
> Basically, it goes like this:
> 
> patsopt -tc --constraint-export -o foo\_dats\_constraint.json -d foo.dats
> 
> for exporting the generated constraints. And the exported constraints can  
> be solved like this:
> 
> patsolve\_z3 -i foo\_dats\_constraint.json
> 
> where patsolve\_z3 is the main command generated from compiling the  
> ATS-extsolve-z3 project.
> 
> Patsolve\_z3 starts to be functioning as of now. However, this is really  
> just the very beginning and  
> there will be a lot more coming gradually. With Z3, ATS is expected to  
> reach a much higher level  
> in terms of program verification.
> 
> Cheers!
> 
> –Hongwei

---

<div class="post-metadata">

**Author:** ![Yannick\_Duchene](https://avatars.discourse-cdn.com/v4/letter/y/b77776/32.png) [@Yannick\_Duchene](https://discourse.ats-lang.org/u/Yannick_Duchene)\
**Post date:** [June 7, 2015, 3:44am UTC](https://discourse.ats-lang.org/t/ats-z3/640/10 "2015-06-07T03:44:08Z")

</div>

> I would like to bring people’s attention to the following ongoing project:
> 
> [https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/ATS-extsolve-z3](https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/ATS-extsolve-z3)
> 
> The basic idea is to use Z3 ([GitHub - Z3Prover/z3: The Z3 Theorem Prover](https://github.com/Z3Prover/z3)) to solve the  
> constraints generated  
> during ATS2-typechecking. I want to first thank Will Blair for his  
> piloting work on this project. For more,  
> please visit:  
> […]

Given that it will be used for ATS, it’s worth to point the license seems  
to have changed and no more has the limitation of “not allowed to design  
commercial applications” (and an outrageous pricing otherwise) as it was  
before. I just noticed it’s now MIT licensed.

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [June 8, 2015, 3:43pm UTC](https://discourse.ats-lang.org/t/ats-z3/640/11 "2015-06-08T15:43:58Z")

</div>

> > Isn’t it entirely transparent from an ATS user point of view?

Actually, I feel it is going to be the opposite.

In general, constraint-solving is undecidable. So one may need to  
generate both constraints and constraint-solving strategies (which  
may depend on a particular constraint-solver).On Monday, June 8, 2015 at 4:07:14 AM UTC-4, Yannick Duchêne wrote:

> Le lundi 8 juin 2015 08:14:42 UTC+2, gmhwxi a écrit :
> 
> > At this stage, I do not really have a good feel as to what can or cannot  
> > be  
> > proven in Z3. However, I do feel that Z3 is very flexible and can become a  
> > very powerful too _if one knows how to use it properly._
> 
> Isn’t it entirely transparent from an ATS user point of view?
> 
> Also, will this become the default in the future? (the question may raise,  
> if using Z3 makes so much difference)

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [June 7, 2015, 6:09pm UTC](https://discourse.ats-lang.org/t/ats-z3/640/12 "2015-06-07T18:09:00Z")

</div>

> Thanks for sharing your insights.
> 
> By pure coincidence, implementing a constraint-solver for ATS based on Z3  
> is straightforward.

Probably more “synchronicity” than coincidence 🙂

> The real focus is  
> to find a reasonable way to support a style of constraint-solving that is  
> open-ended:  
> The programmer should be allowed to not only extend the statics of ATS  
> with additional  
> sorts and (static) functions symbols but also supply constraint-solvers  
> that can handle the  
> newly introduced functional symbols.

That sounds very hard.

Technically, it is probably not so difficult. But to get a synergistic  
integration linguistically should prove an interesting challenge!

john skaller  
skaller@…  
[http://felix-lang.org](http://felix-lang.org)

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [June 7, 2015, 6:29am UTC](https://discourse.ats-lang.org/t/ats-z3/640/13 "2015-06-07T06:29:30Z")

</div>

Thanks for sharing your insights.

By pure coincidence, implementing a constraint-solver for ATS based on Z3  
is straightforward. This is due to Z3 supporting a style of solver which I  
would  
refer to as being “stack-based”. This style precisely matches the way in  
which  
constraints in ATS are represented.

However, replacing the built-in constraint-solver of ATS with another  
Z3-based  
solver is really a by-product of the project of ATS-extsolve-z3. The real  
focus is  
to find a reasonable way to support a style of constraint-solving that is  
open-ended:  
The programmer should be allowed to not only extend the statics of ATS with  
additional  
sorts and (static) functions symbols but also supply constraint-solvers  
that can handle the  
newly introduced functional symbols.

Cheers!On Sat, Jun 6, 2015 at 6:44 PM, john skaller \<skaller@…\> wrote:

> On 07/06/2015, at 7:27 AM, Hongwei Xi wrote:
> 
> > I would like to bring people’s attention to the following ongoing  
> > project:
> 
> [https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/ATS-extsolve-z3](https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/ATS-extsolve-z3)
> 
> > The basic idea is to use Z3 ([GitHub - Z3Prover/z3: The Z3 Theorem Prover](https://github.com/Z3Prover/z3)) to solve  
> > the constraints generated  
> > during ATS2-typechecking.
> 
> I did this kind of thing in Felix at one stage, using compiler stuff to  
> emit  
> user axioms and theorems in WHY format so WHY should then be  
> run to invoke automatic theorem provers.
> 
> This added two more processes communicating with text that  
> had to be parsed on both output an input and of course provers  
> aren’t always fast, so it was done offline.
> 
> I eventually removed it because WHY was too experimental and kept  
> changing, also getting hold of and configuring the external provers wasn’t  
> too hard  
> on Linux but on other platforms proved very difficult.
> 
> You will also have the tricky problem that the solvers aren’t quite aligned  
> with what is actually required by your compiler.
> 
> Still, congratulations, I think this is the right way to go.  
> Leveraging separate projects is tricky and the loss of control is worrying  
> but in the end, a compiler writer simply cannot do everything.  
> In the end, you have to delegate most of the library development too.  
> And then, split the compiler into modules and delegate parts of that  
> as well (eg optimisation, parsing, back end etc).
> 
> –  
> john skaller  
> skaller@…  
> [http://felix-lang.org](http://felix-lang.org)