summaryrefslogtreecommitdiff
path: root/casa/covering/space/CoveringArraySpace.C
blob: 6287bd35a76cb429f7cc9bcfa353a95bf7528cf7 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
// Copyright 2008, 2009 Brady J. Garvin

// This file is part of Covering Arrays by Simulated Annealing (CASA).

// CASA 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.

// CASA 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 CASA.  If not, see <http://www.gnu.org/licenses/>.


#include "covering/space/CoveringArraySpace.H"

CoveringArraySpace::CoveringArraySpace(unsigned strength, Options options) :
  strength(strength), options(options) {
  assert(strength <= options.getSize());
  for (unsigned i = options.getSize(); i--;) {
    // The clause atLeast requires that each column be filled.
    InputClause atLeast;
    for (unsigned
	   j = options.getFirstSymbol(i),
	   limit = options.getLastSymbol(i);
	 j <= limit;
	 ++j) {
      atLeast.append(InputTerm(false, j));
    }
    solver.addClause(atLeast);
    // The clauses atMost require that each pairing of symbols from an option
    // show at least one absence.
    for (unsigned
	   j = options.getFirstSymbol(i),
	   limit = options.getLastSymbol(i);
	 j <= limit; ++j) {
      for (unsigned k = j + 1; k <= limit; ++k) {
	InputClause atMost;
	atMost.append(InputTerm(true, j));
	atMost.append(InputTerm(true, k));
	solver.addClause(atMost);
      }
    }
  }
}

unsigned CoveringArraySpace::computeTargetCoverage() const {
  unsigned result = 0;
  for (Array<unsigned>columns = combinadic.begin(strength);
       columns[strength - 1] < options.getSize();
       combinadic.next(columns)) {
    // Initialization:
    Array<InputTerm>combination(columns.getSize());
    for (unsigned i = columns.getSize(); i--;) {
      combination[i] = InputTerm(false, options.getFirstSymbol(columns[i]));
    }
    // Body:
  loop:
    {
      InputKnown known(combination);
      if (solver(known)) {
	++result;
      }
    }
    // Advance:
    for (unsigned i = columns.getSize(); i--;) {
      unsigned next = combination[i].getVariable() + 1;
      if (next <= options.getLastSymbol(columns[i])) {
	combination[i] = InputTerm(false, next);
	goto loop;
      }
      combination[i] = InputTerm(false, options.getFirstSymbol(columns[i]));
    }
  }
  return result;
}