Adding SMTRat and MathSAT interpreters

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

diff --git a/src/Interpreter/smtinterpreter.h b/src/Interpreter/smtinterpreter.h
index ac62fd712f4128d3e71b43f6d705239785cb2e75..035e76be8c2efd19b1d609117033305352d55e70 100644 (file)
--- a/src/Interpreter/smtinterpreter.h
+++ b/src/Interpreter/smtinterpreter.h
@@ -7,6 +7,9 @@
 #include <iostream>
 #include <fstream>
 
 #include <iostream>
 #include <fstream>
 

+#define SMTFILENAME "satune.smt"
+#define SMTSOLUTIONFILE "solution.sol"
+

 class SMTInterpreter: public Interpreter{
 public:
        SMTInterpreter(CSolver *solver);
 class SMTInterpreter: public Interpreter{
 public:
        SMTInterpreter(CSolver *solver);


@@ -23,7 +26,7 @@ protected:
        virtual string negateConstraint(string constr);
        virtual string encodeBooleanLogic( BooleanLogic *bl);
        virtual string encodeBooleanVar( BooleanVar *bv);
        virtual string negateConstraint(string constr);
        virtual string encodeBooleanLogic( BooleanLogic *bl);
        virtual string encodeBooleanVar( BooleanVar *bv);

-       void extractValue(char *idline, char *valueline);
+       virtual void extractValue(char *idline, char *valueline);

        virtual string processElementFunction(ElementFunction *element, ValuedSignature *signature);
        virtual string operatorPredicateConstraint(CompOp op, ValuedSignature *elemSig1, ValuedSignature *elemSig2);
 };
        virtual string processElementFunction(ElementFunction *element, ValuedSignature *signature);
        virtual string operatorPredicateConstraint(CompOp op, ValuedSignature *elemSig1, ValuedSignature *elemSig2);
 };