From: Hamed Gorjiara Date: Sat, 6 Oct 2018 00:51:54 +0000 (-0700) Subject: Fixing element/set types for the tuner ... X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=960d4357ffef8e4ed9de81b5438a76548d21ed03;p=Benchmarks_CSolver.git Fixing element/set types for the tuner ... --- diff --git a/hexiom/csolverHexiom.py b/hexiom/csolverHexiom.py index ee7f2020..8d07a96b 100755 --- a/hexiom/csolverHexiom.py +++ b/hexiom/csolverHexiom.py @@ -532,7 +532,7 @@ def generateElements(csolverlb, csolver, slot_range, value_range): for slot in range(slot_range[0], slot_range[-1]+1): s1 = [ i for i in range(value_range[0],value_range[-1]+2)] set1 = (c_long* len(s1))(*s1) - s1 = csolverlb.createSet(csolver, c_uint(11), set1, c_uint(len(s1))) + s1 = csolverlb.createSet(csolver, c_uint(1), set1, c_uint(len(s1))) e1 = csolverlb.getElementVar(csolver,s1) csolverlb.mustHaveValue(csolver, e1) elems.append(e1) @@ -540,7 +540,7 @@ def generateElements(csolverlb, csolver, slot_range, value_range): def lessThanValue(csolverlb, csolver, elems, m, n): e1 = elems[m] - e2 = csolverlb.getElementConst(csolver, c_uint(12), n) + e2 = csolverlb.getElementConst(csolver, c_uint(1), n) equals = csolverlb.createPredicateOperator(csolver, c_uint(ps.CompOp.SATC_LT)) inp = [e1,e2] inputs = (c_void_p*len(inp))(*inp) @@ -549,7 +549,7 @@ def lessThanValue(csolverlb, csolver, elems, m, n): def Placement(csolverlb, csolver, elems, m, n): e1 = elems[m] - e2 = csolverlb.getElementConst(csolver, c_uint(12), n) + e2 = csolverlb.getElementConst(csolver, c_uint(1), n) equals = csolverlb.createPredicateOperator(csolver, c_uint(ps.CompOp.SATC_EQUALS)) inp = [e1,e2] inputs = (c_void_p*len(inp))(*inp) @@ -558,7 +558,7 @@ def Placement(csolverlb, csolver, elems, m, n): def emptyValue(csolverlb, csolver, elems, m): e1 = elems[m] - e2 = csolverlb.getElementConst(csolver, c_uint(12), 7) + e2 = csolverlb.getElementConst(csolver, c_uint(1), 7) equals = csolverlb.createPredicateOperator(csolver, c_uint(ps.CompOp.SATC_EQUALS)) inp = [e1,e2] inputs = (c_void_p*len(inp))(*inp) @@ -566,7 +566,7 @@ def emptyValue(csolverlb, csolver, elems, m): return CSConstraint(csolverlb, csolver, b) def replaceWithElemConst(csolverlb, solver, elems, m, n): - elems[m] = csolverlb.getElementConst(solver, c_uint(10), n) + elems[m] = csolverlb.getElementConst(solver, c_uint(1), n) #### # Create clauses #### diff --git a/killerSudoku/csolversudoku.py b/killerSudoku/csolversudoku.py index 6e60ea29..cb603bed 100644 --- a/killerSudoku/csolversudoku.py +++ b/killerSudoku/csolversudoku.py @@ -88,7 +88,7 @@ def generateKillerSudokuConstraints(N, killerRules, serialize): inp = [elem, parElem] inputs = (c_void_p*len(inp))(*inp) parElem = csolverlb.applyFunction(solver, f1, inputs, len(inp), overflow); - esum = csolverlb.getElementConst(solver, c_uint(3), c_long(sumCage)) + esum = csolverlb.getElementConst(solver, c_uint(1), c_long(sumCage)) setSum = csolverlb.getElementRange(solver, esum) equals = csolverlb.createPredicateOperator(solver, c_uint(ps.CompOp.SATC_EQUALS)) inp = [parElem,esum] @@ -101,7 +101,7 @@ def generateKillerSudokuConstraints(N, killerRules, serialize): for cage in killerRules: sumCage = cage[0] if len(cage[1])==1: - problem[cage[1][0][0]][cage[1][0][1]] = csolverlb.getElementConst(solver, c_uint(7), c_long(sumCage)) + problem[cage[1][0][0]][cage[1][0][1]] = csolverlb.getElementConst(solver, c_uint(1), c_long(sumCage)) continue elements, domain = getElement(cage) generateSumConstraint(sumCage, elements, domain) diff --git a/nqueens/nqueens.cc b/nqueens/nqueens.cc index 43f9af6c..5865c860 100644 --- a/nqueens/nqueens.cc +++ b/nqueens/nqueens.cc @@ -384,7 +384,7 @@ void oneQueenInEachRow(CSolver* solver, vector &elems){ vector rowConstr; for(int j=0; jgetElementConst(3, (uint64_t) i); + Element* e2 = solver->getElementConst(1, (uint64_t) i); Element* in[] = {e1, e2}; BooleanEdge equals = solver->applyPredicate(eq, in, 2); rowConstr.push_back(equals); @@ -409,7 +409,7 @@ void diagonallyDifferentConstraint(CSolver *solver, int N, vector &ele int index = i-j; Element* e1 = elems[index]; // cout << "e" << e1 <<"=" << j << ", "; - Element* e2 = solver->getElementConst(2, (uint64_t) j); + Element* e2 = solver->getElementConst(1, (uint64_t) j); Element* in[] = {e1, e2}; BooleanEdge equals = solver->applyPredicate(eq, in, 2); diagonals.push_back(equals); @@ -425,7 +425,7 @@ void diagonallyDifferentConstraint(CSolver *solver, int N, vector &ele int index =N-1- (j-i); Element* e1 = elems[index]; // cout << "e" << e1 <<"=" << j << ", "; - Element* e2 = solver->getElementConst(2, (uint64_t) j); + Element* e2 = solver->getElementConst(1, (uint64_t) j); Element* in[] = {e1, e2}; BooleanEdge equals = solver->applyPredicate(eq, in, 2); diagonals.push_back(equals); @@ -449,7 +449,7 @@ void symmetryBreakingConstraint(CSolver *solver, int N, vector& elems) Predicate *lt = solver->createPredicateOperator(SATC_LT); int mid = N/2 + N%2; Element *e1x = elems[0]; - Element *e2x = solver->getElementConst(2, mid); + Element *e2x = solver->getElementConst(1, mid); Element *inputs [] = {e1x, e2x}; solver->addConstraint(solver->applyPredicate(lt, inputs, 2)); diff --git a/sudoku-csolver/argprocessor.py b/sudoku-csolver/argprocessor.py deleted file mode 100644 index 90a26269..00000000 --- a/sudoku-csolver/argprocessor.py +++ /dev/null @@ -1,21 +0,0 @@ - -import argparse -import sys - - -class AutoTunerArgParser: - def __init__(self): - self.parser = argparse.ArgumentParser(description='Parsing the output log of the CSolver auto tuner ...') - self.parser.add_argument('--file', '-f', metavar='out.log', type=str, nargs=1,help='output log of running the autotuner ...') - self.args = self.parser.parse_args() - - def getFileName(self): - return self.args.file[0] - -# def main(): -# print sys.argv -# argParser = KSudokuArgParser() -# -# -# if __name__ == "__main__": -# main() \ No newline at end of file diff --git a/sudoku-csolver/autotunerparser.py b/sudoku-csolver/autotunerparser.py deleted file mode 100644 index 0cb6b8dc..00000000 --- a/sudoku-csolver/autotunerparser.py +++ /dev/null @@ -1,64 +0,0 @@ -import argprocessor -import re - -configs = {"EXECTIME": "-", - "SATTIME":"-", - "PREPROCESS" : "-", - "ELEMENTOPT" : "-", - "ELEMENTOPTSETS" : "-", - "PROXYVARIABLE" : "-", - "#SubGraph" : "-", - "NODEENCODING" : "-", - "EDGEENCODING" : "-", - "NAIVEENCODER" :"-", - "ENCODINGGRAPHOPT" : "-" - } - -REGEXES = {"EXECTIME": "CSOLVER solve time: (.*)", - "SATTIME":"SAT Solving time: (.*)", - "PREPROCESS" : "Param PREPROCESS = (.*)range=\[0,1\]", - "ELEMENTOPT" : "Param ELEMENTOPT = (.*)range=\[0,1\]", - "ELEMENTOPTSETS" : "Param ELEMENTOPTSETS = (.*)range=\[0,1\]", - "PROXYVARIABLE" : "Param PROXYVARIABLE = (.*)range=\[1,5\]", - "#SubGraph" : "#SubGraph = (.*)", - "NODEENCODING" : "Param NODEENCODING = (.*)range=\[0,3\](.*)", - "EDGEENCODING" : "Param EDGEENCODING = (.*)range=\[0,2\](.*)", - "NAIVEENCODER" : "Param NAIVEENCODER = (.*)range=\[1,3\](.*)", - "ENCODINGGRAPHOPT" : "Param ENCODINGGRAPHOPT = (.*)range=\[0,1\]" - - } - -def printHeader(file): - global configs - mystr="" - for config in configs: - mystr+=str(config)+"," - print >>file, mystr - -def printConfig(file, data): - print data - mystr="" - for config in data: - mystr+=str(data[config])+"," - print >> file, mystr - -def main(): - global configs - argprocess = argprocessor.AutoTunerArgParser() - output = open("tuner.csv", "w") - printHeader(output) - with open(argprocess.getFileName()) as file: - for line in file: - if line.startswith("Mutating"): - printConfig(output,configs) - else : - for regex in REGEXES: - p = re.compile(REGEXES[regex]) - token = p.search(line) - if token is not None: - configs[regex] = re.findall("\d+\.?\d*", line)[0] - - print "Done with parsing " + argprocess.getFileName() - -if __name__ == "__main__": - main() \ No newline at end of file