Z3 Native Trouble

Jan 10, 2014 at 11:14 PM
I have 2 questions about the Z3 native interface.

1) It seems every 300 calls or so I get thrown the error "terminate called, throwing an exception" and Z3 is no longer able to progress. I'm pretty sure the error is coming from within the source and not the API since I've tried to catch the exception and nothing happens. Unfortunately, it's been too intermittent for me to actually see what's going on in a debug mode. Unlike in previous posts about this problem, I'm not using any timeouts.

2) It seems after an even longer time, ~500 calls, the responsiveness really starts to slow down. I think it's a garbage collection problem because when I use the actual z3 program as a separate process, I don't experience this slowdown. After a little bit, the process invocation is actually faster than the native interface. I'm disposing of every object I can think of but it's still really struggling.

Example Code:
cfg = new HashMap<String, String>();
cfg.put("model", "true");
Context ctx = new Context(cfg);

BoolExpr expr = ...

Model model = check(ctx, expr, Status.SATISFIABLE); //From the test example provided
expr.dispose();
ctx.dispose();
Point p = parseModel(model);
if(model != null){
    model.dispose();
}
return p;
Has anyone experienced either of these before?
Coordinator
Jan 16, 2014 at 3:46 PM
Thanks for reporting this issue! This is a really hard one to debug, but generally I can say that some degree of garbage collection problems is expected, because the .NET GC doesn't know about the actual size of the native objects hidden behind the .NET objects (each of which only holds a pointer and therefore looks tiny). If this is indeed the problem, then adding calls to GC.Collect() in the right places might fix the problem for you, although, I would expect you to see some out of memory exceptions too.

Since you get only "terminate called, throwing an exception", it may well be that you're hitting a segfault or some other critical problem in the native part of Z3. These can be hard to catch (but it can be done if your Visual Studio is set up for managed+native debugging and you have a debug DLL of Z3). Do you have any complete example that reliably triggers this behavior?
Jan 17, 2014 at 4:56 PM
Edited Jan 17, 2014 at 4:58 PM
Thanks for getting back to me. I think that I managed to fix it, at least I haven't seen the error since and it is no longer dramatically slowing down. Instead of disposing of the context and the solver every time, they should remain throughout the life of the object, and only be disposed of when all of the solving is done. A new code sample that works is...
    class Z3Native{

        Context ctx;
        Solver solver;

        public Z3Native(){
            HashMap<String String> cfg = new HashMap<String, String>();
            cfg.put("model", "true");
        
            try{
                ctx = new Context(cfgModel);
                solver = ctx.mkSolver();
            }catch(Z3Exception e){
                e.printStackTrace();
            }
        }

        public Model sat(Tree tokensInQuery){
            BoolExpr expr = createExpression(ctx, tokensInQuery);
            Model model = (Model) check(ctx, expr, Status.SATISFIABLE, solver);

            expr.dispose();
            Point p = parseModel(model);
            if(model != null){
                model.dispose();
            }
            return p;
        }

        private Model check(Context ctx, BoolExpr f, Status sat, Solver s){
            try{
                s.push();
                s.add(f);

                if (s.check() != sat){
                    s.pop();
                    return null;
                }else if (sat == Status.SATISFIABLE){
                    Model ret = s.getModel();
                    s.pop();
                    return ret;
                }else{
                    throw Exception;
                }
            }catch(Exception e){
                e.printStackTrace();
            }
        }

        private BoolExpr createExpression(Context ctx, Tree tokensInQuery){
            //do stuff like
            if(tokensInQuery == AND){
                Expr left = createExpression(ctx, tokensInQuery.left());
                Expr right = createExpression(ctx, tokenInQuery.right());

                return ctx.mkAnd(left,  right)
            }

            ...

        }
    }