SolidCode / SolidPython

A python frontend for solid modelling that compiles to OpenSCAD
1.1k stars 172 forks source link

Using z3 to solve constraints? #135

Closed songcq closed 4 years ago

songcq commented 4 years ago

Hi, I'm using z3py solver in my projects to solve 2D constraints like

and we should be able to combine them in arbitrary way. They're useful for finding tangent line/circle and defining fillets (concave fillets can not be constructed using minkowski).

With z3 solver these problems become much easier solve. I'm considering to extract my code into a module and submit to SolidPython, but that means SolidPython will depend on z3. Is that dependency fine or something we should try to avoid?

Thanks

etjones commented 4 years ago

I'm definitely open to adding dependencies if they add new capacities. It sounds like z3py might do that for sure.

I think there's an easier solution for your particular fillet issues (example below), but I'm a little intrigued by the z3py system. Do you have any more examples of how we might use it?

In your specific example though, have you looked at offset() at all? I was working on some filleted stuff recently and realized it is much more capable than I thought.

Here's an example of a concave 2D fillet:

#! /usr/bin/env python

from solid import *
SEGMENTS = 48

def concave_fillet():
    points = (
        (0,0),
        (1,0),
        (1,1),
        (0.5, 0.25),
        (0,1)
    )

    fillet_rad = 0.1
    concave = offset(r=-fillet_rad)(
        offset(r=fillet_rad)(
            polygon(points)
        )
    )

    return concave

if __name__ == '__main__':
    a = concave_fillet()
    out_path = scad_render_to_file(a, file_header='$fn = %s;' % SEGMENTS, include_orig_code=True)
    print(f'Wrote file to {out_path}')
songcq commented 4 years ago

Thank you, your method using offset worked for me. Btw should offset take a segments arguments? The global SEGMENTS doesn't work for me.

I'll keep playing with z3 and maybe show you some more examples in the future.

etjones commented 4 years ago

I’m glad that’s working for you! I’ll have to look into the segments issue. SolidPython’s offset() doesn’t take an explicit segments argument, but it should. In general, the clause file_header='$fn = %s;' % SEGMENTS in the scad_render_to_file() call should enforce the fineness of curves, but I’ll run the attached code again and verify that.

songcq commented 4 years ago

I tried to manually add $fn=100 to the offset in generated openscad code and it worked. Though it only makes sense for r is specified for offset.

For SEGMENTS, my workaround is to manually prepend $fn=100 to generated scad file.

On Mon, Feb 10, 2020 at 11:34 PM Evan Jones notifications@github.com wrote:

Closed #135 https://github.com/SolidCode/SolidPython/issues/135.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/SolidCode/SolidPython/issues/135?email_source=notifications&email_token=ABDX2EM7YJHMDZRJJNGK6NTRCFX2DA5CNFSM4KSB5JKKYY3PNVWWK3TUL52HS4DFWZEXG43VMVCXMZLOORHG65DJMZUWGYLUNFXW5KTDN5WW2ZLOORPWSZGOWQZIITQ#event-3023209550, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABDX2EJPBFZCG7KNNZOOGP3RCFX2DANCNFSM4KSB5JKA .