mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-20 03:12:03 +00:00
Code Activity

try to fix gcc build

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-04-30 13:06:59 -07:00
parent fbe4af6336
commit b4d0216728
1 changed files with 6 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/smt/theory_horn_ineq_def.h
View file

@ -797,10 +797,10 @@ namespace smt {
template<typename Ext> template<typename Ext>
typename theory_horn_ineq<Ext>::numeral theory_horn_ineq<Ext>::mk_weight(bool is_real, bool is_strict, rational const& w) const { typename theory_horn_ineq<Ext>::numeral theory_horn_ineq<Ext>::mk_weight(bool is_real, bool is_strict, rational const& w) const {
if (is_strict) { if (is_strict) {
return numeral(inf_numeral(w)) + (is_real?m_epsilon:numeral(1)); return numeral(Ext::inf_numeral(w)) + (is_real?Ext::m_epsilon:numeral(1));
} }
else { else {
return numeral(inf_numeral(w)); return numeral(Ext::inf_numeral(w));
} }
} }
@ -1001,9 +1001,9 @@ namespace smt {
th_var target = mk_var(ctx.mk_enode(n, false, false, true)); th_var target = mk_var(ctx.mk_enode(n, false, false, true));
coeffs.push_back(std::make_pair(target, rational(-1))); coeffs.push_back(std::make_pair(target, rational(-1)));
VERIFY(m_graph->enable_clause(m_graph->add_ineq(coeffs, numeral(inf_numeral(w)), null_literal))); VERIFY(m_graph->enable_clause(m_graph->add_ineq(coeffs, numeral(Ext::inf_numeral(w)), null_literal)));
negate(coeffs, w); negate(coeffs, w);
VERIFY(m_graph->enable_clause(m_graph->add_ineq(coeffs, numeral(inf_numeral(w)), null_literal))); VERIFY(m_graph->enable_clause(m_graph->add_ineq(coeffs, numeral(Ext::inf_numeral(w)), null_literal)));
return target; return target;
} }
@ -1024,9 +1024,9 @@ namespace smt {
// v = k: v <= k k <= v // v = k: v <= k k <= v
coeffs coeffs; coeffs coeffs;
coeffs.push_back(std::make_pair(v, rational(1))); coeffs.push_back(std::make_pair(v, rational(1)));
VERIFY(m_graph->enable_clause(m_graph->add_ineq(coeffs, numeral(inf_numeral(r)), null_literal))); VERIFY(m_graph->enable_clause(m_graph->add_ineq(coeffs, numeral(Ext::inf_numeral(r)), null_literal)));
coeffs.back().second.neg(); coeffs.back().second.neg();
VERIFY (m_graph->enable_clause(m_graph->add_ineq(coeffs, numeral(inf_numeral(-r)), null_literal))); VERIFY (m_graph->enable_clause(m_graph->add_ineq(coeffs, numeral(Ext::inf_numeral(-r)), null_literal)));
} }
return v; return v;
} }