Method parseSMTLIB2File

src/api/java/Context.java:3031–3046

Parse the given file using the SMT-LIB2 parser. @see #parseSMTLIB2String

(String fileName, Symbol[] sortNames,
            Sort[] sorts, Symbol[] declNames, FuncDecl<?>[] decls)

     * @see #parseSMTLIB2String
     **/
    public BoolExpr[] parseSMTLIB2File(String fileName, Symbol[] sortNames,
            Sort[] sorts, Symbol[] declNames, FuncDecl<?>[] decls)
    {
        int csn = Symbol.arrayLength(sortNames);
        int cs = Sort.arrayLength(sorts);
        int cdn = Symbol.arrayLength(declNames);
        int cd = AST.arrayLength(decls);
        if (csn != cs || cdn != cd)
            throw new Z3Exception("Argument size mismatch");
        ASTVector v = new ASTVector(this, Native.parseSmtlib2File(nCtx(),
                fileName, AST.arrayLength(sorts),
                Symbol.arrayToNative(sortNames), AST.arrayToNative(sorts),
                AST.arrayLength(decls), Symbol.arrayToNative(declNames),
                AST.arrayToNative(decls)));
        return v.ToBoolExprArray();
    }

    /**
     * Creates a new Goal.