1
2 /*
3 * File UIHelper.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 UIHelper.cpp
21 * Implements class UIHelper.
22 */
23
24 #include <fstream>
25
26 #include <stdlib.h>
27 #include <sys/types.h>
28 #include <unistd.h>
29 #include <iostream>
30
31 #include "Forwards.hpp"
32
33 #include "Lib/Environment.hpp"
34 #include "Lib/TimeCounter.hpp"
35 #include "Lib/VString.hpp"
36 #include "Lib/Timer.hpp"
37
38 #include "Kernel/InferenceStore.hpp"
39 #include "Kernel/Problem.hpp"
40 #include "Kernel/FormulaUnit.hpp"
41
42 #include "Parse/SMTLIB2.hpp"
43 #include "Parse/TPTP.hpp"
44
45 #include "AnswerExtractor.hpp"
46 #include "InterpolantMinimizer.hpp"
47 #include "InterpolantMinimizerNew.hpp"
48 #include "Interpolants.hpp"
49 #include "InterpolantsNew.hpp"
50 #include "LaTeX.hpp"
51 #include "LispLexer.hpp"
52 #include "LispParser.hpp"
53 #include "Options.hpp"
54 #include "SimplifyProver.hpp"
55 #include "Statistics.hpp"
56 #include "TPTPPrinter.hpp"
57 #include "UIHelper.hpp"
58 // #include "SMTPrinter.hpp"
59
60 #include "Lib/RCPtr.hpp"
61 #include "Lib/List.hpp"
62 #include "Lib/ScopedPtr.hpp"
63
64 #if GNUMP
65 #include "Kernel/Assignment.hpp"
66 #include "Kernel/Constraint.hpp"
67 #include "Kernel/Signature.hpp"
68
69 #include "ConstraintReaderBack.hpp"
70 #include "Shell/SMTLEX.hpp"
71 #include "Shell/SMTPAR.hpp"
72 #include "Preprocess.hpp"
73
74 #include "MPSLib/Gmputils.h"
75 #include "MPSLib/Model.h"
76 #include "MPSLib/Mpsinput.h"
77
78 #include <algorithm>
79 #include <vector>
80 #include <list>
81 #endif
82
83 namespace Shell {
84
85 using namespace Lib;
86 using namespace Kernel;
87 using namespace Saturation;
88 using namespace std;
89
outputAllowed(bool debug)90 bool outputAllowed(bool debug)
91 {
92 #if VDEBUG
93 if(debug){ return true; }
94 #endif
95
96 // spider and smtcomp output modes are generally silent
97 return !Lib::env.options || (Lib::env.options->outputMode()!=Shell::Options::Output::SPIDER
98 && Lib::env.options->outputMode()!=Shell::Options::Output::SMTCOMP );
99 }
100
reportSpiderFail()101 void reportSpiderFail()
102 {
103 reportSpiderStatus('!');
104 }
105
reportSpiderStatus(char status)106 void reportSpiderStatus(char status)
107 {
108 using namespace Lib;
109
110 if(Lib::env.options && Lib::env.options->outputMode() == Shell::Options::Output::SPIDER) {
111 env.beginOutput();
112 env.out() << status << " "
113 << (Lib::env.options ? Lib::env.options->problemName() : "unknown") << " "
114 << (Lib::env.timer ? Lib::env.timer->elapsedDeciseconds() : 0) << " "
115 << (Lib::env.options ? Lib::env.options->testId() : "unknown") << "\n";
116 env.endOutput();
117 }
118 }
119
szsOutputMode()120 bool szsOutputMode() {
121 return (Lib::env.options && Lib::env.options->outputMode() == Shell::Options::Output::SZS);
122 }
123
addCommentSignForSZS(ostream & out)124 ostream& addCommentSignForSZS(ostream& out)
125 {
126 if (szsOutputMode()) {
127 out << "% ";
128 if (Lib::env.options && Lib::env.options->multicore() != 1) {
129 out << "(" << getpid() << ")";
130 }
131 }
132 return out;
133 }
134
135 bool UIHelper::s_haveConjecture=false;
136 bool UIHelper::s_proofHasConjecture=true;
137
138 bool UIHelper::s_expecting_sat=false;
139 bool UIHelper::s_expecting_unsat=false;
140
outputAllPremises(ostream & out,UnitList * units,vstring prefix)141 void UIHelper::outputAllPremises(ostream& out, UnitList* units, vstring prefix)
142 {
143 CALL("UIHelper::outputAllPremises");
144
145 #if 1
146 InferenceStore::instance()->outputProof(cerr, units);
147 #else
148 Stack<UnitSpec> prems;
149 Stack<UnitSpec> toDo;
150 DHSet<UnitSpec> seen;
151
152 //get the units to start with
153 UnitList::Iterator uit(units);
154 while (uit.hasNext()) {
155 Unit* u = uit.next();
156 toDo.push(UnitSpec(u));
157 }
158
159 while (toDo.isNonEmpty()) {
160 UnitSpec us = toDo.pop();
161 UnitSpecIterator pars = InferenceStore::instance()->getParents(us);
162 while (pars.hasNext()) {
163 UnitSpec par = pars.next();
164 if (seen.contains(par)) {
165 continue;
166 }
167 prems.push(par);
168 toDo.push(par);
169 seen.insert(par);
170 }
171 }
172
173 std::sort(prems.begin(), prems.end(), UIHelper::unitSpecNumberComparator);
174
175 Stack<UnitSpec>::BottomFirstIterator premIt(prems);
176 while (premIt.hasNext()) {
177 UnitSpec prem = premIt.next();
178 out << prefix << prem.toString() << endl;
179 }
180 #endif
181 }
182
outputSaturatedSet(ostream & out,UnitIterator uit)183 void UIHelper::outputSaturatedSet(ostream& out, UnitIterator uit)
184 {
185 CALL("UIHelper::outputSaturatedSet");
186
187 addCommentSignForSZS(out);
188 out << "# SZS output start Saturation." << endl;
189
190 while (uit.hasNext()) {
191 Unit* cl = uit.next();
192 out << TPTPPrinter::toString(cl) << endl;
193 }
194
195 addCommentSignForSZS(out);
196 out << "# SZS output end Saturation." << endl;
197 } // outputSaturatedSet
198
199 UnitList* parsedUnits;
200
201 /**
202 * Return problem object with units obtained according to the content of
203 * @b env.options
204 *
205 * No preprocessing is performed on the units.
206 */
getInputProblem(const Options & opts)207 Problem* UIHelper::getInputProblem(const Options& opts)
208 {
209 CALL("UIHelper::getInputProblem");
210
211 TimeCounter tc1(TC_PARSING);
212 env.statistics->phase = Statistics::PARSING;
213
214 SMTLIBLogic smtLibLogic = SMT_UNDEFINED;
215
216 vstring inputFile = opts.inputFile();
217
218 istream* input;
219 if (inputFile=="") {
220 input=&cin;
221 } else {
222 // CAREFUL: this might not be enough if the ifstream (re)allocates while being operated
223 BYPASSING_ALLOCATOR;
224
225 input=new ifstream(inputFile.c_str());
226 if (input->fail()) {
227 USER_ERROR("Cannot open problem file: "+inputFile);
228 }
229 }
230
231 UnitList* units;
232 switch (opts.inputSyntax()) {
233 /*
234 case Options::InputSyntax::SIMPLIFY:
235 {
236 Shell::LispLexer lexer(*input);
237 Shell::LispParser parser(lexer);
238 LispParser::Expression* expr = parser.parse();
239 SimplifyProver simplify;
240 units = simplify.units(expr);
241 }
242 break;
243 */
244 case Options::InputSyntax::TPTP:
245 {
246 Parse::TPTP parser(*input);
247 try{
248 parser.parse();
249 }
250 catch (UserErrorException& exception) {
251 vstring msg = exception.msg();
252 throw Parse::TPTP::ParseErrorException(msg,parser.lineNumber());
253 }
254 units = parser.units();
255 s_haveConjecture=parser.containsConjecture();
256 }
257 break;
258 /*
259 case Options::InputSyntax::SMTLIB:
260 {
261 Parse::SMTLIB parser(opts);
262 parser.parse(*input);
263 units = parser.getFormulas();
264 s_haveConjecture=true;
265 }
266 break;
267 if (outputAllowed()) {
268 env.beginOutput();
269 addCommentSignForSZS(env.out());
270 env.out() << "Vampire no longer supports the old smtlib format, trying with smtlib2 instead." << endl;
271 env.endOutput();
272 }
273 */
274 case Options::InputSyntax::SMTLIB2:
275 {
276 Parse::SMTLIB2 parser(opts);
277 parser.parse(*input);
278 Unit::onParsingEnd();
279
280 units = parser.getFormulas();
281 smtLibLogic = parser.getLogic();
282 s_haveConjecture=false;
283
284 #if VDEBUG
285 const vstring& expected_status = parser.getStatus();
286 if (expected_status == "sat") {
287 s_expecting_sat = true;
288 } else if (expected_status == "unsat") {
289 s_expecting_unsat = true;
290 }
291 #endif
292
293 break;
294 }
295 /*
296 case Options::InputSyntax::MPS:
297 case Options::InputSyntax::NETLIB:
298 case Options::InputSyntax::HUMAN:
299 {
300 cout << "This is not supported yet";
301 NOT_IMPLEMENTED;
302 }
303 */
304 break;
305 }
306
307 if (inputFile!="") {
308 BYPASSING_ALLOCATOR;
309
310 delete static_cast<ifstream*>(input);
311 input=0;
312 }
313
314 // parsedUnits = units->copy();
315
316 Problem* res = new Problem(units);
317 res->setSMTLIBLogic(smtLibLogic);
318
319 env.statistics->phase=Statistics::UNKNOWN_PHASE;
320 return res;
321 }
322
323 /*
324 static void printInterpolationProofTask(ostream& out, Formula* intp, Color avoid_color, bool negate)
325 {
326 CALL("printInterpolationProofTask");
327
328 UIHelper::outputSortDeclarations(out);
329 UIHelper::outputSymbolDeclarations(out);
330
331 UnitList::Iterator uit(parsedUnits);
332 while (uit.hasNext()) {
333 Unit* u = uit.next();
334
335 if (u->inheritedColor() != avoid_color) { // TODO: this does not work, since some inherited colors are modified destructively by the interpolation extraction code
336 Unit* toPrint = u;
337 if (toPrint->isClause()) { // need formulas, for the many sorted case
338 Formula* f = Formula::fromClause(toPrint->asClause());
339 toPrint = new FormulaUnit(f,u->inference(),Unit::AXIOM);
340 } else {
341 u->setInputType(Unit::AXIOM); // need it to be axiom in any case; the interpolant will be the conjecture
342 }
343
344 out << TPTPPrinter::toString(toPrint) << endl;
345 }
346 }
347
348 FormulaUnit* intpUnit = new FormulaUnit(negate ? new NegatedFormula(intp) : intp,new Inference0(Inference::INPUT),Unit::CONJECTURE);
349 out << TPTPPrinter::toString(intpUnit) << "\n";
350 }
351 */
352
353 /**
354 * Output result based on the content of
355 * @b env.statistics->terminationReason
356 *
357 * If LaTeX output is enabled, it is output in this function.
358 *
359 * If interpolant output is enabled, it is output in this function.
360 */
outputResult(ostream & out)361 void UIHelper::outputResult(ostream& out)
362 {
363 CALL("UIHelper::outputResult");
364
365 switch (env.statistics->terminationReason) {
366 case Statistics::REFUTATION:
367 if(env.options->outputMode() == Options::Output::SMTCOMP){
368 out << "unsat" << endl;
369 return;
370 }
371 addCommentSignForSZS(out);
372 out << "Refutation found. Thanks to " << env.options->thanks() << "!\n";
373 if (szsOutputMode()) {
374 out << "% SZS status " << (UIHelper::haveConjecture() ? ( UIHelper::haveConjectureInProof() ? "Theorem" : "ContradictoryAxioms" ) : "Unsatisfiable")
375 << " for " << env.options->problemName() << endl;
376 }
377 if (env.options->questionAnswering()!=Options::QuestionAnsweringMode::OFF) {
378 ASS(env.statistics->refutation->isClause());
379 AnswerExtractor::tryOutputAnswer(static_cast<Clause*>(env.statistics->refutation));
380 }
381 if (env.options->proof() != Options::Proof::OFF) {
382 if (szsOutputMode()) {
383 out << "% SZS output start Proof for " << env.options->problemName() << endl;
384 }
385 InferenceStore::instance()->outputProof(out, env.statistics->refutation);
386 if (szsOutputMode()) {
387 out << "% SZS output end Proof for " << env.options->problemName() << endl << flush;
388 }
389 // outputProof could have triggered proof minimization which might have cause inductionDepth to change (in fact, decrease)
390 env.statistics->maxInductionDepth = env.statistics->refutation->inference().inductionDepth();
391 }
392 if (env.options->showInterpolant()!=Options::InterpolantMode::OFF) {
393 ASS(env.statistics->refutation->isClause());
394
395 Interpolants::removeConjectureNodesFromRefutation(env.statistics->refutation);
396 Unit* formulifiedRefutation = Interpolants::formulifyRefutation(env.statistics->refutation);
397
398 Formula* interpolant = nullptr;
399
400 switch(env.options->showInterpolant()) {
401 // new interpolation methods described in master thesis of Bernhard Gleiss
402 case Options::InterpolantMode::NEW_HEUR:
403 InterpolantsNew().removeTheoryInferences(formulifiedRefutation); // do this only once for each proof!
404
405 // InterpolantMinimizerNew().analyzeLocalProof(formulifiedRefutation);
406
407 interpolant = InterpolantsNew().getInterpolant(formulifiedRefutation, InterpolantsNew::UnitWeight::VAMPIRE);
408 break;
409 case Options::InterpolantMode::NEW_OPT:
410 #if VZ3
411 InterpolantsNew().removeTheoryInferences(formulifiedRefutation); // do this only once for each proof!
412 interpolant = InterpolantMinimizerNew().getInterpolant(formulifiedRefutation, InterpolantsNew::UnitWeight::VAMPIRE);
413 #else
414 NOT_IMPLEMENTED;
415 #endif
416 break;
417
418 case Options::InterpolantMode::OLD:
419 interpolant = Interpolants().getInterpolant(formulifiedRefutation);
420 break;
421
422 case Options::InterpolantMode::OLD_OPT:
423 Interpolants::fakeNodesFromRightButGrayInputsRefutation(formulifiedRefutation); // grey right input formulas are artificially made children of proper blue parents
424 interpolant = InterpolantMinimizer(InterpolantMinimizer::OT_WEIGHT, false, true, "Minimized interpolant weight").getInterpolant(formulifiedRefutation);
425
426 /*
427 Formula* oldInterpolant = InterpolantMinimizer(InterpolantMinimizer::OT_WEIGHT, true, true, "Original interpolant weight").getInterpolant(static_cast<Clause*>(env.statistics->refutation));
428 Formula* interpolant = InterpolantMinimizer(InterpolantMinimizer::OT_WEIGHT, false, true, "Minimized interpolant weight").getInterpolant(static_cast<Clause*>(env.statistics->refutation));
429 InterpolantMinimizer(InterpolantMinimizer::OT_COUNT, true, true, "Original interpolant count").getInterpolant(static_cast<Clause*>(env.statistics->refutation));
430 Formula* cntInterpolant = InterpolantMinimizer(InterpolantMinimizer::OT_COUNT, false, true, "Minimized interpolant count").getInterpolant(static_cast<Clause*>(env.statistics->refutation));
431 Formula* quantInterpolant = InterpolantMinimizer(InterpolantMinimizer::OT_QUANTIFIERS, false, true, "Minimized interpolant quantifiers").getInterpolant(static_cast<Clause*>(env.statistics->refutation));
432 */
433
434 break;
435 case Options::InterpolantMode::OFF:
436 ASSERTION_VIOLATION;
437 }
438
439 out << "Symbol-weight minimized interpolant: " << TPTPPrinter::toString(interpolant) << endl;
440 out << "Actual weight: " << interpolant->weight() << endl;
441 out<<endl;
442 }
443
444 if (env.options->latexOutput() != "off") {
445 BYPASSING_ALLOCATOR; // for ofstream
446 ofstream latexOut(env.options->latexOutput().c_str());
447
448 LaTeX formatter;
449 latexOut << formatter.refutationToString(env.statistics->refutation);
450 }
451
452 ASS(!s_expecting_sat);
453
454 break;
455 case Statistics::TIME_LIMIT:
456 if(env.options->outputMode() == Options::Output::SMTCOMP){
457 out << "unknown" << endl;
458 return;
459 }
460 addCommentSignForSZS(out);
461 out << "Time limit reached!\n";
462 break;
463 case Statistics::MEMORY_LIMIT:
464 if(env.options->outputMode() == Options::Output::SMTCOMP){
465 out << "unknown" << endl;
466 return;
467 }
468 #if VDEBUG
469 Allocator::reportUsageByClasses();
470 #endif
471 addCommentSignForSZS(out);
472 out << "Memory limit exceeded!\n";
473 break;
474 case Statistics::ACTIVATION_LIMIT: {
475 addCommentSignForSZS(out);
476 out << "Activation limit reached!\n";
477
478 // HERE ADD MORE
479
480 break;
481 }
482 case Statistics::REFUTATION_NOT_FOUND:
483 if(env.options->outputMode() == Options::Output::SMTCOMP){
484 out << "unknown" << endl;
485 return;
486 }
487 addCommentSignForSZS(out);
488 env.statistics->explainRefutationNotFound(out);
489 break;
490 case Statistics::SATISFIABLE:
491 if(env.options->outputMode() == Options::Output::SMTCOMP){
492 out << "sat" << endl;
493 return;
494 }
495 outputSatisfiableResult(out);
496
497 ASS(!s_expecting_unsat);
498
499 break;
500 case Statistics::SAT_SATISFIABLE:
501 outputSatisfiableResult(out);
502 break;
503 case Statistics::SAT_UNSATISFIABLE:
504 out<<"good job\n";
505 break;
506 case Statistics::INAPPROPRIATE:
507 if(env.options->outputMode() == Options::Output::SMTCOMP){
508 out << "unknown" << endl;
509 return;
510 }
511 addCommentSignForSZS(out);
512 out << "Terminated due to inappropriate strategy.\n";
513 break;
514 case Statistics::UNKNOWN:
515 if(env.options->outputMode() == Options::Output::SMTCOMP){
516 out << "unknown" << endl;
517 return;
518 }
519 addCommentSignForSZS(out);
520 out << "Unknown reason of termination!\n";
521 break;
522 default:
523 ASSERTION_VIOLATION;
524 }
525 env.statistics->print(out);
526 }
527
outputSatisfiableResult(ostream & out)528 void UIHelper::outputSatisfiableResult(ostream& out)
529 {
530 CALL("UIHelper::outputSatisfiableResult");
531
532 //out << "Satisfiable!\n";
533 if (szsOutputMode() && !satisfiableStatusWasAlreadyOutput) {
534 out << "% SZS status " << ( UIHelper::haveConjecture() ? "CounterSatisfiable" : "Satisfiable" )
535 <<" for " << env.options->problemName() << endl;
536 }
537 if (!env.statistics->model.empty()) {
538 if (szsOutputMode()) {
539 out << "% SZS output start FiniteModel for " << env.options->problemName() << endl;
540 }
541 out << env.statistics->model;
542 if (szsOutputMode()) {
543 out << "% SZS output end FiniteModel for " << env.options->problemName() << endl;
544 }
545 }
546 else //if (env.statistics->saturatedSet)
547 /* -- MS: it's never incorrect to print the empty one, in fact this prevents us from losing
548 * points at CASC when the input gets completely emptied, by e.g. preprocessing
549 */
550 {
551 outputSaturatedSet(out, pvi(UnitList::Iterator(env.statistics->saturatedSet)));
552 }
553 }
554
555 /**
556 * Output to @b out all symbol declarations for the current signature.
557 * Symbols having default types will not be output.
558 * @author Andrei Voronkov
559 * @since 03/07/2013 Manchester
560 */
outputSymbolDeclarations(ostream & out)561 void UIHelper::outputSymbolDeclarations(ostream& out)
562 {
563 CALL("UIHelper::outputSymbolDeclarations");
564
565 Signature& sig = *env.signature;
566
567 unsigned funcs = sig.functions();
568 for (unsigned i=0; i<funcs; ++i) {
569 if (!env.options->showFOOL()) {
570 if (env.signature->isFoolConstantSymbol(true,i) || env.signature->isFoolConstantSymbol(false,i)) {
571 continue;
572 }
573 }
574 outputSymbolTypeDeclarationIfNeeded(out, true, i);
575 }
576 unsigned preds = sig.predicates();
577 for (unsigned i=0; i<preds; ++i) {
578 outputSymbolTypeDeclarationIfNeeded(out, false, i);
579 }
580 } // UIHelper::outputSymbolDeclarations
581
582 /**
583 * Output to @b out a function or a predicate symbol declaration.
584 * Symbols having default types will not be output.
585 * @author Andrei Voronkov
586 * @since 03/07/2013 Manchester
587 */
outputSymbolTypeDeclarationIfNeeded(ostream & out,bool function,unsigned symNumber)588 void UIHelper::outputSymbolTypeDeclarationIfNeeded(ostream& out, bool function, unsigned symNumber)
589 {
590 CALL("UIHelper::outputSymbolTypeDeclarationIfNeeded");
591
592 Signature::Symbol* sym = function ?
593 env.signature->getFunction(symNumber) : env.signature->getPredicate(symNumber);
594
595 if (sym->interpreted()) {
596 //there is no need to output type definitions for interpreted symbols
597 return;
598 }
599
600 if (sym->overflownConstant()) {
601 // don't output definitions of numbers; not even big ones
602 return;
603 }
604
605 unsigned dummy;
606 if (Theory::tuples()->findProjection(symNumber, !function, dummy)) {
607 return;
608 }
609
610 if (function) {
611 unsigned sort = env.signature->getFunction(symNumber)->fnType()->result();
612 if (env.sorts->isOfStructuredSort(sort, Sorts::StructuredSort::TUPLE)) {
613 return;
614 }
615 }
616
617 OperatorType* type = function ? sym->fnType() : sym->predType();
618
619 if (type->isAllDefault()) {
620 return;
621 }
622
623 out << "tff(" << (function ? "func" : "pred") << "_def_" << symNumber << ", type, "
624 << sym->name() << ": ";
625
626 unsigned arity = sym->arity();
627 if (arity>0) {
628 if (arity==1) {
629 out << env.sorts->sortName(type->arg(0));
630 }
631 else {
632 out << "(";
633 for (unsigned i=0; i<arity; i++) {
634 if (i>0) {
635 out << " * ";
636 }
637 out << env.sorts->sortName(type->arg(i));
638 }
639 out << ")";
640 }
641 out << " > ";
642 }
643 if (function) {
644 out << env.sorts->sortName(sym->fnType()->result());
645 }
646 else {
647 out << "$o";
648 }
649 out << ")." << endl;
650 }
651
652 /**
653 * Output to @b out all sort declarations for the current signature.
654 * Built-in sorts and structures sorts will not be output.
655 * @author Evgeny Kotelnikov
656 * @since 04/09/2015 Gothneburg
657 */
outputSortDeclarations(ostream & out)658 void UIHelper::outputSortDeclarations(ostream& out)
659 {
660 CALL("UIHelper::outputSortDeclarations");
661
662 unsigned sorts = (*env.sorts).count();
663 for (unsigned sort = Sorts::SRT_BOOL; sort < sorts; ++sort) {
664 if (sort < Sorts::FIRST_USER_SORT && ((sort != Sorts::SRT_BOOL) || !env.options->showFOOL())) {
665 continue;
666 }
667 if ((*env.sorts).isStructuredSort(sort)) {
668 continue;
669 }
670 out << "tff(type_def_" << sort << ", type, " << env.sorts->sortName(sort) << ": $tType)." << endl;
671 }
672 } // UIHelper::outputSortDeclarations
673
674 #if GNUMP
675 /**
676 * Add input constraints into the empty @c constraints list.
677 */
getInputConstraints(const Options & opts)678 ConstraintRCList* UIHelper::getInputConstraints(const Options& opts)
679 {
680 CALL("UIHelper::getInputConstraints");
681
682 TimeCounter tc(TC_PARSING);
683 env.statistics->phase = Statistics::PARSING;
684
685 vstring inputFile = env.options->inputFile();
686
687 ScopedPtr<std::ifstream> inputScoped;
688 istream * input;
689 if (inputFile=="") {
690 input=&cin;
691 } else {
692 inputScoped=new ifstream(inputFile.c_str());
693 input = inputScoped.ptr();
694 if (input->fail()) {
695 USER_ERROR("Cannot open problem file: "+inputFile);
696 }
697 }
698
699 ConstraintRCList* res;
700
701 switch(env.options->inputSyntax()) {
702 case Options::InputSyntax::TPTP:
703 USER_ERROR("Format not supported for BPA");
704 break;
705 #if 0
706 case Options::InputSyntax::SMTLIB:
707 case Options::InputSyntax::SMTLIB2:
708 {
709 Parse::SMTLIB parser(opts);
710 parser.parse(*input);
711 UnitList* ulist = parser.getFormulas();
712 UnitList::Iterator ite(ulist);
713 while (ite.hasNext())
714 {
715 Unit* u = ite.next();
716 if ( !u->isClause()) {
717 Formula* f = u->getFormula();
718 std::cout << f->toString();
719 }
720
721
722 }
723 ASSERTION_VIOLATION;
724 s_haveConjecture=true;
725 SMTConstraintReader rdr(parser);
726 res = rdr.constraints();
727 break;
728
729 /*
730 std::cout << "doing the constraint reading" << std::endl;
731 Parse::SMTLIB parser1(*env.options);
732
733 vstring inputFile = env.options->inputFile();
734 std::cout << inputFile << std::endl;
735 istream* input;
736 if (inputFile=="") {
737 input=&cin;
738 } else {
739 input=new ifstream(inputFile.c_str());
740 if (input->fail()) {
741 USER_ERROR("Cannot open problem file: "+inputFile);
742 }
743 }
744
745 parser1.parse(*input);
746 std::cout << parser1.getLispFormula()->toString() << std::endl;
747 */
748 }
749 #endif
750 case Options::InputSyntax::SMTLIB:
751 {
752 SMTLexer lex(*input);
753 SMTParser parser(lex);
754 ConstraintReader rdr(parser);
755 res = rdr.constraints();
756 break;
757 }
758 case Options::InputSyntax::SMTLIB2:
759 {
760 Parse::SMTLIB2 parser(opts, Parse::SMTLIB2::DECLARE_SYMBOLS);
761 parser.parse(*input);
762 SMTLib2ConstraintReader rdr(parser);
763 res = rdr.constraints();
764 break;
765
766 }
767 case Options::InputSyntax::MPS:
768 {
769 Model* m = new Model;
770 MpsInput* mpsin = new MpsInput;
771
772 bool success = mpsin->readMps(env.options->inputFile().c_str(), m);
773 // m->print(std::cout);
774
775 ASS_EQ(success,true);
776 MpsConstraintReader creader(*m);
777 res = creader.constraints();
778
779 #if 0
780 ConstraintRCList::Iterator ite(res);
781 while (ite.hasNext())
782 std::cout << ite.next()->toString() << std::endl;
783 throw TimeLimitExceededException();
784 ASSERTION_VIOLATION;
785 #endif
786 break;
787 }
788 case Options::InputSyntax::HUMAN:
789 USER_ERROR("human syntax is not supported as input syntax");
790 case Options::InputSyntax::NETLIB:
791 // case Options::InputSyntax::SMTLIB2:
792 NOT_IMPLEMENTED;
793 default:
794 ASSERTION_VIOLATION;
795 }
796
797 env.statistics->inputConstraints = res->length();
798 env.statistics->inputVariables = env.signature->vars();
799
800 return res;
801 }
802
803 /**
804 * Preprocess @c inputConstraints into @c constraints.
805 */
getPreprocessedConstraints(const ConstraintRCList * inputConstraints)806 ConstraintRCList* UIHelper::getPreprocessedConstraints(const ConstraintRCList* inputConstraints)
807 {
808 CALL("UIHelper::getPreprocessedConstraints/2");
809
810 TimeCounter tc(TC_PREPROCESSING);
811 env.statistics->phase = Statistics::PREPROCESSING;
812
813 Preprocess prepr(*env.options);
814 ConstraintRCList* constraints = ConstraintRCList::copy(inputConstraints);
815 prepr.preprocess(constraints);
816
817 return constraints;
818 }
819
820 /**
821 * Add preprocessed input constraints into the empty @c constraints list.
822 */
getPreprocessedConstraints(const Options & opts)823 ConstraintRCList* UIHelper::getPreprocessedConstraints(const Options& opts)
824 {
825 CALL("UIHelper::getPreprocessedConstraints/1");
826
827 ConstraintRCList* inpConstraints(getInputConstraints(opts));
828 return getPreprocessedConstraints(inpConstraints);
829 }
830
831 /**
832 * Into stream @c out output @c constraint in format @b syntax.
833 */
outputConstraint(const Constraint & constraint,ostream & out,Options::InputSyntax syntax)834 void UIHelper::outputConstraint(const Constraint& constraint, ostream& out, Options::InputSyntax syntax)
835 {
836 CALL("UIHelper::outputConstraint");
837
838 switch(syntax) {
839 case Options::InputSyntax::HUMAN:
840 outputConstraintInHumanFormat(constraint, out);
841 // outputConstraintInSMTFormat(constraint,out);
842 return;
843 case Options::InputSyntax::SMTLIB:
844 outputConstraintInSMTFormat(constraint,out);
845 return;
846 case Options::InputSyntax::MPS:
847 case Options::InputSyntax::NETLIB:
848 case Options::InputSyntax::SMTLIB2:
849 NOT_IMPLEMENTED;
850 default:
851 ASSERTION_VIOLATION;
852 }
853
854 }
855
outputConstraintInHumanFormat(const Constraint & constraint,ostream & out)856 void UIHelper::outputConstraintInHumanFormat(const Constraint& constraint, ostream& out)
857 {
858 CALL("UIHelper::outputConstraintInHumanFormat");
859
860 /*
861 * Constraint::CoeffIterator coeffs = constraint.coeffs();
862
863
864 switch(constraint.type()) {
865 case CT_EQ:
866 out << "( = "; break;
867 case CT_GR:
868 out << "( >"; break;
869 case CT_GREQ:
870 out << "( >="; break;
871 }
872
873 unsigned closedP = 0;
874 if (constraint.freeCoeff() != CoeffNumber::zero() && constraint.type()!= CT_EQ)
875 {
876 out << " (+";
877 closedP ++;
878 if (constraint.freeCoeff().isNegativeAssumingNonzero())
879 out<< " " << -constraint.freeCoeff().native() <<" ";
880 if (constraint.freeCoeff().isPositiveAssumingNonzero())
881 out<< " (~ " << constraint.freeCoeff().native() <<")";
882 }
883
884 while (coeffs.hasNext()) {
885 Constraint::Coeff coeff = coeffs.next();
886 if (coeffs.hasNext()) {
887 out << " (+ ";
888 closedP++;
889 }
890 if (coeff.value<CoeffNumber::zero()) {
891 out << " (* ( ~ " << -coeff.value << " ) " << env.signature->varName(coeff.var) << ")";
892 }
893 else {
894 out <<" (* "<< coeff.value << " " << env.signature->varName(coeff.var) << " )";
895 }
896
897 }
898
899 if (constraint.freeCoeff() != CoeffNumber::zero() && constraint.type()!= CT_EQ )
900 out << "";
901
902 while (closedP!=0)
903 {
904 out << ")";
905 closedP--;
906 }
907 out << " 0 )";
908
909 */
910 Constraint::CoeffIterator coeffs = constraint.coeffs();
911 if (!coeffs.hasNext()) {
912 out << "0 ";
913 }
914 while (coeffs.hasNext()) {
915 Constraint::Coeff coeff = coeffs.next();
916 if (coeff.value<CoeffNumber::zero()) {
917 out << "(" << coeff.value << "*" << env.signature->varName(coeff.var) << ") ";
918 }
919 else {
920 out << coeff.value << "*" << env.signature->varName(coeff.var) << " ";
921 }
922 if (coeffs.hasNext()) {
923 out << "+ ";
924 }
925 }
926 switch(constraint.type()) {
927 case CT_EQ:
928 out << "="; break;
929 case CT_GR:
930 out << ">"; break;
931 case CT_GREQ:
932 out << ">="; break;
933 }
934 out << " " << constraint.freeCoeff();
935 }
936
937
outputConstraintInSMTFormat(const Constraint & constraint,ostream & out)938 void UIHelper::outputConstraintInSMTFormat(const Constraint& constraint, ostream& out)
939 {
940 CALL("UIHelper::outputConstraintInSMTFormat");
941
942 Constraint::CoeffIterator coeffs = constraint.coeffs();
943
944 /*
945 if (!coeffs.hasNext()) {
946 out << " 0 ";
947 }
948 */
949 switch(constraint.type()) {
950 case CT_EQ:
951 out << "( = "; break;
952 case CT_GR:
953 out << "( >"; break;
954 case CT_GREQ:
955 out << "( >="; break;
956 }
957
958 unsigned closedP = 0;
959 if (constraint.freeCoeff() != CoeffNumber::zero() && constraint.type()!= CT_EQ)
960 {
961 out << " (+";
962 closedP ++;
963 if (constraint.freeCoeff().isNegativeAssumingNonzero())
964 out << " " << -constraint.freeCoeff().native() << " ";
965 if (constraint.freeCoeff().isPositiveAssumingNonzero())
966 out << " (~ " << constraint.freeCoeff().native() << ")";
967 }
968
969 while (coeffs.hasNext()) {
970 Constraint::Coeff coeff = coeffs.next();
971 if (coeffs.hasNext()) {
972 out << " (+ ";
973 closedP++;
974
975 }
976
977 if (coeff.value<CoeffNumber::zero()) {
978
979 out << " (* ( ~ " << -coeff.value << " ) " << env.signature->varName(coeff.var) << ")";
980 }
981 else {
982 out <<" (* "<< coeff.value << " " << env.signature->varName(coeff.var) << " )";
983 }
984
985 }
986
987 if (constraint.freeCoeff() != CoeffNumber::zero() && constraint.type()!= CT_EQ )
988 out << "";
989
990 while (closedP!=0)
991 {
992 out << ")";
993 closedP--;
994 }
995 out << " 0 )";
996
997 /* if (constraint.freeCoeff().isNegative() || constraint.freeCoeff() == CoeffNumber::zero() )
998 out << "(~" << -constraint.freeCoeff() <<") )";
999 else
1000 out << " " << constraint.freeCoeff() <<" )";*/
1001 }
1002
1003 /**
1004 * Into stream @c out output @c constraints in format @b syntax.
1005 */
outputConstraints(ConstraintList * constraints,ostream & out,Options::InputSyntax syntax)1006 void UIHelper::outputConstraints(ConstraintList* constraints, ostream& out, Options::InputSyntax syntax)
1007 {
1008 CALL("UIHelper::outputConstraints");
1009
1010 switch(syntax) {
1011 case Options::InputSyntax::HUMAN:
1012 {
1013 ConstraintList::Iterator ite(constraints);
1014 while (ite.hasNext())
1015 {
1016 outputConstraint(*ite.next(), out, syntax);
1017 out << endl;
1018 }
1019 return;
1020 }
1021 case Options::InputSyntax::SMTLIB:
1022 {
1023 out << " (benchmark SOMENAME" << endl;
1024 out << " :source {converted from MIPLIB} " << endl;
1025 out << " :status unknown " << endl;
1026 out << " :category { industrial } " << endl;
1027 out << " :logic QF_LRA " << endl;
1028
1029 ConstraintList::Iterator fun(constraints);
1030 std::list<vstring> uni;
1031
1032 while (fun.hasNext())
1033 {
1034 Constraint::CoeffIterator coeffs = fun.next()->coeffs();
1035 while (coeffs.hasNext()) {
1036 env.signature->varName(coeffs.next().var);
1037 uni.push_back(env.signature->varName(coeffs.next().var));
1038 //out << ":extrafuns ((" << env.signature->varName(coeffs.next().var) << " Real )) " << endl;
1039 }
1040
1041 }
1042
1043 std::vector<vstring> myvector (uni.begin(),uni.end());
1044 std::vector<vstring>::iterator ite;
1045 ite = unique(myvector.begin(),myvector.end());
1046 myvector.resize( ite - myvector.begin() );
1047 for (ite=myvector.begin(); ite!=myvector.end(); ++ite)
1048 out << " " << *ite;
1049
1050 out << ":formula (and ";
1051 ConstraintList::Iterator it(constraints);
1052 while (it.hasNext()) {
1053 outputConstraint(*it.next(), out, syntax);
1054 out << " \n";
1055 }
1056
1057 out << ") )"<< endl;
1058 return;
1059 }
1060
1061 case Options::InputSyntax::MPS:
1062 case Options::InputSyntax::NETLIB:
1063 case Options::InputSyntax::SMTLIB2:
1064 NOT_IMPLEMENTED;
1065 default:
1066 ASSERTION_VIOLATION;
1067 }
1068 }
1069
outputAssignment(Assignment & assignemt,ostream & out,Shell::Options::InputSyntax syntax)1070 void UIHelper::outputAssignment(Assignment& assignemt, ostream& out, Shell::Options::InputSyntax syntax)
1071 {
1072 CALL("UIHelper::outputAssignment");
1073
1074 switch(syntax) {
1075 case Options::InputSyntax::HUMAN:
1076 case Options::InputSyntax::MPS:
1077 case Options::InputSyntax::SMTLIB:
1078 {
1079 VarIterator vars = assignemt.getAssignedVars();
1080 while (vars.hasNext()) {
1081 Var v = vars.next();
1082 out << env.signature->varName(v) << ": " << assignemt[v] << endl;
1083 }
1084 return;
1085 }
1086 case Options::InputSyntax::NETLIB:
1087 case Options::InputSyntax::SMTLIB2:
1088 NOT_IMPLEMENTED;
1089 default:
1090 ASSERTION_VIOLATION;
1091 }
1092 }
1093
1094 #endif //GNUMP
1095
1096 } // namespace Shell
1097
1098
1099