diff options
author | Kenny Ballou <kballou@devnulllabs.io> | 2020-02-28 15:36:09 -0700 |
---|---|---|
committer | Kenny Ballou <kballou@devnulllabs.io> | 2020-02-28 15:36:09 -0700 |
commit | 76729f9670ba63a9146079b081bdb5b5ae0bbd3d (patch) | |
tree | e56830d65cac39a1bdadf6c4b8076d30fb559bb8 /casa/sat/SAT.C | |
download | casa-76729f9670ba63a9146079b081bdb5b5ae0bbd3d.tar.gz casa-76729f9670ba63a9146079b081bdb5b5ae0bbd3d.tar.xz |
CASA fork: initial commit
Snapshot from http://cse.unl.edu/~citportal/.
Diffstat (limited to 'casa/sat/SAT.C')
-rw-r--r-- | casa/sat/SAT.C | 81 |
1 files changed, 81 insertions, 0 deletions
diff --git a/casa/sat/SAT.C b/casa/sat/SAT.C new file mode 100644 index 0000000..161049b --- /dev/null +++ b/casa/sat/SAT.C @@ -0,0 +1,81 @@ +// 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/>. + + +// Other SAT solvers can be substituted by altering SAT.H and SAT.C. + +#include "sat/SAT.H" + +InputClause::InputClause() : + maxVariable(-1) {} + +InputClause::InputClause(Array<InputTerm>terms) : + maxVariable(-1) { + unsigned size = terms.getSize(); + for (unsigned i = 0; i < size; ++i) { + append(terms[i]); + } +} + +InputClause::InputClause(Array<unsigned>symbols) : + maxVariable(-1) { + unsigned size = symbols.getSize(); + for (unsigned i = 0; i < size; ++i) { + append(InputTerm(false, symbols[i])); + } +} + +InputClause::~InputClause() {} + +InputClause::operator vec<Lit>&() { + return literals; +} +InputClause::operator const vec<Lit>&() const { + return literals; +} + +void InputClause::clear(){ + literals.clear(); +} + +void InputClause::append(InputTerm term) { + int variable = term.getVariable(); + if (variable > maxVariable) { + maxVariable = variable; + } + literals.push(term.isNegated() ? ~Lit(variable) : Lit(variable)); +} + +void InputClause::undoAppend() { + literals.pop(); +} + +void SATSolver::reserve(int variables) { + while (variables >= solver.nVars()) { + solver.newVar(); + } +} + +void SATSolver::addClause(InputClause&clause) { + reserve(clause.getMaxVariable()); + solver.addClause(clause); +} + +bool SATSolver::operator()(const InputKnown&known) { + reserve(known.getMaxVariable()); + return solver.simplify() && solver.solve(known); +} |