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