diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp index af972a36b..c9f6aaa40 100644 --- a/examples/c++/example.cpp +++ b/examples/c++/example.cpp @@ -294,7 +294,7 @@ void error_example() { // Error using the C API can be detected using Z3_get_error_code. // The next call fails because x is a constant. - Z3_ast arg = Z3_get_app_arg(c, x, 0); + //Z3_ast arg = Z3_get_app_arg(c, x, 0); if (Z3_get_error_code(c) != Z3_OK) { std::cout << "last call failed.\n"; } @@ -999,7 +999,6 @@ void opt_example() { opt.add(x + y <= 11); optimize::handle h1 = opt.maximize(x); optimize::handle h2 = opt.maximize(y); - check_result r = sat; while (true) { if (sat == opt.check()) { std::cout << x << ": " << opt.lower(h1) << " " << y << ": " << opt.lower(h2) << "\n"; diff --git a/examples/c/test_capi.c b/examples/c/test_capi.c index cb63fe623..11306a98b 100644 --- a/examples/c/test_capi.c +++ b/examples/c/test_capi.c @@ -2610,7 +2610,7 @@ void fpa_example() { Z3_context ctx; Z3_sort double_sort, rm_sort; Z3_symbol s_rm, s_x, s_y, s_x_plus_y; - Z3_ast rm, x, y, n, x_plus_y, c1, c2, c3, c4, c5, c6; + Z3_ast rm, x, y, n, x_plus_y, c1, c2, c3, c4, c5; Z3_ast args[2], args2[2], and_args[3], args3[3]; printf("\nFPA-example\n"); diff --git a/examples/interp/iz3.cpp b/examples/interp/iz3.cpp index 9f55c1ec6..21ea518a6 100755 --- a/examples/interp/iz3.cpp +++ b/examples/interp/iz3.cpp @@ -42,7 +42,7 @@ int main(int argc, const char **argv) { Z3_config cfg = Z3_mk_config(); // Z3_interpolation_options options = Z3_mk_interpolation_options(); - Z3_params options = 0; + // Z3_params options = 0; /* Parse the command line */ int argn = 1; @@ -104,7 +104,7 @@ int main(int argc, const char **argv) { unsigned num_theory; Z3_ast *theory; - ok = Z3_read_interpolation_problem(ctx, &num, &constraints, tree_mode ? &parents : 0, filename, &error, &num_theory, &theory); + ok = Z3_read_interpolation_problem(ctx, &num, &constraints, tree_mode ? &parents : 0, filename, &error, &num_theory, &theory) != 0; /* If parse failed, print the error message */ @@ -124,7 +124,7 @@ int main(int argc, const char **argv) { std::cout << "Splitting formula into " << nconjs << " conjuncts...\n"; num = nconjs; constraints = new Z3_ast[num]; - for(int k = 0; k < num; k++) + for(unsigned k = 0; k < num; k++) constraints[k] = Z3_get_app_arg(ctx,app,k); } } @@ -163,12 +163,12 @@ int main(int argc, const char **argv) { std::vector asserted(num); /* We start with nothing asserted. */ - for(int i = 0; i < num; i++) + for(unsigned i = 0; i < num; i++) asserted[i] = Z3_mk_true(ctx); /* Now we assert the constrints one at a time until UNSAT. */ - for(int i = 0; i < num; i++){ + for(unsigned i = 0; i < num; i++){ asserted[i] = constraints[i]; Z3_assert_cnstr(ctx,constraints[i]); // assert one constraint result = Z3_L_UNDEF; // FIXME: Z3_interpolate(ctx, num, &asserted[0], parents, options, interpolants, &model, 0, true, 0, 0); @@ -190,7 +190,7 @@ int main(int argc, const char **argv) { printf("unsat\n"); if(output_file.empty()){ printf("interpolant:\n"); - for(int i = 0; i < num-1; i++) + for(unsigned i = 0; i < num-1; i++) printf("%s\n", Z3_ast_to_string(ctx, interpolants[i])); } else { @@ -203,7 +203,7 @@ int main(int argc, const char **argv) { if(check_mode){ std::cout << "Checking interpolant...\n"; bool chk; - chk = Z3_check_interpolant(ctx,num,constraints,parents,interpolants,&error,num_theory,theory); + chk = Z3_check_interpolant(ctx,num,constraints,parents,interpolants,&error,num_theory,theory) != 0; if(chk) std::cout << "Interpolant is correct\n"; else { diff --git a/examples/maxsat/maxsat.c b/examples/maxsat/maxsat.c index f04c25e2c..8f747cb98 100644 --- a/examples/maxsat/maxsat.c +++ b/examples/maxsat/maxsat.c @@ -598,7 +598,7 @@ int smtlib_maxsat(char * file_name, int approach) Z3_context ctx; unsigned num_hard_cnstrs, num_soft_cnstrs; Z3_ast * hard_cnstrs, * soft_cnstrs; - unsigned result; + unsigned result = 0; ctx = mk_context(); Z3_parse_smtlib_file(ctx, file_name, 0, 0, 0, 0, 0, 0); hard_cnstrs = get_hard_constraints(ctx, &num_hard_cnstrs); diff --git a/examples/tptp/tptp5.cpp b/examples/tptp/tptp5.cpp index 0ed92801d..6c355a4a9 100644 --- a/examples/tptp/tptp5.cpp +++ b/examples/tptp/tptp5.cpp @@ -261,7 +261,7 @@ class env { parse(inc_name.c_str(), fmls); while (name_list) { return mk_error(name_list, "name list (not handled)"); - char const* name = name_list->child(0)->symbol(); + //char const* name = name_list->child(0)->symbol(); name_list = name_list->child(2); } } @@ -614,7 +614,7 @@ class env { void mk_mapping_sort(TreeNode* t, z3::sort_vector& domain, z3::sort& s) { char const* name = t->symbol(); - char const* id = 0; + //char const* id = 0; if (!strcmp(name,"tff_top_level_type")) { mk_mapping_sort(t->child(0), domain, s); } @@ -1832,7 +1832,7 @@ public: } z3::expr get_proof_formula(z3::expr proof) { - unsigned na = proof.num_args(); + // unsigned na = proof.num_args(); z3::expr result = proof.arg(proof.num_args()-1); std::vector vars; get_free_vars(result, vars); @@ -2119,7 +2119,7 @@ void parse_cmd_line_args(int argc, char ** argv) { int i = 1; while (i < argc) { char* arg = argv[i]; - char * eq = 0; + //char * eq = 0; char * opt_arg = 0; if (arg[0] == '-' || arg[0] == '/') { ++arg; @@ -2467,7 +2467,7 @@ static void prove_tptp() { int main(int argc, char** argv) { - std::ostream* out = &std::cout; + //std::ostream* out = &std::cout; g_start_time = static_cast(clock()); signal(SIGINT, on_ctrl_c); diff --git a/examples/tptp/tptp5.tab.c b/examples/tptp/tptp5.tab.c index c97225f4c..086f6e622 100644 --- a/examples/tptp/tptp5.tab.c +++ b/examples/tptp/tptp5.tab.c @@ -139,7 +139,7 @@ pTree pToken(char* token, int symbolIndex) { //char pTokenBuf[8240]; pTree ss; - char* symbol = tptp_lval[symbolIndex]; + //char* symbol = tptp_lval[symbolIndex]; char* safeSym = 0; //strncpy(pTokenBuf, token, 39); diff --git a/scripts/mk_unix_dist.py b/scripts/mk_unix_dist.py index a8a60ae75..a64d36bce 100644 --- a/scripts/mk_unix_dist.py +++ b/scripts/mk_unix_dist.py @@ -191,7 +191,7 @@ def mk_zip(): os.chdir(DIST_DIR) zfname = '%s.zip' % dist_path ZIPOUT = zipfile.ZipFile(zfname, 'w', zipfile.ZIP_DEFLATED) - os.path.walk(dist_path, mk_zip_visitor, '*') + os.walk(dist_path, mk_zip_visitor, '*') if is_verbose(): print("Generated '%s'" % zfname) except: diff --git a/scripts/mk_util.py b/scripts/mk_util.py index dff9051e8..e53a90127 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -90,7 +90,7 @@ FPMATH="Default" FPMATH_FLAGS="-mfpmath=sse -msse -msse2" def check_output(cmd): - return str(subprocess.Popen(cmd, stdout=subprocess.PIPE).communicate()[0]).rstrip('\r\n') + return (subprocess.Popen(cmd, stdout=subprocess.PIPE).communicate()[0]).decode("utf-8").rstrip('\r\n') def git_hash(): try: @@ -512,7 +512,7 @@ def dos2unix_tree_core(pattern, dir, files): dos2unix(fname) def dos2unix_tree(): - os.path.walk('src', dos2unix_tree_core, '*') + os.walk('src', dos2unix_tree_core, '*') def check_eol(): if not IS_WINDOWS: @@ -1578,20 +1578,22 @@ class CppExampleComponent(ExampleComponent): def mk_makefile(self, out): dll_name = get_component(Z3_DLL_COMPONENT).dll_name dll = '%s$(SO_EXT)' % dll_name + + objfiles = '' + for cppfile in self.src_files(): + objfile = '%s$(OBJ_EXT)' % (cppfile[:cppfile.rfind('.')]) + objfiles = objfiles + ('%s ' % objfile) + out.write('%s: %s\n' % (objfile, os.path.join(self.to_ex_dir, cppfile))); + out.write('\t%s $(CXXFLAGS) $(OS_DEFINES) $(EXAMP_DEBUG_FLAG) $(CXX_OUT_FLAG)%s $(LINK_FLAGS)' % (self.compiler(), objfile)) + # Add include dir components + out.write(' -I%s' % get_component(API_COMPONENT).to_src_dir) + out.write(' -I%s' % get_component(CPP_COMPONENT).to_src_dir) + out.write(' %s' % os.path.join(self.to_ex_dir, cppfile)) + out.write('\n') + exefile = '%s$(EXE_EXT)' % self.name - out.write('%s: %s' % (exefile, dll)) - for cppfile in self.src_files(): - out.write(' ') - out.write(os.path.join(self.to_ex_dir, cppfile)) - out.write('\n') - out.write('\t%s $(OS_DEFINES) $(EXAMP_DEBUG_FLAG) $(LINK_OUT_FLAG)%s $(LINK_FLAGS)' % (self.compiler(), exefile)) - # Add include dir components - out.write(' -I%s' % get_component(API_COMPONENT).to_src_dir) - out.write(' -I%s' % get_component(CPP_COMPONENT).to_src_dir) - for cppfile in self.src_files(): - out.write(' ') - out.write(os.path.join(self.to_ex_dir, cppfile)) - out.write(' ') + out.write('%s: %s %s\n' % (exefile, dll, objfiles)) + out.write('\t$(LINK) $(LINK_OUT_FLAG)%s $(LINK_FLAGS) %s ' % (exefile, objfiles)) if IS_WINDOWS: out.write('%s.lib' % dll_name) else: diff --git a/scripts/mk_win_dist.py b/scripts/mk_win_dist.py index fb42750e3..8b7e16c79 100644 --- a/scripts/mk_win_dist.py +++ b/scripts/mk_win_dist.py @@ -206,7 +206,7 @@ def mk_zip_core(x64): os.chdir(DIST_DIR) zfname = '%s.zip' % dist_path ZIPOUT = zipfile.ZipFile(zfname, 'w', zipfile.ZIP_DEFLATED) - os.path.walk(dist_path, mk_zip_visitor, '*') + os.walk(dist_path, mk_zip_visitor, '*') if is_verbose(): print("Generated '%s'" % zfname) except: @@ -245,10 +245,10 @@ def cp_vs_runtime_core(x64): else: platform = "x86" - vcdir = subprocess.check_output(['echo', '%VCINSTALLDIR%'], shell=True).rstrip('\r\n') + vcdir = os.environ['VCINSTALLDIR'] path = '%sredist\\%s' % (vcdir, platform) VS_RUNTIME_FILES = [] - os.path.walk(path, cp_vs_runtime_visitor, '*.dll') + os.walk(path, cp_vs_runtime_visitor, '*.dll') bin_dist_path = os.path.join(DIST_DIR, get_dist_path(x64), 'bin') for f in VS_RUNTIME_FILES: shutil.copy(f, bin_dist_path) diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp index fab778bb3..2c1fd7d9b 100644 --- a/src/api/api_interp.cpp +++ b/src/api/api_interp.cpp @@ -255,6 +255,14 @@ extern "C" { scoped_ptr m_solver((*sf)(mk_c(c)->m(), _p, true, true, true, ::symbol::null)); m_solver.get()->updt_params(_p); // why do we have to do this? + + // some boilerplate stolen from Z3_solver_check + unsigned timeout = to_params(p)->m_params.get_uint("timeout", mk_c(c)->get_timeout()); + unsigned rlimit = to_params(p)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit()); + bool use_ctrl_c = to_params(p)->m_params.get_bool("ctrl_c", false); + cancel_eh eh(*m_solver.get()); + api::context::set_interruptable si(*(mk_c(c)), eh); + ast *_pat = to_ast(pat); ptr_vector interp; @@ -263,14 +271,27 @@ extern "C" { ast_manager &_m = mk_c(c)->m(); model_ref m; - lbool _status = iz3interpolate(_m, - *(m_solver.get()), - _pat, - cnsts, - interp, - m, - 0 // ignore params for now - ); + lbool _status; + + { + scoped_ctrl_c ctrlc(eh, false, use_ctrl_c); + scoped_timer timer(timeout, &eh); + scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit); + try { + _status = iz3interpolate(_m, + *(m_solver.get()), + _pat, + cnsts, + interp, + m, + 0 // ignore params for now + ); + } + catch (z3_exception & ex) { + mk_c(c)->handle_exception(ex); + return Z3_L_UNDEF; + } + } for (unsigned i = 0; i < cnsts.size(); i++) _m.dec_ref(cnsts[i]); @@ -292,10 +313,12 @@ extern "C" { else { model_ref mr; m_solver.get()->get_model(mr); - Z3_model_ref *tmp_val = alloc(Z3_model_ref); - tmp_val->m_model = mr.get(); - mk_c(c)->save_object(tmp_val); - *model = of_model(tmp_val); + if(mr.get()){ + Z3_model_ref *tmp_val = alloc(Z3_model_ref); + tmp_val->m_model = mr.get(); + mk_c(c)->save_object(tmp_val); + *model = of_model(tmp_val); + } } *out_interp = of_ast_vector(v); diff --git a/src/api/dotnet/Properties/AssemblyInfo b/src/api/dotnet/Properties/AssemblyInfo index 001264e79..4afbb4a26 100644 --- a/src/api/dotnet/Properties/AssemblyInfo +++ b/src/api/dotnet/Properties/AssemblyInfo @@ -1,4 +1,4 @@ -using System; +using System; using System.Reflection; using System.Runtime.CompilerServices; using System.Runtime.InteropServices; diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 23d4e3e6c..9cf0fd9e5 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -7598,6 +7598,10 @@ def tree_interpolant(pat,p=None,ctx=None): If pat is satisfiable, raises an object of class ModelRef that represents a model of pat. + If neither a proof of unsatisfiability nor a model is obtained + (for example, because of a timeout, or because models are disabled) + then None is returned. + If parameters p are supplied, these are used in creating the solver that determines satisfiability. @@ -7623,7 +7627,9 @@ def tree_interpolant(pat,p=None,ctx=None): res = Z3_compute_interpolant(ctx.ref(),f.as_ast(),p.params,ptr,mptr) if res == Z3_L_FALSE: return AstVector(ptr[0],ctx) - raise ModelRef(mptr[0], ctx) + if mptr[0]: + raise ModelRef(mptr[0], ctx) + return None def binary_interpolant(a,b,p=None,ctx=None): """Compute an interpolant for a binary conjunction. @@ -7638,6 +7644,10 @@ def binary_interpolant(a,b,p=None,ctx=None): If a & b is satisfiable, raises an object of class ModelRef that represents a model of a &b. + If neither a proof of unsatisfiability nor a model is obtained + (for example, because of a timeout, or because models are disabled) + then None is returned. + If parameters p are supplied, these are used in creating the solver that determines satisfiability. @@ -7646,7 +7656,8 @@ def binary_interpolant(a,b,p=None,ctx=None): Not(x >= 0) """ f = And(Interpolant(a),b) - return tree_interpolant(f,p,ctx)[0] + ti = tree_interpolant(f,p,ctx) + return ti[0] if ti != None else None def sequence_interpolant(v,p=None,ctx=None): """Compute interpolant for a sequence of formulas. @@ -7664,6 +7675,10 @@ def sequence_interpolant(v,p=None,ctx=None): If a & b is satisfiable, raises an object of class ModelRef that represents a model of a & b. + If neither a proof of unsatisfiability nor a model is obtained + (for example, because of a timeout, or because models are disabled) + then None is returned. + If parameters p are supplied, these are used in creating the solver that determines satisfiability. diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index 062703be0..cc3ba81a3 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -33,7 +33,7 @@ void fpa_rewriter::updt_params(params_ref const & _p) { fpa_rewriter_params p(_p); m_hi_fp_unspecified = p.hi_fp_unspecified(); } - + void fpa_rewriter::get_param_descrs(param_descrs & r) { } @@ -72,7 +72,7 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con case OP_FPA_SQRT: SASSERT(num_args == 2); st = mk_sqrt(args[0], args[1], result); break; case OP_FPA_ROUND_TO_INTEGRAL: SASSERT(num_args == 2); st = mk_round_to_integral(args[0], args[1], result); break; - case OP_FPA_EQ: SASSERT(num_args == 2); st = mk_float_eq(args[0], args[1], result); break; + case OP_FPA_EQ: SASSERT(num_args == 2); st = mk_float_eq(args[0], args[1], result); break; case OP_FPA_LT: SASSERT(num_args == 2); st = mk_lt(args[0], args[1], result); break; case OP_FPA_GT: SASSERT(num_args == 2); st = mk_gt(args[0], args[1], result); break; case OP_FPA_LE: SASSERT(num_args == 2); st = mk_le(args[0], args[1], result); break; @@ -83,29 +83,29 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con case OP_FPA_IS_NORMAL: SASSERT(num_args == 1); st = mk_is_normal(args[0], result); break; case OP_FPA_IS_SUBNORMAL: SASSERT(num_args == 1); st = mk_is_subnormal(args[0], result); break; case OP_FPA_IS_NEGATIVE: SASSERT(num_args == 1); st = mk_is_negative(args[0], result); break; - case OP_FPA_IS_POSITIVE: SASSERT(num_args == 1); st = mk_is_positive(args[0], result); break; + case OP_FPA_IS_POSITIVE: SASSERT(num_args == 1); st = mk_is_positive(args[0], result); break; - case OP_FPA_FP: SASSERT(num_args == 3); st = mk_fp(args[0], args[1], args[2], result); break; + case OP_FPA_FP: SASSERT(num_args == 3); st = mk_fp(args[0], args[1], args[2], result); break; case OP_FPA_TO_FP: st = mk_to_fp(f, num_args, args, result); break; case OP_FPA_TO_FP_UNSIGNED: SASSERT(num_args == 2); st = mk_to_fp_unsigned(f, args[0], args[1], result); break; case OP_FPA_TO_UBV: SASSERT(num_args == 2); st = mk_to_ubv(f, args[0], args[1], result); break; case OP_FPA_TO_SBV: SASSERT(num_args == 2); st = mk_to_sbv(f, args[0], args[1], result); break; case OP_FPA_TO_IEEE_BV: SASSERT(num_args == 1); st = mk_to_ieee_bv(f, args[0], result); break; - case OP_FPA_TO_REAL: SASSERT(num_args == 1); st = mk_to_real(args[0], result); break; + case OP_FPA_TO_REAL: SASSERT(num_args == 1); st = mk_to_real(args[0], result); break; case OP_FPA_INTERNAL_MIN_I: - case OP_FPA_INTERNAL_MAX_I: - case OP_FPA_INTERNAL_MIN_UNSPECIFIED: - case OP_FPA_INTERNAL_MAX_UNSPECIFIED: + case OP_FPA_INTERNAL_MAX_I: + case OP_FPA_INTERNAL_MIN_UNSPECIFIED: + case OP_FPA_INTERNAL_MAX_UNSPECIFIED: SASSERT(num_args == 2); st = BR_FAILED; break; case OP_FPA_INTERNAL_RM: SASSERT(num_args == 1); st = mk_rm(args[0], result); break; - case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: + case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: SASSERT(num_args == 0); st = mk_to_ubv_unspecified(f, result); break; case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: SASSERT(num_args == 0); st = mk_to_sbv_unspecified(f, result); break; - case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: + case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: SASSERT(num_args == 0); st = mk_to_real_unspecified(result); break; case OP_FPA_INTERNAL_BVWRAP: @@ -113,7 +113,7 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con st = BR_FAILED; break; - default: + default: NOT_IMPLEMENTED_YET(); } return st; @@ -171,7 +171,7 @@ br_status fpa_rewriter::mk_to_real_unspecified(expr_ref & result) { else result = m_util.mk_internal_to_real_unspecified(); - return BR_DONE; + return BR_DONE; } br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { @@ -186,7 +186,7 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const unsigned ebits = f->get_parameter(0).get_int(); unsigned sbits = f->get_parameter(1).get_int(); - if (num_args == 1) { + if (num_args == 1) { if (bu.is_numeral(args[0], r1, bvs1)) { // BV -> float SASSERT(bvs1 == sbits + ebits); @@ -196,13 +196,13 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const const mpz & sm1 = m_fm.m_powers2(sbits - 1); const mpz & em1 = m_fm.m_powers2(ebits); - + scoped_mpq q(mpqm); mpqm.set(q, r1.to_mpq()); SASSERT(mpzm.is_one(q.get().denominator())); scoped_mpz z(mpzm); z = q.get().numerator(); - + mpzm.rem(z, sm1, sig); mpzm.div(z, sm1, z); @@ -214,7 +214,7 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const mpf_exp = m_fm.unbias_exp(ebits, mpf_exp); m_fm.set(v, ebits, sbits, !mpzm.is_zero(z), sig, mpf_exp); - TRACE("fp_rewriter", + TRACE("fp_rewriter", tout << "sgn: " << !mpzm.is_zero(z) << std::endl; tout << "sig: " << mpzm.to_string(sig) << std::endl; tout << "exp: " << mpf_exp << std::endl; @@ -227,9 +227,9 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const else if (num_args == 2) { if (!m_util.is_rm_numeral(args[0], rmv)) return BR_FAILED; - - if (m_util.au().is_numeral(args[1], r1)) { - // rm + real -> float + + if (m_util.au().is_numeral(args[1], r1)) { + // rm + real -> float TRACE("fp_rewriter", tout << "r: " << r1 << std::endl;); scoped_mpf v(m_fm); m_fm.set(v, ebits, sbits, rmv, r1.to_mpq()); @@ -246,7 +246,7 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const // TRACE("fp_rewriter", tout << "result: " << result << std::endl; ); return BR_DONE; } - else if (bu.is_numeral(args[1], r1, bvs1)) { + else if (bu.is_numeral(args[1], r1, bvs1)) { // rm + signed bv -> float TRACE("fp_rewriter", tout << "r1: " << r1 << std::endl;); r1 = bu.norm(r1, bvs1, true); @@ -256,7 +256,7 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const return BR_DONE; } } - else if (num_args == 3) { + else if (num_args == 3) { if (m_util.is_rm_numeral(args[0], rmv) && m_util.au().is_real(args[1]) && m_util.au().is_int(args[2])) { @@ -286,7 +286,7 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const TRACE("fp_rewriter", tout << "v = " << m_fm.to_string(v) << std::endl;); result = m_util.mk_value(v); return BR_DONE; - } + } } return BR_FAILED; @@ -296,13 +296,13 @@ br_status fpa_rewriter::mk_to_fp_unsigned(func_decl * f, expr * arg1, expr * arg SASSERT(f->get_num_parameters() == 2); SASSERT(f->get_parameter(0).is_int()); SASSERT(f->get_parameter(1).is_int()); - bv_util bu(m()); + bv_util bu(m()); unsigned ebits = f->get_parameter(0).get_int(); unsigned sbits = f->get_parameter(1).get_int(); mpf_rounding_mode rmv; rational r; unsigned bvs; - + if (m_util.is_rm_numeral(arg1, rmv) && bu.is_numeral(arg2, r, bvs)) { scoped_mpf v(m_fm); @@ -314,7 +314,7 @@ br_status fpa_rewriter::mk_to_fp_unsigned(func_decl * f, expr * arg1, expr * arg return BR_FAILED; } -br_status fpa_rewriter::mk_add(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) { +br_status fpa_rewriter::mk_add(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) { mpf_rounding_mode rm; if (m_util.is_rm_numeral(arg1, rm)) { scoped_mpf v2(m_fm), v3(m_fm); @@ -335,7 +335,7 @@ br_status fpa_rewriter::mk_sub(expr * arg1, expr * arg2, expr * arg3, expr_ref & return BR_REWRITE2; } -br_status fpa_rewriter::mk_mul(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) { +br_status fpa_rewriter::mk_mul(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) { mpf_rounding_mode rm; if (m_util.is_rm_numeral(arg1, rm)) { scoped_mpf v2(m_fm), v3(m_fm); @@ -386,7 +386,7 @@ br_status fpa_rewriter::mk_neg(expr * arg1, expr_ref & result) { result = to_app(arg1)->get_arg(0); return BR_DONE; } - + scoped_mpf v1(m_fm); if (m_util.is_numeral(arg1, v1)) { m_fm.neg(v1); @@ -414,14 +414,14 @@ br_status fpa_rewriter::mk_abs(expr * arg1, expr_ref & result) { result = arg1; return BR_DONE; } - + scoped_mpf v(m_fm); if (m_util.is_numeral(arg1, v)) { if (m_fm.is_neg(v)) m_fm.neg(v); result = m_util.mk_value(v); return BR_DONE; } - + return BR_FAILED; } @@ -434,7 +434,7 @@ br_status fpa_rewriter::mk_min(expr * arg1, expr * arg2, expr_ref & result) { result = arg1; return BR_DONE; } - + scoped_mpf v1(m_fm), v2(m_fm); if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) { if (m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1) != m_fm.sgn(v2)) { @@ -543,6 +543,7 @@ br_status fpa_rewriter::mk_round_to_integral(expr * arg1, expr * arg2, expr_ref // This the floating point theory == br_status fpa_rewriter::mk_float_eq(expr * arg1, expr * arg2, expr_ref & result) { scoped_mpf v1(m_fm), v2(m_fm); + if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) { result = (m_fm.eq(v1, v2)) ? m().mk_true() : m().mk_false(); return BR_DONE; @@ -745,22 +746,22 @@ br_status fpa_rewriter::mk_rm(expr * arg, expr_ref & result) { case BV_RM_TO_ZERO: default: result = m_util.mk_round_toward_zero(); } - + return BR_DONE; } return BR_FAILED; } -br_status fpa_rewriter::mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) { +br_status fpa_rewriter::mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) { unsynch_mpz_manager & mpzm = m_fm.mpz_manager(); bv_util bu(m()); rational r1, r2, r3; - unsigned bvs1, bvs2, bvs3; + unsigned bvs1, bvs2, bvs3; - if (bu.is_numeral(arg1, r1, bvs1) && - bu.is_numeral(arg2, r2, bvs2) && - bu.is_numeral(arg3, r3, bvs3)) { + if (bu.is_numeral(arg1, r1, bvs1) && + bu.is_numeral(arg2, r2, bvs2) && + bu.is_numeral(arg3, r3, bvs3)) { SASSERT(mpzm.is_one(r2.to_mpq().denominator())); SASSERT(mpzm.is_one(r3.to_mpq().denominator())); SASSERT(mpzm.is_int64(r3.to_mpq().numerator())); @@ -769,7 +770,7 @@ br_status fpa_rewriter::mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref & m_fm.set(v, bvs2, bvs3 + 1, r1.is_one(), r3.to_mpq().numerator(), - m_fm.unbias_exp(bvs2, biased_exp)); + m_fm.unbias_exp(bvs2, biased_exp)); TRACE("fp_rewriter", tout << "simplified (fp ...) to " << m_fm.to_string(v) << std::endl;); result = m_util.mk_value(v); return BR_DONE; @@ -780,24 +781,24 @@ br_status fpa_rewriter::mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref & br_status fpa_rewriter::mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_ref & result) { SASSERT(f->get_num_parameters() == 1); - SASSERT(f->get_parameter(0).is_int()); + SASSERT(f->get_parameter(0).is_int()); int bv_sz = f->get_parameter(0).get_int(); mpf_rounding_mode rmv; scoped_mpf v(m_fm); if (m_util.is_rm_numeral(arg1, rmv) && - m_util.is_numeral(arg2, v)) { + m_util.is_numeral(arg2, v)) { if (m_fm.is_nan(v) || m_fm.is_inf(v) || m_fm.is_neg(v)) { mk_to_ubv_unspecified(f, result); return BR_REWRITE_FULL; - } + } bv_util bu(m()); - scoped_mpq q(m_fm.mpq_manager()); + scoped_mpq q(m_fm.mpq_manager()); m_fm.to_sbv_mpq(rmv, v, q); - - rational r(q); + + rational r(q); rational ul, ll; ul = m_fm.m_powers2.m1(bv_sz); ll = rational(0); @@ -813,7 +814,7 @@ br_status fpa_rewriter::mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_ br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_ref & result) { SASSERT(f->get_num_parameters() == 1); - SASSERT(f->get_parameter(0).is_int()); + SASSERT(f->get_parameter(0).is_int()); int bv_sz = f->get_parameter(0).get_int(); mpf_rounding_mode rmv; scoped_mpf v(m_fm); @@ -829,8 +830,8 @@ br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_ bv_util bu(m()); scoped_mpq q(m_fm.mpq_manager()); m_fm.to_sbv_mpq(rmv, v, q); - - rational r(q); + + rational r(q); rational ul, ll; ul = m_fm.m_powers2.m1(bv_sz - 1); ll = - m_fm.m_powers2(bv_sz - 1); @@ -853,7 +854,7 @@ br_status fpa_rewriter::mk_to_ieee_bv(func_decl * f, expr * arg, expr_ref & resu mk_to_ieee_bv_unspecified(f, result); return BR_REWRITE_FULL; } - + bv_util bu(m()); scoped_mpz rz(m_fm.mpq_manager()); m_fm.to_ieee_bv_mpz(v, rz); @@ -866,7 +867,7 @@ br_status fpa_rewriter::mk_to_ieee_bv(func_decl * f, expr * arg, expr_ref & resu br_status fpa_rewriter::mk_to_real(expr * arg, expr_ref & result) { scoped_mpf v(m_fm); - + if (m_util.is_numeral(arg, v)) { if (m_fm.is_nan(v) || m_fm.is_inf(v)) { result = m_util.mk_internal_to_real_unspecified(); diff --git a/src/ast/rewriter/fpa_rewriter.h b/src/ast/rewriter/fpa_rewriter.h index 689ffad3c..43d138cad 100644 --- a/src/ast/rewriter/fpa_rewriter.h +++ b/src/ast/rewriter/fpa_rewriter.h @@ -39,13 +39,13 @@ public: ast_manager & m() const { return m_util.m(); } family_id get_fid() const { return m_util.get_fid(); } - + void updt_params(params_ref const & p); static void get_param_descrs(param_descrs & r); br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); br_status mk_eq_core(expr * arg1, expr * arg2, expr_ref & result); - + br_status mk_add(expr * arg1, expr * arg2, expr * arg3, expr_ref & result); br_status mk_sub(expr * arg1, expr * arg2, expr * arg3, expr_ref & result); br_status mk_mul(expr * arg1, expr * arg2, expr * arg3, expr_ref & result); @@ -77,7 +77,7 @@ public: br_status mk_to_fp(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); br_status mk_to_fp_unsigned(func_decl * f, expr * arg1, expr * arg2, expr_ref & result); - + br_status mk_rm(expr * arg, expr_ref & result); br_status mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref & result); br_status mk_to_fp_unsigned(expr * arg1, expr * arg2, expr_ref & result); diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 701efb2ba..7b8a83520 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -29,7 +29,7 @@ namespace smt { obj_map & m_conversions; expr * m_e; public: - fpa2bv_conversion_trail_elem(ast_manager & m, obj_map & c, expr * e) : + fpa2bv_conversion_trail_elem(ast_manager & m, obj_map & c, expr * e) : m(m), m_conversions(c), m_e(e) {} virtual ~fpa2bv_conversion_trail_elem() {} virtual void undo(theory_fpa & th) { @@ -63,7 +63,7 @@ namespace smt { m.inc_ref(f); m.inc_ref(result); } - } + } void theory_fpa::fpa2bv_converter_wrapped::mk_rm_const(func_decl * f, expr_ref & result) { SASSERT(f->get_family_id() == null_family_id); @@ -89,12 +89,12 @@ namespace smt { } expr_ref theory_fpa::fpa2bv_converter_wrapped::mk_min_unspecified(func_decl * f, expr * x, expr * y) { - // The only cases in which min is unspecified for is when the arguments are +0.0 and -0.0. + // The only cases in which min is unspecified for is when the arguments are +0.0 and -0.0. unsigned ebits = m_util.get_ebits(f->get_range()); unsigned sbits = m_util.get_sbits(f->get_range()); unsigned bv_sz = ebits + sbits; expr_ref res(m); - + expr * args[] = { x, y }; func_decl * w = m.mk_func_decl(m_th.get_family_id(), OP_FPA_INTERNAL_MIN_UNSPECIFIED, 0, 0, 2, args, f->get_range()); expr_ref a(m), wrapped(m); @@ -110,7 +110,7 @@ namespace smt { m_extra_assertions.push_back(sc); return res; } - + expr_ref theory_fpa::fpa2bv_converter_wrapped::mk_max_unspecified(func_decl * f, expr * x, expr * y) { // The only cases in which max is unspecified for is when the arguments are +0.0 and -0.0. unsigned ebits = m_util.get_ebits(f->get_range()); @@ -118,7 +118,7 @@ namespace smt { unsigned bv_sz = ebits + sbits; expr_ref res(m); - expr * args[] = { x, y }; + expr * args[] = { x, y }; func_decl * w = m.mk_func_decl(m_th.get_family_id(), OP_FPA_INTERNAL_MAX_UNSPECIFIED, 0, 0, 2, args, f->get_range()); expr_ref a(m), wrapped(m); a = m.mk_app(w, x, y); @@ -154,15 +154,15 @@ namespace smt { ast_manager & m = get_manager(); dec_ref_map_values(m, m_conversions); dec_ref_map_values(m, m_wraps); - dec_ref_map_values(m, m_unwraps); + dec_ref_map_values(m, m_unwraps); } app * theory_fpa::fpa_value_proc::mk_value(model_generator & mg, ptr_vector & values) { - ast_manager & m = m_th.get_manager(); + ast_manager & m = m_th.get_manager(); TRACE("t_fpa_detail", for (unsigned i = 0; i < values.size(); i++) tout << "value[" << i << "] = " << mk_ismt2_pp(values[i], m) << std::endl;); - + mpf_manager & mpfm = m_fu.fm(); unsynch_mpz_manager & mpzm = mpfm.mpz_manager(); app * result; @@ -195,7 +195,7 @@ namespace smt { mpzm.set(sig_z, all_z); } - else if (values.size() == 3) { + else if (values.size() == 3) { rational sgn_r(0), exp_r(0), sig_r(0); bool r = m_bu.is_numeral(values[0], sgn_r, bv_sz); @@ -204,7 +204,7 @@ namespace smt { SASSERT(r && bv_sz == m_ebits); r = m_bu.is_numeral(values[2], sig_r, bv_sz); SASSERT(r && bv_sz == m_sbits - 1); - + SASSERT(mpzm.is_one(sgn_r.to_mpq().denominator())); SASSERT(mpzm.is_one(exp_r.to_mpq().denominator())); SASSERT(mpzm.is_one(sig_r.to_mpq().denominator())); @@ -228,25 +228,25 @@ namespace smt { mpzm.to_string(exp_z) << "," << mpzm.to_string(sig_z) << "] --> " << mk_ismt2_pp(result, m_th.get_manager()) << "\n";); - + return result; } app * theory_fpa::fpa_rm_value_proc::mk_value(model_generator & mg, ptr_vector & values) { SASSERT(values.size() == 1); ast_manager & m = m_th.get_manager(); - + TRACE("t_fpa_detail", for (unsigned i = 0; i < values.size(); i++) tout << "value[" << i << "] = " << mk_ismt2_pp(values[i], m) << std::endl;); - app * result = 0; + app * result = 0; unsigned bv_sz; rational val(0); bool r = m_bu.is_numeral(values[0], val, bv_sz); SASSERT(r); SASSERT(bv_sz == 3); - + switch (val.get_uint64()) { case BV_RM_TIES_TO_AWAY: result = m_fu.mk_round_nearest_ties_to_away(); break; @@ -257,7 +257,7 @@ namespace smt { default: result = m_fu.mk_round_toward_zero(); } - TRACE("t_fpa", tout << "fpa_rm_value_proc::mk_value result: " << + TRACE("t_fpa", tout << "fpa_rm_value_proc::mk_value result: " << mk_ismt2_pp(result, m_th.get_manager()) << "\n";); return result; @@ -272,7 +272,7 @@ namespace smt { if (!m_wraps.find(e_srt, w)) { SASSERT(!m_wraps.contains(e_srt)); - + sort * bv_srt; if (m_converter.is_rm(e_srt)) bv_srt = m_bv_util.mk_sort(3); @@ -280,9 +280,9 @@ namespace smt { SASSERT(m_converter.is_float(e_srt)); unsigned ebits = m_fpa_util.get_ebits(e_srt); unsigned sbits = m_fpa_util.get_sbits(e_srt); - bv_srt = m_bv_util.mk_sort(ebits + sbits); + bv_srt = m_bv_util.mk_sort(ebits + sbits); } - + w = m.mk_func_decl(get_family_id(), OP_FPA_INTERNAL_BVWRAP, 0, 0, 1, &e_srt, bv_srt); m_wraps.insert(e_srt, w); m.inc_ref(w); @@ -295,7 +295,7 @@ namespace smt { app_ref theory_fpa::unwrap(expr * e, sort * s) { SASSERT(!m_fpa_util.is_unwrap(e)); - ast_manager & m = get_manager(); + ast_manager & m = get_manager(); sort * bv_srt = m.get_sort(e); func_decl *u; @@ -311,7 +311,7 @@ namespace smt { res = m.mk_app(u, e); return res; } - + expr_ref theory_fpa::convert_atom(expr * e) { ast_manager & m = get_manager(); TRACE("t_fpa_detail", tout << "converting atom: " << mk_ismt2_pp(e, get_manager()) << "\n";); @@ -320,7 +320,7 @@ namespace smt { m_rw(e, res); m_th_rw(res, res); SASSERT(is_app(res)); - SASSERT(m.is_bool(res)); + SASSERT(m.is_bool(res)); return res; } @@ -331,12 +331,12 @@ namespace smt { expr_ref e_conv(m), res(m); proof_ref pr(m); m_rw(e, e_conv); - - if (is_app(e_conv) && to_app(e_conv)->get_family_id() != get_family_id()) { + + if (is_app(e_conv) && to_app(e_conv)->get_family_id() != get_family_id()) { if (!m_fpa_util.is_float(e_conv)) m_th_rw(e_conv, res); else { - expr_ref bv(m); + expr_ref bv(m); bv = wrap(e_conv); unsigned bv_sz = m_bv_util.get_bv_size(bv); unsigned ebits = m_fpa_util.get_ebits(m.get_sort(e_conv)); @@ -365,7 +365,7 @@ namespace smt { m_converter.mk_fp(sgn, exp, sig, res); } else - UNREACHABLE(); + UNREACHABLE(); SASSERT(res.get() != 0); return res; @@ -426,7 +426,7 @@ namespace smt { expr_ref theory_fpa::convert_conversion_term(expr * e) { /* This is for the conversion functions fp.to_* */ - ast_manager & m = get_manager(); + ast_manager & m = get_manager(); expr_ref res(m); proof_ref pr(m); @@ -480,7 +480,7 @@ namespace smt { else if (m_fpa_util.is_float(e) || m_fpa_util.is_rm(e)) res = convert_term(e); else if (m_arith_util.is_real(e) || m_bv_util.is_bv(e)) - res = convert_conversion_term(e); + res = convert_conversion_term(e); else UNREACHABLE(); @@ -492,7 +492,7 @@ namespace smt { m.inc_ref(res); m_trail_stack.push(fpa2bv_conversion_trail_elem(m, m_conversions, e)); } - + return res; } @@ -501,7 +501,7 @@ namespace smt { ast_manager & m = get_manager(); context & ctx = get_context(); simplifier & simp = ctx.get_simplifier(); - + expr_ref res(m), t(m); proof_ref t_pr(m); res = m.mk_true(); @@ -515,21 +515,21 @@ namespace smt { m_converter.m_extra_assertions.reset(); m_th_rw(res); - + CTRACE("t_fpa", !m.is_true(res), tout << "side condition: " << mk_ismt2_pp(res, m) << "\n";); return res; } void theory_fpa::assert_cnstr(expr * e) { if (get_manager().is_true(e)) return; - TRACE("t_fpa_detail", tout << "asserting " << mk_ismt2_pp(e, get_manager()) << "\n";); + TRACE("t_fpa_detail", tout << "asserting " << mk_ismt2_pp(e, get_manager()) << "\n";); context & ctx = get_context(); ctx.internalize(e, false); literal lit(ctx.get_literal(e)); ctx.mark_as_relevant(lit); - ctx.mk_th_axiom(get_id(), 1, &lit); + ctx.mk_th_axiom(get_id(), 1, &lit); TRACE("t_fpa_detail", tout << "done asserting " << mk_ismt2_pp(e, get_manager()) << "\n";); - } + } void theory_fpa::attach_new_th_var(enode * n) { context & ctx = get_context(); @@ -556,10 +556,10 @@ namespace smt { ctx.set_var_theory(l.var(), get_id()); expr_ref bv_atom(m); - bv_atom = convert_atom(atom); + bv_atom = convert_atom(atom); SASSERT(is_app(bv_atom) && m.is_bool(bv_atom)); bv_atom = m.mk_and(bv_atom, mk_side_conditions()); - + assert_cnstr(m.mk_iff(atom, bv_atom)); return true; } @@ -569,29 +569,29 @@ namespace smt { context & ctx = get_context(); TRACE("t_fpa", tout << "internalizing term: " << mk_ismt2_pp(term, get_manager()) << "\n";); SASSERT(term->get_family_id() == get_family_id()); - SASSERT(!ctx.e_internalized(term)); + SASSERT(!ctx.e_internalized(term)); unsigned num_args = term->get_num_args(); for (unsigned i = 0; i < num_args; i++) ctx.internalize(term->get_arg(i), false); - + enode * e = (ctx.e_internalized(term)) ? ctx.get_enode(term) : ctx.mk_enode(term, false, false, true); - + if (is_attached_to_var(e)) return false; attach_new_th_var(e); // The conversion operators fp.to_* appear in non-FP constraints. - // The corresponding constraints will not be translated and added + // The corresponding constraints will not be translated and added // via convert(...) and assert_cnstr(...) in initialize_atom(...). // Therefore, we translate and assert them here. fpa_op_kind k = (fpa_op_kind)term->get_decl_kind(); switch (k) { case OP_FPA_TO_UBV: case OP_FPA_TO_SBV: - case OP_FPA_TO_REAL: + case OP_FPA_TO_REAL: case OP_FPA_TO_IEEE_BV: { expr_ref conv(m); conv = convert(term); @@ -599,32 +599,32 @@ namespace smt { assert_cnstr(mk_side_conditions()); break; } - default: /* ignore */; + default: /* ignore */; } return true; - } + } void theory_fpa::apply_sort_cnstr(enode * n, sort * s) { TRACE("t_fpa", tout << "apply sort cnstr for: " << mk_ismt2_pp(n->get_owner(), get_manager()) << "\n";); SASSERT(s->get_family_id() == get_family_id()); - + ast_manager & m = get_manager(); context & ctx = get_context(); - + app_ref owner(m); owner = n->get_owner(); - + SASSERT(owner->get_decl()->get_range() == s); - if ((m_fpa_util.is_float(s) || m_fpa_util.is_rm(s)) && + if ((m_fpa_util.is_float(s) || m_fpa_util.is_rm(s)) && !is_attached_to_var(n)) { - - attach_new_th_var(n); + + attach_new_th_var(n); if (m_fpa_util.is_rm(s)) { // For every RM term, we need to make sure that it's - // associated bit-vector is within the valid range. + // associated bit-vector is within the valid range. if (!m_fpa_util.is_unwrap(owner)) { expr_ref valid(m), limit(m); limit = m_bv_util.mk_numeral(4, 3); @@ -638,7 +638,7 @@ namespace smt { } } - void theory_fpa::new_eq_eh(theory_var x, theory_var y) { + void theory_fpa::new_eq_eh(theory_var x, theory_var y) { ast_manager & m = get_manager(); enode * e_x = get_enode(x); enode * e_y = get_enode(y); @@ -646,7 +646,7 @@ namespace smt { TRACE("t_fpa", tout << "new eq: " << x << " = " << y << std::endl;); TRACE("t_fpa_detail", tout << mk_ismt2_pp(e_x->get_owner(), m) << " = " << mk_ismt2_pp(e_y->get_owner(), m) << std::endl;); - + fpa_util & fu = m_fpa_util; expr_ref xe(m), ye(m); @@ -664,13 +664,13 @@ namespace smt { "yc = " << mk_ismt2_pp(yc, m) << std::endl;); expr_ref c(m); - + if ((fu.is_float(xe) && fu.is_float(ye)) || (fu.is_rm(xe) && fu.is_rm(ye))) m_converter.mk_eq(xc, yc, c); - else + else c = m.mk_eq(xc, yc); - + m_th_rw(c); assert_cnstr(m.mk_iff(m.mk_eq(xe, ye), c)); assert_cnstr(mk_side_conditions()); @@ -722,33 +722,33 @@ namespace smt { m_trail_stack.push_scope(); } - void theory_fpa::pop_scope_eh(unsigned num_scopes) { + void theory_fpa::pop_scope_eh(unsigned num_scopes) { m_trail_stack.pop_scope(num_scopes); TRACE("t_fpa", tout << "pop " << num_scopes << "; now " << m_trail_stack.get_num_scopes() << "\n";); - // unsigned num_old_vars = get_old_num_vars(num_scopes); + // unsigned num_old_vars = get_old_num_vars(num_scopes); theory::pop_scope_eh(num_scopes); - } + } void theory_fpa::assign_eh(bool_var v, bool is_true) { ast_manager & m = get_manager(); context & ctx = get_context(); expr * e = ctx.bool_var2expr(v); - + TRACE("t_fpa", tout << "assign_eh for: " << v << " (" << is_true << "):\n" << mk_ismt2_pp(e, m) << "\n";); - + expr_ref converted(m); converted = m.mk_and(convert(e), mk_side_conditions()); if (is_true) assert_cnstr(m.mk_implies(e, converted)); - else - assert_cnstr(m.mk_implies(m.mk_not(e), m.mk_not(converted))); + else + assert_cnstr(m.mk_implies(m.mk_not(e), m.mk_not(converted))); } void theory_fpa::relevant_eh(app * n) { ast_manager & m = get_manager(); TRACE("t_fpa", tout << "relevant_eh for: " << mk_ismt2_pp(n, m) << "\n";); - mpf_manager & mpfm = m_fpa_util.fm(); + mpf_manager & mpfm = m_fpa_util.fm(); if (m_fpa_util.is_float(n) || m_fpa_util.is_rm(n)) { if (!m_fpa_util.is_unwrap(n)) { @@ -757,7 +757,7 @@ namespace smt { mpf_rounding_mode rm; scoped_mpf val(mpfm); if (m_fpa_util.is_rm_numeral(n, rm)) { - c = m.mk_eq(wrapped, m_bv_util.mk_numeral(rm, 3)); + c = m.mk_eq(wrapped, m_bv_util.mk_numeral(rm, 3)); assert_cnstr(c); } else if (m_fpa_util.is_numeral(n, val)) { @@ -772,7 +772,7 @@ namespace smt { assert_cnstr(c); } else { - c = m.mk_eq(unwrap(wrapped, m.get_sort(n)), n); + c = m.mk_eq(unwrap(wrapped, m.get_sort(n)), n); assert_cnstr(c); } } @@ -803,7 +803,7 @@ namespace smt { final_check_status theory_fpa::final_check_eh() { TRACE("t_fpa", tout << "final_check_eh\n";); SASSERT(m_converter.m_extra_assertions.empty()); - return FC_DONE; + return FC_DONE; } void theory_fpa::init_model(model_generator & mg) { @@ -813,7 +813,7 @@ namespace smt { } model_value_proc * theory_fpa::mk_value(enode * n, model_generator & mg) { - TRACE("t_fpa", tout << "mk_value for: " << mk_ismt2_pp(n->get_owner(), get_manager()) << + TRACE("t_fpa", tout << "mk_value for: " << mk_ismt2_pp(n->get_owner(), get_manager()) << " (sort " << mk_ismt2_pp(get_manager().get_sort(n->get_owner()), get_manager()) << ")\n";); ast_manager & m = get_manager(); @@ -821,14 +821,14 @@ namespace smt { app_ref owner(m); owner = n->get_owner(); - // If the owner is not internalized, it doesn't have an enode associated. + // If the owner is not internalized, it doesn't have an enode associated. SASSERT(ctx.e_internalized(owner)); - + if (m_fpa_util.is_rm_numeral(owner) || m_fpa_util.is_numeral(owner)) { return alloc(expr_wrapper_proc, owner); } - + model_value_proc * res = 0; app_ref wrapped(m); @@ -849,7 +849,7 @@ namespace smt { a2 = to_app(owner->get_arg(2)); unsigned ebits = m_fpa_util.get_ebits(m.get_sort(owner)); unsigned sbits = m_fpa_util.get_sbits(m.get_sort(owner)); - fpa_value_proc * vp = alloc(fpa_value_proc, this, ebits, sbits); + fpa_value_proc * vp = alloc(fpa_value_proc, this, ebits, sbits); vp->add_dependency(ctx.get_enode(a0)); vp->add_dependency(ctx.get_enode(a1)); vp->add_dependency(ctx.get_enode(a2)); @@ -891,8 +891,8 @@ namespace smt { { ast_manager & m = get_manager(); context & ctx = get_context(); - - out << "fpa theory variables:" << std::endl; + + out << "fpa theory variables:" << std::endl; ptr_vector::const_iterator it = ctx.begin_enodes(); ptr_vector::const_iterator end = ctx.end_enodes(); for (; it != end; it++) { @@ -907,7 +907,7 @@ namespace smt { for (; it != end; it++) { theory_var v = (*it)->get_th_var(m_bv_util.get_family_id()); if (v != -1) out << v << " -> " << - mk_ismt2_pp((*it)->get_owner(), m) << std::endl; + mk_ismt2_pp((*it)->get_owner(), m) << std::endl; } out << "arith theory variables:" << std::endl; diff --git a/src/smt/theory_fpa.h b/src/smt/theory_fpa.h index 29bc71bde..990701c4a 100644 --- a/src/smt/theory_fpa.h +++ b/src/smt/theory_fpa.h @@ -84,13 +84,13 @@ namespace smt { virtual void mk_const(func_decl * f, expr_ref & result); virtual void mk_rm_const(func_decl * f, expr_ref & result); virtual void mk_uninterpreted_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - + virtual expr_ref mk_min_unspecified(func_decl * f, expr * x, expr * y); virtual expr_ref mk_max_unspecified(func_decl * f, expr * x, expr * y); }; - + class fpa_value_proc : public model_value_proc { - protected: + protected: theory_fpa & m_th; ast_manager & m; fpa_util & m_fu; @@ -100,10 +100,10 @@ namespace smt { unsigned m_sbits; public: - fpa_value_proc(theory_fpa * th, unsigned ebits, unsigned sbits) : + fpa_value_proc(theory_fpa * th, unsigned ebits, unsigned sbits) : m_th(*th), m(th->get_manager()), m_fu(th->m_fpa_util), m_bu(th->m_bv_util), m_ebits(ebits), m_sbits(sbits) {} - + virtual ~fpa_value_proc() {} void add_dependency(enode * e) { m_deps.push_back(model_value_dependency(e)); } @@ -123,7 +123,7 @@ namespace smt { buffer m_deps; public: - fpa_rm_value_proc(theory_fpa * th) : + fpa_rm_value_proc(theory_fpa * th) : m_th(*th), m(th->get_manager()), m_fu(th->m_fpa_util), m_bu(th->m_bv_util) {} void add_dependency(enode * e) { m_deps.push_back(model_value_dependency(e)); } @@ -135,7 +135,7 @@ namespace smt { virtual ~fpa_rm_value_proc() {} virtual app * mk_value(model_generator & mg, ptr_vector & values); }; - + protected: fpa2bv_converter_wrapped m_converter; fpa2bv_rewriter m_rw; @@ -159,10 +159,10 @@ namespace smt { virtual void pop_scope_eh(unsigned num_scopes); virtual void reset_eh(); virtual theory* mk_fresh(context*) { return alloc(theory_fpa, get_manager()); } - virtual char const * get_name() const { return "fpa"; } + virtual char const * get_name() const { return "fpa"; } virtual model_value_proc * mk_value(enode * n, model_generator & mg); - + void assign_eh(bool_var v, bool is_true); virtual void relevant_eh(app * n); virtual void init_model(model_generator & m); @@ -181,14 +181,14 @@ namespace smt { expr_ref convert_term(expr * e); expr_ref convert_conversion_term(expr * e); expr_ref convert_unwrap(expr * e); - + void add_trail(ast * a); void attach_new_th_var(enode * n); void assert_cnstr(expr * e); app_ref wrap(expr * e); - app_ref unwrap(expr * e, sort * s); + app_ref unwrap(expr * e, sort * s); }; };