mirror of
https://github.com/Z3Prover/z3
synced 2025-04-26 10:35:33 +00:00
Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt
This commit is contained in:
commit
181911463e
9 changed files with 75 additions and 52 deletions
|
@ -2621,7 +2621,7 @@ public class Context implements AutoCloseable {
|
|||
* @return A conjunction of assertions in the scope (up to push/pop) at the
|
||||
* end of the string.
|
||||
**/
|
||||
public BoolExpr parseSMTLIB2String(String str, Symbol[] sortNames,
|
||||
public BoolExpr[] parseSMTLIB2String(String str, Symbol[] sortNames,
|
||||
Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
|
||||
|
||||
{
|
||||
|
@ -2633,17 +2633,18 @@ public class Context implements AutoCloseable {
|
|||
if (csn != cs || cdn != cd) {
|
||||
throw new Z3Exception("Argument size mismatch");
|
||||
}
|
||||
return (BoolExpr) Expr.create(this, Native.parseSmtlib2String(nCtx(),
|
||||
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.
|
||||
* @see #parseSMTLIB2String
|
||||
**/
|
||||
public BoolExpr parseSMTLIB2File(String fileName, Symbol[] sortNames,
|
||||
public BoolExpr[] parseSMTLIB2File(String fileName, Symbol[] sortNames,
|
||||
Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
|
||||
|
||||
{
|
||||
|
@ -2653,11 +2654,12 @@ public class Context implements AutoCloseable {
|
|||
int cd = AST.arrayLength(decls);
|
||||
if (csn != cs || cdn != cd)
|
||||
throw new Z3Exception("Argument size mismatch");
|
||||
return (BoolExpr) Expr.create(this, Native.parseSmtlib2File(nCtx(),
|
||||
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();
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue