CVC3  2.4.1
vc_cmd.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file vc_cmd.cpp
4  *
5  * Author: Clark Barrett
6  *
7  * Created: Fri Dec 13 22:39:02 2002
8  *
9  * <hr>
10  * License to use, copy, modify, sell and/or distribute this software
11  * and its documentation for any purpose is hereby granted without
12  * royalty, subject to the terms and conditions defined in the \ref
13  * LICENSE file provided with this distribution.
14  *
15  * <hr>
16  *
17  */
18 /*****************************************************************************/
19 
20 #include <fstream>
21 #include "vc_cmd.h"
22 #include "vc.h"
23 #include "parser.h"
24 #include "eval_exception.h"
25 #include "typecheck_exception.h"
26 #include "command_line_flags.h"
27 #include "expr_stream.h"
28 
29 using namespace std;
30 using namespace CVC3;
31 
32 VCCmd::VCCmd(ValidityChecker* vc, Parser* parser, bool calledFromParser)
33  : d_vc(vc), d_parser(parser), d_name_of_cur_ctxt("DEFAULT"),
34  d_calledFromParser(calledFromParser)
35 {
37 }
38 
40 
41 void VCCmd::findAxioms(const Expr& e, ExprMap<bool>& skolemAxioms,
42  ExprMap<bool>& visited) {
43  if(visited.count(e)>0)
44  return;
45  else visited[e] = true;
46  if(e.isSkolem()) {
47  skolemAxioms.insert(e.getExistential(), true);
48  return;
49  }
50  if(e.isClosure()) {
51  findAxioms(e.getBody(), skolemAxioms, visited);
52  }
53  if(e.arity()>0) {
54  Expr::iterator end = e.end();
55  for(Expr::iterator i = e.begin(); i!=end; ++i)
56  findAxioms(*i, skolemAxioms, visited);
57  }
58 
59 }
60 
62 {
63  vector<Expr>vars;
64  const vector<Expr>boundVars = e.getVars();
65  for(unsigned int i=0; i<boundVars.size(); i++) {
66  Expr skolV(e.skolemExpr(i));
67  vars.push_back(skolV);
68  }
69  Expr sub = e.getBody().substExpr(boundVars, vars);
70  return e.iffExpr(sub);
71 }
72 
74 {
75 readAgain:
76  if(d_parser->done()) return false; // No more commands
77  Expr e;
78  try {
79  TRACE_MSG("commands", "** [commands] Parsing command...");
80  e = d_parser->next();
81  TRACE("commands verbose", "evaluateNext(", e, ")");
82  }
83  catch(Exception& e) {
84  cerr << "*** " << e << endl;
85  IF_DEBUG(++(debugger.counter("parse errors"));)
86  }
87  // The parser may return a Null Expr in case of parse errors or end
88  // of file. The right thing to do is to ignore it and repeat
89  // reading.
90  if(e.isNull()) {
91  TRACE_MSG("commands", "** [commands] Null command; read again");
92  goto readAgain;
93  }
94  if( d_vc->getFlags()["parse-only"].getBool() ) {
95  TRACE_MSG("commands", "** [commands] parse-only; skipping evaluateCommand");
96  goto readAgain;
97  }
98 
99  return evaluateCommand(e);
100 }
101 
102 void VCCmd::reportResult(QueryResult qres, bool checkingValidity)
103 {
104  if (d_vc->getFlags()["printResults"].getBool()) {
105  if (d_vc->getEM()->getOutputLang() == SMTLIB_LANG
106  || d_vc->getEM()->getOutputLang() == SMTLIB_V2_LANG) {
107  switch (qres) {
108  case VALID:
109  cout << "unsat" << endl;
110  break;
111  case INVALID:
112  cout << "sat" << endl;
113  break;
114  case ABORT:
115  case UNKNOWN:
116  cout << "unknown" << endl;
117  break;
118  default:
119  FatalAssert(false, "Unexpected case");
120  }
121  }
122  else {
123  switch (qres) {
124  case VALID:
125  cout << (checkingValidity ? "Valid." : "Unsatisfiable.") << endl;
126  break;
127  case INVALID:
128  cout << (checkingValidity ? "Invalid." : "Satisfiable.") << endl;
129  break;
130  case ABORT:
131  cout << "Unknown: resource limit exhausted." << endl;
132  break;
133  case UNKNOWN: {
134  // Vector of reasons in case of incomplete result
135  vector<string> reasons;
136  IF_DEBUG(bool b =) d_vc->incomplete(reasons);
137  DebugAssert(b, "Expected incompleteness");
138  cout << "Unknown.\n\n";
139  cout << "CVC3 was incomplete in this example due to:";
140  for(vector<string>::iterator i=reasons.begin(), iend=reasons.end();
141  i!=iend; ++i)
142  cout << "\n * " << (*i);
143  cout << endl << endl;
144  break;
145  }
146  default:
147  FatalAssert(false, "Unexpected case");
148  }
149  }
150  cout << flush;
151  }
152  //d_vc->printStatistics();
153  // exit(0);
154 }
155 
156 
158 {
159  ExprMap<Expr> m;
161 
162  cout << "Current scope level is " << d_vc->scopeLevel() << "." << endl;
163  ExprMap<Expr>::iterator it = m.begin(), end = m.end();
164  if(it == end)
165  cout << " Did not find concrete model for any vars" << endl;
166  else {
167  cout << "%Satisfiable Variable Assignment: % \n";
168  for(; it!= end; it++) {
169  Expr eq;
170  if(it->first.getType().isBool()) {
171  DebugAssert((it->second).isBoolConst(),
172  "Bad variable assignement: e = "+(it->first).toString()
173  +"\n\n val = "+(it->second).toString());
174  if((it->second).isTrue())
175  eq = it->first;
176  else
177  eq = !(it->first);
178  }
179  else
180  eq = (it->first).eqExpr(it->second);
181  cout << Expr(ASSERT, eq) << "\n";
182  }
183  }
184 }
185 
186 
187 // For debugging: there are missing cases: user-defined types, symbols inside of quantifiers, etc.
189 {
190  if (cache.find(e) != cache.end()) return;
191  switch (e.getKind()) {
192  case SKOLEM_VAR:
193  case UCONST: {
194  cout << e << " : ";
195  ExprStream os(d_vc->getEM());
196  os.dagFlag(false);
197  os << e.getType().getExpr();
198  cout << ";" << endl;
199  break;
200  }
201  case APPLY: {
202  Expr op = e.getOpExpr();
203  if ((op.getKind() == UFUNC) && (cache.find(op) == cache.end())) {
204  cout << op << " : ";
205  ExprStream os(d_vc->getEM());
206  os.dagFlag(false);
207  os << op.getType().getExpr();
208  cout << ";" << endl;
209  cache[op] = true;
210  }
211  // fall through
212  }
213  default: {
214  Expr::iterator i = e.begin(), iend = e.end();
215  for (; i != iend; ++i) {
216  printSymbols(*i, cache);
217  }
218  break;
219  }
220  }
221  cache[e] = true;
222 }
223 
224 
225 bool debug_skolem = false;
226 
227 
229 {
230  vector<Expr> assertions;
231  ExprMap<bool> skolemAxioms;
232  ExprMap<bool> visited;
233 
234  d_vc->getCounterExample(assertions);
235 
236  // get variable information
237  ExprMap<bool> cache;
238  unsigned i;
239  for (i = 0; i < assertions.size(); i++) {
240  printSymbols(assertions[i], cache);
241  }
242 
243  cout << "% Current scope level is " << d_vc->scopeLevel() << "." << endl;
244  if (assertions.size() == 0) {
245  cout << "% There are no assertions\n";
246  } else {
247 
248  cout << "% Assertions which make the QUERY invalid:\n";
249 
250  for (i = 0; i < assertions.size(); i++) {
251  cout << Expr(ASSERT, assertions[i]) << "\n";
252  findAxioms(assertions[i], skolemAxioms, visited);
253  }
254 
255  if (debug_skolem) {
256  cout << "% Including skolemization axioms:\n";
257 
258  ExprMap<bool>::iterator end = skolemAxioms.end();
259  for(ExprMap<bool>::iterator it = skolemAxioms.begin(); it!=end; it++)
260  cout << "ASSERT " << skolemizeAx((*it).first) << ";" << endl;
261  }
262  }
263  cout << endl;
264 }
265 
266 
268 {
269  TRACE("commands", "evaluateCommand(", e0.toString(PRESENTATION_LANG), ") {");
270  Expr e(e0);
271  if(e.getKind() != RAW_LIST || e.arity() == 0 || e[0].getKind() != ID)
272  throw EvalException("Invalid command: "+e.toString());
273  const string& kindName = e[0][0].getString();
274  int kind = d_vc->getEM()->getKind(kindName);
275  if(kind == NULL_KIND)
276  throw EvalException("Unknown command: "+e.toString());
277  switch(kind) {
278  case CONST: { // (CONST (id_1 ... id_n) type) or (CONST id type)
279  if(e.arity() == 3) {
280  Type t(d_vc->parseExpr(e[2]));
281  vector<Expr> vars;
282  if(e[1].getKind() == RAW_LIST)
283  vars = e[1].getKids();
284  else
285  vars.push_back(e[1]);
286  for(vector<Expr>::iterator i=vars.begin(), iend=vars.end(); i!=iend; ++i) {
287  if((*i).getKind() != ID)
288  throw EvalException("Constant name must be an identifier: "
289  +i->toString());
290  }
291  if (t.isFunction()) {
292  for(vector<Expr>::iterator i=vars.begin(), iend=vars.end();
293  i!=iend; ++i) {
294  Op op = d_vc->createOp((*i)[0].getString(), t);
295  TRACE("commands", "evaluateNext: declare new uninterpreted function: ",
296  op, "");
297  }
298  }
299  else {
300  for(vector<Expr>::iterator i=vars.begin(), iend=vars.end();
301  i!=iend; ++i) {
302  // Add to variable list
303  Expr v = d_vc->varExpr((*i)[0].getString(), t);
304  TRACE_MSG("commands", "** [commands] Declare new variable");
305  TRACE("commands verbose", "evaluateNext: declare new UCONST: ",
306  v, "");
307  }
308  }
309  } else if(e.arity() == 4) { // Constant definition (CONST id type def)
310  TRACE_MSG("commands", "** [commands] Define new constant");
311  // Set the type for later typechecking
312  DebugAssert(e[1].getKind() == ID, "Expected ID kind");
313  Type t(d_vc->parseExpr(e[2]));
314  Expr def(d_vc->parseExpr(e[3]));
315 
316  if(t.isFunction()) {
317  d_vc->createOp(e[1][0].getString(), t, def);
318  TRACE("commands verbose", "evaluateNext: define new function: ",
319  e[1][0].getString(), "");
320  } else {
321  d_vc->varExpr(e[1][0].getString(), t, def);
322  TRACE("commands verbose", "evaluateNext: define new variable: ",
323  e[1][0].getString(), "");
324  }
325  } else
326  throw EvalException("Wrong number of arguments in CONST: "+e.toString());
327  break;
328  }
329  case DEFUN: { // (DEFUN name ((x y z type1) ... ) resType [ body ])
330  if(e.arity() != 5 && e.arity() != 4)
331  throw EvalException
332  ("DEFUN requires 3 or 4 arguments:"
333  " (DEFUN f (args) type [ body ]):\n\n "
334  +e.toString());
335  if(e[2].getKind() != RAW_LIST)
336  throw EvalException
337  ("2nd argument of DEFUN must be a list of arguments:\n\n "
338  +e.toString());
339 
340  // Build a CONST declaration and parse it recursively
341 
342  // Build the function type
343  vector<Expr> argTps;
344  for(Expr::iterator i=e[2].begin(), iend=e[2].end(); i!=iend; ++i) {
345  if(i->getKind() != RAW_LIST || i->arity() < 2)
346  throw EvalException
347  ("DEFUN: bad argument declaration:\n\n "+i->toString()
348  +"\n\nIn the following statement:\n\n "
349  +e.toString());
350  Expr tp((*i)[i->arity()-1]);
351  for(int j=0, jend=i->arity()-1; j<jend; ++j)
352  argTps.push_back(tp);
353  }
354  argTps.push_back(e[3]);
355  Expr fnType = d_vc->listExpr("ARROW", argTps);
356  Expr newDecl; // The resulting transformed declaration
357  if(e.arity() == 5) {
358  // Build the LAMBDA expression
359  Expr lambda(d_vc->listExpr("LAMBDA", e[2], e[4]));
360  // Construct the (CONST name fnType lambda) declaration
361  newDecl = d_vc->listExpr("CONST", e[1], fnType, lambda);
362  } else {
363  newDecl = d_vc->listExpr("CONST", e[1], fnType);
364  }
365  // Parse the new declaration
366  return evaluateCommand(newDecl);
367  break;
368  }
369  case TYPEDEF: {
370  if (e.arity() == 2) {
371  // Datatype command
372  DebugAssert(e.arity() == 2, "Bad TYPEDEF");
373  Expr res = d_vc->parseExpr(e[1]);
374  // convert res to vectors
375 
376  Expr eNames = res[0];
377  Expr eCons = res[1];
378  Expr eSel = res[2];
379  Expr eTypes = res[3];
380 
381  vector<string> names;
382  vector<vector<string> > constructors(eNames.arity());
383  vector<vector<vector<string> > > selectors(eNames.arity());
384  vector<vector<vector<Expr> > > types(eNames.arity());
385 
386  int i, j, k;
387  for (i = 0; i < eNames.arity(); ++i) {
388  names.push_back(eNames[i].getString());
389  selectors[i].resize(eSel[i].arity());
390  types[i].resize(eTypes[i].arity());
391  for (j = 0; j < eCons[i].arity(); ++j) {
392  constructors[i].push_back(eCons[i][j].getString());
393  for (k = 0; k < eSel[i][j].arity(); ++k) {
394  selectors[i][j].push_back(eSel[i][j][k].getString());
395  types[i][j].push_back(eTypes[i][j][k]);
396  }
397  }
398  }
399 
400  vector<Type> returnTypes;
401  d_vc->dataType(names, constructors, selectors, types, returnTypes);
402  break;
403  }
404  DebugAssert(e.arity() == 3, "Bad TYPEDEF");
405  Expr def(d_vc->parseExpr(e[2]));
406  Type t = d_vc->createType(e[1][0].getString(), def);
407  TRACE("commands", "evaluateNext: declare new TYPEDEF: ", t, "");
408  }
409  break;
410  case TYPE: {
411  if(e.arity() < 2)
412  throw EvalException("Bad TYPE declaration: "+e.toString());
413  Expr::iterator i=e.begin(), iend=e.end();
414  ++i; // Skip "TYPE" symbol
415  for(; i!=iend; ++i) {
416  if(i->getKind() != ID)
417  throw EvalException("Type name must be an identifier: "+i->toString());
418  Type t = d_vc->createType((*i)[0].getString());
419  TRACE("commands", "evaluateNext: declare new TYPEDECL: ", t, "");
420  }
421  }
422  break;
423  case ASSERT: {
424  if(e.arity() != 2)
425  throw EvalException("ASSERT requires exactly one argument, but is given "
426  +int2string(e.arity()-1)+":\n "+e.toString());
427  TRACE_MSG("commands", "** [commands] Asserting formula");
428  d_vc->assertFormula(d_vc->parseExpr(e[1]));
429  break;
430  }
431  case QUERY: {
432  if(e.arity() != 2)
433  throw EvalException("QUERY requires exactly one argument, but is given "
434  +int2string(e.arity()-1)+":\n "+e.toString());
435  TRACE_MSG("commands", "** [commands] Query formula");
436  QueryResult qres = d_vc->query(d_vc->parseExpr(e[1]));
437  if (qres == UNKNOWN && d_vc->getFlags()["unknown-check-model"].getBool())
438  qres = d_vc->tryModelGeneration();
439  reportResult(qres);
440  if (qres == INVALID) {
441  if (d_vc->getFlags()["counterexample"].getBool()) {
443  }
444  if (d_vc->getFlags()["model"].getBool()) {
445  printModel();
446  }
447  }
448  break;
449  }
450  case CHECKSAT: {
451  QueryResult qres;
452  TRACE_MSG("commands", "** [commands] CheckSat");
453  if (e.arity() == 1) {
454  qres = d_vc->checkUnsat(d_vc->trueExpr());
455  }
456  else if (e.arity() == 2) {
457  qres = d_vc->checkUnsat(d_vc->parseExpr(e[1]));
458  }
459  else {
460  throw EvalException("CHECKSAT requires no more than one argument, but is given "
461  +int2string(e.arity()-1)+":\n "+e.toString());
462  }
463  if (qres == UNKNOWN && !d_vc->getFlags()["translate"].getBool() && d_vc->getFlags()["unknown-check-model"].getBool())
464  qres = d_vc->tryModelGeneration();
465  reportResult(qres, false);
466  if (qres == SATISFIABLE) {
467  if (d_vc->getFlags()["counterexample"].getBool()) {
469  }
470  if (d_vc->getFlags()["model"].getBool()) {
471  printModel();
472  }
473  }
474 // {//for debug only by yeting
475 // Proof p = d_vc->getProof();
476 // if (d_vc->getFlags()["printResults"].getBool()) {
477 // cout << p << endl;
478 // cout << flush;
479 // }
480 // }
481 
482 
483  break;
484  }
485  case CONTINUE: {
486  if (e.arity() != 1) {
487  throw EvalException("CONTINUE takes no arguments");
488  }
489  TRACE_MSG("commands", "** [commands] Continue");
490  QueryResult qres = d_vc->checkContinue();
491  if (d_vc->getFlags()["printResults"].getBool()) {
492  switch (qres) {
493  case VALID:
494  cout << "No more models found." << endl;
495  break;
496  case INVALID:
497  cout << "Model found" << endl;
498  break;
499  case ABORT:
500  cout << "Unknown: resource limit exhausted." << endl;
501  break;
502  case UNKNOWN: {
503  // Vector of reasons in case of incomplete result
504  vector<string> reasons;
505  IF_DEBUG(bool b =) d_vc->incomplete(reasons);
506  DebugAssert(b, "Expected incompleteness");
507  cout << "Unknown.\n\n";
508  cout << "CVC3 was incomplete in this example due to:";
509  for(vector<string>::iterator i=reasons.begin(), iend=reasons.end();
510  i!=iend; ++i)
511  cout << "\n * " << (*i);
512  cout << endl << endl;
513  break;
514  }
515  default:
516  FatalAssert(false, "Unexpected case");
517  }
518  cout << flush;
519  }
520  break;
521  }
522  case RESTART: {
523  if(e.arity() != 2)
524  throw EvalException("RESTART requires exactly one argument, but is given "
525  +int2string(e.arity()-1)+":\n "+e.toString());
526  TRACE_MSG("commands", "** [commands] Restart formula");
527  QueryResult qres = d_vc->restart(d_vc->parseExpr(e[1]));
528  reportResult(qres);
529  if (qres == INVALID) {
530  if (d_vc->getFlags()["counterexample"].getBool()) {
532  }
533  if (d_vc->getFlags()["model"].getBool()) {
534  printModel();
535  }
536  }
537  break;
538  }
539  case TRANSFORM: {
540  if(e.arity() != 2)
541  throw EvalException
542  ("TRANSFORM requires exactly one argument, but is given "
543  +int2string(e.arity()-1)+":\n "+e.toString());
544  TRACE_MSG("commands", "** [commands] Transforming expression");
545  Expr ee = d_vc->parseExpr(e[1]);
546  e = d_vc->simplify(ee);
547  if (d_vc->getFlags()["printResults"].getBool()) d_vc->printExpr(e);
548  break;
549  }
550  case PRINT:
551  if(e.arity() != 2)
552  throw EvalException
553  ("PRINT requires exactly one argument, but is given "
554  +int2string(e.arity()-1)+":\n "+e.toString());
555  d_vc->printExpr(d_vc->parseExpr(e[1]));
556  break;
557  case PUSH:
558  case POP:
559  case PUSH_SCOPE:
560  case POP_SCOPE: {
561  int arg;
562  if (e.arity() == 1) arg = 1;
563  else {
564  DebugAssert(e.arity() == 2 && e[1].getKind() == RATIONAL_EXPR,
565  "Bad argument to "+kindName);
566  arg = e[1].getRational().getInt();
567  if(arg <= 0)
568  throw EvalException("Argument to PUSH or POP is <= 0");
569  }
570  if (kind == PUSH) {
571  for (int i = 0; i < arg; i++) {
572  d_vc->push();
573  }
574  }
575  else if (kind == POP) {
576  if(arg > d_vc->stackLevel())
577  throw EvalException("Argument to POP is out of range:\n"
578  " current stack level = "
580  +"\n argument = "
581  +int2string(arg));
582  for (int i = 0; i < arg; i++) {
583  d_vc->pop();
584  }
585  }
586  else if (kind == PUSH_SCOPE) {
587  for (int i = 0; i < arg; i++) {
588  d_vc->pushScope();
589  }
590  }
591  else if (kind == POP_SCOPE) {
592  if(arg >= d_vc->scopeLevel())
593  throw EvalException("Argument to POP_SCOPE is out of range:\n"
594  " current scope = "
596  +"\n argument = "
597  +int2string(arg));
598  for (int i = 0; i < arg; i++) {
599  d_vc->popScope();
600  }
601  }
602  break;
603  }
604  case POPTO:
605  case POPTO_SCOPE: {
606  int arg;
607  if (e.arity() == 1) arg = 0;
608  else {
609  DebugAssert(e.arity() == 2 && e[1].getKind() == RATIONAL_EXPR,
610  "Bad argument to "+kindName);
611  arg = e[1].getRational().getInt();
612  }
613  if (kind == POPTO) {
614  d_vc->popto(arg);
615  }
616  else {
617  d_vc->poptoScope(arg);
618  }
619  break;
620  }
621  case RESET: {
622  throw ResetException();
623  break;
624  }
625  case WHERE:
626  case ASSERTIONS:
627  case ASSUMPTIONS:
628  {
629  vector<Expr> assertions;
630  ExprMap<bool> skolemAxioms;
631  ExprMap<bool> visited;
632 
633  d_vc->getAssumptions(assertions);
634 
635  if (d_vc->getFlags()["printResults"].getBool()) {
636  cout << "Current stack level is " << d_vc->stackLevel()
637  << " (scope " << d_vc->scopeLevel() << ")." << endl;
638  if (assertions.size() == 0) {
639  cout << "% No active assumptions\n";
640  } else {
641  cout << "% Active assumptions:\n";
642  for (unsigned i = 0; i < assertions.size(); i++) {
643  cout << "ASSERT " << assertions[i] << ";" << endl;
644  findAxioms(assertions[i], skolemAxioms, visited);
645  }
646  ExprMap<bool>::iterator it = skolemAxioms.begin();
647  ExprMap<bool>::iterator end = skolemAxioms.end();
648  if (it != end) {
649  cout << "% Skolemization axioms" << endl;
650  for(; it!=end; ++it)
651  cout << "ASSERT " << skolemizeAx((*it).first) << ";" << endl;
652  }
653  }
654  cout << endl;
655  }
656  break;
657  }
658  case COUNTEREXAMPLE: {
659  if (d_vc->getFlags()["printResults"].getBool()) {
661  }
662  break;
663  }
664  case COUNTERMODEL: {
665  if (d_vc->getFlags()["printResults"].getBool()) {
666  try {
667  printModel();
668  } catch (Exception& e) {
669  throw EvalException(e.toString());
670  }
671  }
672  break;
673  }
674  case TRACE: { // Set a trace flag
675 #ifdef _CVC3_DEBUG_MODE
676  if(e.arity() != 2)
677  throw EvalException("TRACE takes exactly one string argument");
678  if(!e[1].isString())
679  throw EvalException("TRACE requires a string argument");
680  debugger.traceFlag(e[1].getString()) = true;
681 #endif
682  }
683  break;
684  case UNTRACE: { // Unset a trace flag
685 #ifdef _CVC3_DEBUG_MODE
686  if(e.arity() != 2)
687  throw EvalException("UNTRACE takes exactly one string argument");
688  if(!e[1].isString())
689  throw EvalException("UNTRACE requires a string argument");
690  debugger.traceFlag(e[1].getString()) = false;
691 #endif
692  }
693  break;
694  case OPTION: {
695  if(e.arity() != 3)
696  throw EvalException("OPTION takes exactly two arguments "
697  "(name and value of a flag)");
698  if(!e[1].isString())
699  throw EvalException("OPTION: flag name must be a string");
700  CLFlags& flags = d_vc->getFlags();
701  string name(e[1].getString());
702  vector<string> names;
703  size_t n = flags.countFlags(name, names);
704  if(n != 1)
705  throw EvalException("OPTION: found "+int2string(n)
706  +" flags matching "+name
707  +".\nThe flag name must uniquely resolve.");
708  name = names[0];
709  const CLFlag& flag(flags[name]);
710  // If the flag is set on the command line, ignore it
711  if(flag.modified()) break;
712  switch(flag.getType()) {
713  case CLFLAG_BOOL:
714  if(!(e[2].isRational() && e[2].getRational().isInteger()))
715  throw EvalException("OPTION: flag "+name
716  +" expects a boolean value (0 or 1");
717  flags.setFlag(name, e[2].getRational().getInt() != 0);
718  break;
719  case CLFLAG_INT:
720  if(!(e[2].isRational() && e[2].getRational().isInteger()))
721  throw EvalException("OPTION: flag "+name+" expects an integer value");
722  flags.setFlag(name, e[2].getRational().getInt());
723  break;
724  case CLFLAG_STRING:
725  if(!e[2].isString())
726  throw EvalException("OPTION: flag "+name+" expects a string value");
727  flags.setFlag(name, e[2].getString());
728  break;
729  default:
730  throw EvalException("OPTION: the type of flag "+name
731  +" is not supported by the OPTION commnand");
732  break;
733  }
734  d_vc->reprocessFlags();
735  }
736  break;
737  case GET_VALUE: {
738  ExprMap<Expr> m;
740 
741  if (d_vc->getFlags()["printResults"].getBool()) {
742  cout << "(";
743  }
744  for(int i = 0; i < e[1].arity(); ++i) {
745  Expr res = d_vc->getValue(d_vc->parseExpr(e[1][i]));
746  if (d_vc->getFlags()["printResults"].getBool()) {
747  cout << res;
748  if(i < e[1].arity() - 1) {
749  cout << endl;
750  }
751  }
752  }
753  if (d_vc->getFlags()["printResults"].getBool()) {
754  cout << ")" << endl;
755  }
756  break;
757  }
758  case GET_ASSIGNMENT: {
759  ExprMap<Expr> m;
761 
762  Expr res = d_vc->getAssignment();
763  if (d_vc->getFlags()["printResults"].getBool()) {
764  cout << res << endl;
765  cout << flush;
766  }
767  break;
768  }
769  case DUMP_PROOF: {
770  Proof p = d_vc->getProof();
771  if (d_vc->getFlags()["printResults"].getBool()) {
772  cout << p << endl;
773  cout << flush;
774  }
775  break;
776  }
777  case DUMP_ASSUMPTIONS: { // Assumption tracking
778  vector<Expr> assertions;
779 
780  bool b = d_vc->inconsistent(assertions);
781  DebugAssert(b, "not inconsistent");
782 
783  if (d_vc->getFlags()["printResults"].getBool()) {
784  if(assertions.size() == 0) {
785  cout << "% No relevant assumptions\n";
786  } else {
787  cout << "% Relevant assumptions:\n";
788  for (unsigned i = 0; i < assertions.size(); i++) {
789  cout << Expr(ASSERT, assertions[i]) << "\n";
790  }
791  }
792  cout << endl << flush;
793  }
794  break;
795  }
796  case DUMP_TCC: {
797  const Expr& tcc = d_vc->getTCC();
798 
799  if (d_vc->getFlags()["printResults"].getBool()) {
800  if(tcc.isNull())
801  cout << "% No TCC is avaialble" << endl;
802  else
803  cout << "% TCC for the last declaration, ASSERT, or QUERY:\n\n"
804  << tcc << endl;
805  }
806  break;
807  }
808  case DUMP_TCC_ASSUMPTIONS: {
809  vector<Expr> assertions;
810  d_vc->getAssumptionsTCC(assertions);
811  if (d_vc->getFlags()["printResults"].getBool()) {
812  if(assertions.size() == 0) {
813  cout << "% No relevant assumptions\n";
814  } else {
815  cout << "% Relevant assumptions for the last TCC:\n";
816  for (unsigned i = 0; i < assertions.size(); i++) {
817  cout << Expr(ASSERT, assertions[i]) << "\n";
818  }
819  }
820  cout << endl << flush;
821  }
822  break;
823  }
824  case DUMP_TCC_PROOF: {
825  const Proof& tcc = d_vc->getProofTCC();
826  if (d_vc->getFlags()["printResults"].getBool()) {
827  if(tcc.isNull())
828  cout << "% No TCC is avaialble" << endl;
829  else
830  cout << "% Proof of TCC for the last declaration, ASSERT, or QUERY:\n\n"
831  << tcc << endl;
832  }
833  break;
834  }
835  case DUMP_CLOSURE: {
836  const Expr& cl = d_vc->getClosure();
837  if (d_vc->getFlags()["printResults"].getBool()) {
838  if(cl.isNull())
839  cout << "% No closure is avaialble" << endl;
840  else
841  cout << "% Closure for the last QUERY:\n\n" << cl << endl;
842  }
843  break;
844  }
845  case DUMP_CLOSURE_PROOF: {
846  const Proof& cl = d_vc->getProofClosure();
847  if (d_vc->getFlags()["printResults"].getBool()) {
848  if(cl.isNull())
849  cout << "% No closure is avaialble" << endl;
850  else
851  cout << "% Proof of closure for the last QUERY:\n\n" << cl << endl;
852  }
853  break;
854  }
855  case ECHO:
856  if(e.arity() != 2)
857  throw EvalException("ECHO: wrong number of arguments: "
858  + e.toString());
859  if(!e[1].isString())
860  throw EvalException("ECHO: the argument must be a string: "
861  +e.toString());
862  if (d_vc->getFlags()["printResults"].getBool()) {
863  cout << e[1].getString();
864  cout << endl << flush;
865  }
866  break;
867  case SEQ: {
868  Expr::iterator i=e.begin(), iend=e.end();
869  ++i; // Skip "SEQ" symbol
870  bool success = true;
871  for(; i!=iend; ++i) {
872  try {
873  success = success && evaluateCommand(*i);
874  } catch(ResetException& e) {
875  if (++i == iend) throw e;
876  throw EvalException("RESET can only be the last command in a sequence");
877  }
878  }
879  return success;
880  }
881  case ARITH_VAR_ORDER: {
882  if (e.arity() <= 2)
883  throw EvalException("ARITH_VAR_ORDER takes at least two arguments");
884  Expr smaller;
885  Expr bigger = d_vc->parseExpr(e[1]);
886  for (int i = 2; i < e.arity(); i ++) {
887  smaller = bigger;
888  bigger = d_vc->parseExpr(e[i]);
889  if (!d_vc->addPairToArithOrder(smaller, bigger))
890  throw EvalException("ARITH_VAR_ORDER only takes arithmetic terms");
891  }
892  return true;
893  }
894  case ANNOTATION: {
895  for (int i = 1; i < e.arity(); ++i) {
896  if (e[i].arity() == 1) {
897  d_vc->logAnnotation(Expr(ANNOTATION, e[i][0]));
898  }
899  else {
900  DebugAssert(e[i].arity() == 2, "Expected arity 2");
901  d_vc->logAnnotation(Expr(ANNOTATION, e[i][0], e[i][1]));
902  }
903  }
904  break;
905  }
906  case INCLUDE: { // read in the specified file
907  if(e.arity() != 2)
908  throw EvalException("INCLUDE takes exactly one string argument");
909  if(!e[1].isString())
910  throw EvalException("INCLUDE requires a string argument");
911  ifstream fs;
912  fs.open(e[1].getString().c_str(),ios::in);
913  if(!fs.is_open()) {
914  fs.close();
915  throw EvalException("File "+e[1].getString()+" does not exist");
916  }
917  fs.close();
918  d_vc->loadFile(e[1].getString(),
919  d_vc->getEM()->getInputLang(),
920  d_vc->getFlags()["interactive"].getBool(),
921  true /* nested call */);
922  break;
923  }
924  case HELP:
925  cout << "Use the -help command-line option for help." << endl;
926  break;
927  case DUMP_SIG:
928  case DBG:
929  case SUBSTITUTE:
930  case GET_CHILD:
931  case GET_TYPE:
932  case CHECK_TYPE:
933  case FORGET:
934  case CALL:
935  default:
936  throw EvalException("Unknown command: " + e.toString());
937  break;
938  }
939  TRACE_MSG("commands", "evaluateCommand => true }");
940  return true;
941 }
942 
943 
945 {
946  bool error(false);
947  try {
948  bool success(true);
949  while(success) {
950  try {
951  success = evaluateNext();
952  } catch (ResetException& e) {
953  if (d_calledFromParser) {
954  throw EvalException("RESET not supported within INCLUDEd file");
955  }
956  d_parser->reset();
957  d_vc->reset();
958  success = true;
959  } catch (EvalException& e) {
960  error= true;
961  cerr << "*** Eval Error:\n " << e << endl;
962  }
963  }
964 
965  }
966 
967  catch(Exception& e) {
968  cerr << "*** Fatal exception:\n" << e << endl;
969  error= true;
970  } catch(...) {
971  cerr << "*** Unknown fatal exception caught" << endl;
972  error= true;
973  }
974 
975  if (error)
976  {
977  d_parser->printLocation(cerr);
978  cerr << ": this is the location of the error" << endl;
979  }
980 }
int arity() const
Definition: expr.h:1201
bool isNull() const
Definition: expr.h:1223
void printModel()
Definition: vc_cmd.cpp:157
iterator begin() const
Begin iterator.
Definition: expr.h:1211
Definition: kinds.h:104
void printCounterExample()
Definition: vc_cmd.cpp:228
bool evaluateCommand(const Expr &e)
Take a parsed Expr and evaluate it.
Definition: vc_cmd.cpp:267
Definition: kinds.h:118
virtual Op createOp(const std::string &name, const Type &type)=0
Create a named uninterpreted function with a given type.
virtual bool inconsistent(std::vector< Expr > &assumptions)=0
Returns true if the current context is inconsistent.
Data structure of expressions in CVC3.
Definition: expr.h:133
virtual void popScope()=0
Restore the current context to its state at the last internal checkpoint. Do not use unless you know ...
virtual ExprManager * getEM()=0
Return the ExprManager.
virtual Expr getValue(Expr e)=0
Evaluate an expression and return a concrete value in the model.
Generic API for a validity checker.
virtual Expr parseExpr(const Expr &e)=0
Parse an expression using a Theory-specific parser.
virtual int scopeLevel()=0
Returns the current scope level. Initially, the scope level is 1.
virtual void pushScope()=0
Checkpoint the current context and increase the internal scope level. Do not use unless you know what...
QueryResult
Definition: queryresult.h:32
bool isNull() const
Definition: proof.h:47
void insert(const Expr &e, const Data &d)
Definition: expr_map.h:177
virtual void reset()=0
Destroy and recreate validity checker: resets everything except for flags.
virtual Expr getClosure()=0
After successful query, return its closure |- Gamma => phi.
bool isSkolem() const
Definition: expr.h:432
An exception to be thrown at typecheck error.
iterator find(const Expr &e)
Definition: expr_map.h:194
Definition: kinds.h:105
virtual QueryResult checkUnsat(const Expr &e)=0
Check satisfiability of the expr in the current context.
void setFlag(const std::string &name, const CLFlag &f)
virtual void poptoScope(int scopeLevel)=0
Restore the current context to the given scopeLevel.
Definition: kinds.h:136
InputLanguage getInputLang() const
Get the input language for printing.
virtual Context * getCurrentContext()=0
Get the current context.
MS C++ specific settings.
Definition: type.h:42
virtual void printExpr(const Expr &e)=0
Prints e to the standard output.
SMT-LIB v2 format.
Definition: lang.h:52
STL namespace.
iterator begin()
Definition: expr_map.h:190
virtual QueryResult restart(const Expr &e)=0
Restart the most recent query with e as an additional assertion.
ValidityChecker * d_vc
Definition: vc_cmd.h:40
Definition: kinds.h:123
Definition: kinds.h:100
Definition: kinds.h:240
Parser * d_parser
Definition: vc_cmd.h:41
virtual void popto(int stackLevel)=0
Restore the current context to the given stackLevel.
void findAxioms(const Expr &e, ExprMap< bool > &skolemAxioms, ExprMap< bool > &visited)
Definition: vc_cmd.cpp:41
#define DebugAssert(cond, str)
Definition: debug.h:408
const Expr & getExistential() const
Get the existential axiom expression for skolem constant.
Definition: expr.h:1123
Definition: kinds.h:96
virtual void push()=0
Checkpoint the current context and increase the scope level.
Definition: kinds.h:97
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
bool isRational(const Expr &e)
Definition: theory_arith.h:177
virtual Expr getAssignment()=0
Returns the list of pairs (name value) for each :named attribute.
virtual std::string toString() const
Definition: exception.h:46
Expr getOpExpr() const
Get expression of operator (for APPLY Exprs only)
Definition: expr.h:1191
virtual void pop()=0
Restore the current context to its state at the last checkpoint.
#define TRACE_MSG(flag, msg)
Definition: debug.h:414
bool isClosure() const
Definition: expr.h:1007
size_t count(const Expr &e) const
Definition: expr_map.h:173
Definition: kinds.h:242
virtual CLFlags & getFlags() const =0
Return the set of command-line flags.
void printLocation(std::ostream &out) const
Definition: kinds.h:44
static ValidityChecker * vc
Definition: main.cpp:51
Identifier is (ID (STRING_EXPR "name"))
Definition: kinds.h:46
#define FatalAssert(cond, msg)
If something goes horribly wrong, print a message and abort immediately with exit(1).
Definition: debug.h:37
virtual void getAssumptions(std::vector< Expr > &assumptions)=0
Get all assumptions made in this and all previous contexts.
std::string toString() const
Print the expression to a string.
Definition: expr.cpp:344
virtual bool addPairToArithOrder(const Expr &smaller, const Expr &bigger)=0
Definition: kinds.h:101
Expr skolemExpr(int i) const
Create a Skolem constant for the i'th variable of an existential (*this)
Definition: expr.h:977
std::string d_name_of_cur_ctxt
Definition: vc_cmd.h:44
bool debug_skolem
Definition: vc_cmd.cpp:225
Expr iffExpr(const Expr &right) const
Definition: expr.h:965
Definition: kinds.h:102
virtual void assertFormula(const Expr &e)=0
Assert a new formula in the current context.
Definition: kinds.h:88
int getKind() const
Definition: expr.h:1168
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
Definition: expr_stream.h:110
const Expr & getBody() const
Get the body of the closure Expr.
Definition: expr.h:1069
std::string int2string(int n)
Definition: cvc_util.h:46
void processCommands()
Definition: vc_cmd.cpp:944
Definition: kinds.h:58
virtual void logAnnotation(const Expr &annot)=0
Add an annotation to the current script - prints annot when translating.
Definition: kinds.h:98
Definition: kinds.h:131
virtual int stackLevel()=0
Returns the current stack level. Initial level is 0.
#define IF_DEBUG(code)
Definition: debug.h:406
Generic API for a validity checker.
Definition: vc.h:92
virtual QueryResult query(const Expr &e)=0
Check validity of e in the current context.
virtual Proof getProofTCC()=0
Returns the proof of TCC of the last assumption or query.
CtxtMap d_map
Definition: vc_cmd.h:45
virtual void getConcreteModel(ExprMap< Expr > &m)=0
Will assign concrete values to all user created variables.
Definition: kinds.h:90
bool modified() const
Return true if the flag was modified from the default value (e.g. set on the command line) ...
Definition: kinds.h:94
Definition: kinds.h:107
bool d_calledFromParser
Definition: vc_cmd.h:46
Definition: kinds.h:246
virtual QueryResult tryModelGeneration()=0
int getKind(const std::string &name)
Return a kind associated with a name. Returns NULL_KIND if not found.
virtual void loadFile(const std::string &fileName, InputLanguage lang=PRESENTATION_LANG, bool interactive=false, bool calledFromParser=false)=0
Read and execute the commands from a file given by name ("" means stdin)
Definition: kinds.h:95
virtual Type createType(const std::string &typeName)=0
Create named user-defined uninterpreted type.
virtual void reprocessFlags()=0
Force reprocessing of all flags.
const std::vector< Expr > & getVars() const
Get bound variables from a closure Expr.
Definition: expr.h:1062
SMT-LIB format.
Definition: lang.h:34
Definition: kinds.h:125
virtual Expr listExpr(const std::vector< Expr > &kids)=0
Create a list Expr.
Definition: kinds.h:93
void reportResult(QueryResult qres, bool checkingValidity=true)
Definition: vc_cmd.cpp:102
Definition: kinds.h:53
virtual Proof getProof()=0
Returns the proof term for the last proven query.
virtual bool incomplete()=0
Returns true if the invalid result from last query() is imprecise.
void printSymbols(Expr e, ExprMap< bool > &cache)
Print the symbols in e, cache results.
Definition: vc_cmd.cpp:188
bool evaluateNext()
Definition: vc_cmd.cpp:73
Definition: kinds.h:124
Definition: kinds.h:129
Expr substExpr(const std::vector< Expr > &oldTerms, const std::vector< Expr > &newTerms) const
Definition: expr.cpp:178
virtual Expr varExpr(const std::string &name, const Type &type)=0
Create a variable with a given name and type.
Definition: expr.cpp:35
Definition: kinds.h:99
virtual QueryResult checkContinue()=0
Get the next model.
virtual Type dataType(const std::string &name, const std::string &constructor, const std::vector< std::string > &selectors, const std::vector< Expr > &types)=0
Single datatype, single constructor.
bool done() const
virtual Expr trueExpr()=0
Return TRUE Expr.
iterator end()
Definition: expr_map.h:191
size_t countFlags(const std::string &name) const
virtual Proof getProofClosure()=0
Construct a proof of the query closure |- Gamma => phi.
virtual void getCounterExample(std::vector< Expr > &assumptions, bool inOrder=true)=0
Return the internal assumptions that make the queried formula false.
virtual Expr getTCC()=0
Returns the TCC of the last assumption or query.
virtual void getAssumptionsTCC(std::vector< Expr > &assumptions)=0
Return the set of assumptions used in the proof of the last TCC.
Expr skolemizeAx(const Expr &e)
Definition: vc_cmd.cpp:61
bool dagFlag(bool flag=true)
Set the DAG flag (return previous value)
Definition: expr_stream.h:175
Definition: kinds.h:106
Nice SAL-like language for manually written specs.
Definition: lang.h:32
CLFlagType getType() const
Return the type of the flag.
InputLanguage getOutputLang() const
Get the output language for printing.
iterator end() const
End iterator.
Definition: expr.h:1217
virtual Expr simplify(const Expr &e)=0
Simplify e with respect to the current context.