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;
iterator begin() const
Begin iterator.
void printCounterExample()
bool evaluateCommand(const Expr &e)
Take a parsed Expr and evaluate it.
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.
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...
void insert(const Expr &e, const Data &d)
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.
An exception to be thrown at typecheck error.
iterator find(const Expr &e)
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.
InputLanguage getInputLang() const
Get the input language for printing.
virtual Context * getCurrentContext()=0
Get the current context.
MS C++ specific settings.
virtual void printExpr(const Expr &e)=0
Prints e to the standard output.
virtual QueryResult restart(const Expr &e)=0
Restart the most recent query with e as an additional assertion.
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)
#define DebugAssert(cond, str)
const Expr & getExistential() const
Get the existential axiom expression for skolem constant.
virtual void push()=0
Checkpoint the current context and increase the scope level.
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
bool isRational(const Expr &e)
virtual Expr getAssignment()=0
Returns the list of pairs (name value) for each :named attribute.
virtual std::string toString() const
Expr getOpExpr() const
Get expression of operator (for APPLY Exprs only)
virtual void pop()=0
Restore the current context to its state at the last checkpoint.
#define TRACE_MSG(flag, msg)
size_t count(const Expr &e) const
virtual CLFlags & getFlags() const =0
Return the set of command-line flags.
void printLocation(std::ostream &out) const
static ValidityChecker * vc
Identifier is (ID (STRING_EXPR "name"))
#define FatalAssert(cond, msg)
If something goes horribly wrong, print a message and abort immediately with exit(1).
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.
virtual bool addPairToArithOrder(const Expr &smaller, const Expr &bigger)=0
Expr skolemExpr(int i) const
Create a Skolem constant for the i'th variable of an existential (*this)
std::string d_name_of_cur_ctxt
Expr iffExpr(const Expr &right) const
virtual void assertFormula(const Expr &e)=0
Assert a new formula in the current context.
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
const Expr & getBody() const
Get the body of the closure Expr.
std::string int2string(int n)
virtual void logAnnotation(const Expr &annot)=0
Add an annotation to the current script - prints annot when translating.
virtual int stackLevel()=0
Returns the current stack level. Initial level is 0.
Generic API for a validity checker.
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.
virtual void getConcreteModel(ExprMap< Expr > &m)=0
Will assign concrete values to all user created variables.
bool modified() const
Return true if the flag was modified from the default value (e.g. set on the command line) ...
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)
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.
virtual Expr listExpr(const std::vector< Expr > &kids)=0
Create a list Expr.
void reportResult(QueryResult qres, bool checkingValidity=true)
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.
Expr substExpr(const std::vector< Expr > &oldTerms, const std::vector< Expr > &newTerms) const
virtual Expr varExpr(const std::string &name, const Type &type)=0
Create a variable with a given name and type.
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.
virtual Expr trueExpr()=0
Return TRUE Expr.
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)
bool dagFlag(bool flag=true)
Set the DAG flag (return previous value)
Nice SAL-like language for manually written specs.
CLFlagType getType() const
Return the type of the flag.
InputLanguage getOutputLang() const
Get the output language for printing.
iterator end() const
End iterator.
virtual Expr simplify(const Expr &e)=0
Simplify e with respect to the current context.