1
2 /*
3 * File SMTLIBConcat.cpp.
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 SMTLIBConcat.cpp
21 * Implements class SMTLIBConcat.
22 */
23
24 #include <fstream>
25
26 #include "Lib/DHSet.hpp"
27 #include "Lib/Int.hpp"
28 #include "Lib/Stack.hpp"
29 #include "Lib/System.hpp"
30
31 #include "Shell/LispLexer.hpp"
32
33 #include "SMTLIBConcat.hpp"
34
35 namespace VUtils
36 {
37
perform(int argc,char ** argv)38 int SMTLIBConcat::perform(int argc, char** argv)
39 {
40 CALL("SMTLIBConcat::perform");
41
42 Stack<LExpr*> benchExprs;
43
44 for(int i=2; i<argc; i++) {
45 LExpr* bench = parseFile(argv[i]);
46 benchExprs.push(bench);
47 }
48
49 LExpr* merged = mergeBenchmarksIntoSmtlib2(benchExprs);
50
51 rewriteIntsToReals(merged);
52
53 // LExpr* converted = smtlibToSmtlib2(merged);
54
55 cout << merged->toString(false) << endl;
56
57 return 0;
58 }
59
extrafuns2decl(LExpr * expr)60 LExpr* SMTLIBConcat::extrafuns2decl(LExpr* expr)
61 {
62 CALL("SMTLIBConcat::extrafuns2decl");
63
64 //TODO: currently we handle only constants (on non-constants should fail)
65 LispListReader tlRdr(expr);
66 LispListWriter res;
67 res << "declare-fun"
68 << tlRdr.readAtom();
69 res << (LispListWriter())
70 << tlRdr.readAtom();
71 if(tlRdr.hasNext()) {
72 USER_ERROR("non-constant functions not supported: "+expr->toString());
73 }
74 tlRdr.acceptEOL();
75 return res.get();
76 }
77
rewriteSmt1FormToSmt2(LExpr * e0)78 void SMTLIBConcat::rewriteSmt1FormToSmt2(LExpr* e0)
79 {
80 CALL("SMTLIBConcat::rewriteSmt1FormToSmt2");
81
82 Stack<LExpr*> toDo;
83 toDo.push(e0);
84
85 while(toDo.isNonEmpty()) {
86 LExpr* e = toDo.pop();
87 if(e->isAtom()) {
88 continue;
89 }
90 else {
91 ASS(e->isList());
92 LispListReader rdr(e);
93 if(rdr.lookAheadAtom("flet") || rdr.lookAheadAtom("let")) {
94 LExpr* head = rdr.readNext();
95 LExpr* defs = rdr.readNext();
96 rdr.readNext();
97 rdr.acceptEOL();
98
99 head->str = "let";
100 defs->list = (LispListWriter()<<(LispListWriter().append(defs->list))).getList();
101 }
102 LExprList::Iterator elit(e->list);
103 while(elit.hasNext()) {
104 toDo.push(elit.next());
105 }
106 }
107 }
108
109
110
111 }
112
113 //LExpr* SMTLIBConcat::smtlibToSmtlib2(LExpr* benchExpr)
114 //{
115 // CALL("SMTLIBConcat::smtlibToSmtlib2");
116 // ASS(benchExpr->isList())
117 // LispListReader bRdr(benchExpr->list);
118 // LispListWriter res;
119 //
120 // bRdr.acceptAtom("benchmark");
121 // bRdr.acceptAtom();
122 //
123 // while(bRdr.hasNext()) {
124 // if(bRdr.tryAcceptAtom(":status")) {
125 // bRdr.acceptAtom();
126 // }
127 // else if(bRdr.tryAcceptAtom(":source")) {
128 // if(!bRdr.tryAcceptCurlyBrackets()) {
129 // bRdr.acceptAtom();
130 // }
131 // }
132 // else if(bRdr.tryAcceptAtom(":extrafuns")) {
133 // LExprList* funDecls = bRdr.readList();
134 // LExprList::Iterator funIt(funDecls);
135 // while(funIt.hasNext()) {
136 // LExpr* funDecl = funIt.next();
137 // res << extrafuns2decl(funDecl);
138 // }
139 // }
140 // else if(bRdr.tryAcceptAtom(":formula")) {
141 // LExpr* form = bRdr.readNext();
142 // rewriteSmt1FormToSmt2(form);
143 // res << (LispListWriter() << "assert" << form);
144 // }
145 // else {
146 // //this will always give an error as we have bRdr.hasNext() set to true
147 // bRdr.acceptEOL();
148 // }
149 // }
150 //
151 // res << (LispListWriter() << "check-sat");
152 // res << (LispListWriter() << "get-proof");
153 //
154 // return res.get();
155 //}
156
rewriteIntsToReals(LExpr * e0)157 void SMTLIBConcat::rewriteIntsToReals(LExpr* e0)
158 {
159 CALL("SMTLIBConcat::rewriteIntsToReals");
160
161 Stack<LExpr*> toDo;
162 toDo.push(e0);
163
164 while(toDo.isNonEmpty()) {
165 LExpr* e = toDo.pop();
166 if(e->isAtom()) {
167 int aux;
168 if(Int::stringToInt(e->str, aux)) {
169 e->str = e->str+".0";
170 }
171 }
172 else {
173 ASS(e->isList());
174 LExprList::Iterator leit(e->list);
175 while(leit.hasNext()) {
176 toDo.push(leit.next());
177 }
178 }
179 }
180 }
181
addBenchmark(LExpr * expr,DHSet<vstring> & funSet,LispListWriter & wrt)182 void SMTLIBConcat::addBenchmark(LExpr* expr, DHSet<vstring>& funSet, LispListWriter& wrt)
183 {
184 CALL("SMTLIBConcat::readBenchmark");
185
186 ASS_REP(expr->isList(), expr->toString());
187
188 LispListReader tlRdr(expr->list);
189 LExprList* benchLst = tlRdr.readList();
190 tlRdr.acceptEOL();
191
192 LispListReader bRdr(benchLst);
193 bRdr.acceptAtom("benchmark");
194 bRdr.acceptAtom(); //benchmark name
195 while(bRdr.hasNext()) {
196 if(bRdr.tryAcceptAtom(":status")) {
197 bRdr.acceptAtom();
198 }
199 else if(bRdr.tryAcceptAtom(":source")) {
200 if(!bRdr.tryAcceptCurlyBrackets()) {
201 bRdr.acceptAtom();
202 }
203 }
204 else if(bRdr.tryAcceptAtom(":extrafuns")) {
205 LExprList* funDecls = bRdr.readList();
206 LExprList::Iterator funIt(funDecls);
207 while(funIt.hasNext()) {
208 LExpr* funDecl = funIt.next();
209 if(!funDecl->isList() && funDecl->list->head()->isAtom()) { USER_ERROR("function declaration expected: "+funDecl->toString()); }
210
211 vstring fnName = funDecl->list->head()->str;
212 if(!funSet.insert(fnName)) {
213 //duplicate function
214 continue;
215 }
216 wrt << extrafuns2decl(funDecl);
217 }
218 }
219 else if(bRdr.tryAcceptAtom(":formula")) {
220 LExpr* form = bRdr.readNext();
221 rewriteSmt1FormToSmt2(form);
222 wrt << (LispListWriter() << "assert" << form);
223 }
224 else {
225 //this will always give an error as we have bRdr.hasNext() set to true
226 bRdr.acceptEOL();
227 }
228 }
229 }
230
mergeBenchmarksIntoSmtlib2(Stack<LExpr * > & exprs)231 LExpr* SMTLIBConcat::mergeBenchmarksIntoSmtlib2(Stack<LExpr*>& exprs)
232 {
233 CALL("SMTLIBConcat::mergeBenchmarks");
234
235 DHSet<vstring> funSet;
236 Stack<LExpr*> funs;
237
238 LispListWriter res;
239 Stack<LExpr*>::Iterator bit(exprs);
240 while(bit.hasNext()) {
241 LExpr* benchExpr = bit.next();
242 addBenchmark(benchExpr, funSet, res);
243 }
244
245 // LispListWriter resBench;
246 // resBench << "benchmark" << "unnamed" << ":status" << "unknown";
247 //
248 // Stack<LExpr*>::Iterator funIt(funs);
249 // while(funIt.hasNext()) {
250 // LExpr* funDecl = funIt.next();
251 // resBench << ":extrafuns";
252 // resBench << (LispListWriter()<<funDecl);
253 // }
254 //
255 // LispListWriter form;
256 // form << "and";
257 // form.append(formulas);
258 //
259 // resBench << ":formula" << form;
260
261 res << (LispListWriter() << "check-sat");
262 res << (LispListWriter() << "get-proof");
263
264 return res.get();
265 }
266
parseFile(vstring fname)267 LExpr* SMTLIBConcat::parseFile(vstring fname)
268 {
269 CALL("SMTLIBConcat::parseFile");
270
271 if(!System::fileExists(fname)) {
272 USER_ERROR("input file does not exist: "+fname);
273 }
274
275 ifstream fin(fname.c_str());
276 LispLexer lex(fin);
277 LispParser parser(lex);
278 LExpr* res = parser.parse();
279
280 return res;
281 }
282
283 }
284