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
/
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 ALLOY
ENC
_H
-#define ALLOY
ENC
_H
+#ifndef ALLOY
INTERPRETER
_H
+#define ALLOY
INTERPRETER
_H
#include "classlist.h"
#include "signatureenc.h"
#include "classlist.h"
#include "signatureenc.h"
@@
-10,10
+10,14
@@
class AlloyInterpreter: public Interpreter{
public:
AlloyInterpreter(CSolver *solver);
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();
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);
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 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
};
#endif