mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-28 10:19:23 +00:00
Code Activity

chasing bug in the Java bindings

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-12-03 16:58:44 -08:00
parent 0ec6e2f218
commit 54e452a1af
3 changed files with 54 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

42
examples/java/JavaExample.java
View file

@ -182,6 +182,7 @@ class JavaExample
public void SimpleExample() throws Z3Exception public void SimpleExample() throws Z3Exception
{ {
System.out.println("SimpleExample"); System.out.println("SimpleExample");
Log.Append("SimpleExample");
{ {
Context ctx = new Context(); Context ctx = new Context();
@ -367,6 +368,7 @@ class JavaExample
void ArrayExample1(Context ctx) throws Z3Exception, TestFailedException void ArrayExample1(Context ctx) throws Z3Exception, TestFailedException
{ {
System.out.println("ArrayExample1"); System.out.println("ArrayExample1");
Log.Append("ArrayExample1");
Goal g = ctx.MkGoal(true, false, false); Goal g = ctx.MkGoal(true, false, false);
ArraySort asort = ctx.MkArraySort(ctx.IntSort(), ctx.MkBitVecSort(32)); ArraySort asort = ctx.MkArraySort(ctx.IntSort(), ctx.MkBitVecSort(32));
@ -416,6 +418,7 @@ class JavaExample
TestFailedException TestFailedException
{ {
System.out.println("ArrayExample2"); System.out.println("ArrayExample2");
Log.Append("ArrayExample2");
Sort int_type = ctx.IntSort(); Sort int_type = ctx.IntSort();
Sort array_type = ctx.MkArraySort(int_type, int_type); Sort array_type = ctx.MkArraySort(int_type, int_type);
@ -465,6 +468,7 @@ class JavaExample
TestFailedException TestFailedException
{ {
System.out.println("ArrayExample3"); System.out.println("ArrayExample3");
Log.Append("ArrayExample2");
for (int n = 2; n <= 5; n++) for (int n = 2; n <= 5; n++)
{ {
@ -503,6 +507,7 @@ class JavaExample
void SudokuExample(Context ctx) throws Z3Exception, TestFailedException void SudokuExample(Context ctx) throws Z3Exception, TestFailedException
{ {
System.out.println("SudokuExample"); System.out.println("SudokuExample");
Log.Append("SudokuExample");
// 9x9 matrix of integer variables // 9x9 matrix of integer variables
IntExpr[][] X = new IntExpr[9][]; IntExpr[][] X = new IntExpr[9][];
@ -609,6 +614,7 @@ class JavaExample
void QuantifierExample1(Context ctx) throws Z3Exception void QuantifierExample1(Context ctx) throws Z3Exception
{ {
System.out.println("QuantifierExample"); System.out.println("QuantifierExample");
Log.Append("QuantifierExample");
Sort[] types = new Sort[3]; Sort[] types = new Sort[3];
IntExpr[] xs = new IntExpr[3]; IntExpr[] xs = new IntExpr[3];
@ -654,6 +660,7 @@ class JavaExample
{ {
System.out.println("QuantifierExample2"); System.out.println("QuantifierExample2");
Log.Append("QuantifierExample2");
Expr q1, q2; Expr q1, q2;
FuncDecl f = ctx.MkFuncDecl("f", ctx.IntSort(), ctx.IntSort()); FuncDecl f = ctx.MkFuncDecl("f", ctx.IntSort(), ctx.IntSort());
@ -710,9 +717,11 @@ class JavaExample
public void QuantifierExample3() throws Z3Exception, TestFailedException public void QuantifierExample3() throws Z3Exception, TestFailedException
{ {
System.out.println("QuantifierExample3"); System.out.println("QuantifierExample3");
Log.Append("QuantifierExample3");
HashMap<String, String> cfg = new HashMap<String, String>(); HashMap<String, String> cfg = new HashMap<String, String>();
cfg.put("smt.mbqi", "false"); // We must set a global or provide an argument to Prove
// cfg.put("mbqi", "false");
cfg.put("proof", "true"); cfg.put("proof", "true");
cfg.put("auto_config", "false"); cfg.put("auto_config", "false");
@ -759,9 +768,11 @@ class JavaExample
public void QuantifierExample4() throws Z3Exception, TestFailedException public void QuantifierExample4() throws Z3Exception, TestFailedException
{ {
System.out.println("QuantifierExample4"); System.out.println("QuantifierExample4");
Log.Append("QuantifierExample4");
HashMap<String, String> cfg = new HashMap<String, String>(); HashMap<String, String> cfg = new HashMap<String, String>();
cfg.put("smt.mbqi", "false"); // We must set a global or provide an argument to Prove
// cfg.put("mbqi", "false");
cfg.put("proof", "true"); cfg.put("proof", "true");
cfg.put("auto_config", "false"); cfg.put("auto_config", "false");
@ -1117,6 +1128,7 @@ class JavaExample
void LogicExample(Context ctx) throws Z3Exception, TestFailedException void LogicExample(Context ctx) throws Z3Exception, TestFailedException
{ {
System.out.println("LogicTest"); System.out.println("LogicTest");
Log.Append("LogicTest");
Context.ToggleWarningMessages(true); Context.ToggleWarningMessages(true);
@ -1148,6 +1160,7 @@ class JavaExample
void ParOrExample(Context ctx) throws Z3Exception, TestFailedException void ParOrExample(Context ctx) throws Z3Exception, TestFailedException
{ {
System.out.println("ParOrExample"); System.out.println("ParOrExample");
Log.Append("ParOrExample");
BitVecSort bvs = ctx.MkBitVecSort(32); BitVecSort bvs = ctx.MkBitVecSort(32);
Expr x = ctx.MkConst("x", bvs); Expr x = ctx.MkConst("x", bvs);
@ -1179,6 +1192,7 @@ class JavaExample
TestFailedException TestFailedException
{ {
System.out.println("FindModelExample1"); System.out.println("FindModelExample1");
Log.Append("FindModelExample1");
BoolExpr x = ctx.MkBoolConst("x"); BoolExpr x = ctx.MkBoolConst("x");
BoolExpr y = ctx.MkBoolConst("y"); BoolExpr y = ctx.MkBoolConst("y");
@ -1195,7 +1209,8 @@ class JavaExample
public void FindModelExample2(Context ctx) throws Z3Exception, public void FindModelExample2(Context ctx) throws Z3Exception,
TestFailedException TestFailedException
{ {
System.out.println("find_model_example2"); System.out.println("FindModelExample2");
Log.Append("FindModelExample2");
IntExpr x = ctx.MkIntConst("x"); IntExpr x = ctx.MkIntConst("x");
IntExpr y = ctx.MkIntConst("y"); IntExpr y = ctx.MkIntConst("y");
@ -1235,6 +1250,7 @@ class JavaExample
TestFailedException TestFailedException
{ {
System.out.println("ProveExample1"); System.out.println("ProveExample1");
Log.Append("ProveExample1");
/* create uninterpreted type. */ /* create uninterpreted type. */
Sort U = ctx.MkUninterpretedSort(ctx.MkSymbol("U")); Sort U = ctx.MkUninterpretedSort(ctx.MkSymbol("U"));
@ -1281,6 +1297,7 @@ class JavaExample
TestFailedException TestFailedException
{ {
System.out.println("ProveExample2"); System.out.println("ProveExample2");
Log.Append("ProveExample2");
/* declare function g */ /* declare function g */
Sort I = ctx.IntSort(); Sort I = ctx.IntSort();
@ -1336,6 +1353,7 @@ class JavaExample
TestFailedException TestFailedException
{ {
System.out.println("PushPopExample1"); System.out.println("PushPopExample1");
Log.Append("PushPopExample1");
/* create a big number */ /* create a big number */
IntSort int_type = ctx.IntSort(); IntSort int_type = ctx.IntSort();
@ -1402,6 +1420,7 @@ class JavaExample
TestFailedException TestFailedException
{ {
System.out.println("TupleExample"); System.out.println("TupleExample");
Log.Append("TupleExample");
Sort int_type = ctx.IntSort(); Sort int_type = ctx.IntSort();
TupleSort tuple = ctx.MkTupleSort(ctx.MkSymbol("mk_tuple"), // name of TupleSort tuple = ctx.MkTupleSort(ctx.MkSymbol("mk_tuple"), // name of
@ -1436,6 +1455,7 @@ class JavaExample
TestFailedException TestFailedException
{ {
System.out.println("BitvectorExample1"); System.out.println("BitvectorExample1");
Log.Append("BitvectorExample1");
Sort bv_type = ctx.MkBitVecSort(32); Sort bv_type = ctx.MkBitVecSort(32);
BitVecExpr x = (BitVecExpr) ctx.MkConst("x", bv_type); BitVecExpr x = (BitVecExpr) ctx.MkConst("x", bv_type);
@ -1457,6 +1477,7 @@ class JavaExample
TestFailedException TestFailedException
{ {
System.out.println("BitvectorExample2"); System.out.println("BitvectorExample2");
Log.Append("BitvectorExample2");
/* construct x ^ y - 103 == x * y */ /* construct x ^ y - 103 == x * y */
Sort bv_type = ctx.MkBitVecSort(32); Sort bv_type = ctx.MkBitVecSort(32);
@ -1482,6 +1503,7 @@ class JavaExample
TestFailedException TestFailedException
{ {
System.out.println("ParserExample1"); System.out.println("ParserExample1");
Log.Append("ParserExample1");
ctx.ParseSMTLIBString( ctx.ParseSMTLIBString(
"(benchmark tst :extrafuns ((x Int) (y Int)) :formula (> x y) :formula (> x 0))", "(benchmark tst :extrafuns ((x Int) (y Int)) :formula (> x y) :formula (> x 0))",
@ -1499,6 +1521,7 @@ class JavaExample
TestFailedException TestFailedException
{ {
System.out.println("ParserExample2"); System.out.println("ParserExample2");
Log.Append("ParserExample2");
Symbol[] declNames = { ctx.MkSymbol("a"), ctx.MkSymbol("b") }; Symbol[] declNames = { ctx.MkSymbol("a"), ctx.MkSymbol("b") };
FuncDecl a = ctx.MkConstDecl(declNames[0], ctx.MkIntSort()); FuncDecl a = ctx.MkConstDecl(declNames[0], ctx.MkIntSort());
@ -1517,6 +1540,7 @@ class JavaExample
public void ParserExample3(Context ctx) throws Exception public void ParserExample3(Context ctx) throws Exception
{ {
System.out.println("ParserExample3"); System.out.println("ParserExample3");
Log.Append("ParserExample3");
/* declare function g */ /* declare function g */
Sort I = ctx.MkIntSort(); Sort I = ctx.MkIntSort();
@ -1539,6 +1563,7 @@ class JavaExample
public void ParserExample4(Context ctx) throws Z3Exception public void ParserExample4(Context ctx) throws Z3Exception
{ {
System.out.println("ParserExample4"); System.out.println("ParserExample4");
Log.Append("ParserExample4");
ctx.ParseSMTLIBString( ctx.ParseSMTLIBString(
"(benchmark tst :extrafuns ((x Int) (y Int)) :assumption (= x 20) :formula (> x y) :formula (> x 0))", "(benchmark tst :extrafuns ((x Int) (y Int)) :assumption (= x 20) :formula (> x y) :formula (> x 0))",
@ -1585,6 +1610,7 @@ class JavaExample
public void ITEExample(Context ctx) throws Z3Exception public void ITEExample(Context ctx) throws Z3Exception
{ {
System.out.println("ITEExample"); System.out.println("ITEExample");
Log.Append("ITEExample");
BoolExpr f = ctx.MkFalse(); BoolExpr f = ctx.MkFalse();
Expr one = ctx.MkInt(1); Expr one = ctx.MkInt(1);
@ -1600,6 +1626,7 @@ class JavaExample
TestFailedException TestFailedException
{ {
System.out.println("EnumExample"); System.out.println("EnumExample");
Log.Append("EnumExample");
Symbol name = ctx.MkSymbol("fruit"); Symbol name = ctx.MkSymbol("fruit");
@ -1645,6 +1672,7 @@ class JavaExample
TestFailedException TestFailedException
{ {
System.out.println("ListExample"); System.out.println("ListExample");
Log.Append("ListExample");
Sort int_ty; Sort int_ty;
ListSort int_list; ListSort int_list;
@ -1711,6 +1739,7 @@ class JavaExample
TestFailedException TestFailedException
{ {
System.out.println("TreeExample"); System.out.println("TreeExample");
Log.Append("TreeExample");
Sort cell; Sort cell;
FuncDecl nil_decl, is_nil_decl, cons_decl, is_cons_decl, car_decl, cdr_decl; FuncDecl nil_decl, is_nil_decl, cons_decl, is_cons_decl, car_decl, cdr_decl;
@ -1786,6 +1815,7 @@ class JavaExample
TestFailedException TestFailedException
{ {
System.out.println("ForestExample"); System.out.println("ForestExample");
Log.Append("ForestExample");
Sort tree, forest; Sort tree, forest;
FuncDecl nil1_decl, is_nil1_decl, cons1_decl, is_cons1_decl, car1_decl, cdr1_decl; FuncDecl nil1_decl, is_nil1_decl, cons1_decl, is_cons1_decl, car1_decl, cdr1_decl;
@ -1901,6 +1931,7 @@ class JavaExample
public void EvalExample1(Context ctx) throws Z3Exception public void EvalExample1(Context ctx) throws Z3Exception
{ {
System.out.println("EvalExample1"); System.out.println("EvalExample1");
Log.Append("EvalExample1");
IntExpr x = ctx.MkIntConst("x"); IntExpr x = ctx.MkIntConst("x");
IntExpr y = ctx.MkIntConst("y"); IntExpr y = ctx.MkIntConst("y");
@ -1940,6 +1971,7 @@ class JavaExample
public void EvalExample2(Context ctx) throws Z3Exception public void EvalExample2(Context ctx) throws Z3Exception
{ {
System.out.println("EvalExample2"); System.out.println("EvalExample2");
Log.Append("EvalExample2");
Sort int_type = ctx.IntSort(); Sort int_type = ctx.IntSort();
TupleSort tuple = ctx.MkTupleSort(ctx.MkSymbol("mk_tuple"), // name of TupleSort tuple = ctx.MkTupleSort(ctx.MkSymbol("mk_tuple"), // name of
@ -2063,6 +2095,7 @@ class JavaExample
public void FindSmallModelExample(Context ctx) throws Z3Exception public void FindSmallModelExample(Context ctx) throws Z3Exception
{ {
System.out.println("FindSmallModelExample"); System.out.println("FindSmallModelExample");
Log.Append("FindSmallModelExample");
BitVecExpr x = ctx.MkBVConst("x", 32); BitVecExpr x = ctx.MkBVConst("x", 32);
BitVecExpr y = ctx.MkBVConst("y", 32); BitVecExpr y = ctx.MkBVConst("y", 32);
@ -2079,6 +2112,7 @@ class JavaExample
public void SimplifierExample(Context ctx) throws Z3Exception public void SimplifierExample(Context ctx) throws Z3Exception
{ {
System.out.println("SimplifierExample"); System.out.println("SimplifierExample");
Log.Append("SimplifierExample");
IntExpr x = ctx.MkIntConst("x"); IntExpr x = ctx.MkIntConst("x");
IntExpr y = ctx.MkIntConst("y"); IntExpr y = ctx.MkIntConst("y");
@ -2098,6 +2132,7 @@ class JavaExample
public void UnsatCoreAndProofExample() throws Z3Exception public void UnsatCoreAndProofExample() throws Z3Exception
{ {
System.out.println("UnsatCoreAndProofExample"); System.out.println("UnsatCoreAndProofExample");
Log.Append("UnsatCoreAndProofExample");
HashMap<String, String> cfg = new HashMap<String, String>(); HashMap<String, String> cfg = new HashMap<String, String>();
cfg.put("proof", "true"); cfg.put("proof", "true");
@ -2144,6 +2179,7 @@ class JavaExample
public void FiniteDomainExample(Context ctx) throws Z3Exception public void FiniteDomainExample(Context ctx) throws Z3Exception
{ {
System.out.println("FiniteDomainExample"); System.out.println("FiniteDomainExample");
Log.Append("FiniteDomainExample");
FiniteDomainSort s = ctx.MkFiniteDomainSort("S", 10); FiniteDomainSort s = ctx.MkFiniteDomainSort("S", 10);
FiniteDomainSort t = ctx.MkFiniteDomainSort("T", 10); FiniteDomainSort t = ctx.MkFiniteDomainSort("T", 10);

10
src/api/z3_replayer.cpp
View file

@ -232,8 +232,11 @@ struct z3_replayer::imp {
} }
void read_ptr() { void read_ptr() {
if (!(('0' <= curr() && curr() <= '9') || ('A' <= curr() && curr() <= 'F') || ('a' <= curr() && curr() <= 'f'))) if (!(('0' <= curr() && curr() <= '9') || ('A' <= curr() && curr() <= 'F') || ('a' <= curr() && curr() <= 'f'))) {
TRACE("invalid_ptr", tout << "curr: " << curr() << "\n";);
throw z3_replayer_exception("invalid ptr"); throw z3_replayer_exception("invalid ptr");
}
unsigned pos = 0;
m_ptr = 0; m_ptr = 0;
while (true) { while (true) {
char c = curr(); char c = curr();
@ -246,10 +249,13 @@ struct z3_replayer::imp {
else if ('A' <= c && c <= 'F') { else if ('A' <= c && c <= 'F') {
m_ptr = m_ptr * 16 + 10 + (c - 'A'); m_ptr = m_ptr * 16 + 10 + (c - 'A');
} }
else if (pos == 1 && (c == 'x' || c == 'X')) {
// support for 0x.... notation
}
else { else {
return; return;
} }
next(); next(); pos++;
} }
} }

14
src/smt/smt_setup.cpp
View file

@ -266,7 +266,7 @@ namespace smt {
// Moreover, if model construction is enabled, then rational numbers may be needed // Moreover, if model construction is enabled, then rational numbers may be needed
// to compute the actual value of epsilon even if the input does not have rational numbers. // to compute the actual value of epsilon even if the input does not have rational numbers.
// Example: (x < 1) and (x > 0) // Example: (x < 1) and (x > 0)
if (m_params.m_proof_mode != PGM_DISABLED) { if (m_manager.proof_mode() != PGM_DISABLED) {
m_context.register_plugin(alloc(smt::theory_mi_arith_w_proofs, m_manager, m_params)); m_context.register_plugin(alloc(smt::theory_mi_arith_w_proofs, m_manager, m_params));
} }
else if (!m_params.m_arith_auto_config_simplex && is_dense(st)) { else if (!m_params.m_arith_auto_config_simplex && is_dense(st)) {
@ -343,7 +343,7 @@ namespace smt {
tout << "RELEVANCY: " << m_params.m_relevancy_lvl << "\n"; tout << "RELEVANCY: " << m_params.m_relevancy_lvl << "\n";
tout << "ARITH_EQ_BOUNDS: " << m_params.m_arith_eq_bounds << "\n";); tout << "ARITH_EQ_BOUNDS: " << m_params.m_arith_eq_bounds << "\n";);
if (m_params.m_proof_mode != PGM_DISABLED) { if (m_manager.proof_mode() != PGM_DISABLED) {
m_context.register_plugin(alloc(smt::theory_mi_arith_w_proofs, m_manager, m_params)); m_context.register_plugin(alloc(smt::theory_mi_arith_w_proofs, m_manager, m_params));
} }
else if (!m_params.m_arith_auto_config_simplex && is_dense(st)) { else if (!m_params.m_arith_auto_config_simplex && is_dense(st)) {
@ -394,7 +394,7 @@ namespace smt {
m_params.m_lemma_gc_half = true; m_params.m_lemma_gc_half = true;
m_params.m_restart_strategy = RS_GEOMETRIC; m_params.m_restart_strategy = RS_GEOMETRIC;
if (m_params.m_proof_mode != PGM_DISABLED) { if (m_manager.proof_mode() != PGM_DISABLED) {
m_context.register_plugin(alloc(smt::theory_mi_arith_w_proofs, m_manager, m_params)); m_context.register_plugin(alloc(smt::theory_mi_arith_w_proofs, m_manager, m_params));
} }
else if (st.m_arith_k_sum < rational(INT_MAX / 8)) else if (st.m_arith_k_sum < rational(INT_MAX / 8))
@ -409,7 +409,7 @@ namespace smt {
m_params.m_restart_strategy = RS_GEOMETRIC; m_params.m_restart_strategy = RS_GEOMETRIC;
m_params.m_restart_factor = 1.5; m_params.m_restart_factor = 1.5;
m_params.m_restart_adaptive = false; m_params.m_restart_adaptive = false;
if (m_params.m_proof_mode != PGM_DISABLED) { if (m_manager.proof_mode() != PGM_DISABLED) {
m_context.register_plugin(alloc(smt::theory_mi_arith_w_proofs, m_manager, m_params)); m_context.register_plugin(alloc(smt::theory_mi_arith_w_proofs, m_manager, m_params));
} }
// else if (st.m_arith_k_sum < rational(INT_MAX / 8)) // else if (st.m_arith_k_sum < rational(INT_MAX / 8))
@ -683,7 +683,7 @@ namespace smt {
} }
void setup::setup_i_arith() { void setup::setup_i_arith() {
if (m_params.m_proof_mode != PGM_DISABLED) { if (m_manager.proof_mode() != PGM_DISABLED) {
m_context.register_plugin(alloc(smt::theory_mi_arith_w_proofs, m_manager, m_params)); m_context.register_plugin(alloc(smt::theory_mi_arith_w_proofs, m_manager, m_params));
} }
else { else {
@ -692,7 +692,7 @@ namespace smt {
} }
void setup::setup_mi_arith() { void setup::setup_mi_arith() {
if (m_params.m_proof_mode != PGM_DISABLED) { if (m_manager.proof_mode() != PGM_DISABLED) {
m_context.register_plugin(alloc(smt::theory_mi_arith_w_proofs, m_manager, m_params)); m_context.register_plugin(alloc(smt::theory_mi_arith_w_proofs, m_manager, m_params));
} }
else { else {
@ -734,7 +734,7 @@ namespace smt {
} }
break; break;
default: default:
if (m_params.m_proof_mode != PGM_DISABLED) { if (m_manager.proof_mode() != PGM_DISABLED) {
m_context.register_plugin(alloc(smt::theory_mi_arith_w_proofs, m_manager, m_params)); m_context.register_plugin(alloc(smt::theory_mi_arith_w_proofs, m_manager, m_params));
} }
// else if (m_params.m_arith_fixnum) { // else if (m_params.m_arith_fixnum) {