diff --git a/ml/compile_mlapi.cmd b/ml/compile_mlapi.cmd index 02a2f2745..db80521dc 100644 --- a/ml/compile_mlapi.cmd +++ b/ml/compile_mlapi.cmd @@ -22,7 +22,7 @@ if %STATIC% == true ( set Z3DBGLIB=z3lib.lib ) else ( set Z3LIB=z3.lib - set Z3DBGLIB=z3_dbg.lib + set Z3DBGLIB=z3.lib ) REM ocaml 3.11 and later calls the linker through flexlink diff --git a/src/api_headers/z3_api.h b/src/api_headers/z3_api.h index 29806e02e..70518b54c 100644 --- a/src/api_headers/z3_api.h +++ b/src/api_headers/z3_api.h @@ -1159,7 +1159,7 @@ typedef enum #endif -/* +/** Definitions for update_api.py def_Type('CONFIG', 'Z3_config', 'Config') @@ -3970,12 +3970,12 @@ END_MLAPI_EXCLUDE */ Z3_ast_kind Z3_API Z3_get_ast_kind(__in Z3_context c, __in Z3_ast a); - /* + /** def_API('Z3_is_app', BOOL, (_in(CONTEXT), _in(AST))) */ Z3_bool Z3_API Z3_is_app(__in Z3_context c, __in Z3_ast a); - /* + /** def_API('Z3_is_numeral_ast', BOOL, (_in(CONTEXT), _in(AST))) */ Z3_bool Z3_API Z3_is_numeral_ast(__in Z3_context c, __in Z3_ast a); @@ -4757,17 +4757,17 @@ END_MLAPI_EXCLUDE */ Z3_string Z3_API Z3_ast_to_string(__in Z3_context c, __in Z3_ast a); - /* + /** def_API('Z3_pattern_to_string', STRING, (_in(CONTEXT), _in(PATTERN))) */ Z3_string Z3_API Z3_pattern_to_string(__in Z3_context c, __in Z3_pattern p); - /* + /** def_API('Z3_sort_to_string', STRING, (_in(CONTEXT), _in(SORT))) */ Z3_string Z3_API Z3_sort_to_string(__in Z3_context c, __in Z3_sort s); - /* + /** def_API('Z3_func_decl_to_string', STRING, (_in(CONTEXT), _in(FUNC_DECL))) */ Z3_string Z3_API Z3_func_decl_to_string(__in Z3_context c, __in Z3_func_decl d); diff --git a/src/muz_qe/dl_util.h b/src/muz_qe/dl_util.h index 3e01fb8d2..1969da1a9 100644 --- a/src/muz_qe/dl_util.h +++ b/src/muz_qe/dl_util.h @@ -171,19 +171,32 @@ namespace datalog { */ void display_fact(context & ctx, app * f, std::ostream & out); - class scoped_coarse_proof { - ast_manager& m; + class scoped_proof_mode { + ast_manager& m; proof_gen_mode m_mode; public: - scoped_coarse_proof(ast_manager& m): m(m) { + scoped_proof_mode(ast_manager& m, proof_gen_mode mode): m(m) { m_mode = m.proof_mode(); - m.toggle_proof_mode(PGM_COARSE); + m.toggle_proof_mode(mode); } - ~scoped_coarse_proof() { + ~scoped_proof_mode() { m.toggle_proof_mode(m_mode); } + }; + class scoped_coarse_proof : public scoped_proof_mode { + public: + scoped_coarse_proof(ast_manager& m): scoped_proof_mode(m, PGM_COARSE) {} + }; + + class scoped_no_proof : public scoped_proof_mode { + public: + scoped_no_proof(ast_manager& m): scoped_proof_mode(m, PGM_DISABLED) {} + }; + + + class variable_intersection { bool values_match(const expr * v1, const expr * v2); diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp index aa9b37344..b9ae51859 100644 --- a/src/muz_qe/pdr_context.cpp +++ b/src/muz_qe/pdr_context.cpp @@ -1618,24 +1618,16 @@ namespace pdr { - T(x0,x1,x) for transition - phi(x) for n.state() - - psi(x0,x1,x) for psi - M(x0,x1,x) for n.model() Assumptions: - M => psi - psi => phi & T - psi & M agree on which rules are taken. + M => phi & T In other words, - 1. psi is a weakening of M - 2. phi & T is implied by psi + 1. phi & T is implied by M Goal is to find phi0(x0), phi1(x1) such that: - phi(x) & phi0(x0) & phi1(x1) => psi(x0, x1, x) - - or at least (ignoring psi alltogether): - phi(x) & phi0(x0) & phi1(x1) => T(x0, x1, x) Strategy: diff --git a/src/muz_qe/pdr_farkas_learner.cpp b/src/muz_qe/pdr_farkas_learner.cpp index 9dbe91d0b..6494bd223 100644 --- a/src/muz_qe/pdr_farkas_learner.cpp +++ b/src/muz_qe/pdr_farkas_learner.cpp @@ -29,6 +29,7 @@ Revision History: #include "pdr_util.h" #include "pdr_farkas_learner.h" #include "th_rewriter.h" +#include "smtparser.h" #include "pdr_interpolant_provider.h" #include "ast_ll_pp.h" #include "arith_bounds_tactic.h" @@ -857,7 +858,6 @@ namespace pdr { void farkas_learner::test(char const* filename) { -#if 0 if (!filename) { test(); return; @@ -886,7 +886,6 @@ namespace pdr { expr_ref_vector lemmas(m); bool res = fl.get_lemma_guesses(A, B, lemmas); std::cout << "lemmas: " << pp_cube(lemmas, m) << "\n"; -#endif } }; diff --git a/src/muz_qe/pdr_util.cpp b/src/muz_qe/pdr_util.cpp index c09f1a246..1ec358fe1 100644 --- a/src/muz_qe/pdr_util.cpp +++ b/src/muz_qe/pdr_util.cpp @@ -911,22 +911,9 @@ bool model_evaluator::check_model(ptr_vector const& formulas) { template class rewriter_tpl; - class scoped_no_proof { - ast_manager& m; - proof_gen_mode m_mode; - public: - scoped_no_proof(ast_manager& m): m(m) { - m_mode = m.proof_mode(); - m.toggle_proof_mode(PGM_DISABLED); - } - ~scoped_no_proof() { - m.toggle_proof_mode(m_mode); - } - }; - void hoist_non_bool_if(expr_ref& fml) { ast_manager& m = fml.get_manager(); - scoped_no_proof _sp(m); + datalog::scoped_no_proof _sp(m); params_ref p; ite_hoister_star ite_rw(m, p); expr_ref tmp(m); @@ -951,7 +938,7 @@ bool model_evaluator::check_model(ptr_vector const& formulas) { } bool test_ineq(expr* e) const { - SASSERT(a.is_le(e) || a.is_ge(e)); + SASSERT(a.is_le(e) || a.is_ge(e) || m.is_eq(e)); SASSERT(to_app(e)->get_num_args() == 2); expr * lhs = to_app(e)->get_arg(0); expr * rhs = to_app(e)->get_arg(1); @@ -985,6 +972,9 @@ bool model_evaluator::check_model(ptr_vector const& formulas) { if (!a.is_int_real(lhs)) { return true; } + if (a.is_numeral(lhs) || a.is_numeral(rhs)) { + return test_ineq(e); + } return test_term(lhs) && test_term(rhs); }