--- /dev/null
+#include "alloyenc.h"
+#include <string>
+#include "signatureenc.h"
+#include "structs.h"
+#include "csolver.h"
+#include "boolean.h"
+#include "predicate.h"
+#include "element.h"
+#include "signature.h"
+#include <fstream>
+#include <regex>
+
+using namespace std;
+
+const char * AlloyEnc::alloyFileName = "satune.als";
+const char * AlloyEnc::solutionFile = "solution.sol";
+
+AlloyEnc::AlloyEnc(CSolver *_solver):
+ csolver(_solver),
+ sigEnc(this)
+{
+ output.open(alloyFileName);
+ if(!output.is_open()){
+ model_print("AlloyEnc:Error in opening the dump file satune.als\n");
+ exit(-1);
+ }
+}
+
+AlloyEnc::~AlloyEnc(){
+ if(output.is_open()){
+ output.close();
+ }
+}
+
+void AlloyEnc::encode(){
+ SetIteratorBooleanEdge *iterator = csolver->getConstraints();
+ Vector<char *> facts;
+ while(iterator->hasNext()){
+ BooleanEdge constraint = iterator->next();
+ string constr = encodeConstraint(constraint);
+ //model_print("constr=%s\n", constr.c_str());
+ char *cstr = new char [constr.length()+1];
+ strcpy (cstr, constr.c_str());
+ facts.push(cstr);
+ }
+ output << "fact {" << endl;
+ for(uint i=0; i< facts.getSize(); i++){
+ char *cstr = facts.get(i);
+ writeToFile(cstr);
+ delete[] cstr;
+ }
+ output << "}" << endl;
+ delete iterator;
+}
+
+int AlloyEnc::getResult(){
+ ifstream input(solutionFile, ios::in);
+ string line;
+ while(getline(input, line)){
+ if(regex_match(line, regex("Unsatisfiable."))){
+ return IS_UNSAT;
+ }
+ if(regex_match(line, regex(".*Element\\d+.*value=.*Element\\d+.*->\\d+.*"))){
+ int tmp=0, index=0, value=0;
+ const char* s = line.c_str();
+ uint i1, i2, i3;
+ uint64_t i4;
+ if (4 == sscanf(s,"%*[^0123456789]%u%*[^0123456789]%d%*[^0123456789]%d%*[^0123456789]%" PRId64 "", &i1, &i2, &i3, &i4)){
+ model_print("Element%d = %" PRId64 "\n", i1, i4);
+ sigEnc.setValue(i1, i4);
+ }
+ }
+ }
+ return IS_SAT;
+}
+
+int AlloyEnc::solve(){
+ int result = IS_INDETER;
+ char buffer [512];
+ if( output.is_open()){
+ output.close();
+ }
+ snprintf(buffer, sizeof(buffer), "./run.sh java edu.mit.csail.sdg.alloy4whole.ExampleAlloyCompilerNoViz %s > %s", alloyFileName, solutionFile);
+ int status = system(buffer);
+ if (status == 0) {
+ //Read data in from results file
+ result = getResult();
+ }
+ return result;
+}
+
+string AlloyEnc::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;
+ }
+ default:
+ ASSERT(0);
+ }
+ if(c.isNegated()){
+ return "not ( " + res + " )";
+ }
+ return res;
+}
+
+string AlloyEnc::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));
+ switch (bl->op) {
+ case SATC_AND:{
+ ASSERT(size >= 2);
+ string res = "";
+ res += array[0];
+ for( uint i=1; i< size; i++){
+ res += " and " + array[i];
+ }
+ return res;
+ }
+ case SATC_NOT:{
+ return "not " + array[0];
+ }
+ case SATC_IFF:
+ return array[0] + " iff " + array[1];
+ case SATC_OR:
+ case SATC_XOR:
+ case SATC_IMPLIES:
+ default:
+ ASSERT(0);
+
+ }
+}
+
+string AlloyEnc::encodePredicate( BooleanPredicate *bp){
+ switch (bp->predicate->type) {
+ case TABLEPRED:
+ ASSERT(0);
+ case OPERATORPRED:
+ return encodeOperatorPredicate(bp);
+ default:
+ ASSERT(0);
+ }
+}
+
+string AlloyEnc::encodeOperatorPredicate(BooleanPredicate *constraint){
+ PredicateOperator *predicate = (PredicateOperator *) constraint->predicate;
+ ASSERT(constraint->inputs.getSize() == 2);
+ Element *elem0 = constraint->inputs.get(0);
+ ASSERT(elem0->type = ELEMSET);
+ ElementSig *elemSig1 = sigEnc.getElementSignature(elem0);
+ Element *elem1 = constraint->inputs.get(1);
+ ASSERT(elem1->type = ELEMSET);
+ ElementSig *elemSig2 = sigEnc.getElementSignature(elem1);
+ switch (predicate->getOp()) {
+ case SATC_EQUALS:
+ return *elemSig1 + " = " + *elemSig2;
+ case SATC_LT:
+ return *elemSig1 + " < " + *elemSig2;
+ case SATC_GT:
+ return *elemSig1 + " > " + *elemSig2;
+ default:
+ ASSERT(0);
+ }
+ exit(-1);
+}
+
+void AlloyEnc::writeToFile(string str){
+ output << str << endl;
+}
+
+uint64_t AlloyEnc::getValue(Element * element){
+ return sigEnc.getValue(element);
+}
+
--- /dev/null
+#ifndef ALLOYENC_H
+#define ALLOYENC_H
+
+#include "classlist.h"
+#include "signatureenc.h"
+#include <iostream>
+#include <fstream>
+using namespace std;
+
+class AlloyEnc{
+public:
+ AlloyEnc(CSolver *solver);
+ void encode();
+ int solve();
+ void writeToFile(string str);
+ uint64_t getValue(Element * element);
+ ~AlloyEnc();
+private:
+ string encodeConstraint(BooleanEdge constraint);
+ int getResult();
+ string encodeBooleanLogic( BooleanLogic *bl);
+ string encodePredicate( BooleanPredicate *bp);
+ string encodeOperatorPredicate(BooleanPredicate *constraint);
+ CSolver *csolver;
+ SignatureEnc sigEnc;
+ ofstream output;
+ static const char * alloyFileName;
+ static const char * solutionFile;
+};
+
+#endif
--- /dev/null
+#include "signature.h"
+#include "set.h"
+
+ElementSig::ElementSig(uint id, SetSig *_ssig):
+ Signature(id),
+ ssig(_ssig)
+{
+
+}
+
+string ElementSig::toString() const{
+ return "Element" + to_string(id) + ".value";
+}
+
+string ElementSig::getSignature() const{
+ return "one sig Element" + to_string(id) + " {\n\
+ value: Int\n\
+ }{\n\
+ value in " + *ssig + "\n\
+ }";
+
+}
+
+SetSig::SetSig(uint id, Set *set): Signature(id){
+ ASSERT(set->getSize() > 0);
+ domain = to_string(set->getElement(0));
+ for(uint i=1; i< set->getSize(); i++){
+ domain += " + " + to_string(set->getElement(i));
+ }
+}
+
+string SetSig::toString() const{
+ return "Set" + to_string(id) + ".domain";
+}
+
+string SetSig::getSignature() const{
+ return "one sig Set" + to_string(id) + " {\n\
+ domain: set Int\n\
+ }{\n\
+ domain = " + domain + "\n\
+ }";
+
+}
+
+string Signature::operator+(const string& str){
+ return toString() + str;
+}
+
+string operator+(const string& str, const Signature& sig){
+ return str + sig.toString();
+}
--- /dev/null
+#ifndef ELEMENTSIG_H
+#define ELEMENTSIG_H
+#include <string>
+#include <iostream>
+#include "classlist.h"
+using namespace std;
+
+class Signature{
+public:
+ Signature(uint _id):id(_id){}
+ string operator+(const string& s);
+ virtual string toString() const = 0;
+ virtual string getSignature() const =0;
+ virtual ~Signature(){}
+protected:
+ uint id;
+};
+
+class SetSig: public Signature{
+public:
+ SetSig(uint id, Set *set);
+ virtual ~SetSig(){}
+ virtual string toString() const;
+ virtual string getSignature() const;
+private:
+ string domain;
+};
+
+class ElementSig: public Signature{
+public:
+ ElementSig(uint id, SetSig *ssig);
+ uint64_t getValue() { return value;}
+ void setValue(uint64_t v){value = v;}
+ virtual ~ElementSig(){}
+ virtual string toString() const;
+ virtual string getSignature() const;
+private:
+ SetSig *ssig;
+ uint64_t value;
+};
+
+string operator+(const string& str, const Signature& sig);
+
+#endif
--- /dev/null
+#include "signatureenc.h"
+#include "element.h"
+#include "set.h"
+#include "signature.h"
+#include "alloyenc.h"
+
+SignatureEnc::SignatureEnc(AlloyEnc *ae): alloyEncoder(ae){
+}
+
+SignatureEnc::~SignatureEnc(){
+ for(uint i=0; i<signatures.getSize(); i++){
+ Signature *s = signatures.get(i);
+ delete s;
+ }
+}
+
+ElementSig *SignatureEnc::getElementSignature(Element *element){
+ ElementSig *esig = (ElementSig *)encoded.get((void *)element);
+ if(esig == NULL){
+ Set *set = element->getRange();
+ SetSig *ssig = (SetSig *)encoded.get((void *)set);
+ if(ssig == NULL){
+ ssig = new SetSig(signatures.getSize(), set);
+ encoded.put(set, ssig);
+ signatures.push(ssig);
+ alloyEncoder->writeToFile(ssig->getSignature());
+ }
+ esig = new ElementSig(signatures.getSize(), ssig);
+ encoded.put(element, esig);
+ signatures.push(esig);
+ alloyEncoder->writeToFile(esig->getSignature());
+
+ }
+ return esig;
+}
+
+void SignatureEnc::setValue(uint id, uint64_t value){
+ ElementSig *sig = (ElementSig *)signatures.get(id);
+ sig->setValue(value);
+}
+
+uint64_t SignatureEnc::getValue(Element *element){
+ ElementSig *sig = (ElementSig *)encoded.get((void *) element);
+ ASSERT(sig != NULL);
+ return sig->getValue();
+}
--- /dev/null
+#ifndef SIGNATUREENC_H
+#define SIGNATUREENC_H
+
+#include "classlist.h"
+#include "structs.h"
+#include "cppvector.h"
+
+class SignatureEnc {
+public:
+ SignatureEnc(AlloyEnc *_alloyEncoder);
+ ~SignatureEnc();
+ void setValue(uint id, uint64_t value);
+ ElementSig *getElementSignature(Element *element);
+ uint64_t getValue(Element *element);
+private:
+ CloneMap encoded;
+ Vector<Signature*> signatures;
+ AlloyEnc *alloyEncoder;
+};
+#endif
MKDIR_P = mkdir -p
OBJ_DIR = bin
-CPP_SOURCES := $(wildcard *.cc) $(wildcard AST/*.cc) $(wildcard ASTTransform/*.cc) $(wildcard Translator/*.cc) $(wildcard ASTAnalyses/*.cc) $(wildcard ASTAnalyses/Order/*.cc) $(wildcard ASTAnalyses/Encoding/*.cc) $(wildcard ASTAnalyses/Polarity/*.cc) $(wildcard Tuner/*.cc) $(wildcard Collections/*.cc) $(wildcard Backend/*.cc) $(wildcard Encoders/*.cc) $(wildcard Serialize/*.cc)
+CPP_SOURCES := $(wildcard *.cc) $(wildcard AST/*.cc) $(wildcard ASTTransform/*.cc) $(wildcard Translator/*.cc) $(wildcard ASTAnalyses/*.cc) $(wildcard ASTAnalyses/Order/*.cc) $(wildcard ASTAnalyses/Encoding/*.cc) $(wildcard ASTAnalyses/Polarity/*.cc) $(wildcard Tuner/*.cc) $(wildcard Collections/*.cc) $(wildcard Backend/*.cc) $(wildcard Encoders/*.cc) $(wildcard Serialize/*.cc) $(wildcard AlloyEnc/*.cc)
-C_SOURCES := $(wildcard *.c) $(wildcard AST/*.c) $(wildcard ASTTransform/*.c) $(wildcard Translator/*.c) $(wildcard ASTAnalyses/*.c) $(wildcard ASTAnalyses/Order/*.c) $(wildcard ASTAnalyses/Encoding/*.c) $(wildcard ASTAnalyses/Polarity/*.c) $(wildcard Tuner/*.c) $(wildcard Collections/*.c) $(wildcard Backend/*.c) $(wildcard Encoders/*.c) $(wildcard Serialize/*.c)
+C_SOURCES := $(wildcard *.c) $(wildcard AST/*.c) $(wildcard ASTTransform/*.c) $(wildcard Translator/*.c) $(wildcard ASTAnalyses/*.c) $(wildcard ASTAnalyses/Order/*.c) $(wildcard ASTAnalyses/Encoding/*.c) $(wildcard ASTAnalyses/Polarity/*.c) $(wildcard Tuner/*.c) $(wildcard Collections/*.c) $(wildcard Backend/*.c) $(wildcard Encoders/*.c) $(wildcard Serialize/*.c) $(wildcard AlloyEnc/*.c)
-HEADERS := $(wildcard *.h) $(wildcard AST/*.h) $(wildcard ASTTransform/*.h) $(wildcard Translator/*.h) $(wildcard ASTAnalyses/*.h) $(wildcard ASTAnalyses/Order/*.h) $(wildcard ASTAnalyses/Encoding/*.h) $(wildcard ASTAnalyses/Polarity/*.h) $(wildcard Tuner/*.h) $(wildcard Collections/*.h) $(wildcard Backend/*.h) $(wildcard Encoders/*.h) $(wildcard Serialize/*.h)
+HEADERS := $(wildcard *.h) $(wildcard AST/*.h) $(wildcard ASTTransform/*.h) $(wildcard Translator/*.h) $(wildcard ASTAnalyses/*.h) $(wildcard ASTAnalyses/Order/*.h) $(wildcard ASTAnalyses/Encoding/*.h) $(wildcard ASTAnalyses/Polarity/*.h) $(wildcard Tuner/*.h) $(wildcard Collections/*.h) $(wildcard Backend/*.h) $(wildcard Encoders/*.h) $(wildcard Serialize/*.h) $(wildcard AlloyEnc/*.h)
OBJECTS := $(CPP_SOURCES:%.cc=$(OBJ_DIR)/%.o) $(C_SOURCES:%.c=$(OBJ_DIR)/%.o)
CFLAGS := -Wall -O0 -g
CXXFLAGS := -std=c++1y -pthread
-CFLAGS += -IAST -IASTTransform -IASTAnalyses -IASTAnalyses/Polarity -IASTAnalyses/Order -IASTAnalyses/Encoding -ITranslator -ICollections -IBackend -I. -IEncoders -ITuner -ISerialize
+CFLAGS += -IAST -IASTTransform -IASTAnalyses -IASTAnalyses/Polarity -IASTAnalyses/Order -IASTAnalyses/Encoding -ITranslator -ICollections -IBackend -I. -IEncoders -ITuner -ISerialize -IAlloyEnc
LDFLAGS := -ldl -lrt -rdynamic -g
SHARED := -shared
${MKDIR_P} ${OBJ_DIR}/Backend
${MKDIR_P} ${OBJ_DIR}/Encoders
${MKDIR_P} ${OBJ_DIR}/Serialize
+ ${MKDIR_P} ${OBJ_DIR}/AlloyEnc
debug: CFLAGS += -DCONFIG_DEBUG
debug: all
--- /dev/null
+#include "csolver.h"
+
+
+int main(int argc, char **argv) {
+ printf("%d\n", argc);
+ if (argc != 2 && argc != 3) {
+ printf("You only specify the name of the file ...\n");
+ printf("./run.sh deserializer test.dump [--alloy]\n");
+ exit(-1);
+ }
+ CSolver *solver = CSolver::deserialize(argv[1]);
+ if(argc == 3)
+ solver->setAlloyEncode();
+ int value = solver->solve();
+ if (value == 1) {
+ printf("%s is SAT\n", argv[1]);
+ } else {
+ printf("%s is UNSAT\n", argv[1]);
+ }
+ delete solver;
+ return 1;
+
+}
+++ /dev/null
-#include "csolver.h"
-
-
-int main(int argc, char **argv) {
- if (argc != 2) {
- printf("You only specify the name of the file ...");
- exit(-1);
- }
- CSolver *solver = CSolver::deserialize(argv[1]);
- solver->printConstraints();
- delete solver;
- return 1;
-
-}
#!/bin/bash
+export CLASSPATH=../bin/original.jar:.:$CLASSPATH
export LD_LIBRARY_PATH=../bin
# For Mac OSX
export DYLD_LIBRARY_PATH=../bin
CCSOLVER(solver)->mustHaveValue( (Element *) element);
}
+void setAlloyEncode(void *solver){
+ CCSOLVER(solver)->setAlloyEncode();
+}
+
void *clone(void *solver) {
return CCSOLVER(solver)->clone();
}
\ No newline at end of file
void printConstraints(void *solver);
void serialize(void *solver);
void mustHaveValue(void *solver, void *element);
+void setAlloyEncode(void *solver);
void *clone(void *solver);
#ifdef __cplusplus
}
class BooleanLogic;
class Serializer;
class ElementFunction;
+class AlloyEnc;
typedef uint64_t VarType;
typedef unsigned int uint;
class EncodingNode;
class EncodingEdge;
class EncodingSubGraph;
-
+class SignatureEnc;
+class Signature;
+class ElementSig;
+class SetSig;
struct IncrementalSolver;
typedef struct IncrementalSolver IncrementalSolver;
struct TableEntry;
#include "varorderingopt.h"
#include <time.h>
#include <stdarg.h>
+#include "alloyenc.h"
CSolver::CSolver() :
boolTrue(BooleanEdge(new BooleanConst(true))),
booleanVarUsed(false),
tuner(NULL),
elapsedTime(0),
- satsolverTimeout(NOTIMEOUT)
+ satsolverTimeout(NOTIMEOUT),
+ alloyEncoder(NULL)
{
satEncoder = new SATEncoder(this);
}
model_print("Elapse Encode time: %f\n", (time1 - startTime) / NANOSEC);
model_print("Is problem UNSAT after encoding: %d\n", unsat);
- int 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");
- time2 = getTimeNano();
- elapsedTime = time2 - startTime;
- model_print("CSOLVER solve time: %f\n", elapsedTime / NANOSEC);
+ int result = IS_INDETER;
+ if(alloyEncoder != NULL){
+ alloyEncoder->encode();
+ result = alloyEncoder->solve();
+ }else{
+ 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");
+ time2 = getTimeNano();
+ elapsedTime = time2 - startTime;
+ model_print("CSOLVER solve time: %f\n", elapsedTime / NANOSEC);
+ }
if (deleteTuner) {
delete tuner;
tuner = NULL;
return result;
}
+void CSolver::setAlloyEncode(){
+ alloyEncoder = new AlloyEnc(this);
+}
+
void CSolver::printConstraints() {
SetIteratorBooleanEdge *it = getConstraints();
while (it->hasNext()) {
case ELEMSET:
case ELEMCONST:
case ELEMFUNCRETURN:
- return getElementValueSATTranslator(this, element);
+ return alloyEncoder == NULL? getElementValueSATTranslator(this, element):
+ alloyEncoder->getValue(element);
default:
ASSERT(0);
}
void autoTune(uint budget);
void inferFixedOrders();
void inferFixedOrder(Order *order);
-
+ void setAlloyEncode();
void setTuner(Tuner *_tuner) { tuner = _tuner; }
long long getElapsedTime() { return elapsedTime; }
Tuner *tuner;
long long elapsedTime;
long satsolverTimeout;
+ AlloyEnc *alloyEncoder;
friend class ElementOpt;
friend class VarOrderingOpt;
};
csolverlb.clone.restype = c_void_p
csolverlb.serialize.argtypes = [c_void_p]
csolverlb.serialize.restype = None
+ csolverlb.setAlloyEncode.argtypes = [c_void_p]
+ csolverlb.setAlloyEncode.restype = None
return csolverlb
projects / satune.git / commitdiff