}
void BooleanOrder::updateParents() {
- order->constraints.push(this);
+ order->addOrderConstraint(this);
}
BooleanPredicate::BooleanPredicate(Predicate *_predicate, Element **_inputs, uint _numInputs, BooleanEdge _undefinedStatus) :
void print();
Vector<BooleanOrder *> constraints;
OrderEncoding encoding;
+
void setOrderResolver(OrderResolver *_resolver) { ASSERT(encoding.resolver == NULL); encoding.resolver = _resolver;};
void initializeOrderElementsHashtable();
void addOrderConstraint(BooleanOrder *constraint);
void CSolver::replaceBooleanWithTrueNoRemove(BooleanEdge bexpr) {
updateMustValue(bexpr.getBoolean(), bexpr.isNegated() ? BV_MUSTBEFALSE : BV_MUSTBETRUE);
- ASSERT((bexpr->boolVal != BV_UNSAT ) || unsat);
+ ASSERT((bexpr->boolVal != BV_UNSAT) || unsat);
uint size = bexpr->parents.getSize();
for (uint i = 0; i < size; i++) {
#include "csolver.h"
void computePolarities(CSolver *This) {
- if(This->isUnSAT()){
+ if (This->isUnSAT()) {
return;
}
SetIteratorBooleanEdge *iterator = This->getConstraints();
}
void DecomposeOrderTransform::doTransform() {
- if(solver->isUnSAT())
+ if (solver->isUnSAT())
return;
HashsetOrder *orders = solver->getActiveOrders()->copy();
SetIteratorOrder *orderit = orders->iterator();
BooleanEdge benew = solver->orderConstraint(graph->getOrder(), source->getID(), node->getID());
updateEdgePolarity(benew, be);
if (solver->isTrue(benew))
- solver->replaceBooleanWithTrue(be);
+ solver->replaceBooleanWithTrue(be);
else if (solver->isFalse(benew))
- solver->replaceBooleanWithFalse(be);
+ solver->replaceBooleanWithFalse(be);
else
- solver->replaceBooleanWithBoolean(be, benew);
+ solver->replaceBooleanWithBoolean(be, benew);
}
dstnode->inEdges.reset();
delete inedgeit;
BooleanEdge benew = solver->orderConstraint(graph->getOrder(), node->getID(), sink->getID());
updateEdgePolarity(benew, be);
if (solver->isTrue(benew))
- solver->replaceBooleanWithTrue(be);
+ solver->replaceBooleanWithTrue(be);
else if (solver->isFalse(benew))
- solver->replaceBooleanWithFalse(be);
+ solver->replaceBooleanWithFalse(be);
else
- solver->replaceBooleanWithBoolean(be, benew);
+ solver->replaceBooleanWithBoolean(be, benew);
}
dstnode->outEdges.reset();
delete outedgeit;
ElementOpt::ElementOpt(CSolver *_solver)
: Transform(_solver),
- updateSets(false)
+ updateSets(false)
{
}
//Set once we know we are going to use it.
updateSets = solver->getTuner()->getTunable(ELEMENTOPTSETS, &onoff) == 1;
-
+
SetIteratorBooleanEdge *iterator = solver->getConstraints();
while (iterator->hasNext()) {
BooleanEdge constraint = iterator->next();
}
void IntegerEncodingTransform::doTransform() {
- if(solver->isUnSAT()){
+ if (solver->isUnSAT()) {
return;
}
HashsetOrder *orders = solver->getActiveOrders()->copy();
}
void VarOrderingOpt::doTransform() {
- if(solver->isUnSAT()){
+ if (solver->isUnSAT()) {
return;
}
BooleanVarOrdering direction = (BooleanVarOrdering)solver->getTuner()->getTunable(VARIABLEORDER, &boolVarOrderingDesc);
}
void SATEncoder::encodeAllSATEncoder(CSolver *csolver) {
- if(csolver->isUnSAT()){
+ if (csolver->isUnSAT()) {
return;
}
SetIteratorBooleanEdge *iterator = csolver->getConstraints();
type *array; \
}; \
typedef struct Vector ## name Vector ## name; \
- Vector ## name * allocVector ## name(uint capacity); \
- Vector ## name * allocDefVector ## name(); \
- Vector ## name * allocVectorArray ## name(uint capacity, type * array); \
+ Vector ## name *allocVector ## name(uint capacity); \
+ Vector ## name *allocDefVector ## name(); \
+ Vector ## name *allocVectorArray ## name(uint capacity, type * array); \
void pushVector ## name(Vector ## name * vector, type item); \
type lastVector ## name(Vector ## name * vector); \
void popVector ## name(Vector ## name * vector); \
void initVectorArray ## name(Vector ## name * vector, uint capacity, type * array);
#define VectorImpl(name, type, defcap) \
- Vector ## name * allocDefVector ## name() { \
+ Vector ## name *allocDefVector ## name() { \
return allocVector ## name(defcap); \
} \
- Vector ## name * allocVector ## name(uint capacity) { \
- Vector ## name * tmp = (Vector ## name *)ourmalloc(sizeof(Vector ## name)); \
+ Vector ## name *allocVector ## name(uint capacity) { \
+ Vector ## name *tmp = (Vector ## name *)ourmalloc(sizeof(Vector ## name)); \
tmp->size = 0; \
tmp->capacity = capacity; \
tmp->array = (type *) ourmalloc(sizeof(type) * capacity); \
return tmp; \
} \
- Vector ## name * allocVectorArray ## name(uint capacity, type * array) { \
- Vector ## name * tmp = allocVector ## name(capacity); \
+ Vector ## name *allocVectorArray ## name(uint capacity, type * array) { \
+ Vector ## name *tmp = allocVector ## name(capacity); \
tmp->size = capacity; \
memcpy(tmp->array, array, capacity * sizeof(type)); \
return tmp; \
#include <strings.h>
void naiveEncodingDecision(CSolver *This) {
- if(This->isUnSAT()){
+ if (This->isUnSAT()) {
return;
}
SetIteratorBooleanEdge *iterator = This->getConstraints();
#define ALLOYFILENAME "satune.als"
#define ALLOYSOLUTIONFILE "solution.sol"
-AlloyInterpreter::AlloyInterpreter(CSolver *_solver):
- Interpreter(_solver)
+AlloyInterpreter::AlloyInterpreter(CSolver *_solver) :
+ Interpreter(_solver)
{
output.open(ALLOYFILENAME);
- if(!output.is_open()){
+ if (!output.is_open()) {
model_print("AlloyEnc:Error in opening the dump file satune.als\n");
exit(-1);
}
}
-AlloyInterpreter::~AlloyInterpreter(){
- if(output.is_open()){
+AlloyInterpreter::~AlloyInterpreter() {
+ if (output.is_open()) {
output.close();
}
}
-ValuedSignature *AlloyInterpreter::getBooleanSignature(uint id){
+ValuedSignature *AlloyInterpreter::getBooleanSignature(uint id) {
return new AlloyBoolSig(id);
}
-ValuedSignature *AlloyInterpreter::getElementSignature(uint id, Signature *ssig){
+ValuedSignature *AlloyInterpreter::getElementSignature(uint id, Signature *ssig) {
return new AlloyElementSig(id, ssig);
}
-Signature *AlloyInterpreter::getSetSignature(uint id, Set *set){
+Signature *AlloyInterpreter::getSetSignature(uint id, Set *set) {
return new AlloySetSig(id, set);
}
-void AlloyInterpreter::dumpAllConstraints(Vector<char *> &facts){
+void AlloyInterpreter::dumpAllConstraints(Vector<char *> &facts) {
output << "fact {" << endl;
- for(uint i=0; i< facts.getSize(); i++){
+ for (uint i = 0; i < facts.getSize(); i++) {
char *cstr = facts.get(i);
writeToFile(cstr);
}
}
-int AlloyInterpreter::getResult(){
+int AlloyInterpreter::getResult() {
ifstream input(ALLOYSOLUTIONFILE, ios::in);
string line;
- while(getline(input, line)){
- if(line.find("Unsatisfiable.")== 0){
+ while (getline(input, line)) {
+ if (line.find("Unsatisfiable.") == 0) {
return IS_UNSAT;
}
- if(line.find("univ") == 0){
+ if (line.find("univ") == 0) {
continue;
}
- if(line.find("this/AbsBool<:value") == 0 || line.find("this/AbsElement<:value=") == 0){
+ if (line.find("this/AbsBool<:value") == 0 || line.find("this/AbsElement<:value=") == 0) {
const char delim [2] = ",";
- char cline [line.size()+1];
+ char cline [line.size() + 1];
strcpy ( cline, line.c_str() );
char *token = strtok(cline, delim);
- while( token != NULL ) {
+ while ( token != NULL ) {
uint i1, i2, i3;
- if (3 == sscanf(token,"%*[^0123456789]%u%*[^0123456789]%d%*[^0123456789]%u", &i1, &i2, &i3)){
+ if (3 == sscanf(token,"%*[^0123456789]%u%*[^0123456789]%d%*[^0123456789]%u", &i1, &i2, &i3)) {
model_print("Signature%u = %u\n", i1, i3);
sigEnc.setValue(i1, i3);
}
}
-int AlloyInterpreter::getAlloyIntScope(){
+int AlloyInterpreter::getAlloyIntScope() {
double mylog = log2(sigEnc.getMaxValue() + 1);
- return floor(mylog) == mylog ? (int)mylog + 1: (int)mylog + 2;
+ return floor(mylog) == mylog ? (int)mylog + 1 : (int)mylog + 2;
}
-void AlloyInterpreter::dumpFooter(){
+void AlloyInterpreter::dumpFooter() {
output << "pred show {}" << endl;
output << "run show for " << getAlloyIntScope() << " int" << endl;
}
-void AlloyInterpreter::dumpHeader(){
+void AlloyInterpreter::dumpHeader() {
output << "open util/integer" << endl;
}
-void AlloyInterpreter::compileRunCommand(char * command, size_t size){
+void AlloyInterpreter::compileRunCommand(char *command, size_t size) {
model_print("Calling Alloy...\n");
snprintf(command, size, "./run.sh timeout %u java -Xmx10000m edu.mit.csail.sdg.alloy4whole.ExampleAlloyCompilerNoViz %s > %s", getTimeout(), ALLOYFILENAME, ALLOYSOLUTIONFILE);
}
-string AlloyInterpreter::negateConstraint(string constr){
+string AlloyInterpreter::negateConstraint(string constr) {
return "not ( " + constr + " )";
}
-string AlloyInterpreter::encodeBooleanLogic( BooleanLogic *bl){
+string AlloyInterpreter::encodeBooleanLogic( BooleanLogic *bl) {
uint size = bl->inputs.getSize();
string array[size];
for (uint i = 0; i < size; i++)
array[i] = encodeConstraint(bl->inputs.get(i));
string op;
- switch (bl->op){
- case SATC_OR:
- op = " or ";
- break;
- case SATC_AND:
- op = " and ";
- break;
- case SATC_NOT:
- op = " not ";
- break;
- case SATC_IFF:
- op = " iff ";
- break;
- case SATC_IMPLIES:
- op = " implies ";
- break;
- case SATC_XOR:
- default:
- ASSERT(0);
+ switch (bl->op) {
+ case SATC_OR:
+ op = " or ";
+ break;
+ case SATC_AND:
+ op = " and ";
+ break;
+ case SATC_NOT:
+ op = " not ";
+ break;
+ case SATC_IFF:
+ op = " iff ";
+ break;
+ case SATC_IMPLIES:
+ op = " implies ";
+ break;
+ case SATC_XOR:
+ default:
+ ASSERT(0);
}
switch (bl->op) {
- case SATC_OR:
- case SATC_AND:{
- ASSERT(size >= 2);
- string res = "( ";
- res += array[0];
- for( uint i=1; i< size; i++){
- res += op + array[i];
- }
- res += " )";
- return res;
- }
- case SATC_NOT:{
- return "not ( " + array[0] + " )";
+ case SATC_OR:
+ case SATC_AND: {
+ ASSERT(size >= 2);
+ string res = "( ";
+ res += array[0];
+ for ( uint i = 1; i < size; i++) {
+ res += op + array[i];
}
- case SATC_IMPLIES:
- case SATC_IFF:
- return "( " + array[0] + op + array[1] + " )";
- case SATC_XOR:
- default:
- ASSERT(0);
+ res += " )";
+ return res;
+ }
+ case SATC_NOT: {
+ return "not ( " + array[0] + " )";
+ }
+ case SATC_IMPLIES:
+ case SATC_IFF:
+ return "( " + array[0] + op + array[1] + " )";
+ case SATC_XOR:
+ default:
+ ASSERT(0);
}
}
-string AlloyInterpreter::encodeBooleanVar( BooleanVar *bv){
- ValuedSignature * boolSig = sigEnc.getBooleanSignature(bv);
+string AlloyInterpreter::encodeBooleanVar( BooleanVar *bv) {
+ ValuedSignature *boolSig = sigEnc.getBooleanSignature(bv);
return *boolSig + " = 1";
}
-string AlloyInterpreter::processElementFunction(ElementFunction* elemFunc, ValuedSignature *signature){
+string AlloyInterpreter::processElementFunction(ElementFunction *elemFunc, ValuedSignature *signature) {
FunctionOperator *function = (FunctionOperator *) elemFunc->getFunction();
uint numDomains = elemFunc->inputs.getSize();
ASSERT(numDomains > 1);
for (uint i = 0; i < numDomains; i++) {
Element *elem = elemFunc->inputs.get(i);
inputs[i] = sigEnc.getElementSignature(elem);
- if(elem->type == ELEMFUNCRETURN){
+ if (elem->type == ELEMFUNCRETURN) {
result += processElementFunction((ElementFunction *) elem, inputs[i]);
}
}
string op;
- switch(function->op){
- case SATC_ADD:
- op = ".add";
- break;
- case SATC_SUB:
- op = ".sub";
- break;
- default:
- ASSERT(0);
+ switch (function->op) {
+ case SATC_ADD:
+ op = ".add";
+ break;
+ case SATC_SUB:
+ op = ".sub";
+ break;
+ default:
+ ASSERT(0);
}
result += *signature + " = " + *inputs[0];
for (uint i = 1; i < numDomains; i++) {
- result += op + "["+ *inputs[i] +"]";
+ result += op + "[" + *inputs[i] + "]";
}
result += "\n";
return result;
}
-string AlloyInterpreter::operatorPredicateConstraint(CompOp op, ValuedSignature *elemSig1, ValuedSignature *elemSig2){
+string AlloyInterpreter::operatorPredicateConstraint(CompOp op, ValuedSignature *elemSig1, ValuedSignature *elemSig2) {
switch (op) {
- case SATC_EQUALS:
- return *elemSig1 + " = " + *elemSig2;
- case SATC_LT:
- return *elemSig1 + " < " + *elemSig2;
- case SATC_GT:
- return *elemSig1 + " > " + *elemSig2;
- default:
- ASSERT(0);
+ case SATC_EQUALS:
+ return *elemSig1 + " = " + *elemSig2;
+ case SATC_LT:
+ return *elemSig1 + " < " + *elemSig2;
+ case SATC_GT:
+ return *elemSig1 + " > " + *elemSig2;
+ default:
+ ASSERT(0);
}
}
#include <iostream>
#include <fstream>
-class AlloyInterpreter: public Interpreter{
+class AlloyInterpreter : public Interpreter {
public:
AlloyInterpreter(CSolver *solver);
virtual ValuedSignature *getBooleanSignature(uint id);
virtual void dumpFooter();
virtual void dumpHeader();
int getAlloyIntScope();
- virtual void compileRunCommand(char * command , size_t size);
+ virtual void compileRunCommand(char *command, size_t size);
virtual int getResult();
virtual void dumpAllConstraints(Vector<char *> &facts);
virtual string negateConstraint(string constr);
bool AlloySetSig::encodeAbs = true;
bool AlloyElementSig::encodeAbs = true;
-AlloyBoolSig::AlloyBoolSig(uint id):
+AlloyBoolSig::AlloyBoolSig(uint id) :
ValuedSignature(id)
{
}
-string AlloyBoolSig::toString() const{
+string AlloyBoolSig::toString() const {
return "Boolean" + to_string(id) + ".value";
}
-string AlloyBoolSig::getSignature() const{
+string AlloyBoolSig::getSignature() const {
string str;
- if(encodeAbs){
+ if (encodeAbs) {
encodeAbs = false;
str += getAbsSignature();
}
return str;
}
-string AlloyBoolSig::getAbsSignature() const{
+string AlloyBoolSig::getAbsSignature() const {
string str;
- if(AlloySetSig::encodeAbs){
+ if (AlloySetSig::encodeAbs) {
AlloySetSig::encodeAbs = false;
str += "abstract sig AbsSet {\
domain: set Int\
}\n";
}
- str +="one sig BooleanSet extends AbsSet {}{\n\
+ str += "one sig BooleanSet extends AbsSet {}{\n\
domain = 0 + 1 \n\
}\n\
abstract sig AbsBool {\
return str;
}
-AlloyElementSig::AlloyElementSig(uint id, Signature *_ssig):
+AlloyElementSig::AlloyElementSig(uint id, Signature *_ssig) :
ValuedSignature(id),
ssig(_ssig)
{
}
-string AlloyElementSig::toString() const{
+string AlloyElementSig::toString() const {
return "Element" + to_string(id) + ".value";
}
-string AlloyElementSig::getSignature() const{
+string AlloyElementSig::getSignature() const {
string str;
- if(encodeAbs){
+ if (encodeAbs) {
encodeAbs = false;
str += getAbsSignature();
}
return str;
}
-string AlloyElementSig::getAbsSignature() const{
+string AlloyElementSig::getAbsSignature() const {
return "abstract sig AbsElement {\n\
value: Int\n\
}\n";
-
+
}
-AlloySetSig::AlloySetSig(uint id, Set *set): Signature(id){
+AlloySetSig::AlloySetSig(uint id, Set *set) : Signature(id) {
ASSERT(set->getSize() > 0);
domain = to_string(set->getElement(0));
- for(uint i=1; i< set->getSize(); i++){
+ for (uint i = 1; i < set->getSize(); i++) {
domain += " + " + to_string(set->getElement(i));
}
}
-string AlloySetSig::toString() const{
+string AlloySetSig::toString() const {
return "Set" + to_string(id) + ".domain";
}
-string AlloySetSig::getSignature() const{
+string AlloySetSig::getSignature() const {
string str;
- if(encodeAbs){
+ if (encodeAbs) {
encodeAbs = false;
str += getAbsSignature();
}
return str;
}
-string AlloySetSig::getAbsSignature() const{
+string AlloySetSig::getAbsSignature() const {
return "abstract sig AbsSet {\n\
domain: set Int\n\
}\n";
-
+
}
#include "classlist.h"
using namespace std;
-class AlloyBoolSig: public ValuedSignature{
+class AlloyBoolSig : public ValuedSignature {
public:
AlloyBoolSig(uint id);
- virtual ~AlloyBoolSig(){}
+ virtual ~AlloyBoolSig() {}
virtual string toString() const;
virtual string getAbsSignature() const;
virtual string getSignature() const;
static bool encodeAbs;
};
-class AlloySetSig: public Signature{
+class AlloySetSig : public Signature {
public:
AlloySetSig(uint id, Set *set);
- virtual ~AlloySetSig(){}
+ virtual ~AlloySetSig() {}
virtual string toString() const;
virtual string getAbsSignature() const;
virtual string getSignature() const;
string domain;
};
-class AlloyElementSig: public ValuedSignature{
+class AlloyElementSig : public ValuedSignature {
public:
AlloyElementSig(uint id, Signature *ssig);
- virtual ~AlloyElementSig(){}
+ virtual ~AlloyElementSig() {}
virtual string toString() const;
virtual string getAbsSignature() const;
virtual string getSignature() const;
using namespace std;
-Interpreter::Interpreter(CSolver *_solver):
+Interpreter::Interpreter(CSolver *_solver) :
csolver(_solver),
sigEnc(this)
{
}
-Interpreter::~Interpreter(){
+Interpreter::~Interpreter() {
}
-void Interpreter::encode(){
+void Interpreter::encode() {
dumpHeader();
SetIteratorBooleanEdge *iterator = csolver->getConstraints();
Vector<char *> facts;
- while(iterator->hasNext()){
+ while (iterator->hasNext()) {
BooleanEdge constraint = iterator->next();
string constr = encodeConstraint(constraint);
- char *cstr = new char [constr.length()+1];
+ char *cstr = new char [constr.length() + 1];
strcpy (cstr, constr.c_str());
facts.push(cstr);
}
dumpAllConstraints(facts);
- for(uint i=0; i< facts.getSize(); i++){
+ for (uint i = 0; i < facts.getSize(); i++) {
char *cstr = facts.get(i);
delete[] cstr;
}
delete iterator;
}
-uint Interpreter::getTimeout(){
- uint timeout =csolver->getSatSolverTimeout();
- return timeout == (uint)NOTIMEOUT? 1000: timeout;
+uint Interpreter::getTimeout() {
+ uint timeout = csolver->getSatSolverTimeout();
+ return timeout == (uint)NOTIMEOUT ? 1000 : timeout;
}
-int Interpreter::solve(){
+int Interpreter::solve() {
dumpFooter();
int result = IS_INDETER;
char buffer [512];
- if( output.is_open()){
+ if ( output.is_open()) {
output.close();
}
compileRunCommand(buffer, sizeof(buffer));
int status = system(buffer);
- if (status == 0 || status == 512 ) { //For some unknown reason, SMTSat returns 512 when the problem successfully gets solved
+ if (status == 0 || status == 512 ) {//For some unknown reason, SMTSat returns 512 when the problem successfully gets solved
//Read data in from results file
result = getResult();
} else {
return result;
}
-string Interpreter::encodeConstraint(BooleanEdge c){
+string Interpreter::encodeConstraint(BooleanEdge c) {
Boolean *constraint = c.getBoolean();
string res;
- switch(constraint->type){
- case LOGICOP:{
- res = encodeBooleanLogic((BooleanLogic *) constraint);
- break;
- }
- case PREDICATEOP:{
- res = encodePredicate((BooleanPredicate *) constraint);
- break;
- }
- case BOOLEANVAR:{
- res = encodeBooleanVar( (BooleanVar *) constraint);
- break;
- }
- default:
- ASSERT(0);
+ switch (constraint->type) {
+ case LOGICOP: {
+ res = encodeBooleanLogic((BooleanLogic *) constraint);
+ break;
}
- if(c.isNegated()){
+ case PREDICATEOP: {
+ res = encodePredicate((BooleanPredicate *) constraint);
+ break;
+ }
+ case BOOLEANVAR: {
+ res = encodeBooleanVar( (BooleanVar *) constraint);
+ break;
+ }
+ default:
+ ASSERT(0);
+ }
+ if (c.isNegated()) {
return negateConstraint(res);
}
return res;
}
-string Interpreter::encodePredicate( BooleanPredicate *bp){
+string Interpreter::encodePredicate( BooleanPredicate *bp) {
switch (bp->predicate->type) {
- case TABLEPRED:
- ASSERT(0);
- case OPERATORPRED:
- return encodeOperatorPredicate(bp);
- default:
- ASSERT(0);
+ case TABLEPRED:
+ ASSERT(0);
+ case OPERATORPRED:
+ return encodeOperatorPredicate(bp);
+ default:
+ ASSERT(0);
}
}
-string Interpreter::encodeOperatorPredicate(BooleanPredicate *constraint){
+string Interpreter::encodeOperatorPredicate(BooleanPredicate *constraint) {
PredicateOperator *predicate = (PredicateOperator *) constraint->predicate;
ASSERT(constraint->inputs.getSize() == 2);
string str;
Element *elem0 = constraint->inputs.get(0);
ASSERT(elem0->type == ELEMSET || elem0->type == ELEMFUNCRETURN || elem0->type == ELEMCONST);
ValuedSignature *elemSig1 = sigEnc.getElementSignature(elem0);
- if(elem0->type == ELEMFUNCRETURN){
+ if (elem0->type == ELEMFUNCRETURN) {
str += processElementFunction((ElementFunction *) elem0, elemSig1);
}
Element *elem1 = constraint->inputs.get(1);
ASSERT(elem1->type == ELEMSET || elem1->type == ELEMFUNCRETURN || elem1->type == ELEMCONST);
ValuedSignature *elemSig2 = sigEnc.getElementSignature(elem1);
- if(elem1->type == ELEMFUNCRETURN){
+ if (elem1->type == ELEMFUNCRETURN) {
str += processElementFunction((ElementFunction *) elem1, elemSig2);
}
str += operatorPredicateConstraint(predicate->getOp(), elemSig1, elemSig2);
return str;
}
-void Interpreter::writeToFile(string str){
- if(!str.empty()){
+void Interpreter::writeToFile(string str) {
+ if (!str.empty()) {
output << str << endl;
}
}
-bool Interpreter::getBooleanValue(Boolean *b){
+bool Interpreter::getBooleanValue(Boolean *b) {
return (bool)sigEnc.getValue(b);
}
-uint64_t Interpreter::getValue(Element * element){
+uint64_t Interpreter::getValue(Element *element) {
return (uint64_t)sigEnc.getValue(element);
}
#include <fstream>
using namespace std;
-class Interpreter{
+class Interpreter {
public:
Interpreter(CSolver *solver);
void encode();
virtual void dumpFooter() = 0;
virtual void dumpHeader() = 0;
uint getTimeout();
- virtual void compileRunCommand(char * command, size_t size) = 0;
+ virtual void compileRunCommand(char *command, size_t size) = 0;
string encodeConstraint(BooleanEdge constraint);
virtual int getResult() = 0;
virtual string negateConstraint(string constr) = 0;
* and open the template in the editor.
*/
-/*
+/*
* File: smtsolvers.cc
* Author: hamed
- *
+ *
* Created on February 21, 2019, 12:26 PM
*/
#include "mathsatinterpreter.h"
#include "solver_interface.h"
-MathSATInterpreter::MathSATInterpreter(CSolver *solver):
+MathSATInterpreter::MathSATInterpreter(CSolver *solver) :
SMTInterpreter(solver)
-{
+{
}
-void MathSATInterpreter::compileRunCommand(char * command , size_t size){
+void MathSATInterpreter::compileRunCommand(char *command, size_t size) {
model_print("Calling MathSAT...\n");
snprintf(command, size, "./run.sh timeout %u mathsat -model %s > %s", getTimeout(), SMTFILENAME, SMTSOLUTIONFILE);
}
-MathSATInterpreter::~MathSATInterpreter(){
+MathSATInterpreter::~MathSATInterpreter() {
}
-int MathSATInterpreter::getResult(){
+int MathSATInterpreter::getResult() {
ifstream input(SMTSOLUTIONFILE, ios::in);
string line;
- while(getline(input, line)){
- if(line.find("unsat")!= line.npos){
+ while (getline(input, line)) {
+ if (line.find("unsat") != line.npos) {
return IS_UNSAT;
}
- if(line.find("(") != line.npos){
- char cline [line.size()+1];
+ if (line.find("(") != line.npos) {
+ char cline [line.size() + 1];
strcpy ( cline, line.c_str() );
char valuestr [512];
uint id;
- if (2 == sscanf(cline,"%*[^0123456789]%u %s", &id, valuestr)){
+ if (2 == sscanf(cline,"%*[^0123456789]%u %s", &id, valuestr)) {
uint value;
- if (strcmp (valuestr, "true)") == 0 ){
- value =1;
- }else if (strcmp(valuestr, "false)") == 0){
+ if (strcmp (valuestr, "true)") == 0 ) {
+ value = 1;
+ } else if (strcmp(valuestr, "false)") == 0) {
value = 0;
- }else {
+ } else {
ASSERT(2 == sscanf(cline, "%*[^0123456789]%u%*[^0123456789]%u", &id, &value));
}
* and open the template in the editor.
*/
-/*
+/*
* File: mathsatinterpreter.h
* Author: hamed
*
#include "smtinterpreter.h"
-class MathSATInterpreter: public SMTInterpreter{
+class MathSATInterpreter : public SMTInterpreter {
public:
MathSATInterpreter(CSolver *solver);
virtual ~MathSATInterpreter();
protected:
- virtual void compileRunCommand(char * command , size_t size);
+ virtual void compileRunCommand(char *command, size_t size);
virtual int getResult();
};
-#endif /* SMTSOLVERS_H */
+#endif/* SMTSOLVERS_H */
#include "signature.h"
#include "set.h"
-ValuedSignature::ValuedSignature(uint id):
- Signature(id),
- value(-1)
+ValuedSignature::ValuedSignature(uint id) :
+ Signature(id),
+ value(-1)
{
}
-int ValuedSignature::getValue(){
+int ValuedSignature::getValue() {
ASSERT(value != -1);
return value;
}
-string Signature::operator+(const string& str){
+string Signature::operator+(const string &str) {
return toString() + str;
}
-string operator+(const string& str, const Signature& sig){
- return str + sig.toString();
+string operator+(const string &str, const Signature &sig) {
+ return str + sig.toString();
}
#include "classlist.h"
using namespace std;
-class Signature{
+class Signature {
public:
- Signature(uint _id):id(_id){}
- string operator+(const string& s);
+ Signature(uint _id) : id(_id) {}
+ string operator+(const string &s);
virtual string toString() const = 0;
- virtual string getAbsSignature() const =0;
- virtual string getSignature() const =0;
- virtual ~Signature(){}
+ virtual string getAbsSignature() const = 0;
+ virtual string getSignature() const = 0;
+ virtual ~Signature() {}
protected:
uint id;
};
-class ValuedSignature: public Signature{
+class ValuedSignature : public Signature {
public:
ValuedSignature(uint id);
int getValue();
- void setValue(int v){value = v;}
+ void setValue(int v) {value = v;}
protected:
int value;
};
-string operator+(const string& str, const Signature& sig);
+string operator+(const string &str, const Signature &sig);
#endif
#include "signature.h"
#include "interpreter.h"
-SignatureEnc::SignatureEnc(Interpreter *inter):
+SignatureEnc::SignatureEnc(Interpreter *inter) :
interpreter(inter),
maxValue(0)
{
}
-SignatureEnc::~SignatureEnc(){
- for(uint i=0; i<signatures.getSize(); i++){
+SignatureEnc::~SignatureEnc() {
+ for (uint i = 0; i < signatures.getSize(); i++) {
Signature *s = signatures.get(i);
delete s;
}
}
-void SignatureEnc::updateMaxValue(Set *set){
- for(uint i=0; i< set->getSize(); i++){
- if(set->getElement(i) > maxValue){
+void SignatureEnc::updateMaxValue(Set *set) {
+ for (uint i = 0; i < set->getSize(); i++) {
+ if (set->getElement(i) > maxValue) {
maxValue = set->getElement(i);
}
}
}
-ValuedSignature *SignatureEnc::getBooleanSignature(Boolean *bvar){
+ValuedSignature *SignatureEnc::getBooleanSignature(Boolean *bvar) {
ValuedSignature *bsig = (ValuedSignature *)encoded.get((void *)bvar);
- if(bsig == NULL){
+ if (bsig == NULL) {
bsig = interpreter->getBooleanSignature(getUniqueSigID());
encoded.put(bvar, bsig);
signatures.push(bsig);
return bsig;
}
-ValuedSignature *SignatureEnc::getElementSignature(Element *element){
+ValuedSignature *SignatureEnc::getElementSignature(Element *element) {
ValuedSignature *esig = (ValuedSignature *)encoded.get((void *)element);
- if(esig == NULL){
+ if (esig == NULL) {
Set *set = element->getRange();
Signature *ssig = (Signature *)encoded.get((void *)set);
- if(ssig == NULL){
+ if (ssig == NULL) {
ssig = interpreter->getSetSignature(getUniqueSigID(), set);
encoded.put(set, ssig);
signatures.push(ssig);
return esig;
}
-void SignatureEnc::setValue(uint id, uint value){
+void SignatureEnc::setValue(uint id, uint value) {
ValuedSignature *sig = getValuedSignature(id);
ASSERT(sig != NULL);
sig->setValue(value);
}
-int SignatureEnc::getValue(void *astnode){
+int SignatureEnc::getValue(void *astnode) {
ValuedSignature *sig = (ValuedSignature *)encoded.get(astnode);
ASSERT(sig != NULL);
return sig->getValue();
ValuedSignature *getElementSignature(Element *element);
ValuedSignature *getBooleanSignature(Boolean *bvar);
int getValue(void *astnode);
- uint64_t getMaxValue(){ return maxValue;}
+ uint64_t getMaxValue() { return maxValue;}
private:
- ValuedSignature *getValuedSignature(uint uniqueID){return (ValuedSignature*)signatures.get(uniqueID-1);}
- uint getUniqueSigID(){return signatures.getSize() +1;}
+ ValuedSignature *getValuedSignature(uint uniqueID) {return (ValuedSignature *)signatures.get(uniqueID - 1);}
+ uint getUniqueSigID() {return signatures.getSize() + 1;}
void updateMaxValue(Set *set);
CloneMap encoded;
- Vector<Signature*> signatures;
+ Vector<Signature *> signatures;
Interpreter *interpreter;
uint64_t maxValue;
};
using namespace std;
-SMTInterpreter::SMTInterpreter(CSolver *_solver):
- Interpreter(_solver)
+SMTInterpreter::SMTInterpreter(CSolver *_solver) :
+ Interpreter(_solver)
{
output.open(SMTFILENAME);
- if(!output.is_open()){
+ if (!output.is_open()) {
model_print("AlloyEnc:Error in opening the dump file satune.smt\n");
exit(-1);
}
}
-SMTInterpreter::~SMTInterpreter(){
- if(output.is_open()){
+SMTInterpreter::~SMTInterpreter() {
+ if (output.is_open()) {
output.close();
}
}
-ValuedSignature *SMTInterpreter::getBooleanSignature(uint id){
+ValuedSignature *SMTInterpreter::getBooleanSignature(uint id) {
return new SMTBoolSig(id);
}
-ValuedSignature *SMTInterpreter::getElementSignature(uint id, Signature *ssig){
+ValuedSignature *SMTInterpreter::getElementSignature(uint id, Signature *ssig) {
return new SMTElementSig(id, (SMTSetSig *)ssig);
}
-Signature *SMTInterpreter::getSetSignature(uint id, Set *set){
+Signature *SMTInterpreter::getSetSignature(uint id, Set *set) {
return new SMTSetSig(id, set);
}
-void SMTInterpreter::dumpAllConstraints(Vector<char *> &facts){
- for(uint i=0; i< facts.getSize(); i++){
+void SMTInterpreter::dumpAllConstraints(Vector<char *> &facts) {
+ for (uint i = 0; i < facts.getSize(); i++) {
char *cstr = facts.get(i);
writeToFile("(assert " + string(cstr) + ")");
}
}
-void SMTInterpreter::extractValue(char *idline, char *valueline){
+void SMTInterpreter::extractValue(char *idline, char *valueline) {
uint id;
- if (1 == sscanf(idline,"%*[^0123456789]%u", &id)){
+ if (1 == sscanf(idline,"%*[^0123456789]%u", &id)) {
char valuestr [512];
ASSERT(1 == sscanf(valueline,"%s)", valuestr));
uint value;
- if (strcmp (valuestr, "true)") == 0 ){
- value =1;
- }else if (strcmp(valuestr, "false)") == 0){
+ if (strcmp (valuestr, "true)") == 0 ) {
+ value = 1;
+ } else if (strcmp(valuestr, "false)") == 0) {
value = 0;
- }else {
+ } else {
ASSERT(1 == sscanf(valueline, "%*[^0123456789]%u", &value));
}
}
}
-int SMTInterpreter::getResult(){
+int SMTInterpreter::getResult() {
ifstream input(SMTSOLUTIONFILE, ios::in);
string line;
- while(getline(input, line)){
- if(line.find("unsat")!= line.npos){
+ while (getline(input, line)) {
+ if (line.find("unsat") != line.npos) {
return IS_UNSAT;
}
- if(line.find("(define-fun") != line.npos || line.find("( (") != line.npos){
+ if (line.find("(define-fun") != line.npos || line.find("( (") != line.npos) {
string valueline;
ASSERT(getline(input, valueline));
- char cline [line.size()+1];
+ char cline [line.size() + 1];
strcpy ( cline, line.c_str() );
- char vline [valueline.size()+1];
+ char vline [valueline.size() + 1];
strcpy ( vline, valueline.c_str() );
extractValue(cline, vline);
}
return IS_SAT;
}
-void SMTInterpreter::dumpFooter(){
+void SMTInterpreter::dumpFooter() {
output << "(check-sat)" << endl;
output << "(get-model)" << endl;
}
-void SMTInterpreter::dumpHeader(){
+void SMTInterpreter::dumpHeader() {
}
-void SMTInterpreter::compileRunCommand(char * command, size_t size){
+void SMTInterpreter::compileRunCommand(char *command, size_t size) {
model_print("Calling Z3...\n");
snprintf(command, size, "./run.sh z3 -T:%u -in < %s > %s", getTimeout(), SMTFILENAME, SMTSOLUTIONFILE);
}
-string SMTInterpreter::negateConstraint(string constr){
+string SMTInterpreter::negateConstraint(string constr) {
return "( not " + constr + " )";
}
-string SMTInterpreter::encodeBooleanLogic( BooleanLogic *bl){
+string SMTInterpreter::encodeBooleanLogic( BooleanLogic *bl) {
uint size = bl->inputs.getSize();
string array[size];
for (uint i = 0; i < size; i++)
array[i] = encodeConstraint(bl->inputs.get(i));
string op;
- switch (bl->op){
- case SATC_OR:
- op = "or";
- break;
- case SATC_AND:
- op = "and";
- break;
- case SATC_NOT:
- op = "not";
- break;
- case SATC_IMPLIES:
- op = "=>";
- break;
- case SATC_XOR:
- default:
- ASSERT(0);
+ switch (bl->op) {
+ case SATC_OR:
+ op = "or";
+ break;
+ case SATC_AND:
+ op = "and";
+ break;
+ case SATC_NOT:
+ op = "not";
+ break;
+ case SATC_IMPLIES:
+ op = "=>";
+ break;
+ case SATC_XOR:
+ default:
+ ASSERT(0);
}
switch (bl->op) {
- case SATC_XOR:
- case SATC_OR:
- case SATC_AND:{
- ASSERT(size >= 2);
- string res = array[0];
- for( uint i=1; i< size; i++){
- res = "( " + op + " " + res + " " + array[i] + " )";
- }
- return res;
+ case SATC_XOR:
+ case SATC_OR:
+ case SATC_AND: {
+ ASSERT(size >= 2);
+ string res = array[0];
+ for ( uint i = 1; i < size; i++) {
+ res = "( " + op + " " + res + " " + array[i] + " )";
}
- case SATC_NOT:{
- return "( not " + array[0] + " )";
- }
- case SATC_IMPLIES:
- return "( " + op + " " + array[0] + " " + array[1] + " )";
- case SATC_IFF:
- default:
- ASSERT(0);
+ return res;
+ }
+ case SATC_NOT: {
+ return "( not " + array[0] + " )";
+ }
+ case SATC_IMPLIES:
+ return "( " + op + " " + array[0] + " " + array[1] + " )";
+ case SATC_IFF:
+ default:
+ ASSERT(0);
}
}
-string SMTInterpreter::encodeBooleanVar( BooleanVar *bv){
- ValuedSignature * boolSig = sigEnc.getBooleanSignature(bv);
+string SMTInterpreter::encodeBooleanVar( BooleanVar *bv) {
+ ValuedSignature *boolSig = sigEnc.getBooleanSignature(bv);
return *boolSig + "";
}
-string SMTInterpreter::processElementFunction(ElementFunction* elemFunc, ValuedSignature *signature){
+string SMTInterpreter::processElementFunction(ElementFunction *elemFunc, ValuedSignature *signature) {
FunctionOperator *function = (FunctionOperator *) elemFunc->getFunction();
uint numDomains = elemFunc->inputs.getSize();
ASSERT(numDomains > 1);
for (uint i = 0; i < numDomains; i++) {
Element *elem = elemFunc->inputs.get(i);
inputs[i] = sigEnc.getElementSignature(elem);
- if(elem->type == ELEMFUNCRETURN){
+ if (elem->type == ELEMFUNCRETURN) {
result += processElementFunction((ElementFunction *) elem, inputs[i]);
}
}
string op;
- switch(function->op){
- case SATC_ADD:
- op = "+";
- break;
- case SATC_SUB:
- op = "-";
- break;
- default:
- ASSERT(0);
+ switch (function->op) {
+ case SATC_ADD:
+ op = "+";
+ break;
+ case SATC_SUB:
+ op = "-";
+ break;
+ default:
+ ASSERT(0);
}
- result += "( = " + *signature;
+ result += "( = " + *signature;
string tmp = "" + *inputs[0];
for (uint i = 1; i < numDomains; i++) {
tmp = "( " + op + " " + tmp + " " + *inputs[i] + " )";
return result;
}
-string SMTInterpreter::operatorPredicateConstraint(CompOp op, ValuedSignature *elemSig1, ValuedSignature *elemSig2){
+string SMTInterpreter::operatorPredicateConstraint(CompOp op, ValuedSignature *elemSig1, ValuedSignature *elemSig2) {
switch (op) {
- case SATC_EQUALS:
- return "( = " + *elemSig1 + " " + *elemSig2 +" )";
- case SATC_LT:
- return "( < " + *elemSig1 + " " + *elemSig2 + " )";
- case SATC_GT:
- return "(> " + *elemSig1 + " " + *elemSig2 + " )";
- default:
- ASSERT(0);
+ case SATC_EQUALS:
+ return "( = " + *elemSig1 + " " + *elemSig2 + " )";
+ case SATC_LT:
+ return "( < " + *elemSig1 + " " + *elemSig2 + " )";
+ case SATC_GT:
+ return "(> " + *elemSig1 + " " + *elemSig2 + " )";
+ default:
+ ASSERT(0);
}
}
#define SMTFILENAME "satune.smt"
#define SMTSOLUTIONFILE "solution.sol"
-class SMTInterpreter: public Interpreter{
+class SMTInterpreter : public Interpreter {
public:
SMTInterpreter(CSolver *solver);
virtual ValuedSignature *getBooleanSignature(uint id);
protected:
virtual void dumpFooter();
virtual void dumpHeader();
- virtual void compileRunCommand(char * command , size_t size);
+ virtual void compileRunCommand(char *command, size_t size);
virtual int getResult();
virtual void dumpAllConstraints(Vector<char *> &facts);
virtual string negateConstraint(string constr);
* and open the template in the editor.
*/
-/*
+/*
* File: smtratinterpreter.cc
* Author: hamed
- *
+ *
* Created on February 21, 2019, 2:33 PM
*/
#include "smtratinterpreter.h"
-SMTRatInterpreter::SMTRatInterpreter(CSolver *solver):
+SMTRatInterpreter::SMTRatInterpreter(CSolver *solver) :
SMTInterpreter(solver)
-{
+{
}
-void SMTRatInterpreter::compileRunCommand(char * command , size_t size){
+void SMTRatInterpreter::compileRunCommand(char *command, size_t size) {
model_print("Calling SMTRat...\n");
snprintf(command, size, "./run.sh timeout %u smtrat %s > %s", getTimeout(), SMTFILENAME, SMTSOLUTIONFILE);
}
-SMTRatInterpreter::~SMTRatInterpreter(){
+SMTRatInterpreter::~SMTRatInterpreter() {
}
* and open the template in the editor.
*/
-/*
+/*
* File: smtratinterpreter.h
* Author: hamed
*
#define SMTRATINTERPRETER_H
#include "smtinterpreter.h"
-class SMTRatInterpreter: public SMTInterpreter{
+class SMTRatInterpreter : public SMTInterpreter {
public:
SMTRatInterpreter(CSolver *solver);
virtual ~SMTRatInterpreter();
protected:
- void compileRunCommand(char * command , size_t size);
+ void compileRunCommand(char *command, size_t size);
};
-#endif /* SMTRATINTERPRETER_H */
+#endif/* SMTRATINTERPRETER_H */
#include "smtsig.h"
#include "set.h"
-SMTBoolSig::SMTBoolSig(uint id):
+SMTBoolSig::SMTBoolSig(uint id) :
ValuedSignature(id)
{
}
-string SMTBoolSig::toString() const{
+string SMTBoolSig::toString() const {
return "b" + to_string(id);
}
-string SMTBoolSig::getSignature() const{
+string SMTBoolSig::getSignature() const {
return "(declare-const b" + to_string(id) + " Bool)";
}
-string SMTBoolSig::getAbsSignature() const{
+string SMTBoolSig::getAbsSignature() const {
return "";
}
-SMTElementSig::SMTElementSig(uint id, SMTSetSig *_ssig):
+SMTElementSig::SMTElementSig(uint id, SMTSetSig *_ssig) :
ValuedSignature(id),
ssig(_ssig)
{
}
-string SMTElementSig::toString() const{
+string SMTElementSig::toString() const {
return "e" + to_string(id);
}
-string SMTElementSig::getSignature() const{
+string SMTElementSig::getSignature() const {
string str = "(declare-const e" + to_string(id) + " Int)\n";
string constraint = ssig->getAbsSignature();
size_t start_pos;
string placeholder = "$";
- while((start_pos = constraint.find(placeholder)) != string::npos){
+ while ((start_pos = constraint.find(placeholder)) != string::npos) {
constraint.replace(start_pos, placeholder.size(), to_string(id));
}
//constraint.replace(constraint.begin(), constraint.end(), "$", );
return str;
}
-string SMTElementSig::getAbsSignature() const{
+string SMTElementSig::getAbsSignature() const {
return "";
-
+
}
-SMTSetSig::SMTSetSig(uint id, Set *set): Signature(id){
+SMTSetSig::SMTSetSig(uint id, Set *set) : Signature(id) {
ASSERT(set->getSize() > 0);
- int min = set->getElement(0), max = set->getElement(set->getSize()-1);
+ int min = set->getElement(0), max = set->getElement(set->getSize() - 1);
Vector<int> holes;
int prev = set->getElement(0);
- for(uint i=1; i< set->getSize(); i++){
+ for (uint i = 1; i < set->getSize(); i++) {
int curr = set->getElement(i);
- if(prev != curr -1){
- for(int j=prev+1; j< curr; j++){
+ if (prev != curr - 1) {
+ for (int j = prev + 1; j < curr; j++) {
holes.push(j);
}
}
prev = curr;
}
- constraint = "(assert (<= e$ " + to_string(max) +"))\n";
- constraint += "(assert (>= e$ " + to_string(min) +"))\n";
- for(uint i=0; i< holes.getSize(); i++){
- constraint += "(assert (not (= e$ " + to_string(holes.get(i)) +")))\n";
+ constraint = "(assert (<= e$ " + to_string(max) + "))\n";
+ constraint += "(assert (>= e$ " + to_string(min) + "))\n";
+ for (uint i = 0; i < holes.getSize(); i++) {
+ constraint += "(assert (not (= e$ " + to_string(holes.get(i)) + ")))\n";
}
}
-string SMTSetSig::toString() const{
+string SMTSetSig::toString() const {
return "";
}
-string SMTSetSig::getSignature() const{
+string SMTSetSig::getSignature() const {
return "";
}
-string SMTSetSig::getAbsSignature() const{
+string SMTSetSig::getAbsSignature() const {
return constraint;
-
+
}
#include "classlist.h"
using namespace std;
-class SMTBoolSig: public ValuedSignature{
+class SMTBoolSig : public ValuedSignature {
public:
SMTBoolSig(uint id);
- virtual ~SMTBoolSig(){}
+ virtual ~SMTBoolSig() {}
virtual string toString() const;
virtual string getAbsSignature() const;
virtual string getSignature() const;
};
-class SMTSetSig: public Signature{
+class SMTSetSig : public Signature {
public:
SMTSetSig(uint id, Set *set);
- virtual ~SMTSetSig(){}
+ virtual ~SMTSetSig() {}
virtual string toString() const;
virtual string getAbsSignature() const;
virtual string getSignature() const;
string constraint;
};
-class SMTElementSig: public ValuedSignature{
+class SMTElementSig : public ValuedSignature {
public:
SMTElementSig(uint id, SMTSetSig *ssig);
- virtual ~SMTElementSig(){}
+ virtual ~SMTElementSig() {}
virtual string toString() const;
virtual string getAbsSignature() const;
virtual string getSignature() const;
if (filedesc < 0) {
exit(-1);
}
- if(itype != SATUNE){
+ if (itype != SATUNE) {
solver->setInterpreter(itype);
}
}
#include "csolver.h"
-InterpreterType getInterpreterType(char * itype){
- if(strcmp (itype,"--alloy") == 0){
+InterpreterType getInterpreterType(char *itype) {
+ if (strcmp (itype,"--alloy") == 0) {
return ALLOY;
- } else if(strcmp (itype,"--z3") == 0){
+ } else if (strcmp (itype,"--z3") == 0) {
return Z3;
- } else if(strcmp (itype,"--smtrat") == 0){
+ } else if (strcmp (itype,"--smtrat") == 0) {
return SMTRAT;
- } else if(strcmp (itype,"--mathsat") == 0){
+ } else if (strcmp (itype,"--mathsat") == 0) {
return MATHSAT;
} else {
printf("Unknown interpreter type: %s\n", itype);
printf("./run.sh deserializer test.dump [--alloy/--z3/--smtrat/--mathsat] [timeout]\n");
exit(-1);
}
- CSolver *solver;
- if(argc >= 3){
+ CSolver *solver;
+ if (argc >= 3) {
solver = CSolver::deserialize(argv[1], getInterpreterType(argv[2]));
- if(argc == 4){
+ if (argc == 4) {
solver->setSatSolverTimeout(atol(argv[3]));
}
} else {
printf("You should specify a tuner: %s <best.tuner>\n", argv[0]);
exit(-1);
}
-
+
SearchTuner *tuner = new SearchTuner(argv[1]);
tuner->print();
delete tuner;
#include "comptuner.h"
#include "randomtuner.h"
-void printKnownTunerTypes(){
+void printKnownTunerTypes() {
printf("Known Tuner Types:\nRandom Tuner=1\nComp Tuner=2\nKmeans Tuner=3\nSimulated Annealing Tuner=4\n");
}
-BasicTuner *createTuner(uint tunertype, uint budget, uint rounds, uint timeout){
- switch(tunertype){
- case 1: return new RandomTuner(budget, timeout);
- case 2: return new CompTuner(budget, timeout);
- case 3: return new KMeansTuner(budget, rounds, timeout);
- case 4: return new SATuner(budget, timeout);
- default:
- printf("Tuner type %u is unknown\n", tunertype);
- printKnownTunerTypes();
- exit(-1);
+BasicTuner *createTuner(uint tunertype, uint budget, uint rounds, uint timeout) {
+ switch (tunertype) {
+ case 1: return new RandomTuner(budget, timeout);
+ case 2: return new CompTuner(budget, timeout);
+ case 3: return new KMeansTuner(budget, rounds, timeout);
+ case 4: return new SATuner(budget, timeout);
+ default:
+ printf("Tuner type %u is unknown\n", tunertype);
+ printKnownTunerTypes();
+ exit(-1);
}
}
else
multituner->addProblem(argv[i]);
} else
- multituner->addTuner(new SearchTuner(argv[i], true )); //add settings to usedsettigs
+ multituner->addTuner(new SearchTuner(argv[i], true ));//add settings to usedsettigs
}
if (!tunerfiles) {
* and open the template in the editor.
*/
-/*
+/*
* File: basictuner.cc
* Author: hamed
- *
+ *
* Created on December 17, 2018, 2:02 PM
*/
timetaken.put(problem, time);
}
-void TunerRecord::print(){
+void TunerRecord::print() {
model_print("*************TUNER NUMBER=%d***********\n", tunernumber);
tuner->print();
model_print("&&&&&&&&&&&&&USED SETTINGS &&&&&&&&&&&&\n");
model_print("\n");
}
-void TunerRecord::printProblemsInfo(){
+void TunerRecord::printProblemsInfo() {
for (uint j = 0; j < problems.getSize(); j++) {
Problem *problem = problems.get(j);
model_print("Problem %s\n", problem->getProblem());
BasicTuner::BasicTuner(uint _budget, uint _timeout) :
- budget(_budget), timeout(_timeout), execnum(0){
+ budget(_budget), timeout(_timeout), execnum(0) {
}
BasicTuner::~BasicTuner() {
}
}
-bool BasicTuner::tunerExists(TunerRecord *tunerec){
+bool BasicTuner::tunerExists(TunerRecord *tunerec) {
SearchTuner *tuner = tunerec->getTuner();
- for(uint i=0; i< explored.getSize(); i++){
- if(explored.get(i)->getTuner()->equalUsed(tuner)){
+ for (uint i = 0; i < explored.getSize(); i++) {
+ if (explored.get(i)->getTuner()->equalUsed(tuner)) {
model_print("************Tuner <%d> is replicate of Tuner <%d>\n", tunerec->getTunerNumber(), explored.get(i)->getTunerNumber());
return true;
}
return newTuner;
}
-int BasicTuner::subTunerIndex(SearchTuner *newTuner){
- for (uint i=0; i< explored.getSize(); i++){
+int BasicTuner::subTunerIndex(SearchTuner *newTuner) {
+ for (uint i = 0; i < explored.getSize(); i++) {
SearchTuner *tuner = explored.get(i)->getTuner();
- if(tuner->isSubTunerof(newTuner)){
+ if (tuner->isSubTunerof(newTuner)) {
return i;
}
}
* and open the template in the editor.
*/
-/*
+/*
* File: basictuner.h
* Author: hamed
*
public:
Problem(const char *problem);
char *getProblem() {return problem;}
- inline int getResult(){return result;}
- inline int getProblemNumber(){return problemnumber;}
- inline void setResult(int res){result = res;}
- inline void setProblemNumber(int probNum){problemnumber = probNum;}
- inline long long getBestTime() {return besttime ;}
+ inline int getResult() {return result;}
+ inline int getProblemNumber() {return problemnumber;}
+ inline void setResult(int res) {result = res;}
+ inline void setProblemNumber(int probNum) {problemnumber = probNum;}
+ inline long long getBestTime() {return besttime ;}
inline void setBestTime(long long time) {besttime = time;}
~Problem();
CMEMALLOC;
TunerRecord(SearchTuner *_tuner) : tuner(_tuner), tunernumber(-1), isduplicate(false) {}
TunerRecord(SearchTuner *_tuner, int _tunernumber) : tuner(_tuner), tunernumber(_tunernumber), isduplicate(false) {}
SearchTuner *getTuner() {return tuner;}
- void inline addProblem(Problem * problem){problems.push(problem);}
+ void inline addProblem(Problem *problem) {problems.push(problem);}
TunerRecord *changeTuner(SearchTuner *_newtuner);
void updateTuner(SearchTuner *_newtuner) {tuner = _newtuner;}
long long getTime(Problem *problem);
void setTime(Problem *problem, long long time);
- inline void setTunerNumber(int numb){tunernumber = numb;}
- inline int getTunerNumber(){return tunernumber;}
+ inline void setTunerNumber(int numb) {tunernumber = numb;}
+ inline int getTunerNumber() {return tunernumber;}
inline uint problemsSize() {return problems.getSize();}
inline void setDuplicate(bool _duplicate) { isduplicate = _duplicate;}
inline bool isDuplicate() {return isduplicate;}
- inline Problem *getProblem(uint index){return problems.get(index);}
- void print();
+ inline Problem *getProblem(uint index) {return problems.get(index);}
+ void print();
void printProblemsInfo();
CMEMALLOC;
private:
protected:
long long evaluate(Problem *problem, TunerRecord *tuner);
/**
- * returns the index of the tuner which is subtune of
- * the newTuner
- * @param newTuner
- * @return
- */
- int subTunerIndex(SearchTuner *newTuner);
+ * returns the index of the tuner which is subtune of
+ * the newTuner
+ * @param newTuner
+ * @return
+ */
+ int subTunerIndex(SearchTuner *newTuner);
bool tunerExists(TunerRecord *tunerRec);
SearchTuner *mutateTuner(SearchTuner *oldTuner, uint k);
void updateTimeout(Problem *problem, long long metric);
int execnum;
};
-#endif /* BASICTUNER_H */
+#endif/* BASICTUNER_H */
{
}
-CompTuner::~CompTuner(){
-
+CompTuner::~CompTuner() {
+
}
void CompTuner::findBestThreeTuners() {
model_print("Round %u of %u\n", b, budget);
Hashtable<TunerRecord *, int, uint64_t> scores;
Vector<Vector<TunerRecord *> *> allplaces;
- for(uint ii=0; ii< problems.getSize(); ii++){
+ for (uint ii = 0; ii < problems.getSize(); ii++) {
allplaces.push(new Vector<TunerRecord *>());
}
for (uint j = 0; j < tunerV->getSize(); j++) {
TunerRecord *tuner = tunerV->get(j);
-
+
for (uint i = 0; i < problems.getSize(); i++) {
Vector<TunerRecord *> *places = allplaces.get(i);
Problem *problem = problems.get(i);
tuner->setTime(problem, metric);
else
tuner->setTime(problem, -2);
-
- if(tunerExists(tuner)){
+
+ if (tunerExists(tuner)) {
//Solving the problem and noticing the tuner
//already exists
tuner->setDuplicate(true);
}
}
}
- for(uint ii=0; ii < problems.getSize(); ii++){
+ for (uint ii = 0; ii < problems.getSize(); ii++) {
Problem *problem = problems.get(ii);
Vector<TunerRecord *> *places = allplaces.get(ii);
int points = 9;
for (uint k = 0; k < places->getSize() && points; k++) {
TunerRecord *tuner = places->get(k);
- if(tuner->isDuplicate()){
+ if (tuner->isDuplicate()) {
continue;
}
int currScore = 0;
points = points / 3;
}
}
- for(uint ii=0; ii< problems.getSize(); ii++){
+ for (uint ii = 0; ii < problems.getSize(); ii++) {
delete allplaces.get(ii);
}
Vector<TunerRecord *> ranking;
uint tSize = tunerV->getSize();
for (uint i = 0; i < tSize; i++) {
SearchTuner *tmpTuner = mutateTuner(tunerV->get(i)->getTuner(), b);
- while(subTunerIndex(tmpTuner) != -1){
+ while (subTunerIndex(tmpTuner) != -1) {
model_print("******** New Tuner already explored...\n");
delete tmpTuner;
tmpTuner = mutateTuner(tunerV->get(i)->getTuner(), b);
void tune();
void findBestThreeTuners();
protected:
-
+
};
inline long long min(long long num1, long long num2, long long num3) {
* and open the template in the editor.
*/
-/*
+/*
* File: kmeanstuner.cc
* Author: hamed
- *
+ *
* Created on December 19, 2018, 4:16 PM
*/
#include "searchtuner.h"
#include "math.h"
-KMeansTuner::KMeansTuner(uint budget, uint _rounds, uint timeout) :
+KMeansTuner::KMeansTuner(uint budget, uint _rounds, uint timeout) :
BasicTuner(budget, timeout),
rounds(_rounds) {
}
* and open the template in the editor.
*/
-/*
+/*
* File: kmeanstuner.h
* Author: hamed
*
uint rounds;
};
-#endif /* KMEANSTUNER_H */
+#endif/* KMEANSTUNER_H */
#define UNSETVALUE -1
-RandomTuner::RandomTuner(uint _budget, uint _timeout) :
+RandomTuner::RandomTuner(uint _budget, uint _timeout) :
BasicTuner(_budget, _timeout) {
}
-RandomTuner::~RandomTuner(){
-
+RandomTuner::~RandomTuner() {
+
}
void RandomTuner::tune() {
for (uint r = 0; r < budget; r++) {
model_print("Round %u of %u\n", r, budget);
- for (uint i = 0; i < tuners.getSize(); i++){
+ for (uint i = 0; i < tuners.getSize(); i++) {
TunerRecord *tuner = tuners.get(i);
bool isNew = true;
- for (uint j = 0; j < problems.getSize(); j++){
+ for (uint j = 0; j < problems.getSize(); j++) {
Problem *problem = problems.get(j);
long long metric = tuner->getTime(problem);
- if(metric == -1){
+ if (metric == -1) {
metric = evaluate(problem, tuner);
ASSERT(tuner->getTime(problem) == -1);
tuner->addProblem(problem);
tuner->setTime(problem, metric);
else
tuner->setTime(problem, -2);
- if(tunerExists(tuner)){
+ if (tunerExists(tuner)) {
//Solving the problem and noticing the tuner
//already exists
isNew = false;
}
}
}
- if(isNew){
+ if (isNew) {
explored.push(tuner);
}
-
+
}
uint tSize = tuners.getSize();
for (uint i = 0; i < tSize; i++) {
SearchTuner *tmpTuner = mutateTuner(tuners.get(i)->getTuner(), budget);
- while(subTunerIndex(tmpTuner) != -1){
+ while (subTunerIndex(tmpTuner) != -1) {
tmpTuner->randomMutate();
}
TunerRecord *tmp = new TunerRecord(tmpTuner);
}
}
printData();
-
+
}
#include "basictuner.h"
/**
- * This is a Tuner which is being used for
+ * This is a Tuner which is being used for
*/
class RandomTuner : public BasicTuner {
public:
virtual ~RandomTuner();
void tune();
protected:
- bool randomMutation(SearchTuner *tuner);
+ bool randomMutation(SearchTuner *tuner);
TunerRecord *tune(SearchTuner *tuner);
};
{
}
-SATuner::~SATuner(){
+SATuner::~SATuner() {
}
-void SATuner::rankTunerForProblem(Vector<TunerRecord *> *places, TunerRecord *tuner, Problem *problem, long long metric){
+void SATuner::rankTunerForProblem(Vector<TunerRecord *> *places, TunerRecord *tuner, Problem *problem, long long metric) {
uint k = 0;
for (; k < places->getSize(); k++) {
if (metric < places->get(k)->getTime(problem))
break;
}
model_print("Problem<%s>:place[%u]=Tuner<%p,%d>\n", problem->getProblem(), k, tuner, tuner->getTunerNumber());
- places->insertAt(k, tuner);
+ places->insertAt(k, tuner);
}
-void SATuner::removeTunerIndex(Vector<TunerRecord *> *tunerV, int index, Vector<Vector<TunerRecord *> *> &allplaces){
+void SATuner::removeTunerIndex(Vector<TunerRecord *> *tunerV, int index, Vector<Vector<TunerRecord *> *> &allplaces) {
TunerRecord *tuner = tunerV->get(index);
model_print("Removing Tuner %d\n", tuner->getTunerNumber());
tunerV->set(index, NULL);
- for(uint i=0; i < allplaces.getSize(); i++){
+ for (uint i = 0; i < allplaces.getSize(); i++) {
Vector<TunerRecord *> *places = allplaces.get(i);
- for(uint j=0; j < places->getSize(); j++){
- if(tuner == places->get(j)){
+ for (uint j = 0; j < places->getSize(); j++) {
+ if (tuner == places->get(j)) {
places->removeAt(j);
break;
}
}
-void SATuner::removeNullsFromTunerVector( Vector<TunerRecord *> *tunerV){
- for (int i= tunerV->getSize() -1; i >= 0; i--){
- if(tunerV->get(i) == NULL){
+void SATuner::removeNullsFromTunerVector( Vector<TunerRecord *> *tunerV) {
+ for (int i = tunerV->getSize() - 1; i >= 0; i--) {
+ if (tunerV->get(i) == NULL) {
tunerV->removeAt(i);
}
}
model_print("TunerV size after removing nulls = %u\n", tunerV->getSize());
}
-void SATuner::initialize(Vector<TunerRecord *> *tunerV, Vector<Vector<TunerRecord *> *> &allplaces){
- for(uint ii=0; ii< problems.getSize(); ii++){
+void SATuner::initialize(Vector<TunerRecord *> *tunerV, Vector<Vector<TunerRecord *> *> &allplaces) {
+ for (uint ii = 0; ii < problems.getSize(); ii++) {
allplaces.push(new Vector<TunerRecord *>());
}
- for (uint j = 0; j< tunerV->getSize(); j++){
+ for (uint j = 0; j < tunerV->getSize(); j++) {
TunerRecord *tuner = tunerV->get(j);
- for (uint i=0; i < problems.getSize(); i++){
+ for (uint i = 0; i < problems.getSize(); i++) {
Problem *problem = problems.get(i);
long long metric = evaluate(problem, tuner);
ASSERT(tuner->getTime(problem) == -1);
tuner->addProblem(problem);
- if(metric != -1){
- tuner->setTime(problem , metric);
- }else{
- tuner->setTime(problem , -2);
+ if (metric != -1) {
+ tuner->setTime(problem, metric);
+ } else {
+ tuner->setTime(problem, -2);
}
- if(metric >=0){
+ if (metric >= 0) {
Vector<TunerRecord *> *places = allplaces.get(i);
rankTunerForProblem(places, tuner, problem, metric);
}
}
void SATuner::tune() {
- Vector<TunerRecord *> *tunerV = new Vector<TunerRecord *>(&tuners);
+ Vector<TunerRecord *> *tunerV = new Vector<TunerRecord *>(&tuners);
Vector<Vector<TunerRecord *> *> allplaces;
uint tunerNumber = tuners.getSize();
//Initialization
initialize(tunerV, allplaces);
//Starting the body of algorithm
- for (uint t = budget; t >0; t--) {
+ for (uint t = budget; t > 0; t--) {
model_print("Current Temperature = %u\n", t);
Hashtable<TunerRecord *, int, uint64_t> scores;
for (uint i = 0; i < tunerNumber; i++) {
- SearchTuner *tmpTuner = mutateTuner(tunerV->get(i)->getTuner(), budget-t);
+ SearchTuner *tmpTuner = mutateTuner(tunerV->get(i)->getTuner(), budget - t);
int tunerIndex = subTunerIndex(tmpTuner);
TunerRecord *tmp = NULL;
- if(tunerIndex == -1){
+ if (tunerIndex == -1) {
tmp = new TunerRecord(tmpTuner);
tmp->setTunerNumber(allTuners.getSize());
model_print("Mutated tuner %u to generate tuner %u\n", tunerV->get(i)->getTunerNumber(), tmp->getTunerNumber());
- allTuners.push(tmp);
- }else{
+ allTuners.push(tmp);
+ } else {
//Previous tuners might get explored with new combination of tuners.
- tmp = explored.get(tunerIndex);
+ tmp = explored.get(tunerIndex);
model_print("Using exploread tuner <%u>\n", tmp->getTunerNumber());
}
tunerV->push(tmp);
}
}
}
- for(uint ii=0; ii < problems.getSize(); ii++){
+ for (uint ii = 0; ii < problems.getSize(); ii++) {
Problem *problem = problems.get(ii);
ASSERT(ii < allplaces.getSize());
Vector<TunerRecord *> *places = allplaces.get(ii);
- int points = pow(tunerNumber*1.0, 2*tunerNumber - 1);
+ int points = pow(tunerNumber * 1.0, 2 * tunerNumber - 1);
for (uint k = 0; k < places->getSize() && points; k++) {
TunerRecord *tuner = places->get(k);
int currScore = 0;
}
}
- for(uint i= 0; i < tunerNumber; i++){
+ for (uint i = 0; i < tunerNumber; i++) {
ASSERT(i < tunerV->getSize());
TunerRecord *tuner1 = tunerV->get(i);
TunerRecord *tuner2 = tunerV->get(tunerNumber + i);
if( score2 > score1 ){
removeTunerIndex(tunerV, i, allplaces);
- } else if( score2 < score1){
- model_print("score1=%d\tscore2=%d\tt=%u\texp=%f\n", score1, score2, t, exp((score1-score2)*1.0/t));
- double prob = 1/(exp((score1-score2)*1.0/t) );
+ } else if ( score2 < score1) {
+ model_print("score1=%d\tscore2=%d\tt=%u\texp=%f\n", score1, score2, t, exp((score1 - score2) * 1.0 / t));
+ double prob = 1 / (exp((score1 - score2) * 1.0 / t) );
double random = ((double) rand() / (RAND_MAX));
model_print("prob=%f\trandom=%f\n", prob, random);
- if(prob > random){
+ if (prob > random) {
removeTunerIndex(tunerV, i, allplaces);
- }else{
+ } else {
removeTunerIndex(tunerV, tunerNumber + i, allplaces);
}
- } else{
+ } else {
double random = ((double) rand() / (RAND_MAX));
- int index = random > 0.5? i : tunerNumber + i;
+ int index = random > 0.5 ? i : tunerNumber + i;
removeTunerIndex(tunerV, index, allplaces);
}
}
removeNullsFromTunerVector(tunerV);
-
+
}
- for(uint ii=0; ii< allplaces.getSize(); ii++){
+ for (uint ii = 0; ii < allplaces.getSize(); ii++) {
delete allplaces.get(ii);
}
printData();
#include "basictuner.h"
/**
-*This tuner has the simulated annealing in its core
-*
-*/
+ * This tuner has the simulated annealing in its core
+ *
+ */
class SATuner : public BasicTuner {
public:
SATuner(uint budget, uint timeout);
}
setting->setDecision(lowValue, highValue, defaultValue, selectedValue);
settings.add(setting);
- if(addused){
+ if (addused) {
usedSettings.add(setting);
}
}
}
}
-bool SearchTuner::equalUsed(SearchTuner* tuner){
- if(tuner->usedSettings.getSize() != usedSettings.getSize()){
+bool SearchTuner::equalUsed(SearchTuner *tuner) {
+ if (tuner->usedSettings.getSize() != usedSettings.getSize()) {
return false;
}
bool result = true;
SetIteratorTunableSetting *iterator = usedSettings.iterator();
- while(iterator->hasNext()){
+ while (iterator->hasNext()) {
TunableSetting *setting = iterator->next();
- if(!tuner->usedSettings.contains(setting)){
+ if (!tuner->usedSettings.contains(setting)) {
result = false;
break;
- }else{
+ } else {
TunableSetting *tunerSetting = tuner->usedSettings.get(setting);
- if(tunerSetting->selectedValue != setting->selectedValue){
+ if (tunerSetting->selectedValue != setting->selectedValue) {
result = false;
break;
}
}
}
-bool SearchTuner::isSubTunerof(SearchTuner *newTuner){
+bool SearchTuner::isSubTunerof(SearchTuner *newTuner) {
SetIteratorTunableSetting *iterator = usedSettings.iterator();
while (iterator->hasNext()) {
TunableSetting *setting = iterator->next();
- if(!newTuner->settings.contains(setting)){
+ if (!newTuner->settings.contains(setting)) {
return false;
- } else{
+ } else {
TunableSetting *newSetting = newTuner->settings.get(setting);
- if(newSetting->selectedValue != setting->selectedValue){
+ if (newSetting->selectedValue != setting->selectedValue) {
return false;
}
}
void setVarTunable(VarType vartype, TunableParam param, TunableDesc *descriptor, uint value);
void setVarTunable(VarType vartype1, VarType vartype2, TunableParam param, TunableDesc *descriptor, uint value);
SearchTuner *copyUsed();
- bool isSubTunerof(SearchTuner *newTuner);
+ bool isSubTunerof(SearchTuner *newTuner);
void randomMutate();
uint getSize() { return usedSettings.getSize();}
void print();
void serialize(const char *file);
void serializeUsed(const char *file);
void addUsed(const char *file);
- bool equalUsed(SearchTuner *tuner);
+ bool equalUsed(SearchTuner *tuner);
CMEMALLOC;
protected:
/** Used Settings keeps track of settings that were actually used by
* and open the template in the editor.
*/
-/*
+/*
* File: TunableDependent.cc
* Author: hamed
- *
+ *
* Created on October 5, 2018, 11:26 AM
*/
#include "tunabledependent.h"
-TunableDependent::TunableDependent(Tunables dependent, Tunables parent):
+TunableDependent::TunableDependent(Tunables dependent, Tunables parent) :
dependent(dependent),
parent(parent)
{
* and open the template in the editor.
*/
-/*
+/*
* File: TunableDependent.h
* Author: hamed
*
class TunableDependent {
public:
- TunableDependent(Tunables dependent, Tunables parent = (Tunables) -1);
- TunableDependent(TunableDependent &setting);
- virtual ~TunableDependent();
- Tunables dependent;
- Tunables parent;
+ TunableDependent(Tunables dependent, Tunables parent = (Tunables) - 1);
+ TunableDependent(TunableDependent &setting);
+ virtual ~TunableDependent();
+ Tunables dependent;
+ Tunables parent;
};
-#endif /* TUNABLEDEPENDENT_H */
+#endif/* TUNABLEDEPENDENT_H */
return CCSOLVER(solver)->getBooleanVar((VarType) type).getRaw();
}
-void *getBooleanTrue(void *solver){
+void *getBooleanTrue(void *solver) {
return CCSOLVER(solver)->getBooleanTrue().getRaw();
}
-void *getBooleanFalse(void *solver){
+void *getBooleanFalse(void *solver) {
return CCSOLVER(solver)->getBooleanFalse().getRaw();
}
CCSOLVER(solver)->mustHaveValue( (Element *) element);
}
-void setInterpreter(void *solver, unsigned int type){
+void setInterpreter(void *solver, unsigned int type) {
CCSOLVER(solver)->setInterpreter((InterpreterType)type);
}
for (uint i = 0; i < size; i++) {
delete allFunctions.get(i);
}
-
- if(interpreter != NULL){
+
+ if (interpreter != NULL) {
delete interpreter;
}
BooleanEdge CSolver::getBooleanVar(VarType type) {
Boolean *boolean = new BooleanVar(type);
allBooleans.push(boolean);
- if(!booleanVarUsed)
+ if (!booleanVarUsed)
booleanVarUsed = true;
return BooleanEdge(boolean);
}
}
BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint asize) {
- if(!useInterpreter()){
+ if (!useInterpreter()) {
BooleanEdge newarray[asize];
switch (op) {
case SATC_NOT: {
return applyLogicalOperation(SATC_OR, applyLogicalOperation(SATC_NOT, array[0]), array[1]);
}
}
-
+
ASSERT(asize != 0);
Boolean *boolean = new BooleanLogic(this, op, array, asize);
Boolean *b = boolMap.get(boolean);
Boolean *boolean = new BooleanLogic(this, op, array, asize);
allBooleans.push(boolean);
return BooleanEdge(boolean);
-
+
}
}
}
}
Boolean *constraint = new BooleanOrder(order, first, second);
- if (!useInterpreter() ){
+ if (!useInterpreter() ) {
Boolean *b = boolMap.get(constraint);
if (b == NULL) {
}
void CSolver::addConstraint(BooleanEdge constraint) {
- if(!useInterpreter()){
+ if (!useInterpreter()) {
if (isTrue(constraint))
return;
else if (isFalse(constraint)) {
replaceBooleanWithTrueNoRemove(constraint);
constraint->parents.clear();
}
- } else{
+ } else {
constraints.add(constraint);
constraint->parents.clear();
}
}
int CSolver::solve() {
- if(isUnSAT()){
+ if (isUnSAT()) {
return IS_UNSAT;
}
long long startTime = getTimeNano();
deleteTuner = true;
}
int result = IS_INDETER;
- if(useInterpreter()){
+ if (useInterpreter()) {
interpreter->encode();
model_print("Problem encoded in Interpreter\n");
result = interpreter->solve();
model_print("Problem solved by Interpreter\n");
- } else{
+ } else {
{
SetIteratorOrder *orderit = activeOrders.iterator();
eg.encode();
naiveEncodingDecision(this);
- // eg.validate();
+ // eg.validate();
VarOrderingOpt bor(this, satEncoder);
bor.doTransform();
time2 = getTimeNano();
model_print("Encoding Graph Time: %f\n", (time2 - time1) / NANOSEC);
-
+
satEncoder->encodeAllSATEncoder(this);
time1 = getTimeNano();
model_print("Elapse Encode time: %f\n", (time1 - startTime) / NANOSEC);
model_print("Is problem UNSAT after encoding: %d\n", unsat);
-
+
result = unsat ? IS_UNSAT : satEncoder->solve(satsolverTimeout);
model_print("Result Computed in SAT solver:\t%s\n", result == IS_SAT ? "SAT" : result == IS_INDETER ? "INDETERMINATE" : " UNSAT");
return result;
}
-void CSolver::setInterpreter(InterpreterType type){
- if(interpreter == NULL){
- switch(type){
- case SATUNE:
- break;
- case ALLOY:{
- interpreter = new AlloyInterpreter(this);
- break;
- }case Z3:{
- interpreter = new SMTInterpreter(this);
- break;
- }
- case MATHSAT:{
- interpreter = new MathSATInterpreter(this);
- break;
- }
- case SMTRAT:{
- interpreter = new SMTRatInterpreter(this);
- break;
- }
- default:
- ASSERT(0);
+void CSolver::setInterpreter(InterpreterType type) {
+ if (interpreter == NULL) {
+ switch (type) {
+ case SATUNE:
+ break;
+ case ALLOY: {
+ interpreter = new AlloyInterpreter(this);
+ break;
+ } case Z3: {
+ interpreter = new SMTInterpreter(this);
+ break;
+ }
+ case MATHSAT: {
+ interpreter = new MathSATInterpreter(this);
+ break;
+ }
+ case SMTRAT: {
+ interpreter = new SMTRatInterpreter(this);
+ break;
+ }
+ default:
+ ASSERT(0);
}
}
}
case ELEMSET:
case ELEMCONST:
case ELEMFUNCRETURN:
- return useInterpreter()? interpreter->getValue(element):
- getElementValueSATTranslator(this, element);
+ return useInterpreter() ? interpreter->getValue(element) :
+ getElementValueSATTranslator(this, element);
default:
ASSERT(0);
}
Boolean *boolean = bedge.getBoolean();
switch (boolean->type) {
case BOOLEANVAR:
- return useInterpreter()? interpreter->getBooleanValue(boolean):
- getBooleanVariableValueSATTranslator(this, boolean);
+ return useInterpreter() ? interpreter->getBooleanValue(boolean) :
+ getBooleanVariableValueSATTranslator(this, boolean);
default:
ASSERT(0);
}
/** When everything is done, the client calls this function and then csolver starts to encode*/
int solve();
-
+
/** After getting the solution from the SAT solver, client can get the value of an element via this function*/
uint64_t getElementValue(Element *element);
void setUnSAT() { model_print("Setting UNSAT %%%%%%\n"); unsat = true; }
void setSatSolverTimeout(long seconds) { satsolverTimeout = seconds;}
bool isUnSAT() { return unsat; }
- bool isBooleanVarUsed(){return booleanVarUsed;}
+ bool isBooleanVarUsed() {return booleanVarUsed;}
void printConstraint(BooleanEdge boolean);
void printConstraints();
SATEncoder *satEncoder;
bool unsat;
- bool booleanVarUsed;
- Tuner *tuner;
+ bool booleanVarUsed;
+ Tuner *tuner;
long long elapsedTime;
long satsolverTimeout;
Interpreter *interpreter;
* Signature: ()J
*/
JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createCCSolver
- (JNIEnv *, jobject);
+ (JNIEnv *, jobject);
/*
* Class: satune_SatuneJavaAPI
* Signature: (J)V
*/
JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_deleteCCSolver
- (JNIEnv *, jobject, jlong);
+ (JNIEnv *, jobject, jlong);
/*
* Signature: (J)V
*/
JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_resetCCSolver
- (JNIEnv *, jobject, jlong);
+ (JNIEnv *, jobject, jlong);
/*
* Class: satune_SatuneJavaAPI
* Signature: (JIJI)J
*/
JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createSet
- (JNIEnv *, jobject, jlong, jint, jlong, jint);
+ (JNIEnv *, jobject, jlong, jint, jlong, jint);
/*
* Class: satune_SatuneJavaAPI
* Signature: (JIJJ)J
*/
JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createRangeSet
- (JNIEnv *, jobject, jlong, jint, jlong, jlong);
+ (JNIEnv *, jobject, jlong, jint, jlong, jlong);
/*
* Class: satune_SatuneJavaAPI
* Signature: (JIJJ)J
*/
JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createRangeVar
- (JNIEnv *, jobject, jlong, jint, jlong, jlong);
+ (JNIEnv *, jobject, jlong, jint, jlong, jlong);
/*
* Class: satune_SatuneJavaAPI
* Signature: (JI)J
*/
JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createMutableSet
- (JNIEnv *, jobject, jlong, jint);
+ (JNIEnv *, jobject, jlong, jint);
/*
* Class: satune_SatuneJavaAPI
* Signature: (JJJ)V
*/
JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_addItem
- (JNIEnv *, jobject, jlong, jlong, jlong);
+ (JNIEnv *, jobject, jlong, jlong, jlong);
/*
* Class: satune_SatuneJavaAPI
* Signature: (JJ)V
*/
JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_finalizeMutableSet
- (JNIEnv *, jobject, jlong, jlong);
+ (JNIEnv *, jobject, jlong, jlong);
/*
* Class: satune_SatuneJavaAPI
* Signature: (JJ)J
*/
JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getElementVar
- (JNIEnv *, jobject, jlong, jlong);
+ (JNIEnv *, jobject, jlong, jlong);
/*
* Class: satune_SatuneJavaAPI
* Signature: (JIJ)J
*/
JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getElementConst
- (JNIEnv *, jobject, jlong, jint, jlong);
+ (JNIEnv *, jobject, jlong, jint, jlong);
/*
* Class: satune_SatuneJavaAPI
* Signature: (JJ)J
*/
JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getElementRange
- (JNIEnv *, jobject, jlong, jlong);
+ (JNIEnv *, jobject, jlong, jlong);
/*
* Class: satune_SatuneJavaAPI
* Signature: (JI)J
*/
JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getBooleanVar
- (JNIEnv *, jobject, jlong, jint);
+ (JNIEnv *, jobject, jlong, jint);
/*
* Class: satune_SatuneJavaAPI
* Signature: (J)J
*/
JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getBooleanTrue
- (JNIEnv *, jobject, jlong);
+ (JNIEnv *, jobject, jlong);
/*
* Class: satune_SatuneJavaAPI
* Signature: (J)J
*/
JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getBooleanFalse
- (JNIEnv *, jobject, jlong);
+ (JNIEnv *, jobject, jlong);
/*
* Class: satune_SatuneJavaAPI
* Signature: (JIJI)J
*/
JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createFunctionOperator
- (JNIEnv *, jobject, jlong, jint, jlong, jint);
+ (JNIEnv *, jobject, jlong, jint, jlong, jint);
/*
* Class: satune_SatuneJavaAPI
* Signature: (JI)J
*/
JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createPredicateOperator
- (JNIEnv *, jobject, jlong, jint);
+ (JNIEnv *, jobject, jlong, jint);
/*
* Class: satune_SatuneJavaAPI
* Signature: (JJI)J
*/
JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createPredicateTable
- (JNIEnv *, jobject, jlong, jlong, jint);
+ (JNIEnv *, jobject, jlong, jlong, jint);
/*
* Class: satune_SatuneJavaAPI
* Signature: (JJ)J
*/
JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createTable
- (JNIEnv *, jobject, jlong, jlong);
+ (JNIEnv *, jobject, jlong, jlong);
/*
* Class: satune_SatuneJavaAPI
* Signature: (J)J
*/
JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createTableForPredicate
- (JNIEnv *, jobject, jlong);
+ (JNIEnv *, jobject, jlong);
/*
* Class: satune_SatuneJavaAPI
* Signature: (JJJIJ)V
*/
JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_addTableEntry
- (JNIEnv *, jobject, jlong, jlong, jlong, jint, jlong);
+ (JNIEnv *, jobject, jlong, jlong, jlong, jint, jlong);
/*
* Class: satune_SatuneJavaAPI
* Signature: (JJI)J
*/
JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_completeTable
- (JNIEnv *, jobject, jlong, jlong, jint);
+ (JNIEnv *, jobject, jlong, jlong, jint);
/*
* Class: satune_SatuneJavaAPI
* Signature: (JJJIJ)J
*/
JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyFunction
- (JNIEnv *, jobject, jlong, jlong, jlong, jint, jlong);
+ (JNIEnv *, jobject, jlong, jlong, jlong, jint, jlong);
/*
* Class: satune_SatuneJavaAPI
* Signature: (JJJIJ)J
*/
JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyPredicateTable
- (JNIEnv *, jobject, jlong, jlong, jlong, jint, jlong);
+ (JNIEnv *, jobject, jlong, jlong, jlong, jint, jlong);
/*
* Class: satune_SatuneJavaAPI
* Signature: (JJJI)J
*/
JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyPredicate
- (JNIEnv *, jobject, jlong, jlong, jlong, jint);
+ (JNIEnv *, jobject, jlong, jlong, jlong, jint);
/*
* Class: satune_SatuneJavaAPI
* Signature: (JIJI)J
*/
JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyLogicalOperation
- (JNIEnv *, jobject, jlong, jint, jlong, jint);
+ (JNIEnv *, jobject, jlong, jint, jlong, jint);
/*
* Class: satune_SatuneJavaAPI
* Signature: (JIJJ)J
*/
JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyLogicalOperationTwo
- (JNIEnv *, jobject, jlong, jint, jlong, jlong);
+ (JNIEnv *, jobject, jlong, jint, jlong, jlong);
/*
* Class: satune_SatuneJavaAPI
* Signature: (JIJ)J
*/
JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyLogicalOperationOne
- (JNIEnv *, jobject, jlong, jint, jlong);
+ (JNIEnv *, jobject, jlong, jint, jlong);
/*
* Class: satune_SatuneJavaAPI
* Signature: (JJ)V
*/
JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_addConstraint
- (JNIEnv *, jobject, jlong, jlong);
+ (JNIEnv *, jobject, jlong, jlong);
/*
* Class: satune_SatuneJavaAPI
* Signature: (JJ)V
*/
JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_printConstraint
- (JNIEnv *, jobject, jlong, jlong);
+ (JNIEnv *, jobject, jlong, jlong);
/*
* Class: satune_SatuneJavaAPI
* Signature: (JIJ)J
*/
JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createOrder
- (JNIEnv *, jobject, jlong, jint, jlong);
+ (JNIEnv *, jobject, jlong, jint, jlong);
/*
* Class: satune_SatuneJavaAPI
* Signature: (JJJJ)J
*/
JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_orderConstraint
- (JNIEnv *, jobject, jlong, jlong, jlong, jlong);
+ (JNIEnv *, jobject, jlong, jlong, jlong, jlong);
/*
* Class: satune_SatuneJavaAPI
* Signature: (J)I
*/
JNIEXPORT jint JNICALL Java_satune_SatuneJavaAPI_solve
- (JNIEnv *, jobject, jlong);
+ (JNIEnv *, jobject, jlong);
/*
* Class: satune_SatuneJavaAPI
* Signature: (JJ)J
*/
JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getElementValue
- (JNIEnv *, jobject, jlong, jlong);
+ (JNIEnv *, jobject, jlong, jlong);
/*
* Class: satune_SatuneJavaAPI
* Signature: (JJ)I
*/
JNIEXPORT jint JNICALL Java_satune_SatuneJavaAPI_getBooleanValue
- (JNIEnv *, jobject, jlong, jlong);
+ (JNIEnv *, jobject, jlong, jlong);
/*
* Class: satune_SatuneJavaAPI
* Signature: (JJJJ)I
*/
JNIEXPORT jint JNICALL Java_satune_SatuneJavaAPI_getOrderConstraintValue
- (JNIEnv *, jobject, jlong, jlong, jlong, jlong);
+ (JNIEnv *, jobject, jlong, jlong, jlong, jlong);
/*
* Class: satune_SatuneJavaAPI
* Signature: (J)V
*/
JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_printConstraints
- (JNIEnv *, jobject, jlong);
+ (JNIEnv *, jobject, jlong);
/*
* Class: satune_SatuneJavaAPI
* Signature: (J)V
*/
JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_serialize
- (JNIEnv *, jobject, jlong);
+ (JNIEnv *, jobject, jlong);
/*
* Class: satune_SatuneJavaAPI
* Signature: (JJ)V
*/
JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_mustHaveValue
- (JNIEnv *, jobject, jlong, jlong);
+ (JNIEnv *, jobject, jlong, jlong);
/*
* Class: satune_SatuneJavaAPI
* Signature: (JI)V
*/
JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_setInterpreter
- (JNIEnv *, jobject, jlong, jint);
+ (JNIEnv *, jobject, jlong, jint);
/*
* Class: satune_SatuneJavaAPI
* Signature: (J)J
*/
JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_clone
- (JNIEnv *, jobject, jlong);
+ (JNIEnv *, jobject, jlong);
#ifdef __cplusplus
}
projects / satune.git / commitdiff