1 #ifndef SMTINTERPRETER_H
2 #define SMTINTERPRETER_H
5 #include "signatureenc.h"
6 #include "interpreter.h"
10 #define SMTFILENAME "satune.smt"
11 #define SMTSOLUTIONFILE "solution.sol"
13 class SMTInterpreter : public Interpreter {
15 SMTInterpreter(CSolver *solver);
16 virtual ValuedSignature *getBooleanSignature(uint id);
17 virtual ValuedSignature *getElementSignature(uint id, Signature *ssig);
18 virtual Signature *getSetSignature(uint id, Set *set);
19 virtual ~SMTInterpreter();
21 virtual void dumpFooter();
22 virtual void dumpHeader();
23 virtual void compileRunCommand(char *command, size_t size);
24 virtual int getResult();
25 virtual void dumpAllConstraints(Vector<char *> &facts);
26 virtual string negateConstraint(string constr);
27 virtual string encodeBooleanLogic( BooleanLogic *bl);
28 virtual string encodeBooleanVar( BooleanVar *bv);
29 virtual void extractValue(char *idline, char *valueline);
30 virtual string processElementFunction(ElementFunction *element, ValuedSignature *signature);
31 virtual string operatorPredicateConstraint(CompOp op, ValuedSignature *elemSig1, ValuedSignature *elemSig2);