src/Interpreter/smtinterpreter.h

   1 #ifndef SMTINTERPRETER_H
   2 #define SMTINTERPRETER_H
   3
   4 #include "classlist.h"
   5 #include "signatureenc.h"
   6 #include "interpreter.h"
   7 #include <iostream>
   8 #include <fstream>
   9
  10 #define SMTFILENAME "satune.smt"
  11 #define SMTSOLUTIONFILE "solution.sol"
  12
  13 class SMTInterpreter: public Interpreter{
  14 public:
  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();
  20 protected:
  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);
  32 };
  33
  34 #endif