mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 05:48:44 +00:00
Code Activity

move parameter checking to API

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-10-08 13:32:25 -07:00
parent 28fb266d8c
commit adb9117a9e
6 changed files with 10 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/api/api_tactic.cpp
View file

@ -222,6 +222,9 @@ extern "C" {
Z3_TRY; Z3_TRY;
LOG_Z3_tactic_using_params(c, t, p); LOG_Z3_tactic_using_params(c, t, p);
RESET_ERROR_CODE(); RESET_ERROR_CODE();
param_descrs r;
to_tactic_ref(t)->collect_param_descrs(r);
to_param_ref(p).validate(r);
tactic * new_t = using_params(to_tactic_ref(t), to_param_ref(p)); tactic * new_t = using_params(to_tactic_ref(t), to_param_ref(p));
RETURN_TACTIC(new_t); RETURN_TACTIC(new_t);
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);

2
src/api/python/z3.py
View file

@ -4467,7 +4467,7 @@ def args2params(arguments, keywords, ctx=None):
A ':' is added to the keywords, and '_' is replaced with '-' A ':' is added to the keywords, and '_' is replaced with '-'
>>> args2params(['model', True, 'relevancy', 2], {'elim_and' : True}) >>> args2params(['model', True, 'relevancy', 2], {'elim_and' : True})
(params model 1 relevancy 2 elim_and 1) (params model true relevancy 2 elim_and true)
""" """
if __debug__: if __debug__:
_z3_assert(len(arguments) % 2 == 0, "Argument list must have an even number of elements.") _z3_assert(len(arguments) % 2 == 0, "Argument list must have an even number of elements.")

4
src/tactic/smtlogics/nra_tactic.cpp
View file

@ -27,10 +27,10 @@ Notes:
tactic * mk_nra_tactic(ast_manager & m, params_ref const& p) { tactic * mk_nra_tactic(ast_manager & m, params_ref const& p) {
params_ref p1 = p; params_ref p1 = p;
p1.set_uint("seed", 11); p1.set_uint("random_seed", 11);
p1.set_bool("factor", false); p1.set_bool("factor", false);
params_ref p2 = p; params_ref p2 = p;
p2.set_uint("seed", 13); p2.set_uint("random_seed", 13);
p2.set_bool("factor", false); p2.set_bool("factor", false);
return and_then(mk_simplify_tactic(m, p), return and_then(mk_simplify_tactic(m, p),

4
src/tactic/smtlogics/qfnra_tactic.cpp
View file

@ -34,10 +34,10 @@ static tactic * mk_qfnra_sat_solver(ast_manager& m, params_ref const& p, unsigne
tactic * mk_qfnra_tactic(ast_manager & m, params_ref const& p) { tactic * mk_qfnra_tactic(ast_manager & m, params_ref const& p) {
params_ref p1 = p; params_ref p1 = p;
p1.set_uint("seed", 11); p1.set_uint("random_seed", 11);
p1.set_bool("factor", false); p1.set_bool("factor", false);
params_ref p2 = p; params_ref p2 = p;
p2.set_uint("seed", 13); p2.set_uint("random_seed", 13);
p2.set_bool("factor", false); p2.set_bool("factor", false);
return and_then(mk_simplify_tactic(m, p), return and_then(mk_simplify_tactic(m, p),

3
src/tactic/tactical.cpp
View file

@ -1229,9 +1229,6 @@ class using_params_tactical : public unary_tactical {
params_ref m_params; params_ref m_params;
public: public:
using_params_tactical(tactic * t, params_ref const & p):unary_tactical(t), m_params(p) { using_params_tactical(tactic * t, params_ref const & p):unary_tactical(t), m_params(p) {
param_descrs r;
collect_param_descrs(r);
p.validate(r);
t->updt_params(p); t->updt_params(p);
} }

3
src/util/params.cpp
View file

@ -309,7 +309,8 @@ public:
p.display(strm, 2, false, false); p.display(strm, 2, false, false);
throw default_exception(strm.str()); throw default_exception(strm.str());
} }
if (it->second.m_kind != expected) { if (it->second.m_kind != expected &&
!(it->second.m_kind == CPK_UINT && expected == CPK_NUMERAL)) {
std::stringstream strm; std::stringstream strm;
strm << "Parameter " << it->first.str() << " was given argument of type "; strm << "Parameter " << it->first.str() << " was given argument of type ";
strm << it->second.m_kind << ", expected " << expected; strm << it->second.m_kind << ", expected " << expected;