Adding SMT Interpreters

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

diff --git a/src/Interpreter/interpreter.h b/src/Interpreter/interpreter.h
index 814511bf5496543ec6534f2cb8486a2a268d5206..32eed4a0de824a1d63d021682e6cad3ae009dba6 100644 (file)
--- a/src/Interpreter/interpreter.h
+++ b/src/Interpreter/interpreter.h
@@ -3,6 +3,7 @@
 
 #include "classlist.h"
 #include "signatureenc.h"
+#include "signature.h"
 #include <iostream>
 #include <fstream>
 using namespace std;
@@ -15,6 +16,9 @@ public:
        void writeToFile(string str);
        uint64_t getValue(Element *element);
        bool getBooleanValue(Boolean *element);
+       virtual ValuedSignature *getBooleanSignature(uint id) = 0;
+       virtual ValuedSignature *getElementSignature(uint id, Signature *ssig) = 0;
+       virtual Signature *getSetSignature(uint id, Set *set) = 0;
        virtual ~Interpreter();
 protected:
        virtual void dumpFooter() = 0;
@@ -29,8 +33,8 @@ protected:
        virtual string encodeBooleanVar( BooleanVar *bv) = 0;
        string encodePredicate( BooleanPredicate *bp);
        string encodeOperatorPredicate(BooleanPredicate *constraint);
-       virtual string processElementFunction(ElementFunction *element, ElementSig *signature) = 0;
-       virtual string operatorPredicateConstraint(CompOp op, ElementSig *elemSig1, ElementSig *elemSig2) = 0;
+       virtual string processElementFunction(ElementFunction *element, ValuedSignature *signature) = 0;
+       virtual string operatorPredicateConstraint(CompOp op, ValuedSignature *elemSig1, ValuedSignature *elemSig2) = 0;
        CSolver *csolver;
        SignatureEnc sigEnc;
        ofstream output;