Alloy interpreter
authorHamed Gorjiara <hgorjiar@uci.edu>
Tue, 22 Jan 2019 08:20:39 +0000 (00:20 -0800)
committerHamed Gorjiara <hgorjiar@uci.edu>
Tue, 22 Jan 2019 08:20:39 +0000 (00:20 -0800)
17 files changed:
src/AlloyEnc/alloyenc.cc [new file with mode: 0644]
src/AlloyEnc/alloyenc.h [new file with mode: 0644]
src/AlloyEnc/signature.cc [new file with mode: 0644]
src/AlloyEnc/signature.h [new file with mode: 0644]
src/AlloyEnc/signatureenc.cc [new file with mode: 0644]
src/AlloyEnc/signatureenc.h [new file with mode: 0644]
src/Makefile
src/Test/deserializealloytest.cc [new file with mode: 0644]
src/Test/deserializertest.cc [deleted file]
src/Test/run.sh
src/ccsolver.cc
src/ccsolver.h
src/classes.h
src/classlist.h
src/csolver.cc
src/csolver.h
src/pycsolver.py

diff --git a/src/AlloyEnc/alloyenc.cc b/src/AlloyEnc/alloyenc.cc
new file mode 100644 (file)
index 0000000..c7acf23
--- /dev/null
@@ -0,0 +1,182 @@
+#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);
+}
+
diff --git a/src/AlloyEnc/alloyenc.h b/src/AlloyEnc/alloyenc.h
new file mode 100644 (file)
index 0000000..94d991e
--- /dev/null
@@ -0,0 +1,31 @@
+#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
diff --git a/src/AlloyEnc/signature.cc b/src/AlloyEnc/signature.cc
new file mode 100644 (file)
index 0000000..9b02d32
--- /dev/null
@@ -0,0 +1,51 @@
+#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();
+}
diff --git a/src/AlloyEnc/signature.h b/src/AlloyEnc/signature.h
new file mode 100644 (file)
index 0000000..6dcb2e9
--- /dev/null
@@ -0,0 +1,44 @@
+#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
diff --git a/src/AlloyEnc/signatureenc.cc b/src/AlloyEnc/signatureenc.cc
new file mode 100644 (file)
index 0000000..4c11957
--- /dev/null
@@ -0,0 +1,46 @@
+#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();
+}
diff --git a/src/AlloyEnc/signatureenc.h b/src/AlloyEnc/signatureenc.h
new file mode 100644 (file)
index 0000000..d98a636
--- /dev/null
@@ -0,0 +1,20 @@
+#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
index 838a478..457ca9a 100644 (file)
@@ -4,17 +4,17 @@ PHONY += directories
 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
 
@@ -44,6 +44,7 @@ ${OBJ_DIR}:
        ${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
diff --git a/src/Test/deserializealloytest.cc b/src/Test/deserializealloytest.cc
new file mode 100644 (file)
index 0000000..2d6cc25
--- /dev/null
@@ -0,0 +1,23 @@
+#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;
+
+}
diff --git a/src/Test/deserializertest.cc b/src/Test/deserializertest.cc
deleted file mode 100644 (file)
index c8d35c9..0000000
+++ /dev/null
@@ -1,14 +0,0 @@
-#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;
-
-}
index 4590ede..870ba15 100755 (executable)
@@ -1,5 +1,6 @@
 #!/bin/bash
 
+export CLASSPATH=../bin/original.jar:.:$CLASSPATH
 export LD_LIBRARY_PATH=../bin
 # For Mac OSX
 export DYLD_LIBRARY_PATH=../bin
index f9ebdbb..69d002e 100644 (file)
@@ -145,6 +145,10 @@ void mustHaveValue(void *solver, void *element) {
        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
index c88214e..b4a803a 100644 (file)
@@ -41,6 +41,7 @@ int getOrderConstraintValue(void *solver,void *order, long first, long second);
 void printConstraints(void *solver);
 void serialize(void *solver);
 void mustHaveValue(void *solver, void *element);
+void setAlloyEncode(void *solver);
 void *clone(void *solver);
 #ifdef __cplusplus
 }
index 58f5a02..6f476ee 100644 (file)
@@ -28,6 +28,7 @@ class Set;
 class BooleanLogic;
 class Serializer;
 class ElementFunction;
+class AlloyEnc;
 
 typedef uint64_t VarType;
 typedef unsigned int uint;
index c182063..3986a30 100644 (file)
@@ -72,7 +72,10 @@ class EncodingGraph;
 class EncodingNode;
 class EncodingEdge;
 class EncodingSubGraph;
-
+class SignatureEnc;
+class Signature;
+class ElementSig;
+class SetSig;
 struct IncrementalSolver;
 typedef struct IncrementalSolver IncrementalSolver;
 struct TableEntry;
index 45163be..a8eb999 100644 (file)
@@ -29,6 +29,7 @@
 #include "varorderingopt.h"
 #include <time.h>
 #include <stdarg.h>
+#include "alloyenc.h"
 
 CSolver::CSolver() :
        boolTrue(BooleanEdge(new BooleanConst(true))),
@@ -37,7 +38,8 @@ CSolver::CSolver() :
        booleanVarUsed(false),
        tuner(NULL),
        elapsedTime(0),
-       satsolverTimeout(NOTIMEOUT)
+       satsolverTimeout(NOTIMEOUT),
+       alloyEncoder(NULL)
 {
        satEncoder = new SATEncoder(this);
 }
@@ -638,11 +640,17 @@ int CSolver::solve() {
        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;
@@ -650,6 +658,10 @@ int CSolver::solve() {
        return result;
 }
 
+void CSolver::setAlloyEncode(){
+       alloyEncoder = new AlloyEnc(this);
+}
+
 void CSolver::printConstraints() {
        SetIteratorBooleanEdge *it = getConstraints();
        while (it->hasNext()) {
@@ -668,7 +680,8 @@ uint64_t CSolver::getElementValue(Element *element) {
        case ELEMSET:
        case ELEMCONST:
        case ELEMFUNCRETURN:
-               return getElementValueSATTranslator(this, element);
+               return alloyEncoder == NULL? getElementValueSATTranslator(this, element):
+                       alloyEncoder->getValue(element);
        default:
                ASSERT(0);
        }
index c604486..0dc3cef 100644 (file)
@@ -165,7 +165,7 @@ public:
        void autoTune(uint budget);
        void inferFixedOrders();
        void inferFixedOrder(Order *order);
-
+       void setAlloyEncode();
 
        void setTuner(Tuner *_tuner) { tuner = _tuner; }
        long long getElapsedTime() { return elapsedTime; }
@@ -222,6 +222,7 @@ private:
         Tuner *tuner;
        long long elapsedTime;
        long satsolverTimeout;
+       AlloyEnc *alloyEncoder;
        friend class ElementOpt;
        friend class VarOrderingOpt;
 };
index b0e43a9..da911db 100644 (file)
@@ -113,5 +113,7 @@ def loadCSolver():
        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