mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-28 08:58:44 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-04-29 10:14:50 -07:00
parent 6b2ce7fa65
commit 481d9ad14a
1 changed files with 4 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/math/polysat/fixplex_def.h
View file

@ -205,6 +205,7 @@ namespace polysat {
return false; return false;
} }
#if 0
/** /**
\brief Select a variable x_j in the row r defining the base var x_i, \brief Select a variable x_j in the row r defining the base var x_i,
s.t. x_j can be used to patch the error in x_i. Return null_theory_var s.t. x_j can be used to patch the error in x_i. Return null_theory_var
@ -215,8 +216,8 @@ namespace polysat {
bound (above its upper bound). bound (above its upper bound).
*/ */
template<typename Ext> template<typename Ext>
typename simplex<Ext>::var_t typename fixplex<Ext>::var_t
simplex<Ext>::select_pivot_core(var_t x_i, numeral & out_a_ij) { fixplex<Ext>::select_pivot_core(var_t x_i, numeral & out_a_ij) {
SASSERT(is_base(x_i)); SASSERT(is_base(x_i));
var_t max = get_num_vars(); var_t max = get_num_vars();
var_t result = max; var_t result = max;
@ -255,6 +256,7 @@ namespace polysat {
} }
return result < max ? result : null_var; return result < max ? result : null_var;
} }
#endif
/** /**
\brief Given row \brief Given row