projects
/
satune.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
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 "classlist.h"
#include "signatureenc.h"
+#include "signature.h"
#include <iostream>
#include <fstream>
using namespace std;
#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);
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;
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 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;
CSolver *csolver;
SignatureEnc sigEnc;
ofstream output;