diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp
index 180117a96..ab6e67ab9 100644
--- a/examples/c++/example.cpp
+++ b/examples/c++/example.cpp
@@ -143,7 +143,7 @@ void prove_example2() {
void nonlinear_example1() {
std::cout << "nonlinear example 1\n";
config cfg;
- cfg.set(":auto-config", true);
+ cfg.set("auto_config", true);
context c(cfg);
expr x = c.real_const("x");
@@ -158,12 +158,13 @@ void nonlinear_example1() {
std::cout << s.check() << "\n";
model m = s.get_model();
std::cout << m << "\n";
- c.set(":pp-decimal", true); // set decimal notation
+ set_param("pp.decimal", true); // set decimal notation
std::cout << "model in decimal notation\n";
std::cout << m << "\n";
- c.set(":pp-decimal-precision", 50); // increase number of decimal places to 50.
+ set_param("pp.decimal-precision", 50); // increase number of decimal places to 50.
std::cout << "model using 50 decimal places\n";
std::cout << m << "\n";
+ set_param("pp.decimal", false); // disable decimal notation
}
/**
@@ -352,7 +353,7 @@ void quantifier_example() {
// making sure model based quantifier instantiation is enabled.
params p(c);
- p.set(":mbqi", true);
+ p.set("mbqi", true);
s.set(p);
s.add(forall(x, y, f(x, y) >= 0));
@@ -468,7 +469,7 @@ void unsat_core_example3() {
// enabling unsat core tracking
params p(c);
- p.set(":unsat-core", true);
+ p.set("unsat_core", true);
s.set(p);
// The following assertion will not be tracked.
@@ -585,7 +586,7 @@ void tactic_example4() {
std::cout << "tactic example 4\n";
context c;
params p(c);
- p.set(":mul2concat", true);
+ p.set("mul2concat", true);
tactic t =
with(tactic(c, "simplify"), p) &
tactic(c, "solve-eqs") &
@@ -628,8 +629,8 @@ void tactic_example6() {
std::cout << "tactic example 6\n";
context c;
params p(c);
- p.set(":arith-lhs", true);
- p.set(":som", true); // sum-of-monomials normal form
+ p.set("arith_lhs", true);
+ p.set("som", true); // sum-of-monomials normal form
solver s =
(with(tactic(c, "simplify"), p) &
tactic(c, "normalize-bounds") &
diff --git a/examples/c/test_capi.c b/examples/c/test_capi.c
index 70cdc2852..27bf6de2c 100644
--- a/examples/c/test_capi.c
+++ b/examples/c/test_capi.c
@@ -70,7 +70,7 @@ Z3_context mk_context_custom(Z3_config cfg, Z3_error_handler err)
{
Z3_context ctx;
- Z3_set_param_value(cfg, "MODEL", "true");
+ Z3_set_param_value(cfg, "model", "true");
ctx = Z3_mk_context(cfg);
Z3_set_error_handler(ctx, err);
@@ -105,7 +105,7 @@ Z3_context mk_context()
Z3_context mk_proof_context() {
Z3_config cfg = Z3_mk_config();
Z3_context ctx;
- Z3_set_param_value(cfg, "PROOF_MODE", "2");
+ Z3_set_param_value(cfg, "proof", "true");
ctx = mk_context_custom(cfg, throw_z3_error);
Z3_del_config(cfg);
return ctx;
@@ -1038,12 +1038,12 @@ void quantifier_example1()
/* If quantified formulas are asserted in a logical context, then
Z3 may return L_UNDEF. In this case, the model produced by Z3 should be viewed as a potential/candidate model.
*/
- Z3_set_param_value(cfg, "MODEL", "true");
+
/*
The current model finder for quantified formulas cannot handle injectivity.
So, we are limiting the number of iterations to avoid a long "wait".
*/
- Z3_set_param_value(cfg, "MBQI_MAX_ITERATIONS", "10");
+ Z3_global_param_set("smt.mbqi.max_iterations", "10");
ctx = mk_context_custom(cfg, error_handler);
Z3_del_config(cfg);
@@ -1087,8 +1087,9 @@ void quantifier_example1()
if (Z3_get_search_failure(ctx) != Z3_QUANTIFIERS) {
exitf("unexpected result");
}
-
Z3_del_context(ctx);
+ /* reset global parameters set by this function */
+ Z3_global_param_reset_all();
}
/**
@@ -1646,7 +1647,7 @@ void parser_example3()
cfg = Z3_mk_config();
/* See quantifer_example1 */
- Z3_set_param_value(cfg, "MODEL", "true");
+ Z3_set_param_value(cfg, "model", "true");
ctx = mk_context_custom(cfg, error_handler);
Z3_del_config(cfg);
@@ -2249,57 +2250,6 @@ void unsat_core_and_proof_example() {
Z3_del_context(ctx);
}
-/**
- \brief Extract classes of implied equalities.
-
- This example illustrates the use of #Z3_get_implied_equalities.
-*/
-void get_implied_equalities_example() {
- Z3_config cfg = Z3_mk_config();
- Z3_context ctx;
-
- printf("\nget_implied_equalities example\n");
- LOG_MSG("get_implied_equalities example");
-
- Z3_set_param_value(cfg, "ARITH_PROCESS_ALL_EQS", "true");
- Z3_set_param_value(cfg, "ARITH_EQ_BOUNDS", "true");
- ctx = Z3_mk_context(cfg);
- Z3_del_config(cfg);
- {
- Z3_sort int_ty = Z3_mk_int_sort(ctx);
- Z3_ast a = mk_int_var(ctx,"a");
- Z3_ast b = mk_int_var(ctx,"b");
- Z3_ast c = mk_int_var(ctx,"c");
- Z3_ast d = mk_int_var(ctx,"d");
- Z3_func_decl f = Z3_mk_func_decl(ctx, Z3_mk_string_symbol(ctx,"f"), 1, &int_ty, int_ty);
- Z3_ast fa = Z3_mk_app(ctx, f, 1, &a);
- Z3_ast fb = Z3_mk_app(ctx, f, 1, &b);
- Z3_ast fc = Z3_mk_app(ctx, f, 1, &c);
- unsigned const num_terms = 7;
- unsigned i;
- Z3_ast terms[7] = { a, b, c, d, fa, fb, fc };
- unsigned class_ids[7] = { 0, 0, 0, 0, 0, 0, 0 };
-
- Z3_assert_cnstr(ctx, Z3_mk_eq(ctx, a, b));
- Z3_assert_cnstr(ctx, Z3_mk_eq(ctx, b, c));
- Z3_assert_cnstr(ctx, Z3_mk_le(ctx, fc, b));
- Z3_assert_cnstr(ctx, Z3_mk_le(ctx, b, fa));
-
- Z3_get_implied_equalities(ctx, num_terms, terms, class_ids);
- for (i = 0; i < num_terms; ++i) {
- printf("Class %s |-> %d\n", Z3_ast_to_string(ctx, terms[i]), class_ids[i]);
- }
- printf("asserting f(a) <= b\n");
- Z3_assert_cnstr(ctx, Z3_mk_le(ctx, fa, b));
- Z3_get_implied_equalities(ctx, num_terms, terms, class_ids);
- for (i = 0; i < num_terms; ++i) {
- printf("Class %s |-> %d\n", Z3_ast_to_string(ctx, terms[i]), class_ids[i]);
- }
- }
- /* delete logical context */
- Z3_del_context(ctx);
-}
-
#define MAX_RETRACTABLE_ASSERTIONS 1024
/**
@@ -2504,7 +2454,7 @@ void reference_counter_example() {
LOG_MSG("reference_counter_example");
cfg = Z3_mk_config();
- Z3_set_param_value(cfg, "MODEL", "true");
+ Z3_set_param_value(cfg, "model", "true");
// Create a Z3 context where the user is reponsible for managing
// Z3_ast reference counters.
ctx = Z3_mk_context_rc(cfg);
@@ -2685,7 +2635,6 @@ int main() {
binary_tree_example();
enum_example();
unsat_core_and_proof_example();
- get_implied_equalities_example();
incremental_example1();
reference_counter_example();
smt2parser_example();
diff --git a/examples/dotnet/Program.cs b/examples/dotnet/Program.cs
index 75393378b..2085de296 100644
--- a/examples/dotnet/Program.cs
+++ b/examples/dotnet/Program.cs
@@ -248,10 +248,13 @@ namespace test_mapi
return res;
}
- static void Prove(Context ctx, BoolExpr f, params BoolExpr[] assumptions)
+ static void Prove(Context ctx, BoolExpr f, bool useMBQI = false, params BoolExpr[] assumptions)
{
Console.WriteLine("Proving: " + f);
Solver s = ctx.MkSolver();
+ Params p = ctx.MkParams();
+ p.Add("mbqi", useMBQI);
+ s.Parameters = p;
foreach (BoolExpr a in assumptions)
s.Assert(a);
s.Assert(ctx.MkNot(f));
@@ -270,10 +273,13 @@ namespace test_mapi
}
}
- static void Disprove(Context ctx, BoolExpr f, params BoolExpr[] assumptions)
+ static void Disprove(Context ctx, BoolExpr f, bool useMBQI = false, params BoolExpr[] assumptions)
{
Console.WriteLine("Disproving: " + f);
Solver s = ctx.MkSolver();
+ Params p = ctx.MkParams();
+ p.Add("mbqi", useMBQI);
+ s.Parameters = p;
foreach (BoolExpr a in assumptions)
s.Assert(a);
s.Assert(ctx.MkNot(f));
@@ -298,7 +304,7 @@ namespace test_mapi
ArithExpr xr = (ArithExpr)ctx.MkConst(ctx.MkSymbol("x"), ctx.MkRealSort());
ArithExpr yr = (ArithExpr)ctx.MkConst(ctx.MkSymbol("y"), ctx.MkRealSort());
- Goal g4 = ctx.MkGoal(true, false, true);
+ Goal g4 = ctx.MkGoal(true);
g4.Assert(ctx.MkGt(xr, ctx.MkReal(10, 1)));
g4.Assert(ctx.MkEq(yr, ctx.MkAdd(xr, ctx.MkReal(1, 1))));
g4.Assert(ctx.MkGt(yr, ctx.MkReal(1, 1)));
@@ -330,7 +336,7 @@ namespace test_mapi
{
Console.WriteLine("ArrayExample1");
- Goal g = ctx.MkGoal(true, false, false);
+ Goal g = ctx.MkGoal(true);
ArraySort asort = ctx.MkArraySort(ctx.IntSort, ctx.MkBitVecSort(32));
ArrayExpr aex = (ArrayExpr)ctx.MkConst(ctx.MkSymbol("MyArray"), asort);
Expr sel = ctx.MkSelect(aex, ctx.MkInt(0));
@@ -640,95 +646,76 @@ namespace test_mapi
/// Prove that f(x, y) = f(w, v) implies y = v when
/// f is injective in the second argument.
///
- public static void QuantifierExample3()
+ public static void QuantifierExample3(Context ctx)
{
Console.WriteLine("QuantifierExample3");
-
- Dictionary cfg = new Dictionary() {
- { "MBQI", "false" },
- { "PROOF_MODE", "2" },
- { "AUTO_CONFIG", "false" }
- };
-
/* If quantified formulas are asserted in a logical context, then
the model produced by Z3 should be viewed as a potential model. */
- using (Context ctx = new Context(cfg))
- {
- /* declare function f */
- Sort I = ctx.IntSort;
- FuncDecl f = ctx.MkFuncDecl("f", new Sort[] { I, I }, I);
+ /* declare function f */
+ Sort I = ctx.IntSort;
+ FuncDecl f = ctx.MkFuncDecl("f", new Sort[] { I, I }, I);
- /* f is injective in the second argument. */
- BoolExpr inj = InjAxiom(ctx, f, 1);
+ /* f is injective in the second argument. */
+ BoolExpr inj = InjAxiom(ctx, f, 1);
- /* create x, y, v, w, fxy, fwv */
- Expr x = ctx.MkIntConst("x");
- Expr y = ctx.MkIntConst("y");
- Expr v = ctx.MkIntConst("v");
- Expr w = ctx.MkIntConst("w");
- Expr fxy = ctx.MkApp(f, x, y);
- Expr fwv = ctx.MkApp(f, w, v);
+ /* create x, y, v, w, fxy, fwv */
+ Expr x = ctx.MkIntConst("x");
+ Expr y = ctx.MkIntConst("y");
+ Expr v = ctx.MkIntConst("v");
+ Expr w = ctx.MkIntConst("w");
+ Expr fxy = ctx.MkApp(f, x, y);
+ Expr fwv = ctx.MkApp(f, w, v);
- /* f(x, y) = f(w, v) */
- BoolExpr p1 = ctx.MkEq(fxy, fwv);
+ /* f(x, y) = f(w, v) */
+ BoolExpr p1 = ctx.MkEq(fxy, fwv);
- /* prove f(x, y) = f(w, v) implies y = v */
- BoolExpr p2 = ctx.MkEq(y, v);
- Prove(ctx, p2, inj, p1);
+ /* prove f(x, y) = f(w, v) implies y = v */
+ BoolExpr p2 = ctx.MkEq(y, v);
+ Prove(ctx, p2, false, inj, p1);
- /* disprove f(x, y) = f(w, v) implies x = w */
- BoolExpr p3 = ctx.MkEq(x, w);
- Disprove(ctx, p3, inj, p1);
- }
+ /* disprove f(x, y) = f(w, v) implies x = w */
+ BoolExpr p3 = ctx.MkEq(x, w);
+ Disprove(ctx, p3, false, inj, p1);
}
///
/// Prove that f(x, y) = f(w, v) implies y = v when
/// f is injective in the second argument.
///
- public static void QuantifierExample4()
+ public static void QuantifierExample4(Context ctx)
{
Console.WriteLine("QuantifierExample4");
- Dictionary cfg = new Dictionary() {
- { "MBQI", "false" },
- { "PROOF_MODE", "2" },
- { "AUTO_CONFIG","false" }};
-
-
/* If quantified formulas are asserted in a logical context, then
the model produced by Z3 should be viewed as a potential model. */
- using (Context ctx = new Context(cfg))
- {
- /* declare function f */
- Sort I = ctx.IntSort;
- FuncDecl f = ctx.MkFuncDecl("f", new Sort[] { I, I }, I);
+ /* declare function f */
+ Sort I = ctx.IntSort;
+ FuncDecl f = ctx.MkFuncDecl("f", new Sort[] { I, I }, I);
- /* f is injective in the second argument. */
- BoolExpr inj = InjAxiomAbs(ctx, f, 1);
+ /* f is injective in the second argument. */
+ BoolExpr inj = InjAxiomAbs(ctx, f, 1);
- /* create x, y, v, w, fxy, fwv */
- Expr x = ctx.MkIntConst("x");
- Expr y = ctx.MkIntConst("y");
- Expr v = ctx.MkIntConst("v");
- Expr w = ctx.MkIntConst("w");
- Expr fxy = ctx.MkApp(f, x, y);
- Expr fwv = ctx.MkApp(f, w, v);
+ /* create x, y, v, w, fxy, fwv */
+ Expr x = ctx.MkIntConst("x");
+ Expr y = ctx.MkIntConst("y");
+ Expr v = ctx.MkIntConst("v");
+ Expr w = ctx.MkIntConst("w");
+ Expr fxy = ctx.MkApp(f, x, y);
+ Expr fwv = ctx.MkApp(f, w, v);
- /* f(x, y) = f(w, v) */
- BoolExpr p1 = ctx.MkEq(fxy, fwv);
+ /* f(x, y) = f(w, v) */
+ BoolExpr p1 = ctx.MkEq(fxy, fwv);
- /* prove f(x, y) = f(w, v) implies y = v */
- BoolExpr p2 = ctx.MkEq(y, v);
- Prove(ctx, p2, inj, p1);
+ /* prove f(x, y) = f(w, v) implies y = v */
+ BoolExpr p2 = ctx.MkEq(y, v);
+ Prove(ctx, p2, false, inj, p1);
- /* disprove f(x, y) = f(w, v) implies x = w */
- BoolExpr p3 = ctx.MkEq(x, w);
- Disprove(ctx, p3, inj, p1);
- }
+ /* disprove f(x, y) = f(w, v) implies x = w */
+ BoolExpr p3 = ctx.MkEq(x, w);
+ Disprove(ctx, p3, false, inj, p1);
}
///
@@ -756,7 +743,7 @@ namespace test_mapi
BoolExpr trivial_eq = ctx.MkEq(fapp, fapp);
BoolExpr nontrivial_eq = ctx.MkEq(fapp, fapp2);
- Goal g = ctx.MkGoal(true, false, true);
+ Goal g = ctx.MkGoal(true);
g.Assert(trivial_eq);
g.Assert(nontrivial_eq);
Console.WriteLine("Goal: " + g);
@@ -784,18 +771,18 @@ namespace test_mapi
throw new TestFailedException();
- Goal g2 = ctx.MkGoal(true, true, false);
+ Goal g2 = ctx.MkGoal(true, true);
ar = ApplyTactic(ctx, ctx.MkTactic("smt"), g2);
if (ar.NumSubgoals != 1 || !ar.Subgoals[0].IsDecidedSat)
throw new TestFailedException();
- g2 = ctx.MkGoal(true, true, false);
+ g2 = ctx.MkGoal(true, true);
g2.Assert(ctx.MkFalse());
ar = ApplyTactic(ctx, ctx.MkTactic("smt"), g2);
if (ar.NumSubgoals != 1 || !ar.Subgoals[0].IsDecidedUnsat)
throw new TestFailedException();
- Goal g3 = ctx.MkGoal(true, true, false);
+ Goal g3 = ctx.MkGoal(true, true);
Expr xc = ctx.MkConst(ctx.MkSymbol("x"), ctx.IntSort);
Expr yc = ctx.MkConst(ctx.MkSymbol("y"), ctx.IntSort);
g3.Assert(ctx.MkEq(xc, ctx.MkNumeral(1, ctx.IntSort)));
@@ -1063,7 +1050,7 @@ namespace test_mapi
// Or perhaps a tactic for QF_BV
- Goal g = ctx.MkGoal(true, false, true);
+ Goal g = ctx.MkGoal(true);
g.Assert(eq);
Tactic t = ctx.MkTactic("qfbv");
@@ -1086,7 +1073,7 @@ namespace test_mapi
Expr y = ctx.MkConst("y", bvs);
BoolExpr q = ctx.MkEq(x, y);
- Goal g = ctx.MkGoal(true, false, true);
+ Goal g = ctx.MkGoal(true);
g.Assert(q);
Tactic t1 = ctx.MkTactic("qfbv");
@@ -1128,7 +1115,7 @@ namespace test_mapi
///
public static void FindModelExample2(Context ctx)
{
- Console.WriteLine("find_model_example2");
+ Console.WriteLine("FindModelExample2");
IntExpr x = ctx.MkIntConst("x");
IntExpr y = ctx.MkIntConst("y");
@@ -1250,13 +1237,13 @@ namespace test_mapi
/* prove z < 0 */
BoolExpr f = ctx.MkLt(z, zero);
Console.WriteLine("prove: not(g(g(x) - g(y)) = g(z)), x + z <= y <= x implies z < 0");
- Prove(ctx, f, c1, c2, c3);
+ Prove(ctx, f, false, c1, c2, c3);
/* disprove z < -1 */
IntExpr minus_one = ctx.MkInt(-1);
f = ctx.MkLt(z, minus_one);
Console.WriteLine("disprove: not(g(g(x) - g(y)) = g(z)), x + z <= y <= x implies z < -1");
- Disprove(ctx, f, c1, c2, c3);
+ Disprove(ctx, f, false, c1, c2, c3);
}
///
@@ -1448,7 +1435,7 @@ namespace test_mapi
BoolExpr thm = ctx.SMTLIBFormulas[0];
Console.WriteLine("formula: {0}", thm);
- Prove(ctx, thm, ca);
+ Prove(ctx, thm, false, ca);
}
///
@@ -1979,45 +1966,40 @@ namespace test_mapi
///
/// Extract unsatisfiable core example
///
- public static void UnsatCoreAndProofExample()
+ public static void UnsatCoreAndProofExample(Context ctx)
{
Console.WriteLine("UnsatCoreAndProofExample");
- Dictionary cfg = new Dictionary() { { "PROOF_MODE", "2" } };
+ Solver solver = ctx.MkSolver();
- using (Context ctx = new Context(cfg))
+ BoolExpr pa = ctx.MkBoolConst("PredA");
+ BoolExpr pb = ctx.MkBoolConst("PredB");
+ BoolExpr pc = ctx.MkBoolConst("PredC");
+ BoolExpr pd = ctx.MkBoolConst("PredD");
+ BoolExpr p1 = ctx.MkBoolConst("P1");
+ BoolExpr p2 = ctx.MkBoolConst("P2");
+ BoolExpr p3 = ctx.MkBoolConst("P3");
+ BoolExpr p4 = ctx.MkBoolConst("P4");
+ BoolExpr[] assumptions = new BoolExpr[] { ctx.MkNot(p1), ctx.MkNot(p2), ctx.MkNot(p3), ctx.MkNot(p4) };
+ BoolExpr f1 = ctx.MkAnd(new BoolExpr[] { pa, pb, pc });
+ BoolExpr f2 = ctx.MkAnd(new BoolExpr[] { pa, ctx.MkNot(pb), pc });
+ BoolExpr f3 = ctx.MkOr(ctx.MkNot(pa), ctx.MkNot(pc));
+ BoolExpr f4 = pd;
+
+ solver.Assert(ctx.MkOr(f1, p1));
+ solver.Assert(ctx.MkOr(f2, p2));
+ solver.Assert(ctx.MkOr(f3, p3));
+ solver.Assert(ctx.MkOr(f4, p4));
+ Status result = solver.Check(assumptions);
+
+ if (result == Status.UNSATISFIABLE)
{
- Solver solver = ctx.MkSolver();
-
- BoolExpr pa = ctx.MkBoolConst("PredA");
- BoolExpr pb = ctx.MkBoolConst("PredB");
- BoolExpr pc = ctx.MkBoolConst("PredC");
- BoolExpr pd = ctx.MkBoolConst("PredD");
- BoolExpr p1 = ctx.MkBoolConst("P1");
- BoolExpr p2 = ctx.MkBoolConst("P2");
- BoolExpr p3 = ctx.MkBoolConst("P3");
- BoolExpr p4 = ctx.MkBoolConst("P4");
- BoolExpr[] assumptions = new BoolExpr[] { ctx.MkNot(p1), ctx.MkNot(p2), ctx.MkNot(p3), ctx.MkNot(p4) };
- BoolExpr f1 = ctx.MkAnd(new BoolExpr[] { pa, pb, pc });
- BoolExpr f2 = ctx.MkAnd(new BoolExpr[] { pa, ctx.MkNot(pb), pc });
- BoolExpr f3 = ctx.MkOr(ctx.MkNot(pa), ctx.MkNot(pc));
- BoolExpr f4 = pd;
-
- solver.Assert(ctx.MkOr(f1, p1));
- solver.Assert(ctx.MkOr(f2, p2));
- solver.Assert(ctx.MkOr(f3, p3));
- solver.Assert(ctx.MkOr(f4, p4));
- Status result = solver.Check(assumptions);
-
- if (result == Status.UNSATISFIABLE)
+ Console.WriteLine("unsat");
+ Console.WriteLine("proof: {0}", solver.Proof);
+ Console.WriteLine("core: ");
+ foreach (Expr c in solver.UnsatCore)
{
- Console.WriteLine("unsat");
- Console.WriteLine("proof: {0}", solver.Proof);
- Console.WriteLine("core: ");
- foreach (Expr c in solver.UnsatCore)
- {
- Console.WriteLine("{0}", c);
- }
+ Console.WriteLine("{0}", c);
}
}
}
@@ -2054,9 +2036,8 @@ namespace test_mapi
SimpleExample();
- using (Context ctx = new Context(new Dictionary()
- { { "MODEL", "true"},
- { "PROOF_MODE", "2"} }))
+ // These examples need model generation turned on.
+ using (Context ctx = new Context(new Dictionary() { { "model", "true" } }))
{
BasicTests(ctx);
CastingTest(ctx);
@@ -2067,25 +2048,16 @@ namespace test_mapi
ParOrExample(ctx);
FindModelExample1(ctx);
FindModelExample2(ctx);
- ProveExample1(ctx);
- ProveExample2(ctx);
PushPopExample1(ctx);
ArrayExample1(ctx);
- ArrayExample2(ctx);
ArrayExample3(ctx);
- TupleExample(ctx);
BitvectorExample1(ctx);
BitvectorExample2(ctx);
ParserExample1(ctx);
ParserExample2(ctx);
- ParserExample3(ctx);
ParserExample4(ctx);
ParserExample5(ctx);
ITEExample(ctx);
- EnumExample(ctx);
- ListExample(ctx);
- TreeExample(ctx);
- ForestExample(ctx);
EvalExample1(ctx);
EvalExample2(ctx);
FindSmallModelExample(ctx);
@@ -2093,9 +2065,29 @@ namespace test_mapi
FiniteDomainExample(ctx);
}
- QuantifierExample3();
- QuantifierExample4();
- UnsatCoreAndProofExample();
+ // These examples need proof generation turned on.
+ using (Context ctx = new Context(new Dictionary() { { "proof", "true" } }))
+ {
+ ProveExample1(ctx);
+ ProveExample2(ctx);
+ ArrayExample2(ctx);
+ TupleExample(ctx);
+ ParserExample3(ctx);
+ EnumExample(ctx);
+ ListExample(ctx);
+ TreeExample(ctx);
+ ForestExample(ctx);
+ UnsatCoreAndProofExample(ctx);
+ }
+
+ // These examples need proof generation turned on and auto-config set to false.
+ using (Context ctx = new Context(new Dictionary()
+ { {"proof", "true" },
+ {"auto-config", "false" } }))
+ {
+ QuantifierExample3(ctx);
+ QuantifierExample4(ctx);
+ }
Log.Close();
if (Log.isOpen())
diff --git a/examples/java/JavaExample.java b/examples/java/JavaExample.java
index d06f72217..b3cb939ac 100644
--- a/examples/java/JavaExample.java
+++ b/examples/java/JavaExample.java
@@ -182,6 +182,7 @@ class JavaExample
public void SimpleExample() throws Z3Exception
{
System.out.println("SimpleExample");
+ Log.Append("SimpleExample");
{
Context ctx = new Context();
@@ -249,24 +250,28 @@ class JavaExample
return res;
}
- void Prove(Context ctx, BoolExpr f) throws Z3Exception, TestFailedException
+ void Prove(Context ctx, BoolExpr f, boolean useMBQI) throws Z3Exception,
+ TestFailedException
{
BoolExpr[] assumptions = new BoolExpr[0];
- Prove(ctx, f, assumptions);
+ Prove(ctx, f, useMBQI, assumptions);
}
- void Prove(Context ctx, BoolExpr f, BoolExpr assumption)
+ void Prove(Context ctx, BoolExpr f, boolean useMBQI, BoolExpr assumption)
throws Z3Exception, TestFailedException
{
BoolExpr[] assumptions = { assumption };
- Prove(ctx, f, assumptions);
+ Prove(ctx, f, useMBQI, assumptions);
}
- void Prove(Context ctx, BoolExpr f, BoolExpr[] assumptions)
+ void Prove(Context ctx, BoolExpr f, boolean useMBQI, BoolExpr[] assumptions)
throws Z3Exception, TestFailedException
{
System.out.println("Proving: " + f);
Solver s = ctx.MkSolver();
+ Params p = ctx.MkParams();
+ p.Add("mbqi", useMBQI);
+ s.setParameters(p);
for (BoolExpr a : assumptions)
s.Assert(a);
s.Assert(ctx.MkNot(f));
@@ -285,25 +290,28 @@ class JavaExample
}
}
- void Disprove(Context ctx, BoolExpr f) throws Z3Exception,
+ void Disprove(Context ctx, BoolExpr f, boolean useMBQI) throws Z3Exception,
TestFailedException
{
BoolExpr[] a = {};
- Disprove(ctx, f, a);
+ Disprove(ctx, f, useMBQI, a);
}
- void Disprove(Context ctx, BoolExpr f, BoolExpr assumption)
+ void Disprove(Context ctx, BoolExpr f, boolean useMBQI, BoolExpr assumption)
throws Z3Exception, TestFailedException
{
BoolExpr[] a = { assumption };
- Disprove(ctx, f, a);
+ Disprove(ctx, f, useMBQI, a);
}
- void Disprove(Context ctx, BoolExpr f, BoolExpr[] assumptions)
- throws Z3Exception, TestFailedException
+ void Disprove(Context ctx, BoolExpr f, boolean useMBQI,
+ BoolExpr[] assumptions) throws Z3Exception, TestFailedException
{
System.out.println("Disproving: " + f);
Solver s = ctx.MkSolver();
+ Params p = ctx.MkParams();
+ p.Add("mbqi", useMBQI);
+ s.setParameters(p);
for (BoolExpr a : assumptions)
s.Assert(a);
s.Assert(ctx.MkNot(f));
@@ -331,7 +339,7 @@ class JavaExample
ctx.MkRealSort());
ArithExpr yr = (ArithExpr) ctx.MkConst(ctx.MkSymbol("y"),
ctx.MkRealSort());
- Goal g4 = ctx.MkGoal(true, false, true);
+ Goal g4 = ctx.MkGoal(true, false, false);
g4.Assert(ctx.MkGt(xr, ctx.MkReal(10, 1)));
g4.Assert(ctx.MkEq(yr,
ctx.MkAdd(new ArithExpr[] { xr, ctx.MkReal(1, 1) })));
@@ -367,6 +375,7 @@ class JavaExample
void ArrayExample1(Context ctx) throws Z3Exception, TestFailedException
{
System.out.println("ArrayExample1");
+ Log.Append("ArrayExample1");
Goal g = ctx.MkGoal(true, false, false);
ArraySort asort = ctx.MkArraySort(ctx.IntSort(), ctx.MkBitVecSort(32));
@@ -416,6 +425,7 @@ class JavaExample
TestFailedException
{
System.out.println("ArrayExample2");
+ Log.Append("ArrayExample2");
Sort int_type = ctx.IntSort();
Sort array_type = ctx.MkArraySort(int_type, int_type);
@@ -452,7 +462,7 @@ class JavaExample
System.out
.println("prove: store(a1, i1, v1) = store(a2, i2, v2) implies (i1 = i3 or i2 = i3 or select(a1, i3) = select(a2, i3))");
System.out.println(thm);
- Prove(ctx, thm);
+ Prove(ctx, thm, false);
}
// / Show that distinct(a_0, ... , a_n) is
@@ -465,6 +475,7 @@ class JavaExample
TestFailedException
{
System.out.println("ArrayExample3");
+ Log.Append("ArrayExample2");
for (int n = 2; n <= 5; n++)
{
@@ -503,6 +514,7 @@ class JavaExample
void SudokuExample(Context ctx) throws Z3Exception, TestFailedException
{
System.out.println("SudokuExample");
+ Log.Append("SudokuExample");
// 9x9 matrix of integer variables
IntExpr[][] X = new IntExpr[9][];
@@ -609,6 +621,7 @@ class JavaExample
void QuantifierExample1(Context ctx) throws Z3Exception
{
System.out.println("QuantifierExample");
+ Log.Append("QuantifierExample");
Sort[] types = new Sort[3];
IntExpr[] xs = new IntExpr[3];
@@ -654,6 +667,7 @@ class JavaExample
{
System.out.println("QuantifierExample2");
+ Log.Append("QuantifierExample2");
Expr q1, q2;
FuncDecl f = ctx.MkFuncDecl("f", ctx.IntSort(), ctx.IntSort());
@@ -707,97 +721,83 @@ class JavaExample
// / f is injective in the second argument.
- public void QuantifierExample3() throws Z3Exception, TestFailedException
+ public void QuantifierExample3(Context ctx) throws Z3Exception,
+ TestFailedException
{
System.out.println("QuantifierExample3");
-
- HashMap cfg = new HashMap();
- cfg.put("MBQI", "false");
- cfg.put("PROOF_MODE", "2");
- cfg.put("AUTO_CONFIG", "false");
+ Log.Append("QuantifierExample3");
/*
* If quantified formulas are asserted in a logical context, then the
* model produced by Z3 should be viewed as a potential model.
*/
- {
- Context ctx = new Context(cfg);
+ /* declare function f */
+ Sort I = ctx.IntSort();
+ FuncDecl f = ctx.MkFuncDecl("f", new Sort[] { I, I }, I);
- /* declare function f */
- Sort I = ctx.IntSort();
- FuncDecl f = ctx.MkFuncDecl("f", new Sort[] { I, I }, I);
+ /* f is injective in the second argument. */
+ BoolExpr inj = InjAxiom(ctx, f, 1);
- /* f is injective in the second argument. */
- BoolExpr inj = InjAxiom(ctx, f, 1);
+ /* create x, y, v, w, fxy, fwv */
+ Expr x = ctx.MkIntConst("x");
+ Expr y = ctx.MkIntConst("y");
+ Expr v = ctx.MkIntConst("v");
+ Expr w = ctx.MkIntConst("w");
+ Expr fxy = ctx.MkApp(f, new Expr[] { x, y });
+ Expr fwv = ctx.MkApp(f, new Expr[] { w, v });
- /* create x, y, v, w, fxy, fwv */
- Expr x = ctx.MkIntConst("x");
- Expr y = ctx.MkIntConst("y");
- Expr v = ctx.MkIntConst("v");
- Expr w = ctx.MkIntConst("w");
- Expr fxy = ctx.MkApp(f, new Expr[] { x, y });
- Expr fwv = ctx.MkApp(f, new Expr[] { w, v });
+ /* f(x, y) = f(w, v) */
+ BoolExpr p1 = ctx.MkEq(fxy, fwv);
- /* f(x, y) = f(w, v) */
- BoolExpr p1 = ctx.MkEq(fxy, fwv);
+ /* prove f(x, y) = f(w, v) implies y = v */
+ BoolExpr p2 = ctx.MkEq(y, v);
+ Prove(ctx, p2, false, new BoolExpr[] { inj, p1 });
- /* prove f(x, y) = f(w, v) implies y = v */
- BoolExpr p2 = ctx.MkEq(y, v);
- Prove(ctx, p2, new BoolExpr[] { inj, p1 });
-
- /* disprove f(x, y) = f(w, v) implies x = w */
- BoolExpr p3 = ctx.MkEq(x, w);
- Disprove(ctx, p3, new BoolExpr[] { inj, p1 });
- }
+ /* disprove f(x, y) = f(w, v) implies x = w */
+ BoolExpr p3 = ctx.MkEq(x, w);
+ Disprove(ctx, p3, false, new BoolExpr[] { inj, p1 });
}
// / Prove that f(x, y) = f(w, v) implies y = v when
// / f is injective in the second argument.
- public void QuantifierExample4() throws Z3Exception, TestFailedException
+ public void QuantifierExample4(Context ctx) throws Z3Exception, TestFailedException
{
System.out.println("QuantifierExample4");
-
- HashMap cfg = new HashMap();
- cfg.put("MBQI", "false");
- cfg.put("PROOF_MODE", "2");
- cfg.put("AUTO_CONFIG", "false");
+ Log.Append("QuantifierExample4");
/*
* If quantified formulas are asserted in a logical context, then the
* model produced by Z3 should be viewed as a potential model.
*/
- {
- Context ctx = new Context(cfg);
- /* declare function f */
- Sort I = ctx.IntSort();
- FuncDecl f = ctx.MkFuncDecl("f", new Sort[] { I, I }, I);
+ /* declare function f */
+ Sort I = ctx.IntSort();
+ FuncDecl f = ctx.MkFuncDecl("f", new Sort[] { I, I }, I);
- /* f is injective in the second argument. */
- BoolExpr inj = InjAxiomAbs(ctx, f, 1);
+ /* f is injective in the second argument. */
+ BoolExpr inj = InjAxiomAbs(ctx, f, 1);
- /* create x, y, v, w, fxy, fwv */
- Expr x = ctx.MkIntConst("x");
- Expr y = ctx.MkIntConst("y");
- Expr v = ctx.MkIntConst("v");
- Expr w = ctx.MkIntConst("w");
- Expr fxy = ctx.MkApp(f, new Expr[] { x, y });
- Expr fwv = ctx.MkApp(f, new Expr[] { w, v });
+ /* create x, y, v, w, fxy, fwv */
+ Expr x = ctx.MkIntConst("x");
+ Expr y = ctx.MkIntConst("y");
+ Expr v = ctx.MkIntConst("v");
+ Expr w = ctx.MkIntConst("w");
+ Expr fxy = ctx.MkApp(f, new Expr[] { x, y });
+ Expr fwv = ctx.MkApp(f, new Expr[] { w, v });
- /* f(x, y) = f(w, v) */
- BoolExpr p1 = ctx.MkEq(fxy, fwv);
+ /* f(x, y) = f(w, v) */
+ BoolExpr p1 = ctx.MkEq(fxy, fwv);
- /* prove f(x, y) = f(w, v) implies y = v */
- BoolExpr p2 = ctx.MkEq(y, v);
- Prove(ctx, p2, new BoolExpr[] { inj, p1 });
+ /* prove f(x, y) = f(w, v) implies y = v */
+ BoolExpr p2 = ctx.MkEq(y, v);
+ Prove(ctx, p2, false, new BoolExpr[] { inj, p1 });
- /* disprove f(x, y) = f(w, v) implies x = w */
- BoolExpr p3 = ctx.MkEq(x, w);
- Disprove(ctx, p3, new BoolExpr[] { inj, p1 });
- }
+ /* disprove f(x, y) = f(w, v) implies x = w */
+ BoolExpr p3 = ctx.MkEq(x, w);
+ Disprove(ctx, p3, false, new BoolExpr[] { inj, p1 });
}
// / Some basic tests.
@@ -824,7 +824,7 @@ class JavaExample
BoolExpr trivial_eq = ctx.MkEq(fapp, fapp);
BoolExpr nontrivial_eq = ctx.MkEq(fapp, fapp2);
- Goal g = ctx.MkGoal(true, false, true);
+ Goal g = ctx.MkGoal(true, false, false);
g.Assert(trivial_eq);
g.Assert(nontrivial_eq);
System.out.println("Goal: " + g);
@@ -910,7 +910,7 @@ class JavaExample
IntExpr i = ctx.MkInt("1/2");
throw new TestFailedException(); // unreachable
} catch (Z3Exception e)
- {
+ {
}
}
@@ -1081,7 +1081,7 @@ class JavaExample
{
HashMap cfg = new HashMap();
- cfg.put("MODEL", "true");
+ cfg.put("model", "true");
Context ctx = new Context(cfg);
Expr a = ctx.ParseSMTLIB2File(filename, null, null, null, null);
@@ -1117,6 +1117,7 @@ class JavaExample
void LogicExample(Context ctx) throws Z3Exception, TestFailedException
{
System.out.println("LogicTest");
+ Log.Append("LogicTest");
Context.ToggleWarningMessages(true);
@@ -1132,7 +1133,7 @@ class JavaExample
System.out.println("solver result: " + res);
// Or perhaps a tactic for QF_BV
- Goal g = ctx.MkGoal(true, false, true);
+ Goal g = ctx.MkGoal(true, false, false);
g.Assert(eq);
Tactic t = ctx.MkTactic("qfbv");
@@ -1148,13 +1149,14 @@ class JavaExample
void ParOrExample(Context ctx) throws Z3Exception, TestFailedException
{
System.out.println("ParOrExample");
+ Log.Append("ParOrExample");
BitVecSort bvs = ctx.MkBitVecSort(32);
Expr x = ctx.MkConst("x", bvs);
Expr y = ctx.MkConst("y", bvs);
BoolExpr q = ctx.MkEq(x, y);
- Goal g = ctx.MkGoal(true, false, true);
+ Goal g = ctx.MkGoal(true, false, false);
g.Assert(q);
Tactic t1 = ctx.MkTactic("qfbv");
@@ -1179,6 +1181,7 @@ class JavaExample
TestFailedException
{
System.out.println("FindModelExample1");
+ Log.Append("FindModelExample1");
BoolExpr x = ctx.MkBoolConst("x");
BoolExpr y = ctx.MkBoolConst("y");
@@ -1195,7 +1198,8 @@ class JavaExample
public void FindModelExample2(Context ctx) throws Z3Exception,
TestFailedException
{
- System.out.println("find_model_example2");
+ System.out.println("FindModelExample2");
+ Log.Append("FindModelExample2");
IntExpr x = ctx.MkIntConst("x");
IntExpr y = ctx.MkIntConst("y");
@@ -1235,6 +1239,7 @@ class JavaExample
TestFailedException
{
System.out.println("ProveExample1");
+ Log.Append("ProveExample1");
/* create uninterpreted type. */
Sort U = ctx.MkUninterpretedSort(ctx.MkSymbol("U"));
@@ -1255,7 +1260,7 @@ class JavaExample
/* prove g(x) = g(y) */
BoolExpr f = ctx.MkEq(gx, gy);
System.out.println("prove: x = y implies g(x) = g(y)");
- Prove(ctx, ctx.MkImplies(eq, f));
+ Prove(ctx, ctx.MkImplies(eq, f), false);
/* create g(g(x)) */
Expr ggx = g.Apply(gx);
@@ -1263,7 +1268,7 @@ class JavaExample
/* disprove g(g(x)) = g(y) */
f = ctx.MkEq(ggx, gy);
System.out.println("disprove: x = y implies g(g(x)) = g(y)");
- Disprove(ctx, ctx.MkImplies(eq, f));
+ Disprove(ctx, ctx.MkImplies(eq, f), false);
/* Print the model using the custom model printer */
Model m = Check(ctx, ctx.MkNot(f), Status.SATISFIABLE);
@@ -1281,6 +1286,7 @@ class JavaExample
TestFailedException
{
System.out.println("ProveExample2");
+ Log.Append("ProveExample2");
/* declare function g */
Sort I = ctx.IntSort();
@@ -1318,14 +1324,14 @@ class JavaExample
BoolExpr f = ctx.MkLt(z, zero);
System.out
.println("prove: not(g(g(x) - g(y)) = g(z)), x + z <= y <= x implies z < 0");
- Prove(ctx, f, new BoolExpr[] { c1, c2, c3 });
+ Prove(ctx, f, false, new BoolExpr[] { c1, c2, c3 });
/* disprove z < -1 */
IntExpr minus_one = ctx.MkInt(-1);
f = ctx.MkLt(z, minus_one);
System.out
.println("disprove: not(g(g(x) - g(y)) = g(z)), x + z <= y <= x implies z < -1");
- Disprove(ctx, f, new BoolExpr[] { c1, c2, c3 });
+ Disprove(ctx, f, false, new BoolExpr[] { c1, c2, c3 });
}
// / Show how push & pop can be used to create "backtracking" points.
@@ -1336,6 +1342,7 @@ class JavaExample
TestFailedException
{
System.out.println("PushPopExample1");
+ Log.Append("PushPopExample1");
/* create a big number */
IntSort int_type = ctx.IntSort();
@@ -1402,6 +1409,7 @@ class JavaExample
TestFailedException
{
System.out.println("TupleExample");
+ Log.Append("TupleExample");
Sort int_type = ctx.IntSort();
TupleSort tuple = ctx.MkTupleSort(ctx.MkSymbol("mk_tuple"), // name of
@@ -1423,7 +1431,7 @@ class JavaExample
Expr n2 = first.Apply(n1);
BoolExpr n3 = ctx.MkEq(x, n2);
System.out.println("Tuple example: " + n3);
- Prove(ctx, n3);
+ Prove(ctx, n3, false);
}
// / Simple bit-vector example.
@@ -1436,6 +1444,7 @@ class JavaExample
TestFailedException
{
System.out.println("BitvectorExample1");
+ Log.Append("BitvectorExample1");
Sort bv_type = ctx.MkBitVecSort(32);
BitVecExpr x = (BitVecExpr) ctx.MkConst("x", bv_type);
@@ -1448,7 +1457,7 @@ class JavaExample
BoolExpr thm = ctx.MkIff(c1, c2);
System.out
.println("disprove: x - 10 <= 0 IFF x <= 10 for (32-bit) machine integers");
- Disprove(ctx, thm);
+ Disprove(ctx, thm, false);
}
// / Find x and y such that: x ^ y - 103 == x * y
@@ -1457,6 +1466,7 @@ class JavaExample
TestFailedException
{
System.out.println("BitvectorExample2");
+ Log.Append("BitvectorExample2");
/* construct x ^ y - 103 == x * y */
Sort bv_type = ctx.MkBitVecSort(32);
@@ -1482,6 +1492,7 @@ class JavaExample
TestFailedException
{
System.out.println("ParserExample1");
+ Log.Append("ParserExample1");
ctx.ParseSMTLIBString(
"(benchmark tst :extrafuns ((x Int) (y Int)) :formula (> x y) :formula (> x 0))",
@@ -1499,6 +1510,7 @@ class JavaExample
TestFailedException
{
System.out.println("ParserExample2");
+ Log.Append("ParserExample2");
Symbol[] declNames = { ctx.MkSymbol("a"), ctx.MkSymbol("b") };
FuncDecl a = ctx.MkConstDecl(declNames[0], ctx.MkIntSort());
@@ -1517,6 +1529,7 @@ class JavaExample
public void ParserExample3(Context ctx) throws Exception
{
System.out.println("ParserExample3");
+ Log.Append("ParserExample3");
/* declare function g */
Sort I = ctx.MkIntSort();
@@ -1531,7 +1544,7 @@ class JavaExample
BoolExpr thm = ctx.SMTLIBFormulas()[0];
System.out.println("formula: " + thm);
- Prove(ctx, thm, ca);
+ Prove(ctx, thm, false, ca);
}
// / Display the declarations, assumptions and formulas in a SMT-LIB string.
@@ -1539,6 +1552,7 @@ class JavaExample
public void ParserExample4(Context ctx) throws Z3Exception
{
System.out.println("ParserExample4");
+ Log.Append("ParserExample4");
ctx.ParseSMTLIBString(
"(benchmark tst :extrafuns ((x Int) (y Int)) :assumption (= x 20) :formula (> x y) :formula (> x 0))",
@@ -1585,6 +1599,7 @@ class JavaExample
public void ITEExample(Context ctx) throws Z3Exception
{
System.out.println("ITEExample");
+ Log.Append("ITEExample");
BoolExpr f = ctx.MkFalse();
Expr one = ctx.MkInt(1);
@@ -1600,6 +1615,7 @@ class JavaExample
TestFailedException
{
System.out.println("EnumExample");
+ Log.Append("EnumExample");
Symbol name = ctx.MkSymbol("fruit");
@@ -1620,15 +1636,16 @@ class JavaExample
Expr orange = fruit.Consts()[2];
/* Apples are different from oranges */
- Prove(ctx, ctx.MkNot(ctx.MkEq(apple, orange)));
+ Prove(ctx, ctx.MkNot(ctx.MkEq(apple, orange)), false);
/* Apples pass the apple test */
- Prove(ctx, (BoolExpr) ctx.MkApp(fruit.TesterDecls()[0], apple));
+ Prove(ctx, (BoolExpr) ctx.MkApp(fruit.TesterDecls()[0], apple), false);
/* Oranges fail the apple test */
- Disprove(ctx, (BoolExpr) ctx.MkApp(fruit.TesterDecls()[0], orange));
+ Disprove(ctx, (BoolExpr) ctx.MkApp(fruit.TesterDecls()[0], orange),
+ false);
Prove(ctx, (BoolExpr) ctx.MkNot((BoolExpr) ctx.MkApp(
- fruit.TesterDecls()[0], orange)));
+ fruit.TesterDecls()[0], orange)), false);
Expr fruity = ctx.MkConst("fruity", fruit);
@@ -1636,7 +1653,8 @@ class JavaExample
Prove(ctx,
ctx.MkOr(new BoolExpr[] { ctx.MkEq(fruity, apple),
- ctx.MkEq(fruity, banana), ctx.MkEq(fruity, orange) }));
+ ctx.MkEq(fruity, banana), ctx.MkEq(fruity, orange) }),
+ false);
}
// / Create a list datatype.
@@ -1645,6 +1663,7 @@ class JavaExample
TestFailedException
{
System.out.println("ListExample");
+ Log.Append("ListExample");
Sort int_ty;
ListSort int_list;
@@ -1660,25 +1679,25 @@ class JavaExample
l2 = ctx.MkApp(int_list.ConsDecl(), new Expr[] { ctx.MkInt(2), nil });
/* nil != cons(1, nil) */
- Prove(ctx, ctx.MkNot(ctx.MkEq(nil, l1)));
+ Prove(ctx, ctx.MkNot(ctx.MkEq(nil, l1)), false);
/* cons(2,nil) != cons(1, nil) */
- Prove(ctx, ctx.MkNot(ctx.MkEq(l1, l2)));
+ Prove(ctx, ctx.MkNot(ctx.MkEq(l1, l2)), false);
/* cons(x,nil) = cons(y, nil) => x = y */
x = ctx.MkConst("x", int_ty);
y = ctx.MkConst("y", int_ty);
l1 = ctx.MkApp(int_list.ConsDecl(), new Expr[] { x, nil });
l2 = ctx.MkApp(int_list.ConsDecl(), new Expr[] { y, nil });
- Prove(ctx, ctx.MkImplies(ctx.MkEq(l1, l2), ctx.MkEq(x, y)));
+ Prove(ctx, ctx.MkImplies(ctx.MkEq(l1, l2), ctx.MkEq(x, y)), false);
/* cons(x,u) = cons(x, v) => u = v */
u = ctx.MkConst("u", int_list);
v = ctx.MkConst("v", int_list);
l1 = ctx.MkApp(int_list.ConsDecl(), new Expr[] { x, u });
l2 = ctx.MkApp(int_list.ConsDecl(), new Expr[] { y, v });
- Prove(ctx, ctx.MkImplies(ctx.MkEq(l1, l2), ctx.MkEq(u, v)));
- Prove(ctx, ctx.MkImplies(ctx.MkEq(l1, l2), ctx.MkEq(x, y)));
+ Prove(ctx, ctx.MkImplies(ctx.MkEq(l1, l2), ctx.MkEq(u, v)), false);
+ Prove(ctx, ctx.MkImplies(ctx.MkEq(l1, l2), ctx.MkEq(x, y)), false);
/* is_nil(u) or is_cons(u) */
Prove(ctx,
@@ -1686,10 +1705,10 @@ class JavaExample
(BoolExpr) ctx.MkApp(int_list.IsNilDecl(),
new Expr[] { u }),
(BoolExpr) ctx.MkApp(int_list.IsConsDecl(),
- new Expr[] { u }) }));
+ new Expr[] { u }) }), false);
/* occurs check u != cons(x,u) */
- Prove(ctx, ctx.MkNot(ctx.MkEq(u, l1)));
+ Prove(ctx, ctx.MkNot(ctx.MkEq(u, l1)), false);
/* destructors: is_cons(u) => u = cons(head(u),tail(u)) */
fml1 = ctx.MkEq(u, ctx.MkApp(int_list.ConsDecl(),
@@ -1700,9 +1719,9 @@ class JavaExample
fml1);
System.out.println("Formula " + fml);
- Prove(ctx, fml);
+ Prove(ctx, fml, false);
- Disprove(ctx, fml1);
+ Disprove(ctx, fml1, false);
}
// / Create a binary tree datatype.
@@ -1711,6 +1730,7 @@ class JavaExample
TestFailedException
{
System.out.println("TreeExample");
+ Log.Append("TreeExample");
Sort cell;
FuncDecl nil_decl, is_nil_decl, cons_decl, is_cons_decl, car_decl, cdr_decl;
@@ -1741,7 +1761,7 @@ class JavaExample
l2 = ctx.MkApp(cons_decl, new Expr[] { l1, nil });
/* nil != cons(nil, nil) */
- Prove(ctx, ctx.MkNot(ctx.MkEq(nil, l1)));
+ Prove(ctx, ctx.MkNot(ctx.MkEq(nil, l1)), false);
/* cons(x,u) = cons(x, v) => u = v */
u = ctx.MkConst("u", cell);
@@ -1750,17 +1770,18 @@ class JavaExample
y = ctx.MkConst("y", cell);
l1 = ctx.MkApp(cons_decl, new Expr[] { x, u });
l2 = ctx.MkApp(cons_decl, new Expr[] { y, v });
- Prove(ctx, ctx.MkImplies(ctx.MkEq(l1, l2), ctx.MkEq(u, v)));
- Prove(ctx, ctx.MkImplies(ctx.MkEq(l1, l2), ctx.MkEq(x, y)));
+ Prove(ctx, ctx.MkImplies(ctx.MkEq(l1, l2), ctx.MkEq(u, v)), false);
+ Prove(ctx, ctx.MkImplies(ctx.MkEq(l1, l2), ctx.MkEq(x, y)), false);
/* is_nil(u) or is_cons(u) */
Prove(ctx,
ctx.MkOr(new BoolExpr[] {
(BoolExpr) ctx.MkApp(is_nil_decl, new Expr[] { u }),
- (BoolExpr) ctx.MkApp(is_cons_decl, new Expr[] { u }) }));
+ (BoolExpr) ctx.MkApp(is_cons_decl, new Expr[] { u }) }),
+ false);
/* occurs check u != cons(x,u) */
- Prove(ctx, ctx.MkNot(ctx.MkEq(u, l1)));
+ Prove(ctx, ctx.MkNot(ctx.MkEq(u, l1)), false);
/* destructors: is_cons(u) => u = cons(car(u),cdr(u)) */
fml1 = ctx.MkEq(
@@ -1771,9 +1792,9 @@ class JavaExample
ctx.MkApp(cdr_decl, u) }));
fml = ctx.MkImplies((BoolExpr) ctx.MkApp(is_cons_decl, u), fml1);
System.out.println("Formula " + fml);
- Prove(ctx, fml);
+ Prove(ctx, fml, false);
- Disprove(ctx, fml1);
+ Disprove(ctx, fml1, false);
}
// / Create a forest of trees.
@@ -1786,6 +1807,7 @@ class JavaExample
TestFailedException
{
System.out.println("ForestExample");
+ Log.Append("ForestExample");
Sort tree, forest;
FuncDecl nil1_decl, is_nil1_decl, cons1_decl, is_cons1_decl, car1_decl, cdr1_decl;
@@ -1874,8 +1896,8 @@ class JavaExample
f3 = ctx.MkApp(cons1_decl, new Expr[] { t1, f1 });
/* nil != cons(nil,nil) */
- Prove(ctx, ctx.MkNot(ctx.MkEq(nil1, f1)));
- Prove(ctx, ctx.MkNot(ctx.MkEq(nil2, t1)));
+ Prove(ctx, ctx.MkNot(ctx.MkEq(nil1, f1)), false);
+ Prove(ctx, ctx.MkNot(ctx.MkEq(nil2, t1)), false);
/* cons(x,u) = cons(x, v) => u = v */
u = ctx.MkConst("u", forest);
@@ -1884,16 +1906,16 @@ class JavaExample
y = ctx.MkConst("y", tree);
l1 = ctx.MkApp(cons1_decl, new Expr[] { x, u });
l2 = ctx.MkApp(cons1_decl, new Expr[] { y, v });
- Prove(ctx, ctx.MkImplies(ctx.MkEq(l1, l2), ctx.MkEq(u, v)));
- Prove(ctx, ctx.MkImplies(ctx.MkEq(l1, l2), ctx.MkEq(x, y)));
+ Prove(ctx, ctx.MkImplies(ctx.MkEq(l1, l2), ctx.MkEq(u, v)), false);
+ Prove(ctx, ctx.MkImplies(ctx.MkEq(l1, l2), ctx.MkEq(x, y)), false);
/* is_nil(u) or is_cons(u) */
Prove(ctx, ctx.MkOr(new BoolExpr[] {
(BoolExpr) ctx.MkApp(is_nil1_decl, new Expr[] { u }),
- (BoolExpr) ctx.MkApp(is_cons1_decl, new Expr[] { u }) }));
+ (BoolExpr) ctx.MkApp(is_cons1_decl, new Expr[] { u }) }), false);
/* occurs check u != cons(x,u) */
- Prove(ctx, ctx.MkNot(ctx.MkEq(u, l1)));
+ Prove(ctx, ctx.MkNot(ctx.MkEq(u, l1)), false);
}
// / Demonstrate how to use #Eval.
@@ -1901,6 +1923,7 @@ class JavaExample
public void EvalExample1(Context ctx) throws Z3Exception
{
System.out.println("EvalExample1");
+ Log.Append("EvalExample1");
IntExpr x = ctx.MkIntConst("x");
IntExpr y = ctx.MkIntConst("y");
@@ -1940,6 +1963,7 @@ class JavaExample
public void EvalExample2(Context ctx) throws Z3Exception
{
System.out.println("EvalExample2");
+ Log.Append("EvalExample2");
Sort int_type = ctx.IntSort();
TupleSort tuple = ctx.MkTupleSort(ctx.MkSymbol("mk_tuple"), // name of
@@ -2063,6 +2087,7 @@ class JavaExample
public void FindSmallModelExample(Context ctx) throws Z3Exception
{
System.out.println("FindSmallModelExample");
+ Log.Append("FindSmallModelExample");
BitVecExpr x = ctx.MkBVConst("x", 32);
BitVecExpr y = ctx.MkBVConst("y", 32);
@@ -2079,6 +2104,7 @@ class JavaExample
public void SimplifierExample(Context ctx) throws Z3Exception
{
System.out.println("SimplifierExample");
+ Log.Append("SimplifierExample");
IntExpr x = ctx.MkIntConst("x");
IntExpr y = ctx.MkIntConst("y");
@@ -2095,48 +2121,42 @@ class JavaExample
// / Extract unsatisfiable core example
- public void UnsatCoreAndProofExample() throws Z3Exception
+ public void UnsatCoreAndProofExample(Context ctx) throws Z3Exception
{
System.out.println("UnsatCoreAndProofExample");
+ Log.Append("UnsatCoreAndProofExample");
- HashMap cfg = new HashMap();
- cfg.put("PROOF_MODE", "2");
+ Solver solver = ctx.MkSolver();
+ BoolExpr pa = ctx.MkBoolConst("PredA");
+ BoolExpr pb = ctx.MkBoolConst("PredB");
+ BoolExpr pc = ctx.MkBoolConst("PredC");
+ BoolExpr pd = ctx.MkBoolConst("PredD");
+ BoolExpr p1 = ctx.MkBoolConst("P1");
+ BoolExpr p2 = ctx.MkBoolConst("P2");
+ BoolExpr p3 = ctx.MkBoolConst("P3");
+ BoolExpr p4 = ctx.MkBoolConst("P4");
+ BoolExpr[] assumptions = new BoolExpr[] { ctx.MkNot(p1), ctx.MkNot(p2),
+ ctx.MkNot(p3), ctx.MkNot(p4) };
+ BoolExpr f1 = ctx.MkAnd(new BoolExpr[] { pa, pb, pc });
+ BoolExpr f2 = ctx.MkAnd(new BoolExpr[] { pa, ctx.MkNot(pb), pc });
+ BoolExpr f3 = ctx.MkOr(new BoolExpr[] { ctx.MkNot(pa), ctx.MkNot(pc) });
+ BoolExpr f4 = pd;
+
+ solver.Assert(ctx.MkOr(new BoolExpr[] { f1, p1 }));
+ solver.Assert(ctx.MkOr(new BoolExpr[] { f2, p2 }));
+ solver.Assert(ctx.MkOr(new BoolExpr[] { f3, p3 }));
+ solver.Assert(ctx.MkOr(new BoolExpr[] { f4, p4 }));
+ Status result = solver.Check(assumptions);
+
+ if (result == Status.UNSATISFIABLE)
{
- Context ctx = new Context(cfg);
- Solver solver = ctx.MkSolver();
-
- BoolExpr pa = ctx.MkBoolConst("PredA");
- BoolExpr pb = ctx.MkBoolConst("PredB");
- BoolExpr pc = ctx.MkBoolConst("PredC");
- BoolExpr pd = ctx.MkBoolConst("PredD");
- BoolExpr p1 = ctx.MkBoolConst("P1");
- BoolExpr p2 = ctx.MkBoolConst("P2");
- BoolExpr p3 = ctx.MkBoolConst("P3");
- BoolExpr p4 = ctx.MkBoolConst("P4");
- BoolExpr[] assumptions = new BoolExpr[] { ctx.MkNot(p1),
- ctx.MkNot(p2), ctx.MkNot(p3), ctx.MkNot(p4) };
- BoolExpr f1 = ctx.MkAnd(new BoolExpr[] { pa, pb, pc });
- BoolExpr f2 = ctx.MkAnd(new BoolExpr[] { pa, ctx.MkNot(pb), pc });
- BoolExpr f3 = ctx.MkOr(new BoolExpr[] { ctx.MkNot(pa),
- ctx.MkNot(pc) });
- BoolExpr f4 = pd;
-
- solver.Assert(ctx.MkOr(new BoolExpr[] { f1, p1 }));
- solver.Assert(ctx.MkOr(new BoolExpr[] { f2, p2 }));
- solver.Assert(ctx.MkOr(new BoolExpr[] { f3, p3 }));
- solver.Assert(ctx.MkOr(new BoolExpr[] { f4, p4 }));
- Status result = solver.Check(assumptions);
-
- if (result == Status.UNSATISFIABLE)
+ System.out.println("unsat");
+ System.out.println("proof: " + solver.Proof());
+ System.out.println("core: ");
+ for (Expr c : solver.UnsatCore())
{
- System.out.println("unsat");
- System.out.println("proof: " + solver.Proof());
- System.out.println("core: ");
- for (Expr c : solver.UnsatCore())
- {
- System.out.println(c);
- }
+ System.out.println(c);
}
}
}
@@ -2144,6 +2164,7 @@ class JavaExample
public void FiniteDomainExample(Context ctx) throws Z3Exception
{
System.out.println("FiniteDomainExample");
+ Log.Append("FiniteDomainExample");
FiniteDomainSort s = ctx.MkFiniteDomainSort("S", 10);
FiniteDomainSort t = ctx.MkFiniteDomainSort("T", 10);
@@ -2174,10 +2195,9 @@ class JavaExample
p.SimpleExample();
- {
+ { // These examples need model generation turned on.
HashMap cfg = new HashMap();
- cfg.put("MODEL", "true");
- cfg.put("PROOF_MODE", "2");
+ cfg.put("model", "true");
Context ctx = new Context(cfg);
p.BasicTests(ctx);
p.CastingTest(ctx);
@@ -2188,25 +2208,16 @@ class JavaExample
p.ParOrExample(ctx);
p.FindModelExample1(ctx);
p.FindModelExample2(ctx);
- p.ProveExample1(ctx);
- p.ProveExample2(ctx);
p.PushPopExample1(ctx);
p.ArrayExample1(ctx);
- p.ArrayExample2(ctx);
p.ArrayExample3(ctx);
- p.TupleExample(ctx);
p.BitvectorExample1(ctx);
p.BitvectorExample2(ctx);
p.ParserExample1(ctx);
p.ParserExample2(ctx);
- p.ParserExample3(ctx);
p.ParserExample4(ctx);
p.ParserExample5(ctx);
p.ITEExample(ctx);
- p.EnumExample(ctx);
- p.ListExample(ctx);
- p.TreeExample(ctx);
- p.ForestExample(ctx);
p.EvalExample1(ctx);
p.EvalExample2(ctx);
p.FindSmallModelExample(ctx);
@@ -2214,9 +2225,31 @@ class JavaExample
p.FiniteDomainExample(ctx);
}
- p.QuantifierExample3();
- p.QuantifierExample4();
- p.UnsatCoreAndProofExample();
+ { // These examples need proof generation turned on.
+ HashMap cfg = new HashMap();
+ cfg.put("proof", "true");
+ Context ctx = new Context(cfg);
+ p.ProveExample1(ctx);
+ p.ProveExample2(ctx);
+ p.ArrayExample2(ctx);
+ p.TupleExample(ctx);
+ p.ParserExample3(ctx);
+ p.EnumExample(ctx);
+ p.ListExample(ctx);
+ p.TreeExample(ctx);
+ p.ForestExample(ctx);
+ p.UnsatCoreAndProofExample(ctx);
+ }
+
+ { // These examples need proof generation turned on and auto-config
+ // set to false.
+ HashMap cfg = new HashMap();
+ cfg.put("proof", "true");
+ cfg.put("auto-config", "false");
+ Context ctx = new Context(cfg);
+ p.QuantifierExample3(ctx);
+ p.QuantifierExample4(ctx);
+ }
Log.Close();
if (Log.isOpen())
diff --git a/src/api/api_config_params.cpp b/src/api/api_config_params.cpp
index 908900043..aaaabb7b2 100644
--- a/src/api/api_config_params.cpp
+++ b/src/api/api_config_params.cpp
@@ -43,6 +43,13 @@ extern "C" {
}
}
+ void Z3_API Z3_global_param_reset_all() {
+ memory::initialize(UINT_MAX);
+ LOG_Z3_global_param_reset_all();
+ gparams::reset();
+ env_params::updt_params();
+ }
+
std::string g_Z3_global_param_get_buffer;
Z3_bool_opt Z3_API Z3_global_param_get(Z3_string param_id, Z3_string_ptr param_value) {
diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp
index f197e8ad8..69b7ea999 100644
--- a/src/api/api_context.cpp
+++ b/src/api/api_context.cpp
@@ -80,7 +80,7 @@ namespace api {
}
context::context(context_params * p, bool user_ref_count):
- m_params(*p),
+ m_params(p != 0 ? *p : context_params()),
m_user_ref_count(user_ref_count),
m_manager(m_params.m_proof ? PGM_FINE : PGM_DISABLED, m_params.m_trace ? m_params.m_trace_file_name.c_str() : 0),
m_plugins(m_manager),
diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp
index 80577efee..f26ffeeba 100644
--- a/src/api/api_model.cpp
+++ b/src/api/api_model.cpp
@@ -201,7 +201,7 @@ extern "C" {
LOG_Z3_get_as_array_func_decl(c, a);
RESET_ERROR_CODE();
if (is_expr(to_ast(a)) && is_app_of(to_expr(a), mk_c(c)->get_array_fid(), OP_AS_ARRAY)) {
- return of_func_decl(to_func_decl(to_app(a)->get_decl()->get_parameter(0).get_ast()));
+ RETURN_Z3(of_func_decl(to_func_decl(to_app(a)->get_decl()->get_parameter(0).get_ast())));
}
else {
SET_ERROR_CODE(Z3_INVALID_ARG);
diff --git a/src/api/api_params.cpp b/src/api/api_params.cpp
index 74899bc44..19634af32 100644
--- a/src/api/api_params.cpp
+++ b/src/api/api_params.cpp
@@ -66,7 +66,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_params_set_bool(c, p, k, v);
RESET_ERROR_CODE();
- to_params(p)->m_params.set_bool(to_symbol(k), v != 0);
+ to_params(p)->m_params.set_bool(norm_param_name(to_symbol(k)).c_str(), v != 0);
Z3_CATCH;
}
@@ -77,7 +77,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_params_set_uint(c, p, k, v);
RESET_ERROR_CODE();
- to_params(p)->m_params.set_uint(to_symbol(k), v);
+ to_params(p)->m_params.set_uint(norm_param_name(to_symbol(k)).c_str(), v);
Z3_CATCH;
}
@@ -88,7 +88,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_params_set_double(c, p, k, v);
RESET_ERROR_CODE();
- to_params(p)->m_params.set_double(to_symbol(k), v);
+ to_params(p)->m_params.set_double(norm_param_name(to_symbol(k)).c_str(), v);
Z3_CATCH;
}
@@ -99,7 +99,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_params_set_symbol(c, p, k, v);
RESET_ERROR_CODE();
- to_params(p)->m_params.set_sym(to_symbol(k), to_symbol(v));
+ to_params(p)->m_params.set_sym(norm_param_name(to_symbol(k)).c_str(), to_symbol(v));
Z3_CATCH;
}
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 7fc36575a..fca009cea 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -64,6 +64,11 @@ namespace z3 {
class apply_result;
class fixedpoint;
+ inline void set_param(char const * param, char const * value) { Z3_global_param_set(param, value); }
+ inline void set_param(char const * param, bool value) { Z3_global_param_set(param, value ? "true" : "false"); }
+ inline void set_param(char const * param, int value) { std::ostringstream oss; oss << value; Z3_global_param_set(param, oss.str().c_str()); }
+ inline void reset_params() { Z3_global_param_reset_all(); }
+
/**
\brief Exception used to sign API usage errors.
*/
diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index ff36b4553..aee60c43f 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -3657,6 +3657,7 @@ namespace Microsoft.Z3
Goal_DRQ.Clear(this);
Model_DRQ.Clear(this);
Params_DRQ.Clear(this);
+ ParamDescrs_DRQ.Clear(this);
Probe_DRQ.Clear(this);
Solver_DRQ.Clear(this);
Statistics_DRQ.Clear(this);
diff --git a/src/api/dotnet/IDecRefQueue.cs b/src/api/dotnet/IDecRefQueue.cs
index e6276c4f4..d741a8f05 100644
--- a/src/api/dotnet/IDecRefQueue.cs
+++ b/src/api/dotnet/IDecRefQueue.cs
@@ -24,7 +24,7 @@ using System.Threading;
using System.Diagnostics.Contracts;
namespace Microsoft.Z3
-{
+{
[ContractClass(typeof(DecRefQueueContracts))]
internal abstract class IDecRefQueue
{
@@ -35,7 +35,7 @@ namespace Microsoft.Z3
{
Contract.Invariant(this.m_queue != null);
}
-
+
#endregion
readonly internal protected Object m_lock = new Object();
diff --git a/src/api/dotnet/Microsoft.Z3.csproj b/src/api/dotnet/Microsoft.Z3.csproj
index 762b83b28..a1bb868eb 100644
--- a/src/api/dotnet/Microsoft.Z3.csproj
+++ b/src/api/dotnet/Microsoft.Z3.csproj
@@ -252,6 +252,71 @@
;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules
true
+
+ true
+ bin\x86\Debug\
+ DEBUG;TRACE
+ true
+ full
+ x86
+ ..\Debug\Microsoft.Z3.dll.CodeAnalysisLog.xml
+ true
+ GlobalSuppressions.cs
+ prompt
+ MinimumRecommendedRules.ruleset
+ ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets
+ ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules
+
+
+ bin\x86\Release\
+ true
+ ..\external\Microsoft.Z3.xml
+ true
+ pdbonly
+ x86
+ ..\external\Microsoft.Z3.dll.CodeAnalysisLog.xml
+ true
+ GlobalSuppressions.cs
+ prompt
+ MinimumRecommendedRules.ruleset
+ ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets
+ ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules
+
+
+ bin\x86\external\
+ true
+ ..\external\Microsoft.Z3.xml
+ true
+ pdbonly
+ x86
+ bin\Release\Microsoft.Z3.dll.CodeAnalysisLog.xml
+ true
+ GlobalSuppressions.cs
+ prompt
+ MinimumRecommendedRules.ruleset
+ ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets
+ true
+ ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules
+ true
+
+
+ bin\x86\Release_delaysign\
+ DELAYSIGN
+ true
+ ..\Release_delaysign\Microsoft.Z3.xml
+ true
+ pdbonly
+ x86
+ ..\release\Microsoft.Z3.dll.CodeAnalysisLog.xml
+ true
+ GlobalSuppressions.cs
+ prompt
+ MinimumRecommendedRules.ruleset
+ ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets
+ true
+ ;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules
+ true
+
diff --git a/src/api/java/Params.java b/src/api/java/Params.java
index 3bc8b4574..c954c50e5 100644
--- a/src/api/java/Params.java
+++ b/src/api/java/Params.java
@@ -44,8 +44,8 @@ public class Params extends Z3Object
**/
public void Add(String name, boolean value) throws Z3Exception
{
- Native.paramsSetBool(Context().nCtx(), NativeObject(), Context()
- .MkSymbol(name).NativeObject(), (value) ? true : false);
+ Native.paramsSetBool(Context().nCtx(), NativeObject(),
+ Context().MkSymbol(name).NativeObject(), value);
}
/**
diff --git a/src/api/python/z3.py b/src/api/python/z3.py
index b03cf1fd8..033626747 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3.py
@@ -198,10 +198,10 @@ def _get_ctx(ctx):
else:
return ctx
-def set_option(*args, **kws):
+def set_param(*args, **kws):
"""Set Z3 global (or module) parameters.
- >>> set_option(precision=10)
+ >>> set_param(precision=10)
"""
if __debug__:
_z3_assert(len(args) % 2 == 0, "Argument list must have an even number of elements.")
@@ -219,11 +219,21 @@ def set_option(*args, **kws):
Z3_global_param_set(str(prev), _to_param_value(a))
prev = None
-def get_option(name):
+def reset_params():
+ """Reset all global (or module) parameters.
+ """
+ Z3_global_param_reset_all()
+
+def set_option(*args, **kws):
+ """Alias for 'set_param' for backward compatibility.
+ """
+ return set_param(*args, **kws)
+
+def get_param(name):
"""Return the value of a Z3 global (or module) parameter
- >>> get_option('nlsat.reorder')
- true
+ >>> get_param('nlsat.reorder')
+ 'true'
"""
ptr = (ctypes.c_char_p * 1)()
if Z3_global_param_get(str(name), ptr):
@@ -4384,8 +4394,8 @@ def args2params(arguments, keywords, ctx=None):
"""Convert python arguments into a Z3_params object.
A ':' is added to the keywords, and '_' is replaced with '-'
- >>> args2params([':model', True, ':relevancy', 2], {'elim_and' : True})
- (params :model 1 :relevancy 2 :elim-and 1)
+ >>> args2params(['model', True, 'relevancy', 2], {'elim_and' : True})
+ (params model 1 relevancy 2 elim_and 1)
"""
if __debug__:
_z3_assert(len(arguments) % 2 == 0, "Argument list must have an even number of elements.")
@@ -4398,7 +4408,6 @@ def args2params(arguments, keywords, ctx=None):
r.set(prev, a)
prev = None
for k, v in keywords.iteritems():
- k = ':' + k.replace('_', '-')
r.set(k, v)
return r
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 16bf9193c..49d59e125 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -1260,6 +1260,17 @@ extern "C" {
def_API('Z3_global_param_set', VOID, (_in(STRING), _in(STRING)))
*/
void Z3_API Z3_global_param_set(__in Z3_string param_id, __in Z3_string param_value);
+
+
+ /**
+ \brief Restore the value of all global (and module) parameters.
+ This command will not affect already created objects (such as tactics and solvers).
+
+ \sa Z3_global_param_set
+
+ def_API('Z3_global_param_reset_all', VOID, ())
+ */
+ void Z3_API Z3_global_param_reset_all();
/**
\brief Get a global (or module) parameter.
@@ -1312,7 +1323,7 @@ extern "C" {
- well_sorted_check type checker
- auto_config use heuristics to automatically select solver and configure it
- model model generation for solvers, this parameter can be overwritten when creating a solver
- - validate_model validate models produced by solvers
+ - model_validate validate models produced by solvers
- unsat_core unsat-core generation for solvers, this parameter can be overwritten when creating a solver
\sa Z3_set_param_value
@@ -1428,7 +1439,7 @@ extern "C" {
/**
\brief Set a value of a context parameter.
- \sa Use #Z3_global_param_set.
+ \sa Z3_global_param_set
def_API('Z3_update_param_value', VOID, (_in(CONTEXT), _in(STRING), _in(STRING)))
*/
@@ -1437,7 +1448,7 @@ extern "C" {
/**
\brief Return the value of a context parameter.
- \sa Use #Z3_global_param_get
+ \sa Z3_global_param_get
def_API('Z3_get_param_value', BOOL, (_in(CONTEXT), _in(STRING), _out(STRING)))
*/
@@ -1707,7 +1718,7 @@ extern "C" {
use the APIs for creating numerals and pass a numeric
constant together with the sort returned by this call.
- \sa Z3_get_finite_domain_sort_size.
+ \sa Z3_get_finite_domain_sort_size
def_API('Z3_mk_finite_domain_sort', SORT, (_in(CONTEXT), _in(SYMBOL), _in(UINT64)))
*/
diff --git a/src/api/z3_replayer.cpp b/src/api/z3_replayer.cpp
index b41ef876c..079516145 100644
--- a/src/api/z3_replayer.cpp
+++ b/src/api/z3_replayer.cpp
@@ -232,8 +232,11 @@ struct z3_replayer::imp {
}
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");
+ }
+ unsigned pos = 0;
m_ptr = 0;
while (true) {
char c = curr();
@@ -246,10 +249,13 @@ struct z3_replayer::imp {
else if ('A' <= c && c <= 'F') {
m_ptr = m_ptr * 16 + 10 + (c - 'A');
}
+ else if (pos == 1 && (c == 'x' || c == 'X')) {
+ // support for 0x.... notation
+ }
else {
return;
}
- next();
+ next(); pos++;
}
}
diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp
index df9efc4dd..8f65485ae 100644
--- a/src/cmd_context/basic_cmds.cpp
+++ b/src/cmd_context/basic_cmds.cpp
@@ -307,7 +307,7 @@ class set_option_cmd : public set_get_option_cmd {
try {
gparams::set(m_option, value);
env_params::updt_params();
- ctx.params().updt_params();
+ ctx.global_params_updated();
}
catch (gparams::exception ex) {
throw cmd_exception(ex.msg());
@@ -517,7 +517,7 @@ public:
}
else {
try {
- std::string val = gparams::get_value(opt);
+ ctx.regular_stream() << gparams::get_value(opt) << std::endl;
}
catch (gparams::exception ex) {
ctx.print_unsupported(opt);
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 19fbdcd3c..0380e91ea 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -38,22 +38,6 @@ Notes:
#include"model_evaluator.h"
#include"for_each_expr.h"
-std::string smt2_keyword_to_param(symbol const & opt) {
- std::string r;
- SASSERT(opt.bare_str()[0] == ':');
- r = opt.bare_str() + 1;
- unsigned sz = static_cast(r.size());
- for (unsigned i = 0; i < sz; i++) {
- char curr = r[i];
- if ('A' <= curr && curr <= 'Z')
- r[i] = curr - 'A' + 'a';
- else if (curr == '-')
- r[i] = '_';
- }
- TRACE("smt2_keyword_to_param", tout << opt << " -> '" << r << "'\n";);
- return r;
-}
-
func_decls::func_decls(ast_manager & m, func_decl * f):
m_decls(TAG(func_decl*, f, 0)) {
m.inc_ref(f);
@@ -358,6 +342,16 @@ cmd_context::~cmd_context() {
m_check_sat_result = 0;
}
+void cmd_context::global_params_updated() {
+ m_params.updt_params();
+ if (m_solver) {
+ params_ref p;
+ if (!m_params.m_auto_config)
+ p.set_bool("auto_config", false);
+ m_solver->updt_params(p);
+ }
+}
+
void cmd_context::set_produce_models(bool f) {
if (m_solver)
m_solver->set_produce_models(f);
@@ -393,7 +387,7 @@ bool cmd_context::well_sorted_check_enabled() const {
}
bool cmd_context::validate_model_enabled() const {
- return m_params.m_validate_model;
+ return m_params.m_model_validate;
}
cmd_context::check_sat_state cmd_context::cs_state() const {
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index ae517b0c2..2edc87ca6 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -38,11 +38,6 @@ Notes:
#include"scoped_ptr_vector.h"
#include"context_params.h"
-/**
- \brief Auxiliary function for converting SMT2 keywords into Z3 internal parameter names.
-*/
-std::string smt2_keyword_to_param(symbol const & k);
-
class func_decls {
func_decl * m_decls;
public:
@@ -254,6 +249,7 @@ public:
cmd_context(bool main_ctx = true, ast_manager * m = 0, symbol const & l = symbol::null);
~cmd_context();
context_params & params() { return m_params; }
+ void global_params_updated(); // this method should be invoked when global (and module) params are updated.
void set_logic(symbol const & s);
bool has_logic() const { return m_logic != symbol::null; }
symbol const & get_logic() const { return m_logic; }
diff --git a/src/cmd_context/context_params.cpp b/src/cmd_context/context_params.cpp
index c7efa0d8d..495f73b75 100644
--- a/src/cmd_context/context_params.cpp
+++ b/src/cmd_context/context_params.cpp
@@ -62,8 +62,8 @@ void context_params::set(char const * param, char const * value) {
else if (p == "model") {
set_bool(m_model, param, value);
}
- else if (p == "validate_model") {
- set_bool(m_validate_model, param, value);
+ else if (p == "model_validate") {
+ set_bool(m_model_validate, param, value);
}
else if (p == "trace") {
set_bool(m_trace, param, value);
@@ -92,7 +92,7 @@ void context_params::updt_params(params_ref const & p) {
m_auto_config = p.get_bool("auto_config", true);
m_proof = p.get_bool("proof", false);
m_model = p.get_bool("model", true);
- m_validate_model = p.get_bool("validate_model", false);
+ m_model_validate = p.get_bool("model_validate", false);
m_trace = p.get_bool("trace", false);
m_trace_file_name = p.get_str("trace_file_name", "z3.log");
m_unsat_core = p.get_bool("unsat_core", false);
@@ -106,7 +106,7 @@ void context_params::collect_param_descrs(param_descrs & d) {
d.insert("auto_config", CPK_BOOL, "use heuristics to automatically select solver and configure it", "true");
d.insert("proof", CPK_BOOL, "proof generation, it must be enabled when the Z3 context is created", "false");
d.insert("model", CPK_BOOL, "model generation for solvers, this parameter can be overwritten when creating a solver", "true");
- d.insert("validate_model", CPK_BOOL, "validate models produced by solvers", "false");
+ d.insert("model_validate", CPK_BOOL, "validate models produced by solvers", "false");
d.insert("trace", CPK_BOOL, "trace generation for VCC", "false");
d.insert("trace_file_name", CPK_STRING, "trace out file name (see option 'trace')", "z3.log");
d.insert("unsat_core", CPK_BOOL, "unsat-core generation for solvers, this parameter can be overwritten when creating a solver, not every solver in Z3 supports unsat core generation", "false");
diff --git a/src/cmd_context/context_params.h b/src/cmd_context/context_params.h
index 0fe4da93e..6b42b5b50 100644
--- a/src/cmd_context/context_params.h
+++ b/src/cmd_context/context_params.h
@@ -33,7 +33,7 @@ public:
std::string m_trace_file_name;
bool m_well_sorted_check;
bool m_model;
- bool m_validate_model;
+ bool m_model_validate;
bool m_unsat_core;
unsigned m_timeout;
diff --git a/src/cmd_context/parametric_cmd.cpp b/src/cmd_context/parametric_cmd.cpp
index f028c3b9d..c229bc29c 100644
--- a/src/cmd_context/parametric_cmd.cpp
+++ b/src/cmd_context/parametric_cmd.cpp
@@ -38,7 +38,7 @@ cmd_arg_kind parametric_cmd::next_arg_kind(cmd_context & ctx) const {
void parametric_cmd::set_next_arg(cmd_context & ctx, symbol const & s) {
if (m_last == symbol::null) {
- m_last = symbol(smt2_keyword_to_param(s).c_str());
+ m_last = symbol(norm_param_name(s).c_str());
if (pdescrs(ctx).get_kind(m_last.bare_str()) == CPK_INVALID)
throw cmd_exception("invalid keyword argument");
return;
diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp
index 8a7449a88..ca87406c7 100644
--- a/src/cmd_context/tactic_cmds.cpp
+++ b/src/cmd_context/tactic_cmds.cpp
@@ -497,7 +497,7 @@ static tactic * mk_using_params(cmd_context & ctx, sexpr * n) {
throw cmd_exception("invalid using-params combinator, keyword expected", c->get_line(), c->get_pos());
if (i == num_children)
throw cmd_exception("invalid using-params combinator, parameter value expected", c->get_line(), c->get_pos());
- symbol param_name = symbol(smt2_keyword_to_param(c->get_symbol()).c_str());
+ symbol param_name = symbol(norm_param_name(c->get_symbol()).c_str());
c = n->get_child(i);
i++;
switch (descrs.get_kind(param_name)) {
diff --git a/src/muz_qe/dl_cmds.cpp b/src/muz_qe/dl_cmds.cpp
index 8c4e26db7..bf9c24203 100644
--- a/src/muz_qe/dl_cmds.cpp
+++ b/src/muz_qe/dl_cmds.cpp
@@ -28,7 +28,6 @@ Notes:
#include"cancel_eh.h"
#include"scoped_ctrl_c.h"
#include"scoped_timer.h"
-#include"params2smt_params.h"
#include"trail.h"
#include
diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp
index 9faee3ab0..c8c1e3b2a 100644
--- a/src/muz_qe/pdr_context.cpp
+++ b/src/muz_qe/pdr_context.cpp
@@ -1456,7 +1456,6 @@ namespace pdr {
}
if (m_params.use_farkas() && !classify.is_bool()) {
m.toggle_proof_mode(PGM_FINE);
- m_fparams.m_proof_mode = PGM_FINE;
m_fparams.m_arith_bound_prop = BP_NONE;
m_fparams.m_arith_auto_config_simplex = true;
m_fparams.m_arith_propagate_eqs = false;
diff --git a/src/muz_qe/pdr_farkas_learner.cpp b/src/muz_qe/pdr_farkas_learner.cpp
index b3d0b4fd0..06b8f5eeb 100644
--- a/src/muz_qe/pdr_farkas_learner.cpp
+++ b/src/muz_qe/pdr_farkas_learner.cpp
@@ -255,7 +255,6 @@ namespace pdr {
smt_params farkas_learner::get_proof_params(smt_params& orig_params) {
smt_params res(orig_params);
- res.m_proof_mode = PROOF_MODE;
res.m_arith_bound_prop = BP_NONE;
// temp hack to fix the build
// res.m_conflict_resolution_strategy = CR_ALL_DECIDED;
diff --git a/src/muz_qe/pdr_quantifiers.cpp b/src/muz_qe/pdr_quantifiers.cpp
index 51a86e38c..2816a58d4 100644
--- a/src/muz_qe/pdr_quantifiers.cpp
+++ b/src/muz_qe/pdr_quantifiers.cpp
@@ -214,7 +214,7 @@ namespace pdr {
expr_ref_vector fmls(m);
smt_params fparams;
- fparams.m_proof_mode = PGM_FINE;
+ SASSERT(m.proofs_enabled());
fparams.m_mbqi = true;
fmls.push_back(m_A.get());
diff --git a/src/muz_qe/unit_subsumption_tactic.cpp b/src/muz_qe/unit_subsumption_tactic.cpp
index 1fb71490d..afc81723a 100644
--- a/src/muz_qe/unit_subsumption_tactic.cpp
+++ b/src/muz_qe/unit_subsumption_tactic.cpp
@@ -37,7 +37,6 @@ struct unit_subsumption_tactic : public tactic {
m_cancel(false),
m_context(m, m_fparams, p),
m_clauses(m) {
- m_fparams.m_proof_mode = m.proof_mode();
}
void set_cancel(bool f) {
diff --git a/src/muz_qe/vsubst_tactic.cpp b/src/muz_qe/vsubst_tactic.cpp
index b84202ee9..c389d9a66 100644
--- a/src/muz_qe/vsubst_tactic.cpp
+++ b/src/muz_qe/vsubst_tactic.cpp
@@ -45,7 +45,6 @@ Notes:
#include"arith_decl_plugin.h"
#include"for_each_expr.h"
#include"extension_model_converter.h"
-#include"params2smt_params.h"
#include"ast_smt2_pp.h"
class vsubst_tactic : public tactic {
@@ -94,7 +93,7 @@ class vsubst_tactic : public tactic {
}
smt_params params;
- params2smt_params(p, params);
+ params.updt_params(p);
params.m_model = false;
flet fl1(params.m_nlquant_elim, true);
flet fl2(params.m_nl_arith_gb, false);
diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index c0c8d5bc5..ee93dca2f 100644
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/src/parsers/smt2/smt2parser.cpp
@@ -35,6 +35,7 @@ namespace smt2 {
class parser {
cmd_context & m_ctx;
+ params_ref m_params;
scanner m_scanner;
scanner::token m_curr;
cmd * m_curr_cmd;
@@ -2285,6 +2286,10 @@ namespace smt2 {
shrink(m_sexpr_stack, sexpr_spos);
m_symbol_stack.shrink(sym_spos);
m_num_bindings = 0;
+ // HACK for propagating the update of parser parameters
+ if (norm_param_name(s) == "set_option") {
+ updt_params();
+ }
return;
}
else {
@@ -2357,9 +2362,10 @@ namespace smt2 {
}
public:
- parser(cmd_context & ctx, std::istream & is, bool interactive, params_ref const & _p):
+ parser(cmd_context & ctx, std::istream & is, bool interactive, params_ref const & p):
m_ctx(ctx),
- m_scanner(ctx, is, interactive, _p),
+ m_params(p),
+ m_scanner(ctx, is, interactive, p),
m_curr(scanner::NULL_TOKEN),
m_curr_cmd(0),
m_num_bindings(0),
@@ -2397,15 +2403,19 @@ namespace smt2 {
// the following assertion does not hold if ctx was already attached to an AST manager before the parser object is created.
// SASSERT(!m_ctx.has_manager());
- parser_params p(_p);
- m_ignore_user_patterns = p.ignore_user_patterns();
- m_ignore_bad_patterns = p.ignore_bad_patterns();
- m_display_error_for_vs = p.error_for_visual_studio();
+ updt_params();
}
~parser() {
reset_stack();
}
+
+ void updt_params() {
+ parser_params p(m_params);
+ m_ignore_user_patterns = p.ignore_user_patterns();
+ m_ignore_bad_patterns = p.ignore_bad_patterns();
+ m_display_error_for_vs = p.error_for_visual_studio();
+ }
void reset() {
reset_stack();
diff --git a/src/parsers/util/simple_parser.cpp b/src/parsers/util/simple_parser.cpp
index 65f75e870..045a45b24 100644
--- a/src/parsers/util/simple_parser.cpp
+++ b/src/parsers/util/simple_parser.cpp
@@ -112,7 +112,7 @@ expr * simple_parser::parse_expr(scanner & s) {
}
bool simple_parser::parse(std::istream & in, expr_ref & result) {
- scanner s(in, std::cerr, false);
+ scanner s(in, std::cerr, false);
try {
result = parse_expr(s);
if (!result)
diff --git a/src/shell/main.cpp b/src/shell/main.cpp
index 21ee8b71c..d91038b39 100644
--- a/src/shell/main.cpp
+++ b/src/shell/main.cpp
@@ -44,15 +44,9 @@ input_kind g_input_kind = IN_UNSPECIFIED;
bool g_display_statistics = false;
bool g_display_istatistics = false;
-#ifdef _WINDOWS
-#define OPT "/"
-#else
-#define OPT "-"
-#endif
-
void error(const char * msg) {
std::cerr << "Error: " << msg << "\n";
- std::cerr << "For usage information: z3 " << OPT << "h\n";
+ std::cerr << "For usage information: z3 -h\n";
exit(ERR_CMD_LINE);
}
@@ -64,41 +58,46 @@ void display_usage() {
std::cout << "32";
#endif
std::cout << " bit]. (C) Copyright 2006 Microsoft Corp.\n";
- std::cout << "Usage: z3 [options] [" << OPT << "file:]file\n";
+ std::cout << "Usage: z3 [options] [-file:]file\n";
std::cout << "\nInput format:\n";
- std::cout << " " << OPT << "smt use parser for SMT input format.\n";
- std::cout << " " << OPT << "smt2 use parser for SMT 2 input format.\n";
- std::cout << " " << OPT << "dl use parser for Datalog input format.\n";
- std::cout << " " << OPT << "dimacs use parser for DIMACS input format.\n";
- std::cout << " " << OPT << "log use parser for Z3 log input format.\n";
- std::cout << " " << OPT << "in read formula from standard input.\n";
+ std::cout << " -smt use parser for SMT input format.\n";
+ std::cout << " -smt2 use parser for SMT 2 input format.\n";
+ std::cout << " -dl use parser for Datalog input format.\n";
+ std::cout << " -dimacs use parser for DIMACS input format.\n";
+ std::cout << " -log use parser for Z3 log input format.\n";
+ std::cout << " -in read formula from standard input.\n";
std::cout << "\nMiscellaneous:\n";
- std::cout << " " << OPT << "h, " << OPT << "? prints this message.\n";
- std::cout << " " << OPT << "version prints version number of Z3.\n";
- std::cout << " " << OPT << "v:level be verbose, where is the verbosity level.\n";
- std::cout << " " << OPT << "nw disable warning messages.\n";
- std::cout << " " << OPT << "p display Z3 global (and module) parameters.\n";
- std::cout << " " << OPT << "pd display Z3 global (and module) parameter descriptions.\n";
- std::cout << " " << OPT << "pm:name display Z3 module ('name') parameters.\n";
- std::cout << " " << OPT << "pp:name display Z3 parameter description, if 'name' is not provided, then all module names are listed.\n";
+ std::cout << " -h, -? prints this message.\n";
+ std::cout << " -version prints version number of Z3.\n";
+ std::cout << " -v:level be verbose, where is the verbosity level.\n";
+ std::cout << " -nw disable warning messages.\n";
+ std::cout << " -p display Z3 global (and module) parameters.\n";
+ std::cout << " -pd display Z3 global (and module) parameter descriptions.\n";
+ std::cout << " -pm:name display Z3 module ('name') parameters.\n";
+ std::cout << " -pp:name display Z3 parameter description, if 'name' is not provided, then all module names are listed.\n";
std::cout << " --" << " all remaining arguments are assumed to be part of the input file name. This option allows Z3 to read files with strange names such as: -foo.smt2.\n";
std::cout << "\nResources:\n";
// timeout and memout are now available on Linux and OSX too.
- std::cout << " " << OPT << "T:timeout set the timeout (in seconds).\n";
- std::cout << " " << OPT << "t:timeout set the soft timeout (in seconds). It only kills the current query.\n";
- std::cout << " " << OPT << "memory:Megabytes set a limit for virtual memory consumption.\n";
+ std::cout << " -T:timeout set the timeout (in seconds).\n";
+ std::cout << " -t:timeout set the soft timeout (in seconds). It only kills the current query.\n";
+ std::cout << " -memory:Megabytes set a limit for virtual memory consumption.\n";
//
std::cout << "\nOutput:\n";
- std::cout << " " << OPT << "st display statistics.\n";
+ std::cout << " -st display statistics.\n";
#if defined(Z3DEBUG) || defined(_TRACE)
std::cout << "\nDebugging support:\n";
#endif
#ifdef _TRACE
- std::cout << " " << OPT << "tr:tag enable trace messages tagged with .\n";
+ std::cout << " -tr:tag enable trace messages tagged with .\n";
#endif
#ifdef Z3DEBUG
- std::cout << " " << OPT << "dbg:tag enable assertions tagged with .\n";
+ std::cout << " -dbg:tag enable assertions tagged with .\n";
#endif
+ std::cout << "\nParameter setting:\n";
+ std::cout << "Global and module parameters can be set in the command line.\n";
+ std::cout << " param_name=value for setting global parameters.\n";
+ std::cout << " module_name.param_name=value for setting module parameters.\n";
+ std::cout << "Use 'z3 -p' for the complete list of global and module parameters.\n";
}
void parse_cmd_line_args(int argc, char ** argv) {
@@ -132,6 +131,9 @@ void parse_cmd_line_args(int argc, char ** argv) {
#endif
) {
char * opt_name = arg + 1;
+ // allow names such as --help
+ if (*opt_name == '-')
+ opt_name++;
char * opt_arg = 0;
char * colon = strchr(arg, ':');
if (colon) {
@@ -235,7 +237,7 @@ void parse_cmd_line_args(int argc, char ** argv) {
}
else {
std::cerr << "Error: invalid command line option: " << arg << "\n";
- std::cerr << "For usage information: z3 " << OPT << "h\n";
+ std::cerr << "For usage information: z3 -h\n";
exit(ERR_CMD_LINE);
}
}
diff --git a/src/smt/dyn_ack.cpp b/src/smt/dyn_ack.cpp
index fc9b8939f..533d143c3 100644
--- a/src/smt/dyn_ack.cpp
+++ b/src/smt/dyn_ack.cpp
@@ -58,7 +58,7 @@ namespace smt {
\remark if negate == true, then the hypothesis is actually (not (= lhs rhs))
*/
proof * mk_hypothesis(ast_manager & m, app * eq, bool negate, expr * lhs, expr * rhs) {
- SASSERT(m.is_eq(eq));
+ SASSERT(m.is_eq(eq) || m.is_iff(eq));
SASSERT((eq->get_arg(0) == lhs && eq->get_arg(1) == rhs) ||
(eq->get_arg(0) == rhs && eq->get_arg(1) == lhs));
app * h = negate ? m.mk_not(eq) : eq;
diff --git a/src/smt/params/params2smt_params.cpp b/src/smt/params/params2smt_params.cpp
deleted file mode 100644
index b01d9478a..000000000
--- a/src/smt/params/params2smt_params.cpp
+++ /dev/null
@@ -1,79 +0,0 @@
-/*++
-Copyright (c) 2011 Microsoft Corporation
-
-Module Name:
-
- params2smt_params.h
-
-Abstract:
-
- Backward compatibility utilities for parameter setting
-
-Author:
-
- Leonardo de Moura (leonardo) 2011-05-19.
-
-Revision History:
-
---*/
-#include"smt_params.h"
-#include"params.h"
-
-/**
- Update smt_params using s.
- Only the most frequently used options are updated.
-
- This function is mainly used to allow smt::context to be used in
- the new strategy framework.
-*/
-void params2smt_params(params_ref const & s, smt_params & t) {
- t.m_relevancy_lvl = s.get_uint("relevancy", t.m_relevancy_lvl);
- TRACE("qi_cost", s.display(tout); tout << "\n";);
- t.m_qi_cost = s.get_str("qi_cost", t.m_qi_cost.c_str());
- t.m_mbqi = s.get_bool("mbqi", t.m_mbqi);
- t.m_mbqi_max_iterations = s.get_uint("mbqi_max_iterations", t.m_mbqi_max_iterations);
- t.m_random_seed = s.get_uint("random_seed", t.m_random_seed);
- t.m_model = s.get_bool("produce_models", t.m_model);
- if (s.get_bool("produce_proofs", false))
- t.m_proof_mode = PGM_FINE;
- t.m_qi_eager_threshold = s.get_double("qi_eager_threshold", t.m_qi_eager_threshold);
- t.m_qi_lazy_threshold = s.get_double("qi_lazy_threshold", t.m_qi_lazy_threshold);
- t.m_preprocess = s.get_bool("preprocess", t.m_preprocess);
- t.m_hi_div0 = s.get_bool("hi_div0", t.m_hi_div0);
- t.m_auto_config = s.get_bool("auto_config", t.m_auto_config);
- t.m_array_simplify = s.get_bool("array_old_simplifier", t.m_array_simplify);
- t.m_arith_branch_cut_ratio = s.get_uint("arith_branch_cut_ratio", t.m_arith_branch_cut_ratio);
- t.m_arith_expand_eqs = s.get_bool("arith_expand_eqs", t.m_arith_expand_eqs);
-
- if (s.get_bool("arith_greatest_error_pivot", false))
- t.m_arith_pivot_strategy = ARITH_PIVOT_GREATEST_ERROR;
- else if (s.get_bool("arith_least_error_pivot", false))
- t.m_arith_pivot_strategy = ARITH_PIVOT_LEAST_ERROR;
-}
-
-/**
- \brief Copy parameters (from s) that affect the semantics of Z3 (e.g., HI_DIV0).
- It also copies the model construction parameter. Thus, model construction
- can be enabled at the command line.
-*/
-void smt_params2params(smt_params const & s, params_ref & t) {
- if (s.m_model)
- t.set_bool("produce_models", true);
- if (!s.m_hi_div0)
- t.set_bool("hi_div0", false);
-}
-
-/**
- \brief Bridge for using params_ref with smt::context.
-*/
-void solver_smt_params_descrs(param_descrs & r) {
- r.insert("hi_div0", CPK_BOOL, "(default: true) if true, then Z3 uses the usual hardware interpretation for division (rem, mod) by zero. Otherwise, these operations are considered uninterpreted");
- r.insert("relevancy", CPK_UINT, "relevancy propagation heuristic: 0 - disabled, 1 - relevancy is tracked by only affects quantifier instantiation, 2 - relevancy is tracked, and an atom is only asserted if it is relevant");
- r.insert("mbqi", CPK_BOOL, "model based quantifier instantiation (MBQI)");
- r.insert("mbqi_max_iterations", CPK_UINT, "maximum number of rounds of MBQI");
- r.insert("random_seed", CPK_UINT, "random seed for smt solver");
- r.insert("qi_eager_threshold", CPK_DOUBLE, "threshold for eager quantifier instantiation");
- r.insert("qi_lazy_threshold", CPK_DOUBLE, "threshold for lazy quantifier instantiation");
- r.insert("auto_config", CPK_BOOL, "use heuristics to automatically configure smt solver");
- r.insert("arith_branch_cut_ratio", CPK_UINT, "branch&bound / gomory cut ratio");
-}
diff --git a/src/smt/params/params2smt_params.h b/src/smt/params/params2smt_params.h
deleted file mode 100644
index d4f60cb64..000000000
--- a/src/smt/params/params2smt_params.h
+++ /dev/null
@@ -1,31 +0,0 @@
-/*++
-Copyright (c) 2011 Microsoft Corporation
-
-Module Name:
-
- params2smt_params.h
-
-Abstract:
-
- Backward compatibility utilities for parameter setting
-
-Author:
-
- Leonardo de Moura (leonardo) 2011-05-19.
-
-Revision History:
-
---*/
-#ifndef _PARAMS2SMT_PARAMS_H_
-#define _PARAMS2SMT_PARAMS_H_
-
-class params_ref;
-struct smt_params;
-
-void params2smt_params(params_ref const & s, smt_params & t);
-
-void smt_params2params(smt_params const & s, params_ref & t);
-
-void solver_smt_params_descrs(param_descrs & r);
-
-#endif
diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp
deleted file mode 100644
index 691ec009d..000000000
--- a/src/smt/params/smt_params.cpp
+++ /dev/null
@@ -1,50 +0,0 @@
-/*++
-Copyright (c) 2006 Microsoft Corporation
-
-Module Name:
-
- smt_params.cpp
-
-Abstract:
-
-
-
-Author:
-
- Leonardo de Moura (leonardo) 2008-02-20.
-
-Revision History:
-
---*/
-#include"smt_params.h"
-#include"smt_params_helper.hpp"
-
-void smt_params::updt_local_params(params_ref const & _p) {
- smt_params_helper p(_p);
- m_auto_config = p.auto_config();
- m_ematching = p.ematching();
- m_phase_selection = static_cast(p.phase_selection());
- m_restart_strategy = static_cast(p.restart_strategy());
- m_restart_factor = p.restart_factor();
- m_case_split_strategy = static_cast(p.case_split());
- m_delay_units = p.delay_units();
- m_delay_units_threshold = p.delay_units_threshold();
- m_proof_mode = _p.get_bool("produce_proofs", false)? PGM_FINE : PGM_DISABLED;
-}
-
-void smt_params::updt_params(params_ref const & p) {
- preprocessor_params::updt_params(p);
- qi_params::updt_params(p);
- theory_arith_params::updt_params(p);
- theory_bv_params::updt_params(p);
- updt_local_params(p);
-}
-
-void smt_params::updt_params(context_params const & p) {
- m_auto_config = p.m_auto_config;
- m_soft_timeout = p.m_timeout;
- m_model = p.m_model;
- m_model_validate = p.m_validate_model;
- m_proof_mode = p.m_proof ? PGM_FINE : PGM_DISABLED;
-}
-
diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h
index ec057239a..3d823cb51 100644
--- a/src/smt/params/smt_params.h
+++ b/src/smt/params/smt_params.h
@@ -207,7 +207,6 @@ struct smt_params : public preprocessor_params,
bool m_at_labels_cex; // only use labels which contains the @ symbol when building multiple counterexamples.
bool m_check_at_labels; // check that @ labels are inserted to generate unique counter-examples.
bool m_dump_goal_as_smt;
- proof_gen_mode m_proof_mode;
bool m_auto_config;
smt_params(params_ref const & p = params_ref()):
@@ -277,7 +276,6 @@ struct smt_params : public preprocessor_params,
m_at_labels_cex(false),
m_check_at_labels(false),
m_dump_goal_as_smt(false),
- m_proof_mode(PGM_DISABLED),
m_auto_config(true) {
updt_local_params(p);
}
diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg
index 8db95a581..ee583ff85 100644
--- a/src/smt/params/smt_params_helper.pyg
+++ b/src/smt/params/smt_params_helper.pyg
@@ -3,6 +3,8 @@ def_module_params(module_name='smt',
description='smt solver based on lazy smt',
export=True,
params=(('auto_config', BOOL, True, 'automatically configure solver'),
+ ('random_seed', UINT, 0, 'random seed for the smt solver'),
+ ('relevancy', UINT, 2, 'relevancy propagation heuristic: 0 - disabled, 1 - relevancy is tracked by only affects quantifier instantiation, 2 - relevancy is tracked, and an atom is only asserted if it is relevant'),
('macro_finder', BOOL, False, 'try to find universally quantified formulas that can be viewed as macros'),
('ematching', BOOL, True, 'E-Matching based quantifier instantiation'),
('phase_selection', UINT, 4, 'phase selection heuristic: 0 - always false, 1 - always true, 2 - phase caching, 3 - phase caching conservative, 4 - phase caching conservative 2, 5 - random, 6 - number of occurrences'),
@@ -33,6 +35,7 @@ def_module_params(module_name='smt',
('arith.nl.rounds', UINT, 1024, 'threshold for number of (nested) final checks for non linear arithmetic'),
('arith.euclidean_solver', BOOL, False, 'eucliean solver for linear integer arithmetic'),
('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'),
+ ('arith.propagation_mode', UINT, 2, '0 - no propagation, 1 - propagate existing literals, 2 - refine bounds'),
('arith.branch_cut_ratio', UINT, 2, 'branch/cut ratio for linear integer arithmetic'),
('arith.int_eq_branch', BOOL, False, 'branching using derived integer equations'),
('arith.ignore_int', BOOL, False, 'treat integer variables as real')))
diff --git a/src/smt/params/theory_arith_params.cpp b/src/smt/params/theory_arith_params.cpp
index 5a1101524..7281a5daa 100644
--- a/src/smt/params/theory_arith_params.cpp
+++ b/src/smt/params/theory_arith_params.cpp
@@ -32,6 +32,7 @@ void theory_arith_params::updt_params(params_ref const & _p) {
m_arith_branch_cut_ratio = p.arith_branch_cut_ratio();
m_arith_int_eq_branching = p.arith_int_eq_branch();
m_arith_ignore_int = p.arith_ignore_int();
+ m_arith_bound_prop = static_cast(p.arith_propagation_mode());
}
diff --git a/src/smt/qi_queue.cpp b/src/smt/qi_queue.cpp
index 9394dae34..35dd19087 100644
--- a/src/smt/qi_queue.cpp
+++ b/src/smt/qi_queue.cpp
@@ -47,10 +47,21 @@ namespace smt {
void qi_queue::setup() {
TRACE("qi_cost", tout << "qi_cost: " << m_params.m_qi_cost << "\n";);
- if (!m_parser.parse_string(m_params.m_qi_cost.c_str(), m_cost_function))
- throw default_exception("invalid cost function %s", m_params.m_qi_cost.c_str());
- if (!m_parser.parse_string(m_params.m_qi_new_gen.c_str(), m_new_gen_function))
- throw default_exception("invalid new-gen function %s", m_params.m_qi_new_gen.c_str());
+ if (!m_parser.parse_string(m_params.m_qi_cost.c_str(), m_cost_function)) {
+ // it is not reasonable to abort here during the creation of smt::context just because an invalid option was provided.
+ // throw default_exception("invalid cost function %s", m_params.m_qi_cost.c_str());
+
+ // using warning message instead
+ warning_msg("invalid cost function '%s', switching to default one", m_params.m_qi_cost.c_str());
+ // Trying again with default function
+ VERIFY(m_parser.parse_string("(+ weight generation)", m_cost_function));
+ }
+ if (!m_parser.parse_string(m_params.m_qi_new_gen.c_str(), m_new_gen_function)) {
+ // See comment above
+ // throw default_exception("invalid new-gen function %s", m_params.m_qi_new_gen.c_str());
+ warning_msg("invalid new_gen function '%s', switching to default one", m_params.m_qi_new_gen.c_str());
+ VERIFY(m_parser.parse_string("cost", m_new_gen_function));
+ }
m_eager_cost_threshold = m_params.m_qi_eager_threshold;
}
diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp
index 23687af8c..779c68625 100644
--- a/src/smt/smt_kernel.cpp
+++ b/src/smt/smt_kernel.cpp
@@ -19,7 +19,7 @@ Revision History:
#include"smt_kernel.h"
#include"smt_context.h"
#include"ast_smt2_pp.h"
-#include"params2smt_params.h"
+#include"smt_params_helper.hpp"
namespace smt {
@@ -345,7 +345,7 @@ namespace smt {
}
void kernel::collect_param_descrs(param_descrs & d) {
- solver_smt_params_descrs(d);
+ smt_params_helper::collect_param_descrs(d);
}
context & kernel::get_context() {
diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp
index 350ec333f..cefdacef5 100644
--- a/src/smt/smt_model_checker.cpp
+++ b/src/smt/smt_model_checker.cpp
@@ -313,7 +313,7 @@ namespace smt {
TRACE("model_checker", tout << "MODEL_CHECKER INVOKED\n";
tout << "model:\n"; model_pp(tout, *m_curr_model););
if (m_params.m_mbqi_trace) {
- verbose_stream() << "[mbqi] started\n";
+ verbose_stream() << "(smt.mbqi \"started\")\n";
}
init_aux_context();
@@ -325,13 +325,12 @@ namespace smt {
quantifier * q = *it;
if (m_context->is_relevant(q) && m_context->get_assignment(q) == l_true) {
if (m_params.m_mbqi_trace && q->get_qid() != symbol::null) {
- verbose_stream() << "[mbqi] checking: " << q->get_qid() << "\n";
+ verbose_stream() << "(smt.mbqi :checking " << q->get_qid() << ")\n";
}
found_relevant = true;
if (!check(q)) {
- IF_VERBOSE(5, verbose_stream() << "current model does not satisfy: " << q->get_qid() << "\n";);
- if (m_params.m_mbqi_trace) {
- verbose_stream() << "[mbqi] failed " << q->get_qid() << "\n";
+ if (m_params.m_mbqi_trace || get_verbosity_level() >= 5) {
+ verbose_stream() << "(smt.mbqi :failed " << q->get_qid() << ")\n";
}
num_failures++;
}
@@ -348,9 +347,9 @@ namespace smt {
m_curr_model->cleanup();
if (m_params.m_mbqi_trace) {
if (num_failures == 0)
- verbose_stream() << "[mbqi] succeeded\n";
+ verbose_stream() << "(smt.mbqi :succeeded true)\n";
else
- verbose_stream() << "[mbqi] num failures " << num_failures << "\n";
+ verbose_stream() << "(smt.mbqi :num-failures " << num_failures << ")\n";
}
return num_failures == 0;
}
@@ -361,7 +360,7 @@ namespace smt {
}
void model_checker::restart_eh() {
- IF_VERBOSE(100, verbose_stream() << "instantiating new instances...\n";);
+ IF_VERBOSE(100, verbose_stream() << "(smt.mbqi \"instantiating new instances...\")\n";);
assert_new_instances();
reset_new_instances();
}
diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp
index 799dd3c49..d56fe0cff 100644
--- a/src/smt/smt_quantifier.cpp
+++ b/src/smt/smt_quantifier.cpp
@@ -562,7 +562,7 @@ namespace smt {
virtual quantifier_manager::check_model_result
check_model(proto_model * m, obj_map const & root2value) {
if (m_fparams->m_mbqi) {
- IF_VERBOSE(10, verbose_stream() << "model based quantifier instantiation...\n";);
+ IF_VERBOSE(10, verbose_stream() << "(smt.mbqi)\n";);
if (m_model_checker->check(m, root2value)) {
return quantifier_manager::SAT;
}
@@ -594,7 +594,6 @@ namespace smt {
final_check_status final_check_quant() {
if (use_ematching()) {
if (m_lazy_matching_idx < m_fparams->m_qi_max_lazy_multipattern_matching) {
- IF_VERBOSE(100, verbose_stream() << "matching delayed multi-patterns... \n";);
m_lazy_mam->rematch();
m_context->push_trail(value_trail(m_lazy_matching_idx));
m_lazy_matching_idx++;
diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index f088870a4..ac31eb1a9 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -266,8 +266,8 @@ namespace smt {
// 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.
// Example: (x < 1) and (x > 0)
- if (m_params.m_proof_mode != PGM_DISABLED) {
- m_context.register_plugin(alloc(smt::theory_mi_arith_w_proofs, m_manager, m_params));
+ if (m_manager.proofs_enabled()) {
+ m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
}
else if (!m_params.m_arith_auto_config_simplex && is_dense(st)) {
if (!st.m_has_rational && !m_params.m_model && st.m_arith_k_sum < rational(INT_MAX / 8))
@@ -343,8 +343,8 @@ namespace smt {
tout << "RELEVANCY: " << m_params.m_relevancy_lvl << "\n";
tout << "ARITH_EQ_BOUNDS: " << m_params.m_arith_eq_bounds << "\n";);
- if (m_params.m_proof_mode != PGM_DISABLED) {
- m_context.register_plugin(alloc(smt::theory_mi_arith_w_proofs, m_manager, m_params));
+ if (m_manager.proofs_enabled()) {
+ m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
}
else if (!m_params.m_arith_auto_config_simplex && is_dense(st)) {
TRACE("setup", tout << "using dense diff logic...\n";);
@@ -394,8 +394,8 @@ namespace smt {
m_params.m_lemma_gc_half = true;
m_params.m_restart_strategy = RS_GEOMETRIC;
- if (m_params.m_proof_mode != PGM_DISABLED) {
- m_context.register_plugin(alloc(smt::theory_mi_arith_w_proofs, m_manager, m_params));
+ if (m_manager.proofs_enabled()) {
+ m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
}
else if (st.m_arith_k_sum < rational(INT_MAX / 8))
m_context.register_plugin(alloc(smt::theory_dense_si, m_manager, m_params));
@@ -409,8 +409,8 @@ namespace smt {
m_params.m_restart_strategy = RS_GEOMETRIC;
m_params.m_restart_factor = 1.5;
m_params.m_restart_adaptive = false;
- if (m_params.m_proof_mode != PGM_DISABLED) {
- m_context.register_plugin(alloc(smt::theory_mi_arith_w_proofs, m_manager, m_params));
+ if (m_manager.proofs_enabled()) {
+ m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
}
// else if (st.m_arith_k_sum < rational(INT_MAX / 8))
// m_context.register_plugin(alloc(smt::theory_si_arith, m_manager, m_params));
@@ -683,21 +683,11 @@ namespace smt {
}
void setup::setup_i_arith() {
- if (m_params.m_proof_mode != PGM_DISABLED) {
- m_context.register_plugin(alloc(smt::theory_mi_arith_w_proofs, m_manager, m_params));
- }
- else {
- m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params));
- }
+ m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params));
}
void setup::setup_mi_arith() {
- if (m_params.m_proof_mode != PGM_DISABLED) {
- m_context.register_plugin(alloc(smt::theory_mi_arith_w_proofs, m_manager, m_params));
- }
- else {
- m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
- }
+ m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
}
void setup::setup_arith() {
@@ -734,21 +724,10 @@ namespace smt {
}
break;
default:
- if (m_params.m_proof_mode != PGM_DISABLED) {
- m_context.register_plugin(alloc(smt::theory_mi_arith_w_proofs, m_manager, m_params));
- }
- // else if (m_params.m_arith_fixnum) {
- // if (m_params.m_arith_int_only)
- // m_context.register_plugin(alloc(smt::theory_si_arith, m_manager, m_params));
- // else
- // m_context.register_plugin(alloc(smt::theory_smi_arith, m_manager, m_params));
- // }
- else {
- if (m_params.m_arith_int_only)
- m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params));
- else
- m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
- }
+ if (m_params.m_arith_int_only)
+ m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params));
+ else
+ m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
break;
}
}
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index 2aa4ee28f..e8c1c6698 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -56,9 +56,13 @@ namespace smt {
virtual void init_core(ast_manager & m, symbol const & logic) {
reset();
-#pragma omp critical (solver)
+ // We can throw exceptions when creating a smt::kernel object
+ // So, we should create the smt::kernel outside of the criticial section
+ // block. OMP does not allow exceptions to cross critical section boundaries.
+ smt::kernel * new_kernel = alloc(smt::kernel, m, m_params);
+ #pragma omp critical (solver)
{
- m_context = alloc(smt::kernel, m, m_params);
+ m_context = new_kernel;
if (m_callback)
m_context->set_progress_callback(m_callback);
}
@@ -77,59 +81,67 @@ namespace smt {
virtual void reset_core() {
if (m_context != 0) {
-#pragma omp critical (solver)
+ #pragma omp critical (solver)
{
dealloc(m_context);
m_context = 0;
}
}
}
+
+ // An exception may be thrown when creating a smt::kernel.
+ // So, there is no guarantee that m_context != 0 when
+ // using smt_solver from the SMT 2.0 command line frontend.
+ void check_context() const {
+ if (m_context == 0)
+ throw default_exception("Z3 failed to create solver, check previous error messages");
+ }
virtual void assert_expr(expr * t) {
- SASSERT(m_context);
+ check_context();
m_context->assert_expr(t);
}
virtual void push_core() {
- SASSERT(m_context);
+ check_context();
m_context->push();
}
virtual void pop_core(unsigned n) {
- SASSERT(m_context);
+ check_context();
m_context->pop(n);
}
virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
- SASSERT(m_context);
+ check_context();
TRACE("solver_na2as", tout << "smt_solver::check_sat_core: " << num_assumptions << "\n";);
return m_context->check(num_assumptions, assumptions);
}
virtual void get_unsat_core(ptr_vector & r) {
- SASSERT(m_context);
+ check_context();
unsigned sz = m_context->get_unsat_core_size();
for (unsigned i = 0; i < sz; i++)
r.push_back(m_context->get_unsat_core_expr(i));
}
virtual void get_model(model_ref & m) {
- SASSERT(m_context);
+ check_context();
m_context->get_model(m);
}
virtual proof * get_proof() {
- SASSERT(m_context);
+ check_context();
return m_context->get_proof();
}
virtual std::string reason_unknown() const {
- SASSERT(m_context);
+ check_context();
return m_context->last_failure_as_string();
}
virtual void get_labels(svector & r) {
- SASSERT(m_context);
+ check_context();
buffer tmp;
m_context->get_relevant_labels(0, tmp);
r.append(tmp.size(), tmp.c_ptr());
diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp
index 20b6585e1..2c7d58b1a 100644
--- a/src/smt/tactic/smt_tactic.cpp
+++ b/src/smt/tactic/smt_tactic.cpp
@@ -20,7 +20,7 @@ Notes:
#include"tactical.h"
#include"smt_kernel.h"
#include"smt_params.h"
-#include"params2smt_params.h"
+#include"smt_params_helper.hpp"
#include"rewriter_types.h"
class smt_tactic : public tactic {
@@ -70,7 +70,7 @@ public:
virtual void collect_param_descrs(param_descrs & r) {
r.insert("candidate_models", CPK_BOOL, "(default: false) create candidate models even when quantifier or theory reasoning is incomplete.");
r.insert("fail_if_inconclusive", CPK_BOOL, "(default: true) fail if found unsat (sat) for under (over) approximated goal.");
- solver_smt_params_descrs(r);
+ smt_params_helper::collect_param_descrs(r);
}
virtual void set_cancel(bool f) {
diff --git a/src/smt/theory_arith.cpp b/src/smt/theory_arith.cpp
index d57812b7a..0bb356b95 100644
--- a/src/smt/theory_arith.cpp
+++ b/src/smt/theory_arith.cpp
@@ -21,7 +21,6 @@ Revision History:
namespace smt {
- template class theory_arith;
template class theory_arith;
template class theory_arith;
// template class theory_arith;
diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h
index c125558f7..9435a49cd 100644
--- a/src/smt/theory_arith.h
+++ b/src/smt/theory_arith.h
@@ -87,8 +87,8 @@ namespace smt {
typedef vector numeral_vector;
static const int dead_row_id = -1;
- static const bool proofs_enabled = Ext::proofs_enabled;
protected:
+ bool proofs_enabled() const { return get_manager().proofs_enabled(); }
struct linear_monomial {
numeral m_coeff;
@@ -233,8 +233,8 @@ namespace smt {
void reset();
literal_vector& lits() { return m_lits; }
eq_vector& eqs() { return m_eqs; }
- void push_lit(literal l, numeral const& r);
- void push_eq(enode_pair const& p, numeral const& r);
+ void push_lit(literal l, numeral const& r, bool proofs_enabled);
+ void push_eq(enode_pair const& p, numeral const& r, bool proofs_enabled);
unsigned num_params() const { return empty()?0:m_eq_coeffs.size() + m_lit_coeffs.size() + 1; }
numeral const* lit_coeffs() const { return m_lit_coeffs.c_ptr(); }
numeral const* eq_coeffs() const { return m_eq_coeffs.c_ptr(); }
@@ -284,8 +284,8 @@ namespace smt {
bool is_true() const { return m_is_true; }
void assign_eh(bool is_true, inf_numeral const & epsilon);
virtual bool has_justification() const { return true; }
- virtual void push_justification(antecedents& a, numeral const& coeff) {
- a.push_lit(literal(get_bool_var(), !m_is_true), coeff);
+ virtual void push_justification(antecedents& a, numeral const& coeff, bool proofs_enabled) {
+ a.push_lit(literal(get_bool_var(), !m_is_true), coeff, proofs_enabled);
}
};
@@ -301,9 +301,9 @@ namespace smt {
}
virtual ~eq_bound() {}
virtual bool has_justification() const { return true; }
- virtual void push_justification(antecedents& a, numeral const& coeff) {
+ virtual void push_justification(antecedents& a, numeral const& coeff, bool proofs_enabled) {
SASSERT(m_lhs->get_root() == m_rhs->get_root());
- a.push_eq(enode_pair(m_lhs, m_rhs), coeff);
+ a.push_eq(enode_pair(m_lhs, m_rhs), coeff, proofs_enabled);
}
};
@@ -316,7 +316,7 @@ namespace smt {
derived_bound(theory_var v, inf_numeral const & val, bound_kind k):bound(v, val, k, false) {}
virtual ~derived_bound() {}
virtual bool has_justification() const { return true; }
- virtual void push_justification(antecedents& a, numeral const& coeff);
+ virtual void push_justification(antecedents& a, numeral const& coeff, bool proofs_enabled);
virtual void push_lit(literal l, numeral const&) { m_lits.push_back(l); }
virtual void push_eq(enode_pair const& p, numeral const&) { m_eqs.push_back(p); }
};
@@ -329,7 +329,7 @@ namespace smt {
justified_derived_bound(theory_var v, inf_numeral const & val, bound_kind k):derived_bound(v, val, k) {}
virtual ~justified_derived_bound() {}
virtual bool has_justification() const { return true; }
- virtual void push_justification(antecedents& a, numeral const& coeff);
+ virtual void push_justification(antecedents& a, numeral const& coeff, bool proofs_enabled);
virtual void push_lit(literal l, numeral const& coeff);
virtual void push_eq(enode_pair const& p, numeral const& coeff);
@@ -1053,30 +1053,9 @@ namespace smt {
static inf_numeral mk_inf_numeral(numeral const & n, numeral const & r) {
return inf_numeral(n, r);
}
- static const bool proofs_enabled = false;
mi_ext() : m_int_epsilon(rational(1)), m_real_epsilon(rational(0), true) {}
};
- class mi_ext_with_proofs {
- public:
- typedef rational numeral;
- typedef inf_rational inf_numeral;
- inf_numeral m_int_epsilon;
- inf_numeral m_real_epsilon;
- numeral fractional_part(inf_numeral const& n) {
- SASSERT(n.is_rational());
- return n.get_rational() - floor(n);
- }
- static numeral fractional_part(numeral const & n) {
- return n - floor(n);
- }
- static inf_numeral mk_inf_numeral(numeral const & n, numeral const & r) {
- return inf_numeral(n, r);
- }
- static const bool proofs_enabled = true;
- mi_ext_with_proofs() : m_int_epsilon(rational(1)), m_real_epsilon(rational(0), true) {}
- };
-
class i_ext {
public:
typedef rational numeral;
@@ -1090,7 +1069,6 @@ namespace smt {
UNREACHABLE();
return inf_numeral(n);
}
- static const bool proofs_enabled = false;
i_ext() : m_int_epsilon(1), m_real_epsilon(1) {}
};
@@ -1107,7 +1085,6 @@ namespace smt {
UNREACHABLE();
return inf_numeral(n);
}
- static const bool proofs_enabled = false;
si_ext(): m_int_epsilon(s_integer(1)), m_real_epsilon(s_integer(1)) {}
};
@@ -1128,12 +1105,10 @@ namespace smt {
static inf_numeral mk_inf_numeral(numeral const& n, numeral const& i) {
return inf_numeral(n, i);
}
- static const bool proofs_enabled = false;
smi_ext() : m_int_epsilon(s_integer(1)), m_real_epsilon(s_integer(0), true) {}
};
typedef theory_arith theory_mi_arith;
- typedef theory_arith theory_mi_arith_w_proofs;
typedef theory_arith theory_i_arith;
// typedef theory_arith theory_si_arith;
// typedef theory_arith theory_smi_arith;
diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h
index 4d22287ed..1e15365a4 100644
--- a/src/smt/theory_arith_aux.h
+++ b/src/smt/theory_arith_aux.h
@@ -336,7 +336,7 @@ namespace smt {
}
template
- void theory_arith::antecedents::push_lit(literal l, numeral const& r) {
+ void theory_arith::antecedents::push_lit(literal l, numeral const& r, bool proofs_enabled) {
m_lits.push_back(l);
if (proofs_enabled) {
m_lit_coeffs.push_back(r);
@@ -344,7 +344,7 @@ namespace smt {
}
template
- void theory_arith::antecedents::push_eq(enode_pair const& p, numeral const& r) {
+ void theory_arith::antecedents::push_eq(enode_pair const& p, numeral const& r, bool proofs_enabled) {
m_eqs.push_back(p);
if (proofs_enabled) {
m_eq_coeffs.push_back(r);
@@ -690,14 +690,14 @@ namespace smt {
// -----------------------------------
template
- void theory_arith::derived_bound::push_justification(antecedents& a, numeral const& coeff) {
+ void theory_arith::derived_bound::push_justification(antecedents& a, numeral const& coeff, bool proofs_enabled) {
if (proofs_enabled) {
for (unsigned i = 0; i < m_lits.size(); ++i) {
- a.push_lit(m_lits[i], coeff);
+ a.push_lit(m_lits[i], coeff, proofs_enabled);
}
for (unsigned i = 0; i < m_eqs.size(); ++i) {
- a.push_eq(m_eqs[i], coeff);
+ a.push_eq(m_eqs[i], coeff, proofs_enabled);
}
}
else {
@@ -708,12 +708,12 @@ namespace smt {
template
- void theory_arith::justified_derived_bound::push_justification(antecedents& a, numeral const& coeff) {
+ void theory_arith::justified_derived_bound::push_justification(antecedents& a, numeral const& coeff, bool proofs_enabled) {
for (unsigned i = 0; i < this->m_lits.size(); ++i) {
- a.push_lit(this->m_lits[i], coeff*m_lit_coeffs[i]);
+ a.push_lit(this->m_lits[i], coeff*m_lit_coeffs[i], proofs_enabled);
}
for (unsigned i = 0; i < this->m_eqs.size(); ++i) {
- a.push_eq(this->m_eqs[i], coeff*m_eq_coeffs[i]);
+ a.push_eq(this->m_eqs[i], coeff*m_eq_coeffs[i], proofs_enabled);
}
}
@@ -755,7 +755,7 @@ namespace smt {
literal l = ante.lits()[i];
if (lits.contains(l.index()))
continue;
- if (proofs_enabled) {
+ if (proofs_enabled()) {
new_bound.push_lit(l, ante.lit_coeffs()[i]);
}
else {
@@ -768,7 +768,7 @@ namespace smt {
enode_pair const & p = ante.eqs()[i];
if (eqs.contains(p))
continue;
- if (proofs_enabled) {
+ if (proofs_enabled()) {
new_bound.push_eq(p, ante.eq_coeffs()[i]);
}
else {
@@ -796,7 +796,7 @@ namespace smt {
template
void theory_arith::mk_bound_from_row(theory_var v, inf_numeral const & k, bound_kind kind, row const & r) {
inf_numeral k_norm = normalize_bound(v, k, kind);
- derived_bound * new_bound = proofs_enabled?alloc(justified_derived_bound, v, k_norm, kind):alloc(derived_bound, v, k_norm, kind);
+ derived_bound * new_bound = proofs_enabled()?alloc(justified_derived_bound, v, k_norm, kind):alloc(derived_bound, v, k_norm, kind);
m_bounds_to_delete.push_back(new_bound);
m_asserted_bounds.push_back(new_bound);
m_tmp_lit_set.reset();
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index a691096ec..0f3ed1d13 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -2456,7 +2456,7 @@ namespace smt {
delta -= coeff*(k_2 - k_1);
}
TRACE("propagate_bounds", tout << "delta (after replace): " << delta << "\n";);
- new_atom->push_justification(ante, coeff);
+ new_atom->push_justification(ante, coeff, proofs_enabled());
SASSERT(delta >= inf_numeral::zero());
}
}
@@ -2569,7 +2569,7 @@ namespace smt {
for (; it != end; ++it)
lits.push_back(~(*it));
justification * js = 0;
- if (proofs_enabled) {
+ if (proofs_enabled()) {
js = alloc(theory_lemma_justification, get_id(), ctx, lits.size(), lits.c_ptr(),
ante.num_params(), ante.params("assign-bounds"));
}
@@ -2656,13 +2656,13 @@ namespace smt {
for (unsigned i = 0; i < num_literals; i++) {
ctx.display_detailed_literal(tout, lits[i]);
tout << " ";
- if (proofs_enabled) {
+ if (proofs_enabled()) {
tout << "bound: " << bounds.lit_coeffs()[i] << "\n";
}
}
for (unsigned i = 0; i < num_eqs; i++) {
tout << "#" << eqs[i].first->get_owner_id() << "=#" << eqs[i].second->get_owner_id() << " ";
- if (proofs_enabled) {
+ if (proofs_enabled()) {
tout << "bound: " << bounds.eq_coeffs()[i] << "\n";
}
}
diff --git a/src/tactic/arith/degree_shift_tactic.cpp b/src/tactic/arith/degree_shift_tactic.cpp
index 8e2c6d7cb..a1aa0bdc8 100644
--- a/src/tactic/arith/degree_shift_tactic.cpp
+++ b/src/tactic/arith/degree_shift_tactic.cpp
@@ -342,7 +342,7 @@ protected:
tactic * mk_degree_shift_tactic(ast_manager & m, params_ref const & p) {
params_ref mul2power_p;
- mul2power_p.set_bool(":mul-to-power", true);
+ mul2power_p.set_bool("mul_to_power", true);
return and_then(using_params(mk_simplify_tactic(m), mul2power_p),
clean(alloc(degree_shift_tactic, m)));
}
diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp
index d6ed86c08..d2292ede9 100644
--- a/src/tactic/arith/purify_arith_tactic.cpp
+++ b/src/tactic/arith/purify_arith_tactic.cpp
@@ -902,7 +902,7 @@ public:
tactic * mk_purify_arith_tactic(ast_manager & m, params_ref const & p) {
params_ref elim_rem_p = p;
- elim_rem_p.set_bool("elim-rem", true);
+ elim_rem_p.set_bool("elim_rem", true);
params_ref skolemize_p;
skolemize_p.set_bool("skolemize", false);
diff --git a/src/tactic/core/nnf_tactic.cpp b/src/tactic/core/nnf_tactic.cpp
index fdaf03d55..a79a4ed06 100644
--- a/src/tactic/core/nnf_tactic.cpp
+++ b/src/tactic/core/nnf_tactic.cpp
@@ -120,7 +120,7 @@ tactic * mk_snf_tactic(ast_manager & m, params_ref const & p) {
tactic * mk_nnf_tactic(ast_manager & m, params_ref const & p) {
params_ref new_p(p);
- new_p.set_sym("nnf_mode", symbol("full"));
+ new_p.set_sym("mode", symbol("full"));
TRACE("nnf", tout << "mk_nnf: " << new_p << "\n";);
return using_params(mk_snf_tactic(m, p), new_p);
}
diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp
index 290a0ad35..f49ce8422 100644
--- a/src/tactic/sls/sls_tactic.cpp
+++ b/src/tactic/sls/sls_tactic.cpp
@@ -1855,7 +1855,7 @@ tactic * mk_sls_tactic(ast_manager & m, params_ref const & p) {
tactic * mk_preamble(ast_manager & m, params_ref const & p) {
params_ref main_p;
main_p.set_bool("elim_and", true);
- // main_p.set_bool("pull-cheap_ite", true);
+ // main_p.set_bool("pull_cheap_ite", true);
main_p.set_bool("push_ite_bv", true);
main_p.set_bool("blast_distinct", true);
// main_p.set_bool("udiv2mul", true);
diff --git a/src/tactic/smtlogics/nra_tactic.cpp b/src/tactic/smtlogics/nra_tactic.cpp
index 623b7e55e..845b6bfec 100644
--- a/src/tactic/smtlogics/nra_tactic.cpp
+++ b/src/tactic/smtlogics/nra_tactic.cpp
@@ -27,11 +27,11 @@ Notes:
tactic * mk_nra_tactic(ast_manager & m, params_ref const& p) {
params_ref p1 = p;
- p1.set_uint(":seed", 11);
- p1.set_bool(":factor", false);
+ p1.set_uint("seed", 11);
+ p1.set_bool("factor", false);
params_ref p2 = p;
- p2.set_uint(":seed", 13);
- p2.set_bool(":factor", false);
+ p2.set_uint("seed", 13);
+ p2.set_bool("factor", false);
return and_then(mk_simplify_tactic(m, p),
mk_nnf_tactic(m, p),
diff --git a/src/tactic/smtlogics/qfaufbv_tactic.cpp b/src/tactic/smtlogics/qfaufbv_tactic.cpp
index 5f371da0c..cb14fa778 100644
--- a/src/tactic/smtlogics/qfaufbv_tactic.cpp
+++ b/src/tactic/smtlogics/qfaufbv_tactic.cpp
@@ -29,22 +29,22 @@ Notes:
tactic * mk_qfaufbv_tactic(ast_manager & m, params_ref const & p) {
params_ref main_p;
- main_p.set_bool(":elim-and", true);
- main_p.set_bool(":sort-store", true);
+ main_p.set_bool("elim_and", true);
+ main_p.set_bool("sort_store", true);
params_ref simp2_p = p;
- simp2_p.set_bool(":som", true);
- simp2_p.set_bool(":pull-cheap-ite", true);
- simp2_p.set_bool(":push-ite-bv", false);
- simp2_p.set_bool(":local-ctx", true);
- simp2_p.set_uint(":local-ctx-limit", 10000000);
+ simp2_p.set_bool("som", true);
+ simp2_p.set_bool("pull_cheap_ite", true);
+ simp2_p.set_bool("push_ite_bv", false);
+ simp2_p.set_bool("local_ctx", true);
+ simp2_p.set_uint("local_ctx_limit", 10000000);
params_ref ctx_simp_p;
- ctx_simp_p.set_uint(":max-depth", 32);
- ctx_simp_p.set_uint(":max-steps", 5000000);
+ ctx_simp_p.set_uint("max_depth", 32);
+ ctx_simp_p.set_uint("max_steps", 5000000);
params_ref solver_p;
- solver_p.set_bool(":array-old-simplifier", false);
+ solver_p.set_bool("array.simplify", false); // disable array simplifications at old_simplify module
tactic * preamble_st = and_then(mk_simplify_tactic(m),
mk_propagate_values_tactic(m),
diff --git a/src/tactic/smtlogics/qfauflia_tactic.cpp b/src/tactic/smtlogics/qfauflia_tactic.cpp
index 422be13d5..89f96d354 100644
--- a/src/tactic/smtlogics/qfauflia_tactic.cpp
+++ b/src/tactic/smtlogics/qfauflia_tactic.cpp
@@ -26,16 +26,16 @@ Notes:
tactic * mk_qfauflia_tactic(ast_manager & m, params_ref const & p) {
params_ref main_p;
- main_p.set_bool(":elim-and", true);
- main_p.set_bool(":som", true);
- main_p.set_bool(":sort-store", true);
+ main_p.set_bool("elim_and", true);
+ main_p.set_bool("som", true);
+ main_p.set_bool("sort_store", true);
params_ref ctx_simp_p;
- ctx_simp_p.set_uint(":max-depth", 30);
- ctx_simp_p.set_uint(":max-steps", 5000000);
+ ctx_simp_p.set_uint("max_depth", 30);
+ ctx_simp_p.set_uint("max_steps", 5000000);
params_ref solver_p;
- solver_p.set_bool(":array-old-simplifier", false);
+ solver_p.set_bool("array.simplify", false); // disable array simplifications at old_simplify module
tactic * preamble_st = and_then(mk_simplify_tactic(m),
mk_propagate_values_tactic(m),
diff --git a/src/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp
index 5924c5bdf..51b040332 100644
--- a/src/tactic/smtlogics/qfbv_tactic.cpp
+++ b/src/tactic/smtlogics/qfbv_tactic.cpp
@@ -33,40 +33,40 @@ Notes:
tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) {
params_ref main_p;
- main_p.set_bool(":elim-and", true);
- main_p.set_bool(":push-ite-bv", true);
- main_p.set_bool(":blast-distinct", true);
+ main_p.set_bool("elim_and", true);
+ main_p.set_bool("push_ite_bv", true);
+ main_p.set_bool("blast_distinct", true);
params_ref simp2_p = p;
- simp2_p.set_bool(":som", true);
- simp2_p.set_bool(":pull-cheap-ite", true);
- simp2_p.set_bool(":push-ite-bv", false);
- simp2_p.set_bool(":local-ctx", true);
- simp2_p.set_uint(":local-ctx-limit", 10000000);
+ simp2_p.set_bool("som", true);
+ simp2_p.set_bool("pull_cheap_ite", true);
+ simp2_p.set_bool("push_ite_bv", false);
+ simp2_p.set_bool("local_ctx", true);
+ simp2_p.set_uint("local_ctx_limit", 10000000);
params_ref local_ctx_p = p;
- local_ctx_p.set_bool(":local-ctx", true);
+ local_ctx_p.set_bool("local_ctx", true);
params_ref solver_p;
- solver_p.set_bool(":preprocess", false); // preprocessor of smt::context is not needed.
+ solver_p.set_bool("preprocess", false); // preprocessor of smt::context is not needed.
params_ref no_flat_p;
- no_flat_p.set_bool(":flat", false);
+ no_flat_p.set_bool("flat", false);
params_ref ctx_simp_p;
- ctx_simp_p.set_uint(":max-depth", 32);
- ctx_simp_p.set_uint(":max-steps", 50000000);
+ ctx_simp_p.set_uint("max_depth", 32);
+ ctx_simp_p.set_uint("max_steps", 50000000);
params_ref hoist_p;
- hoist_p.set_bool(":hoist-mul", true);
- hoist_p.set_bool(":som", false);
+ hoist_p.set_bool("hoist_mul", true);
+ hoist_p.set_bool("som", false);
params_ref solve_eq_p;
// conservative guassian elimination.
- solve_eq_p.set_uint(":solve-eqs-max-occs", 2);
+ solve_eq_p.set_uint("solve_eqs_max_occs", 2);
params_ref big_aig_p;
- big_aig_p.set_bool(":aig-per-assertion", false);
+ big_aig_p.set_bool("aig_per_assertion", false);
tactic * preamble_st = and_then(and_then(mk_simplify_tactic(m),
mk_propagate_values_tactic(m),
@@ -74,7 +74,7 @@ tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) {
mk_elim_uncnstr_tactic(m),
if_no_proofs(if_no_unsat_cores(mk_bv_size_reduction_tactic(m))),
using_params(mk_simplify_tactic(m), simp2_p)),
- // Z3 can solve a couple of extra benchmarks by using :hoist-mul
+ // Z3 can solve a couple of extra benchmarks by using hoist_mul
// but the timeout in SMT-COMP is too small.
// Moreover, it impacted negatively some easy benchmarks.
// We should decide later, if we keep it or not.
diff --git a/src/tactic/smtlogics/qfidl_tactic.cpp b/src/tactic/smtlogics/qfidl_tactic.cpp
index 57aef4991..de05797e8 100644
--- a/src/tactic/smtlogics/qfidl_tactic.cpp
+++ b/src/tactic/smtlogics/qfidl_tactic.cpp
@@ -37,23 +37,23 @@ Notes:
tactic * mk_qfidl_tactic(ast_manager & m, params_ref const & p) {
params_ref main_p;
- main_p.set_bool(":elim-and", true);
- main_p.set_bool(":blast-distinct", true);
- main_p.set_bool(":som", true);
+ main_p.set_bool("elim_and", true);
+ main_p.set_bool("blast_distinct", true);
+ main_p.set_bool("som", true);
params_ref lhs_p;
- lhs_p.set_bool(":arith-lhs", true);
+ lhs_p.set_bool("arith_lhs", true);
params_ref lia2pb_p;
- lia2pb_p.set_uint(":lia2pb-max-bits", 4);
+ lia2pb_p.set_uint("lia2pb_max_bits", 4);
params_ref pb2bv_p;
- pb2bv_p.set_uint(":pb2bv-all-clauses-limit", 8);
+ pb2bv_p.set_uint("pb2bv_all_clauses_limit", 8);
params_ref pull_ite_p;
- pull_ite_p.set_bool(":pull-cheap-ite", true);
- pull_ite_p.set_bool(":local-ctx", true);
- pull_ite_p.set_uint(":local-ctx-limit", 10000000);
+ pull_ite_p.set_bool("pull_cheap_ite", true);
+ pull_ite_p.set_bool("local_ctx", true);
+ pull_ite_p.set_uint("local_ctx_limit", 10000000);
tactic * preamble_st = and_then(and_then(mk_simplify_tactic(m),
mk_fix_dl_var_tactic(m),
@@ -71,10 +71,10 @@ tactic * mk_qfidl_tactic(ast_manager & m, params_ref const & p) {
params_ref bv_solver_p;
// The cardinality constraint encoding generates a lot of shared if-then-else's that can be flattened.
// Several of them are simplified to and/or. If we flat them, we increase a lot the memory consumption.
- bv_solver_p.set_bool(":flat", false);
- bv_solver_p.set_bool(":som", false);
+ bv_solver_p.set_bool("flat", false);
+ bv_solver_p.set_bool("som", false);
// dynamic psm seems to work well.
- bv_solver_p.set_sym(":gc-strategy", symbol("dyn-psm"));
+ bv_solver_p.set_sym("gc", symbol("dyn_psm"));
tactic * bv_solver = using_params(and_then(mk_simplify_tactic(m),
mk_propagate_values_tactic(m),
@@ -93,7 +93,7 @@ tactic * mk_qfidl_tactic(ast_manager & m, params_ref const & p) {
bv_solver);
params_ref diff_neq_p;
- diff_neq_p.set_uint(":diff-neq-max-k", 25);
+ diff_neq_p.set_uint("diff_neq_max_k", 25);
tactic * st = cond(mk_and(mk_lt(mk_num_consts_probe(), mk_const_probe(static_cast(BIG_PROBLEM))),
mk_and(mk_not(mk_produce_proofs_probe()),
diff --git a/src/tactic/smtlogics/qflia_tactic.cpp b/src/tactic/smtlogics/qflia_tactic.cpp
index 1fb30faae..6b05cff96 100644
--- a/src/tactic/smtlogics/qflia_tactic.cpp
+++ b/src/tactic/smtlogics/qflia_tactic.cpp
@@ -64,17 +64,17 @@ probe * mk_quasi_pb_probe() {
// Create SMT solver that does not use cuts
static tactic * mk_no_cut_smt_tactic(unsigned rs) {
params_ref solver_p;
- solver_p.set_uint(":arith-branch-cut-ratio", 10000000);
- solver_p.set_uint(":random-seed", rs);
+ solver_p.set_uint("arith.branch_cut_ratio", 10000000);
+ solver_p.set_uint("random_seed", rs);
return using_params(mk_smt_tactic_using(false), solver_p);
}
// Create SMT solver that does not use cuts
static tactic * mk_no_cut_no_relevancy_smt_tactic(unsigned rs) {
params_ref solver_p;
- solver_p.set_uint(":arith-branch-cut-ratio", 10000000);
- solver_p.set_uint(":random-seed", rs);
- solver_p.set_uint(":relevancy", 0);
+ solver_p.set_uint("arith.branch_cut_ratio", 10000000);
+ solver_p.set_uint("random_seed", rs);
+ solver_p.set_uint("relevancy", 0);
return using_params(mk_smt_tactic_using(false), solver_p);
}
@@ -82,10 +82,10 @@ static tactic * mk_bv2sat_tactic(ast_manager & m) {
params_ref solver_p;
// The cardinality constraint encoding generates a lot of shared if-then-else's that can be flattened.
// Several of them are simplified to and/or. If we flat them, we increase a lot the memory consumption.
- solver_p.set_bool(":flat", false);
- solver_p.set_bool(":som", false);
+ solver_p.set_bool("flat", false);
+ solver_p.set_bool("som", false);
// dynamic psm seems to work well.
- solver_p.set_sym(":gc-strategy", symbol("dyn-psm"));
+ solver_p.set_sym("gc", symbol("dyn_psm"));
return using_params(and_then(mk_simplify_tactic(m),
mk_propagate_values_tactic(m),
@@ -101,8 +101,8 @@ static tactic * mk_bv2sat_tactic(ast_manager & m) {
static tactic * mk_pb_tactic(ast_manager & m) {
params_ref pb2bv_p;
- pb2bv_p.set_bool(":ite-extra", true);
- pb2bv_p.set_uint(":pb2bv-all-clauses-limit", 8);
+ pb2bv_p.set_bool("ite_extra", true);
+ pb2bv_p.set_uint("pb2bv_all_clauses_limit", 8);
return and_then(fail_if_not(mk_is_pb_probe()),
fail_if(mk_produce_proofs_probe()),
@@ -119,8 +119,8 @@ static tactic * mk_pb_tactic(ast_manager & m) {
static tactic * mk_lia2sat_tactic(ast_manager & m) {
params_ref pb2bv_p;
- pb2bv_p.set_bool(":ite-extra", true);
- pb2bv_p.set_uint(":pb2bv-all-clauses-limit", 8);
+ pb2bv_p.set_bool("ite_extra", true);
+ pb2bv_p.set_uint("pb2bv_all_clauses_limit", 8);
return and_then(fail_if(mk_is_unbounded_probe()),
fail_if(mk_produce_proofs_probe()),
@@ -137,11 +137,11 @@ static tactic * mk_lia2sat_tactic(ast_manager & m) {
// Fails if the problem is no ILP.
static tactic * mk_ilp_model_finder_tactic(ast_manager & m) {
params_ref add_bounds_p1;
- add_bounds_p1.set_rat(":add-bound-lower", rational(-16));
- add_bounds_p1.set_rat(":add-bound-upper", rational(15));
+ add_bounds_p1.set_rat("add_bound_lower", rational(-16));
+ add_bounds_p1.set_rat("add_bound_upper", rational(15));
params_ref add_bounds_p2;
- add_bounds_p2.set_rat(":add-bound-lower", rational(-32));
- add_bounds_p2.set_rat(":add-bound-upper", rational(31));
+ add_bounds_p2.set_rat("add_bound_lower", rational(-32));
+ add_bounds_p2.set_rat("add_bound_upper", rational(31));
return and_then(fail_if_not(mk_and(mk_is_ilp_probe(), mk_is_unbounded_probe())),
fail_if(mk_produce_proofs_probe()),
@@ -170,22 +170,22 @@ static tactic * mk_bounded_tactic(ast_manager & m) {
tactic * mk_qflia_tactic(ast_manager & m, params_ref const & p) {
params_ref main_p;
- main_p.set_bool(":elim-and", true);
- main_p.set_bool(":som", true);
- // main_p.set_bool(":push-ite-arith", true);
+ main_p.set_bool("elim_and", true);
+ main_p.set_bool("som", true);
+ // main_p.set_bool("push_ite_arith", true);
params_ref pull_ite_p;
- pull_ite_p.set_bool(":pull-cheap-ite", true);
- pull_ite_p.set_bool(":push-ite-arith", false);
- pull_ite_p.set_bool(":local-ctx", true);
- pull_ite_p.set_uint(":local-ctx-limit", 10000000);
+ pull_ite_p.set_bool("pull_cheap_ite", true);
+ pull_ite_p.set_bool("push_ite_arith", false);
+ pull_ite_p.set_bool("local_ctx", true);
+ pull_ite_p.set_uint("local_ctx_limit", 10000000);
params_ref ctx_simp_p;
- ctx_simp_p.set_uint(":max-depth", 30);
- ctx_simp_p.set_uint(":max-steps", 5000000);
+ ctx_simp_p.set_uint("max_depth", 30);
+ ctx_simp_p.set_uint("max_steps", 5000000);
params_ref lhs_p;
- lhs_p.set_bool(":arith-lhs", true);
+ lhs_p.set_bool("arith_lhs", true);
tactic * preamble_st = and_then(and_then(mk_simplify_tactic(m),
mk_propagate_values_tactic(m),
@@ -197,10 +197,10 @@ tactic * mk_qflia_tactic(ast_manager & m, params_ref const & p) {
);
params_ref quasi_pb_p;
- quasi_pb_p.set_uint(":lia2pb-max-bits", 64);
+ quasi_pb_p.set_uint("lia2pb_max_bits", 64);
params_ref no_cut_p;
- no_cut_p.set_uint(":arith-branch-cut-ratio", 10000000);
+ no_cut_p.set_uint("arith.branch_cut_ratio", 10000000);
tactic * st = using_params(and_then(preamble_st,
diff --git a/src/tactic/smtlogics/qflra_tactic.cpp b/src/tactic/smtlogics/qflra_tactic.cpp
index 42aaa96b7..41f0e16f3 100644
--- a/src/tactic/smtlogics/qflra_tactic.cpp
+++ b/src/tactic/smtlogics/qflra_tactic.cpp
@@ -29,23 +29,23 @@ Notes:
tactic * mk_qflra_tactic(ast_manager & m, params_ref const & p) {
params_ref pivot_p;
- pivot_p.set_bool(":arith-greatest-error-pivot", true);
+ pivot_p.set_bool("arith.greatest_error_pivot", true);
params_ref main_p = p;
- main_p.set_bool(":elim-and", true);
- main_p.set_bool(":som", true);
- main_p.set_bool(":blast-distinct", true);
+ main_p.set_bool("elim_and", true);
+ main_p.set_bool("som", true);
+ main_p.set_bool("blast_distinct", true);
params_ref ctx_simp_p;
- ctx_simp_p.set_uint(":max-depth", 30);
- ctx_simp_p.set_uint(":max-steps", 5000000);
+ ctx_simp_p.set_uint("max_depth", 30);
+ ctx_simp_p.set_uint("max_steps", 5000000);
params_ref lhs_p;
- lhs_p.set_bool(":arith-lhs", true);
- lhs_p.set_bool(":eq2ineq", true);
+ lhs_p.set_bool("arith_lhs", true);
+ lhs_p.set_bool("eq2ineq", true);
params_ref elim_to_real_p;
- elim_to_real_p.set_bool(":elim-to-real", true);
+ elim_to_real_p.set_bool("elim_to_real", true);
#if 0
diff --git a/src/tactic/smtlogics/qfnia_tactic.cpp b/src/tactic/smtlogics/qfnia_tactic.cpp
index e87d36503..950291221 100644
--- a/src/tactic/smtlogics/qfnia_tactic.cpp
+++ b/src/tactic/smtlogics/qfnia_tactic.cpp
@@ -31,14 +31,14 @@ Notes:
tactic * mk_qfnia_bv_solver(ast_manager & m, params_ref const & p_ref) {
params_ref p = p_ref;
- p.set_bool(":flat", false);
- p.set_bool(":hi-div0", true);
- p.set_bool(":elim-and", true);
- p.set_bool(":blast-distinct", true);
+ p.set_bool("flat", false);
+ p.set_bool("hi_div0", true);
+ p.set_bool("elim_and", true);
+ p.set_bool("blast_distinct", true);
params_ref simp2_p = p;
- simp2_p.set_bool(":local-ctx", true);
- simp2_p.set_uint(":local-ctx-limit", 10000000);
+ simp2_p.set_bool("local_ctx", true);
+ simp2_p.set_uint("local_ctx_limit", 10000000);
tactic * r = using_params(and_then(mk_simplify_tactic(m),
@@ -53,19 +53,19 @@ tactic * mk_qfnia_bv_solver(ast_manager & m, params_ref const & p_ref) {
tactic * mk_qfnia_premable(ast_manager & m, params_ref const & p_ref) {
params_ref pull_ite_p = p_ref;
- pull_ite_p.set_bool(":pull-cheap-ite", true);
- pull_ite_p.set_bool(":local-ctx", true);
- pull_ite_p.set_uint(":local-ctx-limit", 10000000);
+ pull_ite_p.set_bool("pull_cheap_ite", true);
+ pull_ite_p.set_bool("local_ctx", true);
+ pull_ite_p.set_uint("local_ctx_limit", 10000000);
params_ref ctx_simp_p = p_ref;
- ctx_simp_p.set_uint(":max-depth", 30);
- ctx_simp_p.set_uint(":max-steps", 5000000);
+ ctx_simp_p.set_uint("max_depth", 30);
+ ctx_simp_p.set_uint("max_steps", 5000000);
params_ref simp_p = p_ref;
- simp_p.set_bool(":hoist-mul", true);
+ simp_p.set_bool("hoist_mul", true);
params_ref elim_p = p_ref;
- elim_p.set_uint(":max-memory",20);
+ elim_p.set_uint("max_memory",20);
return
and_then(mk_simplify_tactic(m),
@@ -79,7 +79,7 @@ tactic * mk_qfnia_premable(ast_manager & m, params_ref const & p_ref) {
tactic * mk_qfnia_sat_solver(ast_manager & m, params_ref const & p) {
params_ref nia2sat_p = p;
- nia2sat_p.set_uint(":nla2bv-max-bv-size", 64);
+ nia2sat_p.set_uint("nla2bv_max_bv_size", 64);
return and_then(mk_nla2bv_tactic(m, nia2sat_p),
mk_qfnia_bv_solver(m, p),
diff --git a/src/tactic/smtlogics/qfnra_tactic.cpp b/src/tactic/smtlogics/qfnra_tactic.cpp
index a2877eefa..716b4868b 100644
--- a/src/tactic/smtlogics/qfnra_tactic.cpp
+++ b/src/tactic/smtlogics/qfnra_tactic.cpp
@@ -25,7 +25,7 @@ Notes:
static tactic * mk_qfnra_sat_solver(ast_manager& m, params_ref const& p, unsigned bv_size) {
params_ref nra2sat_p = p;
- nra2sat_p.set_uint(":nla2bv-max-bv-size", p.get_uint("nla2bv_max_bv_size", bv_size));
+ nra2sat_p.set_uint("nla2bv_max_bv_size", p.get_uint("nla2bv_max_bv_size", bv_size));
return and_then(mk_nla2bv_tactic(m, nra2sat_p),
mk_smt_tactic(),
@@ -34,11 +34,11 @@ static tactic * mk_qfnra_sat_solver(ast_manager& m, params_ref const& p, unsigne
tactic * mk_qfnra_tactic(ast_manager & m, params_ref const& p) {
params_ref p1 = p;
- p1.set_uint(":seed", 11);
- p1.set_bool(":factor", false);
+ p1.set_uint("seed", 11);
+ p1.set_bool("factor", false);
params_ref p2 = p;
- p2.set_uint(":seed", 13);
- p2.set_bool(":factor", false);
+ p2.set_uint("seed", 13);
+ p2.set_bool("factor", false);
return and_then(mk_simplify_tactic(m, p),
mk_propagate_values_tactic(m, p),
diff --git a/src/tactic/smtlogics/qfuf_tactic.cpp b/src/tactic/smtlogics/qfuf_tactic.cpp
index 3acfb8d98..567325f6a 100644
--- a/src/tactic/smtlogics/qfuf_tactic.cpp
+++ b/src/tactic/smtlogics/qfuf_tactic.cpp
@@ -26,9 +26,9 @@ Notes:
tactic * mk_qfuf_tactic(ast_manager & m, params_ref const & p) {
params_ref s2_p;
- s2_p.set_bool(":pull-cheap-ite", true);
- s2_p.set_bool(":local-ctx", true);
- s2_p.set_uint(":local-ctx-limit", 10000000);
+ s2_p.set_bool("pull_cheap_ite", true);
+ s2_p.set_bool("local_ctx", true);
+ s2_p.set_uint("local_ctx_limit", 10000000);
return and_then(mk_simplify_tactic(m, p),
mk_propagate_values_tactic(m, p),
mk_solve_eqs_tactic(m, p),
diff --git a/src/tactic/smtlogics/qfufbv_tactic.cpp b/src/tactic/smtlogics/qfufbv_tactic.cpp
index 400ff9891..d10b7c1b4 100644
--- a/src/tactic/smtlogics/qfufbv_tactic.cpp
+++ b/src/tactic/smtlogics/qfufbv_tactic.cpp
@@ -28,8 +28,8 @@ Notes:
tactic * mk_qfufbv_tactic(ast_manager & m, params_ref const & p) {
params_ref main_p;
- main_p.set_bool(":elim-and", true);
- main_p.set_bool(":blast-distinct", true);
+ main_p.set_bool("elim_and", true);
+ main_p.set_bool("blast_distinct", true);
tactic * preamble_st = and_then(mk_simplify_tactic(m),
mk_propagate_values_tactic(m),
diff --git a/src/tactic/smtlogics/quant_tactics.cpp b/src/tactic/smtlogics/quant_tactics.cpp
index 4bb896c74..6b5ede813 100644
--- a/src/tactic/smtlogics/quant_tactics.cpp
+++ b/src/tactic/smtlogics/quant_tactics.cpp
@@ -27,13 +27,13 @@ Revision History:
static tactic * mk_quant_preprocessor(ast_manager & m, bool disable_gaussian = false) {
params_ref pull_ite_p;
- pull_ite_p.set_bool(":pull-cheap-ite", true);
- pull_ite_p.set_bool(":local-ctx", true);
- pull_ite_p.set_uint(":local-ctx-limit", 10000000);
+ pull_ite_p.set_bool("pull_cheap_ite", true);
+ pull_ite_p.set_bool("local_ctx", true);
+ pull_ite_p.set_uint("local_ctx_limit", 10000000);
params_ref ctx_simp_p;
- ctx_simp_p.set_uint(":max-depth", 30);
- ctx_simp_p.set_uint(":max-steps", 5000000);
+ ctx_simp_p.set_uint("max_depth", 30);
+ ctx_simp_p.set_uint("max_steps", 5000000);
tactic * solve_eqs;
if (disable_gaussian)
@@ -71,8 +71,8 @@ tactic * mk_uflra_tactic(ast_manager & m, params_ref const & p) {
tactic * mk_auflia_tactic(ast_manager & m, params_ref const & p) {
params_ref qi_p;
- qi_p.set_str(":qi-cost", "0");
- TRACE("qi_cost", qi_p.display(tout); tout << "\n" << qi_p.get_str("qi_cost", "") << "\n";);
+ qi_p.set_str("qi.cost", "0");
+ TRACE("qi_cost", qi_p.display(tout); tout << "\n" << qi_p.get_str("qi.cost", "") << "\n";);
tactic * st = and_then(mk_no_solve_eq_preprocessor(m),
or_else(and_then(fail_if(mk_gt(mk_num_exprs_probe(), mk_const_probe(static_cast(128)))),
using_params(mk_smt_tactic(), qi_p),
diff --git a/src/tactic/ufbv/ufbv_tactic.cpp b/src/tactic/ufbv/ufbv_tactic.cpp
index 85ec506aa..80d403b67 100644
--- a/src/tactic/ufbv/ufbv_tactic.cpp
+++ b/src/tactic/ufbv/ufbv_tactic.cpp
@@ -37,7 +37,7 @@ tactic * mk_der_fp_tactic(ast_manager & m, params_ref const & p) {
tactic * mk_ufbv_preprocessor_tactic(ast_manager & m, params_ref const & p) {
params_ref no_elim_and(p);
- no_elim_and.set_bool(":elim-and", false);
+ no_elim_and.set_bool("elim_and", false);
return and_then(
mk_trace_tactic("ufbv_pre"),
@@ -61,10 +61,10 @@ tactic * mk_ufbv_preprocessor_tactic(ast_manager & m, params_ref const & p) {
tactic * mk_ufbv_tactic(ast_manager & m, params_ref const & p) {
params_ref main_p(p);
- main_p.set_bool(":mbqi", true);
- main_p.set_uint(":mbqi-max-iterations", -1);
- main_p.set_bool(":elim-and", true);
- main_p.set_bool(":solver", true);
+ main_p.set_bool("mbqi", true);
+ main_p.set_uint("mbqi_max_iterations", -1);
+ main_p.set_bool("elim_and", true);
+ main_p.set_bool("solver", true);
tactic * t = and_then(repeat(mk_ufbv_preprocessor_tactic(m, main_p), 2),
mk_smt_tactic_using(false, main_p));
diff --git a/src/test/dl_context.cpp b/src/test/dl_context.cpp
index cdc9c52d9..d5fcddb71 100644
--- a/src/test/dl_context.cpp
+++ b/src/test/dl_context.cpp
@@ -72,9 +72,9 @@ void tst_dl_context() {
params_ref params;
for(unsigned rel_index=0; rel_index=0; eager_checking--) {
- params.set_bool(":eager-emptiness-checking", eager_checking!=0);
+ params.set_bool("eager_emptiness_checking", eager_checking!=0);
std::cerr << "Testing " << relations[rel_index] << "\n";
std::cerr << "Eager emptiness checking " << (eager_checking!=0 ? "on" : "off") << "\n";
diff --git a/src/test/dl_product_relation.cpp b/src/test/dl_product_relation.cpp
index 3fd81bc81..ef43258ad 100644
--- a/src/test/dl_product_relation.cpp
+++ b/src/test/dl_product_relation.cpp
@@ -344,7 +344,7 @@ void tst_dl_product_relation() {
test_functional_columns(fparams, params);
- params.set_sym(":default-relation", symbol("tr_sparse"));
+ params.set_sym("default_relation", symbol("tr_sparse"));
test_finite_product_relation(fparams, params);
}
diff --git a/src/test/dl_query.cpp b/src/test/dl_query.cpp
index 5e61c1836..a642be9d6 100644
--- a/src/test/dl_query.cpp
+++ b/src/test/dl_query.cpp
@@ -49,8 +49,13 @@ void dl_query_test(ast_manager & m, smt_params & fparams, params_ref& params,
dl_decl_util decl_util(m);
+<<<<<<< HEAD
context ctx_q(m, fparams);
params.set_bool(":magic-sets-for-queries", use_magic_sets);
+=======
+ context ctx_q(m, fparams);
+ params.set_bool("magic_sets_for_queries", use_magic_sets);
+>>>>>>> 3736c5ea3b97521dad85cdc6262151fae2875ec5
ctx_q.updt_params(params);
{
parser* p = parser::create(ctx_q,m);
@@ -125,7 +130,7 @@ void dl_query_test(ast_manager & m, smt_params & fparams, params_ref& params,
}
void dl_query_test_wpa(smt_params & fparams, params_ref& params) {
- params.set_bool(":magic-sets-for-queries", true);
+ params.set_bool("magic_sets_for_queries", true);
ast_manager m;
reg_decl_plugins(m);
arith_util arith(m);
@@ -185,8 +190,8 @@ void dl_query_test_wpa(smt_params & fparams, params_ref& params) {
void tst_dl_query() {
smt_params fparams;
params_ref params;
- params.set_sym(":default-table", symbol("sparse"));
- params.set_sym(":default-relation", symbol("tr_sparse"));
+ params.set_sym("default_table", symbol("sparse"));
+ params.set_sym("default_relation", symbol("tr_sparse"));
//params.m_dl_default_table = symbol("hashtable");
//params.m_dl_default_relation = symbol("tr_hashtable");
@@ -212,9 +217,9 @@ void tst_dl_query() {
ctx_base.get_rel_context().saturate();
for(unsigned use_restarts=0; use_restarts<=1; use_restarts++) {
- params.set_uint(":initial-restart-timeout", use_restarts ? 100 : 0);
+ params.set_uint("initial_restart_timeout", use_restarts ? 100 : 0);
for(unsigned use_similar=0; use_similar<=1; use_similar++) {
- params.set_uint(":similarity-compressor", use_similar != 0);
+ params.set_uint("similarity_compressor", use_similar != 0);
for(unsigned use_magic_sets=0; use_magic_sets<=1; use_magic_sets++) {
stopwatch watch;
diff --git a/src/util/debug.cpp b/src/util/debug.cpp
index 41e0a48fc..75ea8586a 100644
--- a/src/util/debug.cpp
+++ b/src/util/debug.cpp
@@ -22,6 +22,7 @@ Revision History:
#endif
#include
#include"str_hashtable.h"
+#include"z3_exception.h"
volatile bool g_enable_assertions = true;
@@ -73,7 +74,7 @@ void invoke_gdb() {
char buffer[1024];
int * x = 0;
for (;;) {
- std::cerr << "(C)ontinue, (A)bort, (S)top, Invoke (G)DB\n";
+ std::cerr << "(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB\n";
char result;
std::cin >> result;
switch(result) {
@@ -88,6 +89,9 @@ void invoke_gdb() {
// force seg fault...
*x = 0;
return;
+ case 't':
+ case 'T':
+ throw default_exception("assertion violation");
case 'G':
case 'g':
sprintf(buffer, "gdb -nw /proc/%d/exe %d", getpid(), getpid());
diff --git a/src/util/gparams.cpp b/src/util/gparams.cpp
index 4aecd0c05..b81531798 100644
--- a/src/util/gparams.cpp
+++ b/src/util/gparams.cpp
@@ -35,6 +35,47 @@ bool is_old_param_name(symbol const & name) {
return false;
}
+char const * g_params_renames[] = {
+ "proof_mode", "proof",
+ "soft_timeout", "timeout",
+ "mbqi", "smt.mbqi",
+ "relevancy", "smt.relevancy",
+ "ematching", "smt.ematching",
+ "macro_finder", "smt.macro_finder",
+ "delay_units", "smt.delay_units",
+ "case_split", "smt.case_split",
+ "phase_selection", "smt.phase_selection",
+ "restart_strategy", "smt.restart_strategy",
+ "restart_factor", "smt.restart_factor",
+ "arith_random_initial_value", "smt.arith.random_initial_value",
+ "bv_reflect", "smt.bv.reflect",
+ "qi_cost", "smt.qi.cost",
+ "qi_eager_threshold", "smt.qi.eager_threshold",
+ "nl_arith", "smt.arith.nl",
+ "nnf_sk_hack", "nnf.sk_hack",
+ "model_v2", "model.v2",
+ "pi_non_nested_arith_weight", "pi.non_nested_arith_weight",
+ "pi_warnings", "pi.warnings",
+ "pp_decimal", "pp.decimal",
+ "pp_decimal", "pp.decimal_precision",
+ "pp_bv_literals", "pp.bv_literals",
+ "pp_bv_neg", "pp.bv_neg",
+ "pp_max_depth", "pp.max_depth",
+ "pp_min_alias_size", "pp.min_alias_size",
+ 0 };
+
+char const * get_new_param_name(symbol const & p) {
+ char const * const * it = g_params_renames;
+ while (*it) {
+ if (p == *it) {
+ it++;
+ return *it;
+ }
+ it += 2;
+ }
+ return 0;
+}
+
struct gparams::imp {
bool m_modules_registered;
dictionary m_module_param_descrs;
@@ -60,19 +101,24 @@ public:
}
~imp() {
- {
- dictionary::iterator it = m_module_param_descrs.begin();
- dictionary::iterator end = m_module_param_descrs.end();
- for (; it != end; ++it) {
- dealloc(it->m_value);
- }
+ reset();
+ dictionary::iterator it = m_module_param_descrs.begin();
+ dictionary::iterator end = m_module_param_descrs.end();
+ for (; it != end; ++it) {
+ dealloc(it->m_value);
}
+ }
+
+ void reset() {
+ #pragma omp critical (gparams)
{
+ m_params.reset();
dictionary::iterator it = m_module_params.begin();
dictionary::iterator end = m_module_params.end();
for (; it != end; ++it) {
dealloc(it->m_value);
}
+ m_module_params.reset();
}
}
@@ -155,7 +201,12 @@ public:
void throw_unknown_parameter(symbol const & param_name, symbol const & mod_name) {
if (mod_name == symbol::null) {
- if (is_old_param_name(param_name)) {
+ char const * new_name = get_new_param_name(param_name);
+ if (new_name) {
+ throw exception("the parameter '%s' was renamed to '%s', invoke 'z3 -p' to obtain the new parameter list, and 'z3 -pp:%s' for the full description of the parameter",
+ param_name.bare_str(), new_name, new_name);
+ }
+ else if (is_old_param_name(param_name)) {
throw exception("unknown parameter '%s', this is an old parameter name, invoke 'z3 -p' to obtain the new parameter list",
param_name.bare_str());
}
@@ -178,6 +229,11 @@ public:
long val = strtol(value, 0, 10);
ps.set_uint(param_name, static_cast(val));
}
+ else if (k == CPK_DOUBLE) {
+ char * aux;
+ double val = strtod(value, &aux);
+ ps.set_double(param_name, val);
+ }
else if (k == CPK_BOOL) {
if (strcmp(value, "true") == 0) {
ps.set_bool(param_name, true);
@@ -196,7 +252,16 @@ public:
ps.set_sym(param_name, symbol(value));
}
else if (k == CPK_STRING) {
- ps.set_str(param_name, value);
+ // There is no guarantee that (external) callers will not delete value after invoking gparams::set.
+ // I see two solutions:
+ // 1) Modify params_ref to create a copy of set_str parameters.
+ // This solution is not nice since we create copies and move the params_ref around.
+ // We would have to keep copying the strings.
+ // Moreover, when we use params_ref internally, the value is usually a static value.
+ // So, we would be paying this price for nothing.
+ // 2) "Copy" value by transforming it into a symbol.
+ // I'm using this solution for now.
+ ps.set_str(param_name, symbol(value).bare_str());
}
else {
if (mod_name == symbol::null)
@@ -434,6 +499,11 @@ public:
gparams::imp * gparams::g_imp = 0;
+void gparams::reset() {
+ SASSERT(g_imp != 0);
+ g_imp->reset();
+}
+
void gparams::set(char const * name, char const * value) {
TRACE("gparams", tout << "setting [" << name << "] <- '" << value << "'\n";);
SASSERT(g_imp != 0);
diff --git a/src/util/gparams.h b/src/util/gparams.h
index a41044c84..a55761830 100644
--- a/src/util/gparams.h
+++ b/src/util/gparams.h
@@ -27,6 +27,11 @@ class gparams {
public:
typedef default_exception exception;
+ /**
+ \brief Reset all global and module parameters.
+ */
+ static void reset();
+
/**
\brief Set a global parameter \c name with \c value.
diff --git a/src/util/params.cpp b/src/util/params.cpp
index c0b8653ae..f302f7721 100644
--- a/src/util/params.cpp
+++ b/src/util/params.cpp
@@ -21,6 +21,29 @@ Notes:
#include"symbol.h"
#include"dictionary.h"
+std::string norm_param_name(char const * n) {
+ if (n == 0)
+ return "_";
+ if (*n == ':')
+ n++;
+ std::string r = n;
+ unsigned sz = r.size();
+ if (sz == 0)
+ return "_";
+ for (unsigned i = 0; i < sz; i++) {
+ char curr = r[i];
+ if ('A' <= curr && curr <= 'Z')
+ r[i] = curr - 'A' + 'a';
+ else if (curr == '-' || curr == ':')
+ r[i] = '_';
+ }
+ return r;
+}
+
+std::string norm_param_name(symbol const & n) {
+ return norm_param_name(n.bare_str());
+}
+
struct param_descrs::imp {
struct info {
param_kind m_kind;
diff --git a/src/util/params.h b/src/util/params.h
index 164de9ab3..13850758c 100644
--- a/src/util/params.h
+++ b/src/util/params.h
@@ -22,6 +22,9 @@ Notes:
#include"cmd_context_types.h"
#include"vector.h"
+std::string norm_param_name(char const * n);
+std::string norm_param_name(symbol const & n);
+
typedef cmd_arg_kind param_kind;
class params;