Adding SMT Interpreters

[satune.git] / src / Interpreter / alloyinterpreter.h

diff --git a/src/Interpreter/alloyinterpreter.h b/src/Interpreter/alloyinterpreter.h
index ec2e4a3f9dc120d780f437a79d16172d8e627d15..e4a1e3b0531761aa33bde0e41868a163d7b57d3a 100644 (file)
--- a/src/Interpreter/alloyinterpreter.h
+++ b/src/Interpreter/alloyinterpreter.h
@@ -1,5 +1,5 @@
-#ifndef ALLOYENC_H
-#define ALLOYENC_H
+#ifndef ALLOYINTERPRETER_H
+#define ALLOYINTERPRETER_H
 
 #include "classlist.h"
 #include "signatureenc.h"
@@ -10,10 +10,14 @@
 class AlloyInterpreter: public Interpreter{
 public:
        AlloyInterpreter(CSolver *solver);
+       virtual ValuedSignature *getBooleanSignature(uint id);
+       virtual ValuedSignature *getElementSignature(uint id, Signature *ssig);
+       virtual Signature *getSetSignature(uint id, Set *set);
        virtual ~AlloyInterpreter();
 protected:
        virtual void dumpFooter();
        virtual void dumpHeader();
+       int getAlloyIntScope();
        virtual void compileRunCommand(char * command , size_t size);
        virtual int getResult();
        virtual void dumpAllConstraints(Vector<char *> &facts);
@@ -21,8 +25,8 @@ protected:
        virtual string encodeBooleanLogic( BooleanLogic *bl);
        virtual string encodeBooleanVar( BooleanVar *bv);
        string encodeOperatorPredicate(BooleanPredicate *constraint);
-       virtual string processElementFunction(ElementFunction *element, ElementSig *signature);
-       virtual string operatorPredicateConstraint(CompOp op, ElementSig *elemSig1, ElementSig *elemSig2);
+       virtual string processElementFunction(ElementFunction *element, ValuedSignature *signature);
+       virtual string operatorPredicateConstraint(CompOp op, ValuedSignature *elemSig1, ValuedSignature *elemSig2);
 };
 
 #endif