3604430784

Build Type

push

github

Committed by GitHub

Commit Message

Merge pull request #422 from ahmed-irfan/ci-coverage

Run Details

75823 of 118295 relevant lines covered (64.1%)

1143759.59 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

0.0

/src/solvers/simplex/simplex_printer.c

/*
 * This file is part of the Yices SMT Solver.
 * Copyright (C) 2017 SRI International.
 *
 * Yices is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 *
 * Yices is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Yices.  If not, see <http://www.gnu.org/licenses/>.
 */

/**************************
 *  PRINT SIMPLEX SOLVER  *
 *************************/

#include <inttypes.h>

#include "solvers/cdcl/smt_core_printer.h"
#include "solvers/egraph/egraph_printer.h"
#include "solvers/simplex/simplex_printer.h"


/*
 * VARIABLE TABLE
 */
static void print_avar(FILE *f, arith_vartable_t *table, thvar_t v) {
  if (arith_var_is_int(table, v)) {
    fprintf(f, "i!%"PRId32, v);
  } else {
    fprintf(f, "z!%"PRId32, v);
  }
}

static void print_avar_power(FILE *f, arith_vartable_t *table, varexp_t *p) {
  print_avar(f, table, p->var);
  if (p->exp > 1) {
    fprintf(f, "^%"PRIu32, p->exp);
  }
}

static void print_avar_product(FILE *f, arith_vartable_t *table, pprod_t *p) {
  int32_t i, n;

  n = p->len;
  if (n == 0) {
    fprintf(f, "1");
  } else {
    i = 0;
    for (;;) {
      print_avar_power(f, table, p->prod + i);
      i ++;
      if (i == n) break;
      fputs(" * ", f);
    }
  }
}

static void print_avar_monomial(FILE *f, arith_vartable_t *table, thvar_t v, rational_t *coeff, bool first) {
  bool negative;
  bool abs_one;

  negative = q_is_neg(coeff);

  if (negative) {
    if (first) {
      fputs("- ", f);
    } else {
      fputs(" - ", f);
    }
    abs_one = q_is_minus_one(coeff);
  } else {
    if (! first) {
      fputs(" + ", f);
    }
    abs_one = q_is_one(coeff);
  }

  if (v == const_idx) {
    q_print_abs(f, coeff);
  } else {
    if (! abs_one) {
      q_print_abs(f, coeff);
      fputs(" * ", f);
    }
    print_avar(f, table, v);
  }
}

static void print_avar_poly(FILE *f, arith_vartable_t *table, polynomial_t *p) {
  uint32_t i, n;

  n = p->nterms;
  if (n == 0) {
    fputc('0', f);
  } else {
    for (i=0; i<n; i++) {
      print_avar_monomial(f, table, p->mono[i].var, &p->mono[i].coeff, i == 0);
    }
  }
}


void print_arith_vartable(FILE *f, arith_vartable_t *table) {
  uint32_t i, n;

  n = table->nvars;
  for (i=0; i<n; i++) {
    print_avar(f, table, i);
    switch (arith_var_kind(table, i)) {
    case AVAR_FREE:
      break;

    case AVAR_POLY:
      fputs(" := ", f);
      print_avar_poly(f, table, arith_var_poly_def(table, i));
      break;

    case AVAR_PPROD:
      fputs(" := ", f);
      print_avar_product(f, table, arith_var_product_def(table, i));
      break;

    case AVAR_CONST:
      fputs(" := ", f);
      q_print(f, arith_var_rational_def(table, i));
      break;
    }

    if (arith_var_has_eterm(table, i)) {
      fputs(" --> ", f);
      print_eterm_id(f, arith_var_eterm(table, i));
    }
    fputc('\n', f);
  }
}


/*
 * ARITHMETIC ATOMS
 */
static void print_arith_atom_op(FILE *f, arithatm_tag_t tag) {
  switch (tag) {
  case GE_ATM:
    fputs(" >= ", f);
    break;
  case LE_ATM:
    fputs(" <= ", f);
    break;
  case EQ_ATM:
    fputs(" == ", f);
    break;
  default:
    fputs(" <badop> ", f);
    break;
  }
}

static void print_arith_atom(FILE *f, arith_vartable_t *table, arith_atom_t *atom) {
  print_avar(f, table, var_of_atom(atom));
  print_arith_atom_op(f, tag_of_atom(atom));
  q_print(f, &atom->bound);
}

void print_arith_atomtable(FILE *f, arith_vartable_t *vtbl, arith_atomtable_t *atbl) {
  uint32_t i, n;
  arith_atom_t *a;

  n = atbl->natoms;
  a = atbl->atoms;
  for (i=0; i<n; i++) {
    print_bvar(f, a[i].boolvar);
    fputs(" := ", f);
    print_arith_atom(f, vtbl, a + i);
    fputs("\t\t", f);
    print_bval(f, bvar_value(atbl->core, a[i].boolvar));
    fputc('\n', f);
  }
}


/*
 * MATRIX
 */

// space for correct alignment when we print xxx[i] in a matrix with n rows
static void print_space(FILE *f, uint32_t i, uint32_t n) {
  uint32_t k;

  k = 1;
  while (10 * k <= i) {
    k *= 10;
  }

  while (10 * k < n) {
    fputc(' ', f);
    k *= 10;
  }
}


// row is printed as a_1 x_1 + .... + a_n x_n == 0
static void print_row(FILE *f, arith_vartable_t *vtbl, row_t *row) {
  uint32_t i, n;
  thvar_t x;
  bool first;

  first = true;
  n = row->size;
  for (i=0; i<n; i++) {
    x = row->data[i].c_idx;
    if (x >= 0) {
      print_avar_monomial(f, vtbl, x, &row->data[i].coeff, first);
      first = false;
    }
  }
  if (first) {
    // nothing printed so the row is empty
    fputc('0', f);
  }
  fputs(" == 0", f);
}


void print_matrix(FILE *f, arith_vartable_t *vtbl, matrix_t *matrix) {
  uint32_t i, n;

  n = matrix->nrows;
  for (i=0; i<n; i++) {
    fprintf(f, "  row[%"PRIu32"]:   ", i);
    print_space(f, i, n);
    print_row(f, vtbl, matrix->row[i]);
    fputc('\n', f);
  }
  fputc('\n', f);
}


void print_elim_matrix(FILE *f, arith_vartable_t *vtbl, elim_matrix_t *elim) {
  uint32_t i, n;

  n = elim->nrows;
  for (i=0; i<n; i++) {
    fprintf(f, "  elim[%"PRIu32"]:   ", i);
    print_space(f, i, n);
    print_avar_poly(f, vtbl, elim->row[i]);
    fputs("  (", f);
    print_avar(f, vtbl, elim->base_var[i]);
    fputs(")\n", f);
  }
  fputc('\n', f);
}


void print_fixed_var_vector(FILE *f, arith_vartable_t *vtbl, fvar_vector_t *fvars) {
  uint32_t i, n;

  n = fvars->nvars;
  for (i=0; i<n; i++) {
    fprintf(f, "  fixed[%"PRIu32"]:   ", i);
    print_space(f, i, n);
    print_avar(f, vtbl, fvars->fvar[i].var);
    fputs(" == ", f);
    q_print(f, &fvars->fvar[i].value);
    fputc('\n', f);
  }
  fputc('\n', f);
}



/*
 * Bounds on variable x
 */
static void print_avar_bounds(FILE *f, simplex_solver_t *solver, thvar_t x) {
  int32_t lb, ub;

  lb = arith_var_lower_index(&solver->vtbl, x);
  ub = arith_var_upper_index(&solver->vtbl, x);
  if (lb >= 0 || ub >= 0) {
    fputs("  ", f);
    if (lb >= 0) {
      xq_print(f, solver->bstack.bound + lb);
      fputs(" <= ", f);
    }
    print_avar(f, &solver->vtbl, x);
    if (ub >= 0) {
      fputs(" <= ", f);
      xq_print(f, solver->bstack.bound + ub);
    }
    fputc('\n', f);
  }
}


/*
 * Value of variable x
 */
static void print_avar_value(FILE *f, arith_vartable_t *vtbl, thvar_t x) {
  fputs("  val[", f);
  print_avar(f, vtbl, x);
  fputs("] = ", f);
  xq_print(f, arith_var_value(vtbl, x));
}


/*
 * Bounds + value of x + row where x is basic
 */
static void print_avar_full(FILE *f, simplex_solver_t *solver, thvar_t x) {
  int32_t lb, ub, r;

  lb = arith_var_lower_index(&solver->vtbl, x);
  ub = arith_var_upper_index(&solver->vtbl, x);
  r = matrix_basic_row(&solver->matrix, x);

  fputs("  ", f);
  print_avar(f, &solver->vtbl, x);
  fputs(" = ", f);
  xq_print(f, arith_var_value(&solver->vtbl, x));
  fputc('\t', f);

  if (lb >= 0 || ub >= 0) {
    if (lb >= 0) {
      xq_print(f, solver->bstack.bound + lb);
      fputs(" <= ", f);
    }
    print_avar(f, &solver->vtbl, x);
    if (ub >= 0) {
      fputs(" <= ", f);
      xq_print(f, solver->bstack.bound + ub);
    }
  } else {
    fputs("no bounds", f);
  }

  if (r >= 0) {
    fprintf(f, "\t\tbasic in row[%"PRIu32"]\n", r);
  } else {
    fprintf(f, "\t\tnon basic\n");
  }
}


/*
 * Bounds + value of x
 */
static void print_avar_bounds_and_value(FILE *f, simplex_solver_t *solver, thvar_t x) {
  int32_t lb, ub;

  lb = arith_var_lower_index(&solver->vtbl, x);
  ub = arith_var_upper_index(&solver->vtbl, x);

  fputs("  ", f);
  print_avar(f, &solver->vtbl, x);
  fputs(" = ", f);
  xq_print(f, arith_var_value(&solver->vtbl, x));

  if (lb >= 0 || ub >= 0) {
    fputc('\t', f);
    if (lb >= 0) {
      xq_print(f, solver->bstack.bound + lb);
      fputs(" <= ", f);
    }
    print_avar(f, &solver->vtbl, x);
    if (ub >= 0) {
      fputs(" <= ", f);
      xq_print(f, solver->bstack.bound + ub);
    }
  }

  fputc('\n', f);
}


/*
 * Simplex components
 */
void print_simplex_vars(FILE *f, simplex_solver_t *solver) {
  print_arith_vartable(f, &solver->vtbl);
}

void print_simplex_atoms(FILE *f, simplex_solver_t *solver) {
  print_arith_atomtable(f, &solver->vtbl, &solver->atbl);
}

void print_simplex_atom(FILE *f, simplex_solver_t *solver, int32_t id) {
  print_arith_atom(f, &solver->vtbl, arith_atom(&solver->atbl, id));
}

void print_simplex_row(FILE *f, simplex_solver_t *solver, row_t *row) {
  print_row(f, &solver->vtbl, row);
}

void print_simplex_matrix(FILE *f, simplex_solver_t *solver) {
  print_matrix(f, &solver->vtbl, &solver->matrix);
}

void print_simplex_saved_rows(FILE *f, simplex_solver_t *solver) {
  pvector_t *v;
  uint32_t i, n;

  v = &solver->saved_rows;
  n = v->size;
  for (i=0; i<n; i++) {
    fprintf(f, "saved[%"PRIu32"]: ", i);
    print_avar_poly(f, &solver->vtbl, v->data[i]);
    fputc('\n', f);
  }
  fputc('\n', f);
}


void print_simplex_basic_vars(FILE *f, simplex_solver_t *solver) {
  matrix_t *matrix;
  uint32_t i, n;
  int32_t x;

  matrix = &solver->matrix;
  n = matrix->nrows;
  for (i=0; i<n; i++) {
    fprintf(f, "  row[%"PRIu32"]: ", i);
    x = matrix->base_var[i];
    if (x >=0 ) {
      fputs("basic var = ", f);
      print_avar(f, &solver->vtbl, x);
      fputc('\n', f);
    } else {
      fputs("no basic var\n", f);
    }
  }
  fputc('\n', f);
}


void print_simplex_bounds(FILE *f, simplex_solver_t *solver) {
  uint32_t i, n;

  n = num_arith_vars(&solver->vtbl);
  for (i=0; i<n; i++) {
    print_avar_bounds(f, solver, i);
  }
}

void print_simplex_assignment(FILE *f, simplex_solver_t *solver) {
  uint32_t i, n;

  n = num_arith_vars(&solver->vtbl);
  for (i=0; i<n; i++) {
    print_avar_value(f, &solver->vtbl, i);
    fputc('\n', f);
  }
}

void print_simplex_bounds_and_assignment(FILE *f, simplex_solver_t *solver) {
  uint32_t i, n;

  n = num_arith_vars(&solver->vtbl);
  for (i=0; i<n; i++) {
    print_avar_bounds_and_value(f, solver, i);
  }
  fputc('\n', f);
}

void print_simplex_allvars(FILE *f, simplex_solver_t *solver) {
  uint32_t i, n;

  n = num_arith_vars(&solver->vtbl);
  for (i=0; i<n; i++) {
    print_avar_full(f, solver, i);
  }
  fputc('\n', f);
}


void print_simplex_vars_summary(FILE *f, simplex_solver_t *solver) {
  arith_vartable_t *table;
  uint32_t i, n;
  int32_t lb, ub;

  table = &solver->vtbl;
  n = num_arith_vars(table);
  for (i=0; i<n; i++) {
    lb = arith_var_lower_index(&solver->vtbl, i);
    ub = arith_var_upper_index(&solver->vtbl, i);

    if (matrix_is_basic_var(&solver->matrix, i)) {
      fputs(" b ", f);
    } else {
      fputs("   ", f);
    }
    print_avar(f, table, i);
    fputs(" = ", f);
    xq_print(f, arith_var_value(&solver->vtbl, i));


    if (lb >= 0 || ub >= 0) {
      fputs("\t", f);
      if (lb >= 0) {
        xq_print(f, solver->bstack.bound + lb);
        fputs(" <= ", f);
      }
      print_avar(f, &solver->vtbl, i);
      if (ub >= 0) {
        fputs(" <= ", f);
        xq_print(f, solver->bstack.bound + ub);
      }
    }

    if (arith_var_has_eterm(table, i)) {
      fputs("\t\teterm: ", f);
      print_eterm_id(f, arith_var_eterm(table, i));
    }
    if (arith_var_def_is_poly(table, i)) {
      fputs("\t\tdef: ", f);
      print_avar_poly(f, table, arith_var_poly_def(table, i));
    } else if (arith_var_def_is_product(table, i)) {
      fputs("\t\tdef: ", f);
      print_avar_product(f, table, arith_var_product_def(table, i));
    }
    fputc('\n', f);
  }
  fputc('\n', f);
}


void print_simplex_vardef(FILE *f, simplex_solver_t *solver, thvar_t v) {
  arith_vartable_t *table;

  table = &solver->vtbl;
  print_avar(f, table, v);
  if (arith_var_def_is_poly(table, v)) {
    fputs(" := ", f);
    print_avar_poly(f, table, arith_var_poly_def(table, v));
  } else if (arith_var_def_is_product(table, v)) {
    fputs(" := ", f);
    print_avar_product(f, table, arith_var_product_def(table, v));
  }
  fputc('\n', f);
}

void print_simplex_var(FILE *f, simplex_solver_t *solver, thvar_t v) {
  print_avar(f, &solver->vtbl, v);
}

void print_simplex_var_value(FILE *f, simplex_solver_t *solver, thvar_t v) {
  xq_print(f, arith_var_value(&solver->vtbl, v));
}

void print_simplex_var_bounds(FILE *f, simplex_solver_t *solver, thvar_t v) {
  print_avar_bounds(f, solver, v);
}

void print_simplex_atomdef(FILE *f, simplex_solver_t *solver, bvar_t v) {
  void *atm;
  arith_atom_t *a;
  int32_t i;

  atm = get_bvar_atom(solver->core, v);
  i = arithatom_tagged_ptr2idx(atm);
  a = arith_atom(&solver->atbl, i);
  assert(a->boolvar == v);
  print_bvar(f, v);
  fputs(" := ", f);
  print_arith_atom(f, &solver->vtbl, a);
  fputc('\n', f);
}


void print_simplex_atom_of_literal(FILE *f, simplex_solver_t *solver, literal_t l) {
  void *atm;
  arith_atom_t *a;
  bvar_t v;
  int32_t i;

  v = var_of(l);
  assert(bvar_has_atom(solver->core, v));
  atm = bvar_atom(solver->core, v);
  assert(atom_tag(atm) == ARITH_ATM_TAG);
  i = arithatom_tagged_ptr2idx(atm);
  a = arith_atom(&solver->atbl, i);
  assert(a->boolvar == v);

  if (is_neg(l)) {
    fputs("(not ", f);
  }
  print_arith_atom(f, &solver->vtbl, a);
  if (is_neg(l)) {
    fputc(')', f);
  }
}


void print_simplex_buffer(FILE *f, simplex_solver_t *solver) {
  poly_buffer_t *b;
  uint32_t i, n;

  b = &solver->buffer;
  n = b->nterms;
  if (n == 0) {
    fputc('0', f);
  } else {
    for (i=0; i<n; i++) {
      print_avar_monomial(f, &solver->vtbl, b->mono[i].var, &b->mono[i].coeff, i == 0);
    }
  }
}


void print_simplex_bound(FILE *f, simplex_solver_t *solver, uint32_t i) {
  fprintf(f, "bound[%"PRIu32"]: ", i);
  if (i < solver->bstack.top) {
    print_avar(f, &solver->vtbl, solver->bstack.var[i]);
    if (arith_tag_get_type(solver->bstack.tag[i]) == ATYPE_UB) {
      fputs(" <= ", f);
    } else {
      fputs(" >= ", f);
    }
    xq_print(f, solver->bstack.bound + i);
  } else {
    fprintf(f, "<INVALID BOUND INDEX>");
  }
}




/*
 * FLAGS/BASE LEVEL
 */
static char *bool2string(bool x) {
  return x ? "true" : "false";
}

void print_simplex_flags(FILE *f, simplex_solver_t *solver) {
  fprintf(f, "base level:     %"PRIu32"\n", solver->base_level);
  fprintf(f, "decision level: %"PRIu32"\n", solver->decision_level);
  fprintf(f, "matrix ready:   %s\n", bool2string(solver->matrix_ready));
  fprintf(f, "tableau ready:  %s\n", bool2string(solver->tableau_ready));
  fprintf(f, "save rows:      %s\n", bool2string(solver->save_rows));
}



/*
 * Print row in a simplified form: replace fixed variables by their value
 */
void print_simplex_reduced_row(FILE *f, simplex_solver_t *solver, row_t *row) {
  arith_vartable_t *vtbl;
  arith_bstack_t *bstack;
  rational_t q;
  uint32_t i, n;
  thvar_t x;
  bool first;
  int32_t l, u;

  vtbl = &solver->vtbl;
  bstack = &solver->bstack;

  // compute the constant
  q_init(&q);
  n = row->size;
  for (i=0; i<n; i++) {
    x = row->data[i].c_idx;
    if (x >= 0) {
      l = arith_var_lower_index(&solver->vtbl, x);
      u = arith_var_upper_index(&solver->vtbl, x);
      if (l >= 0 && u >= 0 && xq_eq(bstack->bound + l, bstack->bound + u)) {
        // x is a a fixed variable
        assert(xq_eq(bstack->bound + l, arith_var_value(vtbl, x)));
        assert(xq_is_rational(arith_var_value(vtbl, x)));
        q_addmul(&q, &row->data[i].coeff, &arith_var_value(vtbl, x)->main);
      }
    }
  }

  // print the non-constant monomials and q
  first = true;
  if (q_is_nonzero(&q)) {
    print_avar_monomial(f, vtbl, const_idx, &q, first);
    first = false;
  }

  for (i=0; i<n; i++) {
    x = row->data[i].c_idx;
    if (x >= 0) {
      l = arith_var_lower_index(&solver->vtbl, x);
      u = arith_var_upper_index(&solver->vtbl, x);
      if (l < 0 || u < 0 || xq_neq(bstack->bound + l, bstack->bound + u)) {
        // x is not a fixed variable
        print_avar_monomial(f, vtbl, x, &row->data[i].coeff, first);
        first = false;
      }
    }
  }

  if (first) {
    // nothing printed so the row is empty
    fputc('0', f);
  }
  fputs(" == 0", f);

  q_clear(&q);
}



/*
 * Variant of print_simplex_bounds
 */
void print_simplex_bounds2(FILE *f, simplex_solver_t *solver) {
  uint32_t i, n;
  int32_t lb, ub;

  n = num_arith_vars(&solver->vtbl);
  for (i=0; i<n; i++) {
    lb = arith_var_lower_index(&solver->vtbl, i);
    ub = arith_var_upper_index(&solver->vtbl, i);
    if (lb >= 0 && ub >= 0) {
      if (xq_neq(solver->bstack.bound + lb, solver->bstack.bound + ub)) {
        fputs("  ", f);
        xq_print(f, solver->bstack.bound + lb);
        fprintf(f, " <= x_%"PRIu32" <= ", i);
        xq_print(f, solver->bstack.bound + ub);
        fputc('\n', f);
      }
    } else if (lb >= 0) {
      fputs("  ", f);
      xq_print(f, solver->bstack.bound + lb);
      fprintf(f, " <= x_%"PRIu32"\n", i);
    } else if (ub >= 0) {
      fprintf(f, "  x_%"PRIu32" <= ", i);
      xq_print(f, solver->bstack.bound + ub);
      fputc('\n', f);
    }
  }
}



1	/*
2	* This file is part of the Yices SMT Solver.
3	* Copyright (C) 2017 SRI International.
4	*
5	* Yices is free software: you can redistribute it and/or modify
6	* it under the terms of the GNU General Public License as published by
7	* the Free Software Foundation, either version 3 of the License, or
8	* (at your option) any later version.
9	*
10	* Yices is distributed in the hope that it will be useful,
11	* but WITHOUT ANY WARRANTY; without even the implied warranty of
12	* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13	* GNU General Public License for more details.
14	*
15	* You should have received a copy of the GNU General Public License
16	* along with Yices. If not, see <http://www.gnu.org/licenses/>.
17	*/
18
19	/**************************
20	* PRINT SIMPLEX SOLVER *
21	*************************/
22
23	#include <inttypes.h>
24
25	#include "solvers/cdcl/smt_core_printer.h"
26	#include "solvers/egraph/egraph_printer.h"
27	#include "solvers/simplex/simplex_printer.h"
28
29
30	/*
31	* VARIABLE TABLE
32	*/
33	static void print_avar(FILE f, arith_vartable_t table, thvar_t v) {	×
34	if (arith_var_is_int(table, v)) {	×
35	fprintf(f, "i!%"PRId32, v);	×
36	} else {
37	fprintf(f, "z!%"PRId32, v);	×
38	}
39	}	×
40
41	static void print_avar_power(FILE f, arith_vartable_t table, varexp_t *p) {	×
42	print_avar(f, table, p->var);	×
43	if (p->exp > 1) {	×
44	fprintf(f, "^%"PRIu32, p->exp);	×
45	}
46	}	×
47
48	static void print_avar_product(FILE f, arith_vartable_t table, pprod_t *p) {	×
49	int32_t i, n;
50
51	n = p->len;	×
52	if (n == 0) {	×
53	fprintf(f, "1");	×
54	} else {
55	i = 0;	×
56	for (;;) {
57	print_avar_power(f, table, p->prod + i);	×
58	i ++;	×
59	if (i == n) break;	×
60	fputs(" * ", f);	×
61	}
62	}
63	}	×
64
65	static void print_avar_monomial(FILE f, arith_vartable_t table, thvar_t v, rational_t *coeff, bool first) {	×
66	bool negative;
67	bool abs_one;
68
69	negative = q_is_neg(coeff);	×
70
71	if (negative) {	×
72	if (first) {	×
73	fputs("- ", f);	×
74	} else {
75	fputs(" - ", f);	×
76	}
77	abs_one = q_is_minus_one(coeff);	×
78	} else {
79	if (! first) {	×
80	fputs(" + ", f);	×
81	}
82	abs_one = q_is_one(coeff);	×
83	}
84
85	if (v == const_idx) {	×
86	q_print_abs(f, coeff);	×
87	} else {
88	if (! abs_one) {	×
89	q_print_abs(f, coeff);	×
90	fputs(" * ", f);	×
91	}
92	print_avar(f, table, v);	×
93	}
94	}	×
95
96	static void print_avar_poly(FILE f, arith_vartable_t table, polynomial_t *p) {	×
97	uint32_t i, n;
98
99	n = p->nterms;	×
100	if (n == 0) {	×
101	fputc('0', f);	×
102	} else {
103	for (i=0; i<n; i++) {	×
104	print_avar_monomial(f, table, p->mono[i].var, &p->mono[i].coeff, i == 0);	×
105	}
106	}
107	}	×
108
109
110	void print_arith_vartable(FILE f, arith_vartable_t table) {	×
111	uint32_t i, n;
112
113	n = table->nvars;	×
114	for (i=0; i<n; i++) {	×
115	print_avar(f, table, i);	×
116	switch (arith_var_kind(table, i)) {	×
117	case AVAR_FREE:	×
118	break;	×
119
120	case AVAR_POLY:	×
121	fputs(" := ", f);	×
122	print_avar_poly(f, table, arith_var_poly_def(table, i));	×
123	break;	×
124
125	case AVAR_PPROD:	×
126	fputs(" := ", f);	×
127	print_avar_product(f, table, arith_var_product_def(table, i));	×
128	break;	×
129
130	case AVAR_CONST:	×
131	fputs(" := ", f);	×
132	q_print(f, arith_var_rational_def(table, i));	×
133	break;	×
134	}
135
136	if (arith_var_has_eterm(table, i)) {	×
137	fputs(" --> ", f);	×
138	print_eterm_id(f, arith_var_eterm(table, i));	×
139	}
140	fputc('\n', f);	×
141	}
142	}	×
143
144
145	/*
146	* ARITHMETIC ATOMS
147	*/
148	static void print_arith_atom_op(FILE *f, arithatm_tag_t tag) {	×
149	switch (tag) {	×
150	case GE_ATM:	×
151	fputs(" >= ", f);	×
152	break;	×
153	case LE_ATM:	×
154	fputs(" <= ", f);	×
155	break;	×
156	case EQ_ATM:	×
157	fputs(" == ", f);	×
158	break;	×
159	default:	×
160	fputs(" <badop> ", f);	×
161	break;	×
162	}
163	}	×
164
165	static void print_arith_atom(FILE f, arith_vartable_t table, arith_atom_t *atom) {	×
166	print_avar(f, table, var_of_atom(atom));	×
167	print_arith_atom_op(f, tag_of_atom(atom));	×
168	q_print(f, &atom->bound);	×
169	}	×
170
171	void print_arith_atomtable(FILE f, arith_vartable_t vtbl, arith_atomtable_t *atbl) {	×
172	uint32_t i, n;
173	arith_atom_t *a;
174
175	n = atbl->natoms;	×
176	a = atbl->atoms;	×
177	for (i=0; i<n; i++) {	×
178	print_bvar(f, a[i].boolvar);	×
179	fputs(" := ", f);	×
180	print_arith_atom(f, vtbl, a + i);	×
181	fputs("\t\t", f);	×
182	print_bval(f, bvar_value(atbl->core, a[i].boolvar));	×
183	fputc('\n', f);	×
184	}
185	}	×
186
187
188	/*
189	* MATRIX
190	*/
191
192	// space for correct alignment when we print xxx[i] in a matrix with n rows
193	static void print_space(FILE *f, uint32_t i, uint32_t n) {	×
194	uint32_t k;
195
196	k = 1;	×
197	while (10 * k <= i) {	×
198	k *= 10;	×
199	}
200
201	while (10 * k < n) {	×
202	fputc(' ', f);	×
203	k *= 10;	×
204	}
205	}	×
206
207
208	// row is printed as a_1 x_1 + .... + a_n x_n == 0
209	static void print_row(FILE f, arith_vartable_t vtbl, row_t *row) {	×
210	uint32_t i, n;
211	thvar_t x;
212	bool first;
213
214	first = true;	×
215	n = row->size;	×
216	for (i=0; i<n; i++) {	×
217	x = row->data[i].c_idx;	×
218	if (x >= 0) {	×
219	print_avar_monomial(f, vtbl, x, &row->data[i].coeff, first);	×
220	first = false;	×
221	}
222	}
223	if (first) {	×
224	// nothing printed so the row is empty
225	fputc('0', f);	×
226	}
227	fputs(" == 0", f);	×
228	}	×
229
230
231	void print_matrix(FILE f, arith_vartable_t vtbl, matrix_t *matrix) {	×
232	uint32_t i, n;
233
234	n = matrix->nrows;	×
235	for (i=0; i<n; i++) {	×
236	fprintf(f, " row[%"PRIu32"]: ", i);	×
237	print_space(f, i, n);	×
238	print_row(f, vtbl, matrix->row[i]);	×
239	fputc('\n', f);	×
240	}
241	fputc('\n', f);	×
242	}	×
243
244
245	void print_elim_matrix(FILE f, arith_vartable_t vtbl, elim_matrix_t *elim) {	×
246	uint32_t i, n;
247
248	n = elim->nrows;	×
249	for (i=0; i<n; i++) {	×
250	fprintf(f, " elim[%"PRIu32"]: ", i);	×
251	print_space(f, i, n);	×
252	print_avar_poly(f, vtbl, elim->row[i]);	×
253	fputs(" (", f);	×
254	print_avar(f, vtbl, elim->base_var[i]);	×
255	fputs(")\n", f);	×
256	}
257	fputc('\n', f);	×
258	}	×
259
260
261	void print_fixed_var_vector(FILE f, arith_vartable_t vtbl, fvar_vector_t *fvars) {	×
262	uint32_t i, n;
263
264	n = fvars->nvars;	×
265	for (i=0; i<n; i++) {	×
266	fprintf(f, " fixed[%"PRIu32"]: ", i);	×
267	print_space(f, i, n);	×
268	print_avar(f, vtbl, fvars->fvar[i].var);	×
269	fputs(" == ", f);	×
270	q_print(f, &fvars->fvar[i].value);	×
271	fputc('\n', f);	×
272	}
273	fputc('\n', f);	×
274	}	×
275
276
277
278	/*
279	* Bounds on variable x
280	*/
281	static void print_avar_bounds(FILE f, simplex_solver_t solver, thvar_t x) {	×
282	int32_t lb, ub;
283
284	lb = arith_var_lower_index(&solver->vtbl, x);	×
285	ub = arith_var_upper_index(&solver->vtbl, x);	×
286	if (lb >= 0 \|\| ub >= 0) {	×
287	fputs(" ", f);	×
288	if (lb >= 0) {	×
289	xq_print(f, solver->bstack.bound + lb);	×
290	fputs(" <= ", f);	×
291	}
292	print_avar(f, &solver->vtbl, x);	×
293	if (ub >= 0) {	×
294	fputs(" <= ", f);	×
295	xq_print(f, solver->bstack.bound + ub);	×
296	}
297	fputc('\n', f);	×
298	}
299	}	×
300
301
302	/*
303	* Value of variable x
304	*/
305	static void print_avar_value(FILE f, arith_vartable_t vtbl, thvar_t x) {	×
306	fputs(" val[", f);	×
307	print_avar(f, vtbl, x);	×
308	fputs("] = ", f);	×
309	xq_print(f, arith_var_value(vtbl, x));	×
310	}	×
311
312
313	/*
314	* Bounds + value of x + row where x is basic
315	*/
316	static void print_avar_full(FILE f, simplex_solver_t solver, thvar_t x) {	×
317	int32_t lb, ub, r;
318
319	lb = arith_var_lower_index(&solver->vtbl, x);	×
320	ub = arith_var_upper_index(&solver->vtbl, x);	×
321	r = matrix_basic_row(&solver->matrix, x);	×
322
323	fputs(" ", f);	×
324	print_avar(f, &solver->vtbl, x);	×
325	fputs(" = ", f);	×
326	xq_print(f, arith_var_value(&solver->vtbl, x));	×
327	fputc('\t', f);	×
328
329	if (lb >= 0 \|\| ub >= 0) {	×
330	if (lb >= 0) {	×
331	xq_print(f, solver->bstack.bound + lb);	×
332	fputs(" <= ", f);	×
333	}
334	print_avar(f, &solver->vtbl, x);	×
335	if (ub >= 0) {	×
336	fputs(" <= ", f);	×
337	xq_print(f, solver->bstack.bound + ub);	×
338	}
339	} else {
340	fputs("no bounds", f);	×
341	}
342
343	if (r >= 0) {	×
344	fprintf(f, "\t\tbasic in row[%"PRIu32"]\n", r);	×
345	} else {
346	fprintf(f, "\t\tnon basic\n");	×
347	}
348	}	×
349
350
351	/*
352	* Bounds + value of x
353	*/
354	static void print_avar_bounds_and_value(FILE f, simplex_solver_t solver, thvar_t x) {	×
355	int32_t lb, ub;
356
357	lb = arith_var_lower_index(&solver->vtbl, x);	×
358	ub = arith_var_upper_index(&solver->vtbl, x);	×
359
360	fputs(" ", f);	×
361	print_avar(f, &solver->vtbl, x);	×
362	fputs(" = ", f);	×
363	xq_print(f, arith_var_value(&solver->vtbl, x));	×
364
365	if (lb >= 0 \|\| ub >= 0) {	×
366	fputc('\t', f);	×
367	if (lb >= 0) {	×
368	xq_print(f, solver->bstack.bound + lb);	×
369	fputs(" <= ", f);	×
370	}
371	print_avar(f, &solver->vtbl, x);	×
372	if (ub >= 0) {	×
373	fputs(" <= ", f);	×
374	xq_print(f, solver->bstack.bound + ub);	×
375	}
376	}
377
378	fputc('\n', f);	×
379	}	×
380
381
382	/*
383	* Simplex components
384	*/
385	void print_simplex_vars(FILE f, simplex_solver_t solver) {	×
386	print_arith_vartable(f, &solver->vtbl);	×
387	}	×
388
389	void print_simplex_atoms(FILE f, simplex_solver_t solver) {	×
390	print_arith_atomtable(f, &solver->vtbl, &solver->atbl);	×
391	}	×
392
393	void print_simplex_atom(FILE f, simplex_solver_t solver, int32_t id) {	×
394	print_arith_atom(f, &solver->vtbl, arith_atom(&solver->atbl, id));	×
395	}	×
396
397	void print_simplex_row(FILE f, simplex_solver_t solver, row_t *row) {	×
398	print_row(f, &solver->vtbl, row);	×
399	}	×
400
401	void print_simplex_matrix(FILE f, simplex_solver_t solver) {	×
402	print_matrix(f, &solver->vtbl, &solver->matrix);	×
403	}	×
404
405	void print_simplex_saved_rows(FILE f, simplex_solver_t solver) {	×
406	pvector_t *v;
407	uint32_t i, n;
408
409	v = &solver->saved_rows;	×
410	n = v->size;	×
411	for (i=0; i<n; i++) {	×
412	fprintf(f, "saved[%"PRIu32"]: ", i);	×
413	print_avar_poly(f, &solver->vtbl, v->data[i]);	×
414	fputc('\n', f);	×
415	}
416	fputc('\n', f);	×
417	}	×
418
419
420	void print_simplex_basic_vars(FILE f, simplex_solver_t solver) {	×
421	matrix_t *matrix;
422	uint32_t i, n;
423	int32_t x;
424
425	matrix = &solver->matrix;	×
426	n = matrix->nrows;	×
427	for (i=0; i<n; i++) {	×
428	fprintf(f, " row[%"PRIu32"]: ", i);	×
429	x = matrix->base_var[i];	×
430	if (x >=0 ) {	×
431	fputs("basic var = ", f);	×
432	print_avar(f, &solver->vtbl, x);	×
433	fputc('\n', f);	×
434	} else {
435	fputs("no basic var\n", f);	×
436	}
437	}
438	fputc('\n', f);	×
439	}	×
440
441
442	void print_simplex_bounds(FILE f, simplex_solver_t solver) {	×
443	uint32_t i, n;
444
445	n = num_arith_vars(&solver->vtbl);	×
446	for (i=0; i<n; i++) {	×
447	print_avar_bounds(f, solver, i);	×
448	}
449	}	×
450
451	void print_simplex_assignment(FILE f, simplex_solver_t solver) {	×
452	uint32_t i, n;
453
454	n = num_arith_vars(&solver->vtbl);	×
455	for (i=0; i<n; i++) {	×
456	print_avar_value(f, &solver->vtbl, i);	×
457	fputc('\n', f);	×
458	}
459	}	×
460
461	void print_simplex_bounds_and_assignment(FILE f, simplex_solver_t solver) {	×
462	uint32_t i, n;
463
464	n = num_arith_vars(&solver->vtbl);	×
465	for (i=0; i<n; i++) {	×
466	print_avar_bounds_and_value(f, solver, i);	×
467	}
468	fputc('\n', f);	×
469	}	×
470
471	void print_simplex_allvars(FILE f, simplex_solver_t solver) {	×
472	uint32_t i, n;
473
474	n = num_arith_vars(&solver->vtbl);	×
475	for (i=0; i<n; i++) {	×
476	print_avar_full(f, solver, i);	×
477	}
478	fputc('\n', f);	×
479	}	×
480
481
482	void print_simplex_vars_summary(FILE f, simplex_solver_t solver) {	×
483	arith_vartable_t *table;
484	uint32_t i, n;
485	int32_t lb, ub;
486
487	table = &solver->vtbl;	×
488	n = num_arith_vars(table);	×
489	for (i=0; i<n; i++) {	×
490	lb = arith_var_lower_index(&solver->vtbl, i);	×
491	ub = arith_var_upper_index(&solver->vtbl, i);	×
492
493	if (matrix_is_basic_var(&solver->matrix, i)) {	×
494	fputs(" b ", f);	×
495	} else {
496	fputs(" ", f);	×
497	}
498	print_avar(f, table, i);	×
499	fputs(" = ", f);	×
500	xq_print(f, arith_var_value(&solver->vtbl, i));	×
501
502
503	if (lb >= 0 \|\| ub >= 0) {	×
504	fputs("\t", f);	×
505	if (lb >= 0) {	×
506	xq_print(f, solver->bstack.bound + lb);	×
507	fputs(" <= ", f);	×
508	}
509	print_avar(f, &solver->vtbl, i);	×
510	if (ub >= 0) {	×
511	fputs(" <= ", f);	×
512	xq_print(f, solver->bstack.bound + ub);	×
513	}
514	}
515
516	if (arith_var_has_eterm(table, i)) {	×
517	fputs("\t\teterm: ", f);	×
518	print_eterm_id(f, arith_var_eterm(table, i));	×
519	}
520	if (arith_var_def_is_poly(table, i)) {	×
521	fputs("\t\tdef: ", f);	×
522	print_avar_poly(f, table, arith_var_poly_def(table, i));	×
523	} else if (arith_var_def_is_product(table, i)) {	×
524	fputs("\t\tdef: ", f);	×
525	print_avar_product(f, table, arith_var_product_def(table, i));	×
526	}
527	fputc('\n', f);	×
528	}
529	fputc('\n', f);	×
530	}	×
531
532
533	void print_simplex_vardef(FILE f, simplex_solver_t solver, thvar_t v) {	×
534	arith_vartable_t *table;
535
536	table = &solver->vtbl;	×
537	print_avar(f, table, v);	×
538	if (arith_var_def_is_poly(table, v)) {	×
539	fputs(" := ", f);	×
540	print_avar_poly(f, table, arith_var_poly_def(table, v));	×
541	} else if (arith_var_def_is_product(table, v)) {	×
542	fputs(" := ", f);	×
543	print_avar_product(f, table, arith_var_product_def(table, v));	×
544	}
545	fputc('\n', f);	×
546	}	×
547
548	void print_simplex_var(FILE f, simplex_solver_t solver, thvar_t v) {	×
549	print_avar(f, &solver->vtbl, v);	×
550	}	×
551
552	void print_simplex_var_value(FILE f, simplex_solver_t solver, thvar_t v) {	×
553	xq_print(f, arith_var_value(&solver->vtbl, v));	×
554	}	×
555
556	void print_simplex_var_bounds(FILE f, simplex_solver_t solver, thvar_t v) {	×
557	print_avar_bounds(f, solver, v);	×
558	}	×
559
560	void print_simplex_atomdef(FILE f, simplex_solver_t solver, bvar_t v) {	×
561	void *atm;
562	arith_atom_t *a;
563	int32_t i;
564
565	atm = get_bvar_atom(solver->core, v);	×
566	i = arithatom_tagged_ptr2idx(atm);	×
567	a = arith_atom(&solver->atbl, i);	×
568	assert(a->boolvar == v);
569	print_bvar(f, v);	×
570	fputs(" := ", f);	×
571	print_arith_atom(f, &solver->vtbl, a);	×
572	fputc('\n', f);	×
573	}	×
574
575
576	void print_simplex_atom_of_literal(FILE f, simplex_solver_t solver, literal_t l) {	×
577	void *atm;
578	arith_atom_t *a;
579	bvar_t v;
580	int32_t i;
581
582	v = var_of(l);	×
583	assert(bvar_has_atom(solver->core, v));
584	atm = bvar_atom(solver->core, v);	×
585	assert(atom_tag(atm) == ARITH_ATM_TAG);
586	i = arithatom_tagged_ptr2idx(atm);	×
587	a = arith_atom(&solver->atbl, i);	×
588	assert(a->boolvar == v);
589
590	if (is_neg(l)) {	×
591	fputs("(not ", f);	×
592	}
593	print_arith_atom(f, &solver->vtbl, a);	×
594	if (is_neg(l)) {	×
595	fputc(')', f);	×
596	}
597	}	×
598
599
600	void print_simplex_buffer(FILE f, simplex_solver_t solver) {	×
601	poly_buffer_t *b;
602	uint32_t i, n;
603
604	b = &solver->buffer;	×
605	n = b->nterms;	×
606	if (n == 0) {	×
607	fputc('0', f);	×
608	} else {
609	for (i=0; i<n; i++) {	×
610	print_avar_monomial(f, &solver->vtbl, b->mono[i].var, &b->mono[i].coeff, i == 0);	×
611	}
612	}
613	}	×
614
615
616	void print_simplex_bound(FILE f, simplex_solver_t solver, uint32_t i) {	×
617	fprintf(f, "bound[%"PRIu32"]: ", i);	×
618	if (i < solver->bstack.top) {	×
619	print_avar(f, &solver->vtbl, solver->bstack.var[i]);	×
620	if (arith_tag_get_type(solver->bstack.tag[i]) == ATYPE_UB) {	×
621	fputs(" <= ", f);	×
622	} else {
623	fputs(" >= ", f);	×
624	}
625	xq_print(f, solver->bstack.bound + i);	×
626	} else {
627	fprintf(f, "<INVALID BOUND INDEX>");	×
628	}
629	}	×
630
631
632
633
634	/*
635	* FLAGS/BASE LEVEL
636	*/
637	static char *bool2string(bool x) {	×
638	return x ? "true" : "false";	×
639	}
640
641	void print_simplex_flags(FILE f, simplex_solver_t solver) {	×
642	fprintf(f, "base level: %"PRIu32"\n", solver->base_level);	×
643	fprintf(f, "decision level: %"PRIu32"\n", solver->decision_level);	×
644	fprintf(f, "matrix ready: %s\n", bool2string(solver->matrix_ready));	×
645	fprintf(f, "tableau ready: %s\n", bool2string(solver->tableau_ready));	×
646	fprintf(f, "save rows: %s\n", bool2string(solver->save_rows));	×
647	}	×
648
649
650
651	/*
652	* Print row in a simplified form: replace fixed variables by their value
653	*/
654	void print_simplex_reduced_row(FILE f, simplex_solver_t solver, row_t *row) {	×
655	arith_vartable_t *vtbl;
656	arith_bstack_t *bstack;
657	rational_t q;
658	uint32_t i, n;
659	thvar_t x;
660	bool first;
661	int32_t l, u;
662
663	vtbl = &solver->vtbl;	×
664	bstack = &solver->bstack;	×
665
666	// compute the constant
667	q_init(&q);	×
668	n = row->size;	×
669	for (i=0; i<n; i++) {	×
670	x = row->data[i].c_idx;	×
671	if (x >= 0) {	×
672	l = arith_var_lower_index(&solver->vtbl, x);	×
673	u = arith_var_upper_index(&solver->vtbl, x);	×
674	if (l >= 0 && u >= 0 && xq_eq(bstack->bound + l, bstack->bound + u)) {	×
675	// x is a a fixed variable
676	assert(xq_eq(bstack->bound + l, arith_var_value(vtbl, x)));
677	assert(xq_is_rational(arith_var_value(vtbl, x)));
678	q_addmul(&q, &row->data[i].coeff, &arith_var_value(vtbl, x)->main);	×
679	}
680	}
681	}
682
683	// print the non-constant monomials and q
684	first = true;	×
685	if (q_is_nonzero(&q)) {	×
686	print_avar_monomial(f, vtbl, const_idx, &q, first);	×
687	first = false;	×
688	}
689
690	for (i=0; i<n; i++) {	×
691	x = row->data[i].c_idx;	×
692	if (x >= 0) {	×
693	l = arith_var_lower_index(&solver->vtbl, x);	×
694	u = arith_var_upper_index(&solver->vtbl, x);	×
695	if (l < 0 \|\| u < 0 \|\| xq_neq(bstack->bound + l, bstack->bound + u)) {	×
696	// x is not a fixed variable
697	print_avar_monomial(f, vtbl, x, &row->data[i].coeff, first);	×
698	first = false;	×
699	}
700	}
701	}
702
703	if (first) {	×
704	// nothing printed so the row is empty
705	fputc('0', f);	×
706	}
707	fputs(" == 0", f);	×
708
709	q_clear(&q);	×
710	}	×
711
712
713
714	/*
715	* Variant of print_simplex_bounds
716	*/
717	void print_simplex_bounds2(FILE f, simplex_solver_t solver) {	×
718	uint32_t i, n;
719	int32_t lb, ub;
720
721	n = num_arith_vars(&solver->vtbl);	×
722	for (i=0; i<n; i++) {	×
723	lb = arith_var_lower_index(&solver->vtbl, i);	×
724	ub = arith_var_upper_index(&solver->vtbl, i);	×
725	if (lb >= 0 && ub >= 0) {	×
726	if (xq_neq(solver->bstack.bound + lb, solver->bstack.bound + ub)) {	×
727	fputs(" ", f);	×
728	xq_print(f, solver->bstack.bound + lb);	×
729	fprintf(f, " <= x_%"PRIu32" <= ", i);	×
730	xq_print(f, solver->bstack.bound + ub);	×
731	fputc('\n', f);	×
732	}
733	} else if (lb >= 0) {	×
734	fputs(" ", f);	×
735	xq_print(f, solver->bstack.bound + lb);	×
736	fprintf(f, " <= x_%"PRIu32"\n", i);	×
737	} else if (ub >= 0) {	×
738	fprintf(f, " x_%"PRIu32" <= ", i);	×
739	xq_print(f, solver->bstack.bound + ub);	×
740	fputc('\n', f);	×
741	}
742	}
743	}	×
744
745

SRI-CSL / yices2 / 3604430784

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous