Method parseSMTLIB2String

src/api/java/Context.java:3010–3025

Parse the given string using the SMT-LIB2 parser. @return A conjunction of assertions. If the string contains push/pop commands, the set of assertions returned are the ones in the last scope level.

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

     * last scope level.
     **/
    public BoolExpr[] parseSMTLIB2String(String str, 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.parseSmtlib2String(nCtx(),
                str, AST.arrayLength(sorts), Symbol.arrayToNative(sortNames),
                AST.arrayToNative(sorts), AST.arrayLength(decls),
                Symbol.arrayToNative(declNames), AST.arrayToNative(decls)));
        return v.ToBoolExprArray();
    }

    /**
     * Parse the given file using the SMT-LIB2 parser.