void GetInfoCommand::invoke(SmtEngine* smtEngine) {
try {
- d_result = smtEngine->getInfo(d_flag).getValue();
+ stringstream ss;
+ ss << smtEngine->getInfo(d_flag);
+ d_result = ss.str();
} catch(BadOptionException& bo) {
d_result = "unsupported";
}
}
function registerOperatorToKind {
- operatorKind=$1
- applyKind=$2
- metakind_operatorKinds="${metakind_operatorKinds} case kind::$applyKind: return kind::$operatorKind;
+ operatorKind=$1
+ applyKind=$2
+ metakind_operatorKinds="${metakind_operatorKinds} case kind::$applyKind: return kind::$operatorKind;
";
}
exit 1
fi
- if [ $mk = OPERATOR ] || [ $mk = PARAMETERIZED -a "$k" != SORT_TYPE ]; then
- if [ $lb = 0 ]; then
+ if [ $mk = OPERATOR -o $mk = PARAMETERIZED ]; then
+ if [ $mk = PARAMETERIZED -a "$k" = SORT_TYPE ]; then
+ # exception: zero-ary SORT_TYPE is permitted for sort constructors
+ :
+ elif [ $mk = PARAMETERIZED -a "$k" = APPLY ]; then
+ # exception: zero-ary APPLY is permitted for defined zero-ary functions
+ :
+ elif [ $lb = 0 ]; then
echo "$kf:$lineno: error in range \`$nc' for \`$k': $mk-kinded kinds must always take at least one child" >&2
exit 1
fi
/* Returns true if name is bound to a defined function. */
bool Parser::isDefinedFunction(const std::string& name) {
- return isFunction(name) && d_declScope.isBoundDefinedFunction(name);
+ // more permissive in type than isFunction(), because defined
+ // functions can be zero-ary and declared functions cannot.
+ return d_declScope.isBoundDefinedFunction(name);
}
/* Returns true if name is bound to a function returning boolean. */
d_logicOperators.insert(kind);
}
+void Parser::preemptCommand(Command* cmd) {
+ d_commandQueue.push_back(cmd);
+}
+
Command* Parser::nextCommand() throw(ParserException) {
Debug("parser") << "nextCommand()" << std::endl;
Command* cmd = NULL;
- if(!done()) {
- try {
- cmd = d_input->parseCommand();
- if(cmd == NULL) {
- setDone();
- }
- } catch(ParserException& e) {
+ if(!d_commandQueue.empty()) {
+ cmd = d_commandQueue.front();
+ d_commandQueue.pop_front();
+ if(cmd == NULL) {
setDone();
- throw;
- } catch(Exception& e) {
- setDone();
- stringstream ss;
- ss << e;
- parseError( ss.str() );
}
- }
- Debug("parser") << "nextCommand() => " << cmd << std::endl;
- return cmd;
-}
-
-Expr Parser::nextExpression() throw(ParserException) {
- Debug("parser") << "nextExpression()" << std::endl;
- Expr result;
- if(!done()) {
- try {
- result = d_input->parseExpr();
- if(result.isNull()) {
+ } else {
+ if(!done()) {
+ try {
+ cmd = d_input->parseCommand();
+ d_commandQueue.push_back(cmd);
+ cmd = d_commandQueue.front();
+ d_commandQueue.pop_front();
+ if(cmd == NULL) {
+ setDone();
+ }
+ } catch(ParserException& e) {
setDone();
+ throw;
+ } catch(Exception& e) {
+ setDone();
+ stringstream ss;
+ ss << e;
+ parseError( ss.str() );
}
- } catch(ParserException& e) {
- setDone();
- throw;
- } catch(Exception& e) {
- setDone();
- stringstream ss;
- ss << e;
- parseError( ss.str() );
}
}
- Debug("parser") << "nextExpression() => " << result << std::endl;
- return result;
+ Debug("parser") << "nextCommand() => " << cmd << std::endl;
+ return cmd;
}
#include <string>
#include <set>
+#include <list>
#include "input.h"
#include "parser_exception.h"
/** The set of operators available in the current logic. */
std::set<Kind> d_logicOperators;
+ /**
+ * "Preemption commands": extra commands implied by subterms that
+ * should be issued before the currently-being-parsed command is
+ * issued. Used to support SMT-LIBv2 ":named" attribute on terms.
+ */
+ std::list<Command*> d_commandQueue;
+
/** Lookup a symbol in the given namespace. */
Expr getSymbol(const std::string& var_name, SymbolType type);
const std::vector<Type>
mkSorts(const std::vector<std::string>& names);
- /** Add an operator to the current legal set.
+ /**
+ * Add an operator to the current legal set.
*
* @param kind the built-in operator to add
*/
void addOperator(Kind kind);
+ /**
+ * Preempt the next returned command with other ones; used to
+ * support the :named attribute in SMT-LIBv2, which implicitly
+ * inserts a new command before the current one.
+ */
+ void preemptCommand(Command* cmd);
+
/** Is the symbol bound to a boolean variable? */
bool isBoolean(const std::string& name);
bool isPredicate(const std::string& name);
Command* nextCommand() throw(ParserException);
- Expr nextExpression() throw(ParserException);
inline void parseError(const std::string& msg) throw (ParserException) {
d_input->parseError(msg);
sortSymbol[t]
{ Debug("parser") << "declare fun: '" << name << "'" << std::endl;
if( sorts.size() > 0 ) {
- t = EXPR_MANAGER->mkFunctionType(sorts,t);
+ t = EXPR_MANAGER->mkFunctionType(sorts, t);
}
PARSER_STATE->mkVar(name, t);
$cmd = new DeclarationCommand(name,t); }
++i) {
sorts.push_back((*i).second);
}
- t = EXPR_MANAGER->mkFunctionType(sorts,t);
+ t = EXPR_MANAGER->mkFunctionType(sorts, t);
}
PARSER_STATE->pushScope();
for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
Kind kind;
std::string name;
std::vector<Expr> args;
+ SExpr sexpr;
}
: /* a built-in operator application */
LPAREN_TOK builtinOp[kind] termList[args,expr] RPAREN_TOK
PARSER_STATE->getFunction(name) :
PARSER_STATE->getVariable(name);
args[0] = expr;
- // TODO: check arity
- expr = MK_EXPR(isDefinedFunction ? CVC4::kind::APPLY : CVC4::kind::APPLY_UF, args); }
+ expr = MK_EXPR(isDefinedFunction ?
+ CVC4::kind::APPLY :
+ CVC4::kind::APPLY_UF, args); }
| /* a let binding */
LPAREN_TOK LET_TOK LPAREN_TOK
RPAREN_TOK
{ PARSER_STATE->popScope(); }
- | /* a variable */
- symbol[name,CHECK_DECLARED,SYM_VARIABLE]
- { expr = PARSER_STATE->getVariable(name); }
+ /* a variable */
+ | symbol[name,CHECK_DECLARED,SYM_VARIABLE]
+ { const bool isDefinedFunction =
+ PARSER_STATE->isDefinedFunction(name);
+ if(isDefinedFunction) {
+ expr = MK_EXPR(CVC4::kind::APPLY,
+ PARSER_STATE->getFunction(name));
+ } else {
+ expr = PARSER_STATE->getVariable(name);
+ }
+ }
+
+ /* attributed expressions */
+ | LPAREN_TOK ATTRIBUTE_TOK term[expr] KEYWORD symbolicExpr[sexpr] RPAREN_TOK
+ { std::string attr = AntlrInput::tokenText($KEYWORD);
+ if(attr == ":named") {
+ name = sexpr.getValue();
+ // FIXME ensure expr is a closed subterm
+ // check that sexpr is a fresh function symbol
+ PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE);
+ // define it
+ Expr func = PARSER_STATE->mkFunction(name, expr.getType());
+ // bind name to expr with define-fun
+ Command* c =
+ new DefineFunctionCommand(func, std::vector<Expr>(), expr);
+ PARSER_STATE->preemptCommand(c);
+ } else {
+ std::stringstream ss;
+ ss << "Attribute `" << attr << "' not supported";
+ PARSER_STATE->parseError(ss.str());
+ }
+ }
/* constants */
| INTEGER_LITERAL
EXIT_TOK : 'exit';
ITE_TOK : 'ite';
LET_TOK : 'let';
+ATTRIBUTE_TOK : '!';
LPAREN_TOK : '(';
RPAREN_TOK : ')';
SET_LOGIC_TOK : 'set-logic';
#include "util/output.h"
#include "util/exception.h"
#include "util/options.h"
+#include "util/configuration.h"
#include "prop/prop_engine.h"
#include "theory/theory_engine.h"
d_propEngine(NULL),
d_assertionList(NULL),
d_haveAdditions(false),
- d_lastResult() {
+ d_status() {
NodeManagerScope nms(d_nodeManager);
throw(BadOptionException) {
Debug("smt") << "SMT setInfo(" << key << ", " << value << ")" << endl;
if(key == ":name" ||
- key == ":status" ||
key == ":source" ||
key == ":category" ||
key == ":difficulty" ||
key == ":notes") {
// ignore these
return;
+ } else if(key == ":status") {
+ string s;
+ if(value.isAtom()) {
+ s = value.getValue();
+ }
+ if(s != "sat" && s != "unsat" && s != "unknown") {
+ throw BadOptionException("argument to (set-info :status ..) must be "
+ "`sat' or `unsat' or `unknown'");
+ }
+ if(s == "sat") {
+ d_status = Result::SAT;
+ } else if(s == "unsat") {
+ d_status = Result::UNSAT;
+ } else if(s == "unknown") {
+ d_status = Result::SAT_UNKNOWN;
+ } else {
+ Unreachable();
+ }
+ return;
}
throw BadOptionException();
}
-const SExpr& SmtEngine::getInfo(const string& key) const
+SExpr SmtEngine::getInfo(const string& key) const
throw(BadOptionException) {
Debug("smt") << "SMT getInfo(" << key << ")" << endl;
- // FIXME implement me
- throw BadOptionException();
+ if(key == ":all-statistics") {
+ vector<SExpr> stats;
+ for(StatisticsRegistry::const_iterator i = StatisticsRegistry::begin();
+ i != StatisticsRegistry::end();
+ ++i) {
+ vector<SExpr> v;
+ v.push_back((*i)->getName());
+ v.push_back((*i)->getValue());
+ stats.push_back(v);
+ }
+ return stats;
+ } else if(key == ":error-behavior") {
+ return SExpr("immediate-exit");
+ } else if(key == ":name") {
+ return Configuration::getName();
+ } else if(key == ":version") {
+ return Configuration::getVersionString();
+ } else if(key == ":authors") {
+ return Configuration::about();
+ } else if(key == ":status") {
+ enum Result::SAT status = d_status.asSatisfiabilityResult().isSAT();
+ switch(status) {
+ case Result::SAT:
+ return SExpr("sat");
+ case Result::UNSAT:
+ return SExpr("unsat");
+ case Result::SAT_UNKNOWN:
+ return SExpr("unknown");
+ default:
+ Unhandled(status);
+ }
+ } else if(key == ":reason-unknown") {
+ throw BadOptionException();
+ } else {
+ throw BadOptionException();
+ }
}
void SmtEngine::setOption(const string& key, const SExpr& value)
throw BadOptionException();
}
-const SExpr& SmtEngine::getOption(const string& key) const
+SExpr SmtEngine::getOption(const string& key) const
throw(BadOptionException) {
Debug("smt") << "SMT getOption(" << key << ")" << endl;
- // FIXME implement me
- throw BadOptionException();
+ if(key == ":print-success") {
+ return SExpr("true");
+ } else if(key == ":expand-definitions") {
+ throw BadOptionException();
+ } else if(key == ":interactive-mode") {
+ throw BadOptionException();
+ } else if(key == ":produce-proofs") {
+ throw BadOptionException();
+ } else if(key == ":produce-unsat-cores") {
+ throw BadOptionException();
+ } else if(key == ":produce-models") {
+ throw BadOptionException();
+ } else if(key == ":produce-assignments") {
+ throw BadOptionException();
+ } else if(key == ":regular-output-channel") {
+ return SExpr("stdout");
+ } else if(key == ":diagnostic-output-channel") {
+ return SExpr("stderr");
+ } else if(key == ":random-seed") {
+ throw BadOptionException();
+ } else if(key == ":verbosity") {
+ throw BadOptionException();
+ } else {
+ throw BadOptionException();
+ }
}
void SmtEngine::defineFunction(Expr func,
Debug("smt") << "SMT defineFunction(" << func << ")" << endl;
NodeManagerScope nms(d_nodeManager);
Type formulaType = formula.getType(true);// type check body
- if(formulaType != FunctionType(func.getType()).getRangeType()) {
+ Type funcType = func.getType();
+ Type rangeType = funcType.isFunction() ?
+ FunctionType(funcType).getRangeType() : funcType;
+ if(formulaType != rangeType) {
stringstream ss;
ss << "Defined function's declared type does not match that of body\n"
<< "The function : " << func << "\n"
- << "Its range type: "
- << FunctionType(func.getType()).getRangeType() << "\n"
+ << "Its range type: " << rangeType << "\n"
<< "The body : " << formula << "\n"
<< "Body type : " << formulaType;
throw TypeCheckingException(func, ss.str());
}
TNode formulaNode = formula.getTNode();
DefinedFunction def(funcNode, formalsNodes, formulaNode);
- d_haveAdditions = true;
+ // Permit (check-sat) (define-fun ...) (get-value ...) sequences.
+ // Otherwise, (check-sat) (get-value ((! foo :named bar))) breaks
+ // d_haveAdditions = true;
d_definedFunctions->insert(funcNode, def);
}
ensureBoolean(e);// ensure expr is type-checked at this point
SmtEnginePrivate::addFormula(*this, e.getNode());
Result r = check().asSatisfiabilityResult();
- d_lastResult = r;
+ d_status = r;
d_haveAdditions = false;
Debug("smt") << "SMT checkSat(" << e << ") ==> " << r << endl;
return r;
ensureBoolean(e);// ensure expr is type-checked at this point
SmtEnginePrivate::addFormula(*this, e.getNode().notNode());
Result r = check().asValidityResult();
- d_lastResult = r;
+ d_status = r;
d_haveAdditions = false;
Debug("smt") << "SMT query(" << e << ") ==> " << r << endl;
return r;
"Cannot get value when produce-models options is off.";
throw ModalException(msg);
}
- if(d_lastResult.asSatisfiabilityResult() != Result::SAT ||
+ if(d_status.asSatisfiabilityResult() != Result::SAT ||
d_haveAdditions) {
const char* msg =
"Cannot get value unless immediately proceded by SAT/INVALID response.";
d_context->pop();
Debug("userpushpop") << "SmtEngine: popped to level "
<< d_context->getLevel() << endl;
- // clear out last result: get-value/get-assignment no longer
- // available here
- d_lastResult = Result();
+ // FIXME: should we reset d_status here?
+ // SMT-LIBv2 spec seems to imply no, but it would make sense to..
}
}/* CVC4 namespace */
bool d_haveAdditions;
/**
- * Result of last checkSat/query.
+ * Most recent result of last checkSat/query or (set-info :status).
*/
- Result d_lastResult;
+ Result d_status;
/**
* This is called by the destructor, just before destroying the
/**
* Query information about the SMT environment.
*/
- const SExpr& getInfo(const std::string& key) const
+ SExpr getInfo(const std::string& key) const
throw(BadOptionException);
/**
/**
* Get an aspect of the current SMT execution environment.
*/
- const SExpr& getOption(const std::string& key) const
+ SExpr getOption(const std::string& key) const
throw(BadOptionException);
/**
"The kind of nodes representing built-in operators"
variable FUNCTION "function"
-parameterized APPLY FUNCTION 1: "defined function application"
+parameterized APPLY FUNCTION 0: "defined function application"
operator EQUAL 2 "equality"
operator DISTINCT 2: "disequality"
throw (TypeCheckingExceptionPrivate) {
TNode f = n.getOperator();
TypeNode fType = f.getType(check);
- if( !fType.isFunction() ) {
+ if( !fType.isFunction() && n.getNumChildren() > 0 ) {
throw TypeCheckingExceptionPrivate(n, "operator does not have function type");
}
if( check ) {
- if (n.getNumChildren() != fType.getNumChildren() - 1) {
- throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the function type");
- }
- TNode::iterator argument_it = n.begin();
- TNode::iterator argument_it_end = n.end();
- TypeNode::iterator argument_type_it = fType.begin();
- for(; argument_it != argument_it_end; ++argument_it) {
- if((*argument_it).getType() != *argument_type_it) {
- throw TypeCheckingExceptionPrivate(n, "argument types do not match the function type");
+ if(fType.isFunction()) {
+ if(n.getNumChildren() != fType.getNumChildren() - 1) {
+ throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the function type");
+ }
+ TNode::iterator argument_it = n.begin();
+ TNode::iterator argument_it_end = n.end();
+ TypeNode::iterator argument_type_it = fType.begin();
+ for(; argument_it != argument_it_end; ++argument_it) {
+ if((*argument_it).getType() != *argument_type_it) {
+ throw TypeCheckingExceptionPrivate(n, "argument types do not match the function type");
+ }
+ }
+ } else {
+ if( n.getNumChildren() > 0 ) {
+ throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the function type");
}
}
}
- return fType.getRangeType();
+ return fType.isFunction() ? fType.getRangeType() : fType;
}
};/* class ApplyTypeRule */
** configuration information about the CVC4 library.
**/
+#include <string>
+
#include "util/configuration.h"
#include "util/configuration_private.h"
+#include "cvc4autoconfig.h"
using namespace std;
namespace CVC4 {
+string Configuration::getName() {
+ return PACKAGE_NAME;
+}
+
bool Configuration::isDebugBuild() {
return IS_DEBUG_BUILD;
}
public:
+ static std::string getName();
+
static bool isDebugBuild();
static bool isTracingBuild();
#include <string>
#include <ostream>
+#include <sstream>
#include <iomanip>
#include <set>
#include <ctime>
class CVC4_PUBLIC StatisticsRegistry {
private:
- struct StatCmp;
+ struct StatCmp {
+ inline bool operator()(const Stat* s1, const Stat* s2) const;
+ };/* class StatisticsRegistry::StatCmp */
typedef std::set< Stat*, StatCmp > StatSet;
static StatSet d_registeredStats;
public:
+
+ typedef StatSet::const_iterator const_iterator;
+
static void flushStatistics(std::ostream& out);
static inline void registerStat(Stat* s) throw(AssertionException);
static inline void unregisterStat(Stat* s) throw(AssertionException);
+
+ static inline const_iterator begin() {
+ return d_registeredStats.begin();
+ }
+ static inline const_iterator end() {
+ return d_registeredStats.end();
+ }
};/* class StatisticsRegistry */
public:
- Stat(const std::string& s) throw(CVC4::AssertionException) : d_name(s)
- {
+ Stat(const std::string& s) throw(CVC4::AssertionException) :
+ d_name(s) {
if(__CVC4_USE_STATISTICS) {
AlwaysAssert(d_name.find(s_delim) == std::string::npos);
}
const std::string& getName() const {
return d_name;
}
-};/* class Stat */
-
-struct StatisticsRegistry::StatCmp {
- bool operator()(const Stat* s1, const Stat* s2) const
- {
- return (s1->getName()) < (s2->getName());
- }
-};/* class StatCmp */
+ virtual std::string getValue() const = 0;
+};/* class Stat */
+inline bool StatisticsRegistry::StatCmp::operator()(const Stat* s1,
+ const Stat* s2) const {
+ return s1->getName() < s2->getName();
+}
-inline void StatisticsRegistry::registerStat(Stat* s) throw(AssertionException) {
+inline void StatisticsRegistry::registerStat(Stat* s)
+ throw(AssertionException) {
if(__CVC4_USE_STATISTICS) {
AlwaysAssert(d_registeredStats.find(s) == d_registeredStats.end());
d_registeredStats.insert(s);
}/* StatisticsRegistry::registerStat */
-inline void StatisticsRegistry::unregisterStat(Stat* s) throw(AssertionException) {
+inline void StatisticsRegistry::unregisterStat(Stat* s)
+ throw(AssertionException) {
if(__CVC4_USE_STATISTICS) {
AlwaysAssert(d_registeredStats.find(s) != d_registeredStats.end());
d_registeredStats.erase(s);
template <class T>
class DataStat : public Stat {
public:
- DataStat(const std::string& s) : Stat(s) {}
+ DataStat(const std::string& s) :
+ Stat(s) {
+ }
virtual const T& getData() const = 0;
virtual void setData(const T&) = 0;
out << getData();
}
}
+
+ std::string getValue() const {
+ std::stringstream ss;
+ ss << getData();
+ return ss.str();
+ }
};/* class DataStat */
const T* d_data;
public:
- ReferenceStat(const std::string& s):
- DataStat<T>(s), d_data(NULL)
- {}
+ ReferenceStat(const std::string& s) :
+ DataStat<T>(s),
+ d_data(NULL) {
+ }
- ReferenceStat(const std::string& s, const T& data):
- DataStat<T>(s), d_data(NULL)
- {
+ ReferenceStat(const std::string& s, const T& data) :
+ DataStat<T>(s),
+ d_data(NULL) {
setData(data);
}
d_data = &t;
}
}
+
const T& getData() const {
if(__CVC4_USE_STATISTICS) {
return *d_data;
public:
- BackedStat(const std::string& s, const T& init): DataStat<T>(s), d_data(init)
- {}
+ BackedStat(const std::string& s, const T& init) :
+ DataStat<T>(s),
+ d_data(init) {
+ }
void setData(const T& t) {
if(__CVC4_USE_STATISTICS) {
class IntStat : public BackedStat<int64_t> {
public:
- IntStat(const std::string& s, int64_t init): BackedStat<int64_t>(s, init)
- {}
+ IntStat(const std::string& s, int64_t init) :
+ BackedStat<int64_t>(s, init) {
+ }
IntStat& operator++() {
if(__CVC4_USE_STATISTICS) {
projects / cvc5.git / commitdiff