1 2 /* 3 * File SMTFormula.hpp. 4 * 5 * This file is part of the source code of the software program 6 * Vampire. It is protected by applicable 7 * copyright laws. 8 * 9 * This source code is distributed under the licence found here 10 * https://vprover.github.io/license.html 11 * and in the source directory 12 * 13 * In summary, you are allowed to use Vampire for non-commercial 14 * purposes but not allowed to distribute, modify, copy, create derivatives, 15 * or use in competitions. 16 * For other uses of Vampire please contact developers for a different 17 * licence, which we will make an effort to provide. 18 */ 19 /** 20 * @file SMTFormula.hpp 21 * Defines class SMTFormula. 22 */ 23 24 #ifndef __SMTFormula__ 25 #define __SMTFormula__ 26 27 #include <iosfwd> 28 29 #include "Forwards.hpp" 30 31 #include "Lib/DHMap.hpp" 32 #include "Lib/DHSet.hpp" 33 #include "Lib/Stack.hpp" 34 35 namespace Shell { 36 37 using namespace Lib; 38 39 class SMTConstant; 40 41 42 struct SMTFormula__HalfImpl; 43 struct SMTFormula__HalfEquiv; 44 45 class SMTFormula 46 { 47 protected: SMTFormula(vstring val)48 SMTFormula(vstring val) : _val(val) {} 49 public: getTrue()50 static SMTFormula getTrue() { return SMTFormula("true"); } getFalse()51 static SMTFormula getFalse() { return SMTFormula("false"); } 52 53 static SMTConstant unsignedValue(unsigned val); 54 static SMTConstant name(vstring name); 55 static SMTConstant name(vstring n1, vstring n2); 56 equals(SMTFormula f1,SMTFormula f2)57 static SMTFormula equals(SMTFormula f1, SMTFormula f2) 58 { return SMTFormula("(= " + f1._val + " " + f2._val + ")"); } 59 less(SMTFormula f1,SMTFormula f2)60 static SMTFormula less(SMTFormula f1, SMTFormula f2) 61 { return SMTFormula("(< " + f1._val + " " + f2._val + ")"); } 62 63 static SMTFormula condNumber(SMTFormula condition, unsigned value); 64 multiply(SMTFormula f1,SMTFormula f2)65 static SMTFormula multiply(SMTFormula f1, SMTFormula f2) 66 { return SMTFormula("(* " + f1._val + " " + f2._val + ")"); } 67 add(SMTFormula f1,SMTFormula f2)68 static SMTFormula add(SMTFormula f1, SMTFormula f2) 69 { return SMTFormula("(+ " + f1._val + " " + f2._val + ")"); } 70 71 static SMTFormula conjunction(const SMTFormula& f1, const SMTFormula& f2); 72 static SMTFormula disjunction(const SMTFormula& f1, const SMTFormula& f2); 73 74 isTrue() const75 bool isTrue() const { return _val=="true"; } isFalse() const76 bool isFalse() const { return _val=="false"; } 77 operator vstring() const78 operator vstring() const { return _val; } 79 operator !() const80 SMTFormula operator!() const 81 { return SMTFormula("(not " + _val + ")"); } 82 operator &(const SMTFormula & f) const83 SMTFormula operator&(const SMTFormula& f) const 84 { return conjunction(*this, f); } 85 operator |(const SMTFormula & f) const86 SMTFormula operator|(const SMTFormula& f) const 87 { return disjunction(*this, f); } 88 89 90 //this is to allow having --> stand for an implication 91 SMTFormula__HalfImpl operator--(int) const; 92 93 //these are to allow having -=- stand for an equivalence 94 SMTFormula__HalfEquiv operator-() const; 95 SMTFormula operator-=(const SMTFormula__HalfEquiv& r) const; 96 97 toString() const98 vstring toString() const { return _val; } 99 private: 100 friend struct SMTFormula__HalfImpl; 101 friend struct SMTFormula__HalfEquiv; 102 103 vstring _val; 104 }; 105 106 //the following is to allow having --> stand for an implication 107 struct SMTFormula__HalfImpl { operator >Shell::SMTFormula__HalfImpl108 SMTFormula operator>(const SMTFormula& r) const 109 { return SMTFormula("(implies " + pf._val + " " + r._val + ")"); } 110 private: 111 friend class SMTFormula; SMTFormula__HalfImplShell::SMTFormula__HalfImpl112 SMTFormula__HalfImpl(const SMTFormula& pf) : pf(pf) {} 113 SMTFormula pf; 114 }; 115 116 //the following is to allow having -=- stand for an equivalence 117 struct SMTFormula__HalfEquiv { 118 private: 119 friend class SMTFormula; SMTFormula__HalfEquivShell::SMTFormula__HalfEquiv120 SMTFormula__HalfEquiv(const SMTFormula& pf) : pf(pf) {} 121 SMTFormula pf; 122 }; 123 124 125 class SMTConstant : public SMTFormula 126 { 127 friend class SMTFormula; 128 SMTConstant(vstring val)129 SMTConstant(vstring val) : SMTFormula(val) {} 130 }; 131 132 133 class SMTBenchmark 134 { 135 public: 136 137 void declarePropositionalConstant(SMTConstant pred); 138 void declareRealConstant(SMTConstant pred); 139 140 void addFormula(const SMTFormula& f, vstring comment=""); 141 void popFormula(); 142 143 void output(ostream& out); 144 private: 145 typedef DHSet<vstring> StringSet; 146 typedef DHMap<vstring,vstring> StringMap; 147 148 StringSet _predDecls; 149 StringMap _funDecls; 150 151 Stack<SMTFormula> _formulas; 152 Stack<vstring> _formulaComments; 153 }; 154 155 class SMTSolverResult 156 { 157 public: 158 enum Status 159 { 160 SAT, UNSAT, UNKNOWN 161 }; 162 163 Status status; 164 DHMap<vstring,vstring> assignment; 165 reset()166 void reset() 167 { 168 status = UNKNOWN; 169 assignment.reset(); 170 } 171 }; 172 173 class SMTSolver 174 { 175 public: ~SMTSolver()176 virtual ~SMTSolver() {} 177 run(SMTBenchmark & problem,SMTSolverResult & res)178 void run(SMTBenchmark& problem, SMTSolverResult& res) 179 { 180 run(problem, res, 0); 181 } 182 183 enum MinimizationResult 184 { 185 EXACT, 186 APPROXIMATE, 187 FAIL 188 }; 189 190 /** 191 * timeout equal to 0 means unlimited 192 */ 193 virtual void run(SMTBenchmark& problem, SMTSolverResult& res, unsigned timeout) = 0; 194 195 MinimizationResult minimize(SMTBenchmark& problem, SMTConstant costFn, SMTSolverResult& res); 196 197 private: 198 SMTSolverResult::Status tryUpperBound(SMTBenchmark& problem, SMTConstant costFn, unsigned val, SMTSolverResult& res); 199 }; 200 201 class YicesSolver : public SMTSolver 202 { 203 public: 204 virtual void run(SMTBenchmark& problem, SMTSolverResult& res, unsigned timeout); 205 }; 206 207 } 208 209 #endif // __SMTFormula__ 210