Using z3 to solve constraints?

[songcq]

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

• a circle has to go through a point
• a circle has to be tangent to some line
• a circle has to be tangent to another circle
• intersection points between lines, circles etc

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]

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]

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]

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]

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 ***@***.***> wrote: Closed #135 <#135>. — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#135?email_source=notifications&email_token=ABDX2EM7YJHMDZRJJNGK6NTRCFX2DA5CNFSM4KSB5JKKYY3PNVWWK3TUL52HS4DFWZEXG43VMVCXMZLOORHG65DJMZUWGYLUNFXW5KTDN5WW2ZLOORPWSZGOWQZIITQ#event-3023209550>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABDX2EJPBFZCG7KNNZOOGP3RCFX2DANCNFSM4KSB5JKA> .