mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 09:55:19 +00:00
Code Activity

Added branch into QF_NRA from QF_FP problems containing to_real terms.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-05-29 14:21:27 +01:00
parent 9428acd578
commit 85419ca503
2 changed files with 8 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
scripts/mk_project.py
View file

@ -55,7 +55,6 @@ def init_project_def():
add_lib('bv_tactics', ['tactic', 'bit_blaster'], 'tactic/bv') add_lib('bv_tactics', ['tactic', 'bit_blaster'], 'tactic/bv')
add_lib('fuzzing', ['ast'], 'test/fuzzing') add_lib('fuzzing', ['ast'], 'test/fuzzing')
add_lib('smt_tactic', ['smt'], 'smt/tactic') add_lib('smt_tactic', ['smt'], 'smt/tactic')
add_lib('fpa_tactics', ['fpa', 'core_tactics', 'bv_tactics', 'sat_tactic', 'smt_tactic'], 'tactic/fpa')
add_lib('sls_tactic', ['tactic', 'normal_forms', 'core_tactics', 'bv_tactics'], 'tactic/sls') add_lib('sls_tactic', ['tactic', 'normal_forms', 'core_tactics', 'bv_tactics'], 'tactic/sls')
add_lib('qe', ['smt','sat'], 'qe') add_lib('qe', ['smt','sat'], 'qe')
add_lib('duality', ['smt', 'interp', 'qe']) add_lib('duality', ['smt', 'interp', 'qe'])
@ -71,6 +70,7 @@ def init_project_def():
add_lib('fp', ['muz', 'pdr', 'clp', 'tab', 'rel', 'bmc', 'duality_intf', 'ddnf'], 'muz/fp') add_lib('fp', ['muz', 'pdr', 'clp', 'tab', 'rel', 'bmc', 'duality_intf', 'ddnf'], 'muz/fp')
add_lib('nlsat_smt_tactic', ['nlsat_tactic', 'smt_tactic'], 'tactic/nlsat_smt') add_lib('nlsat_smt_tactic', ['nlsat_tactic', 'smt_tactic'], 'tactic/nlsat_smt')
add_lib('smtlogic_tactics', ['arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'fp', 'muz','qe','nlsat_smt_tactic'], 'tactic/smtlogics') add_lib('smtlogic_tactics', ['arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'fp', 'muz','qe','nlsat_smt_tactic'], 'tactic/smtlogics')
add_lib('fpa_tactics', ['fpa', 'core_tactics', 'bv_tactics', 'sat_tactic', 'smt_tactic', 'arith_tactics', 'smtlogic_tactics'], 'tactic/fpa')
add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv') add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv')
add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa_tactics', 'aig_tactic', 'fp', 'qe','sls_tactic', 'subpaving_tactic'], 'tactic/portfolio') add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa_tactics', 'aig_tactic', 'fp', 'qe','sls_tactic', 'subpaving_tactic'], 'tactic/portfolio')
add_lib('smtparser', ['portfolio'], 'parsers/smt') add_lib('smtparser', ['portfolio'], 'parsers/smt')

9
src/tactic/fpa/qffp_tactic.cpp
View file

@ -23,6 +23,8 @@ Notes:
#include"fpa2bv_tactic.h" #include"fpa2bv_tactic.h"
#include"smt_tactic.h" #include"smt_tactic.h"
#include"propagate_values_tactic.h" #include"propagate_values_tactic.h"
#include"probe_arith.h"
#include"qfnra_tactic.h"
#include"qffp_tactic.h" #include"qffp_tactic.h"
@ -40,10 +42,13 @@ tactic * mk_qffp_tactic(ast_manager & m, params_ref const & p) {
mk_propagate_values_tactic(m, p), mk_propagate_values_tactic(m, p),
using_params(mk_simplify_tactic(m, p), simp_p), using_params(mk_simplify_tactic(m, p), simp_p),
mk_bit_blaster_tactic(m, p), mk_bit_blaster_tactic(m, p),
using_params(mk_simplify_tactic(m, p), simp_p), using_params(mk_simplify_tactic(m, p), simp_p),
cond(mk_is_propositional_probe(), cond(mk_is_propositional_probe(),
mk_sat_tactic(m, p), mk_sat_tactic(m, p),
mk_smt_tactic(p)), cond(mk_is_qfnra_probe(),
mk_qfnra_tactic(m, p),
mk_smt_tactic(p))
),
mk_fail_if_undecided_tactic()))); mk_fail_if_undecided_tactic())));
st->updt_params(p); st->updt_params(p);