mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

mark assumption literals to be skolem to hide them from models #2406

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-07-18 08:25:42 -07:00
parent 4b6a7371dd
commit 5820b16800
4 changed files with 21 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/ast/ast.h
View file

@ -1820,6 +1820,12 @@ public:
arity, domain);
}
func_decl * mk_skolem_const_decl(symbol const& name, sort* s) {
func_decl_info info;
info.set_skolem(true);
return mk_func_decl(name, static_cast<unsigned>(0), nullptr, s, info);
}
func_decl * mk_const_decl(const char* name, sort * s) {
return mk_func_decl(symbol(name), static_cast<unsigned>(0), nullptr, s);
}
@ -1898,6 +1904,10 @@ public:
return mk_app(decl, static_cast<unsigned>(0), static_cast<expr**>(nullptr));
}
app * mk_skolem_const(symbol const & name, sort * s) {
return mk_const(mk_skolem_const_decl(name, s));
}
app * mk_const(symbol const & name, sort * s) {
return mk_const(mk_const_decl(name, s));
}

2
src/cmd_context/cmd_context.cpp
View file

@ -1364,7 +1364,7 @@ void cmd_context::assert_expr(symbol const & name, expr * t) {
m_check_sat_result = nullptr;
m().inc_ref(t);
m_assertions.push_back(t);
expr * ans = m().mk_const(name, m().mk_bool_sort());
app * ans = m().mk_skolem_const(name, m().mk_bool_sort());
m().inc_ref(ans);
m_assertion_names.push_back(ans);
if (m_solver)

5
src/opt/opt_solver.cpp
View file

@ -406,6 +406,11 @@ namespace opt {
smt::theory_rdl& th = dynamic_cast<smt::theory_rdl&>(opt);
return th.mk_ge(m_fm, v, val);
}
if (typeid(smt::theory_rdl) == typeid(opt)) {
smt::theory_rdl& th = dynamic_cast<smt::theory_rdl&>(opt);
return th.mk_ge(m_fm, v, val);
}
if (typeid(smt::theory_dense_i) == typeid(opt) &&
val.get_infinitesimal().is_zero()) {

9
src/smt/theory_diff_logic_def.h
View file

@ -1118,8 +1118,8 @@ unsigned theory_diff_logic<Ext>::simplex2edge(unsigned e) {
template<typename Ext>
void theory_diff_logic<Ext>::update_simplex(Simplex& S) {
unsynch_mpq_manager mgr;
unsynch_mpq_inf_manager inf_mgr;
unsynch_mpq_manager& mgr = inf_mgr.get_mpq_manager();
unsigned num_nodes = m_graph.get_num_nodes();
vector<dl_edge<GExt> > const& es = m_graph.get_all_edges();
S.ensure_var(num_simplex_vars());
@ -1127,7 +1127,8 @@ void theory_diff_logic<Ext>::update_simplex(Simplex& S) {
numeral const& a = m_graph.get_assignment(i);
rational fin = a.get_rational().to_rational();
rational inf = a.get_infinitesimal().to_rational();
mpq_inf q(mgr.dup(fin.to_mpq()), mgr.dup(inf.to_mpq()));
mpq_inf q;
inf_mgr.set(q, fin.to_mpq(), inf.to_mpq());
S.set_value(node2simplex(i), q);
inf_mgr.del(q);
}
@ -1158,7 +1159,8 @@ void theory_diff_logic<Ext>::update_simplex(Simplex& S) {
numeral const& w = e.get_weight();
rational fin = w.get_rational().to_rational();
rational inf = w.get_infinitesimal().to_rational();
mpq_inf q(mgr.dup(fin.to_mpq()), mgr.dup(inf.to_mpq()));
mpq_inf q;
inf_mgr.set(q, fin.to_mpq(), inf.to_mpq());
S.set_upper(base_var, q);
inf_mgr.del(q);
}
@ -1314,7 +1316,6 @@ expr_ref theory_diff_logic<Ext>::mk_ineq(theory_var v, inf_eps const& val, bool
if (is_strict) {
f = m.mk_not(f);
}
TRACE("arith", tout << "block: " << f << "\n";);
return f;
}