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