diff --git a/CMakeLists.txt b/CMakeLists.txt index c3b6b591c..4a6871451 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -2,7 +2,7 @@ cmake_minimum_required(VERSION 3.4) set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake") -project(Z3 VERSION 4.8.13.0 LANGUAGES CXX C) +project(Z3 VERSION 4.8.14.0 LANGUAGES CXX C) ################################################################################ # Project version diff --git a/RELEASE_NOTES b/RELEASE_NOTES index dae1e81b8..790691c3d 100644 --- a/RELEASE_NOTES +++ b/RELEASE_NOTES @@ -3,14 +3,18 @@ RELEASE NOTES Version 4.8.next ================ - Planned features - - specialized solver support for QF_ABV and ABV based on lazy SMT and dual reduction - - the smtfd solver and tactic implement this strategy, but is not prime for users. + - sat.euf + - a new CDCL core for SMT queries. It extends the SAT engine with theory solver plugins. + the current state is unstable. It lacks efficient ematching. + - polysat + - native word level bit-vector solving. - introduction of simple induction lemmas to handle a limited repertoire of induction proofs. - - circuit optimization techniques for BV in-processing are available as the sat.cut - option, but at this point does not translate into benefits. It is currently - turned off by default. +Version 4.8.13 +============== +The release integrates various bug fixes and tuning. + Version 4.8.12 ============== Release provided to fix git tag discrepancy issues with 4.8.11 diff --git a/examples/SMT-LIB2/bounded model checking/bubble_sort.smt2 b/examples/SMT-LIB2/bounded model checking/bubble_sort.smt2 new file mode 100644 index 000000000..d4e28afbb --- /dev/null +++ b/examples/SMT-LIB2/bounded model checking/bubble_sort.smt2 @@ -0,0 +1,168 @@ +; File name: bubble_sort.smt2 +; +; BUBBLESORT - Copyright (c) March, 2021 - Matteo Nicoli +; +; An example of bounded model checking of the classic bubble sort algorithm. +; we will copy the array values into a list in order to check whether the +; array is ordered or not. That's because: +; - it's easier to walk recursively through a list +; - it gives an example of how list and sequences work in Z3 +; + + +; size of the array +(declare-const dim Int) + +; arrays declaration +(declare-const A0 (Array Int Int)) +(declare-const A1 (Array Int Int)) +(declare-const A2 (Array Int Int)) +(declare-const A3 (Array Int Int)) + +; indexes declaration +(declare-const i0 Int) +(declare-const i1 Int) +(declare-const i2 Int) +(declare-const i3 Int) + +(declare-const j0 Int) +(declare-const j1 Int) +(declare-const j2 Int) +(declare-const j3 Int) + +(declare-const tmp0 Int) +(declare-const tmp1 Int) +(declare-const tmp2 Int) + +; lists declaration (for post condition) +(declare-const l0 (List Int)) +(declare-const l1 (List Int)) +(declare-const l2 (List Int)) +(declare-const l3 (List Int)) +(declare-const l4 (List Int)) + +(define-fun init_indexes ((_i Int) (_j Int)) Bool + (and + (= _i 0) + (= _j 0) + ) +) + +(define-fun inner_loop + ( + (_A0 (Array Int Int)) + (_A1 (Array Int Int)) + (tmp Int) + (_i0 Int) + (_dim Int) + ) Bool + (ite + (> (select _A0 _i0) (select _A0 (+ _i0 1))) + (and + (= tmp (select _A0 _i0)) + (= _A1 (store _A0 _i0 (select _A0 (+ _i0 1)))) + (= _A1 (store _A0 (+ _i0 1) tmp)) + ) + (= _A1 _A0) + ) +) + +; the body of the bubblesort algorithm +(define-fun bsort_step + ( + (_A0 (Array Int Int)) + (_A1 (Array Int Int)) + (tmp Int) + (_i0 Int) + (_j0 Int) + (_i1 Int) + (_j1 Int) + (_dim Int) + ) Bool + (ite + (< _j0 (- _dim 1)) + (and + (ite + (< _i0 (- _dim 1)) + (and + (inner_loop _A0 _A1 tmp _i0 _dim) + (= _i1 (+ _i0 1)) + ) + (= _j1 (+ _j0 1)) + ) + (= _j1 (+ _j0 1)) + ) + (and + (= _j1 (+ _j0 1)) + (= _A1 _A0) + ) + ) +) + +; the function by which we check whether the list is ordered +(define-fun-rec check ((_l (List Int))) Bool + (ite + (= _l nil) + true + (ite + (not (= (tail _l) nil)) + (and + (>= (head _l) (head (tail _l))) + (check (tail _l)) + ) + true + ) + ) +) + +; sets the size of the array +(assert (= dim 4)) + +; initialization of the counters +(assert (init_indexes i0 j0)) + +; the first step of the sorting algorithm +(assert (bsort_step A0 A1 tmp0 i0 j0 i1 j1 dim)) +(assert (bsort_step A1 A2 tmp1 i1 j1 i2 j2 dim)) +(assert (bsort_step A2 A3 tmp2 i2 j2 i3 j3 dim)) + +; filling the list for test +(assert + (and + (= l0 nil) + (= l1 (insert (select A3 0) l0)) + (= l2 (insert (select A3 1) l1)) + (= l3 (insert (select A3 2) l2)) + (= l4 (insert (select A3 3) l3)) + ) +) + +(echo "BUBBLE SORT") + +(push) + +; (negated) post-condition +(assert (not (check l4))) + +(echo "Testing the validity of the algorithm; `unsat` expected: ") + +; `unsat` expected +(check-sat) + +(echo "---------------------") + +(pop) + +; post-condition +(assert (check l4)) + +(echo "Getting a model; `sat` expected: ") + +; `sat` expected +(check-sat) + +(echo "---------------------") + +(echo "Model: ") +(get-value (A3)) +(exit) diff --git a/examples/SMT-LIB2/bounded model checking/loop_unrolling.smt2 b/examples/SMT-LIB2/bounded model checking/loop_unrolling.smt2 new file mode 100644 index 000000000..45ce586f1 --- /dev/null +++ b/examples/SMT-LIB2/bounded model checking/loop_unrolling.smt2 @@ -0,0 +1,114 @@ +; File name: loop_unrolling.smt2 +; +; Copyright (c) March, 2021 - Matteo Nicoli +; +; +; Let's start considering a simple C program involving an iteration: +; +; #define DIM 2 +; +; /* uninterpreted functions */ +; long get_number(); +; void fill_array(long *A); +; +; int main() +; { +; long x = get_number(); +; long A[DIM]; +; long i = 0; +; long found = 0; +; +; fill_array(A); +; +; while(i < DIM) { +; if(x == A[i]) +; found = 1; +; i++; +; } +; } +; +; Below, we can see its SSA representation in SMT-LIB2. +; Our goal is to verify that, at the end of the program, the variable `found` +; is equal to 1 if, and only if, `x` is an element of the array. + + +(declare-const x Int) +(declare-const A (Array Int Int)) +(declare-const i_0 Int) +(declare-const found_0 Int) + +(declare-const found_1 Int) +(declare-const found_2 Int) +(declare-const i_1 Int) +(declare-const i_2 Int) + +; Pre-condition: variables initialization +(assert + (and + (= i_0 0) + (= found_0 0) + ) +) + +; Transition funcion +(define-fun body ((f_0 Int) (f Int) (i_0 Int) (i_1 Int)(_A (Array Int Int)) (_x Int)) Bool + (and + (= f (ite (= _x (select _A i_0)) 1 f_0)) + (= i_1 (+ i_0 1)) + ) +) + +; Post-condition function +(define-fun post ((_f Int) (_i Int) (_x Int) (_A (Array Int Int))) Bool + (= + (= _f 1) + (= _x (select _A _i)) + ) +) + +; Transition function is called DIM times: +; for practical reasons, we are considering here DIM = 2 +(assert (body found_0 found_1 i_0 i_1 A x)) +(assert (body found_1 found_2 i_1 i_2 A x)) + +(push) + +(echo "Bounded model checking with loop unrolling") + +(echo "------------------------------------------") + +; Post-condition (negated) is called DIM times +(assert + (not + (or + (post found_2 i_0 x A) + (post found_2 i_1 x A) + ) + ) +) + +(echo "Testing the validity of the post-condition: `unsat expected`") + +; `unsat` expected +(check-sat) + +(pop) + +; Post-condition (called DIM times) +(assert + (or + (post found_2 i_0 x A) + (post found_2 i_1 x A) + ) +) + +(echo "Getting a model; `sat` expected: ") + +; `sat` expected +(check-sat) + +(echo "------------------------------------------") + +(echo "Model: ") +(get-value (x A found_2)) +(exit) diff --git a/examples/SMT-LIB2/bounded model checking/loop_unrolling_bitvec.smt2 b/examples/SMT-LIB2/bounded model checking/loop_unrolling_bitvec.smt2 new file mode 100644 index 000000000..ceb792875 --- /dev/null +++ b/examples/SMT-LIB2/bounded model checking/loop_unrolling_bitvec.smt2 @@ -0,0 +1,116 @@ +; File name: loop_unrolling_bitvec.smt2 +; +; Copyright (c) March, 2021 - Matteo Nicoli +; +; +; Let's start considering a simple C program involving an iteration: +; +; #define DIM 2 +; +; /* uninterpreted functions */ +; long get_number(); +; void fill_array(long *A); +; +; int main() +; { +; long x = get_number(); +; long A[DIM]; +; long i = 0; +; long found = 0; +; +; fill_array(A); +; +; while(i < DIM) { +; if(x == A[i]) +; found = 1; +; i++; +; } +; } +; +; Below, we can see its SSA representation in SMT-LIB2. +; Our goal is to verify that, at the end of the program, the variable `found` +; is equal to 1 if, and only if, `x` is an element of the array. +; We define our custom sort `IntValue` that represents a 32-bit integer value. + + +(define-sort IntValue () (_ BitVec 32)) +(declare-const x IntValue) +(declare-const A (Array IntValue IntValue)) +(declare-const i_0 IntValue) +(declare-const found_0 IntValue) + +(declare-const found_1 IntValue) +(declare-const found_2 IntValue) +(declare-const i_1 IntValue) +(declare-const i_2 IntValue) + +; Pre-condition: variables initialization +(assert + (and + (= i_0 #x00000000) + (= found_0 #x00000000) + ) +) + +; Transition funcion +(define-fun body ((f_0 IntValue) (f IntValue) (i_0 IntValue) (i_1 IntValue)(_A (Array IntValue IntValue)) (_x IntValue)) Bool + (and + (= f (ite (= _x (select _A i_0)) #x00000001 f_0)) + (= i_1 (bvadd i_0 #x00000001)) + ) +) + +; Post-condition function +(define-fun post ((_f IntValue) (_i IntValue) (_x IntValue) (_A (Array IntValue IntValue))) Bool + (= + (= _f #x00000001) + (= _x (select _A _i)) + ) +) + +; Transition function is called DIM times: +; for practical reasons, we are considering here DIM = 2 +(assert (body found_0 found_1 i_0 i_1 A x)) +(assert (body found_1 found_2 i_1 i_2 A x)) + +(push) + +(echo "Bounded model checking with loop unrolling") + +(echo "------------------------------------------") + +; Post-condition (negated) is called DIM times +(assert + (not + (or + (post found_2 i_0 x A) + (post found_2 i_1 x A) + ) + ) +) + +(echo "Testing the validity of the post-condition: `unsat expected`") + +; `unsat` expected +(check-sat) + +(pop) + +; Post-condition (called DIM times) +(assert + (or + (post found_2 i_0 x A) + (post found_2 i_1 x A) + ) +) + +(echo "Getting a model; `sat` expected: ") + +; `sat` expected +(check-sat) + +(echo "------------------------------------------") + +(echo "Model: ") +(get-value (x A found_2)) +(exit) diff --git a/examples/c/test_capi.c b/examples/c/test_capi.c index a9c472f37..a6fcbdb22 100644 --- a/examples/c/test_capi.c +++ b/examples/c/test_capi.c @@ -561,7 +561,6 @@ void display_ast(Z3_context c, FILE * out, Z3_ast v) } case Z3_QUANTIFIER_AST: { fprintf(out, "quantifier"); - ; } default: fprintf(out, "#unknown"); diff --git a/examples/python/bounded model checking/bubble_sort.py b/examples/python/bounded model checking/bubble_sort.py index 0495f97f9..80e87eee2 100644 --- a/examples/python/bounded model checking/bubble_sort.py +++ b/examples/python/bounded model checking/bubble_sort.py @@ -1,4 +1,6 @@ -# BUBBLESORT - Copyright (c) June, 2020 - Matteo Nicoli +# File name: bubble_sort.py +# +# BUBBLESORT - Copyright (c) June, 2020 - Matteo Nicoli from z3 import Solver, Int, Array, IntSort, And, Not, If, Select, Store, sat @@ -36,34 +38,56 @@ def check(variables, Ar, dim) : yield variables[e] == Select(Ar,e) def mk_post_condition(values) : - condition = [] - for v1,v2 in zip(values,values[1:]) : - condition.append(v1 <= v2) + condition = [v1 <= v2 for v1,v2 in zip(values,values[1:])] return And(*condition) -dim = int(input("size of the array: ")) -i = [Int(f"i_{x}") for x in range(dim + 1)] -j = [Int(f"j_{x}") for x in range(dim + 1)] -A = [Array(f"A_{x}",IntSort(),IntSort()) for x in range(dim + 1)] -tmp = [Int(f"tmp_{x}") for x in range(dim)] +def main() : + dim = int(input("size of the array: ")) -s = Solver() + i = [Int(f"i_{x}") for x in range(dim + 1)] + j = [Int(f"j_{x}") for x in range(dim + 1)] + A = [Array(f"A_{x}",IntSort(),IntSort()) for x in range(dim + 1)] + tmp = [Int(f"tmp_{x}") for x in range(dim)] -init_condition = init(i[0],j[0]) -s.add(init_condition) + s = Solver() -tran_condition= mk_tran_condition(A, i, j, tmp, dim) -s.add(And(*tran_condition)) + init_condition = init(i[0],j[0]) + s.add(init_condition) -values = [Int(f"n_{x}") for x in range(dim)] -init_check_condition = check(values,A[-1],dim) -s.add(And(*init_check_condition)) + tran_condition = mk_tran_condition(A, i, j, tmp, dim) + s.add(And(*tran_condition)) -post_condition = mk_post_condition(values) -s.add(Not(post_condition)) + values = [Int(f"n_{x}") for x in range(dim)] + init_check_condition = check(values,A[-1],dim) + s.add(And(*init_check_condition)) -if s.check() == sat : - print(f"counterexample:\n{s.model()}") -else : - print("valid") \ No newline at end of file + post_condition = mk_post_condition(values) + + print("Bubble sort") + print("---------------------") + + s.push() + s.add(Not(post_condition)) + + print("Testing the validity of the algorithm; `valid expected`:") + + if s.check() == sat : + print(f"counterexample:\n{s.model()}") + else : + print("valid") + + print("---------------------") + + s.pop() + + s.add(post_condition) + print("Getting a model...") + print("Model:") + + if s.check() == sat : + print(s.model()) + + +if __name__ == "__main__" : + main() diff --git a/scripts/mk_project.py b/scripts/mk_project.py index d2331e11e..e3d181b41 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -8,7 +8,7 @@ from mk_util import * def init_version(): - set_version(4, 8, 13, 0) + set_version(4, 8, 14, 0) # Z3 Project definition def init_project_def(): diff --git a/scripts/nightly.yaml b/scripts/nightly.yaml index 5b7a15aa3..d26f77934 100644 --- a/scripts/nightly.yaml +++ b/scripts/nightly.yaml @@ -1,5 +1,5 @@ variables: - ReleaseVersion: '4.8.11' + ReleaseVersion: '4.8.13' stages: - stage: Build @@ -36,14 +36,14 @@ stages: - job: UbuntuDoc displayName: "Ubuntu Doc build" pool: - vmImage: "Ubuntu-18.04" + vmImage: "Ubuntu-latest" steps: - script: sudo apt-get install ocaml opam libgmp-dev - - script: sudo apt-get install doxygen - - script: sudo apt-get install graphviz - script: opam init -y - script: eval `opam config env`; opam install zarith ocamlfind -y - - script: python scripts/mk_make.py --ml --staticlib + - script: eval `opam config env`; python scripts/mk_make.py --ml + - script: sudo apt-get install doxygen + - script: sudo apt-get install graphviz - script: | set -e cd build @@ -51,7 +51,6 @@ stages: make -j3 make -j3 examples make -j3 test-z3 - ./ml_example cd .. - script: | set -e diff --git a/scripts/release.yml b/scripts/release.yml index 901afc575..9a1982744 100644 --- a/scripts/release.yml +++ b/scripts/release.yml @@ -6,7 +6,7 @@ trigger: none variables: - ReleaseVersion: '4.8.12' + ReleaseVersion: '4.8.13' stages: @@ -76,14 +76,14 @@ stages: - job: UbuntuDoc displayName: "Ubuntu Doc build" pool: - vmImage: "Ubuntu-18.04" + vmImage: "Ubuntu-latest" steps: - script: sudo apt-get install ocaml opam libgmp-dev - - script: sudo apt-get install doxygen - - script: sudo apt-get install graphviz - script: opam init -y - script: eval `opam config env`; opam install zarith ocamlfind -y - - script: python scripts/mk_make.py --ml --staticlib + - script: eval `opam config env`; python scripts/mk_make.py --ml + - script: sudo apt-get install doxygen + - script: sudo apt-get install graphviz - script: | set -e cd build @@ -91,7 +91,6 @@ stages: make -j3 make -j3 examples make -j3 test-z3 - ./ml_example cd .. - script: | set -e @@ -310,6 +309,7 @@ stages: jobs: - job: GitHubPublish + condition: eq(0,1) displayName: "Publish to GitHub" pool: vmImage: "windows-latest" @@ -397,9 +397,9 @@ stages: artifact: 'PythonPackage' path: dist - task: DownloadSecureFile@1 - name: pypirc + name: pypircs inputs: - secureFile: 'pypirc' + secureFile: 'pypircs' - script: python3 -m pip install --upgrade pip - script: python3 -m pip install --user -U setuptools importlib_metadata wheel twine - - script: python3 -m twine upload --config-file $(pypirc.secureFilePath) -r $(pypiReleaseServer) dist/* \ No newline at end of file + - script: python3 -m twine upload --config-file $(pypircs.secureFilePath) -r $(pypiReleaseServer) dist/* \ No newline at end of file diff --git a/src/ackermannization/ackermannize_bv_tactic.cpp b/src/ackermannization/ackermannize_bv_tactic.cpp index dcf6a7c59..79cad2fb2 100644 --- a/src/ackermannization/ackermannize_bv_tactic.cpp +++ b/src/ackermannization/ackermannize_bv_tactic.cpp @@ -31,6 +31,8 @@ public: ~ackermannize_bv_tactic() override { } + char const* name() const override { return "ackermannize_bv"; } + void operator()(goal_ref const & g, goal_ref_buffer & result) override { tactic_report report("ackermannize_bv", *g); fail_if_unsat_core_generation("ackermannize", g); diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 10a98c477..7f67879bc 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -1232,6 +1232,7 @@ extern "C" { if (mk_c(c)->get_char_fid() == _d->get_family_id()) { switch (_d->get_decl_kind()) { + case OP_CHAR_CONST: return Z3_OP_CHAR_CONST; case OP_CHAR_LE: return Z3_OP_CHAR_LE; case OP_CHAR_TO_INT: return Z3_OP_CHAR_TO_INT; case OP_CHAR_TO_BV: return Z3_OP_CHAR_TO_BV; diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 0f2473956..66a1384f5 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -87,8 +87,6 @@ namespace api { m_error_code = Z3_OK; m_print_mode = Z3_PRINT_SMTLIB_FULL; - - m_interruptable = nullptr; m_error_handler = &default_error_handler; m_bv_fid = m().mk_family_id("bv"); @@ -98,7 +96,7 @@ namespace api { m_datalog_fid = m().mk_family_id("datalog_relation"); m_fpa_fid = m().mk_family_id("fpa"); m_seq_fid = m().mk_family_id("seq"); - m_char_fid = m().mk_family_id("char"); + m_char_fid = m().mk_family_id("char"); m_special_relations_fid = m().mk_family_id("specrels"); m_dt_plugin = static_cast(m().get_plugin(m_dt_fid)); @@ -120,19 +118,18 @@ namespace api { context::set_interruptable::set_interruptable(context & ctx, event_handler & i): m_ctx(ctx) { lock_guard lock(ctx.m_mux); - SASSERT(m_ctx.m_interruptable == 0); - m_ctx.m_interruptable = &i; + m_ctx.m_interruptable.push_back(& i); } context::set_interruptable::~set_interruptable() { lock_guard lock(m_ctx.m_mux); - m_ctx.m_interruptable = nullptr; + m_ctx.m_interruptable.pop_back(); } void context::interrupt() { lock_guard lock(m_mux); - if (m_interruptable) - (*m_interruptable)(API_INTERRUPT_EH_CALLER); + for (auto * eh : m_interruptable) + (*eh)(API_INTERRUPT_EH_CALLER); m_limit.cancel(); m().limit().cancel(); } diff --git a/src/api/api_context.h b/src/api/api_context.h index ae9671f7a..41c797163 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -115,7 +115,7 @@ namespace api { std::string m_exception_msg; // catch the message associated with a Z3 exception Z3_ast_print_mode m_print_mode; - event_handler * m_interruptable; // Reference to an object that can be interrupted by Z3_interrupt + ptr_vector m_interruptable; // Reference to an object that can be interrupted by Z3_interrupt public: // Scoped obj for setting m_interruptable diff --git a/src/api/api_parsers.cpp b/src/api/api_parsers.cpp index c40e0ccf3..94132a361 100644 --- a/src/api/api_parsers.cpp +++ b/src/api/api_parsers.cpp @@ -157,6 +157,9 @@ extern "C" { LOG_Z3_eval_smtlib2_string(c, str); if (!mk_c(c)->cmd()) { mk_c(c)->cmd() = alloc(cmd_context, false, &(mk_c(c)->m())); + install_dl_cmds(*mk_c(c)->cmd()); + install_opt_cmds(*mk_c(c)->cmd()); + install_smt2_extra_cmds(*mk_c(c)->cmd()); mk_c(c)->cmd()->set_solver_factory(mk_smt_strategic_solver_factory()); } scoped_ptr& ctx = mk_c(c)->cmd(); diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 659e4c4a4..ea009b1bc 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -17,6 +17,7 @@ Revision History: --*/ #include +#include #include "util/scoped_ctrl_c.h" #include "util/cancel_eh.h" #include "util/file_path.h" @@ -158,10 +159,19 @@ extern "C" { init_solver_core(c, s); } + static void init_solver_log(Z3_context c, Z3_solver s) { + static std::thread::id g_thread_id = std::this_thread::get_id(); + static bool g_is_threaded = false; solver_params sp(to_solver(s)->m_params); symbol smt2log = sp.smtlib2_log(); if (smt2log.is_non_empty_string() && !to_solver(s)->m_pp) { + if (g_is_threaded || g_thread_id != std::this_thread::get_id()) { + g_is_threaded = true; + std::ostringstream strm; + strm << smt2log << "-" << std::this_thread::get_id(); + smt2log = symbol(strm.str()); + } to_solver(s)->m_pp = alloc(solver2smt2_pp, mk_c(c)->m(), smt2log.str()); } } @@ -856,7 +866,7 @@ extern "C" { Z3_CATCH_RETURN(nullptr); } - class api_context_obj : public solver::context_obj { + class api_context_obj : public user_propagator::context_obj { api::context* c; public: api_context_obj(api::context* c):c(c) {} @@ -873,9 +883,9 @@ extern "C" { Z3_TRY; RESET_ERROR_CODE(); init_solver(c, s); - solver::push_eh_t _push = push_eh; - solver::pop_eh_t _pop = pop_eh; - solver::fresh_eh_t _fresh = [=](void * user_ctx, ast_manager& m, solver::context_obj*& _ctx) { + user_propagator::push_eh_t _push = push_eh; + user_propagator::pop_eh_t _pop = pop_eh; + user_propagator::fresh_eh_t _fresh = [=](void * user_ctx, ast_manager& m, user_propagator::context_obj*& _ctx) { ast_context_params params; params.set_foreign_manager(&m); auto* ctx = alloc(api::context, ¶ms, false); @@ -892,7 +902,7 @@ extern "C" { Z3_fixed_eh fixed_eh) { Z3_TRY; RESET_ERROR_CODE(); - solver::fixed_eh_t _fixed = (void(*)(void*,solver::propagate_callback*,unsigned,expr*))fixed_eh; + user_propagator::fixed_eh_t _fixed = (void(*)(void*,user_propagator::callback*,unsigned,expr*))fixed_eh; to_solver_ref(s)->user_propagate_register_fixed(_fixed); Z3_CATCH; } @@ -903,7 +913,7 @@ extern "C" { Z3_final_eh final_eh) { Z3_TRY; RESET_ERROR_CODE(); - solver::final_eh_t _final = (bool(*)(void*,solver::propagate_callback*))final_eh; + user_propagator::final_eh_t _final = (bool(*)(void*,user_propagator::callback*))final_eh; to_solver_ref(s)->user_propagate_register_final(_final); Z3_CATCH; } @@ -914,7 +924,7 @@ extern "C" { Z3_eq_eh eq_eh) { Z3_TRY; RESET_ERROR_CODE(); - solver::eq_eh_t _eq = (void(*)(void*,solver::propagate_callback*,unsigned,unsigned))eq_eh; + user_propagator::eq_eh_t _eq = (void(*)(void*,user_propagator::callback*,unsigned,unsigned))eq_eh; to_solver_ref(s)->user_propagate_register_eq(_eq); Z3_CATCH; } @@ -925,7 +935,7 @@ extern "C" { Z3_eq_eh diseq_eh) { Z3_TRY; RESET_ERROR_CODE(); - solver::eq_eh_t _diseq = (void(*)(void*,solver::propagate_callback*,unsigned,unsigned))diseq_eh; + user_propagator::eq_eh_t _diseq = (void(*)(void*,user_propagator::callback*,unsigned,unsigned))diseq_eh; to_solver_ref(s)->user_propagate_register_diseq(_diseq); Z3_CATCH; } @@ -938,11 +948,19 @@ extern "C" { Z3_CATCH_RETURN(0); } + unsigned Z3_API Z3_solver_propagate_register_cb(Z3_context c, Z3_solver_callback s, Z3_ast e) { + Z3_TRY; + LOG_Z3_solver_propagate_register_cb(c, s, e); + RESET_ERROR_CODE(); + return reinterpret_cast(s)->register_cb(to_expr(e)); + Z3_CATCH_RETURN(0); + } + void Z3_API Z3_solver_propagate_consequence(Z3_context c, Z3_solver_callback s, unsigned num_fixed, unsigned const* fixed_ids, unsigned num_eqs, unsigned const* eq_lhs, unsigned const* eq_rhs, Z3_ast conseq) { Z3_TRY; LOG_Z3_solver_propagate_consequence(c, s, num_fixed, fixed_ids, num_eqs, eq_lhs, eq_rhs, conseq); RESET_ERROR_CODE(); - reinterpret_cast(s)->propagate_cb(num_fixed, fixed_ids, num_eqs, eq_lhs, eq_rhs, to_expr(conseq)); + reinterpret_cast(s)->propagate_cb(num_fixed, fixed_ids, num_eqs, eq_lhs, eq_rhs, to_expr(conseq)); Z3_CATCH; } diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 51f88a3ea..95c09e47a 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -1911,7 +1911,7 @@ namespace z3 { } inline expr bvredand(expr const & a) { assert(a.is_bv()); - Z3_ast r = Z3_mk_bvredor(a.ctx(), a); + Z3_ast r = Z3_mk_bvredand(a.ctx(), a); a.check_error(); return expr(a.ctx(), r); } @@ -4030,8 +4030,12 @@ namespace z3 { */ unsigned add(expr const& e) { - assert(s); - return Z3_solver_propagate_register(ctx(), *s, e); + if (cb) + return Z3_solver_propagate_register_cb(ctx(), cb, e); + if (s) + return Z3_solver_propagate_register(ctx(), *s, e); + assert(false); + return 0; } void conflict(unsigned num_fixed, unsigned const* fixed) { diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 6b49e9e27..9fcdfb1b5 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -1717,9 +1717,8 @@ public class Context implements AutoCloseable { * {@code [domain -> range]}, and {@code i} must have the sort * {@code domain}. The sort of the result is {@code range}. * - * @see #mkArraySort + * @see #mkArraySort(Sort[], Sort) * @see #mkStore - **/ public Expr mkSelect(Expr> a, Expr i) { @@ -1740,7 +1739,7 @@ public class Context implements AutoCloseable { * {@code [domains -> range]}, and {@code args} must have the sorts * {@code domains}. The sort of the result is {@code range}. * - * @see #mkArraySort + * @see #mkArraySort(Sort[], Sort) * @see #mkStore **/ public Expr mkSelect(Expr> a, Expr[] args) @@ -1764,7 +1763,7 @@ public class Context implements AutoCloseable { * {@code select}) on all indices except for {@code i}, where it * maps to {@code v} (and the {@code select} of {@code a} * with respect to {@code i} may be a different value). - * @see #mkArraySort + * @see #mkArraySort(Sort[], Sort) * @see #mkSelect **/ @@ -1789,7 +1788,7 @@ public class Context implements AutoCloseable { * {@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 #mkArraySort(Sort[], Sort) * @see #mkSelect **/ @@ -1807,7 +1806,7 @@ public class Context implements AutoCloseable { * Remarks: The resulting term is an array, such * that a {@code select} on an arbitrary index produces the value * {@code v}. - * @see #mkArraySort + * @see #mkArraySort(Sort[], Sort) * @see #mkSelect * **/ @@ -1827,7 +1826,7 @@ public class Context implements AutoCloseable { * {@code f} must have type {@code range_1 .. range_n -> range}. * {@code v} must have sort range. The sort of the result is * {@code [domain_i -> range]}. - * @see #mkArraySort + * @see #mkArraySort(Sort[], Sort) * @see #mkSelect * @see #mkStore diff --git a/src/api/python/z3/z3printer.py b/src/api/python/z3/z3printer.py index 7c675cc5b..228f212d9 100644 --- a/src/api/python/z3/z3printer.py +++ b/src/api/python/z3/z3printer.py @@ -770,6 +770,8 @@ class Formatter: return self.pp_set("Empty", a) elif k == Z3_OP_RE_FULL_SET: return self.pp_set("Full", a) + elif k == Z3_OP_CHAR_CONST: + return self.pp_char(a) return self.pp_name(a) def pp_int(self, a): @@ -1060,6 +1062,10 @@ class Formatter: def pp_set(self, id, a): return seq1(id, [self.pp_sort(a.sort())]) + def pp_char(self, a): + n = a.params()[0] + return to_format(str(n)) + def pp_pattern(self, a, d, xs): if a.num_args() == 1: return self.pp_expr(a.arg(0), d, xs) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 7d1366329..767eebc43 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1222,6 +1222,7 @@ typedef enum { Z3_OP_RE_COMPLEMENT, // char + Z3_OP_CHAR_CONST, Z3_OP_CHAR_LE, Z3_OP_CHAR_TO_INT, Z3_OP_CHAR_TO_BV, @@ -3450,6 +3451,10 @@ extern "C" { /** \brief Create a sort for unicode strings. + The sort for characters can be changed to ASCII by setting + the global parameter \c encoding to \c ascii, or alternative + to 16 bit characters by setting \c encoding to \c bmp. + def_API('Z3_mk_string_sort', SORT, (_in(CONTEXT), )) */ Z3_sort Z3_API Z3_mk_string_sort(Z3_context c); @@ -3458,7 +3463,8 @@ extern "C" { \brief Create a sort for unicode characters. The sort for characters can be changed to ASCII by setting - the global parameter \c unicode to \c false. + the global parameter \c encoding to \c ascii, or alternative + to 16 bit characters by setting \c encoding to \c bmp. def_API('Z3_mk_char_sort', SORT, (_in(CONTEXT), )) */ @@ -3482,8 +3488,8 @@ extern "C" { \brief Create a string constant out of the string that is passed in The string may contain escape encoding for non-printable characters or characters outside of the basic printable ASCII range. For example, - the escape encoding \u{0} represents the character 0 and the encoding - \u{100} represents the character 256. + the escape encoding \\u{0} represents the character 0 and the encoding + \\u{100} represents the character 256. def_API('Z3_mk_string', AST, (_in(CONTEXT), _in(STRING))) */ @@ -3493,7 +3499,7 @@ extern "C" { \brief Create a string constant out of the string that is passed in It takes the length of the string as well to take into account 0 characters. The string is treated as if it is unescaped so a sequence - of characters \u{0} is treated as 5 characters and not the character 0. + of characters \\u{0} is treated as 5 characters and not the character 0. def_API('Z3_mk_lstring', AST, (_in(CONTEXT), _in(UINT), _in(STRING))) */ @@ -6679,6 +6685,16 @@ extern "C" { unsigned Z3_API Z3_solver_propagate_register(Z3_context c, Z3_solver s, Z3_ast e); + /** + \brief register an expression to propagate on with the solver. + Only expressions of type Bool and type Bit-Vector can be registered for propagation. + Unlike \ref Z3_solver_propagate_register, this function takes a solver callback context + as argument. It can be invoked during a callback to register new expressions. + + def_API('Z3_solver_propagate_register_cb', UINT, (_in(CONTEXT), _in(SOLVER_CALLBACK), _in(AST))) + */ + unsigned Z3_API Z3_solver_propagate_register_cb(Z3_context c, Z3_solver_callback cb, Z3_ast e); + /** \brief propagate a consequence based on fixed values. This is a callback a client may invoke during the fixed_eh callback. diff --git a/src/ast/ast.h b/src/ast/ast.h index 739f63dc8..b04e67003 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -1050,6 +1050,12 @@ public: */ virtual bool is_value(app * a) const { return false; } + + /** + \brief return true if the expression can be used as a model value. + */ + virtual bool is_model_value(app* a) const { return is_value(a); } + /** \brief Return true if \c a is a unique plugin value. The following property should hold for unique theory values: diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index 66ce1a3ba..ce183ce6b 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -717,6 +717,8 @@ namespace datatype { todo.pop_back(); continue; } + if (!is_declared(s)) + return true; already_found.insert(datatype_name(s), GRAY); def const& d = get_def(s); bool can_process = true; diff --git a/src/ast/for_each_expr.cpp b/src/ast/for_each_expr.cpp index 2762fda38..54e176fc5 100644 --- a/src/ast/for_each_expr.cpp +++ b/src/ast/for_each_expr.cpp @@ -65,7 +65,7 @@ bool has_skolem_functions(expr * n) { } subterms::subterms(expr_ref_vector const& es, bool include_bound): m_include_bound(include_bound), m_es(es) {} -subterms::subterms(expr_ref const& e, bool include_bound) : m_include_bound(include_bound), m_es(e.m()) { m_es.push_back(e); } +subterms::subterms(expr_ref const& e, bool include_bound) : m_include_bound(include_bound), m_es(e.m()) {if (e) m_es.push_back(e); } subterms::iterator subterms::begin() { return iterator(*this, true); } subterms::iterator subterms::end() { return iterator(*this, false); } subterms::iterator::iterator(subterms& f, bool start): m_include_bound(f.m_include_bound), m_es(f.m_es) { @@ -112,7 +112,7 @@ bool subterms::iterator::operator!=(iterator const& other) const { subterms_postorder::subterms_postorder(expr_ref_vector const& es): m_es(es) {} -subterms_postorder::subterms_postorder(expr_ref const& e) : m_es(e.m()) { m_es.push_back(e); } +subterms_postorder::subterms_postorder(expr_ref const& e) : m_es(e.m()) { if (e) m_es.push_back(e); } subterms_postorder::iterator subterms_postorder::begin() { return iterator(*this, true); } subterms_postorder::iterator subterms_postorder::end() { return iterator(*this, false); } subterms_postorder::iterator::iterator(subterms_postorder& f, bool start): m_es(f.m_es) { diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index 6caef9a93..e120f7baf 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -855,6 +855,16 @@ br_status bv_rewriter::mk_bv_shl(expr * arg1, expr * arg2, expr_ref & result) { return BR_REWRITE2; } + expr* x = nullptr, *y = nullptr; + if (m_util.is_bv_shl(arg1, x, y)) { + expr_ref sum(m_util.mk_bv_add(y, arg2), m()); + expr_ref cond(m_util.mk_ule(y, sum), m()); + result = m().mk_ite(cond, + m_util.mk_bv_shl(x, sum), + mk_numeral(0, bv_size)); + return BR_REWRITE3; + } + return BR_FAILED; } @@ -1436,18 +1446,34 @@ br_status bv_rewriter::mk_bv2int(expr * arg, expr_ref & result) { bool bv_rewriter::is_mul_no_overflow(expr* e) { - if (!m_util.is_bv_mul(e)) return false; + if (!m_util.is_bv_mul(e)) + return false; unsigned sz = get_bv_size(e); unsigned sum = 0; - for (expr* x : *to_app(e)) sum += sz-num_leading_zero_bits(x); - return sum < sz; + for (expr* x : *to_app(e)) + sum += sz - num_leading_zero_bits(x); + if (sum > sz + 1) + return false; + if (sum <= sz) + return true; + rational v; + unsigned shift; + for (expr* x : *to_app(e)) + if (m_util.is_numeral(x, v) && v.is_power_of_two(shift)) + return true; + return false; } bool bv_rewriter::is_add_no_overflow(expr* e) { - if (!is_add(e)) return false; - for (expr* x : *to_app(e)) { - if (0 == num_leading_zero_bits(x)) return false; - } + if (!is_add(e)) + return false; + unsigned num_args = to_app(e)->get_num_args(); + if (num_args <= 1) + return true; + num_args -= 2; + for (expr* x : *to_app(e)) + if (num_args >= num_leading_zero_bits(x)) + return false; return true; } diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp index 557541027..55d58e3f7 100644 --- a/src/ast/rewriter/seq_axioms.cpp +++ b/src/ast/rewriter/seq_axioms.cpp @@ -205,10 +205,12 @@ namespace seq { drop_last_axiom(e, s); return; } +#if 1 if (is_extract_prefix(s, _i, _l)) { extract_prefix_axiom(e, s, l); return; } +#endif if (is_extract_suffix(s, _i, _l)) { extract_suffix_axiom(e, s, i); return; @@ -325,8 +327,7 @@ namespace seq { 0 <= l <= len(s) => len(e) = l len(s) < l => e = s */ - void axioms::extract_prefix_axiom(expr* e, expr* s, expr* l) { - + void axioms::extract_prefix_axiom(expr* e, expr* s, expr* l) { TRACE("seq", tout << "prefix " << mk_bounded_pp(e, m, 2) << " " << mk_bounded_pp(s, m, 2) << " " << mk_bounded_pp(l, m, 2) << "\n";); expr_ref le = mk_len(e); expr_ref ls = mk_len(s); @@ -1029,6 +1030,29 @@ namespace seq { add_clause(le, emp); } + /** + * Assume that r has the property that if r accepts string p + * then r does *not* accept any suffix of p. It is conceptually easy to + * convert a deterministic automaton for a regex to a suffix blocking acceptor + * by removing outgoing edges from accepting states and redirecting them + * to a sink. Alternative, introduce a different string membership predicate that is + * prefix sensitive. + * + * Let e = replace_re(s, r, t) + * Then a claim is that the following axioms suffice to encode str.replace_re + * + * s = "" => e = t + * r = "" => e = s + t + * s not in .*r.* => e = t + * s = x + y + [z] + u & y + [z] in r & x + y not in .*r.* => e = x + t + u + */ + void axioms::replace_re_axiom(expr* e) { + expr* s = nullptr, *r = nullptr, *t = nullptr; + VERIFY(seq.str.is_replace_re(e, s, r, t)); + NOT_IMPLEMENTED_YET(); + } + + /** Unit is injective: @@ -1170,4 +1194,5 @@ namespace seq { return bound_tracker; } + } diff --git a/src/ast/rewriter/seq_axioms.h b/src/ast/rewriter/seq_axioms.h index 6cd83b00f..0a2eb2ed2 100644 --- a/src/ast/rewriter/seq_axioms.h +++ b/src/ast/rewriter/seq_axioms.h @@ -106,6 +106,7 @@ namespace seq { void unit_axiom(expr* n); void length_axiom(expr* n); void unroll_not_contains(expr* e); + void replace_re_axiom(expr* e); expr_ref length_limit(expr* s, unsigned k); expr_ref is_digit(expr* ch); diff --git a/src/ast/rewriter/seq_skolem.cpp b/src/ast/rewriter/seq_skolem.cpp index 90b33c24e..c2e948216 100644 --- a/src/ast/rewriter/seq_skolem.cpp +++ b/src/ast/rewriter/seq_skolem.cpp @@ -33,6 +33,7 @@ skolem::skolem(ast_manager& m, th_rewriter& rw): m_aut_step = "aut.step"; m_pre = "seq.pre"; // (seq.pre s l): prefix of string s of length l m_post = "seq.post"; // (seq.post s l): suffix of string s of length k, based on extract starting at index i of length l + m_postp = "seq.postp"; m_eq = "seq.eq"; m_max_unfolding = "seq.max_unfolding"; m_length_limit = "seq.length_limit"; diff --git a/src/ast/rewriter/seq_skolem.h b/src/ast/rewriter/seq_skolem.h index 1a5928a0b..913942b8a 100644 --- a/src/ast/rewriter/seq_skolem.h +++ b/src/ast/rewriter/seq_skolem.h @@ -37,7 +37,8 @@ namespace seq { symbol m_aut_step; // regex unfolding state symbol m_accept; // regex symbol m_is_empty, m_is_non_empty; // regex emptiness check - symbol m_pre, m_post; // inverse of at: (pre s i) + (at s i) + (post s i) = s if 0 <= i < (len s) + symbol m_pre, m_post; // inverse of at: (pre s i) + (at s i) + (post s i) = s if 0 <= i < (len s) + symbol m_postp; symbol m_eq; // equality atom symbol m_max_unfolding, m_length_limit; @@ -84,6 +85,7 @@ namespace seq { expr_ref mk_tail(expr* s, expr* i) { return mk(m_tail, s, i); } expr_ref mk_post(expr* s, expr* i) { return mk(m_post, s, i); } + expr_ref mk_postp(expr* s, expr* i) { return mk(m_postp, s, i); } expr_ref mk_ite(expr* c, expr* t, expr* e) { return mk(symbol("seq.if"), c, t, e, nullptr, t->get_sort()); } expr_ref mk_last(expr* s); expr_ref mk_first(expr* s); diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index ebae138e3..0829aa09f 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -705,6 +705,17 @@ bool seq_decl_plugin::is_value(app* e) const { } } +bool seq_decl_plugin::is_model_value(app* e) const { + if (is_app_of(e, m_family_id, OP_SEQ_EMPTY)) + return true; + if (is_app_of(e, m_family_id, OP_STRING_CONST)) + return true; + if (is_app_of(e, m_family_id, OP_SEQ_UNIT) && + m_manager->is_value(e->get_arg(0))) + return true; + return false; +} + bool seq_decl_plugin::are_equal(app* a, app* b) const { if (a == b) return true; // handle concatenations diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index f194e6a67..09a10ee9a 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -179,6 +179,8 @@ public: bool is_value(app * e) const override; + bool is_model_value(app* e) const override; + bool is_unique_value(app * e) const override; bool are_equal(app* a, app* b) const override; diff --git a/src/ast/static_features.cpp b/src/ast/static_features.cpp index f6c0a59ae..c58ff254c 100644 --- a/src/ast/static_features.cpp +++ b/src/ast/static_features.cpp @@ -406,12 +406,25 @@ void static_features::process(expr * e, bool form_ctx, bool or_and_ctx, bool ite } if (stack_depth > m_max_stack_depth) { - for (expr* arg : subterms::ground(expr_ref(e, m))) - if (get_depth(arg) <= 3 || is_quantifier(arg)) - process(arg, form_ctx, or_and_ctx, ite_ctx, stack_depth - 10); + ptr_vector todo; + todo.push_back(e); + for (unsigned i = 0; i < todo.size(); ++i) { + e = todo[i]; + if (is_marked(e)) + continue; + if (is_basic_expr(e)) { + mark(e); + todo.append(to_app(e)->get_num_args(), to_app(e)->get_args()); + } + else { + process(e, form_ctx, or_and_ctx, ite_ctx, stack_depth - 10); + } + } return; } + mark(e); + update_core(e); if (is_quantifier(e)) { diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index 9b11f883a..3aaf8f29e 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -324,6 +324,7 @@ static void set_upper(impq & u, bool & inf_u, impq const & v) { } } +// this function assumes that all basic columns dependend on j are feasible bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq & l, bool & inf_u, impq & u, mpq & m) { if (lrac.m_r_heading[j] >= 0) // the basic var return false; @@ -336,62 +337,52 @@ bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq l = u = zero_of_type(); m = mpq(1); - if (has_lower(j)) { + if (has_lower(j)) set_lower(l, inf_l, lower_bound(j) - xj); - } - if (has_upper(j)) { + + if (has_upper(j)) set_upper(u, inf_u, upper_bound(j) - xj); - } + - unsigned row_index; lp_assert(settings().use_tableau()); const auto & A = lra.A_r(); - unsigned rounds = 0; - for (auto c : A.column(j)) { - row_index = c.var(); - const mpq & a = c.coeff(); - unsigned i = lrac.m_r_basis[row_index]; - TRACE("random_update", tout << "i = " << i << ", a = " << a << "\n";); - if (column_is_int(i) && !a.is_int()) - m = lcm(m, denominator(a)); - } TRACE("random_update", tout << "m = " << m << "\n";); + auto delta = [](mpq const& x, impq const& y, impq const& z) { + if (x.is_one()) + return y - z; + if (x.is_minus_one()) + return z - y; + return (y - z) / x; + }; + for (auto c : A.column(j)) { - if (!inf_l && !inf_u && l >= u) break; - row_index = c.var(); + unsigned row_index = c.var(); const mpq & a = c.coeff(); unsigned i = lrac.m_r_basis[row_index]; impq const & xi = get_value(i); + lp_assert(lrac.m_r_solver.column_is_feasible(i)); + if (column_is_int(i) && !a.is_int()) + m = lcm(m, denominator(a)); -#define SET_BOUND(_fn_, a, b, x, y, z) \ - if (x.is_one()) \ - _fn_(a, b, y - z); \ - else if (x.is_minus_one()) \ - _fn_(a, b, z - y); \ - else if (z == y) \ - _fn_(a, b, zero_of_type()); \ - else \ - { _fn_(a, b, (y - z)/x); } \ + if (!inf_l && !inf_u) { + if (l == u) + continue; + } if (a.is_neg()) { - if (has_lower(i)) { - SET_BOUND(set_lower, l, inf_l, a, xi, lrac.m_r_lower_bounds()[i]); - } - if (has_upper(i)) { - SET_BOUND(set_upper, u, inf_u, a, xi, lrac.m_r_upper_bounds()[i]); - } + if (has_lower(i)) + set_lower(l, inf_l, delta(a, xi, lrac.m_r_lower_bounds()[i])); + if (has_upper(i)) + set_upper(u, inf_u, delta(a, xi, lrac.m_r_upper_bounds()[i])); } else { - if (has_upper(i)) { - SET_BOUND(set_lower, l, inf_l, a, xi, lrac.m_r_upper_bounds()[i]); - } - if (has_lower(i)) { - SET_BOUND(set_upper, u, inf_u, a, xi, lrac.m_r_lower_bounds()[i]); - } + if (has_upper(i)) + set_lower(l, inf_l, delta(a, xi, lrac.m_r_upper_bounds()[i])); + if (has_lower(i)) + set_upper(u, inf_u, delta(a, xi, lrac.m_r_lower_bounds()[i])); } - ++rounds; } l += xj; @@ -545,7 +536,7 @@ for (const auto &c : row) } std::ostream& int_solver::display_row_info(std::ostream & out, unsigned row_index) const { auto & rslv = lrac.m_r_solver; - auto row = rslv.m_A.m_rows[row_index]; + auto const& row = rslv.m_A.m_rows[row_index]; return display_row(out, row); } diff --git a/src/math/lp/lar_core_solver_def.h b/src/math/lp/lar_core_solver_def.h index 06f414d11..f20aa7e6b 100644 --- a/src/math/lp/lar_core_solver_def.h +++ b/src/math/lp/lar_core_solver_def.h @@ -179,11 +179,17 @@ void lar_core_solver::solve() { } lp_assert(!settings().use_tableau() || r_basis_is_OK()); } - if (m_r_solver.get_status() == lp_status::INFEASIBLE) { + switch (m_r_solver.get_status()) + { + case lp_status::INFEASIBLE: fill_not_improvable_zero_sum(); - } - else if (m_r_solver.get_status() != lp_status::UNBOUNDED) { + break; + case lp_status::CANCELLED: + case lp_status::UNBOUNDED: // do nothing in these cases + break; + default: // adjust the status to optimal m_r_solver.set_status(lp_status::OPTIMAL); + break; } lp_assert(r_basis_is_OK()); lp_assert(m_r_solver.non_basic_columns_are_set_correctly()); diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index 561a94e99..f78dab119 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -798,6 +798,18 @@ namespace lp { } + // this function just looks at the status + bool lar_solver::is_feasible() const { + switch (this->get_status()) { + case lp_status::OPTIMAL: + case lp_status::FEASIBLE: + case lp_status::UNBOUNDED: + return true; + default: + return false; + } + } + numeric_pair lar_solver::get_basic_var_value_from_row(unsigned i) { numeric_pair r = zero_of_type>(); diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index b4c69d783..1cd776cc2 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -296,6 +296,8 @@ class lar_solver : public column_namer { mutable mpq m_delta; public: + // this function just looks at the status + bool is_feasible() const; const map, default_eq>& fixed_var_table_int() const { return m_fixed_var_table_int; } @@ -555,6 +557,10 @@ public: return m_mpq_lar_core_solver.column_is_bounded(j); } + bool check_feasible() const { + return m_mpq_lar_core_solver.m_r_solver.calc_current_x_is_feasible_include_non_basis(); + } + std::pair add_equality(lpvar j, lpvar k); inline void get_bound_constraint_witnesses_for_column(unsigned j, constraint_index & lc, constraint_index & uc) const { diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h index 1ea872517..14f646fc1 100644 --- a/src/math/lp/lp_bound_propagator.h +++ b/src/math/lp/lp_bound_propagator.h @@ -116,28 +116,42 @@ class lp_bound_propagator { map, default_eq> m_val2fixed_row; + + bool is_fixed_row(unsigned r, unsigned & x) { + x = UINT_MAX; + const auto & row = lp().get_row(r); + for (unsigned k = 0; k < row.size(); k++) { + const auto& c = row[k]; + if (column_is_fixed(c.var())) + continue; + if (x != UINT_MAX) + return false; + x = c.var(); + } + return x != UINT_MAX; + } - void try_add_equation_with_internal_fixed_tables(unsigned r1, vertex const* v) { + void try_add_equation_with_internal_fixed_tables(unsigned r1) { SASSERT(m_fixed_vertex); - if (v != m_root) + unsigned v1, v2; + if (!is_fixed_row(r1, v1)) return; - unsigned v1 = v->column(); unsigned r2 = UINT_MAX; if (!m_val2fixed_row.find(val(v1), r2) || r2 >= lp().row_count()) { m_val2fixed_row.insert(val(v1), r1); return; } - unsigned v2, v3; - int polarity; - if (!is_tree_offset_row(r2, v2, v3, polarity) || !not_set(v3) || - is_int(v1) != is_int(v2) || val(v1) != val(v2)) { + if (!is_fixed_row(r2, v2) || val(v1) != val(v2) || is_int(v1) != is_int(v2)) { m_val2fixed_row.insert(val(v1), r1); return; } + if (v1 == v2) + return; explanation ex; explain_fixed_in_row(r1, ex); explain_fixed_in_row(r2, ex); + TRACE("eq", print_row(tout, r1); print_row(tout, r2); tout << v1 << " == " << v2 << " = " << val(v1) << "\n"); add_eq_on_columns(ex, v1, v2, true); } @@ -146,7 +160,7 @@ class lp_bound_propagator { unsigned v_j = v->column(); unsigned j = null_lpvar; if (!lp().find_in_fixed_tables(val(v_j), is_int(v_j), j)) { - // try_add_equation_with_internal_fixed_tables(row_index, v); + try_add_equation_with_internal_fixed_tables(row_index); return; } diff --git a/src/math/lp/lp_dual_core_solver_def.h b/src/math/lp/lp_dual_core_solver_def.h index 1e6553458..4a847fe85 100644 --- a/src/math/lp/lp_dual_core_solver_def.h +++ b/src/math/lp/lp_dual_core_solver_def.h @@ -100,10 +100,7 @@ template bool lp_dual_core_solver::done() { if (this->get_status() == lp_status::OPTIMAL) { return true; } - if (this->total_iterations() > this->m_settings.max_total_number_of_iterations) { // debug !!!! - this->set_status(lp_status::ITERATIONS_EXHAUSTED); - return true; - } + return false; // todo, need to be more cases } @@ -747,6 +744,6 @@ template void lp_dual_core_solver::solve() { // s one_iteration(); } while (this->get_status() != lp_status::FLOATING_POINT_ERROR && this->get_status() != lp_status::DUAL_UNBOUNDED && this->get_status() != lp_status::OPTIMAL && this->iters_with_no_cost_growing() <= this->m_settings.max_number_of_iterations_with_no_improvements - && this->total_iterations() <= this->m_settings.max_total_number_of_iterations); + ); } } diff --git a/src/math/lp/lp_dual_simplex_def.h b/src/math/lp/lp_dual_simplex_def.h index 1b12106ea..34079cd94 100644 --- a/src/math/lp/lp_dual_simplex_def.h +++ b/src/math/lp/lp_dual_simplex_def.h @@ -31,9 +31,6 @@ template void lp_dual_simplex::decide_on_status_a break; case lp_status::DUAL_UNBOUNDED: lp_unreachable(); - case lp_status::ITERATIONS_EXHAUSTED: - this->m_status = lp_status::ITERATIONS_EXHAUSTED; - break; case lp_status::TIME_EXHAUSTED: this->m_status = lp_status::TIME_EXHAUSTED; break; diff --git a/src/math/lp/lp_primal_core_solver_def.h b/src/math/lp/lp_primal_core_solver_def.h index aeaf485a7..75eff208a 100644 --- a/src/math/lp/lp_primal_core_solver_def.h +++ b/src/math/lp/lp_primal_core_solver_def.h @@ -956,8 +956,6 @@ template unsigned lp_primal_core_solver::solve() && this->iters_with_no_cost_growing() <= this->m_settings.max_number_of_iterations_with_no_improvements && - this->total_iterations() <= this->m_settings.max_total_number_of_iterations - && !(this->current_x_is_feasible() && this->m_look_for_feasible_solution_only)); lp_assert(this->get_status() == lp_status::FLOATING_POINT_ERROR @@ -1097,10 +1095,8 @@ template bool lp_primal_core_solver::done() { return true; } if (this->m_iters_with_no_cost_growing >= this->m_settings.max_number_of_iterations_with_no_improvements) { - this->get_status() = lp_status::ITERATIONS_EXHAUSTED; return true; - } - if (this->total_iterations() >= this->m_settings.max_total_number_of_iterations) { - this->get_status() = lp_status::ITERATIONS_EXHAUSTED; return true; + this->set_status(lp_status::CANCELLED); + return true; } return false; } diff --git a/src/math/lp/lp_primal_core_solver_tableau_def.h b/src/math/lp/lp_primal_core_solver_tableau_def.h index 115e1a344..03f07115b 100644 --- a/src/math/lp/lp_primal_core_solver_tableau_def.h +++ b/src/math/lp/lp_primal_core_solver_tableau_def.h @@ -182,9 +182,7 @@ unsigned lp_primal_core_solver::solve_with_tableau() { if (this->m_settings.get_cancel_flag() || this->iters_with_no_cost_growing() > this->m_settings.max_number_of_iterations_with_no_improvements - || - this->total_iterations() > this->m_settings.max_total_number_of_iterations - ) { + ) { this->set_status(lp_status::CANCELLED); break; // from the loop } diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index 7a0fef5c7..2be55dcb1 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -71,7 +71,6 @@ enum class lp_status { FEASIBLE, FLOATING_POINT_ERROR, TIME_EXHAUSTED, - ITERATIONS_EXHAUSTED, EMPTY, UNSTABLE, CANCELLED @@ -210,7 +209,6 @@ public: double harris_feasibility_tolerance { 1e-7 }; // page 179 of Istvan Maros double ignore_epsilon_of_harris { 10e-5 }; unsigned max_number_of_iterations_with_no_improvements { 2000000 }; - unsigned max_total_number_of_iterations { 20000000 }; double time_limit; // the maximum time limit of the total run time in seconds // dual section double dual_feasibility_tolerance { 1e-7 }; // page 71 of the PhD thesis of Achim Koberstein diff --git a/src/math/lp/lp_settings_def.h b/src/math/lp/lp_settings_def.h index 247cb98d3..4c783049c 100644 --- a/src/math/lp/lp_settings_def.h +++ b/src/math/lp/lp_settings_def.h @@ -45,7 +45,6 @@ const char* lp_status_to_string(lp_status status) { case lp_status::FEASIBLE: return "FEASIBLE"; case lp_status::FLOATING_POINT_ERROR: return "FLOATING_POINT_ERROR"; case lp_status::TIME_EXHAUSTED: return "TIME_EXHAUSTED"; - case lp_status::ITERATIONS_EXHAUSTED: return "ITERATIONS_EXHAUSTED"; case lp_status::EMPTY: return "EMPTY"; case lp_status::UNSTABLE: return "UNSTABLE"; default: @@ -62,7 +61,6 @@ lp_status lp_status_from_string(std::string status) { if (status == "FEASIBLE") return lp_status::FEASIBLE; if (status == "FLOATING_POINT_ERROR") return lp_status::FLOATING_POINT_ERROR; if (status == "TIME_EXHAUSTED") return lp_status::TIME_EXHAUSTED; - if (status == "ITERATIONS_EXHAUSTED") return lp_status::ITERATIONS_EXHAUSTED; if (status == "EMPTY") return lp_status::EMPTY; lp_unreachable(); return lp_status::UNKNOWN; // it is unreachable diff --git a/src/math/lp/lp_solver.h b/src/math/lp/lp_solver.h index 9b0b8fb0a..68beca06f 100644 --- a/src/math/lp/lp_solver.h +++ b/src/math/lp/lp_solver.h @@ -158,13 +158,7 @@ public: m_settings.time_limit = time_limit_in_seconds; } - void set_max_iterations_per_stage(unsigned max_iterations) { - m_settings.max_total_number_of_iterations = max_iterations; - } - - unsigned get_max_iterations_per_stage() const { - return m_settings.max_total_number_of_iterations; - } + protected: bool problem_is_empty(); diff --git a/src/math/lp/random_updater_def.h b/src/math/lp/random_updater_def.h index aca4e1d65..25ef6f82f 100644 --- a/src/math/lp/random_updater_def.h +++ b/src/math/lp/random_updater_def.h @@ -51,25 +51,23 @@ bool random_updater::shift_var(unsigned j) { void random_updater::update() { + // VERIFY(m_lar_solver.check_feasible()); auto columns = m_var_set.index(); // m_var_set is going to change during the loop for (auto j : columns) { if (!m_var_set.contains(j)) { TRACE("lar_solver_rand", tout << "skipped " << j << "\n";); continue; } - if (!m_lar_solver.is_base(j)) { + if (!m_lar_solver.is_base(j)) shift_var(j); - } else { + else { unsigned row_index = m_lar_solver.r_heading()[j]; for (auto & row_c : m_lar_solver.get_row(row_index)) { unsigned cj = row_c.var(); if (!m_lar_solver.is_base(cj) && - !m_lar_solver.column_is_fixed(cj) - && - shift_var(cj) - ) { - break; // done with the basic var j - } + !m_lar_solver.column_is_fixed(cj) && + shift_var(cj)) + break; // done with the basic var j } } } diff --git a/src/math/subpaving/tactic/subpaving_tactic.cpp b/src/math/subpaving/tactic/subpaving_tactic.cpp index c453806bf..1bc0cb630 100644 --- a/src/math/subpaving/tactic/subpaving_tactic.cpp +++ b/src/math/subpaving/tactic/subpaving_tactic.cpp @@ -220,6 +220,8 @@ public: dealloc(m_imp); } + char const* name() const override { return "subpaving"; } + tactic * translate(ast_manager & m) override { return alloc(subpaving_tactic, m, m_params); } diff --git a/src/muz/fp/horn_tactic.cpp b/src/muz/fp/horn_tactic.cpp index 591e57944..b66ddf275 100644 --- a/src/muz/fp/horn_tactic.cpp +++ b/src/muz/fp/horn_tactic.cpp @@ -392,6 +392,8 @@ public: dealloc(m_imp); } + char const* name() const override { return "horn"; } + void updt_params(params_ref const & p) override { m_params = p; m_imp->updt_params(p); diff --git a/src/nlsat/tactic/nlsat_tactic.cpp b/src/nlsat/tactic/nlsat_tactic.cpp index 8de478199..ddf85ce19 100644 --- a/src/nlsat/tactic/nlsat_tactic.cpp +++ b/src/nlsat/tactic/nlsat_tactic.cpp @@ -223,6 +223,8 @@ public: SASSERT(m_imp == 0); } + char const* name() const override { return "nlsat"; } + void updt_params(params_ref const & p) override { m_params = p; } diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp index 0bc7ba986..21489be58 100644 --- a/src/opt/optsmt.cpp +++ b/src/opt/optsmt.cpp @@ -305,11 +305,9 @@ namespace opt { expr_ref fml(m), bound(m.mk_true(), m), tmp(m); expr* vars[1]; { - for (unsigned i = 0; i < m_upper.size(); ++i) { + for (unsigned i = 0; i < m_upper.size(); ++i) ors.push_back(m_s->mk_ge(i, m_upper[i])); - } - - + fml = mk_or(ors); tmp = m.mk_fresh_const("b", m.mk_bool_sort()); fml = m.mk_implies(tmp, fml); @@ -328,8 +326,7 @@ namespace opt { m_s->get_model(m_model); m_s->get_labels(m_labels); for (unsigned i = 0; i < ors.size(); ++i) { - expr_ref tmp(m); - if (m_model->is_true(ors[i].get())) { + if (m_model->is_true(ors.get(i))) { m_lower[i] = m_upper[i]; ors[i] = m.mk_false(); disj[i] = m.mk_false(); diff --git a/src/qe/nlqsat.cpp b/src/qe/nlqsat.cpp index 6439a91c9..28cfa5c3e 100644 --- a/src/qe/nlqsat.cpp +++ b/src/qe/nlqsat.cpp @@ -839,6 +839,8 @@ namespace qe { ~nlqsat() override { } + char const* name() const override { return "nlqsat"; } + void updt_params(params_ref const & p) override { params_ref p2(p); p2.set_bool("factor", false); diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp index 58fe3b293..f6dd9c712 100644 --- a/src/qe/qe_lite.cpp +++ b/src/qe/qe_lite.cpp @@ -2459,6 +2459,8 @@ public: m_params(p), m_qe(m, p, true) {} + char const* name() const override { return "qe_lite"; } + tactic * translate(ast_manager & m) override { return alloc(qe_lite_tactic, m, m_params); } diff --git a/src/qe/qe_tactic.cpp b/src/qe/qe_tactic.cpp index 0aa3824e7..da1ce5efd 100644 --- a/src/qe/qe_tactic.cpp +++ b/src/qe/qe_tactic.cpp @@ -100,6 +100,8 @@ public: dealloc(m_imp); } + char const* name() const override { return "qe"; } + void updt_params(params_ref const & p) override { m_params = p; m_imp->updt_params(p); diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index 537a7ab56..767b96e5d 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -1257,6 +1257,8 @@ namespace qe { ~qsat() override { clear(); } + + char const* name() const override { return "qsat"; } void updt_params(params_ref const & p) override { } diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index e5fd2ef70..51f2c3d98 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -342,9 +342,7 @@ namespace sat { clause* solver::mk_clause(unsigned num_lits, literal * lits, sat::status st) { m_model_is_current = false; - for (unsigned i = 0; i < num_lits; i++) - VERIFY(!was_eliminated(lits[i])); - + DEBUG_CODE({ for (unsigned i = 0; i < num_lits; i++) { CTRACE("sat", was_eliminated(lits[i]), tout << lits[i] << " was eliminated\n";); diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index e2ce43637..ea81f0c4d 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -661,25 +661,25 @@ public: void user_propagate_init( void* ctx, - solver::push_eh_t& push_eh, - solver::pop_eh_t& pop_eh, - solver::fresh_eh_t& fresh_eh) override { + user_propagator::push_eh_t& push_eh, + user_propagator::pop_eh_t& pop_eh, + user_propagator::fresh_eh_t& fresh_eh) override { ensure_euf()->user_propagate_init(ctx, push_eh, pop_eh, fresh_eh); } - void user_propagate_register_fixed(solver::fixed_eh_t& fixed_eh) override { + void user_propagate_register_fixed(user_propagator::fixed_eh_t& fixed_eh) override { ensure_euf()->user_propagate_register_fixed(fixed_eh); } - void user_propagate_register_final(solver::final_eh_t& final_eh) override { + void user_propagate_register_final(user_propagator::final_eh_t& final_eh) override { ensure_euf()->user_propagate_register_final(final_eh); } - void user_propagate_register_eq(solver::eq_eh_t& eq_eh) override { + void user_propagate_register_eq(user_propagator::eq_eh_t& eq_eh) override { ensure_euf()->user_propagate_register_eq(eq_eh); } - void user_propagate_register_diseq(solver::eq_eh_t& diseq_eh) override { + void user_propagate_register_diseq(user_propagator::eq_eh_t& diseq_eh) override { ensure_euf()->user_propagate_register_diseq(diseq_eh); } @@ -959,11 +959,11 @@ private: extract_asm2dep(asm2dep); sat::literal_vector const& core = m_solver.get_core(); TRACE("sat", - for (auto kv : m_dep2asm) { + for (auto const& kv : m_dep2asm) { tout << mk_pp(kv.m_key, m) << " |-> " << sat::literal(kv.m_value) << "\n"; } tout << "asm2fml: "; - for (auto kv : asm2fml) { + for (auto const& kv : asm2fml) { tout << mk_pp(kv.m_key, m) << " |-> " << mk_pp(kv.m_value, m) << "\n"; } tout << "core: "; for (auto c : core) tout << c << " "; tout << "\n"; diff --git a/src/sat/smt/arith_internalize.cpp b/src/sat/smt/arith_internalize.cpp index f28948868..882dd23b0 100644 --- a/src/sat/smt/arith_internalize.cpp +++ b/src/sat/smt/arith_internalize.cpp @@ -308,7 +308,6 @@ namespace arith { bool solver::internalize_atom(expr* atom) { TRACE("arith", tout << mk_pp(atom, m) << "\n";); - SASSERT(!ctx.get_enode(atom)); expr* n1, *n2; rational r; lp_api::bound_kind k; diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index 049bf0ce2..da68691c7 100644 --- a/src/sat/smt/arith_solver.cpp +++ b/src/sat/smt/arith_solver.cpp @@ -627,8 +627,9 @@ namespace arith { else if (use_nra_model() && lp().external_to_local(v) != lp::null_lpvar) { anum const& an = nl_value(v, *m_a1); if (a.is_int(o) && !m_nla->am().is_int(an)) - value = a.mk_numeral(rational::zero(), a.is_int(o)); - //value = a.mk_numeral(m_nla->am(), nl_value(v, *m_a1), a.is_int(o)); + value = a.mk_numeral(rational::zero(), a.is_int(o)); + else + value = a.mk_numeral(m_nla->am(), nl_value(v, *m_a1), a.is_int(o)); } else if (v != euf::null_theory_var) { rational r = get_value(v); @@ -985,7 +986,7 @@ namespace arith { IF_VERBOSE(12, verbose_stream() << "final-check " << lp().get_status() << "\n"); SASSERT(lp().ax_is_correct()); - if (lp().get_status() != lp::lp_status::OPTIMAL || lp().has_changed_columns()) { + if (!lp().is_feasible() || lp().has_changed_columns()) { switch (make_feasible()) { case l_false: get_infeasibility_explanation_and_set_conflict(); @@ -1096,6 +1097,8 @@ namespace arith { return l_false; case lp::lp_status::FEASIBLE: case lp::lp_status::OPTIMAL: + case lp::lp_status::UNBOUNDED: + SASSERT(!lp().has_changed_columns()); return l_true; case lp::lp_status::TIME_EXHAUSTED: default: diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp index 21a02909e..ea5bfe274 100644 --- a/src/sat/smt/euf_model.cpp +++ b/src/sat/smt/euf_model.cpp @@ -131,6 +131,7 @@ namespace euf { void solver::dependencies2values(user_sort& us, deps_t& deps, model_ref& mdl) { for (enode* n : deps.top_sorted()) { + TRACE("model", tout << bpp(n->get_root()) << "\n"); unsigned id = n->get_root_id(); if (m_values.get(id, nullptr)) continue; diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index 2af8485c1..bbdd6ce0e 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -295,7 +295,7 @@ namespace euf { return; bool sign = l.sign(); m_egraph.set_value(n, sign ? l_false : l_true); - for (auto th : enode_th_vars(n)) + for (auto const& th : enode_th_vars(n)) m_id2solver[th.get_id()]->asserted(l); size_t* c = to_ptr(l); @@ -519,8 +519,7 @@ namespace euf { void solver::push() { si.push(); - scope s; - s.m_var_lim = m_var_trail.size(); + scope s(m_var_trail.size()); m_scopes.push_back(s); m_trail.push_scope(); for (auto* e : m_solvers) @@ -994,9 +993,9 @@ namespace euf { void solver::user_propagate_init( void* ctx, - ::solver::push_eh_t& push_eh, - ::solver::pop_eh_t& pop_eh, - ::solver::fresh_eh_t& fresh_eh) { + user_propagator::push_eh_t& push_eh, + user_propagator::pop_eh_t& pop_eh, + user_propagator::fresh_eh_t& fresh_eh) { m_user_propagator = alloc(user_solver::solver, *this); m_user_propagator->add(ctx, push_eh, pop_eh, fresh_eh); for (unsigned i = m_scopes.size(); i-- > 0; ) diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index 0df07faff..d70206d11 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -72,6 +72,7 @@ namespace euf { }; struct scope { unsigned m_var_lim; + scope(unsigned l) : m_var_lim(l) {} }; @@ -400,27 +401,27 @@ namespace euf { // user propagator void user_propagate_init( void* ctx, - ::solver::push_eh_t& push_eh, - ::solver::pop_eh_t& pop_eh, - ::solver::fresh_eh_t& fresh_eh); + user_propagator::push_eh_t& push_eh, + user_propagator::pop_eh_t& pop_eh, + user_propagator::fresh_eh_t& fresh_eh); bool watches_fixed(enode* n) const; void assign_fixed(enode* n, expr* val, unsigned sz, literal const* explain); void assign_fixed(enode* n, expr* val, literal_vector const& explain) { assign_fixed(n, val, explain.size(), explain.data()); } void assign_fixed(enode* n, expr* val, literal explain) { assign_fixed(n, val, 1, &explain); } - void user_propagate_register_final(::solver::final_eh_t& final_eh) { + void user_propagate_register_final(user_propagator::final_eh_t& final_eh) { check_for_user_propagator(); m_user_propagator->register_final(final_eh); } - void user_propagate_register_fixed(::solver::fixed_eh_t& fixed_eh) { + void user_propagate_register_fixed(user_propagator::fixed_eh_t& fixed_eh) { check_for_user_propagator(); m_user_propagator->register_fixed(fixed_eh); } - void user_propagate_register_eq(::solver::eq_eh_t& eq_eh) { + void user_propagate_register_eq(user_propagator::eq_eh_t& eq_eh) { check_for_user_propagator(); m_user_propagator->register_eq(eq_eh); } - void user_propagate_register_diseq(::solver::eq_eh_t& diseq_eh) { + void user_propagate_register_diseq(user_propagator::eq_eh_t& diseq_eh) { check_for_user_propagator(); m_user_propagator->register_diseq(diseq_eh); } diff --git a/src/sat/smt/sat_dual_solver.cpp b/src/sat/smt/sat_dual_solver.cpp index 599caf6e5..86d73a2d8 100644 --- a/src/sat/smt/sat_dual_solver.cpp +++ b/src/sat/smt/sat_dual_solver.cpp @@ -22,6 +22,7 @@ namespace sat { m_solver(m_params, l) { SASSERT(!m_solver.get_config().m_drat); + m_solver.set_incremental(true); } void dual_solver::flush() { @@ -104,10 +105,10 @@ namespace sat { root = ext2lit(clause[0]); else { root = literal(m_solver.mk_var(), false); - m_solver.set_external(root.var()); for (unsigned i = 0; i < sz; ++i) m_solver.mk_clause(root, ~ext2lit(clause[i]), status::input()); - } + } + m_solver.set_external(root.var()); m_roots.push_back(~root); TRACE("dual", tout << "root: " << ~root << " => " << literal_vector(sz, clause) << "\n";); } diff --git a/src/sat/smt/sat_dual_solver.h b/src/sat/smt/sat_dual_solver.h index d0465ac32..08a31084e 100644 --- a/src/sat/smt/sat_dual_solver.h +++ b/src/sat/smt/sat_dual_solver.h @@ -23,7 +23,13 @@ Author: namespace sat { class dual_solver { - no_drat_params m_params; + class dual_params : public no_drat_params { + public: + dual_params() { + set_bool("core.minimize", false); + } + }; + dual_params m_params; solver m_solver; lim_svector m_units, m_roots; lim_svector m_tracked_vars; diff --git a/src/sat/smt/user_solver.cpp b/src/sat/smt/user_solver.cpp index 5a1a07f11..edbaf6d8d 100644 --- a/src/sat/smt/user_solver.cpp +++ b/src/sat/smt/user_solver.cpp @@ -47,6 +47,10 @@ namespace user_solver { DEBUG_CODE(validate_propagation();); } + unsigned solver::register_cb(expr* e) { + return add_expr(e); + } + sat::check_result solver::check() { if (!(bool)m_final_eh) return sat::check_result::CR_DONE; diff --git a/src/sat/smt/user_solver.h b/src/sat/smt/user_solver.h index 2939a2f0a..b11742608 100644 --- a/src/sat/smt/user_solver.h +++ b/src/sat/smt/user_solver.h @@ -21,11 +21,12 @@ Author: #include "sat/smt/sat_th.h" #include "solver/solver.h" +#include "tactic/user_propagator_base.h" namespace user_solver { - class solver : public euf::th_euf_solver, public ::solver::propagate_callback { + class solver : public euf::th_euf_solver, public user_propagator::callback { struct prop_info { unsigned_vector m_ids; @@ -47,15 +48,15 @@ namespace user_solver { }; void* m_user_context; - ::solver::push_eh_t m_push_eh; - ::solver::pop_eh_t m_pop_eh; - ::solver::fresh_eh_t m_fresh_eh; - ::solver::final_eh_t m_final_eh; - ::solver::fixed_eh_t m_fixed_eh; - ::solver::eq_eh_t m_eq_eh; - ::solver::eq_eh_t m_diseq_eh; - ::solver::context_obj* m_api_context { nullptr }; - unsigned m_qhead { 0 }; + user_propagator::push_eh_t m_push_eh; + user_propagator::pop_eh_t m_pop_eh; + user_propagator::fresh_eh_t m_fresh_eh; + user_propagator::final_eh_t m_final_eh; + user_propagator::fixed_eh_t m_fixed_eh; + user_propagator::eq_eh_t m_eq_eh; + user_propagator::eq_eh_t m_diseq_eh; + user_propagator::context_obj* m_api_context = nullptr; + unsigned m_qhead = 0; vector m_prop; unsigned_vector m_prop_lim; vector m_id2justification; @@ -91,9 +92,9 @@ namespace user_solver { */ void add( void* ctx, - ::solver::push_eh_t& push_eh, - ::solver::pop_eh_t& pop_eh, - ::solver::fresh_eh_t& fresh_eh) { + user_propagator::push_eh_t& push_eh, + user_propagator::pop_eh_t& pop_eh, + user_propagator::fresh_eh_t& fresh_eh) { m_user_context = ctx; m_push_eh = push_eh; m_pop_eh = pop_eh; @@ -102,14 +103,15 @@ namespace user_solver { unsigned add_expr(expr* e); - void register_final(::solver::final_eh_t& final_eh) { m_final_eh = final_eh; } - void register_fixed(::solver::fixed_eh_t& fixed_eh) { m_fixed_eh = fixed_eh; } - void register_eq(::solver::eq_eh_t& eq_eh) { m_eq_eh = eq_eh; } - void register_diseq(::solver::eq_eh_t& diseq_eh) { m_diseq_eh = diseq_eh; } + void register_final(user_propagator::final_eh_t& final_eh) { m_final_eh = final_eh; } + void register_fixed(user_propagator::fixed_eh_t& fixed_eh) { m_fixed_eh = fixed_eh; } + void register_eq(user_propagator::eq_eh_t& eq_eh) { m_eq_eh = eq_eh; } + void register_diseq(user_propagator::eq_eh_t& diseq_eh) { m_diseq_eh = diseq_eh; } bool has_fixed() const { return (bool)m_fixed_eh; } void propagate_cb(unsigned num_fixed, unsigned const* fixed_ids, unsigned num_eqs, unsigned const* lhs, unsigned const* rhs, expr* conseq) override; + unsigned register_cb(expr* e) override; void new_fixed_eh(euf::theory_var v, expr* value, unsigned num_lits, sat::literal const* jlits); diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp index 521a70fb7..38c25eae3 100644 --- a/src/sat/tactic/sat_tactic.cpp +++ b/src/sat/tactic/sat_tactic.cpp @@ -198,6 +198,8 @@ public: SASSERT(m_imp == 0); } + char const* name() const override { return "sat"; } + void updt_params(params_ref const & p) override { m_params = p; if (m_imp) m_imp->updt_params(p); diff --git a/src/smt/CMakeLists.txt b/src/smt/CMakeLists.txt index 9d2a2b406..e6ee97046 100644 --- a/src/smt/CMakeLists.txt +++ b/src/smt/CMakeLists.txt @@ -70,9 +70,9 @@ z3_add_component(smt theory_str.cpp theory_str_mc.cpp theory_str_regex.cpp + theory_user_propagator.cpp theory_utvpi.cpp theory_wmaxsat.cpp - user_propagator.cpp uses_theory.cpp watch_list.cpp COMPONENT_DEPENDENCIES diff --git a/src/smt/seq_eq_solver.cpp b/src/smt/seq_eq_solver.cpp index 9203c35bd..a54ebdac9 100644 --- a/src/smt/seq_eq_solver.cpp +++ b/src/smt/seq_eq_solver.cpp @@ -1120,9 +1120,9 @@ struct remove_obj_pair_map : public trail { remove_obj_pair_map(ast_manager& m, obj_pair_hashtable & map, expr* a, expr* b): m(m), m_map(map), a(a), b(b) {} void undo() override { + m_map.erase(std::make_pair(a, b)); m.dec_ref(a); m.dec_ref(b); - m_map.erase(std::make_pair(a, b)); } }; diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index ee3341e43..48eb23b4f 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -198,7 +198,7 @@ namespace smt { return; ast_translation tr(src_ctx.m, m, false); auto* p = get_theory(m.mk_family_id("user_propagator")); - m_user_propagator = reinterpret_cast(p); + m_user_propagator = reinterpret_cast(p); SASSERT(m_user_propagator); for (unsigned i = 0; i < src_ctx.m_user_propagator->get_num_vars(); ++i) { app* e = src_ctx.m_user_propagator->get_expr(i); @@ -2886,11 +2886,11 @@ namespace smt { void context::user_propagate_init( void* ctx, - solver::push_eh_t& push_eh, - solver::pop_eh_t& pop_eh, - solver::fresh_eh_t& fresh_eh) { + user_propagator::push_eh_t& push_eh, + user_propagator::pop_eh_t& pop_eh, + user_propagator::fresh_eh_t& fresh_eh) { setup_context(false); - m_user_propagator = alloc(user_propagator, *this); + m_user_propagator = alloc(theory_user_propagator, *this); m_user_propagator->add(ctx, push_eh, pop_eh, fresh_eh); for (unsigned i = m_scopes.size(); i-- > 0; ) m_user_propagator->push_scope_eh(); @@ -3552,7 +3552,7 @@ namespace smt { parallel p(*this); return p(asms); } - lbool r; + lbool r = l_undef; do { pop_to_base_lvl(); expr_ref_vector asms(m, num_assumptions, assumptions); @@ -3573,7 +3573,7 @@ namespace smt { if (!check_preamble(true)) return l_undef; TRACE("before_search", display(tout);); setup_context(false); - lbool r; + lbool r = l_undef; do { pop_to_base_lvl(); expr_ref_vector asms(cube); diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index b5a19569a..700c2f211 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -46,7 +46,7 @@ Revision History: #include "util/statistics.h" #include "smt/fingerprints.h" #include "smt/proto_model/proto_model.h" -#include "smt/user_propagator.h" +#include "smt/theory_user_propagator.h" #include "model/model.h" #include "solver/progress_callback.h" #include "solver/assertions/asserted_formulas.h" @@ -88,7 +88,7 @@ namespace smt { scoped_ptr m_qmanager; scoped_ptr m_model_generator; scoped_ptr m_relevancy_propagator; - user_propagator* m_user_propagator; + theory_user_propagator* m_user_propagator; random_gen m_random; bool m_flushing; // (debug support) true when flushing mutable unsigned m_lemma_id; @@ -1695,29 +1695,29 @@ namespace smt { */ void user_propagate_init( void* ctx, - solver::push_eh_t& push_eh, - solver::pop_eh_t& pop_eh, - solver::fresh_eh_t& fresh_eh); + user_propagator::push_eh_t& push_eh, + user_propagator::pop_eh_t& pop_eh, + user_propagator::fresh_eh_t& fresh_eh); - void user_propagate_register_final(solver::final_eh_t& final_eh) { + void user_propagate_register_final(user_propagator::final_eh_t& final_eh) { if (!m_user_propagator) throw default_exception("user propagator must be initialized"); m_user_propagator->register_final(final_eh); } - void user_propagate_register_fixed(solver::fixed_eh_t& fixed_eh) { + void user_propagate_register_fixed(user_propagator::fixed_eh_t& fixed_eh) { if (!m_user_propagator) throw default_exception("user propagator must be initialized"); m_user_propagator->register_fixed(fixed_eh); } - void user_propagate_register_eq(solver::eq_eh_t& eq_eh) { + void user_propagate_register_eq(user_propagator::eq_eh_t& eq_eh) { if (!m_user_propagator) throw default_exception("user propagator must be initialized"); m_user_propagator->register_eq(eq_eh); } - void user_propagate_register_diseq(solver::eq_eh_t& diseq_eh) { + void user_propagate_register_diseq(user_propagator::eq_eh_t& diseq_eh) { if (!m_user_propagator) throw default_exception("user propagator must be initialized"); m_user_propagator->register_diseq(diseq_eh); diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp index ecd443a55..4b321fd4a 100644 --- a/src/smt/smt_kernel.cpp +++ b/src/smt/smt_kernel.cpp @@ -223,25 +223,25 @@ namespace smt { void user_propagate_init( void* ctx, - solver::push_eh_t& push_eh, - solver::pop_eh_t& pop_eh, - solver::fresh_eh_t& fresh_eh) { + user_propagator::push_eh_t& push_eh, + user_propagator::pop_eh_t& pop_eh, + user_propagator::fresh_eh_t& fresh_eh) { m_kernel.user_propagate_init(ctx, push_eh, pop_eh, fresh_eh); } - void user_propagate_register_final(solver::final_eh_t& final_eh) { + void user_propagate_register_final(user_propagator::final_eh_t& final_eh) { m_kernel.user_propagate_register_final(final_eh); } - void user_propagate_register_fixed(solver::fixed_eh_t& fixed_eh) { + void user_propagate_register_fixed(user_propagator::fixed_eh_t& fixed_eh) { m_kernel.user_propagate_register_fixed(fixed_eh); } - void user_propagate_register_eq(solver::eq_eh_t& eq_eh) { + void user_propagate_register_eq(user_propagator::eq_eh_t& eq_eh) { m_kernel.user_propagate_register_eq(eq_eh); } - void user_propagate_register_diseq(solver::eq_eh_t& diseq_eh) { + void user_propagate_register_diseq(user_propagator::eq_eh_t& diseq_eh) { m_kernel.user_propagate_register_diseq(diseq_eh); } @@ -451,25 +451,25 @@ namespace smt { void kernel::user_propagate_init( void* ctx, - solver::push_eh_t& push_eh, - solver::pop_eh_t& pop_eh, - solver::fresh_eh_t& fresh_eh) { + user_propagator::push_eh_t& push_eh, + user_propagator::pop_eh_t& pop_eh, + user_propagator::fresh_eh_t& fresh_eh) { m_imp->user_propagate_init(ctx, push_eh, pop_eh, fresh_eh); } - void kernel::user_propagate_register_fixed(solver::fixed_eh_t& fixed_eh) { + void kernel::user_propagate_register_fixed(user_propagator::fixed_eh_t& fixed_eh) { m_imp->user_propagate_register_fixed(fixed_eh); } - void kernel::user_propagate_register_final(solver::final_eh_t& final_eh) { + void kernel::user_propagate_register_final(user_propagator::final_eh_t& final_eh) { m_imp->user_propagate_register_final(final_eh); } - void kernel::user_propagate_register_eq(solver::eq_eh_t& eq_eh) { + void kernel::user_propagate_register_eq(user_propagator::eq_eh_t& eq_eh) { m_imp->user_propagate_register_eq(eq_eh); } - void kernel::user_propagate_register_diseq(solver::eq_eh_t& diseq_eh) { + void kernel::user_propagate_register_diseq(user_propagator::eq_eh_t& diseq_eh) { m_imp->user_propagate_register_diseq(diseq_eh); } diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h index 68fbca582..2259dd997 100644 --- a/src/smt/smt_kernel.h +++ b/src/smt/smt_kernel.h @@ -289,17 +289,17 @@ namespace smt { */ void user_propagate_init( void* ctx, - solver::push_eh_t& push_eh, - solver::pop_eh_t& pop_eh, - solver::fresh_eh_t& fresh_eh); + user_propagator::push_eh_t& push_eh, + user_propagator::pop_eh_t& pop_eh, + user_propagator::fresh_eh_t& fresh_eh); - void user_propagate_register_fixed(solver::fixed_eh_t& fixed_eh); + void user_propagate_register_fixed(user_propagator::fixed_eh_t& fixed_eh); - void user_propagate_register_final(solver::final_eh_t& final_eh); + void user_propagate_register_final(user_propagator::final_eh_t& final_eh); - void user_propagate_register_eq(solver::eq_eh_t& eq_eh); + void user_propagate_register_eq(user_propagator::eq_eh_t& eq_eh); - void user_propagate_register_diseq(solver::eq_eh_t& diseq_eh); + void user_propagate_register_diseq(user_propagator::eq_eh_t& diseq_eh); /** diff --git a/src/smt/smt_model_generator.cpp b/src/smt/smt_model_generator.cpp index dcdb9a198..73d8cad9d 100644 --- a/src/smt/smt_model_generator.cpp +++ b/src/smt/smt_model_generator.cpp @@ -105,7 +105,7 @@ namespace smt { else proc = alloc(expr_wrapper_proc, m.mk_false()); } - else if (m.is_value(r->get_expr())) + else if (m.is_model_value(r->get_expr())) proc = alloc(expr_wrapper_proc, r->get_expr()); else { family_id fid = s->get_family_id(); diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 930a731a1..9352e33f4 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -215,25 +215,25 @@ namespace { void user_propagate_init( void* ctx, - solver::push_eh_t& push_eh, - solver::pop_eh_t& pop_eh, - solver::fresh_eh_t& fresh_eh) override { + user_propagator::push_eh_t& push_eh, + user_propagator::pop_eh_t& pop_eh, + user_propagator::fresh_eh_t& fresh_eh) override { m_context.user_propagate_init(ctx, push_eh, pop_eh, fresh_eh); } - void user_propagate_register_fixed(solver::fixed_eh_t& fixed_eh) override { + void user_propagate_register_fixed(user_propagator::fixed_eh_t& fixed_eh) override { m_context.user_propagate_register_fixed(fixed_eh); } - void user_propagate_register_final(solver::final_eh_t& final_eh) override { + void user_propagate_register_final(user_propagator::final_eh_t& final_eh) override { m_context.user_propagate_register_final(final_eh); } - void user_propagate_register_eq(solver::eq_eh_t& eq_eh) override { + void user_propagate_register_eq(user_propagator::eq_eh_t& eq_eh) override { m_context.user_propagate_register_eq(eq_eh); } - void user_propagate_register_diseq(solver::eq_eh_t& diseq_eh) override { + void user_propagate_register_diseq(user_propagator::eq_eh_t& diseq_eh) override { m_context.user_propagate_register_diseq(diseq_eh); } diff --git a/src/smt/tactic/ctx_solver_simplify_tactic.cpp b/src/smt/tactic/ctx_solver_simplify_tactic.cpp index fd05c4a8e..6b1d1b7f4 100644 --- a/src/smt/tactic/ctx_solver_simplify_tactic.cpp +++ b/src/smt/tactic/ctx_solver_simplify_tactic.cpp @@ -63,6 +63,8 @@ public: m_fns.reset(); } + char const* name() const override { return "ctx_solver_simplify"; } + void updt_params(params_ref const & p) override { m_solver.updt_params(p); } diff --git a/src/smt/tactic/smt_tactic_core.cpp b/src/smt/tactic/smt_tactic_core.cpp index 3aa2df869..5cbe469fd 100644 --- a/src/smt/tactic/smt_tactic_core.cpp +++ b/src/smt/tactic/smt_tactic_core.cpp @@ -37,32 +37,35 @@ typedef obj_map expr2expr_map; class smt_tactic : public tactic { + ast_manager& m; smt_params m_params; params_ref m_params_ref; statistics m_stats; - smt::kernel * m_ctx; + smt::kernel* m_ctx = nullptr; symbol m_logic; - progress_callback * m_callback; - bool m_candidate_models; - bool m_fail_if_inconclusive; + progress_callback* m_callback = nullptr; + bool m_candidate_models = false; + bool m_fail_if_inconclusive = false; public: - smt_tactic(params_ref const & p): + smt_tactic(ast_manager& m, params_ref const & p): + m(m), m_params_ref(p), - m_ctx(nullptr), - m_callback(nullptr) { + m_vars(m) { updt_params_core(p); TRACE("smt_tactic", tout << "p: " << p << "\n";); } tactic * translate(ast_manager & m) override { - return alloc(smt_tactic, m_params_ref); + return alloc(smt_tactic, m, m_params_ref); } ~smt_tactic() override { SASSERT(m_ctx == nullptr); } + char const* name() const override { return "smt"; } + smt_params & fparams() { return m_params; } @@ -137,6 +140,7 @@ public: ~scoped_init_ctx() { smt::kernel * d = m_owner.m_ctx; m_owner.m_ctx = nullptr; + m_owner.m_user_ctx = nullptr; if (d) dealloc(d); @@ -151,7 +155,6 @@ public: goal_ref_buffer & result) override { try { IF_VERBOSE(10, verbose_stream() << "(smt.tactic start)\n";); - ast_manager & m = in->m(); tactic_report report("smt", *in); TRACE("smt_tactic", tout << this << "\nAUTO_CONFIG: " << fparams().m_auto_config << " HIDIV0: " << fparams().m_hi_div0 << " " << " PREPROCESS: " << fparams().m_preprocess << "\n"; @@ -163,7 +166,7 @@ public: TRACE("smt_tactic_detail", in->display(tout);); TRACE("smt_tactic_memory", tout << "wasted_size: " << m.get_allocator().get_wasted_size() << "\n";); scoped_init_ctx init(*this, m); - SASSERT(m_ctx != 0); + SASSERT(m_ctx); expr_ref_vector clauses(m); expr2expr_map bool2dep; @@ -194,10 +197,11 @@ public: if (m_ctx->canceled()) { throw tactic_exception(Z3_CANCELED_MSG); } + user_propagate_delay_init(); lbool r; try { - if (assumptions.empty()) + if (assumptions.empty() && !m_user_ctx) r = m_ctx->setup_and_check(); else r = m_ctx->check(assumptions.size(), assumptions.data()); @@ -306,10 +310,163 @@ public: throw tactic_exception(ex.msg()); } } + + void* m_user_ctx = nullptr; + user_propagator::push_eh_t m_push_eh; + user_propagator::pop_eh_t m_pop_eh; + user_propagator::fresh_eh_t m_fresh_eh; + user_propagator::fixed_eh_t m_fixed_eh; + user_propagator::final_eh_t m_final_eh; + user_propagator::eq_eh_t m_eq_eh; + user_propagator::eq_eh_t m_diseq_eh; + expr_ref_vector m_vars; + unsigned_vector m_var2internal; + unsigned_vector m_internal2var; + + user_propagator::fixed_eh_t i_fixed_eh; + user_propagator::final_eh_t i_final_eh; + user_propagator::eq_eh_t i_eq_eh; + user_propagator::eq_eh_t i_diseq_eh; + + + + struct callback : public user_propagator::callback { + smt_tactic* t = nullptr; + user_propagator::callback* cb = nullptr; + unsigned_vector fixed, lhs, rhs; + void propagate_cb(unsigned num_fixed, unsigned const* fixed_ids, unsigned num_eqs, unsigned const* eq_lhs, unsigned const* eq_rhs, expr* conseq) override { + fixed.reset(); + lhs.reset(); + rhs.reset(); + for (unsigned i = 0; i < num_fixed; ++i) + fixed.push_back(t->m_var2internal[fixed_ids[i]]); + for (unsigned i = 0; i < num_eqs; ++i) { + lhs.push_back(t->m_var2internal[eq_lhs[i]]); + rhs.push_back(t->m_var2internal[eq_rhs[i]]); + } + cb->propagate_cb(num_fixed, fixed.data(), num_eqs, lhs.data(), rhs.data(), conseq); + } + + unsigned register_cb(expr* e) override { + unsigned j = t->m_vars.size(); + t->m_vars.push_back(e); + unsigned i = cb->register_cb(e); + t->m_var2internal.setx(j, i, 0); + t->m_internal2var.setx(i, j, 0); + return j; + } + }; + + callback i_cb; + + void init_i_fixed_eh() { + if (!m_fixed_eh) + return; + i_fixed_eh = [this](void* ctx, user_propagator::callback* cb, unsigned id, expr* value) { + i_cb.t = this; + i_cb.cb = cb; + m_fixed_eh(ctx, &i_cb, m_internal2var[id], value); + }; + m_ctx->user_propagate_register_fixed(i_fixed_eh); + } + + void init_i_final_eh() { + if (!m_final_eh) + return; + i_final_eh = [this](void* ctx, user_propagator::callback* cb) { + i_cb.t = this; + i_cb.cb = cb; + m_final_eh(ctx, &i_cb); + }; + m_ctx->user_propagate_register_final(i_final_eh); + } + + void init_i_eq_eh() { + if (!m_eq_eh) + return; + i_eq_eh = [this](void* ctx, user_propagator::callback* cb, unsigned u, unsigned v) { + i_cb.t = this; + i_cb.cb = cb; + m_eq_eh(ctx, &i_cb, m_internal2var[u], m_internal2var[v]); + }; + m_ctx->user_propagate_register_eq(i_eq_eh); + } + + void init_i_diseq_eh() { + if (!m_diseq_eh) + return; + i_diseq_eh = [this](void* ctx, user_propagator::callback* cb, unsigned u, unsigned v) { + i_cb.t = this; + i_cb.cb = cb; + m_diseq_eh(ctx, &i_cb, m_internal2var[u], m_internal2var[v]); + }; + m_ctx->user_propagate_register_diseq(i_diseq_eh); + } + + + void user_propagate_delay_init() { + if (!m_user_ctx) + return; + m_ctx->user_propagate_init(m_user_ctx, m_push_eh, m_pop_eh, m_fresh_eh); + init_i_fixed_eh(); + init_i_final_eh(); + init_i_eq_eh(); + init_i_diseq_eh(); + + unsigned i = 0; + for (expr* v : m_vars) { + unsigned j = m_ctx->user_propagate_register(v); + m_var2internal.setx(i, j, 0); + m_internal2var.setx(j, i, 0); + ++i; + } + } + + void user_propagate_clear() override { + m_user_ctx = nullptr; + m_vars.reset(); + m_fixed_eh = nullptr; + m_final_eh = nullptr; + m_eq_eh = nullptr; + m_diseq_eh = nullptr; + } + + void user_propagate_init( + void* ctx, + user_propagator::push_eh_t& push_eh, + user_propagator::pop_eh_t& pop_eh, + user_propagator::fresh_eh_t& fresh_eh) override { + user_propagate_clear(); + m_user_ctx = ctx; + m_push_eh = push_eh; + m_pop_eh = pop_eh; + m_fresh_eh = fresh_eh; + } + + void user_propagate_register_fixed(user_propagator::fixed_eh_t& fixed_eh) override { + m_fixed_eh = fixed_eh; + } + + void user_propagate_register_final(user_propagator::final_eh_t& final_eh) override { + m_final_eh = final_eh; + } + + void user_propagate_register_eq(user_propagator::eq_eh_t& eq_eh) override { + m_eq_eh = eq_eh; + } + + void user_propagate_register_diseq(user_propagator::eq_eh_t& diseq_eh) override { + m_diseq_eh = diseq_eh; + } + + unsigned user_propagate_register(expr* e) override { + m_vars.push_back(e); + return m_vars.size() - 1; + } }; -static tactic * mk_seq_smt_tactic(params_ref const & p) { - return alloc(smt_tactic, p); +static tactic * mk_seq_smt_tactic(ast_manager& m, params_ref const & p) { + return alloc(smt_tactic, m, p); } @@ -319,13 +476,13 @@ tactic * mk_parallel_smt_tactic(ast_manager& m, params_ref const& p) { tactic * mk_smt_tactic_core(ast_manager& m, params_ref const& p, symbol const& logic) { parallel_params pp(p); - return pp.enable() ? mk_parallel_tactic(mk_smt_solver(m, p, logic), p) : mk_seq_smt_tactic(p); + return pp.enable() ? mk_parallel_tactic(mk_smt_solver(m, p, logic), p) : mk_seq_smt_tactic(m, p); } tactic * mk_smt_tactic_core_using(ast_manager& m, bool auto_config, params_ref const& _p) { parallel_params pp(_p); params_ref p = _p; p.set_bool("auto_config", auto_config); - return using_params(pp.enable() ? mk_parallel_smt_tactic(m, p) : mk_seq_smt_tactic(p), p); + return using_params(pp.enable() ? mk_parallel_smt_tactic(m, p) : mk_seq_smt_tactic(m, p), p); } diff --git a/src/smt/tactic/unit_subsumption_tactic.cpp b/src/smt/tactic/unit_subsumption_tactic.cpp index 44086aa7e..97ce4a1c1 100644 --- a/src/smt/tactic/unit_subsumption_tactic.cpp +++ b/src/smt/tactic/unit_subsumption_tactic.cpp @@ -38,6 +38,8 @@ struct unit_subsumption_tactic : public tactic { m_clauses(m) { } + char const* name() const override { return "unit_subsumption"; } + void cleanup() override {} void operator()(/* in */ goal_ref const & in, diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 0abc2870d..42e98e471 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1529,7 +1529,7 @@ public: IF_VERBOSE(12, verbose_stream() << "final-check " << lp().get_status() << "\n"); lbool is_sat = l_true; SASSERT(lp().ax_is_correct()); - if (lp().get_status() != lp::lp_status::OPTIMAL || lp().has_changed_columns()) { + if (!lp().is_feasible() || lp().has_changed_columns()) { is_sat = make_feasible(); } final_check_status st = FC_DONE; @@ -2084,7 +2084,7 @@ public: while (m_asserted_qhead < m_asserted_atoms.size() && !ctx().inconsistent() && m.inc()) { auto [bv, is_true] = m_asserted_atoms[m_asserted_qhead]; - m_bv_to_propagate.push_back(bv); + // m_bv_to_propagate.push_back(bv); api_bound* b = nullptr; TRACE("arith", tout << "propagate: " << literal(bv, !is_true) << "\n"; @@ -3083,21 +3083,14 @@ public: TRACE("pcs", tout << lp().constraints();); auto status = lp().find_feasible_solution(); TRACE("arith_verbose", display(tout);); - switch (status) { - case lp::lp_status::INFEASIBLE: - return l_false; - case lp::lp_status::FEASIBLE: - case lp::lp_status::OPTIMAL: - // SASSERT(lp().all_constraints_hold()); + if (lp().is_feasible()) return l_true; - case lp::lp_status::TIME_EXHAUSTED: - - default: - TRACE("arith", tout << "status treated as inconclusive: " << status << "\n";); + if (status == lp::lp_status::INFEASIBLE) + return l_false; + TRACE("arith", tout << "status treated as inconclusive: " << status << "\n";); // TENTATIVE_UNBOUNDED, UNBOUNDED, TENTATIVE_DUAL_UNBOUNDED, DUAL_UNBOUNDED, - // FLOATING_POINT_ERROR, TIME_EXAUSTED, ITERATIONS_EXHAUSTED, EMPTY, UNSTABLE - return l_undef; - } + // FLOATING_POINT_ERROR, TIME_EXAUSTED, EMPTY, UNSTABLE + return l_undef; } lp::explanation m_explanation; @@ -3467,7 +3460,7 @@ public: st = lp::lp_status::UNBOUNDED; } else { - if (lp().get_status() != lp::lp_status::OPTIMAL || lp().has_changed_columns()) + if (!lp().is_feasible() || lp().has_changed_columns()) make_feasible(); vi = get_lpvar(v); @@ -3477,7 +3470,10 @@ public: st = lp::lp_status::FEASIBLE; lp().restore_x(); } - + if (m_nla && (st == lp::lp_status::OPTIMAL || st == lp::lp_status::UNBOUNDED)) { + st = lp::lp_status::FEASIBLE; + lp().restore_x(); + } } switch (st) { case lp::lp_status::OPTIMAL: { diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 3db4c4776..1564a2015 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2206,8 +2206,9 @@ expr_ref theory_seq::elim_skolem(expr* e) { if (m_sk.is_post(a, x, y) && cache.contains(x) && cache.contains(y)) { x = cache[x]; y = cache[y]; + auto mk_max = [&](expr* x, expr* y) { return m.mk_ite(m_autil.mk_ge(x, y), x, y); }; result = m_util.str.mk_length(x); - result = m_util.str.mk_substr(x, y, m_autil.mk_sub(result, y)); + result = m_util.str.mk_substr(x, mk_max(y,m_autil.mk_int(0)), m_autil.mk_sub(result, y)); trail.push_back(result); cache.insert(a, result); todo.pop_back(); @@ -2277,16 +2278,14 @@ expr_ref theory_seq::elim_skolem(expr* e) { args.reset(); for (expr* arg : *to_app(a)) { - if (cache.find(arg, b)) { + if (cache.find(arg, b)) args.push_back(b); - } - else { + else todo.push_back(arg); - } } - if (args.size() < to_app(a)->get_num_args()) { + + if (args.size() < to_app(a)->get_num_args()) continue; - } if (m_util.is_skolem(a)) { IF_VERBOSE(0, verbose_stream() << "unhandled skolem " << mk_pp(a, m) << "\n"); @@ -2367,11 +2366,12 @@ void theory_seq::validate_fmls(enode_pair_vector const& eqs, literal_vector cons if (r == l_true) { model_ref mdl; k.get_model(mdl); + TRACE("seq", tout << "failed to validate\n" << *mdl << "\n"); IF_VERBOSE(0, verbose_stream() << r << "\n" << fmls << "\n"; verbose_stream() << *mdl.get() << "\n"; - k.display(verbose_stream())); - UNREACHABLE(); + k.display(verbose_stream()) << "\n"); + //UNREACHABLE(); } } diff --git a/src/smt/user_propagator.cpp b/src/smt/theory_user_propagator.cpp similarity index 59% rename from src/smt/user_propagator.cpp rename to src/smt/theory_user_propagator.cpp index 7fbfd567f..2b50e07ab 100644 --- a/src/smt/user_propagator.cpp +++ b/src/smt/theory_user_propagator.cpp @@ -3,7 +3,7 @@ Copyright (c) 2020 Microsoft Corporation Module Name: - user_propagator.cpp + theory_user_propagator.cpp Abstract: @@ -17,20 +17,20 @@ Author: #include "ast/ast_pp.h" -#include "smt/user_propagator.h" +#include "smt/theory_user_propagator.h" #include "smt/smt_context.h" using namespace smt; -user_propagator::user_propagator(context& ctx): +theory_user_propagator::theory_user_propagator(context& ctx): theory(ctx, ctx.get_manager().mk_family_id("user_propagator")) {} -user_propagator::~user_propagator() { +theory_user_propagator::~theory_user_propagator() { dealloc(m_api_context); } -void user_propagator::force_push() { +void theory_user_propagator::force_push() { for (; m_num_scopes > 0; --m_num_scopes) { theory::push_scope_eh(); m_push_eh(m_user_context); @@ -38,7 +38,7 @@ void user_propagator::force_push() { } } -unsigned user_propagator::add_expr(expr* e) { +unsigned theory_user_propagator::add_expr(expr* e) { force_push(); enode* n = ensure_enode(e); if (is_attached_to_var(n)) @@ -48,17 +48,23 @@ unsigned user_propagator::add_expr(expr* e) { return v; } -void user_propagator::propagate_cb( +void theory_user_propagator::propagate_cb( unsigned num_fixed, unsigned const* fixed_ids, unsigned num_eqs, unsigned const* eq_lhs, unsigned const* eq_rhs, expr* conseq) { - if (ctx.lit_internalized(conseq) && ctx.get_assignment(ctx.get_literal(conseq)) == l_true) + CTRACE("user_propagate", ctx.lit_internalized(conseq) && ctx.get_assignment(ctx.get_literal(conseq)) == l_true, + ctx.display(tout << "redundant consequence: " << mk_pp(conseq, m) << "\n")); + if (ctx.lit_internalized(conseq) && ctx.get_assignment(ctx.get_literal(conseq)) == l_true) return; m_prop.push_back(prop_info(num_fixed, fixed_ids, num_eqs, eq_lhs, eq_rhs, expr_ref(conseq, m))); } -theory * user_propagator::mk_fresh(context * new_ctx) { - auto* th = alloc(user_propagator, *new_ctx); +unsigned theory_user_propagator::register_cb(expr* e) { + return add_expr(e); +} + +theory * theory_user_propagator::mk_fresh(context * new_ctx) { + auto* th = alloc(theory_user_propagator, *new_ctx); void* ctx = m_fresh_eh(m_user_context, new_ctx->get_manager(), th->m_api_context); th->add(ctx, m_push_eh, m_pop_eh, m_fresh_eh); if ((bool)m_fixed_eh) th->register_fixed(m_fixed_eh); @@ -68,7 +74,7 @@ theory * user_propagator::mk_fresh(context * new_ctx) { return th; } -final_check_status user_propagator::final_check_eh() { +final_check_status theory_user_propagator::final_check_eh() { if (!(bool)m_final_eh) return FC_DONE; force_push(); @@ -79,7 +85,7 @@ final_check_status user_propagator::final_check_eh() { return done ? FC_DONE : FC_CONTINUE; } -void user_propagator::new_fixed_eh(theory_var v, expr* value, unsigned num_lits, literal const* jlits) { +void theory_user_propagator::new_fixed_eh(theory_var v, expr* value, unsigned num_lits, literal const* jlits) { if (!m_fixed_eh) return; force_push(); @@ -91,11 +97,11 @@ void user_propagator::new_fixed_eh(theory_var v, expr* value, unsigned num_lits, m_fixed_eh(m_user_context, this, v, value); } -void user_propagator::push_scope_eh() { +void theory_user_propagator::push_scope_eh() { ++m_num_scopes; } -void user_propagator::pop_scope_eh(unsigned num_scopes) { +void theory_user_propagator::pop_scope_eh(unsigned num_scopes) { unsigned n = std::min(num_scopes, m_num_scopes); m_num_scopes -= n; num_scopes -= n; @@ -108,11 +114,12 @@ void user_propagator::pop_scope_eh(unsigned num_scopes) { m_prop_lim.shrink(old_sz); } -bool user_propagator::can_propagate() { +bool theory_user_propagator::can_propagate() { return m_qhead < m_prop.size(); } -void user_propagator::propagate() { +void theory_user_propagator::propagate() { + TRACE("user_propagate", tout << "propagating queue head: " << m_qhead << " prop queue: " << m_prop.size() << "\n"); if (m_qhead == m_prop.size()) return; force_push(); @@ -127,9 +134,10 @@ void user_propagator::propagate() { for (auto const& p : prop.m_eqs) m_eqs.push_back(enode_pair(get_enode(p.first), get_enode(p.second))); DEBUG_CODE(for (auto const& p : m_eqs) VERIFY(p.first->get_root() == p.second->get_root());); - DEBUG_CODE(for (unsigned id : prop.m_ids) VERIFY(m_fixed.contains(id));); - DEBUG_CODE(for (literal lit : m_lits) VERIFY(ctx.get_assignment(lit) == l_true);); + DEBUG_CODE(for (unsigned id : prop.m_ids) VERIFY(m_fixed.contains(id));); + DEBUG_CODE(for (literal lit : m_lits) VERIFY(ctx.get_assignment(lit) == l_true);); + TRACE("user_propagate", tout << "propagating #" << prop.m_conseq->get_id() << ": " << prop.m_conseq << "\n"); if (m.is_false(prop.m_conseq)) { js = ctx.mk_justification( @@ -138,11 +146,25 @@ void user_propagator::propagate() { ctx.set_conflict(js); } else { - literal lit = mk_literal(prop.m_conseq); - js = ctx.mk_justification( - ext_theory_propagation_justification( - get_id(), ctx.get_region(), m_lits.size(), m_lits.data(), m_eqs.size(), m_eqs.data(), lit)); - ctx.assign(lit, js); + for (auto& lit : m_lits) + lit.neg(); + for (auto const& [a,b] : m_eqs) + m_lits.push_back(~mk_eq(a->get_expr(), b->get_expr(), false)); + + literal lit; + if (has_quantifiers(prop.m_conseq)) { + expr_ref fn(m.mk_fresh_const("aux-literal", m.mk_bool_sort()), m); + expr_ref eq(m.mk_eq(fn, prop.m_conseq), m); + ctx.assert_expr(eq); + ctx.internalize_assertions(); + lit = mk_literal(fn); + } + else + lit = mk_literal(prop.m_conseq); + ctx.mark_as_relevant(lit); + m_lits.push_back(lit); + ctx.mk_th_lemma(get_id(), m_lits); + TRACE("user_propagate", ctx.display(tout);); } ++m_stats.m_num_propagations; ++qhead; @@ -151,7 +173,7 @@ void user_propagator::propagate() { m_qhead = qhead; } -void user_propagator::collect_statistics(::statistics & st) const { +void theory_user_propagator::collect_statistics(::statistics & st) const { st.update("user-propagations", m_stats.m_num_propagations); st.update("user-watched", get_num_vars()); } diff --git a/src/smt/user_propagator.h b/src/smt/theory_user_propagator.h similarity index 75% rename from src/smt/user_propagator.h rename to src/smt/theory_user_propagator.h index dcf41c3bb..d007de6a0 100644 --- a/src/smt/user_propagator.h +++ b/src/smt/theory_user_propagator.h @@ -27,7 +27,7 @@ Notes: #include "solver/solver.h" namespace smt { - class user_propagator : public theory, public solver::propagate_callback { + class theory_user_propagator : public theory, public user_propagator::callback { struct prop_info { unsigned_vector m_ids; @@ -49,14 +49,14 @@ namespace smt { }; void* m_user_context = nullptr; - solver::push_eh_t m_push_eh; - solver::pop_eh_t m_pop_eh; - solver::fresh_eh_t m_fresh_eh; - solver::final_eh_t m_final_eh; - solver::fixed_eh_t m_fixed_eh; - solver::eq_eh_t m_eq_eh; - solver::eq_eh_t m_diseq_eh; - solver::context_obj* m_api_context = nullptr; + user_propagator::push_eh_t m_push_eh; + user_propagator::pop_eh_t m_pop_eh; + user_propagator::fresh_eh_t m_fresh_eh; + user_propagator::final_eh_t m_final_eh; + user_propagator::fixed_eh_t m_fixed_eh; + user_propagator::eq_eh_t m_eq_eh; + user_propagator::eq_eh_t m_diseq_eh; + user_propagator::context_obj* m_api_context = nullptr; unsigned m_qhead = 0; uint_set m_fixed; vector m_prop; @@ -70,18 +70,18 @@ namespace smt { void force_push(); public: - user_propagator(context& ctx); + theory_user_propagator(context& ctx); - ~user_propagator() override; + ~theory_user_propagator() override; /* * \brief initial setup for user propagator. */ void add( void* ctx, - solver::push_eh_t& push_eh, - solver::pop_eh_t& pop_eh, - solver::fresh_eh_t& fresh_eh) { + user_propagator::push_eh_t& push_eh, + user_propagator::pop_eh_t& pop_eh, + user_propagator::fresh_eh_t& fresh_eh) { m_user_context = ctx; m_push_eh = push_eh; m_pop_eh = pop_eh; @@ -90,14 +90,15 @@ namespace smt { unsigned add_expr(expr* e); - void register_final(solver::final_eh_t& final_eh) { m_final_eh = final_eh; } - void register_fixed(solver::fixed_eh_t& fixed_eh) { m_fixed_eh = fixed_eh; } - void register_eq(solver::eq_eh_t& eq_eh) { m_eq_eh = eq_eh; } - void register_diseq(solver::eq_eh_t& diseq_eh) { m_diseq_eh = diseq_eh; } + void register_final(user_propagator::final_eh_t& final_eh) { m_final_eh = final_eh; } + void register_fixed(user_propagator::fixed_eh_t& fixed_eh) { m_fixed_eh = fixed_eh; } + void register_eq(user_propagator::eq_eh_t& eq_eh) { m_eq_eh = eq_eh; } + void register_diseq(user_propagator::eq_eh_t& diseq_eh) { m_diseq_eh = diseq_eh; } bool has_fixed() const { return (bool)m_fixed_eh; } void propagate_cb(unsigned num_fixed, unsigned const* fixed_ids, unsigned num_eqs, unsigned const* lhs, unsigned const* rhs, expr* conseq) override; + unsigned register_cb(expr* e) override; void new_fixed_eh(theory_var v, expr* value, unsigned num_lits, literal const* jlits); diff --git a/src/solver/parallel_tactic.cpp b/src/solver/parallel_tactic.cpp index 8336f0050..2f3ba7798 100644 --- a/src/solver/parallel_tactic.cpp +++ b/src/solver/parallel_tactic.cpp @@ -757,6 +757,8 @@ public: init(); } + char const* name() const override { return "parallel_tactic"; } + void operator()(const goal_ref & g,goal_ref_buffer & result) override { cleanup(); fail_if_proof_generation("parallel-tactic", g); diff --git a/src/solver/solver.h b/src/solver/solver.h index 550105167..090cd9d9b 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -18,6 +18,7 @@ Notes: --*/ #pragma once +#include "tactic/user_propagator_base.h" #include "solver/check_sat_result.h" #include "solver/progress_callback.h" #include "util/params.h" @@ -47,7 +48,7 @@ solver* mk_smt2_solver(ast_manager& m, params_ref const& p); - statistics - results based on check_sat_result API */ -class solver : public check_sat_result { +class solver : public check_sat_result, public user_propagator::core { params_ref m_params; symbol m_cancel_backup_file; public: @@ -239,52 +240,6 @@ public: virtual expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level) = 0; - class propagate_callback { - public: - virtual ~propagate_callback() = default; - virtual void propagate_cb(unsigned num_fixed, unsigned const* fixed_ids, unsigned num_eqs, unsigned const* eq_lhs, unsigned const* eq_rhs, expr* conseq) = 0; - }; - class context_obj { - public: - virtual ~context_obj() {} - }; - typedef std::function final_eh_t; - typedef std::function fixed_eh_t; - typedef std::function eq_eh_t; - typedef std::function fresh_eh_t; - typedef std::function push_eh_t; - typedef std::function pop_eh_t; - - virtual void user_propagate_init( - void* ctx, - push_eh_t& push_eh, - pop_eh_t& pop_eh, - fresh_eh_t& fresh_eh) { - throw default_exception("user-propagators are only supported on the SMT solver"); - } - - - virtual void user_propagate_register_fixed(fixed_eh_t& fixed_eh) { - throw default_exception("user-propagators are only supported on the SMT solver"); - } - - virtual void user_propagate_register_final(final_eh_t& final_eh) { - throw default_exception("user-propagators are only supported on the SMT solver"); - } - - virtual void user_propagate_register_eq(eq_eh_t& eq_eh) { - throw default_exception("user-propagators are only supported on the SMT solver"); - } - - virtual void user_propagate_register_diseq(eq_eh_t& diseq_eh) { - throw default_exception("user-propagators are only supported on the SMT solver"); - } - - virtual unsigned user_propagate_register(expr* e) { - throw default_exception("user-propagators are only supported on the SMT solver"); - } - - /** \brief Display the content of this solver. */ diff --git a/src/solver/solver2tactic.cpp b/src/solver/solver2tactic.cpp index 8641a2aa8..389ee124b 100644 --- a/src/solver/solver2tactic.cpp +++ b/src/solver/solver2tactic.cpp @@ -186,6 +186,8 @@ public: tactic * translate(ast_manager & m) override { return alloc(solver2tactic, m_solver->translate(m, m_params)); } + + char const* name() const override { return "solver2tactic"; } }; tactic* mk_solver2tactic(solver* s) { return alloc(solver2tactic, s); } diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index 761c202cf..94f7fb336 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -84,6 +84,39 @@ public: void set_phase(phase* p) override { } void move_to_front(expr* e) override { } + void user_propagate_init( + void* ctx, + user_propagator::push_eh_t& push_eh, + user_propagator::pop_eh_t& pop_eh, + user_propagator::fresh_eh_t& fresh_eh) override { + m_tactic->user_propagate_init(ctx, push_eh, pop_eh, fresh_eh); + } + + void user_propagate_register_fixed(user_propagator::fixed_eh_t& fixed_eh) override { + m_tactic->user_propagate_register_fixed(fixed_eh); + } + + void user_propagate_register_final(user_propagator::final_eh_t& final_eh) override { + m_tactic->user_propagate_register_final(final_eh); + } + + void user_propagate_register_eq(user_propagator::eq_eh_t& eq_eh) override { + m_tactic->user_propagate_register_eq(eq_eh); + } + + void user_propagate_register_diseq(user_propagator::eq_eh_t& diseq_eh) override { + m_tactic->user_propagate_register_diseq(diseq_eh); + } + + unsigned user_propagate_register(expr* e) override { + return m_tactic->user_propagate_register(e); + } + + void user_propagate_clear() override { + if (m_tactic) + m_tactic->user_propagate_clear(); + } + expr_ref_vector cube(expr_ref_vector& vars, unsigned ) override { set_reason_unknown("cubing is not supported on tactics"); @@ -120,6 +153,7 @@ tactic2solver::tactic2solver(ast_manager & m, tactic * t, params_ref const & p, } tactic2solver::~tactic2solver() { + user_propagate_clear(); } void tactic2solver::updt_params(params_ref const & p) { diff --git a/src/tactic/aig/aig_tactic.cpp b/src/tactic/aig/aig_tactic.cpp index 7b80582fe..5ffc0dc20 100644 --- a/src/tactic/aig/aig_tactic.cpp +++ b/src/tactic/aig/aig_tactic.cpp @@ -45,6 +45,8 @@ public: aig_tactic(params_ref const & p = params_ref()):m_aig_manager(nullptr) { updt_params(p); } + + char const* name() const override { return "aig"; } tactic * translate(ast_manager & m) override { aig_tactic * t = alloc(aig_tactic); diff --git a/src/tactic/arith/add_bounds_tactic.cpp b/src/tactic/arith/add_bounds_tactic.cpp index b1367ea21..4493568bf 100644 --- a/src/tactic/arith/add_bounds_tactic.cpp +++ b/src/tactic/arith/add_bounds_tactic.cpp @@ -145,6 +145,8 @@ public: ~add_bounds_tactic() override { dealloc(m_imp); } + + char const* name() const override { return "add_bounds"; } void updt_params(params_ref const & p) override { m_params = p; diff --git a/src/tactic/arith/arith_bounds_tactic.cpp b/src/tactic/arith/arith_bounds_tactic.cpp index a8fcc4e00..87308078a 100644 --- a/src/tactic/arith/arith_bounds_tactic.cpp +++ b/src/tactic/arith/arith_bounds_tactic.cpp @@ -27,6 +27,8 @@ struct arith_bounds_tactic : public tactic { /* out */ goal_ref_buffer & result) override { bounds_arith_subsumption(in, result); } + + char const* name() const override { return "arith_bounds"; } tactic* translate(ast_manager & mgr) override { return alloc(arith_bounds_tactic, mgr); diff --git a/src/tactic/arith/card2bv_tactic.cpp b/src/tactic/arith/card2bv_tactic.cpp index 552270551..fce096f23 100644 --- a/src/tactic/arith/card2bv_tactic.cpp +++ b/src/tactic/arith/card2bv_tactic.cpp @@ -42,6 +42,8 @@ public: ~card2bv_tactic() override { } + char const* name() const override { return "card2bv"; } + void updt_params(params_ref const & p) override { m_params = p; } diff --git a/src/tactic/arith/degree_shift_tactic.cpp b/src/tactic/arith/degree_shift_tactic.cpp index d3c5bb74c..e34910e78 100644 --- a/src/tactic/arith/degree_shift_tactic.cpp +++ b/src/tactic/arith/degree_shift_tactic.cpp @@ -284,6 +284,8 @@ public: dealloc(m_imp); } + char const* name() const override { return "degree_shift"; } + void operator()(goal_ref const & in, goal_ref_buffer & result) override { (*m_imp)(in, result); diff --git a/src/tactic/arith/diff_neq_tactic.cpp b/src/tactic/arith/diff_neq_tactic.cpp index a2ca66af2..92ce7cd29 100644 --- a/src/tactic/arith/diff_neq_tactic.cpp +++ b/src/tactic/arith/diff_neq_tactic.cpp @@ -357,6 +357,8 @@ public: dealloc(m_imp); } + char const* name() const override { return "diff_neq"; } + void updt_params(params_ref const & p) override { m_params = p; m_imp->updt_params(p); diff --git a/src/tactic/arith/eq2bv_tactic.cpp b/src/tactic/arith/eq2bv_tactic.cpp index 865c268a1..a1a1a56cc 100644 --- a/src/tactic/arith/eq2bv_tactic.cpp +++ b/src/tactic/arith/eq2bv_tactic.cpp @@ -268,6 +268,8 @@ public: tactic * translate(ast_manager & m) override { return alloc(eq2bv_tactic, m); } + + char const* name() const override { return "eq2bv"; } void collect_param_descrs(param_descrs & r) override { } diff --git a/src/tactic/arith/factor_tactic.cpp b/src/tactic/arith/factor_tactic.cpp index 7875aaf6d..07b59a3f9 100644 --- a/src/tactic/arith/factor_tactic.cpp +++ b/src/tactic/arith/factor_tactic.cpp @@ -294,6 +294,8 @@ public: dealloc(m_imp); } + char const* name() const override { return "factor"; } + void updt_params(params_ref const & p) override { m_params = p; m_imp->m_rw.cfg().updt_params(p); diff --git a/src/tactic/arith/fix_dl_var_tactic.cpp b/src/tactic/arith/fix_dl_var_tactic.cpp index c5d119685..f2039c378 100644 --- a/src/tactic/arith/fix_dl_var_tactic.cpp +++ b/src/tactic/arith/fix_dl_var_tactic.cpp @@ -300,6 +300,8 @@ public: dealloc(m_imp); } + char const* name() const override { return "fix_dl_var"; } + void updt_params(params_ref const & p) override { m_params = p; m_imp->updt_params(p); diff --git a/src/tactic/arith/fm_tactic.cpp b/src/tactic/arith/fm_tactic.cpp index 4f10b0b3f..ef8109de0 100644 --- a/src/tactic/arith/fm_tactic.cpp +++ b/src/tactic/arith/fm_tactic.cpp @@ -1642,6 +1642,8 @@ public: dealloc(m_imp); } + char const* name() const override { return "fm"; } + void updt_params(params_ref const & p) override { m_params = p; m_imp->updt_params(p); diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp index ae0467039..77786e267 100644 --- a/src/tactic/arith/lia2card_tactic.cpp +++ b/src/tactic/arith/lia2card_tactic.cpp @@ -132,6 +132,8 @@ public: dealloc(m_todo); } + char const* name() const override { return "lia2card"; } + void updt_params(params_ref const & p) override { m_params = p; m_compile_equality = p.get_bool("compile_equality", true); diff --git a/src/tactic/arith/lia2pb_tactic.cpp b/src/tactic/arith/lia2pb_tactic.cpp index 9af642e69..d67f49a37 100644 --- a/src/tactic/arith/lia2pb_tactic.cpp +++ b/src/tactic/arith/lia2pb_tactic.cpp @@ -305,6 +305,8 @@ public: dealloc(m_imp); } + char const* name() const override { return "lia2pb"; } + void updt_params(params_ref const & p) override { m_params = p; m_imp->updt_params(p); diff --git a/src/tactic/arith/nla2bv_tactic.cpp b/src/tactic/arith/nla2bv_tactic.cpp index 43def0741..887cc9e31 100644 --- a/src/tactic/arith/nla2bv_tactic.cpp +++ b/src/tactic/arith/nla2bv_tactic.cpp @@ -438,6 +438,8 @@ public: ~nla2bv_tactic() override { } + char const* name() const override { return "nla2bv"; } + void updt_params(params_ref const & p) override { m_params.append(p); } diff --git a/src/tactic/arith/normalize_bounds_tactic.cpp b/src/tactic/arith/normalize_bounds_tactic.cpp index 957859cc7..b7ef28f49 100644 --- a/src/tactic/arith/normalize_bounds_tactic.cpp +++ b/src/tactic/arith/normalize_bounds_tactic.cpp @@ -153,6 +153,8 @@ public: dealloc(m_imp); } + char const* name() const override { return "normalize_bounds"; } + void updt_params(params_ref const & p) override { m_imp->updt_params(p); } diff --git a/src/tactic/arith/pb2bv_tactic.cpp b/src/tactic/arith/pb2bv_tactic.cpp index 98724923b..b63c85f1b 100644 --- a/src/tactic/arith/pb2bv_tactic.cpp +++ b/src/tactic/arith/pb2bv_tactic.cpp @@ -1007,6 +1007,8 @@ public: dealloc(m_imp); } + char const* name() const override { return "pb2bv"; } + void updt_params(params_ref const & p) override { m_params = p; m_imp->updt_params(p); diff --git a/src/tactic/arith/propagate_ineqs_tactic.cpp b/src/tactic/arith/propagate_ineqs_tactic.cpp index f4169cfba..d55ea4ecf 100644 --- a/src/tactic/arith/propagate_ineqs_tactic.cpp +++ b/src/tactic/arith/propagate_ineqs_tactic.cpp @@ -49,6 +49,8 @@ public: ~propagate_ineqs_tactic() override; + char const* name() const override { return "propagate_ineqs"; } + void updt_params(params_ref const & p) override; void collect_param_descrs(param_descrs & r) override {} diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp index 1691fe29a..db43a3ee6 100644 --- a/src/tactic/arith/purify_arith_tactic.cpp +++ b/src/tactic/arith/purify_arith_tactic.cpp @@ -903,6 +903,8 @@ public: ~purify_arith_tactic() override { } + char const* name() const override { return "purify_arith"; } + void updt_params(params_ref const & p) override { m_params = p; } diff --git a/src/tactic/arith/recover_01_tactic.cpp b/src/tactic/arith/recover_01_tactic.cpp index 7e1fe17ca..a7cef82e3 100644 --- a/src/tactic/arith/recover_01_tactic.cpp +++ b/src/tactic/arith/recover_01_tactic.cpp @@ -398,6 +398,8 @@ public: dealloc(m_imp); } + char const* name() const override { return "recover_01"; } + void updt_params(params_ref const & p) override { m_params = p; m_imp->updt_params(p); diff --git a/src/tactic/bv/bit_blaster_tactic.cpp b/src/tactic/bv/bit_blaster_tactic.cpp index 60dabbf5b..744f207f3 100644 --- a/src/tactic/bv/bit_blaster_tactic.cpp +++ b/src/tactic/bv/bit_blaster_tactic.cpp @@ -119,6 +119,8 @@ public: dealloc(m_imp); } + char const* name() const override { return "bit_blaster"; } + void updt_params(params_ref const & p) override { m_params = p; m_imp->updt_params(p); diff --git a/src/tactic/bv/bv1_blaster_tactic.cpp b/src/tactic/bv/bv1_blaster_tactic.cpp index 9fd077599..3af58bf66 100644 --- a/src/tactic/bv/bv1_blaster_tactic.cpp +++ b/src/tactic/bv/bv1_blaster_tactic.cpp @@ -431,6 +431,8 @@ public: dealloc(m_imp); } + char const* name() const override { return "bv1_blaster"; } + void updt_params(params_ref const & p) override { m_params = p; m_imp->m_rw.cfg().updt_params(p); diff --git a/src/tactic/bv/bv_bound_chk_tactic.cpp b/src/tactic/bv/bv_bound_chk_tactic.cpp index baef6c4f2..e0b6e4d81 100644 --- a/src/tactic/bv/bv_bound_chk_tactic.cpp +++ b/src/tactic/bv/bv_bound_chk_tactic.cpp @@ -140,6 +140,7 @@ public: void cleanup() override; void collect_statistics(statistics & st) const override; void reset_statistics() override; + char const* name() const override { return "bv_bound_chk"; } }; class bv_bound_chk_tactic::imp { diff --git a/src/tactic/bv/bv_size_reduction_tactic.cpp b/src/tactic/bv/bv_size_reduction_tactic.cpp index 5b9a4b21e..a9d15a2a6 100644 --- a/src/tactic/bv/bv_size_reduction_tactic.cpp +++ b/src/tactic/bv/bv_size_reduction_tactic.cpp @@ -54,6 +54,8 @@ public: return alloc(bv_size_reduction_tactic, m); } + char const* name() const override { return "bv_size"; } + void operator()(goal_ref const & g, goal_ref_buffer & result) override; void cleanup() override { diff --git a/src/tactic/bv/bvarray2uf_tactic.cpp b/src/tactic/bv/bvarray2uf_tactic.cpp index 0d1925a4a..d0bd6538b 100644 --- a/src/tactic/bv/bvarray2uf_tactic.cpp +++ b/src/tactic/bv/bvarray2uf_tactic.cpp @@ -113,6 +113,8 @@ public: dealloc(m_imp); } + char const* name() const override { return "bvarray2uf"; } + void updt_params(params_ref const & p) override { m_params = p; m_imp->updt_params(p); diff --git a/src/tactic/bv/dt2bv_tactic.cpp b/src/tactic/bv/dt2bv_tactic.cpp index 3b18222af..4f9ae6e9d 100644 --- a/src/tactic/bv/dt2bv_tactic.cpp +++ b/src/tactic/bv/dt2bv_tactic.cpp @@ -104,6 +104,8 @@ public: dt2bv_tactic(ast_manager& m, params_ref const& p): m(m), m_params(p), m_dt(m), m_bv(m), m_is_fd(*this) {} + + char const* name() const override { return "dt2bv"; } tactic * translate(ast_manager & m) override { return alloc(dt2bv_tactic, m, m_params); diff --git a/src/tactic/bv/elim_small_bv_tactic.cpp b/src/tactic/bv/elim_small_bv_tactic.cpp index 178a8fc77..7c72abde9 100644 --- a/src/tactic/bv/elim_small_bv_tactic.cpp +++ b/src/tactic/bv/elim_small_bv_tactic.cpp @@ -234,6 +234,8 @@ public: m_params(p) { } + char const* name() const override { return "elim_small_bv"; } + tactic * translate(ast_manager & m) override { return alloc(elim_small_bv_tactic, m, m_params); } diff --git a/src/tactic/bv/max_bv_sharing_tactic.cpp b/src/tactic/bv/max_bv_sharing_tactic.cpp index 16e4b9679..0efe4f58c 100644 --- a/src/tactic/bv/max_bv_sharing_tactic.cpp +++ b/src/tactic/bv/max_bv_sharing_tactic.cpp @@ -277,6 +277,8 @@ public: dealloc(m_imp); } + char const* name() const override { return "max_bv_sharing"; } + void updt_params(params_ref const & p) override { m_params = p; m_imp->m_rw.cfg().updt_params(p); diff --git a/src/tactic/core/blast_term_ite_tactic.cpp b/src/tactic/core/blast_term_ite_tactic.cpp index 97662a0c9..fe1269732 100644 --- a/src/tactic/core/blast_term_ite_tactic.cpp +++ b/src/tactic/core/blast_term_ite_tactic.cpp @@ -171,6 +171,8 @@ public: dealloc(m_imp); } + char const* name() const override { return "blast_term_ite"; } + void updt_params(params_ref const & p) override { m_params = p; m_imp->m_rw.m_cfg.updt_params(p); diff --git a/src/tactic/core/cofactor_term_ite_tactic.cpp b/src/tactic/core/cofactor_term_ite_tactic.cpp index 8260d59c7..d1b8f5b1b 100644 --- a/src/tactic/core/cofactor_term_ite_tactic.cpp +++ b/src/tactic/core/cofactor_term_ite_tactic.cpp @@ -51,6 +51,7 @@ public: } ~cofactor_term_ite_tactic() override {} + char const* name() const override { return "cofactor"; } void updt_params(params_ref const & p) override { m_params = p; m_elim_ite.updt_params(p); } void collect_param_descrs(param_descrs & r) override { m_elim_ite.collect_param_descrs(r); } diff --git a/src/tactic/core/collect_statistics_tactic.cpp b/src/tactic/core/collect_statistics_tactic.cpp index b3c6d0e24..3d8ebfb12 100644 --- a/src/tactic/core/collect_statistics_tactic.cpp +++ b/src/tactic/core/collect_statistics_tactic.cpp @@ -53,6 +53,8 @@ public: ~collect_statistics_tactic() override {} + char const* name() const override { return "collect_statistics"; } + tactic * translate(ast_manager & m_) override { return alloc(collect_statistics_tactic, m_, m_params); } diff --git a/src/tactic/core/ctx_simplify_tactic.h b/src/tactic/core/ctx_simplify_tactic.h index e7c1660c8..0beced06e 100644 --- a/src/tactic/core/ctx_simplify_tactic.h +++ b/src/tactic/core/ctx_simplify_tactic.h @@ -49,6 +49,8 @@ public: ~ctx_simplify_tactic() override; + char const* name() const override { return "ctx_simplify"; } + void updt_params(params_ref const & p) override; static void get_param_descrs(param_descrs & r); void collect_param_descrs(param_descrs & r) override { get_param_descrs(r); } diff --git a/src/tactic/core/der_tactic.cpp b/src/tactic/core/der_tactic.cpp index f26202015..011804803 100644 --- a/src/tactic/core/der_tactic.cpp +++ b/src/tactic/core/der_tactic.cpp @@ -68,6 +68,8 @@ public: ~der_tactic() override { dealloc(m_imp); } + + char const* name() const override { return "der"; } void operator()(goal_ref const & in, goal_ref_buffer & result) override { diff --git a/src/tactic/core/distribute_forall_tactic.cpp b/src/tactic/core/distribute_forall_tactic.cpp index cb7eac498..1d171aae3 100644 --- a/src/tactic/core/distribute_forall_tactic.cpp +++ b/src/tactic/core/distribute_forall_tactic.cpp @@ -102,6 +102,8 @@ public: return alloc(distribute_forall_tactic); } + char const* name() const override { return "distribute_forall"; } + void operator()(goal_ref const & g, goal_ref_buffer & result) override { ast_manager & m = g->m(); diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp index 719de8911..1dda062c8 100644 --- a/src/tactic/core/dom_simplify_tactic.cpp +++ b/src/tactic/core/dom_simplify_tactic.cpp @@ -182,6 +182,7 @@ tactic * dom_simplify_tactic::translate(ast_manager & m) { return alloc(dom_simplify_tactic, m, m_simplifier->translate(m), m_params); } + void dom_simplify_tactic::operator()(goal_ref const & in, goal_ref_buffer & result) { tactic_report report("dom-simplify", *in.get()); simplify_goal(*(in.get())); diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h index 541d50838..b5d5e1ce9 100644 --- a/src/tactic/core/dom_simplify_tactic.h +++ b/src/tactic/core/dom_simplify_tactic.h @@ -131,6 +131,8 @@ public: ~dom_simplify_tactic() override; + char const* name() const override { return "dom_simplify"; } + tactic * translate(ast_manager & m) override; void updt_params(params_ref const & p) override {} static void get_param_descrs(param_descrs & r) {} diff --git a/src/tactic/core/elim_term_ite_tactic.cpp b/src/tactic/core/elim_term_ite_tactic.cpp index c2d972b62..42adf04a9 100644 --- a/src/tactic/core/elim_term_ite_tactic.cpp +++ b/src/tactic/core/elim_term_ite_tactic.cpp @@ -136,6 +136,8 @@ public: dealloc(m_imp); } + char const* name() const override { return "elim_term_ite"; } + tactic * translate(ast_manager & m) override { return alloc(elim_term_ite_tactic, m, m_params); } diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp index 4df4d1fc4..915a0f3c0 100644 --- a/src/tactic/core/elim_uncnstr_tactic.cpp +++ b/src/tactic/core/elim_uncnstr_tactic.cpp @@ -853,6 +853,8 @@ public: updt_params(p); } + char const* name() const override { return "elim_uncstr"; } + tactic * translate(ast_manager & m) override { return alloc(elim_uncnstr_tactic, m, m_params); } diff --git a/src/tactic/core/injectivity_tactic.cpp b/src/tactic/core/injectivity_tactic.cpp index 82e78d771..485eda4dd 100644 --- a/src/tactic/core/injectivity_tactic.cpp +++ b/src/tactic/core/injectivity_tactic.cpp @@ -255,6 +255,8 @@ public: dealloc(m_map); } + char const* name() const override { return "injectivity"; } + void updt_params(params_ref const & p) override { m_params = p; m_finder->updt_params(p); diff --git a/src/tactic/core/nnf_tactic.cpp b/src/tactic/core/nnf_tactic.cpp index 72ebb949d..164cf9311 100644 --- a/src/tactic/core/nnf_tactic.cpp +++ b/src/tactic/core/nnf_tactic.cpp @@ -49,6 +49,8 @@ public: ~nnf_tactic() override {} + char const* name() const override { return "nnf"; } + void updt_params(params_ref const & p) override { m_params = p; } void collect_param_descrs(param_descrs & r) override { nnf::get_param_descrs(r); } diff --git a/src/tactic/core/occf_tactic.cpp b/src/tactic/core/occf_tactic.cpp index b1f9d3f93..c3c027fef 100644 --- a/src/tactic/core/occf_tactic.cpp +++ b/src/tactic/core/occf_tactic.cpp @@ -196,6 +196,8 @@ public: dealloc(m_imp); } + char const* name() const override { return "occf"; } + void updt_params(params_ref const & p) override {} void collect_param_descrs(param_descrs & r) override {} diff --git a/src/tactic/core/pb_preprocess_tactic.cpp b/src/tactic/core/pb_preprocess_tactic.cpp index 1d4805c67..ef3db804b 100644 --- a/src/tactic/core/pb_preprocess_tactic.cpp +++ b/src/tactic/core/pb_preprocess_tactic.cpp @@ -107,6 +107,8 @@ public: tactic * translate(ast_manager & m) override { return alloc(pb_preprocess_tactic, m); } + + char const* name() const override { return "pb_preprocess"; } void operator()( goal_ref const & g, diff --git a/src/tactic/core/propagate_values_tactic.cpp b/src/tactic/core/propagate_values_tactic.cpp index 6cf340e57..b735de4b7 100644 --- a/src/tactic/core/propagate_values_tactic.cpp +++ b/src/tactic/core/propagate_values_tactic.cpp @@ -216,6 +216,8 @@ public: return alloc(propagate_values_tactic, m, m_params); } + char const* name() const override { return "propagate_values"; } + void updt_params(params_ref const & p) override { m_params = p; m_r.updt_params(p); diff --git a/src/tactic/core/reduce_args_tactic.cpp b/src/tactic/core/reduce_args_tactic.cpp index f6ea1b09b..436ee3272 100644 --- a/src/tactic/core/reduce_args_tactic.cpp +++ b/src/tactic/core/reduce_args_tactic.cpp @@ -64,6 +64,7 @@ Notes: class reduce_args_tactic : public tactic { struct imp; imp * m_imp; + public: reduce_args_tactic(ast_manager & m); @@ -72,9 +73,13 @@ public: } ~reduce_args_tactic() override; + + char const* name() const override { return "reduce_args"; } void operator()(goal_ref const & g, goal_ref_buffer & result) override; void cleanup() override; + unsigned user_propagate_register(expr* e) override; + void user_propagate_clear() override; }; tactic * mk_reduce_args_tactic(ast_manager & m, params_ref const & p) { @@ -82,14 +87,15 @@ tactic * mk_reduce_args_tactic(ast_manager & m, params_ref const & p) { } struct reduce_args_tactic::imp { - ast_manager & m_manager; + expr_ref_vector m_vars; + ast_manager & m; bv_util m_bv; array_util m_ar; - ast_manager & m() const { return m_manager; } imp(ast_manager & m): - m_manager(m), + m_vars(m), + m(m), m_bv(m), m_ar(m) { } @@ -115,17 +121,17 @@ struct reduce_args_tactic::imp { } void checkpoint() { - tactic::checkpoint(m_manager); + tactic::checkpoint(m); } struct find_non_candidates_proc { - ast_manager & m_manager; + ast_manager & m; bv_util & m_bv; array_util & m_ar; obj_hashtable & m_non_candidates; find_non_candidates_proc(ast_manager & m, bv_util & bv, array_util& ar, obj_hashtable & non_candidates): - m_manager(m), + m(m), m_bv(bv), m_ar(ar), m_non_candidates(non_candidates) { @@ -151,7 +157,7 @@ struct reduce_args_tactic::imp { unsigned j = n->get_num_args(); while (j > 0) { --j; - if (may_be_unique(m_manager, m_bv, n->get_arg(j))) + if (may_be_unique(m, m_bv, n->get_arg(j))) return; } m_non_candidates.insert(d); @@ -164,7 +170,10 @@ struct reduce_args_tactic::imp { */ void find_non_candidates(goal const & g, obj_hashtable & non_candidates) { non_candidates.reset(); - find_non_candidates_proc proc(m_manager, m_bv, m_ar, non_candidates); + for (expr* v : m_vars) + if (is_app(v)) + non_candidates.insert(to_app(v)->get_decl()); + find_non_candidates_proc proc(m, m_bv, m_ar, non_candidates); expr_fast_mark1 visited; unsigned sz = g.size(); for (unsigned i = 0; i < sz; i++) { @@ -173,23 +182,20 @@ struct reduce_args_tactic::imp { } TRACE("reduce_args", tout << "non_candidates:\n"; - obj_hashtable::iterator it = non_candidates.begin(); - obj_hashtable::iterator end = non_candidates.end(); - for (; it != end; ++it) { - func_decl * d = *it; - tout << d->get_name() << "\n"; - }); + for (func_decl* d : non_candidates) + tout << d->get_name() << "\n"; + ); } struct populate_decl2args_proc { - ast_manager & m_manager; + ast_manager & m; bv_util & m_bv; obj_hashtable & m_non_candidates; obj_map & m_decl2args; obj_map > m_decl2base; // for args = base + offset populate_decl2args_proc(ast_manager & m, bv_util & bv, obj_hashtable & nc, obj_map & d): - m_manager(m), m_bv(bv), m_non_candidates(nc), m_decl2args(d) {} + m(m), m_bv(bv), m_non_candidates(nc), m_decl2args(d) {} void operator()(var * n) {} void operator()(quantifier * n) {} @@ -213,7 +219,7 @@ struct reduce_args_tactic::imp { it->m_value.reserve(j); while (j > 0) { --j; - it->m_value.set(j, may_be_unique(m_manager, m_bv, n->get_arg(j), base)); + it->m_value.set(j, may_be_unique(m, m_bv, n->get_arg(j), base)); bases[j] = base; } } else { @@ -221,7 +227,7 @@ struct reduce_args_tactic::imp { SASSERT(j == it->m_value.size()); while (j > 0) { --j; - it->m_value.set(j, it->m_value.get(j) && may_be_unique(m_manager, m_bv, n->get_arg(j), base) && bases[j] == base); + it->m_value.set(j, it->m_value.get(j) && may_be_unique(m, m_bv, n->get_arg(j), base) && bases[j] == base); } } } @@ -232,7 +238,7 @@ struct reduce_args_tactic::imp { obj_map & decl2args) { expr_fast_mark1 visited; decl2args.reset(); - populate_decl2args_proc proc(m_manager, m_bv, non_candidates, decl2args); + populate_decl2args_proc proc(m, m_bv, non_candidates, decl2args); unsigned sz = g.size(); for (unsigned i = 0; i < sz; i++) { checkpoint(); @@ -241,28 +247,24 @@ struct reduce_args_tactic::imp { // Remove all cases where the simplification is not applicable. ptr_buffer bad_decls; - obj_map::iterator it = decl2args.begin(); - obj_map::iterator end = decl2args.end(); - for (; it != end; it++) { + for (auto const& [k, v] : decl2args) { bool is_zero = true; - for (unsigned i = 0; i < it->m_value.size() && is_zero ; i++) { - if (it->m_value.get(i)) + for (unsigned i = 0; i < v.size() && is_zero; i++) { + if (v.get(i)) is_zero = false; } - if (is_zero) - bad_decls.push_back(it->m_key); + if (is_zero) + bad_decls.push_back(k); } - ptr_buffer::iterator it2 = bad_decls.begin(); - ptr_buffer::iterator end2 = bad_decls.end(); - for (; it2 != end2; ++it2) - decl2args.erase(*it2); + for (func_decl* a : bad_decls) + decl2args.erase(a); TRACE("reduce_args", tout << "decl2args:" << std::endl; - for (obj_map::iterator it = decl2args.begin() ; it != decl2args.end() ; it++) { - tout << it->m_key->get_name() << ": "; - for (unsigned i = 0 ; i < it->m_value.size() ; i++) - tout << (it->m_value.get(i) ? "1" : "0"); + for (auto const& [k, v] : decl2args) { + tout << k->get_name() << ": "; + for (unsigned i = 0; i < v.size(); ++i) + tout << (v.get(i) ? "1" : "0"); tout << std::endl; }); } @@ -306,22 +308,17 @@ struct reduce_args_tactic::imp { typedef obj_map decl2arg2func_map; struct reduce_args_ctx { - ast_manager & m_manager; + ast_manager & m; decl2arg2func_map m_decl2arg2funcs; - reduce_args_ctx(ast_manager & m): m_manager(m) { + reduce_args_ctx(ast_manager & m): m(m) { } ~reduce_args_ctx() { - obj_map::iterator it = m_decl2arg2funcs.begin(); - obj_map::iterator end = m_decl2arg2funcs.end(); - for (; it != end; ++it) { - arg2func * map = it->m_value; - arg2func::iterator it2 = map->begin(); - arg2func::iterator end2 = map->end(); - for (; it2 != end2; ++it2) { - m_manager.dec_ref(it2->m_key); - m_manager.dec_ref(it2->m_value); + for (auto const& [_, map] : m_decl2arg2funcs) { + for (auto const& [k, v] : *map) { + m.dec_ref(k); + m.dec_ref(v); } dealloc(map); } @@ -335,7 +332,7 @@ struct reduce_args_tactic::imp { decl2arg2func_map & m_decl2arg2funcs; reduce_args_rw_cfg(imp & owner, obj_map & decl2args, decl2arg2func_map & decl2arg2funcs): - m(owner.m_manager), + m(owner.m), m_owner(owner), m_decl2args(decl2args), m_decl2arg2funcs(decl2arg2funcs) { @@ -391,16 +388,16 @@ struct reduce_args_tactic::imp { reduce_args_rw_cfg m_cfg; public: reduce_args_rw(imp & owner, obj_map & decl2args, decl2arg2func_map & decl2arg2funcs): - rewriter_tpl(owner.m_manager, false, m_cfg), + rewriter_tpl(owner.m, false, m_cfg), m_cfg(owner, decl2args, decl2arg2funcs) { } }; model_converter * mk_mc(obj_map & decl2args, decl2arg2func_map & decl2arg2funcs) { ptr_buffer new_args; - var_ref_vector new_vars(m_manager); + var_ref_vector new_vars(m); ptr_buffer new_eqs; - generic_model_converter * f_mc = alloc(generic_model_converter, m_manager, "reduce_args"); + generic_model_converter * f_mc = alloc(generic_model_converter, m, "reduce_args"); for (auto const& kv : decl2arg2funcs) { func_decl * f = kv.m_key; arg2func * map = kv.m_value; @@ -410,18 +407,14 @@ struct reduce_args_tactic::imp { new_vars.reset(); new_args.reset(); for (unsigned i = 0; i < f->get_arity(); i++) { - new_vars.push_back(m_manager.mk_var(i, f->get_domain(i))); + new_vars.push_back(m.mk_var(i, f->get_domain(i))); if (!bv.get(i)) new_args.push_back(new_vars.back()); } - arg2func::iterator it2 = map->begin(); - arg2func::iterator end2 = map->end(); - for (; it2 != end2; ++it2) { - app * t = it2->m_key; - func_decl * new_def = it2->m_value; + for (auto const& [t, new_def] : *map) { f_mc->hide(new_def); SASSERT(new_def->get_arity() == new_args.size()); - app * new_t = m_manager.mk_app(new_def, new_args.size(), new_args.data()); + app * new_t = m.mk_app(new_def, new_args.size(), new_args.data()); if (def == nullptr) { def = new_t; } @@ -429,15 +422,15 @@ struct reduce_args_tactic::imp { new_eqs.reset(); for (unsigned i = 0; i < f->get_arity(); i++) { if (bv.get(i)) - new_eqs.push_back(m_manager.mk_eq(new_vars.get(i), t->get_arg(i))); + new_eqs.push_back(m.mk_eq(new_vars.get(i), t->get_arg(i))); } SASSERT(new_eqs.size() > 0); expr * cond; if (new_eqs.size() == 1) cond = new_eqs[0]; else - cond = m_manager.mk_and(new_eqs.size(), new_eqs.data()); - def = m_manager.mk_ite(cond, new_t, def); + cond = m.mk_and(new_eqs.size(), new_eqs.data()); + def = m.mk_ite(cond, new_t, def); } } SASSERT(def); @@ -459,7 +452,7 @@ struct reduce_args_tactic::imp { if (decl2args.empty()) return; - reduce_args_ctx ctx(m_manager); + reduce_args_ctx ctx(m); reduce_args_rw rw(*this, decl2args, ctx.m_decl2arg2funcs); unsigned sz = g.size(); @@ -467,7 +460,7 @@ struct reduce_args_tactic::imp { if (g.inconsistent()) break; expr * f = g.form(i); - expr_ref new_f(m_manager); + expr_ref new_f(m); rw(f, new_f); g.update(i, new_f); } @@ -482,6 +475,7 @@ struct reduce_args_tactic::imp { }; reduce_args_tactic::reduce_args_tactic(ast_manager & m) { + expr_ref_vector vars(m); m_imp = alloc(imp, m); } @@ -493,7 +487,7 @@ void reduce_args_tactic::operator()(goal_ref const & g, goal_ref_buffer & result) { fail_if_unsat_core_generation("reduce-args", g); result.reset(); - if (!m_imp->m().proofs_enabled()) { + if (!m_imp->m.proofs_enabled()) { m_imp->operator()(*(g.get())); } g->inc_depth(); @@ -501,8 +495,21 @@ void reduce_args_tactic::operator()(goal_ref const & g, } void reduce_args_tactic::cleanup() { - ast_manager & m = m_imp->m(); + ast_manager & m = m_imp->m; + expr_ref_vector vars = m_imp->m_vars; m_imp->~imp(); m_imp = new (m_imp) imp(m); + m_imp->m_vars.append(vars); } +unsigned reduce_args_tactic::user_propagate_register(expr* e) { + m_imp->m_vars.push_back(e); + return 0; +} + +void reduce_args_tactic::user_propagate_clear() { + m_imp->m_vars.reset(); +} + + + diff --git a/src/tactic/core/reduce_invertible_tactic.cpp b/src/tactic/core/reduce_invertible_tactic.cpp index a60f20aab..cfcc42482 100644 --- a/src/tactic/core/reduce_invertible_tactic.cpp +++ b/src/tactic/core/reduce_invertible_tactic.cpp @@ -47,6 +47,8 @@ public: ~reduce_invertible_tactic() override { } + char const* name() const override { return "reduce_invertible"; } + tactic * translate(ast_manager & m) override { return alloc(reduce_invertible_tactic, m); } diff --git a/src/tactic/core/simplify_tactic.h b/src/tactic/core/simplify_tactic.h index 9fff34190..fc262f998 100644 --- a/src/tactic/core/simplify_tactic.h +++ b/src/tactic/core/simplify_tactic.h @@ -43,6 +43,8 @@ public: tactic * translate(ast_manager & m) override { return alloc(simplify_tactic, m, m_params); } + char const* name() const override { return "simplify"; } + }; tactic * mk_simplify_tactic(ast_manager & m, params_ref const & p = params_ref()); diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp index b9feaf949..9d844b7ed 100644 --- a/src/tactic/core/solve_eqs_tactic.cpp +++ b/src/tactic/core/solve_eqs_tactic.cpp @@ -1089,6 +1089,8 @@ public: dealloc(m_imp); } + char const* name() const override { return "solve_eqs"; } + void updt_params(params_ref const & p) override { m_params = p; m_imp->updt_params(p); diff --git a/src/tactic/core/special_relations_tactic.h b/src/tactic/core/special_relations_tactic.h index 6bb72852d..a1cafb7c0 100644 --- a/src/tactic/core/special_relations_tactic.h +++ b/src/tactic/core/special_relations_tactic.h @@ -59,6 +59,8 @@ public: tactic * translate(ast_manager & m) override { return alloc(special_relations_tactic, m, m_params); } + char const* name() const override { return "special_relations"; } + }; tactic * mk_special_relations_tactic(ast_manager & m, params_ref const & p = params_ref()); diff --git a/src/tactic/core/split_clause_tactic.cpp b/src/tactic/core/split_clause_tactic.cpp index 453e4a218..12b76b638 100644 --- a/src/tactic/core/split_clause_tactic.cpp +++ b/src/tactic/core/split_clause_tactic.cpp @@ -91,6 +91,8 @@ public: ~split_clause_tactic() override { } + char const* name() const override { return "split_clause"; } + void updt_params(params_ref const & p) override { m_largest_clause = p.get_bool("split_largest_clause", false); } diff --git a/src/tactic/core/symmetry_reduce_tactic.cpp b/src/tactic/core/symmetry_reduce_tactic.cpp index 17049e2d1..9aa4c9448 100644 --- a/src/tactic/core/symmetry_reduce_tactic.cpp +++ b/src/tactic/core/symmetry_reduce_tactic.cpp @@ -37,6 +37,8 @@ public: } ~symmetry_reduce_tactic() override; + + char const* name() const override { return "symmetry_reduce"; } void operator()(goal_ref const & g, goal_ref_buffer & result) override; diff --git a/src/tactic/core/tseitin_cnf_tactic.cpp b/src/tactic/core/tseitin_cnf_tactic.cpp index b466c50fb..e26fded8f 100644 --- a/src/tactic/core/tseitin_cnf_tactic.cpp +++ b/src/tactic/core/tseitin_cnf_tactic.cpp @@ -891,6 +891,8 @@ public: dealloc(m_imp); } + char const* name() const override { return "tseitin_cnf"; } + void updt_params(params_ref const & p) override { m_params = p; m_imp->updt_params(p); diff --git a/src/tactic/fpa/fpa2bv_tactic.cpp b/src/tactic/fpa/fpa2bv_tactic.cpp index 13cb4c3e7..be98dea00 100644 --- a/src/tactic/fpa/fpa2bv_tactic.cpp +++ b/src/tactic/fpa/fpa2bv_tactic.cpp @@ -120,6 +120,8 @@ public: dealloc(m_imp); } + char const* name() const override { return "fp2bv"; } + void updt_params(params_ref const & p) override { m_params = p; m_imp->updt_params(p); diff --git a/src/tactic/portfolio/solver_subsumption_tactic.cpp b/src/tactic/portfolio/solver_subsumption_tactic.cpp index 3a23f5984..6b275508b 100644 --- a/src/tactic/portfolio/solver_subsumption_tactic.cpp +++ b/src/tactic/portfolio/solver_subsumption_tactic.cpp @@ -105,12 +105,12 @@ class solver_subsumption_tactic : public tactic { vector> pre(mid, fmls.data()); vector> post(fmls.size() - mid, fmls.data() + mid); push(); - for (auto [p, f] : post) + for (auto const& [p, f] : post) assert_expr(f); simplify(pre, change); pop(); push(); - for (auto [p, f] : pre) + for (auto const& [p, f] : pre) assert_expr(f); simplify(post, change); pop(); @@ -133,6 +133,8 @@ public: ~solver_subsumption_tactic() override {} + char const* name() const override { return "solver_subsumption"; } + void updt_params(params_ref const& p) override { m_params = p; unsigned max_conflicts = p.get_uint("max_conflicts", 2); diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp index fd0dcaa3b..ece6940f3 100644 --- a/src/tactic/sls/sls_tactic.cpp +++ b/src/tactic/sls/sls_tactic.cpp @@ -50,6 +50,8 @@ public: dealloc(m_engine); } + char const* name() const override { return "sls"; } + void updt_params(params_ref const & p) override { m_params = p; m_engine->updt_params(p); diff --git a/src/tactic/smtlogics/qfufbv_tactic.cpp b/src/tactic/smtlogics/qfufbv_tactic.cpp index ad9e8b46f..57c6ae99a 100644 --- a/src/tactic/smtlogics/qfufbv_tactic.cpp +++ b/src/tactic/smtlogics/qfufbv_tactic.cpp @@ -53,6 +53,8 @@ public: ~qfufbv_ackr_tactic() override { } + char const* name() const override { return "qfufbv_ackr"; } + void operator()(goal_ref const & g, goal_ref_buffer & result) override { ast_manager& m(g->m()); tactic_report report("qfufbv_ackr", *g); diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp index 66f58f71e..575435904 100644 --- a/src/tactic/tactic.cpp +++ b/src/tactic/tactic.cpp @@ -90,6 +90,8 @@ public: void cleanup() override {} + char const* name() const override { return "fail"; } + tactic * translate(ast_manager & m) override { return this; } }; diff --git a/src/tactic/tactic.h b/src/tactic/tactic.h index 37a211cb4..4c4b9358d 100644 --- a/src/tactic/tactic.h +++ b/src/tactic/tactic.h @@ -20,17 +20,18 @@ Notes: --*/ #pragma once -#include "tactic/goal.h" #include "util/params.h" -#include "util/statistics.h" -#include "tactic/tactic_exception.h" #include "util/lbool.h" +#include "util/statistics.h" +#include "tactic/user_propagator_base.h" +#include "tactic/goal.h" +#include "tactic/tactic_exception.h" class progress_callback; typedef ptr_buffer goal_buffer; -class tactic { +class tactic : public user_propagator::core { unsigned m_ref_count; public: tactic():m_ref_count(0) {} @@ -76,6 +77,17 @@ public: static void checkpoint(ast_manager& m); + void user_propagate_init( + void* ctx, + user_propagator::push_eh_t& push_eh, + user_propagator::pop_eh_t& pop_eh, + user_propagator::fresh_eh_t& fresh_eh) override { + throw default_exception("tactic does not support user propagation"); + } + + unsigned user_propagate_register(expr* e) override { return 0; } + virtual char const* name() const = 0; + protected: friend class nary_tactical; friend class binary_tactical; @@ -105,6 +117,7 @@ public: void operator()(goal_ref const & in, goal_ref_buffer& result) override; void cleanup() override {} tactic * translate(ast_manager & m) override { return this; } + char const* name() const override { return "skip"; } }; tactic * mk_skip_tactic(); diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index 07be90518..19009aa44 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -100,6 +100,8 @@ class and_then_tactical : public binary_tactical { public: and_then_tactical(tactic * t1, tactic * t2):binary_tactical(t1, t2) {} + char const* name() const override { return "and_then"; } + void operator()(goal_ref const & in, goal_ref_buffer& result) override { bool proofs_enabled = in->proofs_enabled(); @@ -164,6 +166,40 @@ public: return translate_core(m); } + void user_propagate_init( + void* ctx, + user_propagator::push_eh_t& push_eh, + user_propagator::pop_eh_t& pop_eh, + user_propagator::fresh_eh_t& fresh_eh) override { + m_t2->user_propagate_init(ctx, push_eh, pop_eh, fresh_eh); + } + + void user_propagate_register_fixed(user_propagator::fixed_eh_t& fixed_eh) override { + m_t2->user_propagate_register_fixed(fixed_eh); + } + + void user_propagate_register_final(user_propagator::final_eh_t& final_eh) override { + m_t2->user_propagate_register_final(final_eh); + } + + void user_propagate_register_eq(user_propagator::eq_eh_t& eq_eh) override { + m_t2->user_propagate_register_eq(eq_eh); + } + + void user_propagate_register_diseq(user_propagator::eq_eh_t& diseq_eh) override { + m_t2->user_propagate_register_diseq(diseq_eh); + } + + unsigned user_propagate_register(expr* e) override { + m_t1->user_propagate_register(e); + return m_t2->user_propagate_register(e); + } + + void user_propagate_clear() override { + m_t1->user_propagate_clear(); + m_t2->user_propagate_clear(); + } + }; tactic * and_then(tactic * t1, tactic * t2) { @@ -279,6 +315,8 @@ class or_else_tactical : public nary_tactical { public: or_else_tactical(unsigned num, tactic * const * ts):nary_tactical(num, ts) { SASSERT(num > 0); } + char const* name() const override { return "or_else"; } + void operator()(goal_ref const & in, goal_ref_buffer& result) override { goal orig(*(in.get())); unsigned sz = m_ts.size(); @@ -380,6 +418,8 @@ public: error_code = 0; } + char const* name() const override { return "par"; } + void operator()(goal_ref const & in, goal_ref_buffer& result) override { bool use_seq; use_seq = false; @@ -516,6 +556,8 @@ class par_and_then_tactical : public and_then_tactical { public: par_and_then_tactical(tactic * t1, tactic * t2):and_then_tactical(t1, t2) {} + char const* name() const override { return "par_then"; } + void operator()(goal_ref const & in, goal_ref_buffer& result) override { bool use_seq; use_seq = false; @@ -783,6 +825,9 @@ public: void reset() override { m_t->reset(); } void set_logic(symbol const& l) override { m_t->set_logic(l); } void set_progress_callback(progress_callback * callback) override { m_t->set_progress_callback(callback); } + unsigned user_propagate_register(expr* e) override { return m_t->user_propagate_register(e); } + void user_propagate_clear() override { m_t->user_propagate_clear(); } + protected: template @@ -878,6 +923,8 @@ public: unary_tactical(t), m_max_depth(max_depth) { } + + char const* name() const override { return "repeat"; } void operator()(goal_ref const & in, goal_ref_buffer& result) override { operator()(0, in, result); @@ -898,6 +945,8 @@ class fail_if_branching_tactical : public unary_tactical { public: fail_if_branching_tactical(tactic * t, unsigned threshold):unary_tactical(t), m_threshold(threshold) {} + char const* name() const override { return "fail_if_branching"; } + void operator()(goal_ref const & in, goal_ref_buffer& result) override { m_t->operator()(in, result); if (result.size() > m_threshold) { @@ -920,6 +969,8 @@ class cleanup_tactical : public unary_tactical { public: cleanup_tactical(tactic * t):unary_tactical(t) {} + char const* name() const override { return "cleanup"; } + void operator()(goal_ref const & in, goal_ref_buffer& result) override { m_t->operator()(in, result); m_t->cleanup(); @@ -939,6 +990,8 @@ class try_for_tactical : public unary_tactical { unsigned m_timeout; public: try_for_tactical(tactic * t, unsigned ts):unary_tactical(t), m_timeout(ts) {} + + char const* name() const override { return "try_for"; } void operator()(goal_ref const & in, goal_ref_buffer& result) override { cancel_eh eh(in->m().limit()); @@ -966,6 +1019,8 @@ public: t->updt_params(p); } + char const* name() const override { return "using_params"; } + void updt_params(params_ref const & p) override { TRACE("using_params", tout << "before p: " << p << "\n"; @@ -1015,6 +1070,8 @@ public: tactic * new_t = m_t->translate(m); return alloc(annotate_tactical, m_name.c_str(), new_t); } + + char const* name() const override { return "annotate"; } }; @@ -1030,6 +1087,8 @@ public: m_p(p) { SASSERT(m_p); } + + char const* name() const override { return "cond"; } void operator()(goal_ref const & in, goal_ref_buffer & result) override { if (m_p->operator()(*(in.get())).is_true()) @@ -1061,6 +1120,8 @@ public: SASSERT(m_p); } + char const* name() const override { return "fail_if"; } + void cleanup() override {} void operator()(goal_ref const & in, goal_ref_buffer& result) override { @@ -1086,6 +1147,8 @@ tactic * fail_if_not(probe * p) { class if_no_proofs_tactical : public unary_tactical { public: if_no_proofs_tactical(tactic * t):unary_tactical(t) {} + + char const* name() const override { return "if_no_proofs"; } void operator()(goal_ref const & in, goal_ref_buffer & result) override { if (in->proofs_enabled()) { @@ -1102,6 +1165,8 @@ public: class if_no_unsat_cores_tactical : public unary_tactical { public: if_no_unsat_cores_tactical(tactic * t):unary_tactical(t) {} + + char const* name() const override { return "if_no_unsat_cores"; } void operator()(goal_ref const & in, goal_ref_buffer& result) override { if (in->unsat_core_enabled()) { @@ -1118,6 +1183,8 @@ public: class if_no_models_tactical : public unary_tactical { public: if_no_models_tactical(tactic * t):unary_tactical(t) {} + + char const* name() const override { return "if_no_models"; } void operator()(goal_ref const & in, goal_ref_buffer& result) override { if (in->models_enabled()) { diff --git a/src/tactic/ufbv/macro_finder_tactic.cpp b/src/tactic/ufbv/macro_finder_tactic.cpp index 86c606538..c5745d85c 100644 --- a/src/tactic/ufbv/macro_finder_tactic.cpp +++ b/src/tactic/ufbv/macro_finder_tactic.cpp @@ -105,6 +105,8 @@ public: dealloc(m_imp); } + char const* name() const override { return "macro_finder"; } + void updt_params(params_ref const & p) override { m_params = p; m_imp->updt_params(p); diff --git a/src/tactic/ufbv/quasi_macros_tactic.cpp b/src/tactic/ufbv/quasi_macros_tactic.cpp index 33c2927bb..0e0cb7cb2 100644 --- a/src/tactic/ufbv/quasi_macros_tactic.cpp +++ b/src/tactic/ufbv/quasi_macros_tactic.cpp @@ -100,6 +100,8 @@ public: dealloc(m_imp); } + char const* name() const override { return "quasi_macros"; } + void updt_params(params_ref const & p) override { m_params = p; m_imp->updt_params(p); diff --git a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp index bb2b4d5be..d5bfec8fe 100644 --- a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp +++ b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp @@ -28,6 +28,8 @@ public: ufbv_rewriter_tactic(ast_manager & m, params_ref const & p): m_manager(m), m_params(p) {} + char const* name() const override { return "ufbv"; } + tactic * translate(ast_manager & m) override { return alloc(ufbv_rewriter_tactic, m, m_params); } diff --git a/src/tactic/user_propagator_base.h b/src/tactic/user_propagator_base.h new file mode 100644 index 000000000..899722c2a --- /dev/null +++ b/src/tactic/user_propagator_base.h @@ -0,0 +1,66 @@ + +#pragma once + +#include "ast/ast.h" + +namespace user_propagator { + + class callback { + public: + virtual ~callback() = default; + virtual void propagate_cb(unsigned num_fixed, unsigned const* fixed_ids, unsigned num_eqs, unsigned const* eq_lhs, unsigned const* eq_rhs, expr* conseq) = 0; + virtual unsigned register_cb(expr* e) = 0; + }; + + class context_obj { + public: + virtual ~context_obj() {} + }; + + typedef std::function final_eh_t; + typedef std::function fixed_eh_t; + typedef std::function eq_eh_t; + typedef std::function fresh_eh_t; + typedef std::function push_eh_t; + typedef std::function pop_eh_t; + + + class core { + public: + + virtual ~core() {} + + virtual void user_propagate_init( + void* ctx, + push_eh_t& push_eh, + pop_eh_t& pop_eh, + fresh_eh_t& fresh_eh) { + throw default_exception("user-propagators are only supported on the SMT solver"); + } + + virtual void user_propagate_register_fixed(fixed_eh_t& fixed_eh) { + throw default_exception("user-propagators are only supported on the SMT solver"); + } + + virtual void user_propagate_register_final(final_eh_t& final_eh) { + throw default_exception("user-propagators are only supported on the SMT solver"); + } + + virtual void user_propagate_register_eq(eq_eh_t& eq_eh) { + throw default_exception("user-propagators are only supported on the SMT solver"); + } + + virtual void user_propagate_register_diseq(eq_eh_t& diseq_eh) { + throw default_exception("user-propagators are only supported on the SMT solver"); + } + + virtual unsigned user_propagate_register(expr* e) { + throw default_exception("user-propagators are only supported on the SMT solver"); + } + + virtual void user_propagate_clear() { + } + + }; + +} diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp index 9d24d2787..d7329309c 100644 --- a/src/test/lp/lp.cpp +++ b/src/test/lp/lp.cpp @@ -1396,10 +1396,7 @@ void update_settings(argument_parser & args_parser, lp_settings& settings) { } template -void setup_solver(unsigned max_iterations, unsigned time_limit, bool look_for_min, argument_parser & args_parser, lp_solver * solver) { - if (max_iterations > 0) - solver->set_max_iterations_per_stage(max_iterations); - +void setup_solver(unsigned time_limit, bool look_for_min, argument_parser & args_parser, lp_solver * solver) { if (time_limit > 0) solver->set_time_limit(time_limit); @@ -1429,7 +1426,7 @@ void compare_solutions(mps_reader & reader, lp_solver reader(file_name); reader.read(); if (!reader.is_ok()) { @@ -1438,7 +1435,7 @@ void solve_mps_double(std::string file_name, bool look_for_min, unsigned max_ite } lp_solver * solver = reader.create_solver(dual); - setup_solver(max_iterations, time_limit, look_for_min, args_parser, solver); + setup_solver(time_limit, look_for_min, args_parser, solver); stopwatch sw; sw.start(); if (dual) { @@ -1461,7 +1458,7 @@ void solve_mps_double(std::string file_name, bool look_for_min, unsigned max_ite std::cout << "processed in " << span / 1000.0 << " seconds, running for " << solver->m_total_iterations << " iterations" << " one iter for " << (double)span/solver->m_total_iterations << " ms" << std::endl; if (compare_with_primal) { auto * primal_solver = reader.create_solver(false); - setup_solver(max_iterations, time_limit, look_for_min, args_parser, primal_solver); + setup_solver(time_limit, look_for_min, args_parser, primal_solver); primal_solver->find_maximal_solution(); if (solver->get_status() != primal_solver->get_status()) { std::cout << "statuses are different: dual " << lp_status_to_string(solver->get_status()) << " primal = " << lp_status_to_string(primal_solver->get_status()) << std::endl; @@ -1489,12 +1486,12 @@ void solve_mps_double(std::string file_name, bool look_for_min, unsigned max_ite delete solver; } -void solve_mps_rational(std::string file_name, bool look_for_min, unsigned max_iterations, unsigned time_limit, bool dual, argument_parser & args_parser) { +void solve_mps_rational(std::string file_name, bool look_for_min, unsigned time_limit, bool dual, argument_parser & args_parser) { mps_reader reader(file_name); reader.read(); if (reader.is_ok()) { auto * solver = reader.create_solver(dual); - setup_solver(max_iterations, time_limit, look_for_min, args_parser, solver); + setup_solver(time_limit, look_for_min, args_parser, solver); stopwatch sw; sw.start(); solver->find_maximal_solution(); @@ -1516,27 +1513,27 @@ void solve_mps_rational(std::string file_name, bool look_for_min, unsigned max_i std::cout << "cannot process " << file_name << std::endl; } } -void get_time_limit_and_max_iters_from_parser(argument_parser & args_parser, unsigned & time_limit, unsigned & max_iters); // forward definition +void get_time_limit_and_max_iters_from_parser(argument_parser & args_parser, unsigned & time_limit); // forward definition -void solve_mps(std::string file_name, bool look_for_min, unsigned max_iterations, unsigned time_limit, bool solve_for_rational, bool dual, bool compare_with_primal, argument_parser & args_parser) { +void solve_mps(std::string file_name, bool look_for_min, unsigned time_limit, bool solve_for_rational, bool dual, bool compare_with_primal, argument_parser & args_parser) { if (!solve_for_rational) { std::cout << "solving " << file_name << std::endl; - solve_mps_double(file_name, look_for_min, max_iterations, time_limit, dual, compare_with_primal, args_parser); + solve_mps_double(file_name, look_for_min, time_limit, dual, compare_with_primal, args_parser); } else { std::cout << "solving " << file_name << " in rationals " << std::endl; - solve_mps_rational(file_name, look_for_min, max_iterations, time_limit, dual, args_parser); + solve_mps_rational(file_name, look_for_min, time_limit, dual, args_parser); } } void solve_mps(std::string file_name, argument_parser & args_parser) { bool look_for_min = args_parser.option_is_used("--min"); - unsigned max_iterations, time_limit; + unsigned time_limit; bool solve_for_rational = args_parser.option_is_used("--mpq"); bool dual = args_parser.option_is_used("--dual"); bool compare_with_primal = args_parser.option_is_used("--compare_with_primal"); - get_time_limit_and_max_iters_from_parser(args_parser, time_limit, max_iterations); - solve_mps(file_name, look_for_min, max_iterations, time_limit, solve_for_rational, dual, compare_with_primal, args_parser); + get_time_limit_and_max_iters_from_parser(args_parser, time_limit); + solve_mps(file_name, look_for_min, time_limit, solve_for_rational, dual, compare_with_primal, args_parser); } void solve_mps_in_rational(std::string file_name, bool dual, argument_parser & /*args_parser*/) { @@ -1903,7 +1900,7 @@ void process_test_file(std::string test_dir, std::string test_file_name, argumen void solve_some_mps(argument_parser & args_parser) { unsigned max_iters, time_limit; - get_time_limit_and_max_iters_from_parser(args_parser, time_limit, max_iters); + get_time_limit_and_max_iters_from_parser(args_parser, time_limit); unsigned successes = 0; unsigned failures = 0; unsigned inconclusives = 0; @@ -1935,7 +1932,7 @@ void solve_some_mps(argument_parser & args_parser) { return; } if (!solve_for_rational) { - solve_mps(file_names[6], false, 0, time_limit, false, dual, compare_with_primal, args_parser); + solve_mps(file_names[6], false, time_limit, false, dual, compare_with_primal, args_parser); solve_mps_with_known_solution(file_names[3], nullptr, lp_status::INFEASIBLE, dual); // chvatal: 135(d) std::unordered_map sol; sol["X1"] = 0; @@ -1960,11 +1957,11 @@ void solve_some_mps(argument_parser & args_parser) { solve_mps_with_known_solution(file_names[4], &sol, lp_status::OPTIMAL, dual); // chvatal: 135(e) solve_mps_with_known_solution(file_names[2], nullptr, lp_status::UNBOUNDED, dual); // chvatal: 135(c) solve_mps_with_known_solution(file_names[1], nullptr, lp_status::UNBOUNDED, dual); // chvatal: 135(b) - solve_mps(file_names[8], false, 0, time_limit, false, dual, compare_with_primal, args_parser); + solve_mps(file_names[8], false, time_limit, false, dual, compare_with_primal, args_parser); // return; for (auto& s : file_names) { try { - solve_mps(s, minimums.find(s) != minimums.end(), max_iters, time_limit, false, dual, compare_with_primal, args_parser); + solve_mps(s, minimums.find(s) != minimums.end(), time_limit, false, dual, compare_with_primal, args_parser); } catch(const char *s){ std::cout<< "exception: "<< s << std::endl; @@ -2315,14 +2312,7 @@ void finalize(unsigned ret) { // return ret; } -void get_time_limit_and_max_iters_from_parser(argument_parser & args_parser, unsigned & time_limit, unsigned & max_iters) { - std::string s = args_parser.get_option_value("--max_iters"); - if (!s.empty()) { - max_iters = atoi(s.c_str()); - } else { - max_iters = 0; - } - +void get_time_limit_and_max_iters_from_parser(argument_parser & args_parser, unsigned & time_limit) { std::string time_limit_string = args_parser.get_option_value("--time_limit"); if (!time_limit_string.empty()) { time_limit = atoi(time_limit_string.c_str()); @@ -2504,7 +2494,7 @@ void process_test_file(std::string test_dir, std::string test_file_name, argumen if (args_parser.option_is_used("--lar")) test_lar_on_file(input_file_name, args_parser); else - solve_mps(input_file_name, minimize, max_iters, time_limit, use_mpq, dual, false, args_parser); + solve_mps(input_file_name, minimize, time_limit, use_mpq, dual, false, args_parser); } catch(...) { std::cout << "catching the failure" << std::endl; @@ -2624,7 +2614,7 @@ void test_files_from_directory(std::string test_file_dir, argument_parser & args vector> files = get_file_list_of_dir(test_file_dir); std::sort(files.begin(), files.end(), sort_pred()); unsigned max_iters, time_limit; - get_time_limit_and_max_iters_from_parser(args_parser, time_limit, max_iters); + get_time_limit_and_max_iters_from_parser(args_parser, time_limit); unsigned successes = 0, failures = 0, inconclusives = 0; for (auto & t : files) { process_test_file(test_file_dir, t.first, args_parser, out_dir, max_iters, time_limit, successes, failures, inconclusives); @@ -2651,10 +2641,6 @@ void run_lar_solver(argument_parser & args_parser, lar_solver * solver, mps_read solver->settings().presolve_with_double_solver_for_lar = true; } - std::string iter = args_parser.get_option_value("--max_iters"); - if (!iter.empty()) { - solver->settings().max_total_number_of_iterations = atoi(iter.c_str()); - } if (args_parser.option_is_used("--compare_with_primal")){ if (reader == nullptr) { std::cout << "cannot compare with primal, the reader is null " << std::endl; @@ -4074,14 +4060,13 @@ void test_lp_local(int argn, char**argv) { ret = 0; return finalize(ret); } - unsigned max_iters; unsigned time_limit; - get_time_limit_and_max_iters_from_parser(args_parser, time_limit, max_iters); + get_time_limit_and_max_iters_from_parser(args_parser, time_limit); bool dual = args_parser.option_is_used("--dual"); bool solve_for_rational = args_parser.option_is_used("--mpq"); std::string file_name = args_parser.get_option_value("--file"); if (!file_name.empty()) { - solve_mps(file_name, args_parser.option_is_used("--min"), max_iters, time_limit, solve_for_rational, dual, args_parser.option_is_used("--compare_with_primal"), args_parser); + solve_mps(file_name, args_parser.option_is_used("--min"), time_limit, solve_for_rational, dual, args_parser.option_is_used("--compare_with_primal"), args_parser); ret = 0; return finalize(ret); }