mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-12 09:03:26 +00:00
Code Activity

java

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-03-14 09:04:08 -07:00
parent eb1122c5cb
commit 5e2723a16e
1 changed files with 6 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/api/java/Context.java
View file

@ -2543,14 +2543,15 @@ public class Context implements AutoCloseable {
/** /**
* Parse the given string using the SMT-LIB2 parser. * Parse the given string using the SMT-LIB2 parser.
* *
* @return A conjunction of assertions in the scope (up to push/pop) at the * @return A conjunction of assertions.
* end of the string. *
* If the string contains push/pop commands, the
* set of assertions returned are the ones in the
* last scope level.
**/ **/
public BoolExpr parseSMTLIB2String(String str, Symbol[] sortNames, public BoolExpr parseSMTLIB2String(String str, Symbol[] sortNames,
Sort[] sorts, Symbol[] declNames, FuncDecl[] decls) Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
{ {
int csn = Symbol.arrayLength(sortNames); int csn = Symbol.arrayLength(sortNames);
int cs = Sort.arrayLength(sorts); int cs = Sort.arrayLength(sorts);
int cdn = Symbol.arrayLength(declNames); int cdn = Symbol.arrayLength(declNames);