33 : d_vc(vc), d_parser(parser), d_name_of_cur_ctxt(
"DEFAULT"),
34 d_calledFromParser(calledFromParser)
43 if(visited.
count(e)>0)
45 else visited[e] =
true;
64 const vector<Expr>boundVars = e.
getVars();
65 for(
unsigned int i=0; i<boundVars.size(); i++) {
67 vars.push_back(skolV);
79 TRACE_MSG(
"commands",
"** [commands] Parsing command...");
81 TRACE(
"commands verbose",
"evaluateNext(", e,
")");
84 cerr <<
"*** " << e <<
endl;
85 IF_DEBUG(++(debugger.counter(
"parse errors"));)
91 TRACE_MSG(
"commands",
"** [commands] Null command; read again");
95 TRACE_MSG(
"commands",
"** [commands] parse-only; skipping evaluateCommand");
109 cout <<
"unsat" <<
endl;
112 cout <<
"sat" <<
endl;
116 cout <<
"unknown" <<
endl;
125 cout << (checkingValidity ?
"Valid." :
"Unsatisfiable.") <<
endl;
128 cout << (checkingValidity ?
"Invalid." :
"Satisfiable.") <<
endl;
131 cout <<
"Unknown: resource limit exhausted." <<
endl;
135 vector<string> reasons;
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();
142 cout <<
"\n * " << (*i);
143 cout << endl <<
endl;
165 cout <<
" Did not find concrete model for any vars" <<
endl;
167 cout <<
"%Satisfiable Variable Assignment: % \n";
168 for(; it!= end; it++) {
170 if(it->first.getType().isBool()) {
172 "Bad variable assignement: e = "+(it->first).toString()
173 +
"\n\n val = "+(it->second).toString());
174 if((it->second).isTrue())
180 eq = (it->first).eqExpr(it->second);
190 if (cache.
find(e) != cache.
end())
return;
197 os << e.getType().getExpr();
207 os << op.getType().getExpr();
215 for (; i != iend; ++i) {
230 vector<Expr> assertions;
239 for (i = 0; i < assertions.size(); i++) {
244 if (assertions.size() == 0) {
245 cout <<
"% There are no assertions\n";
248 cout <<
"% Assertions which make the QUERY invalid:\n";
250 for (i = 0; i < assertions.size(); i++) {
252 findAxioms(assertions[i], skolemAxioms, visited);
256 cout <<
"% Including skolemization axioms:\n";
271 if(e.getKind() !=
RAW_LIST || e.arity() == 0 || e[0].getKind() !=
ID)
273 const string& kindName = e[0][0].getString();
283 vars = e[1].getKids();
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)
291 if (t.isFunction()) {
292 for(vector<Expr>::iterator i=vars.begin(), iend=vars.end();
295 TRACE(
"commands",
"evaluateNext: declare new uninterpreted function: ",
300 for(vector<Expr>::iterator i=vars.begin(), iend=vars.end();
304 TRACE_MSG(
"commands",
"** [commands] Declare new variable");
305 TRACE(
"commands verbose",
"evaluateNext: declare new UCONST: ",
309 }
else if(e.arity() == 4) {
310 TRACE_MSG(
"commands",
"** [commands] Define new constant");
318 TRACE(
"commands verbose",
"evaluateNext: define new function: ",
319 e[1][0].getString(),
"");
322 TRACE(
"commands verbose",
"evaluateNext: define new variable: ",
323 e[1][0].getString(),
"");
326 throw EvalException(
"Wrong number of arguments in CONST: "+e.toString());
330 if(e.arity() != 5 && e.arity() != 4)
332 (
"DEFUN requires 3 or 4 arguments:"
333 " (DEFUN f (args) type [ body ]):\n\n "
337 (
"2nd argument of DEFUN must be a list of arguments:\n\n "
344 for(
Expr::iterator i=e[2].begin(), iend=e[2].end(); i!=iend; ++i) {
345 if(i->getKind() !=
RAW_LIST || i->arity() < 2)
347 (
"DEFUN: bad argument declaration:\n\n "+i->toString()
348 +
"\n\nIn the following statement:\n\n "
350 Expr tp((*i)[i->arity()-1]);
351 for(
int j=0, jend=i->arity()-1; j<jend; ++j)
352 argTps.push_back(tp);
354 argTps.push_back(e[3]);
361 newDecl =
d_vc->
listExpr(
"CONST", e[1], fnType, lambda);
370 if (e.arity() == 2) {
376 Expr eNames = res[0];
379 Expr eTypes = res[3];
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());
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]);
400 vector<Type> returnTypes;
401 d_vc->
dataType(names, constructors, selectors, types, returnTypes);
407 TRACE(
"commands",
"evaluateNext: declare new TYPEDEF: ", t,
"");
415 for(; i!=iend; ++i) {
419 TRACE(
"commands",
"evaluateNext: declare new TYPEDECL: ", t,
"");
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");
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");
452 TRACE_MSG(
"commands",
"** [commands] CheckSat");
453 if (e.arity() == 1) {
456 else if (e.arity() == 2) {
460 throw EvalException(
"CHECKSAT requires no more than one argument, but is given "
461 +
int2string(e.arity()-1)+
":\n "+e.toString());
486 if (e.arity() != 1) {
489 TRACE_MSG(
"commands",
"** [commands] Continue");
494 cout <<
"No more models found." <<
endl;
497 cout <<
"Model found" <<
endl;
500 cout <<
"Unknown: resource limit exhausted." <<
endl;
504 vector<string> reasons;
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();
511 cout <<
"\n * " << (*i);
512 cout << endl <<
endl;
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");
542 (
"TRANSFORM requires exactly one argument, but is given "
543 +
int2string(e.arity()-1)+
":\n "+e.toString());
544 TRACE_MSG(
"commands",
"** [commands] Transforming expression");
553 (
"PRINT requires exactly one argument, but is given "
554 +
int2string(e.arity()-1)+
":\n "+e.toString());
562 if (e.arity() == 1) arg = 1;
565 "Bad argument to "+kindName);
566 arg = e[1].getRational().getInt();
571 for (
int i = 0; i < arg; i++) {
575 else if (kind ==
POP) {
578 " current stack level = "
582 for (
int i = 0; i < arg; i++) {
587 for (
int i = 0; i < arg; i++) {
593 throw EvalException(
"Argument to POP_SCOPE is out of range:\n"
598 for (
int i = 0; i < arg; i++) {
607 if (e.arity() == 1) arg = 0;
610 "Bad argument to "+kindName);
611 arg = e[1].getRational().getInt();
629 vector<Expr> assertions;
638 if (assertions.size() == 0) {
639 cout <<
"% No active assumptions\n";
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);
649 cout <<
"% Skolemization axioms" <<
endl;
675 #ifdef _CVC3_DEBUG_MODE
677 throw EvalException(
"TRACE takes exactly one string argument");
680 debugger.traceFlag(e[1].getString()) =
true;
685 #ifdef _CVC3_DEBUG_MODE
687 throw EvalException(
"UNTRACE takes exactly one string argument");
690 debugger.traceFlag(e[1].getString()) =
false;
697 "(name and value of a flag)");
701 string name(e[1].getString());
702 vector<string> names;
706 +
" flags matching "+name
707 +
".\nThe flag name must uniquely resolve.");
709 const CLFlag& flag(flags[name]);
714 if(!(e[2].
isRational() && e[2].getRational().isInteger()))
716 +
" expects a boolean value (0 or 1");
717 flags.
setFlag(name, e[2].getRational().getInt() != 0);
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());
726 throw EvalException(
"OPTION: flag "+name+
" expects a string value");
727 flags.
setFlag(name, e[2].getString());
731 +
" is not supported by the OPTION commnand");
744 for(
int i = 0; i < e[1].arity(); ++i) {
748 if(i < e[1].arity() - 1) {
778 vector<Expr> assertions;
784 if(assertions.size() == 0) {
785 cout <<
"% No relevant assumptions\n";
787 cout <<
"% Relevant assumptions:\n";
788 for (
unsigned i = 0; i < assertions.size(); i++) {
792 cout <<
endl << flush;
801 cout <<
"% No TCC is avaialble" <<
endl;
803 cout <<
"% TCC for the last declaration, ASSERT, or QUERY:\n\n"
809 vector<Expr> assertions;
812 if(assertions.size() == 0) {
813 cout <<
"% No relevant assumptions\n";
815 cout <<
"% Relevant assumptions for the last TCC:\n";
816 for (
unsigned i = 0; i < assertions.size(); i++) {
820 cout <<
endl << flush;
828 cout <<
"% No TCC is avaialble" <<
endl;
830 cout <<
"% Proof of TCC for the last declaration, ASSERT, or QUERY:\n\n"
839 cout <<
"% No closure is avaialble" <<
endl;
841 cout <<
"% Closure for the last QUERY:\n\n" << cl <<
endl;
849 cout <<
"% No closure is avaialble" <<
endl;
851 cout <<
"% Proof of closure for the last QUERY:\n\n" << cl <<
endl;
863 cout << e[1].getString();
864 cout <<
endl << flush;
871 for(; i!=iend; ++i) {
875 if (++i == iend)
throw e;
876 throw EvalException(
"RESET can only be the last command in a sequence");
883 throw EvalException(
"ARITH_VAR_ORDER takes at least two arguments");
886 for (
int i = 2; i < e.arity(); i ++) {
890 throw EvalException(
"ARITH_VAR_ORDER only takes arithmetic terms");
895 for (
int i = 1; i < e.arity(); ++i) {
896 if (e[i].arity() == 1) {
900 DebugAssert(e[i].arity() == 2,
"Expected arity 2");
908 throw EvalException(
"INCLUDE takes exactly one string argument");
912 fs.open(e[1].getString().c_str(),ios::in);
915 throw EvalException(
"File "+e[1].getString()+
" does not exist");
925 cout <<
"Use the -help command-line option for help." <<
endl;
939 TRACE_MSG(
"commands",
"evaluateCommand => true }");
954 throw EvalException(
"RESET not supported within INCLUDEd file");
961 cerr <<
"*** Eval Error:\n " << e <<
endl;
968 cerr <<
"*** Fatal exception:\n" << e <<
endl;
971 cerr <<
"*** Unknown fatal exception caught" <<
endl;
978 cerr <<
": this is the location of the error" <<
endl;