mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-18 03:46:17 +00:00
Code Activity

adding simplex to diff

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-03-01 13:44:41 -08:00
parent eb6d39ba46
commit c4b1f5c30e
1 changed files with 9 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/smt/theory_diff_logic_def.h
View file

@ -29,6 +29,9 @@ Revision History:
#include"warning.h" #include"warning.h"
#include"smt_model_generator.h" #include"smt_model_generator.h"
#include"model_implicant.h" #include"model_implicant.h"
#include"simplex.h"
#include"simplex_def.h"
using namespace smt; using namespace smt;
@ -998,9 +1001,7 @@ void theory_diff_logic<Ext>::get_implied_bound_antecedents(edge_id bridge_edge,
template<typename Ext> template<typename Ext>
inf_eps_rational<inf_rational> theory_diff_logic<Ext>::maximize(theory_var v) { inf_eps_rational<inf_rational> theory_diff_logic<Ext>::maximize(theory_var v) {
#if 0 simplex::simplex<simplex::mpq_ext> S;
// disabled until fixed.
objective_term const& objective = m_objectives[v]; objective_term const& objective = m_objectives[v];
IF_VERBOSE(1, IF_VERBOSE(1,
@ -1009,6 +1010,11 @@ inf_eps_rational<inf_rational> theory_diff_logic<Ext>::maximize(theory_var v) {
} }
verbose_stream() << "Free coefficient " << m_objective_consts[v] << "\n";); verbose_stream() << "Free coefficient " << m_objective_consts[v] << "\n";);
#if 0
// disabled until fixed.
// Objective coefficients now become balances // Objective coefficients now become balances
vector<fin_numeral> balances(m_graph.get_num_nodes()); vector<fin_numeral> balances(m_graph.get_num_nodes());
balances.fill(fin_numeral::zero()); balances.fill(fin_numeral::zero());