Merge branch 'upstream-master' into develop

README.md

@@ -124,7 +124,7 @@ utility is used to install ``Microsoft.Z3.dll`` into the
 [pkg-config](http://www.freedesktop.org/wiki/Software/pkg-config/) file
 (``Microsoft.Z3.Sharp.pc``) is also installed which allows the
 [MonoDevelop](http://www.monodevelop.com/) IDE to find the bindings. Running
-``make uninstall`` will remove the dll from the GAC and the pkg-config file.
+``make uninstall`` will remove the dll from the GAC and the ``pkg-config`` file.
 
 See [``examples/dotnet``](examples/dotnet) for examples.
 
@@ -170,8 +170,8 @@ If you do need to install to a non standard prefix a better approach is to use
 a [Python virtual environment](https://virtualenv.readthedocs.org/en/latest/)
 and install Z3 there. Python packages also work for Python3.
 Under Windows, recall to build inside the Visual C++ native command build environment.
-Note that the buit/python/z3 directory should be accessible from where python is used with Z3 
+Note that the ``build/python/z3`` directory should be accessible from where python is used with Z3 
-and it depends on libz3.dll to be in the path.
+and it depends on ``libz3.dll`` to be in the path.
 
 ```bash
 virtualenv venv

examples/c/CMakeLists.txt

@@ -7,6 +7,19 @@
 # the C++ standard library in resulting in a link failure.
 project(Z3_C_EXAMPLE C CXX)
 cmake_minimum_required(VERSION 2.8.12)
+
+# Set C version required to C99
+if ("${CMAKE_VERSION}" VERSION_LESS "3.1")
+  if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU") OR
+      ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang"))
+    set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -std=c99 ")
+  endif()
+else()
+  set(CMAKE_C_STANDARD_REQUIRED ON)
+  set(CMAKE_C_STANDARD 99)
+  set(CMAKE_C_EXTENSIONS OFF)
+endif()
+
 find_package(Z3
   REQUIRED
   CONFIG

examples/c/test_capi.c

@@ -2769,80 +2769,279 @@ void fpa_example() {
     double_sort = Z3_mk_fpa_sort(ctx, 11, 53);
     rm_sort = Z3_mk_fpa_rounding_mode_sort(ctx);
 
-	// Show that there are x, y s.t. (x + y) = 42.0 (with rounding mode).
+    // Show that there are x, y s.t. (x + y) = 42.0 (with rounding mode).
-	s_rm = Z3_mk_string_symbol(ctx, "rm");
+    s_rm = Z3_mk_string_symbol(ctx, "rm");
-	rm = Z3_mk_const(ctx, s_rm, rm_sort);
+    rm = Z3_mk_const(ctx, s_rm, rm_sort);
-	s_x = Z3_mk_string_symbol(ctx, "x");
+    s_x = Z3_mk_string_symbol(ctx, "x");
-	s_y = Z3_mk_string_symbol(ctx, "y");
+    s_y = Z3_mk_string_symbol(ctx, "y");
-	x = Z3_mk_const(ctx, s_x, double_sort);
+    x = Z3_mk_const(ctx, s_x, double_sort);
-	y = Z3_mk_const(ctx, s_y, double_sort);
+    y = Z3_mk_const(ctx, s_y, double_sort);
-	n = Z3_mk_fpa_numeral_double(ctx, 42.0, double_sort);
+    n = Z3_mk_fpa_numeral_double(ctx, 42.0, double_sort);
-
+    
-	s_x_plus_y = Z3_mk_string_symbol(ctx, "x_plus_y");
+    s_x_plus_y = Z3_mk_string_symbol(ctx, "x_plus_y");
-	x_plus_y = Z3_mk_const(ctx, s_x_plus_y, double_sort);
+    x_plus_y = Z3_mk_const(ctx, s_x_plus_y, double_sort);
-	c1 = Z3_mk_eq(ctx, x_plus_y, Z3_mk_fpa_add(ctx, rm, x, y));
+    c1 = Z3_mk_eq(ctx, x_plus_y, Z3_mk_fpa_add(ctx, rm, x, y));
-
+    
-	args[0] = c1;
+    args[0] = c1;
-	args[1] = Z3_mk_eq(ctx, x_plus_y, n);
+    args[1] = Z3_mk_eq(ctx, x_plus_y, n);
-	c2 = Z3_mk_and(ctx, 2, (Z3_ast*)&args);
+    c2 = Z3_mk_and(ctx, 2, (Z3_ast*)&args);
-
+    
-	args2[0] = c2;
+    args2[0] = c2;
-	args2[1] = Z3_mk_not(ctx, Z3_mk_eq(ctx, rm, Z3_mk_fpa_rtz(ctx)));
+    args2[1] = Z3_mk_not(ctx, Z3_mk_eq(ctx, rm, Z3_mk_fpa_rtz(ctx)));
-	c3 = Z3_mk_and(ctx, 2, (Z3_ast*)&args2);
+    c3 = Z3_mk_and(ctx, 2, (Z3_ast*)&args2);
-
+    
-	and_args[0] = Z3_mk_not(ctx, Z3_mk_fpa_is_zero(ctx, y));
+    and_args[0] = Z3_mk_not(ctx, Z3_mk_fpa_is_zero(ctx, y));
-	and_args[1] = Z3_mk_not(ctx, Z3_mk_fpa_is_nan(ctx, y));
+    and_args[1] = Z3_mk_not(ctx, Z3_mk_fpa_is_nan(ctx, y));
-	and_args[2] = Z3_mk_not(ctx, Z3_mk_fpa_is_infinite(ctx, y));
+    and_args[2] = Z3_mk_not(ctx, Z3_mk_fpa_is_infinite(ctx, y));
-	args3[0] = c3;
+    args3[0] = c3;
-	args3[1] = Z3_mk_and(ctx, 3, and_args);
+    args3[1] = Z3_mk_and(ctx, 3, and_args);
-	c4 = Z3_mk_and(ctx, 2, (Z3_ast*)&args3);
+    c4 = Z3_mk_and(ctx, 2, (Z3_ast*)&args3);
-
+    
-	printf("c4: %s\n", Z3_ast_to_string(ctx, c4));
+    printf("c4: %s\n", Z3_ast_to_string(ctx, c4));
-	Z3_solver_push(ctx, s);
+    Z3_solver_push(ctx, s);
-	Z3_solver_assert(ctx, s, c4);
+    Z3_solver_assert(ctx, s, c4);
-	check(ctx, s, Z3_L_TRUE);
+    check(ctx, s, Z3_L_TRUE);
-	Z3_solver_pop(ctx, s, 1);
+    Z3_solver_pop(ctx, s, 1);
-
+    
-	// Show that the following are equal:
+    // Show that the following are equal:
-	//   (fp #b0 #b10000000001 #xc000000000000)
+    //   (fp #b0 #b10000000001 #xc000000000000)
-	//   ((_ to_fp 11 53) #x401c000000000000))
+    //   ((_ to_fp 11 53) #x401c000000000000))
-	//   ((_ to_fp 11 53) RTZ 1.75 2)))
+    //   ((_ to_fp 11 53) RTZ 1.75 2)))
-	//   ((_ to_fp 11 53) RTZ 7.0)))
+    //   ((_ to_fp 11 53) RTZ 7.0)))
-
+    
-	Z3_solver_push(ctx, s);
+    Z3_solver_push(ctx, s);
-	c1 = Z3_mk_fpa_fp(ctx,
+    c1 = Z3_mk_fpa_fp(ctx,
-					  Z3_mk_numeral(ctx, "0", Z3_mk_bv_sort(ctx, 1)),
+                      Z3_mk_numeral(ctx, "0", Z3_mk_bv_sort(ctx, 1)),
-					  Z3_mk_numeral(ctx, "1025", Z3_mk_bv_sort(ctx, 11)),
+                      Z3_mk_numeral(ctx, "1025", Z3_mk_bv_sort(ctx, 11)),
                       Z3_mk_numeral(ctx, "3377699720527872", Z3_mk_bv_sort(ctx, 52)));
-	c2 = Z3_mk_fpa_to_fp_bv(ctx,
+    c2 = Z3_mk_fpa_to_fp_bv(ctx,
-							Z3_mk_numeral(ctx, "4619567317775286272", Z3_mk_bv_sort(ctx, 64)),
+                            Z3_mk_numeral(ctx, "4619567317775286272", Z3_mk_bv_sort(ctx, 64)),
-							Z3_mk_fpa_sort(ctx, 11, 53));
+                            Z3_mk_fpa_sort(ctx, 11, 53));
     c3 = Z3_mk_fpa_to_fp_int_real(ctx,
                                   Z3_mk_fpa_rtz(ctx),
-								  Z3_mk_numeral(ctx, "2", Z3_mk_int_sort(ctx)), /* exponent */
+                                  Z3_mk_numeral(ctx, "2", Z3_mk_int_sort(ctx)), /* exponent */
                                   Z3_mk_numeral(ctx, "1.75", Z3_mk_real_sort(ctx)), /* significand */
                                   Z3_mk_fpa_sort(ctx, 11, 53));
     c4 = Z3_mk_fpa_to_fp_real(ctx,
-							  Z3_mk_fpa_rtz(ctx),
+                              Z3_mk_fpa_rtz(ctx),
-							  Z3_mk_numeral(ctx, "7.0", Z3_mk_real_sort(ctx)),
+                              Z3_mk_numeral(ctx, "7.0", Z3_mk_real_sort(ctx)),
-							  Z3_mk_fpa_sort(ctx, 11, 53));
+                              Z3_mk_fpa_sort(ctx, 11, 53));
-	args3[0] = Z3_mk_eq(ctx, c1, c2);
+    args3[0] = Z3_mk_eq(ctx, c1, c2);
-	args3[1] = Z3_mk_eq(ctx, c1, c3);
+    args3[1] = Z3_mk_eq(ctx, c1, c3);
-	args3[2] = Z3_mk_eq(ctx, c1, c4);
+    args3[2] = Z3_mk_eq(ctx, c1, c4);
-	c5 = Z3_mk_and(ctx, 3, args3);
+    c5 = Z3_mk_and(ctx, 3, args3);
-
+    
-	printf("c5: %s\n", Z3_ast_to_string(ctx, c5));
+    printf("c5: %s\n", Z3_ast_to_string(ctx, c5));
-	Z3_solver_assert(ctx, s, c5);
+    Z3_solver_assert(ctx, s, c5);
-	check(ctx, s, Z3_L_TRUE);
+    check(ctx, s, Z3_L_TRUE);
-	Z3_solver_pop(ctx, s, 1);
+    Z3_solver_pop(ctx, s, 1);
-
+    
     del_solver(ctx, s);
     Z3_del_context(ctx);
 }
 
+/**
+   \brief Demonstrates some basic features of model construction
+*/
+
+void mk_model_example() {
+    Z3_context ctx;
+    Z3_model m;
+    Z3_sort intSort;
+    Z3_symbol aSymbol, bSymbol, cSymbol;
+    Z3_func_decl aFuncDecl, bFuncDecl, cFuncDecl;
+    Z3_ast aApp, bApp, cApp;
+    Z3_sort int2intArraySort;
+    Z3_ast zeroNumeral, oneNumeral, twoNumeral, threeNumeral, fourNumeral;
+    Z3_sort arrayDomain[1];
+    Z3_func_decl cAsFuncDecl;
+    Z3_func_interp cAsFuncInterp;
+    Z3_ast_vector zeroArgs;
+    Z3_ast_vector oneArgs;
+    Z3_ast cFuncDeclAsArray;
+    Z3_string modelAsString;
+
+    printf("\nmk_model_example\n");
+    ctx = mk_context();
+    // Construct empty model
+    m = Z3_mk_model(ctx);
+    Z3_model_inc_ref(ctx, m);
+
+    // Create constants "a" and "b"
+    intSort = Z3_mk_int_sort(ctx);
+    aSymbol = Z3_mk_string_symbol(ctx, "a");
+    aFuncDecl = Z3_mk_func_decl(ctx, aSymbol,
+                                /*domain_size=*/0,
+                                /*domain=*/NULL,
+                                /*range=*/intSort);
+    aApp = Z3_mk_app(ctx, aFuncDecl,
+                     /*num_args=*/0,
+                     /*args=*/NULL);
+    bSymbol = Z3_mk_string_symbol(ctx, "b");
+    bFuncDecl = Z3_mk_func_decl(ctx, bSymbol,
+                                /*domain_size=*/0,
+                                /*domain=*/NULL,
+                                /*range=*/intSort);
+    bApp = Z3_mk_app(ctx, bFuncDecl,
+                     /*num_args=*/0,
+                     /*args=*/NULL);
+
+    // Create array "c" that maps int to int.
+    cSymbol = Z3_mk_string_symbol(ctx, "c");
+    int2intArraySort = Z3_mk_array_sort(ctx,
+                                        /*domain=*/intSort,
+                                        /*range=*/intSort);
+    cFuncDecl = Z3_mk_func_decl(ctx, cSymbol,
+                                /*domain_size=*/0,
+                                /*domain=*/NULL,
+                                /*range=*/int2intArraySort);
+    cApp = Z3_mk_app(ctx, cFuncDecl,
+                     /*num_args=*/0,
+                     /*args=*/NULL);
+
+    // Create numerals to be used in model
+    zeroNumeral = Z3_mk_int(ctx, 0, intSort);
+    oneNumeral = Z3_mk_int(ctx, 1, intSort);
+    twoNumeral = Z3_mk_int(ctx, 2, intSort);
+    threeNumeral = Z3_mk_int(ctx, 3, intSort);
+    fourNumeral = Z3_mk_int(ctx, 4, intSort);
+
+    // Add assignments to model
+    // a == 1
+    Z3_add_const_interp(ctx, m, aFuncDecl, oneNumeral);
+    // b == 2
+    Z3_add_const_interp(ctx, m, bFuncDecl, twoNumeral);
+
+    // Create a fresh function that represents
+    // reading from array.
+    arrayDomain[0] = intSort;
+    cAsFuncDecl = Z3_mk_fresh_func_decl(ctx,
+                                        /*prefix=*/"",
+                                        /*domain_size*/ 1,
+                                        /*domain=*/arrayDomain,
+                                        /*sort=*/intSort);
+    // Create function interpretation with default
+    // value of "0".
+    cAsFuncInterp =
+        Z3_add_func_interp(ctx, m, cAsFuncDecl,
+                           /*default_value=*/zeroNumeral);
+    Z3_func_interp_inc_ref(ctx, cAsFuncInterp);
+    // Add [0] = 3
+    zeroArgs = Z3_mk_ast_vector(ctx);
+    Z3_ast_vector_inc_ref(ctx, zeroArgs);
+    Z3_ast_vector_push(ctx, zeroArgs, zeroNumeral);
+    Z3_func_interp_add_entry(ctx, cAsFuncInterp, zeroArgs, threeNumeral);
+    // Add [1] = 4
+    oneArgs = Z3_mk_ast_vector(ctx);
+    Z3_ast_vector_inc_ref(ctx, oneArgs);
+    Z3_ast_vector_push(ctx, oneArgs, oneNumeral);
+    Z3_func_interp_add_entry(ctx, cAsFuncInterp, oneArgs, fourNumeral);
+
+    // Now use the `(_ as_array)` to associate
+    // the `cAsFuncInterp` with the `cFuncDecl`
+    // in the model
+    cFuncDeclAsArray = Z3_mk_as_array(ctx, cAsFuncDecl);
+    Z3_add_const_interp(ctx, m, cFuncDecl, cFuncDeclAsArray);
+
+    // Print the model
+    modelAsString = Z3_model_to_string(ctx, m);
+    printf("Model:\n%s\n", modelAsString);
+
+    // Check the interpretations we expect to be present
+    // are.
+    {
+        Z3_func_decl expectedInterpretations[3] = {aFuncDecl, bFuncDecl, cFuncDecl};
+        int index;
+        for (index = 0;
+             index < sizeof(expectedInterpretations) / sizeof(Z3_func_decl);
+             ++index) {
+            Z3_func_decl d = expectedInterpretations[index];
+            if (Z3_model_has_interp(ctx, m, d)) {
+                printf("Found interpretation for \"%s\"\n",
+                       Z3_ast_to_string(ctx, Z3_func_decl_to_ast(ctx, d)));
+            } else {
+                printf("Missing interpretation");
+                exit(1);
+            }
+        }
+    }
+
+    {
+        // Evaluate a + b under model
+        Z3_ast addArgs[] = {aApp, bApp};
+        Z3_ast aPlusB = Z3_mk_add(ctx,
+                                  /*num_args=*/2,
+                                  /*args=*/addArgs);
+        Z3_ast aPlusBEval = NULL;
+        Z3_bool aPlusBEvalSuccess =
+            Z3_model_eval(ctx, m, aPlusB,
+                          /*model_completion=*/Z3_FALSE, &aPlusBEval);
+        if (aPlusBEvalSuccess != Z3_TRUE) {
+            printf("Failed to evaluate model\n");
+            exit(1);
+        }
+
+        {
+            int aPlusBValue = 0;
+            Z3_bool getAPlusBValueSuccess =
+                Z3_get_numeral_int(ctx, aPlusBEval, &aPlusBValue);
+            if (getAPlusBValueSuccess != Z3_TRUE) {
+                printf("Failed to get integer value for a+b\n");
+                exit(1);
+            }
+            printf("Evaluated a + b = %d\n", aPlusBValue);
+            if (aPlusBValue != 3) {
+                printf("a+b did not evaluate to expected value\n");
+                exit(1);
+            }
+        }
+    }
+
+    {    
+        // Evaluate c[0] + c[1] + c[2] under model
+        Z3_ast c0 = Z3_mk_select(ctx, cApp, zeroNumeral);
+        Z3_ast c1 = Z3_mk_select(ctx, cApp, oneNumeral);
+        Z3_ast c2 = Z3_mk_select(ctx, cApp, twoNumeral);
+        Z3_ast arrayAddArgs[] = {c0, c1, c2};
+        Z3_ast arrayAdd = Z3_mk_add(ctx,
+                                    /*num_args=*/3,
+                                    /*args=*/arrayAddArgs);
+        Z3_ast arrayAddEval = NULL;
+        Z3_bool arrayAddEvalSuccess =
+            Z3_model_eval(ctx, m, arrayAdd,
+                          /*model_completion=*/Z3_FALSE, &arrayAddEval);
+        if (arrayAddEvalSuccess != Z3_TRUE) {
+            printf("Failed to evaluate model\n");
+            exit(1);
+        }
+        {
+            int arrayAddValue = 0;
+            Z3_bool getArrayAddValueSuccess =
+                Z3_get_numeral_int(ctx, arrayAddEval, &arrayAddValue);
+            if (getArrayAddValueSuccess != Z3_TRUE) {
+                printf("Failed to get integer value for c[0] + c[1] + c[2]\n");
+                exit(1);
+            }
+            printf("Evaluated c[0] + c[1] + c[2] = %d\n", arrayAddValue);
+            if (arrayAddValue != 7) {
+                printf("c[0] + c[1] + c[2] did not evaluate to expected value\n");
+                exit(1);
+            }
+        }
+    }
+
+    Z3_ast_vector_dec_ref(ctx, oneArgs);
+    Z3_ast_vector_dec_ref(ctx, zeroArgs);
+    Z3_func_interp_dec_ref(ctx, cAsFuncInterp);
+    Z3_model_dec_ref(ctx, m);
+    Z3_del_context(ctx);
+}
+
 /*@}*/
 /*@}*/
 
+
+
 int main() {
 #ifdef LOG_Z3_CALLS
     Z3_open_log("z3.log");
@@ -2886,5 +3085,6 @@ int main() {
     substitute_example();
     substitute_vars_example();
     fpa_example();
+    mk_model_example();
     return 0;
 }

scripts/mk_project.py

@@ -43,14 +43,14 @@ def init_project_def():
     add_lib('cmd_context', ['solver', 'rewriter', 'interp'])
     add_lib('extra_cmds', ['cmd_context', 'subpaving_tactic', 'arith_tactics'], 'cmd_context/extra_cmds')
     add_lib('smt2parser', ['cmd_context', 'parser_util'], 'parsers/smt2')
-    add_lib('proof_checker', ['rewriter'], 'ast/proof_checker')
+    add_lib('proofs', ['rewriter', 'util'], 'ast/proofs')
     add_lib('fpa', ['ast', 'util', 'rewriter', 'model'], 'ast/fpa')
     add_lib('pattern', ['normal_forms', 'smt2parser', 'rewriter'], 'ast/pattern')
     add_lib('bit_blaster', ['rewriter', 'rewriter'], 'ast/rewriter/bit_blaster')
     add_lib('smt_params', ['ast', 'rewriter', 'pattern', 'bit_blaster'], 'smt/params')
     add_lib('proto_model', ['model', 'rewriter', 'smt_params'], 'smt/proto_model')
     add_lib('smt', ['bit_blaster', 'macros', 'normal_forms', 'cmd_context', 'proto_model',
-                    'substitution', 'grobner', 'euclid', 'simplex', 'proof_checker', 'pattern', 'parser_util', 'fpa', 'lp'])
+                    'substitution', 'grobner', 'euclid', 'simplex', 'proofs', 'pattern', 'parser_util', 'fpa', 'lp'])
     add_lib('bv_tactics', ['tactic', 'bit_blaster', 'core_tactics'], 'tactic/bv')
     add_lib('fuzzing', ['ast'], 'test/fuzzing')
     add_lib('smt_tactic', ['smt'], 'smt/tactic')

src/CMakeLists.txt

@@ -67,7 +67,7 @@ add_subdirectory(interp)
 add_subdirectory(cmd_context)
 add_subdirectory(cmd_context/extra_cmds)
 add_subdirectory(parsers/smt2)
-add_subdirectory(ast/proof_checker)
+add_subdirectory(ast/proofs)
 add_subdirectory(ast/fpa)
 add_subdirectory(ast/macros)
 add_subdirectory(ast/pattern)

src/api/api_array.cpp

@@ -34,6 +34,19 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
 
+    Z3_sort Z3_API Z3_mk_array_sort_n(Z3_context c, unsigned n, Z3_sort const* domain, Z3_sort range) {
+        Z3_TRY;
+        LOG_Z3_mk_array_sort_n(c, n, domain, range);
+        RESET_ERROR_CODE();
+        vector<parameter> params;
+        for (unsigned i = 0; i < n; ++i) params.push_back(parameter(to_sort(domain[i])));
+        params.push_back(parameter(to_sort(range)));
+        sort * ty =  mk_c(c)->m().mk_sort(mk_c(c)->get_array_fid(), ARRAY_SORT, params.size(), params.c_ptr());
+        mk_c(c)->save_ast_trail(ty);
+        RETURN_Z3(of_sort(ty));
+        Z3_CATCH_RETURN(0);
+    }
+
     Z3_ast Z3_API Z3_mk_select(Z3_context c, Z3_ast a, Z3_ast i) {
         Z3_TRY;
         LOG_Z3_mk_select(c, a, i);
@@ -57,6 +70,35 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
 
+    Z3_ast Z3_API Z3_mk_select_n(Z3_context c, Z3_ast a, unsigned n, Z3_ast const* idxs) {
+        Z3_TRY;
+        LOG_Z3_mk_select_n(c, a, n, idxs);
+        RESET_ERROR_CODE();
+        ast_manager & m = mk_c(c)->m();
+        expr * _a        = to_expr(a);
+        // expr * _i        = to_expr(i);
+        sort * a_ty = m.get_sort(_a);
+        // sort * i_ty = m.get_sort(_i);
+        if (a_ty->get_family_id() != mk_c(c)->get_array_fid()) {
+            SET_ERROR_CODE(Z3_SORT_ERROR);
+            RETURN_Z3(0);
+        }
+        ptr_vector<sort> domain;
+        ptr_vector<expr> args;
+        args.push_back(_a);
+        domain.push_back(a_ty);
+        for (unsigned i = 0; i < n; ++i) {
+            args.push_back(to_expr(idxs[i]));
+            domain.push_back(m.get_sort(to_expr(idxs[i])));
+        }
+        func_decl * d   = m.mk_func_decl(mk_c(c)->get_array_fid(), OP_SELECT, 2, a_ty->get_parameters(), domain.size(), domain.c_ptr());
+        app * r        = m.mk_app(d, args.size(), args.c_ptr());
+        mk_c(c)->save_ast_trail(r);
+        check_sorts(c, r);
+        RETURN_Z3(of_ast(r));
+        Z3_CATCH_RETURN(0);
+    }
+
     Z3_ast Z3_API Z3_mk_store(Z3_context c, Z3_ast a, Z3_ast i, Z3_ast v) {
         Z3_TRY;
         LOG_Z3_mk_store(c, a, i, v);
@@ -82,6 +124,37 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
 
+    Z3_ast Z3_API Z3_mk_store_n(Z3_context c, Z3_ast a, unsigned n, Z3_ast const* idxs, Z3_ast v) {
+        Z3_TRY;
+        LOG_Z3_mk_store_n(c, a, n, idxs, v);
+        RESET_ERROR_CODE();
+        ast_manager & m = mk_c(c)->m();
+        expr * _a        = to_expr(a);
+        expr * _v        = to_expr(v);
+        sort * a_ty = m.get_sort(_a);
+        sort * v_ty = m.get_sort(_v);
+        if (a_ty->get_family_id() != mk_c(c)->get_array_fid()) {
+            SET_ERROR_CODE(Z3_SORT_ERROR);
+            RETURN_Z3(0);
+        }
+        ptr_vector<sort> domain;
+        ptr_vector<expr> args;
+        args.push_back(_a);
+        domain.push_back(a_ty);
+        for (unsigned i = 0; i < n; ++i) {
+            args.push_back(to_expr(idxs[i]));
+            domain.push_back(m.get_sort(to_expr(idxs[i])));
+        }
+        args.push_back(_v);
+        domain.push_back(v_ty);
+        func_decl * d   = m.mk_func_decl(mk_c(c)->get_array_fid(), OP_STORE, 2, a_ty->get_parameters(), domain.size(), domain.c_ptr());
+        app * r        = m.mk_app(d, args.size(), args.c_ptr());
+        mk_c(c)->save_ast_trail(r);
+        check_sorts(c, r);
+        RETURN_Z3(of_ast(r));
+        Z3_CATCH_RETURN(0);
+    }
+
     Z3_ast Z3_API Z3_mk_map(Z3_context c, Z3_func_decl f, unsigned n, Z3_ast const* args) {
         Z3_TRY;
         LOG_Z3_mk_map(c, f, n, args);
@@ -188,6 +261,18 @@ extern "C" {
     MK_BINARY(Z3_mk_set_subset, mk_c(c)->get_array_fid(), OP_SET_SUBSET, SKIP);
     MK_BINARY(Z3_mk_array_ext, mk_c(c)->get_array_fid(), OP_ARRAY_EXT, SKIP);
 
+    Z3_ast Z3_API Z3_mk_as_array(Z3_context c, Z3_func_decl f) {
+        Z3_TRY;
+        LOG_Z3_mk_as_array(c, f);
+        RESET_ERROR_CODE();
+        ast_manager & m = mk_c(c)->m();
+        array_util a(m);
+        app * r = a.mk_as_array(to_func_decl(f));
+        mk_c(c)->save_ast_trail(r);
+        return of_ast(r);
+        Z3_CATCH_RETURN(0);
+    }
+
     Z3_ast Z3_mk_set_member(Z3_context c, Z3_ast elem, Z3_ast set) {
         return Z3_mk_select(c, set, elem);
     }
@@ -222,7 +307,8 @@ extern "C" {
         CHECK_VALID_AST(t, 0);
         if (to_sort(t)->get_family_id() == mk_c(c)->get_array_fid() &&
             to_sort(t)->get_decl_kind() == ARRAY_SORT) {
-            Z3_sort r = reinterpret_cast<Z3_sort>(to_sort(t)->get_parameter(1).get_ast());
+            unsigned n = to_sort(t)->get_num_parameters();
+            Z3_sort r = reinterpret_cast<Z3_sort>(to_sort(t)->get_parameter(n-1).get_ast());
             RETURN_Z3(r);
         }
         SET_ERROR_CODE(Z3_INVALID_ARG);

src/api/api_interp.cpp

@@ -249,7 +249,7 @@ extern "C" {
         params_ref _p;
         _p.set_bool("proof", true); // this is currently useless
 
-        scoped_proof_mode spm(mk_c(c)->m(), PGM_FINE);
+        scoped_proof_mode spm(mk_c(c)->m(), PGM_ENABLED);
         scoped_ptr<solver_factory> sf = mk_smt_solver_factory();
         scoped_ptr<solver> m_solver((*sf)(mk_c(c)->m(), _p, true, true, true, ::symbol::null));
         m_solver.get()->updt_params(_p); // why do we have to do this?

src/api/api_model.cpp

@@ -255,8 +255,13 @@ extern "C" {
         LOG_Z3_add_const_interp(c, m, f, a);
         RESET_ERROR_CODE();
         func_decl* d = to_func_decl(f);
-        model* mdl = to_model_ref(m);
+        if (d->get_arity() != 0) {
-        mdl->register_decl(d, to_expr(a));
+            SET_ERROR_CODE(Z3_INVALID_ARG);
+        }
+        else {
+            model* mdl = to_model_ref(m);
+            mdl->register_decl(d, to_expr(a));
+        }
         Z3_CATCH;
     }
 

src/api/c++/z3++.h

@@ -250,6 +250,8 @@ namespace z3 {
            Example: Given a context \c c, <tt>c.array_sort(c.int_sort(), c.bool_sort())</tt> is an array sort from integer to Boolean.
         */
         sort array_sort(sort d, sort r);
+        sort array_sort(sort_vector const& d, sort r);
+
         /**
            \brief Return an enumeration sort: enum_names[0], ..., enum_names[n-1].
            \c cs and \c ts are output parameters. The method stores in \c cs the constants corresponding to the enumerated elements,
@@ -2327,6 +2329,11 @@ namespace z3 {
     inline sort context::re_sort(sort& s) { Z3_sort r = Z3_mk_re_sort(m_ctx, s); check_error(); return sort(*this, r); }
 
     inline sort context::array_sort(sort d, sort r) { Z3_sort s = Z3_mk_array_sort(m_ctx, d, r); check_error(); return sort(*this, s); }
+    inline sort context::array_sort(sort_vector const& d, sort r) {
+        array<Z3_sort> dom(d);
+        Z3_sort s = Z3_mk_array_sort_n(m_ctx, dom.size(), dom.ptr(), r); check_error(); return sort(*this, s); 
+    }
+
     inline sort context::enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts) {
         array<Z3_symbol> _enum_names(n);
         for (unsigned i = 0; i < n; i++) { _enum_names[i] = Z3_mk_string_symbol(*this, enum_names[i]); }
@@ -2573,11 +2580,32 @@ namespace z3 {
         a.check_error();
         return expr(a.ctx(), r);
     }
+    inline expr select(expr const & a, expr_vector const & i) {
+        check_context(a, i);
+        array<Z3_ast> idxs(i);
+        Z3_ast r = Z3_mk_select_n(a.ctx(), a, idxs.size(), idxs.ptr());
+        a.check_error();
+        return expr(a.ctx(), r);
+    }
+
     inline expr store(expr const & a, int i, expr const & v) { return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), v); }
     inline expr store(expr const & a, expr i, int v) { return store(a, i, a.ctx().num_val(v, a.get_sort().array_range())); }
     inline expr store(expr const & a, int i, int v) {
         return store(a, a.ctx().num_val(i, a.get_sort().array_domain()), a.ctx().num_val(v, a.get_sort().array_range()));
     }
+    inline expr store(expr const & a, expr_vector const & i, expr const & v) {
+        check_context(a, i); check_context(a, v);
+        array<Z3_ast> idxs(i);
+        Z3_ast r = Z3_mk_store_n(a.ctx(), a, idxs.size(), idxs.ptr(), v);
+        a.check_error();
+        return expr(a.ctx(), r);
+    }
+
+    inline expr as_array(func_decl & f) { 
+        Z3_ast r = Z3_mk_as_array(f.ctx(), f); 
+        f.check_error();  
+        return expr(f.ctx(), r); 
+    }
 
 #define MK_EXPR1(_fn, _arg)                     \
     Z3_ast r = _fn(_arg.ctx(), _arg);           \

src/api/dotnet/ArraySort.cs

@@ -63,6 +63,13 @@ namespace Microsoft.Z3
             Contract.Requires(domain != null);
             Contract.Requires(range != null);
         }
+        internal ArraySort(Context ctx, Sort[] domain, Sort range)
+            : base(ctx, Native.Z3_mk_array_sort_n(ctx.nCtx, (uint)domain.Length, AST.ArrayToNative(domain), range.NativeObject))
+        {
+            Contract.Requires(ctx != null);
+            Contract.Requires(domain != null);
+            Contract.Requires(range != null);
+        }
         #endregion
     };
 

src/api/dotnet/Context.cs

@@ -274,6 +274,20 @@ namespace Microsoft.Z3
             return new ArraySort(this, domain, range);
         }
 
+        /// <summary>
+        /// Create a new n-ary array sort.
+        /// </summary>
+        public ArraySort MkArraySort(Sort[] domain, Sort range)
+        {
+            Contract.Requires(domain != null);
+            Contract.Requires(range != null);
+            Contract.Ensures(Contract.Result<ArraySort>() != null);
+
+            CheckContextMatch<Sort>(domain);
+            CheckContextMatch(range);
+            return new ArraySort(this, domain, range);
+        }
+
         /// <summary>
         /// Create a new tuple sort.
         /// </summary>
@@ -2113,6 +2127,7 @@ namespace Microsoft.Z3
             return (ArrayExpr)MkConst(MkSymbol(name), MkArraySort(domain, range));
         }
 
+
         /// <summary>
         /// Array read.
         /// </summary>
@@ -2123,8 +2138,8 @@ namespace Microsoft.Z3
         /// The node <c>a</c> must have an array sort <c>[domain -> range]</c>,
         /// and <c>i</c> must have the sort <c>domain</c>.
         /// The sort of the result is <c>range</c>.
-        /// <seealso cref="MkArraySort"/>
+        /// <seealso cref="MkArraySort(Sort, Sort)"/>
-        /// <seealso cref="MkStore"/>
+        /// <seealso cref="MkStore(ArrayExpr, Expr, Expr)"/>
         /// </remarks>
         public Expr MkSelect(ArrayExpr a, Expr i)
         {
@@ -2137,6 +2152,30 @@ namespace Microsoft.Z3
             return Expr.Create(this, Native.Z3_mk_select(nCtx, a.NativeObject, i.NativeObject));
         }
 
+        /// <summary>
+        /// Array read.
+        /// </summary>
+        /// <remarks>
+        /// The argument <c>a</c> is the array and <c>args</c> are the indices
+        /// of the array that gets read.
+        ///
+        /// The node <c>a</c> must have an array sort <c>[domain1,..,domaink -> range]</c>,
+        /// and <c>args</c> must have the sort <c>domain1,..,domaink</c>.
+        /// The sort of the result is <c>range</c>.
+        /// <seealso cref="MkArraySort(Sort, Sort)"/>
+        /// <seealso cref="MkStore(ArrayExpr, Expr, Expr)"/>
+        /// </remarks>
+        public Expr MkSelect(ArrayExpr a, params Expr[] args)
+        {
+            Contract.Requires(a != null);
+            Contract.Requires(args != null && Contract.ForAll(args, n => n != null));
+            Contract.Ensures(Contract.Result<Expr>() != null);
+
+            CheckContextMatch(a);
+            CheckContextMatch<Expr>(args);
+            return Expr.Create(this, Native.Z3_mk_select_n(nCtx, a.NativeObject, AST.ArrayLength(args), AST.ArrayToNative(args)));
+        }
+
         /// <summary>
         /// Array update.
         /// </summary>
@@ -2151,8 +2190,9 @@ namespace Microsoft.Z3
         /// on all indices except for <c>i</c>, where it maps to <c>v</c>
         /// (and the <c>select</c> of <c>a</c> with
         /// respect to <c>i</c> may be a different value).
-        /// <seealso cref="MkArraySort"/>
+        /// <seealso cref="MkArraySort(Sort, Sort)"/>
-        /// <seealso cref="MkSelect"/>
+        /// <seealso cref="MkSelect(ArrayExpr, Expr)"/>
+        /// <seealso cref="MkSelect(ArrayExpr, Expr[])"/>
         /// </remarks>
         public ArrayExpr MkStore(ArrayExpr a, Expr i, Expr v)
         {
@@ -2167,14 +2207,45 @@ namespace Microsoft.Z3
             return new ArrayExpr(this, Native.Z3_mk_store(nCtx, a.NativeObject, i.NativeObject, v.NativeObject));
         }
 
+        /// <summary>
+        /// Array update.
+        /// </summary>
+        /// <remarks>
+        /// The node <c>a</c> must have an array sort <c>[domain1,..,domaink -> range]</c>,
+        /// <c>args</c> must have sort <c>domain1,..,domaink</c>,
+        /// <c>v</c> must have sort range. The sort of the result is <c>[domain -> range]</c>.
+        /// The semantics of this function is given by the theory of arrays described in the SMT-LIB
+        /// standard. See http://smtlib.org for more details.
+        /// The result of this function is an array that is equal to <c>a</c>
+        /// (with respect to <c>select</c>)
+        /// on all indices except for <c>args</c>, where it maps to <c>v</c>
+        /// (and the <c>select</c> of <c>a</c> with
+        /// respect to <c>args</c> may be a different value).
+        /// <seealso cref="MkArraySort(Sort, Sort)"/>
+        /// <seealso cref="MkSelect(ArrayExpr, Expr)"/>
+        /// <seealso cref="MkSelect(ArrayExpr, Expr[])"/>
+        /// </remarks>
+        public ArrayExpr MkStore(ArrayExpr a, Expr[] args, Expr v)
+        {
+            Contract.Requires(a != null);
+            Contract.Requires(args != null);
+            Contract.Requires(v != null);
+            Contract.Ensures(Contract.Result<ArrayExpr>() != null);
+
+            CheckContextMatch<Expr>(args);
+            CheckContextMatch(a);
+            CheckContextMatch(v);
+            return new ArrayExpr(this, Native.Z3_mk_store_n(nCtx, a.NativeObject, AST.ArrayLength(args), AST.ArrayToNative(args), v.NativeObject));
+        }
+
         /// <summary>
         /// Create a constant array.
         /// </summary>
         /// <remarks>
         /// The resulting term is an array, such that a <c>select</c>on an arbitrary index
         /// produces the value <c>v</c>.
-        /// <seealso cref="MkArraySort"/>
+        /// <seealso cref="MkArraySort(Sort, Sort)"/>
-        /// <seealso cref="MkSelect"/>
+        /// <seealso cref="MkSelect(ArrayExpr, Expr)"/>
         /// </remarks>
         public ArrayExpr MkConstArray(Sort domain, Expr v)
         {
@@ -2194,9 +2265,9 @@ namespace Microsoft.Z3
         /// Eeach element of <c>args</c> must be of an array sort <c>[domain_i -> range_i]</c>.
         /// The function declaration <c>f</c> must have type <c> range_1 .. range_n -> range</c>.
         /// <c>v</c> must have sort range. The sort of the result is <c>[domain_i -> range]</c>.
-        /// <seealso cref="MkArraySort"/>
+        /// <seealso cref="MkArraySort(Sort, Sort)"/>
-        /// <seealso cref="MkSelect"/>
+        /// <seealso cref="MkSelect(ArrayExpr, Expr)"/>
-        /// <seealso cref="MkStore"/>
+        /// <seealso cref="MkStore(ArrayExpr, Expr, Expr)"/>
         /// </remarks>
         public ArrayExpr MkMap(FuncDecl f, params ArrayExpr[] args)
         {

src/api/java/ArraySort.java

@@ -56,4 +56,10 @@ public class ArraySort extends Sort
         super(ctx, Native.mkArraySort(ctx.nCtx(), domain.getNativeObject(),
                 range.getNativeObject()));
     }
+
+    ArraySort(Context ctx, Sort[] domains, Sort range)
+    {
+        super(ctx, Native.mkArraySortN(ctx.nCtx(), domains.length, AST.arrayToNative(domains),
+                range.getNativeObject()));
+    }
 };

src/api/java/Context.java

@@ -224,6 +224,17 @@ public class Context implements AutoCloseable {
         return new ArraySort(this, domain, range);
     }
 
+
+    /**
+     * Create a new array sort.
+     **/
+    public ArraySort mkArraySort(Sort[] domains, Sort range)
+    {
+        checkContextMatch(domains);
+        checkContextMatch(range);
+        return new ArraySort(this, domains, range);
+    }
+
     /**
      * Create a new string sort
      **/
@@ -414,7 +425,7 @@ public class Context implements AutoCloseable {
      * that is passed in as argument is updated with value v,
      * the remaining fields of t are unchanged.
      **/
-    public Expr MkUpdateField(FuncDecl field, Expr t, Expr v) 
+    public Expr mkUpdateField(FuncDecl field, Expr t, Expr v) 
         throws Z3Exception
     {
         return Expr.create (this, 
@@ -706,7 +717,7 @@ public class Context implements AutoCloseable {
     }
 
     /**
-     * Mk an expression representing {@code not(a)}.
+     * Create an expression representing {@code not(a)}.
      **/
     public BoolExpr mkNot(BoolExpr a)
     {
@@ -1679,6 +1690,28 @@ public class Context implements AutoCloseable {
                         i.getNativeObject()));
     }
 
+    /**
+     * Array read.
+     * Remarks:  The argument {@code a} is the array and
+     * {@code args} are the indices of the array that gets read.
+     * 
+     * The node {@code a} must have an array sort
+     * {@code [domains -> range]}, and {@code args} must have the sorts
+     * {@code domains}. The sort of the result is {@code range}.
+     * 
+     * @see #mkArraySort
+     * @see #mkStore
+
+     **/
+    public Expr mkSelect(ArrayExpr a, Expr[] args)
+    {
+        checkContextMatch(a);
+        checkContextMatch(args);
+        return Expr.create(
+                this,
+                Native.mkSelectN(nCtx(), a.getNativeObject(), args.length, AST.arrayToNative(args)));
+    }
+
     /**
      * Array update.
      * Remarks:  The node {@code a} must have an array sort
@@ -1704,6 +1737,31 @@ public class Context implements AutoCloseable {
                 i.getNativeObject(), v.getNativeObject()));
     }
 
+    /**
+     * Array update.
+     * Remarks:  The node {@code a} must have an array sort
+     * {@code [domains -> range]}, {@code i} must have sort
+     * {@code domain}, {@code v} must have sort range. The sort of the
+     * result is {@code [domains -> range]}. The semantics of this function
+     * is given by the theory of arrays described in the SMT-LIB standard. See
+     * http://smtlib.org for more details. The result of this function is an
+     * array that is equal to {@code a} (with respect to
+     * {@code select}) on all indices except for {@code args}, where it
+     * maps to {@code v} (and the {@code select} of {@code a}
+     * with respect to {@code args} may be a different value). 
+     * @see #mkArraySort
+     * @see #mkSelect
+
+     **/
+    public ArrayExpr mkStore(ArrayExpr a, Expr[] args, Expr v)
+    {
+        checkContextMatch(a);
+        checkContextMatch(args);
+        checkContextMatch(v);
+        return new ArrayExpr(this, Native.mkStoreN(nCtx(), a.getNativeObject(),
+                             args.length, AST.arrayToNative(args), v.getNativeObject()));
+    }
+
     /**
      * Create a constant array.
      * Remarks:  The resulting term is an array, such
@@ -2104,7 +2162,7 @@ public class Context implements AutoCloseable {
     /**
      * Create a range expression.
      */
-    public ReExpr MkRange(SeqExpr lo, SeqExpr hi) 
+    public ReExpr mkRange(SeqExpr lo, SeqExpr hi) 
     {
         checkContextMatch(lo, hi);
         return (ReExpr) Expr.create(this, Native.mkReRange(nCtx(), lo.getNativeObject(), hi.getNativeObject()));

src/api/z3_api.h

@@ -1881,6 +1881,17 @@ extern "C" {
     */
     Z3_sort Z3_API Z3_mk_array_sort(Z3_context c, Z3_sort domain, Z3_sort range);
 
+    /**
+       \brief Create an array type with N arguments
+
+       \sa Z3_mk_select_n
+       \sa Z3_mk_store_n
+
+       def_API('Z3_mk_array_sort_n', SORT, (_in(CONTEXT), _in(UINT), _in_array(1, SORT), _in(SORT)))
+    */
+    Z3_sort Z3_API Z3_mk_array_sort_n(Z3_context c, unsigned n, Z3_sort const * domain, Z3_sort range);
+
+
     /**
        \brief Create a tuple type.
 
@@ -2973,6 +2984,15 @@ extern "C" {
     */
     Z3_ast Z3_API Z3_mk_select(Z3_context c, Z3_ast a, Z3_ast i);
 
+    /**
+       \brief n-ary Array read.
+       The argument \c a is the array and \c idxs are the indices of the array that gets read.
+
+       def_API('Z3_mk_select_n', AST, (_in(CONTEXT), _in(AST), _in(UINT), _in_array(2, AST)))
+
+    */
+    Z3_ast Z3_API Z3_mk_select_n(Z3_context c, Z3_ast a, unsigned n, Z3_ast const* idxs);
+
     /**
        \brief Array update.
 
@@ -2991,6 +3011,14 @@ extern "C" {
     */
     Z3_ast Z3_API Z3_mk_store(Z3_context c, Z3_ast a, Z3_ast i, Z3_ast v);
 
+    /**
+       \brief n-ary Array update.
+
+       def_API('Z3_mk_store_n', AST, (_in(CONTEXT), _in(AST), _in(UINT), _in_array(2, AST), _in(AST)))
+
+    */
+    Z3_ast Z3_API Z3_mk_store_n(Z3_context c, Z3_ast a, unsigned n, Z3_ast const* idxs, Z3_ast v);
+
     /**
         \brief Create the constant array.
 
@@ -3031,6 +3059,15 @@ extern "C" {
         def_API('Z3_mk_array_default', AST, (_in(CONTEXT), _in(AST)))
     */
     Z3_ast Z3_API Z3_mk_array_default(Z3_context c, Z3_ast array);
+
+    /**
+       \brief Create array with the same interpretation as a function.
+       The array satisfies the property (f x) = (select (_ as-array f) x) 
+       for every argument x.
+
+       def_API('Z3_mk_as_array', AST, (_in(CONTEXT), _in(FUNC_DECL)))
+     */
+    Z3_ast Z3_API Z3_mk_as_array(Z3_context c, Z3_func_decl f);
     /*@}*/
 
     /** @name Sets */
@@ -3854,6 +3891,7 @@ extern "C" {
 
     /**
        \brief Return the domain of the given array sort.
+       In the case of a multi-dimensional array, this function returns the sort of the first dimension.
 
        \pre Z3_get_sort_kind(c, t) == Z3_ARRAY_SORT
 

src/ast/CMakeLists.txt

@@ -10,6 +10,7 @@ z3_add_component(ast
     ast_printer.cpp
     ast_smt2_pp.cpp
     ast_smt_pp.cpp
+    ast_pp_dot.cpp
     ast_translation.cpp
     ast_util.cpp
     bv_decl_plugin.cpp

src/ast/array_decl_plugin.cpp

@@ -242,7 +242,9 @@ func_decl* array_decl_plugin::mk_select(unsigned arity, sort * const * domain) {
     parameter const* parameters = s->get_parameters();
  
     if (num_parameters != arity) {
-        m_manager->raise_exception("select requires as many arguments as the size of the domain");
+        std::stringstream strm;
+        strm << "select requires " << num_parameters << " arguments, but was provided with " << arity << " arguments";
+        m_manager->raise_exception(strm.str().c_str());
         return 0;
     }
     ptr_buffer<sort> new_domain; // we need this because of coercions.
@@ -314,7 +316,7 @@ func_decl * array_decl_plugin::mk_array_ext(unsigned arity, sort * const * domai
         return 0;
     }
     sort * r = to_sort(s->get_parameter(i).get_ast());
-    parameter param(s);
+    parameter param(i);
     return m_manager->mk_func_decl(m_array_ext_sym, arity, domain, r, func_decl_info(m_family_id, OP_ARRAY_EXT, 1, &param));
 }
 
@@ -592,3 +594,9 @@ sort * array_util::mk_array_sort(unsigned arity, sort* const* domain, sort* rang
     params.push_back(parameter(range));
     return m_manager.mk_sort(m_fid, ARRAY_SORT, params.size(), params.c_ptr());
 }
+
+func_decl* array_util::mk_array_ext(sort *domain, unsigned i) {    
+    sort * domains[2] = { domain, domain };
+    parameter p(i);
+    return m_manager.mk_func_decl(m_fid, OP_ARRAY_EXT, 1, &p, 2, domains);
+}

src/ast/array_decl_plugin.h

@@ -143,6 +143,7 @@ public:
     bool is_const(expr* n) const { return is_app_of(n, m_fid, OP_CONST_ARRAY); }
     bool is_map(expr* n) const { return is_app_of(n, m_fid, OP_ARRAY_MAP); }
     bool is_as_array(expr * n) const { return is_app_of(n, m_fid, OP_AS_ARRAY); }
+    bool is_as_array(expr * n, func_decl*& f) const { return is_as_array(n) && (f = get_as_array_func_decl(n), true); }
     bool is_select(func_decl* f) const { return is_decl_of(f, m_fid, OP_SELECT); }
     bool is_store(func_decl* f) const { return is_decl_of(f, m_fid, OP_STORE); }
     bool is_const(func_decl* f) const { return is_decl_of(f, m_fid, OP_CONST_ARRAY); }
@@ -182,13 +183,15 @@ public:
         return mk_const_array(s, m_manager.mk_true());
     }
 
+    func_decl * mk_array_ext(sort* domain, unsigned i);
+
     sort * mk_array_sort(sort* dom, sort* range) { return mk_array_sort(1, &dom, range); }
 
     sort * mk_array_sort(unsigned arity, sort* const* domain, sort* range);
 
-    app * mk_as_array(sort * s, func_decl * f) {
+    app * mk_as_array(func_decl * f) {
         parameter param(f);
-        return m_manager.mk_app(m_fid, OP_AS_ARRAY, 1, &param, 0, 0, s);
+        return m_manager.mk_app(m_fid, OP_AS_ARRAY, 1, &param, 0, 0, 0);
     }
 };
 

src/ast/ast.cpp

@@ -805,7 +805,6 @@ func_decl * basic_decl_plugin::mk_proof_decl(char const* name, basic_op_kind k,
 }
 
 func_decl * basic_decl_plugin::mk_proof_decl(basic_op_kind k, unsigned num_parents) {
-    SASSERT(k == PR_UNDEF || m_manager->proofs_enabled());
     switch (static_cast<basic_op_kind>(k)) {
         //
         // A description of the semantics of the proof
@@ -2626,7 +2625,7 @@ bool ast_manager::is_fully_interp(sort * s) const {
 // -----------------------------------
 
 proof * ast_manager::mk_proof(family_id fid, decl_kind k, unsigned num_args, expr * const * args) {
-    if (m_proof_mode == PGM_DISABLED)
+    if (proofs_disabled())
         return m_undef_proof;
     return mk_app(fid, k, num_args, args);
 }
@@ -2662,8 +2661,7 @@ proof * ast_manager::mk_goal(expr * f) {
 }
 
 proof * ast_manager::mk_modus_ponens(proof * p1, proof * p2) {
-    if (m_proof_mode == PGM_DISABLED)
+    if (!p1 || !p2) return nullptr;
-        return m_undef_proof;
     SASSERT(has_fact(p1));
     SASSERT(has_fact(p2));
     CTRACE("mk_modus_ponens", !(is_implies(get_fact(p2)) || is_iff(get_fact(p2)) || is_oeq(get_fact(p2))),
@@ -2684,14 +2682,10 @@ proof * ast_manager::mk_modus_ponens(proof * p1, proof * p2) {
 }
 
 proof * ast_manager::mk_reflexivity(expr * e) {
-    if (m_proof_mode == PGM_DISABLED)
-        return m_undef_proof;
     return mk_app(m_basic_family_id, PR_REFLEXIVITY, mk_eq(e, e));
 }
 
 proof * ast_manager::mk_oeq_reflexivity(expr * e) {
-    if (m_proof_mode == PGM_DISABLED)
-        return m_undef_proof;
     return mk_app(m_basic_family_id, PR_REFLEXIVITY, mk_oeq(e, e));
 }
 
@@ -2705,8 +2699,7 @@ proof * ast_manager::mk_commutativity(app * f) {
    \brief Given a proof of p, return a proof of (p <=> true)
 */
 proof * ast_manager::mk_iff_true(proof * pr) {
-    if (m_proof_mode == PGM_DISABLED)
+    if (!pr) return pr;
-        return m_undef_proof;
     SASSERT(has_fact(pr));
     SASSERT(is_bool(get_fact(pr)));
     return mk_app(m_basic_family_id, PR_IFF_TRUE, pr, mk_iff(get_fact(pr), mk_true()));
@@ -2716,8 +2709,7 @@ proof * ast_manager::mk_iff_true(proof * pr) {
    \brief Given a proof of (not p), return a proof of (p <=> false)
 */
 proof * ast_manager::mk_iff_false(proof * pr) {
-    if (m_proof_mode == PGM_DISABLED)
+    if (!pr) return pr;
-        return m_undef_proof;
     SASSERT(has_fact(pr));
     SASSERT(is_not(get_fact(pr)));
     expr * p = to_app(get_fact(pr))->get_arg(0);
@@ -2725,10 +2717,7 @@ proof * ast_manager::mk_iff_false(proof * pr) {
 }
 
 proof * ast_manager::mk_symmetry(proof * p) {
-    if (m_proof_mode == PGM_DISABLED)
+    if (!p) return p;
-        return m_undef_proof;
-    if (!p)
-        return p;
     if (is_reflexivity(p))
         return p;
     if (is_symmetry(p))
@@ -2741,8 +2730,6 @@ proof * ast_manager::mk_symmetry(proof * p) {
 }
 
 proof * ast_manager::mk_transitivity(proof * p1, proof * p2) {
-    if (m_proof_mode == PGM_DISABLED)
-        return m_undef_proof;
     if (!p1)
         return p2;
     if (!p2)
@@ -2787,8 +2774,6 @@ proof * ast_manager::mk_transitivity(proof * p1, proof * p2, proof * p3, proof *
 }
 
 proof * ast_manager::mk_transitivity(unsigned num_proofs, proof * const * proofs) {
-    if (m_proof_mode == PGM_DISABLED)
-        return m_undef_proof;
     SASSERT(num_proofs > 0);
     proof * r = proofs[0];
     for (unsigned i = 1; i < num_proofs; i++)
@@ -2797,11 +2782,8 @@ proof * ast_manager::mk_transitivity(unsigned num_proofs, proof * const * proofs
 }
 
 proof * ast_manager::mk_transitivity(unsigned num_proofs, proof * const * proofs, expr * n1, expr * n2) {
-    if (m_proof_mode == PGM_DISABLED)
+    if (num_proofs == 0) 
-        return m_undef_proof;
+        return nullptr;
-    if (fine_grain_proofs())
-        return mk_transitivity(num_proofs, proofs);
-    SASSERT(num_proofs > 0);
     if (num_proofs == 1)
         return proofs[0];
     DEBUG_CODE({
@@ -2817,8 +2799,6 @@ proof * ast_manager::mk_transitivity(unsigned num_proofs, proof * const * proofs
 }
 
 proof * ast_manager::mk_monotonicity(func_decl * R, app * f1, app * f2, unsigned num_proofs, proof * const * proofs) {
-    if (m_proof_mode == PGM_DISABLED)
-        return m_undef_proof;
     SASSERT(f1->get_num_args() == f2->get_num_args());
     SASSERT(f1->get_decl() == f2->get_decl());
     ptr_buffer<expr> args;
@@ -2828,8 +2808,6 @@ proof * ast_manager::mk_monotonicity(func_decl * R, app * f1, app * f2, unsigned
 }
 
 proof * ast_manager::mk_congruence(app * f1, app * f2, unsigned num_proofs, proof * const * proofs) {
-    if (m_proof_mode == PGM_DISABLED)
-        return m_undef_proof;
     SASSERT(get_sort(f1) == get_sort(f2));
     sort * s    = get_sort(f1);
     sort * d[2] = { s, s };
@@ -2837,8 +2815,6 @@ proof * ast_manager::mk_congruence(app * f1, app * f2, unsigned num_proofs, proo
 }
 
 proof * ast_manager::mk_oeq_congruence(app * f1, app * f2, unsigned num_proofs, proof * const * proofs) {
-    if (m_proof_mode == PGM_DISABLED)
-        return m_undef_proof;
     SASSERT(get_sort(f1) == get_sort(f2));
     sort * s    = get_sort(f1);
     sort * d[2] = { s, s };
@@ -2846,11 +2822,7 @@ proof * ast_manager::mk_oeq_congruence(app * f1, app * f2, unsigned num_proofs,
 }
 
 proof * ast_manager::mk_quant_intro(quantifier * q1, quantifier * q2, proof * p) {
-    if (m_proof_mode == PGM_DISABLED)
+    if (!p) return nullptr;
-        return m_undef_proof;
-    if (!p) {
-        return 0;
-    }
     SASSERT(q1->get_num_decls() == q2->get_num_decls());
     SASSERT(has_fact(p));
     SASSERT(is_iff(get_fact(p)));
@@ -2858,8 +2830,7 @@ proof * ast_manager::mk_quant_intro(quantifier * q1, quantifier * q2, proof * p)
 }
 
 proof * ast_manager::mk_oeq_quant_intro(quantifier * q1, quantifier * q2, proof * p) {
-    if (m_proof_mode == PGM_DISABLED)
+    if (!p) return nullptr;
-        return m_undef_proof;
     SASSERT(q1->get_num_decls() == q2->get_num_decls());
     SASSERT(has_fact(p));
     SASSERT(is_oeq(get_fact(p)));
@@ -2867,25 +2838,26 @@ proof * ast_manager::mk_oeq_quant_intro(quantifier * q1, quantifier * q2, proof
 }
 
 proof * ast_manager::mk_distributivity(expr * s, expr * r) {
-    if (m_proof_mode == PGM_DISABLED)
-        return m_undef_proof;
     return mk_app(m_basic_family_id, PR_DISTRIBUTIVITY, mk_eq(s, r));
 }
 
 proof * ast_manager::mk_rewrite(expr * s, expr * t) {
-    if (m_proof_mode == PGM_DISABLED)
+    SASSERT(proofs_enabled());
+    if (proofs_disabled())
         return m_undef_proof;
     return mk_app(m_basic_family_id, PR_REWRITE, mk_eq(s, t));
 }
 
 proof * ast_manager::mk_oeq_rewrite(expr * s, expr * t) {
-    if (m_proof_mode == PGM_DISABLED)
+    SASSERT(proofs_enabled());
+    if (proofs_disabled())
         return m_undef_proof;
     return mk_app(m_basic_family_id, PR_REWRITE, mk_oeq(s, t));
 }
 
 proof * ast_manager::mk_rewrite_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) {
-    if (m_proof_mode == PGM_DISABLED)
+    SASSERT(proofs_enabled());
+    if (proofs_disabled())
         return m_undef_proof;
     ptr_buffer<expr> args;
     args.append(num_proofs, (expr**) proofs);
@@ -2894,37 +2866,43 @@ proof * ast_manager::mk_rewrite_star(expr * s, expr * t, unsigned num_proofs, pr
 }
 
 proof * ast_manager::mk_pull_quant(expr * e, quantifier * q) {
-    if (m_proof_mode == PGM_DISABLED)
+    SASSERT(proofs_enabled());
+    if (proofs_disabled())
         return m_undef_proof;
     return mk_app(m_basic_family_id, PR_PULL_QUANT, mk_iff(e, q));
 }
 
 proof * ast_manager::mk_pull_quant_star(expr * e, quantifier * q) {
-    if (m_proof_mode == PGM_DISABLED)
+    SASSERT(proofs_enabled());
+    if (proofs_disabled())
         return m_undef_proof;
     return mk_app(m_basic_family_id, PR_PULL_QUANT_STAR, mk_iff(e, q));
 }
 
 proof * ast_manager::mk_push_quant(quantifier * q, expr * e) {
-    if (m_proof_mode == PGM_DISABLED)
+    SASSERT(proofs_enabled());
+    if (proofs_disabled())
         return m_undef_proof;
     return mk_app(m_basic_family_id, PR_PUSH_QUANT, mk_iff(q, e));
 }
 
 proof * ast_manager::mk_elim_unused_vars(quantifier * q, expr * e) {
-    if (m_proof_mode == PGM_DISABLED)
+    SASSERT(proofs_enabled());
+    if (proofs_disabled())
         return m_undef_proof;
     return mk_app(m_basic_family_id, PR_ELIM_UNUSED_VARS, mk_iff(q, e));
 }
 
 proof * ast_manager::mk_der(quantifier * q, expr * e) {
-    if (m_proof_mode == PGM_DISABLED)
+    SASSERT(proofs_enabled());
+    if (proofs_disabled())
         return m_undef_proof;
     return mk_app(m_basic_family_id, PR_DER, mk_iff(q, e));
 }
 
 proof * ast_manager::mk_quant_inst(expr * not_q_or_i, unsigned num_bind, expr* const* binding) {
-    if (m_proof_mode == PGM_DISABLED)
+    SASSERT(proofs_enabled());
+    if (proofs_disabled())
         return m_undef_proof;
     vector<parameter> params;
     for (unsigned i = 0; i < num_bind; ++i) {
@@ -2959,7 +2937,8 @@ bool ast_manager::is_rewrite(expr const* e, expr*& r1, expr*& r2) const {
 }
 
 proof * ast_manager::mk_def_axiom(expr * ax) {
-    if (m_proof_mode == PGM_DISABLED)
+    SASSERT(proofs_enabled());
+    if (proofs_disabled())
         return m_undef_proof;
     return mk_app(m_basic_family_id, PR_DEF_AXIOM, ax);
 }
@@ -3001,7 +2980,7 @@ proof * ast_manager::mk_unit_resolution(unsigned num_proofs, proof * const * pro
                 new_lits.push_back(lit);
         }
         DEBUG_CODE({
-            for (unsigned i = 1; m_proof_mode == PGM_FINE && i < num_proofs; i++) {
+                for (unsigned i = 1; proofs_enabled() && i < num_proofs; i++) {
                 CTRACE("mk_unit_resolution_bug", !found.get(i, false),
                        for (unsigned j = 0; j < num_proofs; j++) {
                            if (j == i) tout << "Index " << i << " was not found:\n";
@@ -3080,14 +3059,11 @@ proof * ast_manager::mk_unit_resolution(unsigned num_proofs, proof * const * pro
 }
 
 proof * ast_manager::mk_hypothesis(expr * h) {
-    if (m_proof_mode == PGM_DISABLED)
-        return m_undef_proof;
     return mk_app(m_basic_family_id, PR_HYPOTHESIS, h);
 }
 
 proof * ast_manager::mk_lemma(proof * p, expr * lemma) {
-    if (m_proof_mode == PGM_DISABLED)
+    if (!p) return p;
-        return m_undef_proof;
     SASSERT(has_fact(p));
     CTRACE("mk_lemma", !is_false(get_fact(p)), tout << mk_ll_pp(p, *this) << "\n";);
     SASSERT(is_false(get_fact(p)));
@@ -3100,7 +3076,7 @@ proof * ast_manager::mk_def_intro(expr * new_def) {
 }
 
 proof * ast_manager::mk_apply_defs(expr * n, expr * def, unsigned num_proofs, proof * const * proofs) {
-    if (m_proof_mode == PGM_DISABLED)
+    if (proofs_disabled())
         return m_undef_proof;
     ptr_buffer<expr> args;
     args.append(num_proofs, (expr**) proofs);
@@ -3109,10 +3085,7 @@ proof * ast_manager::mk_apply_defs(expr * n, expr * def, unsigned num_proofs, pr
 }
 
 proof * ast_manager::mk_iff_oeq(proof * p) {
-    if (m_proof_mode == PGM_DISABLED)
+    if (!p) return p;
-        return m_undef_proof;
-    if (!p)
-        return p;
 
     SASSERT(has_fact(p));
     SASSERT(is_iff(get_fact(p)) || is_oeq(get_fact(p)));
@@ -3136,7 +3109,7 @@ bool ast_manager::check_nnf_proof_parents(unsigned num_proofs, proof * const * p
 }
 
 proof * ast_manager::mk_nnf_pos(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) {
-    if (m_proof_mode == PGM_DISABLED)
+    if (proofs_disabled())
         return m_undef_proof;
     check_nnf_proof_parents(num_proofs, proofs);
     ptr_buffer<expr> args;
@@ -3146,7 +3119,7 @@ proof * ast_manager::mk_nnf_pos(expr * s, expr * t, unsigned num_proofs, proof *
 }
 
 proof * ast_manager::mk_nnf_neg(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) {
-    if (m_proof_mode == PGM_DISABLED)
+    if (proofs_disabled())
         return m_undef_proof;
     check_nnf_proof_parents(num_proofs, proofs);
     ptr_buffer<expr> args;
@@ -3156,7 +3129,7 @@ proof * ast_manager::mk_nnf_neg(expr * s, expr * t, unsigned num_proofs, proof *
 }
 
 proof * ast_manager::mk_nnf_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) {
-    if (m_proof_mode == PGM_DISABLED)
+    if (proofs_disabled())
         return m_undef_proof;
     ptr_buffer<expr> args;
     args.append(num_proofs, (expr**) proofs);
@@ -3165,7 +3138,7 @@ proof * ast_manager::mk_nnf_star(expr * s, expr * t, unsigned num_proofs, proof
 }
 
 proof * ast_manager::mk_skolemization(expr * q, expr * e) {
-    if (m_proof_mode == PGM_DISABLED)
+    if (proofs_disabled())
         return m_undef_proof;
     SASSERT(is_bool(q));
     SASSERT(is_bool(e));
@@ -3173,7 +3146,7 @@ proof * ast_manager::mk_skolemization(expr * q, expr * e) {
 }
 
 proof * ast_manager::mk_cnf_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) {
-    if (m_proof_mode == PGM_DISABLED)
+    if (proofs_disabled())
         return m_undef_proof;
     ptr_buffer<expr> args;
     args.append(num_proofs, (expr**) proofs);
@@ -3182,7 +3155,7 @@ proof * ast_manager::mk_cnf_star(expr * s, expr * t, unsigned num_proofs, proof
 }
 
 proof * ast_manager::mk_and_elim(proof * p, unsigned i) {
-    if (m_proof_mode == PGM_DISABLED)
+    if (proofs_disabled())
         return m_undef_proof;
     SASSERT(has_fact(p));
     SASSERT(is_and(get_fact(p)));
@@ -3193,7 +3166,7 @@ proof * ast_manager::mk_and_elim(proof * p, unsigned i) {
 }
 
 proof * ast_manager::mk_not_or_elim(proof * p, unsigned i) {
-    if (m_proof_mode == PGM_DISABLED)
+    if (proofs_disabled())
         return m_undef_proof;
     SASSERT(has_fact(p));
     SASSERT(is_not(get_fact(p)));
@@ -3216,7 +3189,7 @@ proof * ast_manager::mk_th_lemma(
     unsigned num_params, parameter const* params
     )
 {
-    if (m_proof_mode == PGM_DISABLED)
+    if (proofs_disabled())
         return m_undef_proof;
 
     ptr_buffer<expr> args;

src/ast/ast.h

@@ -1396,8 +1396,7 @@ public:
 
 enum proof_gen_mode {
     PGM_DISABLED,
-    PGM_COARSE,
+    PGM_ENABLED
-    PGM_FINE
 };
 
 // -----------------------------------
@@ -2088,15 +2087,14 @@ protected:
     proof * mk_proof(family_id fid, decl_kind k, expr * arg1, expr * arg2);
     proof * mk_proof(family_id fid, decl_kind k, expr * arg1, expr * arg2, expr * arg3);
 
+    proof * mk_undef_proof() const { return m_undef_proof; }
+
 public:
     bool proofs_enabled() const { return m_proof_mode != PGM_DISABLED; }
     bool proofs_disabled() const { return m_proof_mode == PGM_DISABLED; }
-    bool coarse_grain_proofs() const { return m_proof_mode == PGM_COARSE; }
-    bool fine_grain_proofs() const { return m_proof_mode == PGM_FINE; }
     proof_gen_mode proof_mode() const { return m_proof_mode; }
     void toggle_proof_mode(proof_gen_mode m) { m_proof_mode = m; } // APIs for creating proof objects return [undef]
 
-    proof * mk_undef_proof() const { return m_undef_proof; }
 
     bool is_proof(expr const * n) const { return is_app(n) && to_app(n)->get_decl()->get_range() == m_proof_sort; }
 

src/ast/ast_pp_dot.cpp

@@ -0,0 +1,133 @@
+/*++
+
+Abstract: Pretty-printer for proofs in Graphviz format
+
+--*/
+
+#include "util/util.h"
+#include "util/map.h"
+#include "ast/ast_pp_dot.h"
+
+// string escaping for DOT
+std::string escape_dot(std::string const & s) {
+    std::string res;
+    res.reserve(s.size()); // preallocate
+    for (auto c : s) {
+        if (c == '\n')
+            res.append("\\l");
+        else
+            res.push_back(c);
+    }
+    return res;
+}
+
+// map from proofs to unique IDs
+typedef obj_map<const expr, unsigned> expr2id;
+
+// temporary structure for traversing the proof and printing it
+struct ast_pp_dot_st {
+    ast_manager &           m_manager;
+    std::ostream &          m_out;
+    const ast_pp_dot *      m_pp;
+    unsigned                m_next_id;
+    expr2id                 m_id_map;
+    obj_hashtable<const expr>     m_printed;
+    svector<const expr *>   m_to_print;
+    bool                    m_first;
+
+    ast_pp_dot_st(const ast_pp_dot * pp, std::ostream & out) :
+        m_manager(pp->get_manager()),
+        m_out(out),
+        m_pp(pp),
+        m_next_id(0),
+        m_id_map(),
+        m_printed(),
+        m_to_print(),
+        m_first(true) {}
+
+    ~ast_pp_dot_st() {};
+    
+    void push_term(const expr * a) { m_to_print.push_back(a); }        
+
+    void pp_loop() {
+        // DFS traversal
+        while (!m_to_print.empty()) {
+            const expr * a = m_to_print.back();
+            m_to_print.pop_back();
+            if (!m_printed.contains(a)) {
+                m_printed.insert(a);
+                if (m().is_proof(a))
+                    pp_step(to_app(a));
+                else
+                    pp_atomic_step(a);
+            }
+        }
+    }
+
+private:
+
+    inline ast_manager & m() const { return m_manager; }
+
+    // label for an expression
+    std::string label_of_expr(const expr * e) const {
+        expr_ref er((expr*)e, m());
+        std::ostringstream out;
+        out << er << std::flush;
+        return escape_dot(out.str());
+    }
+
+    void pp_atomic_step(const expr * e) {
+        unsigned id = get_id(e);
+        m_out << "node_" << id << " [shape=box,color=\"yellow\",style=\"filled\",label=\"" << label_of_expr(e) << "\"] ;" << std::endl;
+    }
+    
+    void pp_step(const proof * p) {
+        TRACE("pp_ast_dot_step", tout << " :kind " << p->get_kind() << " :num-args " << p->get_num_args() << "\n";);
+        if (m().has_fact(p)) {
+            // print result
+            expr* p_res = m().get_fact(p); // result of proof step
+            unsigned id = get_id(p);
+            unsigned num_parents = m().get_num_parents(p);
+            const char* color =
+                m_first ? (m_first=false,"color=\"red\"") : num_parents==0 ? "color=\"yellow\"": "";
+            m_out << "node_" << id <<
+                " [shape=box,style=\"filled\",label=\"" << label_of_expr(p_res) << "\""
+                << color << "]" << std::endl;
+            // now print edges to parents (except last one, which is the result)
+            std::string label = p->get_decl()->get_name().str();
+            for (unsigned i = 0 ; i < num_parents; ++i) {
+                expr* parent = m().get_parent(p, i);
+                // explore parent, also print a link to it
+                push_term(to_app(parent));
+                m_out << "node_" << id << " -> " << "node_" << get_id((expr*)parent)
+                    << "[label=\"" << label << "\"];" << std::endl;;
+            }
+        } else {
+            pp_atomic_step(p);
+        }
+    }
+
+    // find a unique ID for this proof
+    unsigned get_id(const expr * e) {
+        unsigned id = 0;
+        if (!m_id_map.find(e, id)) {
+             id = m_next_id++;
+             m_id_map.insert(e, id);
+        }
+        return id;
+    }
+
+};
+
+// main printer
+std::ostream & ast_pp_dot::pp(std::ostream & out) const {
+    out << "digraph proof { " << std::endl;
+    ast_pp_dot_st pp_st(this, out);
+    pp_st.push_term(m_pr);
+    pp_st.pp_loop();
+    out << std::endl << " } " << std::endl << std::flush;
+    return out;
+}
+
+std::ostream &operator<<(std::ostream &out, const ast_pp_dot & p) { return p.pp(out); }
+

src/ast/ast_pp_dot.h

@@ -0,0 +1,24 @@
+/*++
+
+Abstract: Pretty-printer for proofs in Graphviz format
+
+--*/
+
+#pragma once
+
+#include <iostream>
+#include "ast_pp.h"
+
+class ast_pp_dot {
+    ast_manager &       m_manager;
+    proof * const       m_pr;
+
+  public:
+    ast_pp_dot(proof *pr, ast_manager &m) : m_manager(m), m_pr(pr) {}
+    ast_pp_dot(proof_ref &e) : m_manager(e.m()), m_pr(e.get()) {}
+    
+    std::ostream & pp(std::ostream & out) const;
+    ast_manager & get_manager() const { return m_manager; }
+};
+
+std::ostream &operator<<(std::ostream &out, const ast_pp_dot & p);

src/ast/fpa/bv2fpa_converter.cpp

@@ -250,7 +250,7 @@ bv2fpa_converter::array_model bv2fpa_converter::convert_array_func_interp(model_
     am.new_float_fd = m.mk_fresh_func_decl(arity, array_domain.c_ptr(), rng);
     am.new_float_fi = convert_func_interp(mc, am.new_float_fd, bv_f);
     am.bv_fd = bv_f;
-    am.result = arr_util.mk_as_array(f->get_range(), am.new_float_fd);
+    am.result = arr_util.mk_as_array(am.new_float_fd);
     return am;
 }
 

src/ast/fpa/fpa2bv_converter.cpp

@@ -3076,8 +3076,6 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const *
     split_fp(x, sgn, e, s);
     mk_is_nan(x, x_is_nan);
 
-    sort * fp_srt = m.get_sort(x);
-
     expr_ref unspec(m);
     mk_to_ieee_bv_unspecified(f, num, args, unspec);
 

src/ast/normal_forms/pull_quant.cpp

@@ -229,7 +229,7 @@ struct pull_quant::imp {
                         proofs.push_back(m_manager.mk_pull_quant(arg, to_quantifier(new_arg)));
                 }
                 pull_quant1(to_app(n)->get_decl(), new_args.size(), new_args.c_ptr(), r);
-                if (m_manager.fine_grain_proofs()) {
+                if (m_manager.proofs_enabled()) {
                     app   * r1 = m_manager.mk_app(to_app(n)->get_decl(), new_args.size(), new_args.c_ptr());
                     proof * p1 = proofs.empty() ? 0 : m_manager.mk_congruence(to_app(n), r1, proofs.size(), proofs.c_ptr());
                     proof * p2 = r1 == r ? 0 : m_manager.mk_pull_quant(r1, to_quantifier(r));
@@ -240,7 +240,7 @@ struct pull_quant::imp {
                 expr_ref new_expr(m_manager);
                 pull_quant1(to_quantifier(n)->get_expr(), new_expr);
                 pull_quant1(to_quantifier(n), new_expr, r);
-                if (m_manager.fine_grain_proofs()) {
+                if (m_manager.proofs_enabled()) {
                     quantifier * q1 = m_manager.update_quantifier(to_quantifier(n), new_expr);
                     proof * p1 = 0;
                     if (n != q1) {

src/ast/pattern/pattern_inference.cpp

@@ -606,7 +606,7 @@ bool pattern_inference_cfg::reduce_quantifier(
                 result = m.update_quantifier_weight(tmp, new_weight);
                 TRACE("pattern_inference", tout << "found patterns in database, weight: " << new_weight << "\n" << mk_pp(new_q, m) << "\n";);
             }
-            if (m.fine_grain_proofs())
+            if (m.proofs_enabled())
                 result_pr = m.mk_rewrite(q, new_q);
             return true;
         }
@@ -671,7 +671,7 @@ bool pattern_inference_cfg::reduce_quantifier(
     quantifier_ref new_q(m.update_quantifier(q, new_patterns.size(), (expr**) new_patterns.c_ptr(), new_body), m);
     if (weight != q->get_weight())
         new_q = m.update_quantifier_weight(new_q, weight);
-    if (m.fine_grain_proofs()) {
+    if (m.proofs_enabled()) {
         proof* new_body_pr = m.mk_reflexivity(new_body);
         result_pr = m.mk_quant_intro(q, new_q, new_body_pr);
     }
@@ -689,7 +689,7 @@ bool pattern_inference_cfg::reduce_quantifier(
                     warning_msg("pulled nested quantifier to be able to find an useable pattern (quantifier id: %s)", q->get_qid().str().c_str());
                 }
                 new_q = m.update_quantifier(result2, new_patterns.size(), (expr**) new_patterns.c_ptr(), result2->get_expr());
-                if (m.fine_grain_proofs()) {
+                if (m.proofs_enabled()) {
                     result_pr = m.mk_transitivity(new_pr, m.mk_quant_intro(result2, new_q, m.mk_reflexivity(new_q->get_expr())));
                 }
                 TRACE("pattern_inference", tout << "pulled quantifier:\n" << mk_pp(new_q, m) << "\n";);

src/ast/proofs/CMakeLists.txt

@@ -1,6 +1,7 @@
-z3_add_component(proof_checker
+z3_add_component(proofs
   SOURCES
     proof_checker.cpp
+    proof_utils.cpp
   COMPONENT_DEPENDENCIES
     rewriter
-)
+)

src/ast/proofs/proof_checker.cpp

@@ -4,10 +4,9 @@ Copyright (c) 2015 Microsoft Corporation
 
 --*/
 
-#include "ast/proof_checker/proof_checker.h"
+#include "ast/proofs/proof_checker.h"
 #include "ast/ast_ll_pp.h"
 #include "ast/ast_pp.h"
-// include "spc_decl_plugin.h"
 #include "ast/ast_smt_pp.h"
 #include "ast/arith_decl_plugin.h"
 #include "ast/rewriter/th_rewriter.h"

src/ast/proofs/proof_utils.cpp

@@ -1,15 +1,343 @@
-
 /*++
-Copyright (c) 2015 Microsoft Corporation
+Copyright (c) 2017 Arie Gurfinkel
+
+Module Name:
+
+    proof_utils.cpp
+
+Abstract:
+    Utilities to traverse and manipulate proofs
+
+Author:
+    Bernhard Gleiss
+    Arie Gurfinkel
+
+Revision History:
 
 --*/
 
-#include "muz/base/dl_util.h"
+#include "ast/ast_util.h"
-#include "muz/base/proof_utils.h"
+#include "ast/ast_pp.h"
-#include "ast/ast_smt2_pp.h"
+#include "ast/proofs/proof_utils.h"
+#include "ast/proofs/proof_checker.h"
 #include "ast/rewriter/var_subst.h"
+#include "util/container_util.h"
+
+
+proof_post_order::proof_post_order(proof* root, ast_manager& manager) : m(manager)
+{m_todo.push_back(root);}
+
+bool proof_post_order::hasNext()
+{return !m_todo.empty();}
+
+/*
+ * iterative post-order depth-first search (DFS) through the proof DAG
+ */
+proof* proof_post_order::next()
+{
+    while (!m_todo.empty()) {
+        proof* currentNode = m_todo.back();
+
+        // if we haven't already visited the current unit
+        if (!m_visited.is_marked(currentNode)) {
+            bool existsUnvisitedParent = false;
+
+            // add unprocessed premises to stack for DFS. 
+            // If there is at least one unprocessed premise, don't compute the result
+            // for currentProof now, but wait until those unprocessed premises are processed.
+            for (unsigned i = 0; i < m.get_num_parents(currentNode); ++i) {
+                SASSERT(m.is_proof(currentNode->get_arg(i)));
+                proof* premise = to_app(currentNode->get_arg(i));
+
+                // if we haven't visited the current premise yet
+                if (!m_visited.is_marked(premise)) {
+                    // add it to the stack
+                    m_todo.push_back(premise);
+                    existsUnvisitedParent = true;
+                }
+            }
+
+            // if we already visited all parent-inferences, we can visit the inference too
+            if (!existsUnvisitedParent) {
+                m_visited.mark(currentNode, true);
+                m_todo.pop_back();
+                return currentNode;
+            }
+        } else {
+            m_todo.pop_back();
+        }
+    }
+    // we have already iterated through all inferences
+    return nullptr;
+}
+
 
 class reduce_hypotheses {
+    ast_manager &m;
+    // tracking all created expressions
+    expr_ref_vector m_pinned;
+
+    // cache for the transformation
+    obj_map<proof, proof*> m_cache;
+
+    // map from unit literals to their hypotheses-free derivations
+    obj_map<expr, proof*> m_units;
+
+    // -- all hypotheses in the the proof
+    obj_hashtable<expr> m_hyps;
+
+    // marks hypothetical proofs
+    ast_mark m_hypmark;
+
+
+    // stack
+    ptr_vector<proof> m_todo;
+
+    void reset()
+    {
+        m_cache.reset();
+        m_units.reset();
+        m_hyps.reset();
+        m_hypmark.reset();
+        m_pinned.reset();
+    }
+
+    bool compute_mark1(proof *pr)
+    {
+        bool hyp_mark = false;
+        // lemmas clear all hypotheses
+        if (!m.is_lemma(pr)) {
+            for (unsigned i = 0, sz = m.get_num_parents(pr); i < sz; ++i) {
+                if (m_hypmark.is_marked(m.get_parent(pr, i))) {
+                    hyp_mark = true;
+                    break;
+                }
+            }
+        }
+        m_hypmark.mark(pr, hyp_mark);
+        return hyp_mark;
+    }
+
+    void compute_marks(proof* pr)  {
+        proof *p;
+        proof_post_order pit(pr, m);
+        while (pit.hasNext()) {
+            p = pit.next();
+            if (m.is_hypothesis(p)) {
+                m_hypmark.mark(p, true);
+                m_hyps.insert(m.get_fact(p));
+            } 
+            else {
+                bool hyp_mark = compute_mark1(p);
+                // collect units that are hyp-free and are used as hypotheses somewhere
+                if (!hyp_mark && m.has_fact(p) && m_hyps.contains(m.get_fact(p))) { 
+                    m_units.insert(m.get_fact(p), p); 
+                }
+            }
+        }
+    }
+    void find_units(proof *pr)
+    {
+        // optional. not implemented yet.
+    }
+
+    void reduce(proof* pf, proof_ref &out)
+    {
+        proof *res = NULL;
+
+        m_todo.reset();
+        m_todo.push_back(pf);
+        ptr_buffer<proof> args;
+        bool dirty = false;
+
+        while (!m_todo.empty()) {
+            proof *p, *tmp, *pp;
+            unsigned todo_sz;
+
+            p = m_todo.back();
+            if (m_cache.find(p, tmp)) {
+                res = tmp;
+                m_todo.pop_back();
+                continue;
+            }
+
+            dirty = false;
+            args.reset();
+            todo_sz = m_todo.size();
+            for (unsigned i = 0, sz = m.get_num_parents(p); i < sz; ++i) {
+                pp = m.get_parent(p, i);
+                if (m_cache.find(pp, tmp)) {
+                    args.push_back(tmp);
+                    dirty = dirty || pp != tmp;
+                } else {
+                    m_todo.push_back(pp);
+                }
+            }
+
+            if (todo_sz < m_todo.size()) { continue; }
+            else { m_todo.pop_back(); }
+
+            if (m.is_hypothesis(p)) {
+                // hyp: replace by a corresponding unit
+                if (m_units.find(m.get_fact(p), tmp)) {
+                    res = tmp;
+                } else { res = p; }
+            }
+
+            else if (!dirty) { res = p; }
+
+            else if (m.is_lemma(p)) {
+                //lemma: reduce the premise; remove reduced consequences from conclusion
+                SASSERT(args.size() == 1);
+                res = mk_lemma_core(args.get(0), m.get_fact(p));
+                compute_mark1(res);
+            } else if (m.is_unit_resolution(p)) {
+                // unit: reduce untis; reduce the first premise; rebuild unit resolution
+                res = mk_unit_resolution_core(args.size(), args.c_ptr());
+                compute_mark1(res);
+            } else  {
+                // other: reduce all premises; reapply
+                if (m.has_fact(p)) { args.push_back(to_app(m.get_fact(p))); }
+                SASSERT(p->get_decl()->get_arity() == args.size());
+                res = m.mk_app(p->get_decl(), args.size(), (expr * const*)args.c_ptr());
+                m_pinned.push_back(res);
+                compute_mark1(res);
+            }
+
+            SASSERT(res);
+            m_cache.insert(p, res);
+
+            if (m.has_fact(res) && m.is_false(m.get_fact(res))) { break; }
+        }
+
+        out = res;
+    }
+
+    // returns true if (hypothesis (not a)) would be reduced
+    bool is_reduced(expr *a)
+    {
+        expr_ref e(m);
+        if (m.is_not(a)) { e = to_app(a)->get_arg(0); }
+        else { e = m.mk_not(a); }
+
+        return m_units.contains(e);
+    }
+
+    proof *mk_lemma_core(proof *pf, expr *fact)
+    {
+        ptr_buffer<expr> args;
+        expr_ref lemma(m);
+
+        if (m.is_or(fact)) {
+            for (unsigned i = 0, sz = to_app(fact)->get_num_args(); i < sz; ++i) {
+                expr *a = to_app(fact)->get_arg(i);
+                if (!is_reduced(a))
+                { args.push_back(a); }
+            }
+        } else if (!is_reduced(fact))
+        { args.push_back(fact); }
+
+
+        if (args.size() == 0) { return pf; }
+        else if (args.size() == 1) {
+            lemma = args.get(0);
+        } else {
+            lemma = m.mk_or(args.size(), args.c_ptr());
+        }
+        proof* res = m.mk_lemma(pf, lemma);
+        m_pinned.push_back(res);
+
+        if (m_hyps.contains(lemma))
+        { m_units.insert(lemma, res); }
+        return res;
+    }
+
+    proof *mk_unit_resolution_core(unsigned num_args, proof* const *args)
+    {
+
+        ptr_buffer<proof> pf_args;
+        pf_args.push_back(args [0]);
+
+        app *cls_fact = to_app(m.get_fact(args[0]));
+        ptr_buffer<expr> cls;
+        if (m.is_or(cls_fact)) {
+            for (unsigned i = 0, sz = cls_fact->get_num_args(); i < sz; ++i)
+            { cls.push_back(cls_fact->get_arg(i)); }
+        } else { cls.push_back(cls_fact); }
+
+        // construct new resovent
+        ptr_buffer<expr> new_fact_cls;
+        bool found;
+        // XXX quadratic
+        for (unsigned i = 0, sz = cls.size(); i < sz; ++i) {
+            found = false;
+            for (unsigned j = 1; j < num_args; ++j) {
+                if (m.is_complement(cls.get(i), m.get_fact(args [j]))) {
+                    found = true;
+                    pf_args.push_back(args [j]);
+                    break;
+                }
+            }
+            if (!found) {
+                new_fact_cls.push_back(cls.get(i));
+            }
+        }
+
+        SASSERT(new_fact_cls.size() + pf_args.size() - 1 == cls.size());
+        expr_ref new_fact(m);
+        new_fact = mk_or(m, new_fact_cls.size(), new_fact_cls.c_ptr());
+
+        // create new proof step
+        proof *res = m.mk_unit_resolution(pf_args.size(), pf_args.c_ptr(), new_fact);
+        m_pinned.push_back(res);
+        return res;
+    }
+
+    // reduce all units, if any unit reduces to false return true and put its proof into out
+    bool reduce_units(proof_ref &out)
+    {
+        proof_ref res(m);
+        for (auto entry : m_units) {
+            reduce(entry.get_value(), res);
+            if (m.is_false(m.get_fact(res))) {
+                out = res;
+                return true;
+            }
+            res.reset();
+        }
+        return false;
+    }
+
+
+public:
+    reduce_hypotheses(ast_manager &m) : m(m), m_pinned(m) {}
+
+
+    void operator()(proof_ref &pr)
+    {
+        compute_marks(pr);
+        if (!reduce_units(pr)) {
+            reduce(pr.get(), pr);
+        }
+        reset();
+    }
+};
+
+void reduce_hypotheses(proof_ref &pr) {
+    ast_manager &m = pr.get_manager();
+    class reduce_hypotheses hypred(m);
+    hypred(pr);
+    DEBUG_CODE(proof_checker pc(m);
+               expr_ref_vector side(m);
+               SASSERT(pc.check(pr, side));
+              );
+}
+
+
+
+#include "ast/ast_smt2_pp.h"
+
+class reduce_hypotheses0 {
     typedef obj_hashtable<expr> expr_set;
     ast_manager&          m;
     // reference for any expression created by the tranformation
@@ -85,7 +413,7 @@ class reduce_hypotheses {
                         m_hyprefs.push_back(hyps);
                         inherited = false;
                     }
-                    datalog::set_union(*hyps, *hyps1);
+                    set_union(*hyps, *hyps1);
                 }
             }
         }
@@ -137,7 +465,7 @@ class reduce_hypotheses {
     }    
     
 public:
-    reduce_hypotheses(ast_manager& m): m(m), m_refs(m) {}
+    reduce_hypotheses0(ast_manager& m): m(m), m_refs(m) {}
     
     void operator()(proof_ref& pr) {
         proof_ref tmp(m);
@@ -416,7 +744,7 @@ public:
 
 void proof_utils::reduce_hypotheses(proof_ref& pr) {
     ast_manager& m = pr.get_manager();
-    class reduce_hypotheses reduce(m);
+    class reduce_hypotheses0 reduce(m);
     reduce(pr);
     CTRACE("proof_utils", !is_closed(m, pr), tout << mk_pp(pr, m) << "\n";);
 }

src/ast/proofs/proof_utils.h

@@ -0,0 +1,238 @@
+/*++
+Copyright (c) 2017 Microsoft Corporation
+
+Module Name:
+
+    proof_utils.h
+
+Abstract:
+    Utilities to traverse and manipulate proofs
+
+Author:
+    Bernhard Gleiss
+    Arie Gurfinkel
+    Nikolaj Bjorner
+
+Revision History:
+
+--*/
+
+#ifndef PROOF_UTILS_H_
+#define PROOF_UTILS_H_
+#include "ast/ast.h"
+#include "ast/ast_pp.h"
+#include "ast/rewriter/bool_rewriter.h"
+#include "ast/proofs/proof_checker.h"
+
+/*
+ * iterator, which traverses the proof in depth-first post-order.
+ */
+
+class proof_post_order {
+public:
+    proof_post_order(proof* refutation, ast_manager& manager);
+    bool hasNext();
+    proof* next();
+
+private:
+    ptr_vector<proof> m_todo;
+    ast_mark          m_visited; // the proof nodes we have already visited
+    ast_manager&      m;
+};
+
+void reduce_hypotheses(proof_ref &pr);
+
+
+class proof_utils {
+public:
+    /**
+       \brief reduce the set of hypotheses used in the proof.
+     */
+    static void reduce_hypotheses(proof_ref& pr);
+
+    /**
+       \brief Check that a proof does not contain open hypotheses.
+    */
+    static bool is_closed(ast_manager& m, proof* p);
+
+    /**
+       \brief Permute unit resolution rule with th-lemma
+    */
+    static void permute_unit_resolution(proof_ref& pr);
+
+    /**
+       \brief Push instantiations created in hyper-resolutions up to leaves.
+       This produces a "ground" proof where leaves are annotated by instantiations.
+    */
+    static void push_instantiations_up(proof_ref& pr);
+
+
+};
+
+class elim_aux_assertions {
+
+    static bool matches_fact(expr_ref_vector &args, expr* &match) {
+        ast_manager &m = args.get_manager();
+        expr *fact = args.back();
+        for (unsigned i = 0, sz = args.size() - 1; i < sz; ++i) {
+            expr *arg = args.get(i);
+            if (m.is_proof(arg) &&
+                m.has_fact(to_app(arg)) &&
+                m.get_fact(to_app(arg)) == fact) {
+                match = arg;
+                return true;
+            }
+        }
+        return false;
+    }
+
+    app_ref m_aux;
+public:
+    elim_aux_assertions(app_ref aux) : m_aux(aux) {}
+
+    void mk_or_core(expr_ref_vector &args, expr_ref &res)
+    {
+        ast_manager &m = args.get_manager();
+        unsigned j = 0;
+        for (unsigned i = 0, sz = args.size(); i < sz; ++i) {
+            if (m.is_false(args.get(i))) { continue; }
+            if (i != j) { args [j] = args.get(i); }
+            ++j;
+        }
+        SASSERT(j >= 1);
+        res = j > 1 ? m.mk_or(j, args.c_ptr()) : args.get(0);
+    }
+
+    void mk_app(func_decl *decl, expr_ref_vector &args, expr_ref &res)
+    {
+        ast_manager &m = args.get_manager();
+        bool_rewriter brwr(m);
+
+        if (m.is_or(decl))
+        { mk_or_core(args, res); }
+        else if (m.is_iff(decl) && args.size() == 2)
+            // avoiding simplifying equalities. In particular,
+            // we don't want (= (not a) (not b)) to be reduced to (= a b)
+        { res = m.mk_iff(args.get(0), args.get(1)); }
+        else
+        { brwr.mk_app(decl, args.size(), args.c_ptr(), res); }
+    }
+
+    void operator()(ast_manager &m, proof *pr, proof_ref &res)
+    {
+        DEBUG_CODE(proof_checker pc(m);
+                   expr_ref_vector side(m);
+                   SASSERT(pc.check(pr, side));
+                  );
+        obj_map<app, app*> cache;
+        bool_rewriter brwr(m);
+
+        // for reference counting of new proofs
+        app_ref_vector pinned(m);
+
+        ptr_vector<app> todo;
+        todo.push_back(pr);
+
+        expr_ref not_aux(m);
+        not_aux = m.mk_not(m_aux);
+
+        expr_ref_vector args(m);
+
+        while (!todo.empty()) {
+            app *p, *r;
+            expr *a;
+
+            p = todo.back();
+            if (cache.find(pr, r)) {
+                todo.pop_back();
+                continue;
+            }
+
+            SASSERT(!todo.empty() || pr == p);
+            bool dirty = false;
+            unsigned todo_sz = todo.size();
+            args.reset();
+            for (unsigned i = 0, sz = p->get_num_args(); i < sz; ++i) {
+                expr* arg = p->get_arg(i);
+                if (arg == m_aux.get()) {
+                    dirty = true;
+                    args.push_back(m.mk_true());
+                } else if (arg == not_aux.get()) {
+                    dirty = true;
+                    args.push_back(m.mk_false());
+                }
+                // skip (asserted m_aux)
+                else if (m.is_asserted(arg, a) && a == m_aux.get()) {
+                    dirty = true;
+                }
+                // skip (hypothesis m_aux)
+                else if (m.is_hypothesis(arg, a) && a == m_aux.get()) {
+                    dirty = true;
+                } else if (is_app(arg) && cache.find(to_app(arg), r)) {
+                    dirty |= (arg != r);
+                    args.push_back(r);
+                } else if (is_app(arg))
+                { todo.push_back(to_app(arg)); }
+                else
+                    // -- not an app
+                { args.push_back(arg); }
+
+            }
+            if (todo_sz < todo.size()) {
+                // -- process parents
+                args.reset();
+                continue;
+            }
+
+            // ready to re-create
+            app_ref newp(m);
+            if (!dirty) { newp = p; }
+            else if (m.is_unit_resolution(p)) {
+                if (args.size() == 2)
+                    // unit resolution with m_aux that got collapsed to nothing
+                { newp = to_app(args.get(0)); }
+                else {
+                    ptr_vector<proof> parents;
+                    for (unsigned i = 0, sz = args.size() - 1; i < sz; ++i)
+                    { parents.push_back(to_app(args.get(i))); }
+                    SASSERT(parents.size() == args.size() - 1);
+                    newp = m.mk_unit_resolution(parents.size(), parents.c_ptr());
+                    // XXX the old and new facts should be
+                    // equivalent. The test here is much
+                    // stronger. It might need to be relaxed.
+                    SASSERT(m.get_fact(newp) == args.back());
+                    pinned.push_back(newp);
+                }
+            } else if (matches_fact(args, a)) {
+                newp = to_app(a);
+            } else {
+                expr_ref papp(m);
+                mk_app(p->get_decl(), args, papp);
+                newp = to_app(papp.get());
+                pinned.push_back(newp);
+            }
+            cache.insert(p, newp);
+            todo.pop_back();
+            CTRACE("virtual",
+                   p->get_decl_kind() == PR_TH_LEMMA &&
+                   p->get_decl()->get_parameter(0).get_symbol() == "arith" &&
+                   p->get_decl()->get_num_parameters() > 1 &&
+                   p->get_decl()->get_parameter(1).get_symbol() == "farkas",
+                   tout << "Old pf: " << mk_pp(p, m) << "\n"
+                   << "New pf: " << mk_pp(newp, m) << "\n";);
+        }
+
+        proof *r;
+        VERIFY(cache.find(pr, r));
+
+        DEBUG_CODE(
+            proof_checker pc(m);
+            expr_ref_vector side(m);
+            SASSERT(pc.check(r, side));
+        );
+
+        res = r ;
+    }
+};
+
+#endif

src/ast/rewriter/fpa_rewriter.cpp

@@ -119,7 +119,6 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const
             // BV -> float
             SASSERT(bvs1 == sbits + ebits);
             unsynch_mpz_manager & mpzm = m_fm.mpz_manager();
-            unsynch_mpq_manager & mpqm = m_fm.mpq_manager();
             scoped_mpz sig(mpzm), exp(mpzm);
 
             const mpz & sm1 = m_fm.m_powers2(sbits - 1);

src/ast/scoped_proof.h

@@ -37,7 +37,7 @@ public:
 
 class scoped_proof : public scoped_proof_mode {
 public:
-    scoped_proof(ast_manager& m): scoped_proof_mode(m, PGM_FINE) {}
+    scoped_proof(ast_manager& m): scoped_proof_mode(m, PGM_ENABLED) {}
 };
 
 class scoped_no_proof : public scoped_proof_mode {

src/cmd_context/basic_cmds.cpp

@@ -20,6 +20,7 @@ Notes:
 #include "util/version.h"
 #include "ast/ast_smt_pp.h"
 #include "ast/ast_smt2_pp.h"
+#include "ast/ast_pp_dot.h"
 #include "ast/ast_pp.h"
 #include "ast/array_decl_plugin.h"
 #include "ast/pp.h"
@@ -202,6 +203,26 @@ ATOMIC_CMD(get_proof_cmd, "get-proof", "retrieve proof", {
     }
 });
 
+ATOMIC_CMD(get_proof_graph_cmd, "get-proof-graph", "retrieve proof and print it in graphviz", {
+    if (!ctx.produce_proofs())
+        throw cmd_exception("proof construction is not enabled, use command (set-option :produce-proofs true)");
+    if (!ctx.has_manager() ||
+        ctx.cs_state() != cmd_context::css_unsat)
+        throw cmd_exception("proof is not available");
+    proof_ref pr(ctx.m());
+    pr = ctx.get_check_sat_result()->get_proof();
+    if (pr == 0)
+        throw cmd_exception("proof is not available");
+    if (ctx.well_sorted_check_enabled() && !is_well_sorted(ctx.m(), pr)) {
+        throw cmd_exception("proof is not well sorted");
+    }
+
+    context_params& params = ctx.params();
+    const std::string& file = params.m_dot_proof_file;
+    std::ofstream out(file);
+    out << ast_pp_dot(pr) << std::endl;
+});
+
 static void print_core(cmd_context& ctx) {
     ptr_vector<expr> core;
     ctx.get_check_sat_result()->get_unsat_core(core);
@@ -840,6 +861,7 @@ void install_basic_cmds(cmd_context & ctx) {
     ctx.insert(alloc(get_assignment_cmd));
     ctx.insert(alloc(get_assertions_cmd));
     ctx.insert(alloc(get_proof_cmd));
+    ctx.insert(alloc(get_proof_graph_cmd));
     ctx.insert(alloc(get_unsat_core_cmd));
     ctx.insert(alloc(set_option_cmd));
     ctx.insert(alloc(get_option_cmd));

src/cmd_context/cmd_context.cpp

@@ -774,7 +774,6 @@ bool cmd_context::is_func_decl(symbol const & s) const {
 }
 
 void cmd_context::insert(symbol const & s, func_decl * f) {
-    m_check_sat_result = 0;
     if (!m_check_logic(f)) {
         throw cmd_exception(m_check_logic.get_last_error());
     }
@@ -805,7 +804,6 @@ void cmd_context::insert(symbol const & s, func_decl * f) {
 }
 
 void cmd_context::insert(symbol const & s, psort_decl * p) {
-    m_check_sat_result = 0;
     if (m_psort_decls.contains(s)) {
         throw cmd_exception("sort already defined ", s);
     }
@@ -819,7 +817,6 @@ void cmd_context::insert(symbol const & s, psort_decl * p) {
 
 void cmd_context::insert(symbol const & s, unsigned arity, sort *const* domain, expr * t) {
     expr_ref _t(t, m());
-    m_check_sat_result = 0;
     if (m_builtin_decls.contains(s)) {
         throw cmd_exception("invalid macro/named expression, builtin symbol ", s);
     }
@@ -1066,16 +1063,31 @@ void cmd_context::mk_app(symbol const & s, unsigned num_args, expr * const * arg
         if (fs.more_than_one())
             throw cmd_exception("ambiguous constant reference, more than one constant with the same sort, use a qualified expression (as <symbol> <sort>) to disumbiguate ", s);
         func_decl * f = fs.first();
-        if (f == 0)
+        if (f == 0) {
             throw cmd_exception("unknown constant ", s);
+        }
         if (f->get_arity() != 0)
             throw cmd_exception("invalid function application, missing arguments ", s);
         result = m().mk_const(f);
     }
     else {
         func_decl * f = fs.find(m(), num_args, args, range);
-        if (f == 0)
+        if (f == 0) {
-            throw cmd_exception("unknown constant ", s);
+            std::ostringstream buffer;
+            buffer << "unknown constant " << s << " ";
+            buffer << " (";
+            bool first = true;
+            for (unsigned i = 0; i < num_args; ++i, first = false) {
+                if (!first) buffer << " ";
+                buffer << mk_pp(m().get_sort(args[i]), m());
+            }            
+            buffer << ") ";
+            if (range) buffer << mk_pp(range, m()) << " ";
+            for (unsigned i = 0; i < fs.get_num_entries(); ++i) {
+                buffer << "\ndeclared: " << mk_pp(fs.get_entry(i), m()) << " ";
+            }
+            throw cmd_exception(buffer.str().c_str());
+        }
         if (well_sorted_check_enabled())
             m().check_sort(f, num_args, args);
         result = m().mk_app(f, num_args, args);

src/cmd_context/context_params.cpp

@@ -111,6 +111,9 @@ void context_params::set(char const * param, char const * value) {
     else if (p == "trace_file_name") {
         m_trace_file_name = value;
     }
+    else if (p == "dot_proof_file") {
+        m_dot_proof_file = value;  
+    }
     else if (p == "unsat_core") {
         set_bool(m_unsat_core, param, value);
     }
@@ -146,6 +149,7 @@ void context_params::updt_params(params_ref const & p) {
     m_dump_models       = p.get_bool("dump_models", m_dump_models);
     m_trace             = p.get_bool("trace", m_trace);
     m_trace_file_name   = p.get_str("trace_file_name", "z3.log");
+    m_dot_proof_file    = p.get_str("dot_proof_file", "proof.dot");
     m_unsat_core        = p.get_bool("unsat_core", m_unsat_core);
     m_debug_ref_count   = p.get_bool("debug_ref_count", m_debug_ref_count);
     m_smtlib2_compliant = p.get_bool("smtlib2_compliant", m_smtlib2_compliant);
@@ -161,6 +165,7 @@ void context_params::collect_param_descrs(param_descrs & d) {
     d.insert("dump_models", CPK_BOOL, "dump models whenever check-sat returns sat", "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("dot_proof_file", CPK_STRING, "file in which to output graphical proofs", "proof.dot");
     d.insert("debug_ref_count", CPK_BOOL, "debug support for AST reference counting", "false");
     d.insert("smtlib2_compliant", CPK_BOOL, "enable/disable SMT-LIB 2.0 compliance", "false");
     collect_solver_param_descrs(d);
@@ -192,7 +197,7 @@ void context_params::get_solver_params(ast_manager const & m, params_ref & p, bo
 
 ast_manager * context_params::mk_ast_manager() {
     ast_manager * r = alloc(ast_manager,
-                            m_proof ? PGM_FINE : PGM_DISABLED,
+                            m_proof ? PGM_ENABLED : PGM_DISABLED,
                             m_trace ? m_trace_file_name.c_str() : 0);
     if (m_smtlib2_compliant)
         r->enable_int_real_coercions(false);

src/cmd_context/context_params.h

@@ -30,6 +30,7 @@ class context_params {
 public:
     bool        m_auto_config;
     bool        m_proof;
+    std::string m_dot_proof_file;
     bool        m_interpolants;
     bool        m_debug_ref_count;
     bool        m_trace;

src/cmd_context/interpolant_cmds.cpp

@@ -147,7 +147,7 @@ static void compute_interpolant_and_maybe_check(cmd_context & ctx, expr * t, par
     ast_manager &_m = ctx.m();
     // TODO: the following is a HACK to enable proofs in the old smt solver
     // When we stop using that solver, this hack can be removed
-    scoped_proof_mode spm(_m,PGM_FINE);
+    scoped_proof_mode spm(_m,PGM_ENABLED);
     ctx.params().get_solver_params(_m, p, proofs_enabled, models_enabled, unsat_core_enabled);
     p.set_bool("proof", true);
     scoped_ptr<solver> sp = (ctx.get_interpolating_solver_factory())(_m, p, true, models_enabled, false, ctx.get_logic());

src/interp/iz3mgr.h

@@ -57,12 +57,12 @@ typedef ast raw_ast;
 
 /** Wrapper around an ast pointer */
 class ast_i {
- protected:
+protected:
     raw_ast *_ast;
- public:
+public:
     raw_ast * const &raw() const {return _ast;}
     ast_i(raw_ast *a){_ast = a;}
-  
+    
     ast_i(){_ast = 0;}
     bool eq(const ast_i &other) const {
         return _ast == other._ast;
@@ -86,19 +86,19 @@ class ast_i {
 /** Reference counting verison of above */
 class ast_r : public ast_i {
     ast_manager *_m;
- public:
+public:
- ast_r(ast_manager *m, raw_ast *a) : ast_i(a) {
+    ast_r(ast_manager *m, raw_ast *a) : ast_i(a) {
         _m = m;
         m->inc_ref(a);
     }
-  
+    
     ast_r() {_m = 0;}
-
+    
- ast_r(const ast_r &other) : ast_i(other) {
+    ast_r(const ast_r &other) : ast_i(other) {
         _m = other._m;
         if (_m) _m->inc_ref(_ast);
     }
-
+    
     ast_r &operator=(const ast_r &other) {
         if(_ast)
             _m->dec_ref(_ast);
@@ -107,12 +107,12 @@ class ast_r : public ast_i {
         if (_m) _m->inc_ref(_ast);
         return *this;
     }
-
+    
-    ~ast_r(){
+    ~ast_r() {
         if(_ast)
             _m->dec_ref(_ast);
     }
-  
+    
     ast_manager *mgr() const {return _m;}
 
 };

src/interp/iz3translate.cpp

@@ -29,6 +29,7 @@
 #include "interp/iz3profiling.h"
 #include "interp/iz3interp.h"
 #include "interp/iz3proof_itp.h"
+#include "ast/ast_pp.h"
 
 #include <assert.h>
 #include <algorithm>
@@ -1851,6 +1852,21 @@ public:
                 }
                 break;
             }
+            case PR_TRANSITIVITY_STAR: {
+                // assume the premises are x = y, y = z, z = u, u = v, ..
+                
+                ast x = arg(conc(prem(proof,0)),0);
+                ast y = arg(conc(prem(proof,0)),1);
+                ast z = arg(conc(prem(proof,1)),1);
+                res = iproof->make_transitivity(x,y,z,args[0],args[1]);
+
+                for (unsigned i = 2; i < nprems; ++i) {
+                    y = z;
+                    z = arg(conc(prem(proof,i)),1);
+                    res = iproof->make_transitivity(x,y,z,res,args[i]);
+                }
+                break;
+            }
             case PR_QUANT_INTRO:
             case PR_MONOTONICITY:
                 {
@@ -2029,6 +2045,7 @@ public:
                 break;
             }
             default:
+                IF_VERBOSE(0, verbose_stream() << "Unsupported proof rule: " << expr_ref((expr*)proof.raw(), *proof.mgr()) << "\n";);
                 //                pfgoto(proof);                
                 // SASSERT(0 && "translate_main: unsupported proof rule");
                 throw unsupported();

src/interp/iz3translate.h

@@ -36,7 +36,7 @@ class iz3translation : public iz3base {
 
     /** This is thrown when the proof cannot be translated. */
     struct unsupported: public iz3_exception {
-        unsupported(): iz3_exception("unsupported") {}
+    unsupported(): iz3_exception("unsupported") { }
     };
 
     static iz3translation *create(iz3mgr &mgr,

src/muz/base/CMakeLists.txt

@@ -10,7 +10,6 @@ z3_add_component(muz
     dl_rule_transformer.cpp
     dl_util.cpp
     hnf.cpp
-    proof_utils.cpp
     rule_properties.cpp
   COMPONENT_DEPENDENCIES
     aig_tactic

src/muz/base/dl_boogie_proof.cpp

@@ -53,7 +53,7 @@ Example from Boogie:
 
 #include "muz/base/dl_boogie_proof.h"
 #include "model/model_pp.h"
-#include "muz/base/proof_utils.h"
+#include "ast/proofs/proof_utils.h"
 #include "ast/ast_pp.h"
 #include "ast/ast_util.h"
 

src/muz/base/dl_context.cpp

@@ -453,7 +453,8 @@ namespace datalog {
         return new_pred;
     }
 
-  void context::add_rule(expr* rl, symbol const& name, unsigned bound) {
+    void context::add_rule(expr* rl, symbol const& name, unsigned bound) {
+        SASSERT(rl);
         m_rule_fmls.push_back(rl);
         m_rule_names.push_back(name);
         m_rule_bounds.push_back(bound);
@@ -461,7 +462,7 @@ namespace datalog {
 
     void context::flush_add_rules() {
         datalog::rule_manager& rm = get_rule_manager();
-        scoped_proof_mode _scp(m, generate_proof_trace()?PGM_FINE:PGM_DISABLED);
+        scoped_proof_mode _scp(m, generate_proof_trace()?PGM_ENABLED:PGM_DISABLED);
         while (m_rule_fmls_head < m_rule_fmls.size()) {
             expr* fml = m_rule_fmls[m_rule_fmls_head].get();
             proof* p = generate_proof_trace()?m.mk_asserted(fml):0;

src/muz/base/dl_rule.cpp

@@ -141,7 +141,7 @@ namespace datalog {
 
 
     void rule_manager::mk_rule(expr* fml, proof* p, rule_set& rules, symbol const& name) {
-        scoped_proof_mode _sc(m, m_ctx.generate_proof_trace()?PGM_FINE:PGM_DISABLED);
+        scoped_proof_mode _sc(m, m_ctx.generate_proof_trace()?PGM_ENABLED:PGM_DISABLED);
         proof_ref pr(p, m);
         expr_ref fml1(m);
         bind_variables(fml, true, fml1);
@@ -343,7 +343,7 @@ namespace datalog {
         }
         TRACE("dl", tout << rule_expr << "\n";);
 
-        scoped_proof_mode _sc(m, m_ctx.generate_proof_trace()?PGM_FINE:PGM_DISABLED);
+        scoped_proof_mode _sc(m, m_ctx.generate_proof_trace()?PGM_ENABLED:PGM_DISABLED);
         proof_ref pr(m);
         if (m_ctx.generate_proof_trace()) {
             pr = m.mk_asserted(rule_expr);

src/muz/base/dl_util.h

@@ -11,7 +11,7 @@ Abstract:
 
 Author:
 
-    Leonardo de Moura (leonardo) 2010-05-20.
+    Krystof Hoder 2010
 
 Revision History:
 
@@ -31,6 +31,7 @@ Revision History:
 #include "util/statistics.h"
 #include "util/stopwatch.h"
 #include "util/lbool.h"
+#include "util/container_util.h"
 
 namespace datalog {
 
@@ -381,129 +382,6 @@ namespace datalog {
     */
     void apply_subst(expr_ref_vector& tgt, expr_ref_vector const& sub);
 
-    // -----------------------------------
-    //
-    // container functions
-    //
-    // -----------------------------------
-
-    template<class Set1, class Set2>
-    void set_intersection(Set1 & tgt, const Set2 & src) {
-        svector<typename Set1::data> to_remove;
-        typename Set1::iterator vit = tgt.begin();
-        typename Set1::iterator vend = tgt.end();
-        for(;vit!=vend;++vit) {
-            typename Set1::data itm=*vit;
-            if(!src.contains(itm)) {
-                to_remove.push_back(itm);
-            }
-        }
-        while(!to_remove.empty()) {
-            tgt.remove(to_remove.back());
-            to_remove.pop_back();
-        }
-    }
-
-    template<class Set>
-    void set_difference(Set & tgt, const Set & to_remove) {
-        typename Set::iterator vit = to_remove.begin();
-        typename Set::iterator vend = to_remove.end();
-        for(;vit!=vend;++vit) {
-            typename Set::data itm=*vit;
-            tgt.remove(itm);
-        }
-    }
-
-    template<class Set1, class Set2>
-    void set_union(Set1 & tgt, const Set2 & to_add) {
-        typename Set2::iterator vit = to_add.begin();
-        typename Set2::iterator vend = to_add.end();
-        for(;vit!=vend;++vit) {
-            typename Set1::data itm=*vit;
-            tgt.insert(itm);
-        }
-    }
-
-    void idx_set_union(idx_set & tgt, const idx_set & src);
-
-    template<class T>
-    void unite_disjoint_maps(T & tgt, const T & src) {
-        typename T::iterator it = src.begin();
-        typename T::iterator end = src.end();
-        for(; it!=end; ++it) {
-            SASSERT(!tgt.contains(it->m_key));
-            tgt.insert(it->m_key, it->m_value);
-        }
-    }
-
-    template<class T, class U>
-    void collect_map_range(T & acc, const U & map) {
-        typename U::iterator it = map.begin();
-        typename U::iterator end = map.end();
-        for(; it!=end; ++it) {
-            acc.push_back(it->m_value);
-        }
-    }
-
-
-    template<class T>
-    void print_container(const T & begin, const T & end, std::ostream & out) {
-        T it = begin;
-        out << "(";
-        bool first = true;
-        for(; it!=end; ++it) {
-            if(first) { first = false; } else { out << ","; }
-            out << (*it);
-        }
-        out << ")";
-    }
-
-    template<class T>
-    void print_container(const T & cont, std::ostream & out) {
-        print_container(cont.begin(), cont.end(), out);
-    }
-
-    template<class T, class M>
-    void print_container(const ref_vector<T,M> & cont, std::ostream & out) {
-        print_container(cont.c_ptr(), cont.c_ptr() + cont.size(), out);
-    }
-
-    template<class T>
-    void print_map(const T & cont, std::ostream & out) {
-        typename T::iterator it = cont.begin();
-        typename T::iterator end = cont.end();
-        out << "(";
-        bool first = true;
-        for(; it!=end; ++it) {
-            if(first) { first = false; } else { out << ","; }
-            out << it->m_key << "->" << it->m_value;
-        }
-        out << ")";
-    }
-
-    template<class It, class V> 
-    unsigned find_index(const It & begin, const It & end, const V & val) {
-        unsigned idx = 0;
-        It it = begin;
-        for(; it!=end; it++, idx++) {
-            if(*it==val) {
-                return idx;
-            }
-        }
-        return UINT_MAX;
-    }
-
-    template<class T, class U>
-    bool containers_equal(const T & begin1, const T & end1, const U & begin2, const U & end2) {
-        T it1 = begin1;
-        U it2 = begin2;
-        for(; it1!=end1 && it2!=end2; ++it1, ++it2) {
-            if(*it1!=*it2) { 
-                return false;
-            }
-        }
-        return it1==end1 && it2==end2;
-    }
 
     template<class T, class U>
     bool vectors_equal(const T & c1, const U & c2) {
@@ -521,6 +399,8 @@ namespace datalog {
         return true;
     }
 
+    void idx_set_union(idx_set & tgt, const idx_set & src);
+
     template<class T>
     struct default_obj_chash {
         unsigned operator()(T const& cont, unsigned i) const {

src/muz/base/proof_utils.h

@@ -1,48 +0,0 @@
-/*++
-Copyright (c) 2012 Microsoft Corporation
-
-Module Name:
-
-    proof_utils.h
-
-Abstract:
-
-    Utilities for transforming proofs.
-
-Author:
-
-    Nikolaj Bjorner (nbjorner) 2012-10-12.
-
-Revision History:
-
---*/
-#ifndef PROOF_UTILS_H_
-#define PROOF_UTILS_H_
-
-class proof_utils {
-public:
-    /**
-       \brief reduce the set of hypotheses used in the proof.
-     */
-    static void reduce_hypotheses(proof_ref& pr);
-
-    /**
-       \brief Check that a proof does not contain open hypotheses.
-    */
-    static bool is_closed(ast_manager& m, proof* p);
-
-    /**
-       \brief Permute unit resolution rule with th-lemma
-    */
-    static void permute_unit_resolution(proof_ref& pr);
-
-    /**
-       \brief Push instantiations created in hyper-resolutions up to leaves.
-       This produces a "ground" proof where leaves are annotated by instantiations.
-    */
-    static void push_instantiations_up(proof_ref& pr);
-
-
-};
-
-#endif

src/muz/fp/dl_cmds.cpp

@@ -189,11 +189,12 @@ public:
         m_bound = bound;
         m_arg_idx++;
     }
-    virtual void reset(cmd_context & ctx) { m_dl_ctx->reset(); prepare(ctx); }
+    virtual void reset(cmd_context & ctx) { m_dl_ctx->reset(); prepare(ctx); m_t = nullptr; }
     virtual void prepare(cmd_context& ctx) { m_arg_idx = 0; m_name = symbol::null; m_bound = UINT_MAX; }
     virtual void finalize(cmd_context & ctx) { 
     }
     virtual void execute(cmd_context & ctx) {
+        if (!m_t) throw cmd_exception("invalid rule, expected formula");
         m_dl_ctx->add_rule(m_t, m_name, m_bound);
     }
 };

src/muz/pdr/pdr_context.cpp

@@ -41,9 +41,8 @@ Notes:
 #include "ast/ast_smt2_pp.h"
 #include "qe/qe_lite.h"
 #include "ast/ast_ll_pp.h"
-#include "ast/proof_checker/proof_checker.h"
+#include "ast/proofs/proof_checker.h"
 #include "smt/smt_value_sort.h"
-#include "muz/base/proof_utils.h"
 #include "muz/base/dl_boogie_proof.h"
 #include "ast/scoped_proof.h"
 #include "tactic/core/blast_term_ite_tactic.h"
@@ -1825,7 +1824,7 @@ namespace pdr {
             m_core_generalizers.push_back(alloc(core_multi_generalizer, *this, 0));
         }
         if (!classify.is_bool()) {
-            m.toggle_proof_mode(PGM_FINE);
+            m.toggle_proof_mode(PGM_ENABLED);
             m_fparams.m_arith_bound_prop = BP_NONE;
             m_fparams.m_arith_auto_config_simplex = true;
             m_fparams.m_arith_propagate_eqs = false;

src/muz/pdr/pdr_farkas_learner.cpp

@@ -31,7 +31,7 @@ Revision History:
 #include "ast/rewriter/th_rewriter.h"
 #include "ast/ast_ll_pp.h"
 #include "tactic/arith/arith_bounds_tactic.h"
-#include "muz/base/proof_utils.h"
+#include "ast/proofs/proof_utils.h"
 #include "ast/reg_decl_plugins.h"
 
 
@@ -372,7 +372,7 @@ namespace pdr {
     
     farkas_learner::farkas_learner(smt_params& params, ast_manager& outer_mgr) 
         : m_proof_params(get_proof_params(params)), 
-          m_pr(PGM_FINE),
+          m_pr(PGM_ENABLED),
           m_constr(0),
           m_combine_farkas_coefficients(true),
           p2o(m_pr, outer_mgr),
@@ -733,8 +733,8 @@ namespace pdr {
                     }
                     else {
                         expr_set* hyps3 = alloc(expr_set);
-                        datalog::set_union(*hyps3, *hyps);
+                        set_union(*hyps3, *hyps);
-                        datalog::set_union(*hyps3, *hyps2);
+                        set_union(*hyps3, *hyps2);
                         hyps = hyps3;
                         hyprefs.push_back(hyps);
                     }
@@ -795,7 +795,7 @@ namespace pdr {
             case PR_LEMMA: {
                 expr_set* hyps2 = alloc(expr_set);
                 hyprefs.push_back(hyps2);
-                datalog::set_union(*hyps2, *hyps); 
+                set_union(*hyps2, *hyps); 
                 hyps = hyps2;
                 expr* fml = m.get_fact(p);
                 hyps->remove(fml);

src/muz/pdr/pdr_generalizers.cpp

@@ -81,7 +81,7 @@ namespace pdr {
         m_gen(n, core0, uses_level1);
         new_cores.push_back(std::make_pair(core0, uses_level1));
         obj_hashtable<expr> core_exprs, core1_exprs;
-        datalog::set_union(core_exprs, core0);
+        set_union(core_exprs, core0);
         for (unsigned i = 0; i < old_core.size(); ++i) {
             expr* lit = old_core[i].get();             
             if (core_exprs.contains(lit)) {
@@ -94,8 +94,8 @@ namespace pdr {
                 if (core1.size() < old_core.size()) {
                     new_cores.push_back(std::make_pair(core1, uses_level1));
                     core1_exprs.reset();
-                    datalog::set_union(core1_exprs, core1);
+                    set_union(core1_exprs, core1);
-                    datalog::set_intersection(core_exprs, core1_exprs);
+                    set_intersection(core_exprs, core1_exprs);
                 }
             }
         }

src/muz/spacer/CMakeLists.txt

@@ -7,7 +7,6 @@ z3_add_component(spacer
   spacer_farkas_learner.cpp
   spacer_generalizers.cpp
   spacer_manager.cpp
-  spacer_marshal.cpp
   spacer_prop_solver.cpp
   spacer_smt_context_manager.cpp
   spacer_sym_mux.cpp
@@ -15,11 +14,9 @@ z3_add_component(spacer
   spacer_itp_solver.cpp
   spacer_virtual_solver.cpp
   spacer_legacy_mbp.cpp
-  spacer_proof_utils.cpp
   spacer_unsat_core_learner.cpp
   spacer_unsat_core_plugin.cpp
   spacer_matrix.cpp
-  spacer_min_cut.cpp
   spacer_antiunify.cpp
   spacer_mev_array.cpp
   spacer_qe_project.cpp

src/muz/spacer/spacer_context.cpp

@@ -40,7 +40,7 @@ Notes:
 #include "ast/ast_smt2_pp.h"
 #include "ast/ast_ll_pp.h"
 #include "ast/ast_util.h"
-#include "ast/proof_checker/proof_checker.h"
+#include "ast/proofs/proof_checker.h"
 #include "smt/smt_value_sort.h"
 #include "ast/scoped_proof.h"
 #include "muz/spacer/spacer_qe_project.h"
@@ -2139,7 +2139,7 @@ void context::reset_lemma_generalizers()
 void context::init_lemma_generalizers(datalog::rule_set& rules)
 {
     reset_lemma_generalizers();
-    m.toggle_proof_mode(PGM_FINE);
+    m.toggle_proof_mode(PGM_ENABLED);
     smt_params &fparams = m_pm.fparams ();
     if (!m_params.spacer_eq_prop ()) {
         fparams.m_arith_bound_prop = BP_NONE;

src/muz/spacer/spacer_farkas_learner.cpp

@@ -31,7 +31,7 @@ Revision History:
 #include "muz/spacer/spacer_farkas_learner.h"
 #include "ast/rewriter/th_rewriter.h"
 #include "ast/ast_ll_pp.h"
-#include "muz/base/proof_utils.h"
+#include "ast/proofs/proof_utils.h"
 #include "ast/reg_decl_plugins.h"
 #include "smt/smt_farkas_util.h"
 
@@ -231,8 +231,8 @@ void farkas_learner::get_lemmas(proof* root, expr_set const& bs, expr_ref_vector
                     hyps = hyps2;
                 } else {
                     expr_set* hyps3 = alloc(expr_set);
-                    datalog::set_union(*hyps3, *hyps);
+                    set_union(*hyps3, *hyps);
-                    datalog::set_union(*hyps3, *hyps2);
+                    set_union(*hyps3, *hyps2);
                     hyps = hyps3;
                     hyprefs.push_back(hyps);
                 }
@@ -291,7 +291,7 @@ void farkas_learner::get_lemmas(proof* root, expr_set const& bs, expr_ref_vector
         case PR_LEMMA: {
             expr_set* hyps2 = alloc(expr_set);
             hyprefs.push_back(hyps2);
-            datalog::set_union(*hyps2, *hyps);
+            set_union(*hyps2, *hyps);
             hyps = hyps2;
             expr* fml = m.get_fact(p);
             hyps->remove(fml);

src/muz/spacer/spacer_itp_solver.h

@@ -135,7 +135,7 @@ public:
     virtual expr * get_assumption(unsigned idx) const
     {return m_solver.get_assumption(idx);}
     virtual std::ostream &display(std::ostream &out) const
-    {m_solver.display(out); return out;}
+    { return m_solver.display(out); }
 
     /* check_sat_result interface */
 
@@ -170,7 +170,7 @@ public:
     public:
         scoped_bg(itp_solver &s) : m_s(s), m_bg_sz(m_s.get_num_bg()) {}
         ~scoped_bg()
-        {if(m_s.get_num_bg() > m_bg_sz) { m_s.pop_bg(m_s.get_num_bg() - m_bg_sz); }}
+        {if (m_s.get_num_bg() > m_bg_sz) { m_s.pop_bg(m_s.get_num_bg() - m_bg_sz); }}
     };
 };
 }

src/muz/spacer/spacer_legacy_frames.cpp

@@ -23,9 +23,9 @@
 #include "ast/ast_smt2_pp.h"
 #include "ast/ast_ll_pp.h"
 #include "ast/ast_util.h"
-#include "ast/proof_checker/proof_checker.h"
+#include "ast/proofs/proof_checker.h"
 #include "smt/smt_value_sort.h"
-#include "muz/base/proof_utils.h"
+#include "ast/proofs/proof_utils.h"
 #include "ast/scoped_proof.h"
 #include "muz/spacer/spacer_qe_project.h"
 #include "tactic/core/blast_term_ite_tactic.h"

src/muz/spacer/spacer_min_cut.cpp

@@ -1,289 +0,0 @@
-/*++
-Copyright (c) 2017 Arie Gurfinkel
-
-Module Name:
-
-    spacer_min_cut.cpp
-
-Abstract:
-    min cut solver
-
-Author:
-    Bernhard Gleiss
-
-Revision History:
-
-
---*/
-#include "muz/spacer/spacer_min_cut.h"
-
-namespace spacer {
-
-    spacer_min_cut::spacer_min_cut()
-    {
-        m_n = 2;
-
-        // push back two empty vectors for source and sink
-        m_edges.push_back(vector<std::pair<unsigned, unsigned>>());
-        m_edges.push_back(vector<std::pair<unsigned, unsigned>>());
-    }
-
-    unsigned spacer_min_cut::new_node()
-    {
-        return m_n++;
-    }
-
-    void spacer_min_cut::add_edge(unsigned int i, unsigned int j, unsigned int capacity)
-    {
-        if (i >= m_edges.size())
-        {
-            m_edges.resize(i + 1);
-        }
-        m_edges[i].insert(std::make_pair(j, 1));
-        STRACE("spacer.mincut",
-               verbose_stream() << "adding edge (" << i << "," << j << ")\n";
-        );
-
-    }
-
-    void spacer_min_cut::compute_min_cut(vector<unsigned>& cut_nodes)
-    {
-        if (m_n == 2)
-        {
-            return;
-        }
-
-        m_d.resize(m_n);
-        m_pred.resize(m_n);
-
-        // compute initial distances and number of nodes
-        compute_initial_distances();
-
-        unsigned i = 0;
-
-        while (m_d[0] < m_n)
-        {
-            unsigned j = get_admissible_edge(i);
-
-            if (j < m_n)
-            {
-                // advance(i)
-                m_pred[j] = i;
-                i = j;
-
-                // if i is the sink, augment path
-                if (i == 1)
-                {
-                    augment_path();
-                    i = 0;
-                }
-            }
-            else
-            {
-                // retreat
-                compute_distance(i);
-                if (i != 0)
-                {
-                    i = m_pred[i];
-                }
-            }
-        }
-
-        // split nodes into reachable and unreachable ones
-        vector<bool> reachable(m_n);
-        compute_reachable_nodes(reachable);
-
-        // find all edges between reachable and unreachable nodes and for each such edge, add corresponding lemma to unsat-core
-        compute_cut_and_add_lemmas(reachable, cut_nodes);
-    }
-
-    void spacer_min_cut::compute_initial_distances()
-    {
-        vector<unsigned> todo;
-        vector<bool> visited(m_n);
-
-        todo.push_back(0); // start at the source, since we do postorder traversel
-
-        while (!todo.empty())
-        {
-            unsigned current = todo.back();
-
-            // if we haven't already visited current
-            if (!visited[current]) {
-                bool existsUnvisitedParent = false;
-
-                // add unprocessed parents to stack for DFS. If there is at least one unprocessed parent, don't compute the result
-                // for current now, but wait until those unprocessed parents are processed.
-                for (unsigned i = 0, sz = m_edges[current].size(); i < sz; ++i)
-                {
-                    unsigned parent = m_edges[current][i].first;
-
-                    // if we haven't visited the current parent yet
-                    if(!visited[parent])
-                    {
-                        // add it to the stack
-                        todo.push_back(parent);
-                        existsUnvisitedParent = true;
-                    }
-                }
-
-                // if we already visited all parents, we can visit current too
-                if (!existsUnvisitedParent) {
-                    visited[current] = true;
-                    todo.pop_back();
-
-                    compute_distance(current); // I.H. all parent distances are already computed
-                }
-            }
-            else {
-                todo.pop_back();
-            }
-        }
-    }
-
-    unsigned spacer_min_cut::get_admissible_edge(unsigned i)
-    {
-        for (const auto& pair : m_edges[i])
-        {
-            if (pair.second > 0 && m_d[i] == m_d[pair.first] + 1)
-            {
-                return pair.first;
-            }
-        }
-        return m_n; // no element found
-    }
-
-    void spacer_min_cut::augment_path()
-    {
-        // find bottleneck capacity
-        unsigned max = std::numeric_limits<unsigned int>::max();
-        unsigned k = 1;
-        while (k != 0)
-        {
-            unsigned l = m_pred[k];
-            for (const auto& pair : m_edges[l])
-            {
-                if (pair.first == k)
-                {
-                    if (max > pair.second)
-                    {
-                        max = pair.second;
-                    }
-                }
-            }
-            k = l;
-        }
-
-        k = 1;
-        while (k != 0)
-        {
-            unsigned l = m_pred[k];
-
-            // decrease capacity
-            for (auto& pair : m_edges[l])
-            {
-                if (pair.first == k)
-                {
-                    pair.second -= max;
-                }
-            }
-            // increase reverse flow
-            bool already_exists = false;
-            for (auto& pair : m_edges[k])
-            {
-                if (pair.first == l)
-                {
-                    already_exists = true;
-                    pair.second += max;
-                }
-            }
-            if (!already_exists)
-            {
-                m_edges[k].insert(std::make_pair(l, max));
-            }
-            k = l;
-        }
-    }
-
-    void spacer_min_cut::compute_distance(unsigned i)
-    {
-        if (i == 1) // sink node
-        {
-            m_d[1] = 0;
-        }
-        else
-        {
-            unsigned min = std::numeric_limits<unsigned int>::max();
-
-            // find edge (i,j) with positive residual capacity and smallest distance
-            for (const auto& pair : m_edges[i])
-            {
-                if (pair.second > 0)
-                {
-                    unsigned tmp = m_d[pair.first] + 1;
-                    if (tmp < min)
-                    {
-                        min = tmp;
-                    }
-                }
-            }
-            m_d[i] = min;
-        }
-    }
-
-    void spacer_min_cut::compute_reachable_nodes(vector<bool>& reachable)
-    {
-        vector<unsigned> todo;
-
-        todo.push_back(0);
-        while (!todo.empty())
-        {
-            unsigned current = todo.back();
-            todo.pop_back();
-
-            if (!reachable[current])
-            {
-                reachable[current] = true;
-
-                for (const auto& pair : m_edges[current])
-                {
-                    if (pair.second > 0)
-                    {
-                        todo.push_back(pair.first);
-                    }
-                }
-            }
-        }
-    }
-
-    void spacer_min_cut::compute_cut_and_add_lemmas(vector<bool>& reachable, vector<unsigned>& cut_nodes)
-    {
-        vector<unsigned> todo;
-        vector<bool> visited(m_n);
-
-        todo.push_back(0);
-        while (!todo.empty())
-        {
-            unsigned current = todo.back();
-            todo.pop_back();
-
-            if (!visited[current])
-            {
-                visited[current] = true;
-
-                for (const auto& pair : m_edges[current])
-                {
-                    unsigned successor = pair.first;
-                    if (reachable[successor])
-                    {
-                        todo.push_back(successor);
-                    }
-                    else
-                    {
-                        cut_nodes.push_back(successor);
-                    }
-                }
-            }
-        }
-    }
-}

src/muz/spacer/spacer_min_cut.h

@@ -1,53 +0,0 @@
-/*++
-Copyright (c) 2017 Arie Gurfinkel
-
-Module Name:
-
-    spacer_min_cut.h
-
-Abstract:
-    min cut solver
-
-Author:
-    Bernhard Gleiss
-
-Revision History:
-
-
---*/
-
-#ifndef _SPACER_MIN_CUT_H_
-#define _SPACER_MIN_CUT_H_
-
-#include "ast/ast.h"
-#include "util/vector.h"
-
-namespace spacer {
-
-    class spacer_min_cut {
-    public:
-        spacer_min_cut();
-
-        unsigned new_node();
-        void add_edge(unsigned i, unsigned j, unsigned capacity);
-        void compute_min_cut(vector<unsigned>& cut_nodes);
-
-    private:
-
-        unsigned m_n; // number of vertices in the graph
-
-        vector<vector<std::pair<unsigned, unsigned> > > m_edges; // map from node to all outgoing edges together with their weights (also contains "reverse edges")
-        vector<unsigned> m_d; // approximation of distance from node to sink in residual graph
-        vector<unsigned> m_pred; // predecessor-information for reconstruction of augmenting path
-        vector<expr*> m_node_to_formula; // maps each node to the corresponding formula in the original proof
-
-        void compute_initial_distances();
-        unsigned get_admissible_edge(unsigned i);
-        void augment_path();
-        void compute_distance(unsigned i);
-        void compute_reachable_nodes(vector<bool>& reachable);
-        void compute_cut_and_add_lemmas(vector<bool>& reachable, vector<unsigned>& cut_nodes);
-    };
-}
-
-#endif

src/muz/spacer/spacer_proof_utils.cpp

@@ -1,332 +0,0 @@
-/*++
-Copyright (c) 2017 Arie Gurfinkel
-
-Module Name:
-
-    spacer_proof_utils.cpp
-
-Abstract:
-    Utilities to traverse and manipulate proofs
-
-Author:
-    Bernhard Gleiss
-    Arie Gurfinkel
-
-Revision History:
-
---*/
-
-#include "muz/spacer/spacer_proof_utils.h"
-#include "ast/ast_util.h"
-#include "ast/ast_pp.h"
-
-#include "ast/proof_checker/proof_checker.h"
-
-namespace spacer {
-
-ProofIteratorPostOrder::ProofIteratorPostOrder(proof* root, ast_manager& manager) : m(manager)
-{m_todo.push_back(root);}
-
-bool ProofIteratorPostOrder::hasNext()
-{return !m_todo.empty();}
-
-/*
- * iterative post-order depth-first search (DFS) through the proof DAG
- */
-proof* ProofIteratorPostOrder::next()
-{
-    while (!m_todo.empty()) {
-        proof* currentNode = m_todo.back();
-
-        // if we haven't already visited the current unit
-        if (!m_visited.is_marked(currentNode)) {
-            bool existsUnvisitedParent = false;
-
-            // add unprocessed premises to stack for DFS. If there is at least one unprocessed premise, don't compute the result
-            // for currentProof now, but wait until those unprocessed premises are processed.
-            for (unsigned i = 0; i < m.get_num_parents(currentNode); ++i) {
-                SASSERT(m.is_proof(currentNode->get_arg(i)));
-                proof* premise = to_app(currentNode->get_arg(i));
-
-                // if we haven't visited the current premise yet
-                if (!m_visited.is_marked(premise)) {
-                    // add it to the stack
-                    m_todo.push_back(premise);
-                    existsUnvisitedParent = true;
-                }
-            }
-
-            // if we already visited all parent-inferences, we can visit the inference too
-            if (!existsUnvisitedParent) {
-                m_visited.mark(currentNode, true);
-                m_todo.pop_back();
-                return currentNode;
-            }
-        } else {
-            m_todo.pop_back();
-        }
-    }
-    // we have already iterated through all inferences
-    return NULL;
-}
-
-
-class reduce_hypotheses {
-    ast_manager &m;
-    // tracking all created expressions
-    expr_ref_vector m_pinned;
-
-    // cache for the transformation
-    obj_map<proof, proof*> m_cache;
-
-    // map from unit literals to their hypotheses-free derivations
-    obj_map<expr, proof*> m_units;
-
-    // -- all hypotheses in the the proof
-    obj_hashtable<expr> m_hyps;
-
-    // marks hypothetical proofs
-    ast_mark m_hypmark;
-
-
-    // stack
-    ptr_vector<proof> m_todo;
-
-    void reset()
-    {
-        m_cache.reset();
-        m_units.reset();
-        m_hyps.reset();
-        m_hypmark.reset();
-        m_pinned.reset();
-    }
-
-    bool compute_mark1(proof *pr)
-    {
-        bool hyp_mark = false;
-        // lemmas clear all hypotheses
-        if (!m.is_lemma(pr)) {
-            for (unsigned i = 0, sz = m.get_num_parents(pr); i < sz; ++i) {
-                if (m_hypmark.is_marked(m.get_parent(pr, i))) {
-                    hyp_mark = true;
-                    break;
-                }
-            }
-        }
-        m_hypmark.mark(pr, hyp_mark);
-        return hyp_mark;
-    }
-
-    void compute_marks(proof* pr)
-    {
-        proof *p;
-        ProofIteratorPostOrder pit(pr, m);
-        while (pit.hasNext()) {
-            p = pit.next();
-            if (m.is_hypothesis(p)) {
-                m_hypmark.mark(p, true);
-                m_hyps.insert(m.get_fact(p));
-            } else {
-                bool hyp_mark = compute_mark1(p);
-                // collect units that are hyp-free and are used as hypotheses somewhere
-                if (!hyp_mark && m.has_fact(p) && m_hyps.contains(m.get_fact(p)))
-                { m_units.insert(m.get_fact(p), p); }
-            }
-        }
-    }
-    void find_units(proof *pr)
-    {
-        // optional. not implemented yet.
-    }
-
-    void reduce(proof* pf, proof_ref &out)
-    {
-        proof *res = NULL;
-
-        m_todo.reset();
-        m_todo.push_back(pf);
-        ptr_buffer<proof> args;
-        bool dirty = false;
-
-        while (!m_todo.empty()) {
-            proof *p, *tmp, *pp;
-            unsigned todo_sz;
-
-            p = m_todo.back();
-            if (m_cache.find(p, tmp)) {
-                res = tmp;
-                m_todo.pop_back();
-                continue;
-            }
-
-            dirty = false;
-            args.reset();
-            todo_sz = m_todo.size();
-            for (unsigned i = 0, sz = m.get_num_parents(p); i < sz; ++i) {
-                pp = m.get_parent(p, i);
-                if (m_cache.find(pp, tmp)) {
-                    args.push_back(tmp);
-                    dirty = dirty || pp != tmp;
-                } else {
-                    m_todo.push_back(pp);
-                }
-            }
-
-            if (todo_sz < m_todo.size()) { continue; }
-            else { m_todo.pop_back(); }
-
-            if (m.is_hypothesis(p)) {
-                // hyp: replace by a corresponding unit
-                if (m_units.find(m.get_fact(p), tmp)) {
-                    res = tmp;
-                } else { res = p; }
-            }
-
-            else if (!dirty) { res = p; }
-
-            else if (m.is_lemma(p)) {
-                //lemma: reduce the premise; remove reduced consequences from conclusion
-                SASSERT(args.size() == 1);
-                res = mk_lemma_core(args.get(0), m.get_fact(p));
-                compute_mark1(res);
-            } else if (m.is_unit_resolution(p)) {
-                // unit: reduce untis; reduce the first premise; rebuild unit resolution
-                res = mk_unit_resolution_core(args.size(), args.c_ptr());
-                compute_mark1(res);
-            } else  {
-                // other: reduce all premises; reapply
-                if (m.has_fact(p)) { args.push_back(to_app(m.get_fact(p))); }
-                SASSERT(p->get_decl()->get_arity() == args.size());
-                res = m.mk_app(p->get_decl(), args.size(), (expr * const*)args.c_ptr());
-                m_pinned.push_back(res);
-                compute_mark1(res);
-            }
-
-            SASSERT(res);
-            m_cache.insert(p, res);
-
-            if (m.has_fact(res) && m.is_false(m.get_fact(res))) { break; }
-        }
-
-        out = res;
-    }
-
-    // returns true if (hypothesis (not a)) would be reduced
-    bool is_reduced(expr *a)
-    {
-        expr_ref e(m);
-        if (m.is_not(a)) { e = to_app(a)->get_arg(0); }
-        else { e = m.mk_not(a); }
-
-        return m_units.contains(e);
-    }
-    proof *mk_lemma_core(proof *pf, expr *fact)
-    {
-        ptr_buffer<expr> args;
-        expr_ref lemma(m);
-
-        if (m.is_or(fact)) {
-            for (unsigned i = 0, sz = to_app(fact)->get_num_args(); i < sz; ++i) {
-                expr *a = to_app(fact)->get_arg(i);
-                if (!is_reduced(a))
-                { args.push_back(a); }
-            }
-        } else if (!is_reduced(fact))
-        { args.push_back(fact); }
-
-
-        if (args.size() == 0) { return pf; }
-        else if (args.size() == 1) {
-            lemma = args.get(0);
-        } else {
-            lemma = m.mk_or(args.size(), args.c_ptr());
-        }
-        proof* res = m.mk_lemma(pf, lemma);
-        m_pinned.push_back(res);
-
-        if (m_hyps.contains(lemma))
-        { m_units.insert(lemma, res); }
-        return res;
-    }
-
-    proof *mk_unit_resolution_core(unsigned num_args, proof* const *args)
-    {
-
-        ptr_buffer<proof> pf_args;
-        pf_args.push_back(args [0]);
-
-        app *cls_fact = to_app(m.get_fact(args[0]));
-        ptr_buffer<expr> cls;
-        if (m.is_or(cls_fact)) {
-            for (unsigned i = 0, sz = cls_fact->get_num_args(); i < sz; ++i)
-            { cls.push_back(cls_fact->get_arg(i)); }
-        } else { cls.push_back(cls_fact); }
-
-        // construct new resovent
-        ptr_buffer<expr> new_fact_cls;
-        bool found;
-        // XXX quadratic
-        for (unsigned i = 0, sz = cls.size(); i < sz; ++i) {
-            found = false;
-            for (unsigned j = 1; j < num_args; ++j) {
-                if (m.is_complement(cls.get(i), m.get_fact(args [j]))) {
-                    found = true;
-                    pf_args.push_back(args [j]);
-                    break;
-                }
-            }
-            if (!found) {
-                new_fact_cls.push_back(cls.get(i));
-            }
-        }
-
-        SASSERT(new_fact_cls.size() + pf_args.size() - 1 == cls.size());
-        expr_ref new_fact(m);
-        new_fact = mk_or(m, new_fact_cls.size(), new_fact_cls.c_ptr());
-
-        // create new proof step
-        proof *res = m.mk_unit_resolution(pf_args.size(), pf_args.c_ptr(), new_fact);
-        m_pinned.push_back(res);
-        return res;
-    }
-
-    // reduce all units, if any unit reduces to false return true and put its proof into out
-    bool reduce_units(proof_ref &out)
-    {
-        proof_ref res(m);
-        for (auto entry : m_units) {
-            reduce(entry.get_value(), res);
-            if (m.is_false(m.get_fact(res))) {
-                out = res;
-                return true;
-            }
-            res.reset();
-        }
-        return false;
-    }
-
-
-public:
-    reduce_hypotheses(ast_manager &m) : m(m), m_pinned(m) {}
-
-
-    void operator()(proof_ref &pr)
-    {
-        compute_marks(pr);
-        if (!reduce_units(pr)) {
-            reduce(pr.get(), pr);
-        }
-        reset();
-    }
-};
-void reduce_hypotheses(proof_ref &pr)
-{
-    ast_manager &m = pr.get_manager();
-    class reduce_hypotheses hypred(m);
-    hypred(pr);
-    DEBUG_CODE(proof_checker pc(m);
-               expr_ref_vector side(m);
-               SASSERT(pc.check(pr, side));
-              );
-}
-}

src/muz/spacer/spacer_proof_utils.h

@@ -1,43 +0,0 @@
-/*++
-Copyright (c) 2017 Arie Gurfinkel
-
-Module Name:
-
-    spacer_proof_utils.cpp
-
-Abstract:
-    Utilities to traverse and manipulate proofs
-
-Author:
-    Bernhard Gleiss
-    Arie Gurfinkel
-
-Revision History:
-
---*/
-
-#ifndef _SPACER_PROOF_UTILS_H_
-#define _SPACER_PROOF_UTILS_H_
-#include "ast/ast.h"
-
-namespace spacer {
-/*
- * iterator, which traverses the proof in depth-first post-order.
- */
-class ProofIteratorPostOrder {
-public:
-    ProofIteratorPostOrder(proof* refutation, ast_manager& manager);
-    bool hasNext();
-    proof* next();
-
-private:
-    ptr_vector<proof> m_todo;
-    ast_mark m_visited; // the proof nodes we have already visited
-
-    ast_manager& m;
-};
-
-
-void reduce_hypotheses(proof_ref &pr);
-}
-#endif

src/muz/spacer/spacer_unsat_core_learner.cpp

@@ -41,7 +41,7 @@ void unsat_core_learner::compute_unsat_core(proof *root, expr_set& asserted_b, e
     // transform proof in order to get a proof which is better suited for unsat-core-extraction
     proof_ref pr(root, m);
 
-    spacer::reduce_hypotheses(pr);
+    reduce_hypotheses(pr);
     STRACE("spacer.unsat_core_learner",
            verbose_stream() << "Reduced proof:\n" << mk_ismt2_pp(pr, m) << "\n";
     );
@@ -50,7 +50,7 @@ void unsat_core_learner::compute_unsat_core(proof *root, expr_set& asserted_b, e
     collect_symbols_b(asserted_b);
 
     // traverse proof
-    ProofIteratorPostOrder it(root, m);
+    proof_post_order it(root, m);
     while (it.hasNext())
     {
         proof* currentNode = it.next();
@@ -138,7 +138,7 @@ void unsat_core_learner::compute_unsat_core(proof *root, expr_set& asserted_b, e
         std::unordered_map<unsigned, unsigned> id_to_small_id;
         unsigned counter = 0;
 
-        ProofIteratorPostOrder it2(root, m);
+        proof_post_order it2(root, m);
         while (it2.hasNext())
         {
             proof* currentNode = it2.next();

src/muz/spacer/spacer_unsat_core_learner.h

@@ -20,7 +20,7 @@ Revision History:
 
 #include "ast/ast.h"
 #include "muz/spacer/spacer_util.h"
-#include "muz/spacer/spacer_proof_utils.h"
+#include "ast/proofs/proof_utils.h"
 
 namespace spacer {
 

src/muz/spacer/spacer_unsat_core_plugin.cpp

@@ -20,13 +20,13 @@ Revision History:
 
 #include "ast/rewriter/bool_rewriter.h"
 #include "ast/arith_decl_plugin.h"
+#include "ast/proofs/proof_utils.h"
 
 #include "solver/solver.h"
 
 #include "smt/smt_farkas_util.h"
 #include "smt/smt_solver.h"
 
-#include "muz/spacer/spacer_proof_utils.h"
 #include "muz/spacer/spacer_matrix.h"
 #include "muz/spacer/spacer_unsat_core_plugin.h"
 #include "muz/spacer/spacer_unsat_core_learner.h"
@@ -735,7 +735,7 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector<rat
                 m_node_to_formula[node_other] = m.get_fact(i);
                 m_node_to_formula[node_i] = m.get_fact(i);
 
-                m_min_cut.add_edge(node_other, node_i, 1);
+                m_min_cut.add_edge(node_other, node_i);
             }
         }
 
@@ -765,12 +765,12 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector<rat
                 m_node_to_formula[node_j] = m.get_fact(j);
                 m_node_to_formula[node_other] = m.get_fact(j);
 
-                m_min_cut.add_edge(node_j, node_other, 1);
+                m_min_cut.add_edge(node_j, node_other);
             }
         }
 
         // finally connect nodes
-        m_min_cut.add_edge(node_i, node_j, 1);
+        m_min_cut.add_edge(node_i, node_j);
     }
 
     /*
@@ -779,7 +779,7 @@ void unsat_core_plugin_farkas_lemma::compute_linear_combination(const vector<rat
      */
     void unsat_core_plugin_min_cut::finalize()
     {
-        vector<unsigned int> cut_nodes;
+        unsigned_vector cut_nodes;
         m_min_cut.compute_min_cut(cut_nodes);
 
         for (unsigned cut_node : cut_nodes)

src/muz/spacer/spacer_unsat_core_plugin.h

@@ -19,7 +19,7 @@ Revision History:
 #define _SPACER_UNSAT_CORE_PLUGIN_H_
 
 #include "ast/ast.h"
-#include "muz/spacer/spacer_min_cut.h"
+#include "util/min_cut.h"
 
 namespace spacer {
 
@@ -109,7 +109,7 @@ private:
 
         vector<expr*> m_node_to_formula; // maps each node to the corresponding formula in the original proof
 
-        spacer_min_cut m_min_cut;
+        min_cut m_min_cut;
     };
 }
 #endif

src/muz/spacer/spacer_util.cpp

@@ -72,73 +72,67 @@ namespace spacer {
     //
 
     model_evaluator_util::model_evaluator_util(ast_manager& m) :
-        m(m), m_mev(NULL)
+        m(m), m_mev(nullptr) { 
-    { reset (NULL); }
+        reset (nullptr); 
+    }
 
     model_evaluator_util::~model_evaluator_util() {reset (NULL);}
 
 
-void model_evaluator_util::reset(model* model)
+    void model_evaluator_util::reset(model* model) {
-{
         if (m_mev) {
             dealloc(m_mev);
             m_mev = NULL;
         }
         m_model = model;
-    if (!m_model) { return; }
+        if (!m_model) { return; }
         m_mev = alloc(model_evaluator, *m_model);
     }
-
+    
-bool model_evaluator_util::eval(expr *e, expr_ref &result, bool model_completion)
+    bool model_evaluator_util::eval(expr *e, expr_ref &result, bool model_completion) {
-{
         m_mev->set_model_completion (model_completion);
         try {
             m_mev->operator() (e, result);
             return true;
-        } catch (model_evaluator_exception &ex) {
+        } 
+        catch (model_evaluator_exception &ex) {
             (void)ex;
             TRACE("spacer_model_evaluator", tout << ex.msg () << "\n";);
             return false;
         }
     }
-
+    
     bool model_evaluator_util::eval(const expr_ref_vector &v,
-                                expr_ref& res, bool model_completion)
+                                    expr_ref& res, bool model_completion) {
-{
         expr_ref e(m);
         e = mk_and (v);
         return eval(e, res, model_completion);
     }
-
+    
-
+    
-bool model_evaluator_util::is_true(const expr_ref_vector &v)
+    bool model_evaluator_util::is_true(const expr_ref_vector &v) {
-{
         expr_ref res(m);
         return eval (v, res, false) && m.is_true (res);
     }
-
+    
-bool model_evaluator_util::is_false(expr *x)
+    bool model_evaluator_util::is_false(expr *x) {
-{
         expr_ref res(m);
         return eval(x, res, false) && m.is_false (res);
     }
-bool model_evaluator_util::is_true(expr *x)
+
-{
+    bool model_evaluator_util::is_true(expr *x) {
         expr_ref res(m);
         return eval(x, res, false) && m.is_true (res);
     }
-
+    
-
+    void reduce_disequalities(model& model, unsigned threshold, expr_ref& fml) {
-void reduce_disequalities(model& model, unsigned threshold, expr_ref& fml)
-{
         ast_manager& m = fml.get_manager();
         expr_ref_vector conjs(m);
         flatten_and(fml, conjs);
         obj_map<expr, unsigned> diseqs;
         expr* n, *lhs, *rhs;
         for (unsigned i = 0; i < conjs.size(); ++i) {
-            if (m.is_not(conjs[i].get(), n) &&
+            if (m.is_not(conjs[i].get(), n) && m.is_eq(n, lhs, rhs)) {
-                m.is_eq(n, lhs, rhs)) {
                 if (!m.is_value(rhs)) {
                     std::swap(lhs, rhs);
                 }
@@ -155,14 +149,12 @@ void reduce_disequalities(model& model, unsigned threshold, expr_ref& fml)
         expr_ref val(m), tmp(m);
         proof_ref pr(m);
         pr = m.mk_asserted(m.mk_true());
-        obj_map<expr, unsigned>::iterator it  = diseqs.begin();
+        for (auto const& kv : diseqs) {
-        obj_map<expr, unsigned>::iterator end = diseqs.end();
+            if (kv.m_value >= threshold) {
-        for (; it != end; ++it) {
+                model.eval(kv.m_key, val);
-            if (it->m_value >= threshold) {
+                sub.insert(kv.m_key, val, pr);
-                model.eval(it->m_key, val);
+                conjs.push_back(m.mk_eq(kv.m_key, val));
-                sub.insert(it->m_key, val, pr);
+                num_deleted += kv.m_value;
-                conjs.push_back(m.mk_eq(it->m_key, val));
-                num_deleted += it->m_value;
             }
         }
         if (orig_size < conjs.size()) {
@@ -178,14 +170,17 @@ void reduce_disequalities(model& model, unsigned threshold, expr_ref& fml)
                     SASSERT(orig_size <= 1 + conjs.size());
                     if (i + 1 == orig_size) {
                         // no-op.
-                } else if (orig_size <= conjs.size()) {
+                    } 
+                    else if (orig_size <= conjs.size()) {
                         // no-op
-                } else {
+                    } 
+                    else {
                         SASSERT(orig_size == 1 + conjs.size());
                         --orig_size;
                         --i;
                     }
-            } else {
+                } 
+                else {
                     conjs[i] = tmp;
                 }
             }
@@ -202,9 +197,8 @@ void reduce_disequalities(model& model, unsigned threshold, expr_ref& fml)
         ast_manager& m;
     public:
         ite_hoister(ast_manager& m): m(m) {}
-
+        
-    br_status mk_app_core(func_decl* f, unsigned num_args, expr* const* args, expr_ref& result)
+        br_status mk_app_core(func_decl* f, unsigned num_args, expr* const* args, expr_ref& result) {
-    {
             if (m.is_ite(f)) {
                 return BR_FAILED;
             }
@@ -233,13 +227,12 @@ void reduce_disequalities(model& model, unsigned threshold, expr_ref& fml)
     struct ite_hoister_cfg: public default_rewriter_cfg {
         ite_hoister m_r;
         bool rewrite_patterns() const { return false; }
-    br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr)
+        br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
-    {
             return m_r.mk_app_core(f, num, args, result);
         }
         ite_hoister_cfg(ast_manager & m, params_ref const & p):m_r(m) {}
     };
-
+    
     class ite_hoister_star : public rewriter_tpl<ite_hoister_cfg> {
         ite_hoister_cfg m_cfg;
     public:
@@ -247,9 +240,8 @@ void reduce_disequalities(model& model, unsigned threshold, expr_ref& fml)
             rewriter_tpl<ite_hoister_cfg>(m, false, m_cfg),
             m_cfg(m, p) {}
     };
-
+    
-void hoist_non_bool_if(expr_ref& fml)
+    void hoist_non_bool_if(expr_ref& fml) {
-{
         ast_manager& m = fml.get_manager();
         scoped_no_proof _sp(m);
         params_ref p;
@@ -266,8 +258,7 @@ void hoist_non_bool_if(expr_ref& fml)
         bool m_is_dl;
         bool m_test_for_utvpi;
 
-    bool is_numeric(expr* e) const
+        bool is_numeric(expr* e) const {
-    {
             if (a.is_numeral(e)) {
                 return true;
             }
@@ -278,13 +269,11 @@ void hoist_non_bool_if(expr_ref& fml)
             return false;
         }
 
-    bool is_arith_expr(expr *e) const
+        bool is_arith_expr(expr *e) const {
-    {
             return is_app(e) && a.get_family_id() == to_app(e)->get_family_id();
         }
-
+        
-    bool is_offset(expr* e) const
+        bool is_offset(expr* e) const {
-    {
             if (a.is_numeral(e)) {
                 return true;
             }
@@ -315,47 +304,44 @@ void hoist_non_bool_if(expr_ref& fml)
             return !is_arith_expr(e);
         }
 
-    bool is_minus_one(expr const * e) const
+        bool is_minus_one(expr const * e) const {
-    {
+            rational r;
-        rational r;
+            return a.is_numeral(e, r) && r.is_minus_one();
-        return a.is_numeral(e, r) && r.is_minus_one();
         }
 
-    bool test_ineq(expr* e) const
+        bool test_ineq(expr* e) const {
-    {
             SASSERT(a.is_le(e) || a.is_ge(e) || m.is_eq(e));
             SASSERT(to_app(e)->get_num_args() == 2);
             expr * lhs = to_app(e)->get_arg(0);
             expr * rhs = to_app(e)->get_arg(1);
             if (is_offset(lhs) && is_offset(rhs))
-        { return true; }
+                { return true; }
             if (!is_numeric(rhs))
-        { std::swap(lhs, rhs); }
+                { std::swap(lhs, rhs); }
             if (!is_numeric(rhs))
-        { return false; }
+                { return false; }
             // lhs can be 'x' or '(+ x (* -1 y))'
             if (is_offset(lhs))
-        { return true; }
+                { return true; }
             expr* arg1, *arg2;
             if (!a.is_add(lhs, arg1, arg2))
-        { return false; }
+                { return false; }
             // x
             if (m_test_for_utvpi) {
                 return is_offset(arg1) && is_offset(arg2);
             }
             if (is_arith_expr(arg1))
-        { std::swap(arg1, arg2); }
+                { std::swap(arg1, arg2); }
             if (is_arith_expr(arg1))
-        { return false; }
+                { return false; }
             // arg2: (* -1 y)
             expr* m1, *m2;
             if (!a.is_mul(arg2, m1, m2))
-        { return false; }
+                { return false; }
             return is_minus_one(m1) && is_offset(m2);
         }
 
-    bool test_eq(expr* e) const
+        bool test_eq(expr* e) const {
-    {
             expr* lhs, *rhs;
             VERIFY(m.is_eq(e, lhs, rhs));
             if (!a.is_int_real(lhs)) {
@@ -370,9 +356,8 @@ void hoist_non_bool_if(expr_ref& fml)
                 !a.is_mul(lhs) &&
                 !a.is_mul(rhs);
         }
-
+        
-    bool test_term(expr* e) const
+        bool test_term(expr* e) const {
-    {
             if (m.is_bool(e)) {
                 return true;
             }
@@ -490,7 +475,7 @@ bool is_utvpi_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls)
      * eliminate simple equalities using qe_lite
      * then, MBP for Booleans (substitute), reals (based on LW), ints (based on Cooper), and arrays
      */
-    void qe_project (ast_manager& m, app_ref_vector& vars, expr_ref& fml,
+void qe_project (ast_manager& m, app_ref_vector& vars, expr_ref& fml,
                      const model_ref& M, bool reduce_all_selects, bool use_native_mbp,
                 bool dont_sub)
 {

src/muz/spacer/spacer_virtual_solver.cpp

@@ -23,7 +23,8 @@ Notes:
 #include "muz/spacer/spacer_util.h"
 #include "ast/rewriter/bool_rewriter.h"
 
-#include "ast/proof_checker/proof_checker.h"
+#include "ast/proofs/proof_checker.h"
+#include "ast/proofs/proof_utils.h"
 
 #include "ast/scoped_proof.h"
 
@@ -64,172 +65,11 @@ virtual_solver::~virtual_solver()
 }
 
 namespace {
-static bool matches_fact(expr_ref_vector &args, expr* &match)
-{
-    ast_manager &m = args.get_manager();
-    expr *fact = args.back();
-    for (unsigned i = 0, sz = args.size() - 1; i < sz; ++i) {
-        expr *arg = args.get(i);
-        if (m.is_proof(arg) &&
-                m.has_fact(to_app(arg)) &&
-                m.get_fact(to_app(arg)) == fact) {
-            match = arg;
-            return true;
-        }
-    }
-    return false;
-}
 
 
-class elim_aux_assertions {
+// TBD: move to ast/proofs/elim_aux_assertions
-    app_ref m_aux;
-public:
-    elim_aux_assertions(app_ref aux) : m_aux(aux) {}
 
-    void mk_or_core(expr_ref_vector &args, expr_ref &res)
-    {
-        ast_manager &m = args.get_manager();
-        unsigned j = 0;
-        for (unsigned i = 0, sz = args.size(); i < sz; ++i) {
-            if (m.is_false(args.get(i))) { continue; }
-            if (i != j) { args [j] = args.get(i); }
-            ++j;
-        }
-        SASSERT(j >= 1);
-        res = j > 1 ? m.mk_or(j, args.c_ptr()) : args.get(0);
-    }
 
-    void mk_app(func_decl *decl, expr_ref_vector &args, expr_ref &res)
-    {
-        ast_manager &m = args.get_manager();
-        bool_rewriter brwr(m);
-
-        if (m.is_or(decl))
-        { mk_or_core(args, res); }
-        else if (m.is_iff(decl) && args.size() == 2)
-            // avoiding simplifying equalities. In particular,
-            // we don't want (= (not a) (not b)) to be reduced to (= a b)
-        { res = m.mk_iff(args.get(0), args.get(1)); }
-        else
-        { brwr.mk_app(decl, args.size(), args.c_ptr(), res); }
-    }
-
-    void operator()(ast_manager &m, proof *pr, proof_ref &res)
-    {
-        DEBUG_CODE(proof_checker pc(m);
-                   expr_ref_vector side(m);
-                   SASSERT(pc.check(pr, side));
-                  );
-        obj_map<app, app*> cache;
-        bool_rewriter brwr(m);
-
-        // for reference counting of new proofs
-        app_ref_vector pinned(m);
-
-        ptr_vector<app> todo;
-        todo.push_back(pr);
-
-        expr_ref not_aux(m);
-        not_aux = m.mk_not(m_aux);
-
-        expr_ref_vector args(m);
-
-        while (!todo.empty()) {
-            app *p, *r;
-            expr *a;
-
-            p = todo.back();
-            if (cache.find(pr, r)) {
-                todo.pop_back();
-                continue;
-            }
-
-            SASSERT(!todo.empty() || pr == p);
-            bool dirty = false;
-            unsigned todo_sz = todo.size();
-            args.reset();
-            for (unsigned i = 0, sz = p->get_num_args(); i < sz; ++i) {
-                expr* arg = p->get_arg(i);
-                if (arg == m_aux.get()) {
-                    dirty = true;
-                    args.push_back(m.mk_true());
-                } else if (arg == not_aux.get()) {
-                    dirty = true;
-                    args.push_back(m.mk_false());
-                }
-                // skip (asserted m_aux)
-                else if (m.is_asserted(arg, a) && a == m_aux.get()) {
-                    dirty = true;
-                }
-                // skip (hypothesis m_aux)
-                else if (m.is_hypothesis(arg, a) && a == m_aux.get()) {
-                    dirty = true;
-                } else if (is_app(arg) && cache.find(to_app(arg), r)) {
-                    dirty |= (arg != r);
-                    args.push_back(r);
-                } else if (is_app(arg))
-                { todo.push_back(to_app(arg)); }
-                else
-                    // -- not an app
-                { args.push_back(arg); }
-
-            }
-            if (todo_sz < todo.size()) {
-                // -- process parents
-                args.reset();
-                continue;
-            }
-
-            // ready to re-create
-            app_ref newp(m);
-            if (!dirty) { newp = p; }
-            else if (m.is_unit_resolution(p)) {
-                if (args.size() == 2)
-                    // unit resolution with m_aux that got collapsed to nothing
-                { newp = to_app(args.get(0)); }
-                else {
-                    ptr_vector<proof> parents;
-                    for (unsigned i = 0, sz = args.size() - 1; i < sz; ++i)
-                    { parents.push_back(to_app(args.get(i))); }
-                    SASSERT(parents.size() == args.size() - 1);
-                    newp = m.mk_unit_resolution(parents.size(), parents.c_ptr());
-                    // XXX the old and new facts should be
-                    // equivalent. The test here is much
-                    // stronger. It might need to be relaxed.
-                    SASSERT(m.get_fact(newp) == args.back());
-                    pinned.push_back(newp);
-                }
-            } else if (matches_fact(args, a)) {
-                newp = to_app(a);
-            } else {
-                expr_ref papp(m);
-                mk_app(p->get_decl(), args, papp);
-                newp = to_app(papp.get());
-                pinned.push_back(newp);
-            }
-            cache.insert(p, newp);
-            todo.pop_back();
-            CTRACE("virtual",
-                   p->get_decl_kind() == PR_TH_LEMMA &&
-                   p->get_decl()->get_parameter(0).get_symbol() == "arith" &&
-                   p->get_decl()->get_num_parameters() > 1 &&
-                   p->get_decl()->get_parameter(1).get_symbol() == "farkas",
-                   tout << "Old pf: " << mk_pp(p, m) << "\n"
-                   << "New pf: " << mk_pp(newp, m) << "\n";);
-        }
-
-        proof *r;
-        VERIFY(cache.find(pr, r));
-
-        DEBUG_CODE(
-            proof_checker pc(m);
-            expr_ref_vector side(m);
-            SASSERT(pc.check(r, side));
-        );
-
-        res = r ;
-    }
-};
 }
 
 proof *virtual_solver::get_proof()

src/muz/spacer/spacer_virtual_solver.h

@@ -92,7 +92,6 @@ public:
     virtual bool get_produce_models();
     virtual smt_params &fparams();
     virtual void reset();
-
     virtual void set_progress_callback(progress_callback *callback)
     {UNREACHABLE();}
 
@@ -134,6 +133,9 @@ private:
 
 
     void refresh();
+
+    smt_params &fparams() { return m_fparams; }
+
 public:
     virtual_solver_factory(ast_manager &mgr, smt_params &fparams);
     virtual ~virtual_solver_factory();
@@ -144,7 +146,6 @@ public:
     void collect_param_descrs(param_descrs &r) { /* empty */ }
     void set_produce_models(bool f) { m_fparams.m_model = f; }
     bool get_produce_models() { return m_fparams.m_model; }
-    smt_params &fparams() { return m_fparams; }
 };
 
 }

src/opt/maxres.cpp

@@ -315,14 +315,13 @@ public:
 
     void found_optimum() {
         IF_VERBOSE(1, verbose_stream() << "found optimum\n";);
-        rational upper(0);
+        m_lower.reset();
         for (unsigned i = 0; i < m_soft.size(); ++i) {
             m_assignment[i] = is_true(m_soft[i]);
             if (!m_assignment[i]) {
-                upper += m_weights[i];
+                m_lower += m_weights[i];
             }
         }
-        SASSERT(upper == m_lower);
         m_upper = m_lower;
         m_found_feasible_optimum = true;
     }
@@ -397,10 +396,11 @@ public:
     void get_current_correction_set(model* mdl, exprs& cs) {
         cs.reset();
         if (!mdl) return;
-        for (unsigned i = 0; i < m_asms.size(); ++i) {
+        for (expr* a : m_asms) {
-            if (is_false(mdl, m_asms[i].get())) {
+            if (is_false(mdl, a)) {
-                cs.push_back(m_asms[i].get());
+                cs.push_back(a);
             }
+            TRACE("opt", expr_ref tmp(m); mdl->eval(a, tmp, true); tout << mk_pp(a, m) << ": " << tmp << "\n";);
         }
         TRACE("opt", display_vec(tout << "new correction set: ", cs););
     }
@@ -509,6 +509,7 @@ public:
         trace();
         if (m_c.num_objectives() == 1 && m_pivot_on_cs && m_csmodel.get() && m_correction_set_size < core.size()) {
             exprs cs;
+            TRACE("opt", tout << "cs " << m_correction_set_size << " " << core.size() << "\n";);
             get_current_correction_set(m_csmodel.get(), cs);
             m_correction_set_size = cs.size();
             if (m_correction_set_size < core.size()) {

src/opt/opt_context.cpp

@@ -819,7 +819,7 @@ namespace opt {
         bool is_max = is_maximize(fml, term, orig_term, index);
         bool is_min = !is_max && is_minimize(fml, term, orig_term, index);
         if (is_min && get_pb_sum(term, terms, weights, offset)) {
-            TRACE("opt", tout << "try to convert minimization" << mk_pp(term, m) << "\n";);
+            TRACE("opt", tout << "try to convert minimization\n" << mk_pp(term, m) << "\n";);
             // minimize 2*x + 3*y 
             // <=>
             // (assert-soft (not x) 2)

src/parsers/smt/smtlib_solver.cpp

@@ -34,7 +34,7 @@ Revision History:
 namespace smtlib {
 
     solver::solver():
-        m_ast_manager(m_params.m_proof ? PGM_FINE : PGM_DISABLED, 
+        m_ast_manager(m_params.m_proof ? PGM_ENABLED : PGM_DISABLED, 
                       m_params.m_trace ? m_params.m_trace_file_name.c_str() : 0),
         m_ctx(0),
         m_error_code(0) {

src/parsers/smt2/CMakeLists.txt

@@ -1,5 +1,6 @@
 z3_add_component(smt2parser
   SOURCES
+    marshal.cpp
     smt2parser.cpp
     smt2scanner.cpp
   COMPONENT_DEPENDENCIES

src/parsers/smt2/marshal.cpp

@@ -2,14 +2,14 @@
 Copyright (c) 2017 Arie Gurfinkel
 Module Name:
 
-   spacer_marshal.cpp
+   marshal.cpp
 
 Abstract:
 
    marshaling and unmarshaling of expressions
 
    --*/
-#include "muz/spacer/spacer_marshal.h"
+#include "parsers/smt2/marshal.h"
 
 #include <sstream>
 
@@ -18,39 +18,33 @@ Abstract:
 #include "util/vector.h"
 #include "ast/ast_smt_pp.h"
 #include "ast/ast_pp.h"
+#include "ast/ast_util.h"
 
-namespace spacer {
+std::ostream &marshal(std::ostream &os, expr_ref e, ast_manager &m) {
-std::ostream &marshal(std::ostream &os, expr_ref e, ast_manager &m)
-{
     ast_smt_pp pp(m);
     pp.display_smt2(os, e);
     return os;
 }
 
-std::string marshal(expr_ref e, ast_manager &m)
+std::string marshal(expr_ref e, ast_manager &m) {
-{
     std::stringstream ss;
     marshal(ss, e, m);
     return ss.str();
 }
 
 
-expr_ref unmarshal(std::istream &is, ast_manager &m)
+expr_ref unmarshal(std::istream &is, ast_manager &m) {
-{
     cmd_context ctx(false, &m);
     ctx.set_ignore_check(true);
     if (!parse_smt2_commands(ctx, is)) { return expr_ref(0, m); }
 
     ptr_vector<expr>::const_iterator it  = ctx.begin_assertions();
     ptr_vector<expr>::const_iterator end = ctx.end_assertions();
-    if (it == end) { return expr_ref(m.mk_true(), m); }
     unsigned size = static_cast<unsigned>(end - it);
-    return expr_ref(m.mk_and(size, it), m);
+    return expr_ref(mk_and(m, size, it), m);
 }
 
-expr_ref unmarshal(std::string s, ast_manager &m)
+expr_ref unmarshal(std::string s, ast_manager &m) {
-{
     std::istringstream is(s);
     return unmarshal(is, m);
 }
-}

src/parsers/smt2/marshal.h

@@ -2,7 +2,7 @@
 Copyright (c) 2017 Arie Gurfinkel
 Module Name:
 
-   spacer_marshal.h
+   marshal.h
 
 Abstract:
 
@@ -17,14 +17,11 @@ Abstract:
 
 #include "ast/ast.h"
 
-namespace spacer {
 std::ostream &marshal(std::ostream &os, expr_ref e, ast_manager &m);
 std::string marshal(expr_ref e, ast_manager &m);
 expr_ref unmarshal(std::string s, ast_manager &m);
 expr_ref unmarshal(std::istream &is, ast_manager &m);
 
 
-}
-
 
 #endif

src/parsers/smt2/smt2parser.cpp

@@ -1881,6 +1881,8 @@ namespace smt2 {
                 // the resultant expression is on the top of the stack
                 TRACE("let_frame", tout << "let result expr: " << mk_pp(expr_stack().back(), m()) << "\n";);
                 expr_ref r(m());
+                if (expr_stack().empty())
+                    throw parser_exception("invalid let expression");
                 r = expr_stack().back();
                 expr_stack().pop_back();
                 // remove local declarations from the stack

src/smt/CMakeLists.txt

@@ -75,7 +75,7 @@ z3_add_component(smt
     normal_forms
     parser_util
     pattern
-    proof_checker
+    proofs
     proto_model
     simplex
     substitution

src/smt/asserted_formulas.cpp

@@ -101,14 +101,14 @@ void asserted_formulas::push_assertion(expr * e, proof * pr, vector<justified_ex
     else if (m.is_and(e)) {
         for (unsigned i = 0; i < to_app(e)->get_num_args(); ++i) {
             expr* arg = to_app(e)->get_arg(i);
-            proof_ref _pr(m.mk_and_elim(pr, i), m);
+            proof_ref _pr(m.proofs_enabled() ? m.mk_and_elim(pr, i) : 0, m);
             push_assertion(arg, _pr, result);
         }
     }
     else if (m.is_not(e, e1) && m.is_or(e1)) {
         for (unsigned i = 0; i < to_app(e1)->get_num_args(); ++i) {
             expr* arg = to_app(e1)->get_arg(i);
-            proof_ref _pr(m.mk_not_or_elim(pr, i), m);
+            proof_ref _pr(m.proofs_enabled() ? m.mk_not_or_elim(pr, i) : 0, m);
             expr_ref  narg(mk_not(m, arg), m);
             push_assertion(narg, _pr, result);
         }
@@ -163,7 +163,7 @@ void asserted_formulas::assert_expr(expr * e, proof * _in_pr) {
 }
 
 void asserted_formulas::assert_expr(expr * e) {
-    assert_expr(e, m.mk_asserted(e));
+    assert_expr(e, m.proofs_enabled() ? m.mk_asserted(e) : nullptr);
 }
 
 void asserted_formulas::get_assertions(ptr_vector<expr> & result) const {
@@ -365,7 +365,7 @@ void asserted_formulas::nnf_cnf() {
         CASSERT("well_sorted", is_well_sorted(m, n));
         apply_nnf(n, push_todo, push_todo_prs, r1, pr1);
         CASSERT("well_sorted",is_well_sorted(m, r1));
-        pr = m.mk_modus_ponens(pr, pr1);
+        pr = m.proofs_enabled() ? m.mk_modus_ponens(pr, pr1) : nullptr;
         push_todo.push_back(r1);
         push_todo_prs.push_back(pr);
 
@@ -506,16 +506,16 @@ void asserted_formulas::update_substitution(expr* n, proof* pr) {
         }
         if (is_gt(rhs, lhs)) {
             TRACE("propagate_values", tout << "insert " << mk_pp(rhs, m) << " -> " << mk_pp(lhs, m) << "\n";);
-            m_scoped_substitution.insert(rhs, lhs, m.mk_symmetry(pr));
+            m_scoped_substitution.insert(rhs, lhs, m.proofs_enabled() ? m.mk_symmetry(pr) : nullptr);
             return;
         }
         TRACE("propagate_values", tout << "incompatible " << mk_pp(n, m) << "\n";);
     }
     if (m.is_not(n, n1)) {
-        m_scoped_substitution.insert(n1, m.mk_false(), m.mk_iff_false(pr));
+        m_scoped_substitution.insert(n1, m.mk_false(), m.proofs_enabled() ? m.mk_iff_false(pr) : nullptr);
     }
     else {
-        m_scoped_substitution.insert(n, m.mk_true(), m.mk_iff_true(pr));
+        m_scoped_substitution.insert(n, m.mk_true(), m.proofs_enabled() ? m.mk_iff_true(pr) : nullptr);
     }
 }
 

src/smt/smt_conflict_resolution.cpp

@@ -810,8 +810,6 @@ namespace smt {
             m_new_proofs.push_back(pr);
             return pr;
         }
-        if (m_manager.coarse_grain_proofs())
-            return pr;
         TRACE("norm_eq_proof",
               tout << "#" << n1->get_owner_id() << " = #" << n2->get_owner_id() << "\n";
               tout << mk_ll_pp(pr, m_manager, true, false););
@@ -1217,7 +1215,7 @@ namespace smt {
         mk_proof(rhs, c, prs2);
         while (!prs2.empty()) {
             proof * pr = prs2.back();
-            if (m_manager.fine_grain_proofs()) {
+            if (m_manager.proofs_enabled()) {
                 pr = m_manager.mk_symmetry(pr);
                 m_new_proofs.push_back(pr);
                 prs1.push_back(pr);

src/smt/smt_context.cpp

@@ -23,7 +23,7 @@ Revision History:
 #include "ast/ast_ll_pp.h"
 #include "util/warning.h"
 #include "smt/smt_quick_checker.h"
-#include "ast/proof_checker/proof_checker.h"
+#include "ast/proofs/proof_checker.h"
 #include "ast/ast_util.h"
 #include "smt/uses_theory.h"
 #include "model/model.h"

src/smt/smt_justification.cpp

@@ -129,7 +129,7 @@ namespace smt {
 
         if (m_node1 != m_node1->get_root()) {
             proof * pr = cr.get_proof(m_node1, m_node1->get_root());
-            if (pr && m.fine_grain_proofs())
+            if (pr && m.proofs_enabled())
                 pr = m.mk_symmetry(pr);
             prs.push_back(pr);
             if (!pr) 

src/smt/theory_array.cpp

@@ -53,18 +53,12 @@ namespace smt {
         var_data * d2 = m_var_data[v2];
         if (!d1->m_prop_upward && d2->m_prop_upward)
             set_prop_upward(v1);
-        ptr_vector<enode>::iterator it   = d2->m_stores.begin();
+        for (enode* n : d2->m_stores) 
-        ptr_vector<enode>::iterator end  = d2->m_stores.end();
+            add_store(v1, n);
-        for (; it != end; ++it) 
+        for (enode* n : d2->m_parent_stores) 
-            add_store(v1, *it);
+            add_parent_store(v1, n);
-        it  = d2->m_parent_stores.begin();
+        for (enode* n : d2->m_parent_selects) 
-        end = d2->m_parent_stores.end();
+            add_parent_select(v1, n);
-        for (; it != end; ++it)
-            add_parent_store(v1, *it);
-        it  = d2->m_parent_selects.begin();
-        end = d2->m_parent_selects.end();
-        for (; it != end; ++it)
-            add_parent_select(v1, *it);
         TRACE("array", tout << "after merge\n"; display_var(tout, v1););
     }
 
@@ -103,16 +97,11 @@ namespace smt {
         d->m_parent_selects.push_back(s);
         TRACE("array", tout << mk_pp(s->get_owner(), get_manager()) << " " << mk_pp(get_enode(v)->get_owner(), get_manager()) << "\n";);
         m_trail_stack.push(push_back_trail<theory_array, enode *, false>(d->m_parent_selects));
-        ptr_vector<enode>::iterator it  = d->m_stores.begin();
+        for (enode* n : d->m_stores) {
-        ptr_vector<enode>::iterator end = d->m_stores.end();
+            instantiate_axiom2a(s, n);
-        for (; it != end; ++it) {
-            instantiate_axiom2a(s, *it);
         }
         if (!m_params.m_array_weak && !m_params.m_array_delay_exp_axiom && d->m_prop_upward) {
-            it  = d->m_parent_stores.begin();
+            for (enode* store : d->m_parent_stores) {
-            end = d->m_parent_stores.end();
-            for (; it != end; ++it) {
-                enode * store = *it;
                 SASSERT(is_store(store));
                 if (!m_params.m_array_cg || store->is_cgr()) {
                     instantiate_axiom2b(s, store);
@@ -129,27 +118,19 @@ namespace smt {
         var_data * d     = m_var_data[v];
         d->m_parent_stores.push_back(s);
         m_trail_stack.push(push_back_trail<theory_array, enode *, false>(d->m_parent_stores));
-        if (!m_params.m_array_weak && !m_params.m_array_delay_exp_axiom && d->m_prop_upward) {
+        if (!m_params.m_array_weak && !m_params.m_array_delay_exp_axiom && d->m_prop_upward) 
-            ptr_vector<enode>::iterator it  = d->m_parent_selects.begin();
+            for (enode* n : d->m_parent_selects) 
-            ptr_vector<enode>::iterator end = d->m_parent_selects.end();
+                if (!m_params.m_array_cg || n->is_cgr())
-            for (; it != end; ++it) 
+                    instantiate_axiom2b(n, s);
-                if (!m_params.m_array_cg || (*it)->is_cgr())
-                    instantiate_axiom2b(*it, s);
-        }
     }
 
     bool theory_array::instantiate_axiom2b_for(theory_var v) {
         bool result = false;
         var_data * d = m_var_data[v];
-        ptr_vector<enode>::iterator it  = d->m_parent_stores.begin();
+        for (enode* n1 : d->m_parent_stores) 
-        ptr_vector<enode>::iterator end = d->m_parent_stores.end();
+            for (enode * n2 : d->m_parent_selects) 
-        for (; it != end; ++it) {
+                if (instantiate_axiom2b(n2, n1))
-            ptr_vector<enode>::iterator it2  = d->m_parent_selects.begin();
-            ptr_vector<enode>::iterator end2 = d->m_parent_selects.end();
-            for (; it2 != end2; ++it2) 
-                if (instantiate_axiom2b(*it2, *it))
                     result = true;
-        }
         return result;
     }
 
@@ -167,10 +148,8 @@ namespace smt {
             d->m_prop_upward = true;
             if (!m_params.m_array_delay_exp_axiom)
                 instantiate_axiom2b_for(v);
-            ptr_vector<enode>::iterator it  = d->m_stores.begin();
+            for (enode * n : d->m_stores) 
-            ptr_vector<enode>::iterator end = d->m_stores.end();
+                set_prop_upward(n);
-            for (; it != end; ++it)
-                set_prop_upward(*it);
         }
     }
 
@@ -209,11 +188,9 @@ namespace smt {
         }
         d->m_stores.push_back(s);
         m_trail_stack.push(push_back_trail<theory_array, enode *, false>(d->m_stores));
-        ptr_vector<enode>::iterator it  = d->m_parent_selects.begin();
+        for (enode * n : d->m_parent_selects) {
-        ptr_vector<enode>::iterator end = d->m_parent_selects.end();
+            SASSERT(is_select(n));
-        for (; it != end; ++it) {
+            instantiate_axiom2a(n, s);
-            SASSERT(is_select(*it));
-            instantiate_axiom2a(*it, s);
         }
         if (m_params.m_array_always_prop_upward || lambda_equiv_class_size >= 1) 
             set_prop_upward(s);
@@ -374,7 +351,7 @@ namespace smt {
     
     final_check_status theory_array::final_check_eh() {
         m_final_check_idx++;
-        final_check_status r;
+        final_check_status r = FC_DONE;
         if (m_params.m_array_lazy_ieq) {
             // Delay the creation of interface equalities...  The
             // motivation is too give other theories and quantifier

src/smt/theory_array_base.cpp

@@ -210,17 +210,15 @@ namespace smt {
 
 
 
-
     func_decl_ref_vector * theory_array_base::register_sort(sort * s_array) {
         unsigned dimension = get_dimension(s_array);
         func_decl_ref_vector * ext_skolems = 0;
         if (!m_sort2skolem.find(s_array, ext_skolems)) {       
+            array_util util(get_manager());
             ast_manager & m = get_manager();
             ext_skolems = alloc(func_decl_ref_vector, m);
             for (unsigned i = 0; i < dimension; ++i) {
-                sort * ext_sk_domain[2] = { s_array, s_array };
+                func_decl * ext_sk_decl = util.mk_array_ext(s_array, i);
-                parameter p(i);
-                func_decl * ext_sk_decl = m.mk_func_decl(get_id(), OP_ARRAY_EXT, 1, &p, 2, ext_sk_domain);
                 ext_skolems->push_back(ext_sk_decl);
             }
             m_sort2skolem.insert(s_array, ext_skolems);

src/smt/theory_seq.cpp

@@ -3466,6 +3466,8 @@ static bool get_arith_value(context& ctx, theory_id afid, expr* e, expr_ref& v)
 bool theory_seq::get_num_value(expr* e, rational& val) const {
     context& ctx = get_context();
     expr_ref _val(m);
+	if (!ctx.e_internalized(e))
+		return false;
     enode* next = ctx.get_enode(e), *n = next;
     do { 
         if (get_arith_value(ctx, m_autil.get_family_id(), next->get_owner(), _val) && m_autil.is_numeral(_val, val) && val.is_int()) {

src/smt/theory_str.cpp

@@ -190,13 +190,13 @@ namespace smt {
 
     expr * theory_str::rewrite_implication(expr * premise, expr * conclusion) {
         ast_manager & m = get_manager();
-        return m.mk_or(m.mk_not(premise), conclusion);
+        return m.mk_or(mk_not(m, premise), conclusion);
     }
 
     void theory_str::assert_implication(expr * premise, expr * conclusion) {
         ast_manager & m = get_manager();
         TRACE("str", tout << "asserting implication " << mk_ismt2_pp(premise, m) << " -> " << mk_ismt2_pp(conclusion, m) << std::endl;);
-        expr_ref axiom(m.mk_or(m.mk_not(premise), conclusion), m);
+        expr_ref axiom(m.mk_or(mk_not(m, premise), conclusion), m);
         assert_axiom(axiom);
     }
 
@@ -545,7 +545,7 @@ namespace smt {
         context & ctx = get_context();
         ast_manager & m = get_manager();
 
-        expr_ref ax1(m.mk_not(ctx.mk_eq_atom(s, mk_string(""))), m);
+        expr_ref ax1(mk_not(m, ctx.mk_eq_atom(s, mk_string(""))), m);
         assert_axiom(ax1);
 
         {
@@ -557,7 +557,7 @@ namespace smt {
             SASSERT(zero);
             // build LHS > RHS and assert
             // we have to build !(LHS <= RHS) instead
-            expr_ref lhs_gt_rhs(m.mk_not(m_autil.mk_le(len_str, zero)), m);
+            expr_ref lhs_gt_rhs(mk_not(m, m_autil.mk_le(len_str, zero)), m);
             SASSERT(lhs_gt_rhs);
             assert_axiom(lhs_gt_rhs);
         }
@@ -592,7 +592,7 @@ namespace smt {
             SASSERT(zero);
             // build LHS > RHS and assert
             // we have to build !(LHS <= RHS) instead
-            expr_ref lhs_gt_rhs(m.mk_not(m_autil.mk_le(len_str, zero)), m);
+            expr_ref lhs_gt_rhs(mk_not(m, m_autil.mk_le(len_str, zero)), m);
             SASSERT(lhs_gt_rhs);
             assert_axiom(lhs_gt_rhs);
         }
@@ -1089,7 +1089,7 @@ namespace smt {
                           m_autil.mk_ge(expr->get_arg(1), mk_int(0)),
                           // REWRITE for arithmetic theory:
                           // m_autil.mk_lt(expr->get_arg(1), mk_strlen(expr->get_arg(0)))
-                          m.mk_not(m_autil.mk_ge(m_autil.mk_add(expr->get_arg(1), m_autil.mk_mul(mk_int(-1), mk_strlen(expr->get_arg(0)))), mk_int(0)))
+                          mk_not(m, m_autil.mk_ge(m_autil.mk_add(expr->get_arg(1), m_autil.mk_mul(mk_int(-1), mk_strlen(expr->get_arg(0)))), mk_int(0)))
                                ), m);
 
         expr_ref_vector and_item(m);
@@ -1130,7 +1130,7 @@ namespace smt {
         expr_ref_vector innerItems(m);
         innerItems.push_back(ctx.mk_eq_atom(expr->get_arg(1), mk_concat(ts0, ts1)));
         innerItems.push_back(ctx.mk_eq_atom(mk_strlen(ts0), mk_strlen(expr->get_arg(0))));
-        innerItems.push_back(m.mk_ite(ctx.mk_eq_atom(ts0, expr->get_arg(0)), expr, m.mk_not(expr)));
+        innerItems.push_back(m.mk_ite(ctx.mk_eq_atom(ts0, expr->get_arg(0)), expr, mk_not(m, expr)));
         expr_ref then1(m.mk_and(innerItems.size(), innerItems.c_ptr()), m);
         SASSERT(then1);
 
@@ -1143,7 +1143,7 @@ namespace smt {
             , m);
         SASSERT(topLevelCond);
 
-        expr_ref finalAxiom(m.mk_ite(topLevelCond, then1, m.mk_not(expr)), m);
+        expr_ref finalAxiom(m.mk_ite(topLevelCond, then1, mk_not(m, expr)), m);
         SASSERT(finalAxiom);
         assert_axiom(finalAxiom);
     }
@@ -1167,7 +1167,7 @@ namespace smt {
         expr_ref_vector innerItems(m);
         innerItems.push_back(ctx.mk_eq_atom(expr->get_arg(1), mk_concat(ts0, ts1)));
         innerItems.push_back(ctx.mk_eq_atom(mk_strlen(ts1), mk_strlen(expr->get_arg(0))));
-        innerItems.push_back(m.mk_ite(ctx.mk_eq_atom(ts1, expr->get_arg(0)), expr, m.mk_not(expr)));
+        innerItems.push_back(m.mk_ite(ctx.mk_eq_atom(ts1, expr->get_arg(0)), expr, mk_not(m, expr)));
         expr_ref then1(m.mk_and(innerItems.size(), innerItems.c_ptr()), m);
         SASSERT(then1);
 
@@ -1180,7 +1180,7 @@ namespace smt {
             , m);
         SASSERT(topLevelCond);
 
-        expr_ref finalAxiom(m.mk_ite(topLevelCond, then1, m.mk_not(expr)), m);
+        expr_ref finalAxiom(m.mk_ite(topLevelCond, then1, mk_not(m, expr)), m);
         SASSERT(finalAxiom);
         assert_axiom(finalAxiom);
     }
@@ -1204,7 +1204,7 @@ namespace smt {
             if (haystackStr.contains(needleStr)) {
                 assert_axiom(ex);
             } else {
-                assert_axiom(m.mk_not(ex));
+                assert_axiom(mk_not(m, ex));
             }
             return;
         }
@@ -1265,7 +1265,7 @@ namespace smt {
         SASSERT(tmpLen);
         thenItems.push_back(ctx.mk_eq_atom(expr->get_arg(0), mk_concat(x3, x4)));
         thenItems.push_back(ctx.mk_eq_atom(mk_strlen(x3), tmpLen));
-        thenItems.push_back(m.mk_not(mk_contains(x3, expr->get_arg(1))));
+        thenItems.push_back(mk_not(m, mk_contains(x3, expr->get_arg(1))));
         expr_ref thenBranch(m.mk_and(thenItems.size(), thenItems.c_ptr()), m);
         SASSERT(thenBranch);
 
@@ -1341,7 +1341,7 @@ namespace smt {
 
         expr_ref ite1(m.mk_ite(
                           //m_autil.mk_lt(expr->get_arg(2), zeroAst),
-                          m.mk_not(m_autil.mk_ge(expr->get_arg(2), zeroAst)),
+                          mk_not(m, m_autil.mk_ge(expr->get_arg(2), zeroAst)),
                           ctx.mk_eq_atom(resAst, mk_indexof(expr->get_arg(0), expr->get_arg(1))),
                           ite2
                                ), m);
@@ -1384,7 +1384,7 @@ namespace smt {
         thenItems.push_back(m_autil.mk_ge(indexAst, mk_int(0)));
         //  args[0] = x1 . args[1] . x2
         //  x1 doesn't contain args[1]
-        thenItems.push_back(m.mk_not(mk_contains(x2, expr->get_arg(1))));
+        thenItems.push_back(mk_not(m, mk_contains(x2, expr->get_arg(1))));
         thenItems.push_back(ctx.mk_eq_atom(indexAst, mk_strlen(x1)));
 
         bool canSkip = false;
@@ -1402,7 +1402,7 @@ namespace smt {
             expr_ref tmpLen(m_autil.mk_add(indexAst, mk_int(1)), m);
             thenItems.push_back(ctx.mk_eq_atom(expr->get_arg(0), mk_concat(x3, x4)));
             thenItems.push_back(ctx.mk_eq_atom(mk_strlen(x3), tmpLen));
-            thenItems.push_back(m.mk_not(mk_contains(x4, expr->get_arg(1))));
+            thenItems.push_back(mk_not(m, mk_contains(x4, expr->get_arg(1))));
         }
         //----------------------------
         // else branch
@@ -1452,7 +1452,7 @@ namespace smt {
         argumentsValid_terms.push_back(m_autil.mk_ge(substrPos, zero));
         // pos < strlen(base)
         // --> pos + -1*strlen(base) < 0
-        argumentsValid_terms.push_back(m.mk_not(m_autil.mk_ge(
+        argumentsValid_terms.push_back(mk_not(m, m_autil.mk_ge(
                                                     m_autil.mk_add(substrPos, m_autil.mk_mul(minusOne, substrLen)),
                                                     zero)));
 
@@ -1473,7 +1473,7 @@ namespace smt {
 
         // Case 1: pos < 0 or pos >= strlen(base) or len < 0
         // ==> (Substr ...) = ""
-        expr_ref case1_premise(m.mk_not(argumentsValid), m);
+        expr_ref case1_premise(mk_not(m, argumentsValid), m);
         SASSERT(case1_premise);
         ctx.internalize(case1_premise, false);
         expr_ref case1_conclusion(ctx.mk_eq_atom(expr, mk_string("")), m);
@@ -1505,7 +1505,7 @@ namespace smt {
         case3_conclusion_terms.push_back(ctx.mk_eq_atom(mk_strlen(t3), substrLen));
         case3_conclusion_terms.push_back(ctx.mk_eq_atom(expr, t3));
         expr_ref case3_conclusion(mk_and(case3_conclusion_terms), m);
-        expr_ref case3(rewrite_implication(m.mk_and(argumentsValid, m.mk_not(lenOutOfBounds)), case3_conclusion), m);
+        expr_ref case3(rewrite_implication(m.mk_and(argumentsValid, mk_not(m, lenOutOfBounds)), case3_conclusion), m);
         SASSERT(case3);
 
         ctx.internalize(case1, false);
@@ -1548,7 +1548,7 @@ namespace smt {
         argumentsValid_terms.push_back(m_autil.mk_ge(substrPos, zero));
         // pos < strlen(base)
         // --> pos + -1*strlen(base) < 0
-        argumentsValid_terms.push_back(m.mk_not(m_autil.mk_ge(
+        argumentsValid_terms.push_back(mk_not(m, m_autil.mk_ge(
                                                     m_autil.mk_add(substrPos, m_autil.mk_mul(minusOne, substrLen)),
                                                     zero)));
         // len >= 0
@@ -1564,7 +1564,7 @@ namespace smt {
 
         // Case 1: pos < 0 or pos >= strlen(base) or len < 0
         // ==> (Substr ...) = ""
-        expr_ref case1_premise(m.mk_not(argumentsValid), m);
+        expr_ref case1_premise(mk_not(m, argumentsValid), m);
         expr_ref case1_conclusion(ctx.mk_eq_atom(expr, mk_string("")), m);
         expr_ref case1(m.mk_implies(case1_premise, case1_conclusion), m);
 
@@ -1589,7 +1589,7 @@ namespace smt {
         case3_conclusion_terms.push_back(ctx.mk_eq_atom(mk_strlen(t3), substrLen));
         case3_conclusion_terms.push_back(ctx.mk_eq_atom(expr, t3));
         expr_ref case3_conclusion(mk_and(case3_conclusion_terms), m);
-        expr_ref case3(m.mk_implies(m.mk_and(argumentsValid, m.mk_not(lenOutOfBounds)), case3_conclusion), m);
+        expr_ref case3(m.mk_implies(m.mk_and(argumentsValid, mk_not(m, lenOutOfBounds)), case3_conclusion), m);
 
         assert_axiom(case1);
         assert_axiom(case2);
@@ -1630,7 +1630,7 @@ namespace smt {
         expr_ref tmpLen(m_autil.mk_add(i1, mk_strlen(expr->get_arg(1)), mk_int(-1)), m);
         thenItems.push_back(ctx.mk_eq_atom(expr->get_arg(0), mk_concat(x3, x4)));
         thenItems.push_back(ctx.mk_eq_atom(mk_strlen(x3), tmpLen));
-        thenItems.push_back(m.mk_not(mk_contains(x3, expr->get_arg(1))));
+        thenItems.push_back(mk_not(m, mk_contains(x3, expr->get_arg(1))));
         thenItems.push_back(ctx.mk_eq_atom(result, mk_concat(x1, mk_concat(expr->get_arg(2), x2))));
         // -----------------------
         // false branch
@@ -1684,7 +1684,7 @@ namespace smt {
             expr_ref tl(mk_str_var("tl"), m);
             expr_ref conclusion1(ctx.mk_eq_atom(S, mk_concat(hd, tl)), m);
             expr_ref conclusion2(ctx.mk_eq_atom(mk_strlen(hd), m_autil.mk_numeral(rational::one(), true)), m);
-            expr_ref conclusion3(m.mk_not(ctx.mk_eq_atom(hd, mk_string("0"))), m);
+            expr_ref conclusion3(mk_not(m, ctx.mk_eq_atom(hd, mk_string("0"))), m);
             expr_ref conclusion(m.mk_and(conclusion1, conclusion2, conclusion3), m);
             SASSERT(premise);
             SASSERT(conclusion);
@@ -1708,7 +1708,7 @@ namespace smt {
         // axiom 1: N < 0 <==> (str.from-int N) = ""
         expr * N = ex->get_arg(0);
         {
-            expr_ref axiom1_lhs(m.mk_not(m_autil.mk_ge(N, m_autil.mk_numeral(rational::zero(), true))), m);
+            expr_ref axiom1_lhs(mk_not(m, m_autil.mk_ge(N, m_autil.mk_numeral(rational::zero(), true))), m);
             expr_ref axiom1_rhs(ctx.mk_eq_atom(ex, mk_string("")), m);
             expr_ref axiom1(ctx.mk_eq_atom(axiom1_lhs, axiom1_rhs), m);
             SASSERT(axiom1);
@@ -1947,7 +1947,7 @@ namespace smt {
                 // inconsistency check: value
                 if (!can_two_nodes_eq(eqc_nn1, eqc_nn2)) {
                     TRACE("str", tout << "inconsistency detected: " << mk_pp(eqc_nn1, m) << " cannot be equal to " << mk_pp(eqc_nn2, m) << std::endl;);
-                    expr_ref to_assert(m.mk_not(ctx.mk_eq_atom(eqc_nn1, eqc_nn2)), m);
+                    expr_ref to_assert(mk_not(m, ctx.mk_eq_atom(eqc_nn1, eqc_nn2)), m);
                     assert_axiom(to_assert);
                     // this shouldn't use the integer theory at all, so we don't allow the option of quick-return
                     return false;
@@ -2160,7 +2160,7 @@ namespace smt {
                                 expr_ref implyR11(ctx.mk_eq_atom(mk_strlen(arg1), mk_int(makeUpLenArg1)), m);
                                 assert_implication(implyL11, implyR11);
                             } else {
-                                expr_ref neg(m.mk_not(implyL11), m);
+                                expr_ref neg(mk_not(m, implyL11), m);
                                 assert_axiom(neg);
                             }
                         }
@@ -2231,7 +2231,7 @@ namespace smt {
                                 expr_ref implyR11(ctx.mk_eq_atom(mk_strlen(arg0), mk_int(makeUpLenArg0)), m);
                                 assert_implication(implyL11, implyR11);
                             } else {
-                                expr_ref neg(m.mk_not(implyL11), m);
+                                expr_ref neg(mk_not(m, implyL11), m);
                                 assert_axiom(neg);
                             }
                         }
@@ -2762,7 +2762,7 @@ namespace smt {
         }
 
         if (!can_two_nodes_eq(new_nn1, new_nn2)) {
-            expr_ref detected(m.mk_not(ctx.mk_eq_atom(new_nn1, new_nn2)), m);
+            expr_ref detected(mk_not(m, ctx.mk_eq_atom(new_nn1, new_nn2)), m);
             TRACE("str", tout << "inconsistency detected: " << mk_ismt2_pp(detected, m) << std::endl;);
             assert_axiom(detected);
             return;
@@ -5008,7 +5008,7 @@ namespace smt {
                             implyR = boolVar;
                         } else {
                             //implyR = Z3_mk_eq(ctx, boolVar, Z3_mk_false(ctx));
-                            implyR = m.mk_not(boolVar);
+                            implyR = mk_not(m, boolVar);
                         }
                     } else {
                         // ------------------------------------------------------------------------------------------------
@@ -5037,7 +5037,7 @@ namespace smt {
                                         litems.push_back(ctx.mk_eq_atom(substrAst, aConcat));
                                     }
                                     //implyR = Z3_mk_eq(ctx, boolVar, Z3_mk_false(ctx));
-                                    implyR = m.mk_not(boolVar);
+                                    implyR = mk_not(m, boolVar);
                                     break;
                                 }
                             }
@@ -5076,7 +5076,7 @@ namespace smt {
                             implyR = boolVar;
                         } else {
                             // implyR = Z3_mk_eq(ctx, boolVar, Z3_mk_false(ctx));
-                            implyR = m.mk_not(boolVar);
+                            implyR = mk_not(m, boolVar);
                         }
                     }
 
@@ -5146,7 +5146,7 @@ namespace smt {
                                             litems.push_back(ctx.mk_eq_atom(substrAst, aConcat));
                                         }
                                         expr_ref implyLHS(mk_and(litems), m);
-                                        expr_ref implyR(m.mk_not(boolVar), m);
+                                        expr_ref implyR(mk_not(m, boolVar), m);
                                         assert_implication(implyLHS, implyR);
                                         break;
                                     }
@@ -6515,7 +6515,7 @@ namespace smt {
                             if (matchRes) {
                                 assert_implication(implyL, boolVar);
                             } else {
-                                assert_implication(implyL, m.mk_not(boolVar));
+                                assert_implication(implyL, mk_not(m, boolVar));
                             }
                         }
                     }
@@ -6603,7 +6603,7 @@ namespace smt {
                           << arg1_str << "\" + \"" << arg2_str <<
                           "\" != \"" << const_str << "\"" << "\n";);
                     expr_ref equality(ctx.mk_eq_atom(concat, str), m);
-                    expr_ref diseq(m.mk_not(equality), m);
+                    expr_ref diseq(mk_not(m, equality), m);
                     assert_axiom(diseq);
                     return;
                 }
@@ -6621,7 +6621,7 @@ namespace smt {
                           "\" is longer than \"" << const_str << "\","
                           << " so cannot be concatenated with anything to form it" << "\n";);
                     expr_ref equality(ctx.mk_eq_atom(newConcat, str), m);
-                    expr_ref diseq(m.mk_not(equality), m);
+                    expr_ref diseq(mk_not(m, equality), m);
                     assert_axiom(diseq);
                     return;
                 } else {
@@ -6635,7 +6635,7 @@ namespace smt {
                               << "actually \"" << arg2_str << "\""
                               << "\n";);
                         expr_ref equality(ctx.mk_eq_atom(newConcat, str), m);
-                        expr_ref diseq(m.mk_not(equality), m);
+                        expr_ref diseq(mk_not(m, equality), m);
                         assert_axiom(diseq);
                         return;
                     } else {

src/tactic/bv/bvarray2uf_rewriter.cpp

@@ -117,7 +117,7 @@ func_decl_ref bvarray2uf_rewriter_cfg::mk_uf_for_array(expr * e) {
             if (is_uninterp_const(e)) {
                 if (m_emc)
                     m_emc->insert(to_app(e)->get_decl(),
-                                  m_array_util.mk_as_array(m_manager.get_sort(e), bv_f));
+                                  m_array_util.mk_as_array(bv_f));
             }
             else if (m_fmc)
                 m_fmc->insert(bv_f);
@@ -193,7 +193,7 @@ br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr
             if (is_uninterp_const(e)) {
                 if (m_emc)
                     m_emc->insert(e->get_decl(),
-                        m_array_util.mk_as_array(m_manager.get_sort(e), bv_f));
+                        m_array_util.mk_as_array(bv_f));
             }
             else if (m_fmc)
                 m_fmc->insert(bv_f);
@@ -207,7 +207,7 @@ br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr
         q = m_manager.mk_forall(1, sorts, names, body);
         extra_assertions.push_back(q);
 
-        result = m_array_util.mk_as_array(f->get_range(), bv_f);
+        result = m_array_util.mk_as_array(bv_f);
 
         TRACE("bvarray2uf_rw", tout << "result: " << mk_ismt2_pp(result, m_manager) << ")" << std::endl;);
         res = BR_DONE;
@@ -234,7 +234,7 @@ br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr
         if (is_bv_array(t)) {
             // From [1]: For every array term t we create a fresh uninterpreted function f_t.
             f_t = mk_uf_for_array(t);
-            result = m_array_util.mk_as_array(m_manager.get_sort(t), f_t);
+            result = m_array_util.mk_as_array(f_t);
             res = BR_DONE;
         }
         else if (has_bv_arrays) {
@@ -274,7 +274,7 @@ br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr
                     expr * v = args[0];
                     func_decl_ref f_t(mk_uf_for_array(t), m_manager);
 
-                    result = m_array_util.mk_as_array(f->get_range(), f_t);
+                    result = m_array_util.mk_as_array(f_t);
                     res = BR_DONE;
 
                     // Add \forall x . f_t(x) = v
@@ -321,7 +321,7 @@ br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr
                     expr_ref frllx(m_manager.mk_forall(1, sorts, names, body), m_manager);
                     extra_assertions.push_back(frllx);
 
-                    result = m_array_util.mk_as_array(f->get_range(), f_t);
+                    result = m_array_util.mk_as_array(f_t);
                     res = BR_DONE;
                 }
                 else if (m_array_util.is_store(f)) {
@@ -342,7 +342,7 @@ br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr
                         func_decl_ref f_s(mk_uf_for_array(s), m_manager);
                         func_decl_ref f_t(mk_uf_for_array(t), m_manager);
 
-                        result = m_array_util.mk_as_array(f->get_range(), f_t);
+                        result = m_array_util.mk_as_array(f_t);
                         res = BR_DONE;
 
                         sort * sorts[1] = { get_index_sort(f->get_range()) };

src/tactic/core/dom_simplify_tactic.cpp

@@ -441,7 +441,7 @@ ptr_vector<expr> const & dom_simplify_tactic::tree(expr * e) {
 }
 
 
-// ----------------------
+// ---------------------
 // expr_substitution_simplifier
 
 bool expr_substitution_simplifier::assert_expr(expr * t, bool sign) {

src/tactic/core/dom_simplify_tactic.h

@@ -95,7 +95,6 @@ class dom_simplify_tactic : public tactic {
     expr_ref_vector      m_trail, m_args;
     obj_map<expr, expr*> m_result;
     expr_dominators      m_dominators;
-    unsigned             m_scope_level;
     unsigned             m_depth;
     unsigned             m_max_depth;
     ptr_vector<expr>     m_empty;
@@ -128,8 +127,7 @@ public:
     dom_simplify_tactic(ast_manager & m, dom_simplifier* s, params_ref const & p = params_ref()):
         m(m), m_simplifier(s), m_params(p), 
         m_trail(m), m_args(m), 
-        m_dominators(m), 
+        m_dominators(m), m_depth(0), m_max_depth(1024), m_forward(true) {}
-        m_scope_level(0), m_depth(0), m_max_depth(1024), m_forward(true) {}
 
 
     virtual ~dom_simplify_tactic();

src/test/proof_checker.cpp

@@ -4,11 +4,11 @@ Copyright (c) 2015 Microsoft Corporation
 
 --*/
 
-#include "ast/proof_checker/proof_checker.h"
+#include "ast/proofs/proof_checker.h"
 #include "ast/ast_ll_pp.h"
 
 void tst_checker1() {
-    ast_manager m(PGM_FINE);
+    ast_manager m(PGM_ENABLED);
     expr_ref a(m);
     proof_ref p1(m), p2(m), p3(m), p4(m);
     expr_ref_vector side_conditions(m);

src/util/CMakeLists.txt

@@ -28,6 +28,7 @@ z3_add_component(util
     lbool.cpp
     luby.cpp
     memory_manager.cpp
+    min_cut.cpp
     mpbq.cpp
     mpf.cpp
     mpff.cpp

src/util/container_util.h

@@ -0,0 +1,122 @@
+/*++
+Copyright (c) 2017 Microsoft Corporation
+
+Module Name:
+
+    container_util.h
+
+Abstract:
+
+    Useful functions for containers
+
+Author:
+
+    Krystof Hoder, Nikolaj Bjorner 2017-10-24
+
+Revision History:
+
+    Extracted from dl_util.h
+
+--*/
+
+#ifndef CONTAINER_UTIL_H_
+#define CONTAINER_UTIL_H_
+
+// -----------------------------------
+//
+// container functions
+//
+// -----------------------------------
+
+template<class Set1, class Set2>
+    void set_intersection(Set1 & tgt, const Set2 & src) {
+    svector<typename Set1::data> to_remove;
+    for (auto const& itm : tgt) 
+        if (!src.contains(itm)) 
+            to_remove.push_back(itm);
+    while (!to_remove.empty()) {
+        tgt.remove(to_remove.back());
+        to_remove.pop_back();
+    }
+}
+
+template<class Set>
+void set_difference(Set & tgt, const Set & to_remove) {
+    for (auto const& itm : to_remove) 
+        tgt.remove(itm);
+}
+
+template<class Set1, class Set2>
+void set_union(Set1 & tgt, const Set2 & to_add) {
+    for (auto const& itm : to_add) 
+        tgt.insert(itm);
+}
+
+template<class T>
+void unite_disjoint_maps(T & tgt, const T & src) {
+    for (auto const& kv : src) {
+        SASSERT(!tgt.contains(kv.m_key));
+        tgt.insert(kv.m_key, kv.m_value);
+    }
+}
+
+template<class T, class U>
+void collect_map_range(T & acc, const U & map) {
+    for (auto const& kv : map) 
+        acc.push_back(kv.m_value);
+}
+
+
+template<class T>
+void print_container(const T & begin, const T & end, std::ostream & out) {
+    T it = begin;
+    out << "(";
+    bool first = true;
+    for(; it!=end; ++it) {
+        if(first) { first = false; } else { out << ","; }
+        out << (*it);
+    }
+    out << ")";
+}
+
+template<class T>
+void print_container(const T & cont, std::ostream & out) {
+    print_container(cont.begin(), cont.end(), out);
+}
+
+template<class T, class M>
+void print_container(const ref_vector<T,M> & cont, std::ostream & out) {
+    print_container(cont.c_ptr(), cont.c_ptr() + cont.size(), out);
+}
+
+template<class T>
+void print_map(const T & cont, std::ostream & out) {
+    out << "(";
+    bool first = true;
+    for (auto const& kv : cont) {
+        if (first) { first = false; } else { out << ","; }
+        out << kv.m_key << "->" << kv.m_value;
+    }
+    out << ")";
+}
+
+template<class It, class V> 
+unsigned find_index(const It & begin, const It & end, const V & val) {
+    It it = begin;
+    for (unsigned idx = 0; it != end; it++, idx++) {
+        if (*it == val) {
+            return idx;
+        }
+    }
+    return UINT_MAX;
+}
+
+template<class T, class U>
+bool containers_equal(const T & begin1, const T & end1, const U & begin2, const U & end2) {
+    T it1 = begin1;
+    U it2 = begin2;
+    for (; it1 != end1 && it2 != end2 && *it1 == *it2; ++it1, ++it2) {};
+    return it1 == end1 && it2 == end2;
+}
+
+#endif

src/util/min_cut.cpp

@@ -0,0 +1,232 @@
+/*++
+Copyright (c) 2017 Arie Gurfinkel
+
+Module Name:
+
+    min_cut.cpp
+
+Abstract:
+    min cut solver
+
+Author:
+    Bernhard Gleiss
+
+Revision History:
+
+
+--*/
+#include "util/min_cut.h"
+#include "util/trace.h"
+
+min_cut::min_cut() {    
+    // push back two empty vectors for source and sink
+    m_edges.push_back(edge_vector());
+    m_edges.push_back(edge_vector());
+}
+
+unsigned min_cut::new_node() {
+    m_edges.push_back(edge_vector());
+    return m_edges.size() - 1;
+}
+
+void min_cut::add_edge(unsigned int i, unsigned int j, unsigned capacity) {
+    m_edges.reserve(i + 1);
+    m_edges[i].push_back(edge(j, capacity));
+    TRACE("spacer.mincut", tout << "adding edge (" << i << "," << j << ")\n";);    
+}
+
+void min_cut::compute_min_cut(unsigned_vector& cut_nodes) {
+    if (m_edges.size() == 2) {
+        return;
+    }
+    
+    m_d.resize(m_edges.size());
+    m_pred.resize(m_edges.size());
+    
+    // compute initial distances and number of nodes
+    compute_initial_distances();
+    
+    unsigned i = 0;
+    
+    while (m_d[0] < m_edges.size()) {
+        unsigned j = get_admissible_edge(i);
+            
+        if (j < m_edges.size()) {
+            // advance(i)
+            m_pred[j] = i;
+            i = j;
+            
+            // if i is the sink, augment path
+            if (i == 1) {
+                augment_path();
+                i = 0;
+            }
+        }
+        else {
+            // retreat
+            compute_distance(i);
+            if (i != 0) {
+                i = m_pred[i];
+            }
+        }
+    }
+
+    // split nodes into reachable and unreachable ones
+    bool_vector reachable(m_edges.size());
+    compute_reachable_nodes(reachable);
+    
+    // find all edges between reachable and unreachable nodes and 
+    // for each such edge, add corresponding lemma to unsat-core
+    compute_cut_and_add_lemmas(reachable, cut_nodes);
+}
+
+void min_cut::compute_initial_distances() {
+    unsigned_vector todo;
+    bool_vector visited(m_edges.size());
+    
+    todo.push_back(0); // start at the source, since we do postorder traversel
+    
+    while (!todo.empty()) {
+        unsigned current = todo.back();
+        
+        // if we haven't already visited current
+        if (!visited[current]) {
+            bool exists_unvisited_parent = false;
+            
+            // add unprocessed parents to stack for DFS. If there is at least 
+            // one unprocessed parent, don't compute the result
+            // for current now, but wait until those unprocessed parents are processed
+            for (auto const& edge : m_edges[current]) {
+                unsigned parent = edge.node;
+                
+                // if we haven't visited the current parent yet
+                if (!visited[parent]) {
+                    // add it to the stack
+                    todo.push_back(parent);
+                    exists_unvisited_parent = true;
+                }
+            }
+            
+            // if we already visited all parents, we can visit current too
+            if (!exists_unvisited_parent) {
+                visited[current] = true;
+                todo.pop_back();
+                
+                compute_distance(current); // I.H. all parent distances are already computed
+            }
+        }
+        else {
+            todo.pop_back();
+        }
+    }
+}
+
+unsigned min_cut::get_admissible_edge(unsigned i) {
+    for (const auto& edge : m_edges[i]) {
+        if (edge.weight > 0 && m_d[i] == m_d[edge.node] + 1) {
+            return edge.node;
+        }
+    }
+    return m_edges.size(); // no element found
+}
+
+void min_cut::augment_path() {
+    // find bottleneck capacity
+    unsigned max = std::numeric_limits<unsigned int>::max();
+    unsigned k = 1;
+    while (k != 0) {
+        unsigned l = m_pred[k];
+        for (const auto& edge : m_edges[l]) {
+            if (edge.node == k) {
+                max = std::min(max, edge.weight);
+            }
+        }
+        k = l;
+    }
+
+    k = 1;
+    while (k != 0) {
+        unsigned l = m_pred[k];
+        
+        // decrease capacity
+        for (auto& edge : m_edges[l]) {
+            if (edge.node == k) {
+                edge.weight -= max;
+            }
+        }
+        // increase reverse flow
+        bool already_exists = false;
+        for (auto& edge : m_edges[k]) {
+            if (edge.node == l) {
+                already_exists = true;
+                edge.weight += max;
+            }
+        }
+        if (!already_exists) {
+            m_edges[k].push_back(edge(1, max));
+        }
+        k = l;
+    }
+}
+
+void min_cut::compute_distance(unsigned i) {
+    if (i == 1) { // sink node
+        m_d[1] = 0;
+    }
+    else {
+        unsigned min = std::numeric_limits<unsigned int>::max();
+        
+        // find edge (i,j) with positive residual capacity and smallest distance
+        for (const auto& edge : m_edges[i]) {
+            if (edge.weight > 0) {
+                min = std::min(min, m_d[edge.node] + 1);
+            }
+        }
+        m_d[i] = min;
+    }
+}
+
+void min_cut::compute_reachable_nodes(bool_vector& reachable) {
+    unsigned_vector todo;
+    
+    todo.push_back(0);
+    while (!todo.empty()) {
+        unsigned current = todo.back();
+        todo.pop_back();
+        
+        if (!reachable[current]) {
+            reachable[current] = true;
+            
+            for (const auto& edge : m_edges[current]) {
+                if (edge.weight > 0) {
+                    todo.push_back(edge.node);
+                }
+            }
+        }
+    }
+}
+
+void min_cut::compute_cut_and_add_lemmas(bool_vector& reachable, unsigned_vector& cut_nodes) {
+    unsigned_vector todo;
+    bool_vector visited(m_edges.size());
+        
+    todo.push_back(0);
+    while (!todo.empty()) {
+        unsigned current = todo.back();
+        todo.pop_back();
+        
+        if (!visited[current]) {
+            visited[current] = true;
+
+            for (const auto& edge : m_edges[current]) {
+                unsigned successor = edge.node;
+                if (reachable[successor]) {
+                    todo.push_back(successor);
+                }
+                else {
+                    cut_nodes.push_back(successor);
+                }
+            }
+        }
+    }
+}

src/util/min_cut.h

@@ -0,0 +1,63 @@
+/*++
+Copyright (c) 2017 Arie Gurfinkel
+
+Module Name:
+
+    min_cut.h
+
+Abstract:
+    min cut solver
+
+Author:
+    Bernhard Gleiss
+
+Revision History:
+
+
+--*/
+
+#ifndef MIN_CUT_H_
+#define MIN_CUT_H_
+
+#include "util/vector.h"
+
+
+class min_cut {
+public:
+    min_cut();
+
+    /*
+      \brief create a node
+    */
+    unsigned new_node();
+
+    /*
+      \brief add an i -> j edge with (unit) capacity 
+    */
+    void add_edge(unsigned i, unsigned j, unsigned capacity = 1);
+
+    /*
+      \brief produce a min cut between source node = 0 and target node = 1.
+      NB. the function changes capacities on edges.
+    */
+    void compute_min_cut(unsigned_vector& cut_nodes);
+    
+private:
+
+    typedef svector<bool> bool_vector;
+    struct edge { unsigned node; unsigned weight; edge(unsigned n, unsigned w): node(n), weight(w) {} edge(): node(0), weight(0) {} };
+    typedef svector<edge> edge_vector;
+        
+    vector<edge_vector> m_edges; // map from node to all outgoing edges together with their weights (also contains "reverse edges")
+    unsigned_vector m_d;    // approximation of distance from node to sink in residual graph
+    unsigned_vector m_pred; // predecessor-information for reconstruction of augmenting path
+    
+    void compute_initial_distances();
+    unsigned get_admissible_edge(unsigned i);
+    void augment_path();
+    void compute_distance(unsigned i);
+    void compute_reachable_nodes(bool_vector& reachable);
+    void compute_cut_and_add_lemmas(bool_vector& reachable, unsigned_vector& cut_nodes);
+};
+
+#endif