#include "expr/command.h"
#include "smt/smt_engine.h"
+#include "smt/bad_option_exception.h"
#include "util/output.h"
using namespace std;
/* class DefineFunctionCommand */
-DefineFunctionCommand::DefineFunctionCommand(const std::string& name,
- const std::vector<std::pair<std::string, Type> >& args,
- Type type,
- Expr formula) :
- d_name(name),
- d_args(args),
- d_type(type),
+DefineFunctionCommand::DefineFunctionCommand(Expr func,
+ const std::vector<Expr>& formals,
+ Expr formula) :
+ d_func(func),
+ d_formals(formals),
d_formula(formula) {
}
void DefineFunctionCommand::invoke(SmtEngine* smtEngine) {
- smtEngine->defineFunction(d_name, d_args, d_type, d_formula);
+ smtEngine->defineFunction(d_func, d_formals, d_formula);
}
void DefineFunctionCommand::toStream(std::ostream& out) const {
- out << "DefineFunction( \"" << d_name << "\", [";
- copy( d_args.begin(), d_args.end() - 1,
- ostream_iterator<std::pair<std::string, Type> >(out, ", ") );
- out << d_args.back();
- out << "], << " << d_type << " >>, << " << d_formula << " >> )";
+ out << "DefineFunction( \"" << d_func << "\", [";
+ if(d_formals.size() > 0) {
+ copy( d_formals.begin(), d_formals.end() - 1,
+ ostream_iterator<Expr>(out, ", ") );
+ out << d_formals.back();
+ }
+ out << "], << " << d_formula << " >> )";
}
/* class GetValueCommand */
try {
smtEngine->setInfo(d_flag, d_sexpr);
//d_result = "success";
- } catch(BadOption& bo) {
+ } catch(BadOptionException& bo) {
d_result = "unsupported";
}
}
void GetInfoCommand::invoke(SmtEngine* smtEngine) {
try {
d_result = smtEngine->getInfo(d_flag).getValue();
- } catch(BadOption& bo) {
+ } catch(BadOptionException& bo) {
d_result = "unsupported";
}
}
try {
smtEngine->setOption(d_flag, d_sexpr);
//d_result = "success";
- } catch(BadOption& bo) {
+ } catch(BadOptionException& bo) {
d_result = "unsupported";
}
}
void GetOptionCommand::invoke(SmtEngine* smtEngine) {
try {
d_result = smtEngine->getOption(d_flag).getValue();
- } catch(BadOption& bo) {
+ } catch(BadOptionException& bo) {
d_result = "unsupported";
}
}
class CVC4_PUBLIC DefineFunctionCommand : public Command {
protected:
- std::string d_name;
- std::vector<std::pair<std::string, Type> > d_args;
- Type d_type;
+ Expr d_func;
+ std::vector<Expr> d_formals;
Expr d_formula;
public:
- DefineFunctionCommand(const std::string& name,
- const std::vector<std::pair<std::string, Type> >& args,
- Type type, Expr formula);
+ DefineFunctionCommand(Expr func,
+ const std::vector<Expr>& formals,
+ Expr formula);
void invoke(SmtEngine* smtEngine);
void toStream(std::ostream& out) const;
};/* class DefineFunctionCommand */
d_node->toStream(out, depth, types);
}
-Node Expr::getNode() const {
+Node Expr::getNode() const throw() {
+ return *d_node;
+}
+
+TNode Expr::getTNode() const throw() {
return *d_node;
}
class Expr;
class ExprManager;
+class SmtEngine;
class Type;
+namespace smt {
+ class SmtEnginePrivate;
+}/* CVC4::smt namespace */
+
namespace expr {
class CVC4_PUBLIC ExprSetDepth;
class CVC4_PUBLIC ExprPrintTypes;
* Returns the actual internal node.
* @return the internal node
*/
- NodeTemplate<true> getNode() const;
+ NodeTemplate<true> getNode() const throw();
+
+ /**
+ * Returns the actual internal node as a TNode.
+ * @return the internal node
+ */
+ NodeTemplate<false> getTNode() const throw();
// Friend to access the actual internal expr information and private methods
friend class SmtEngine;
+ friend class smt::SmtEnginePrivate;
friend class ExprManager;
};
TypeNode getType(bool check = false) const
throw (CVC4::TypeCheckingExceptionPrivate, CVC4::AssertionException);
+ /**
+ * Substitution of Nodes.
+ */
+ Node substitute(TNode node, TNode replacement) const;
+
+ /**
+ * Simultaneous substitution of Nodes.
+ */
+ template <class Iterator1, class Iterator2>
+ Node substitute(Iterator1 nodesBegin,
+ Iterator1 nodesEnd,
+ Iterator2 replacementsBegin,
+ Iterator2 replacementsEnd) const;
+
/**
* Returns the kind of this node.
* @return the kind
return NodeManager::currentNM()->getType(*this, check);
}
+template <bool ref_count>
+Node NodeTemplate<ref_count>::substitute(TNode node,
+ TNode replacement) const {
+ NodeBuilder<> nb(getKind());
+ if(getMetaKind() == kind::metakind::PARAMETERIZED) {
+ // push the operator
+ nb << getOperator();
+ }
+ for(TNode::const_iterator i = begin(),
+ iend = end();
+ i != iend;
+ ++i) {
+ if(*i == node) {
+ nb << replacement;
+ } else {
+ (*i).substitute(node, replacement);
+ }
+ }
+ Node n = nb;
+ return n;
+}
+
+template <bool ref_count>
+template <class Iterator1, class Iterator2>
+Node NodeTemplate<ref_count>::substitute(Iterator1 nodesBegin,
+ Iterator1 nodesEnd,
+ Iterator2 replacementsBegin,
+ Iterator2 replacementsEnd) const {
+ Assert( nodesEnd - nodesBegin == replacementsEnd - replacementsBegin,
+ "Substitution iterator ranges must be equal size" );
+ Iterator1 j = find(nodesBegin, nodesEnd, *this);
+ if(j != nodesEnd) {
+ return *(replacementsBegin + (j - nodesBegin));
+ } else if(getNumChildren() == 0) {
+ return *this;
+ } else {
+ NodeBuilder<> nb(getKind());
+ if(getMetaKind() == kind::metakind::PARAMETERIZED) {
+ // push the operator
+ nb << getOperator();
+ }
+ for(TNode::const_iterator i = begin(),
+ iend = end();
+ i != iend;
+ ++i) {
+ nb << (*i).substitute(nodesBegin, nodesEnd,
+ replacementsBegin, replacementsEnd);
+ }
+ Node n = nb;
+ return n;
+ }
+}
+
#ifdef CVC4_DEBUG
/**
* Pretty printer for use within gdb. This is not intended to be used
return iterator(d_i++);
}
- typedef std::input_iterator_tag iterator_category;
- };
+ iterator& operator--() {
+ --d_i;
+ return *this;
+ }
+
+ iterator operator--(int) {
+ return iterator(d_i--);
+ }
+
+ iterator& operator+=(difference_type p) {
+ d_i += p;
+ return *this;
+ }
+
+ iterator& operator-=(difference_type p) {
+ d_i -= p;
+ return *this;
+ }
+
+ iterator operator+(difference_type p) {
+ return iterator(d_i + p);
+ }
+
+ iterator operator-(difference_type p) {
+ return iterator(d_i - p);
+ }
+
+ difference_type operator-(iterator i) {
+ return d_i - i.d_i;
+ }
+
+ typedef std::random_access_iterator_tag iterator_category;
+ };/* class NodeValue::iterator<T> */
+
+ // operator+ (as a function) cannot be a template, so we have to
+ // define two versions
+ friend NodeValue::iterator<NodeTemplate<true> >
+ operator+(NodeValue::iterator<NodeTemplate<true> >::difference_type p,
+ NodeValue::iterator<NodeTemplate<true> > i);
+ friend NodeValue::iterator<NodeTemplate<false> >
+ operator+(NodeValue::iterator<NodeTemplate<false> >::difference_type p,
+ NodeValue::iterator<NodeTemplate<false> > i);
/** Decrement ref counts of children */
inline void decrRefCounts();
};/* class NodeValue */
+/**
+ * Provides a symmetric addition operator to that already defined in
+ * the iterator class.
+ */
+inline NodeValue::iterator<NodeTemplate<true> >
+operator+(NodeValue::iterator<NodeTemplate<true> >::difference_type p,
+ NodeValue::iterator<NodeTemplate<true> > i) {
+ return i + p;
+}
+
+/**
+ * Provides a symmetric addition operator to that already defined in
+ * the iterator class.
+ */
+inline NodeValue::iterator<NodeTemplate<false> >
+operator+(NodeValue::iterator<NodeTemplate<false> >::difference_type p,
+ NodeValue::iterator<NodeTemplate<false> > i) {
+ return i + p;
+}
+
/**
* For hash_maps, hash_sets, etc.. but this is for expr package
* internal use only at present! This is likely to be POORLY
replacementsNodes.push_back(*(*i).d_typeNode);
}
- return makeType(d_typeNode->substitute(typesNodes, replacementsNodes));
+ return makeType(d_typeNode->substitute(typesNodes.begin(),
+ typesNodes.end(),
+ replacementsNodes.begin(),
+ replacementsNodes.end()));
}
void Type::toStream(ostream& out) const {
*/
class CVC4_PUBLIC Type {
+ friend class SmtEngine;
+ friend class SmtEnginePrivate;
friend class ExprManager;
friend class TypeNode;
friend class TypeHashStrategy;
Type(NodeManager* em, TypeNode* typeNode);
/** Accessor for derived classes */
- static TypeNode* getTypeNode(const Type& t) { return t.d_typeNode; }
+ static TypeNode* getTypeNode(const Type& t) throw() { return t.d_typeNode; }
public:
// push the operator
nb << TypeNode(d_nv->d_children[0]);
}
- for(TypeNode::iterator i = begin(), iend = end(); i != iend; ++i) {
+ for(TypeNode::const_iterator i = begin(),
+ iend = end();
+ i != iend;
+ ++i) {
if(*i == type) {
nb << replacement;
} else {
return nb.constructTypeNode();
}
-TypeNode TypeNode::substitute(const vector<TypeNode>& types,
- const vector<TypeNode>& replacements) const {
- vector<TypeNode>::const_iterator j = find(types.begin(), types.end(), *this);
- if(j != types.end()) {
- return replacements[j - types.begin()];
- } else if(getNumChildren() == 0) {
- return *this;
- } else {
- NodeBuilder<> nb(getKind());
- if(getMetaKind() == kind::metakind::PARAMETERIZED) {
- // push the operator
- nb << TypeNode(d_nv->d_children[0]);
- }
- for(TypeNode::iterator i = begin(), iend = end(); i != iend; ++i) {
- nb << (*i).substitute(types, replacements);
- }
- return nb.constructTypeNode();
- }
-}
-
bool TypeNode::isBoolean() const {
return getKind() == kind::TYPE_CONSTANT &&
getConst<TypeConstant>() == BOOLEAN_TYPE;
/**
* Simultaneous substitution of TypeNodes.
*/
- TypeNode substitute(const std::vector<TypeNode>& types,
- const std::vector<TypeNode>& replacements) const;
+ template <class Iterator1, class Iterator2>
+ TypeNode substitute(Iterator1 typesBegin,
+ Iterator1 typesEnd,
+ Iterator2 replacementsBegin,
+ Iterator2 replacementsEnd) const;
/**
* Structural comparison operator for expressions.
namespace CVC4 {
+template <class Iterator1, class Iterator2>
+TypeNode TypeNode::substitute(Iterator1 typesBegin,
+ Iterator1 typesEnd,
+ Iterator2 replacementsBegin,
+ Iterator2 replacementsEnd) const {
+ Assert( typesEnd - typesBegin == replacementsEnd - replacementsBegin,
+ "Substitution iterator ranges must be equal size" );
+ Iterator1 j = find(typesBegin, typesEnd, *this);
+ if(j != typesEnd) {
+ return *(replacementsBegin + (j - typesBegin));
+ } else if(getNumChildren() == 0) {
+ return *this;
+ } else {
+ NodeBuilder<> nb(getKind());
+ if(getMetaKind() == kind::metakind::PARAMETERIZED) {
+ // push the operator
+ nb << TypeNode(d_nv->d_children[0]);
+ }
+ for(TypeNode::const_iterator i = begin(),
+ iend = end();
+ i != iend;
+ ++i) {
+ nb << (*i).substitute(typesBegin, typesEnd,
+ replacementsBegin, replacementsEnd);
+ }
+ return nb.constructTypeNode();
+ }
+}
+
inline size_t TypeNode::getNumChildren() const {
return d_nv->getNumChildren();
}
DEFAULT_EXPR_DEPTH,
PRINT_EXPR_TYPES,
UF_THEORY,
+ LAZY_DEFINITION_EXPANSION,
INTERACTIVE,
NO_INTERACTIVE
};/* enum OptionValue */
{ "default-expr-depth", required_argument, NULL, DEFAULT_EXPR_DEPTH },
{ "print-expr-types", no_argument , NULL, PRINT_EXPR_TYPES },
{ "uf" , required_argument, NULL, UF_THEORY },
+ { "lazy-definition-expansion", no_argument, NULL, LAZY_DEFINITION_EXPANSION },
{ "interactive", no_argument , NULL, INTERACTIVE },
{ "no-interactive", no_argument , NULL, NO_INTERACTIVE },
{ NULL , no_argument , NULL, '\0' }
}
break;
+ case LAZY_DEFINITION_EXPANSION:
+ opts->lazyDefinitionExpansion = true;
+ break;
+
case INTERACTIVE:
opts->interactive = true;
opts->interactiveSetByUser = true;
Type t;
std::vector<Expr> terms;
std::vector<Type> sorts;
- std::vector<std::pair<std::string, Type> > sortedVars;
+ std::vector<std::pair<std::string, Type> > sortedVarNames;
SExpr sexpr;
}
: /* set the logic */
$cmd = new DeclarationCommand(name,t); }
| /* function definition */
DEFINE_FUN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
- LPAREN_TOK sortedVarList[sortedVars] RPAREN_TOK
+ LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
sortSymbol[t]
{ /* add variables to parser state before parsing term */
Debug("parser") << "define fun: '" << name << "'" << std::endl;
- if( sortedVars.size() > 0 ) {
+ if( sortedVarNames.size() > 0 ) {
std::vector<CVC4::Type> sorts;
- sorts.reserve(sortedVars.size());
+ sorts.reserve(sortedVarNames.size());
for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
- sortedVars.begin(), iend = sortedVars.end();
+ sortedVarNames.begin(), iend = sortedVarNames.end();
i != iend;
++i) {
sorts.push_back((*i).second);
}
PARSER_STATE->pushScope();
for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
- sortedVars.begin(), iend = sortedVars.end();
+ sortedVarNames.begin(), iend = sortedVarNames.end();
i != iend;
++i) {
- PARSER_STATE->mkVar((*i).first, (*i).second);
+ terms.push_back(PARSER_STATE->mkVar((*i).first, (*i).second));
}
}
term[expr]
// declare the name down here (while parsing term, signature
// must not be extended with the name itself; no recursion
// permitted)
- PARSER_STATE->mkFunction(name, t);
- $cmd = new DefineFunctionCommand(name, sortedVars, t, expr);
+ Expr func = PARSER_STATE->mkFunction(name, t);
+ $cmd = new DefineFunctionCommand(func, terms, expr);
}
| /* value query */
GET_VALUE_TOK LPAREN_TOK termList[terms,expr] RPAREN_TOK
smt_engine.cpp \
smt_engine.h \
noninteractive_exception.h \
- bad_option.h
+ bad_option_exception.h \
+ no_such_function_exception.h
+++ /dev/null
-/********************* */
-/*! \file bad_option.h
- ** \verbatim
- ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief An exception that is thrown when an option setting is not
- ** understood.
- **
- ** An exception that is thrown when an interactive-only feature while
- ** CVC4 is being used in a non-interactive setting (for example, the
- ** "(get-assertions)" command in an SMT-LIBv2 script).
- **/
-
-#include "cvc4_public.h"
-
-#ifndef __CVC4__SMT__BAD_OPTION_H
-#define __CVC4__SMT__BAD_OPTION_H
-
-#include "util/exception.h"
-
-namespace CVC4 {
-
-class CVC4_PUBLIC BadOption : public CVC4::Exception {
-public:
- BadOption() :
- Exception("Unrecognized informational or option key or setting") {
- }
-
- BadOption(const std::string& msg) :
- Exception(msg) {
- }
-
- BadOption(const char* msg) :
- Exception(msg) {
- }
-};/* class BadOption */
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__SMT__BAD_OPTION_H */
--- /dev/null
+/********************* */
+/*! \file bad_option_exception.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief An exception that is thrown when an option setting is not
+ ** understood.
+ **
+ ** An exception that is thrown when an interactive-only feature while
+ ** CVC4 is being used in a non-interactive setting (for example, the
+ ** "(get-assertions)" command in an SMT-LIBv2 script).
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__SMT__BAD_OPTION_EXCEPTION_H
+#define __CVC4__SMT__BAD_OPTION_EXCEPTION_H
+
+#include "util/exception.h"
+
+namespace CVC4 {
+
+class CVC4_PUBLIC BadOptionException : public CVC4::Exception {
+public:
+ BadOptionException() :
+ Exception("Unrecognized informational or option key or setting") {
+ }
+
+ BadOptionException(const std::string& msg) :
+ Exception(msg) {
+ }
+
+ BadOptionException(const char* msg) :
+ Exception(msg) {
+ }
+};/* class BadOptionException */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__SMT__BAD_OPTION_EXCEPTION_H */
--- /dev/null
+/********************* */
+/*! \file no_such_function_exception.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief An exception that is thrown when an option setting is not
+ ** understood.
+ **
+ ** An exception that is thrown when an interactive-only feature while
+ ** CVC4 is being used in a non-interactive setting (for example, the
+ ** "(get-assertions)" command in an SMT-LIBv2 script).
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__SMT__NO_SUCH_FUNCTION_EXCEPTION_H
+#define __CVC4__SMT__NO_SUCH_FUNCTION_EXCEPTION_H
+
+#include "util/exception.h"
+
+namespace CVC4 {
+
+class CVC4_PUBLIC NoSuchFunctionException : public CVC4::Exception {
+public:
+ NoSuchFunctionException(Expr name) :
+ Exception(std::string("Undefined function: `") + name.toString() + "': ") {
+ }
+
+ NoSuchFunctionException(Expr name, const std::string& msg) :
+ Exception(std::string("Undefined function: `") + name.toString() + "': " + msg) {
+ }
+};/* class NoSuchFunctionException */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__SMT__NO_SUCH_FUNCTION_EXCEPTION_H */
** The main entry point into the CVC4 library's SMT interface.
**/
+#include <vector>
+#include <string>
+
#include "smt/smt_engine.h"
#include "smt/noninteractive_exception.h"
+#include "smt/bad_option_exception.h"
+#include "smt/no_such_function_exception.h"
#include "context/context.h"
#include "context/cdlist.h"
+#include "expr/expr.h"
#include "expr/command.h"
#include "expr/node_builder.h"
#include "util/output.h"
#include "prop/prop_engine.h"
#include "theory/theory_engine.h"
+using namespace std;
using namespace CVC4;
using namespace CVC4::smt;
using namespace CVC4::prop;
namespace smt {
+/**
+ * Representation of a defined function. We keep these around in
+ * SmtEngine to permit expanding definitions late (and lazily), to
+ * support getValue() over defined functions, to support user output
+ * in terms of defined functions, etc.
+ */
+class DefinedFunction {
+ Node d_func;
+ std::vector<Node> d_formals;
+ Node d_formula;
+public:
+ DefinedFunction() {}
+ DefinedFunction(Node func, vector<Node> formals, Node formula) :
+ d_func(func),
+ d_formals(formals),
+ d_formula(formula) {
+ }
+ Node getFunction() const { return d_func; }
+ vector<Node> getFormals() const { return d_formals; }
+ Node getFormula() const { return d_formula; }
+};/* class DefinedFunction */
+
/**
* This is an inelegant solution, but for the present, it will work.
* The point of this is to separate the public and private portions of
* passes over the Node. TODO: may need to specify a LEVEL of
* preprocessing (certain contexts need more/less ?).
*/
- static Node preprocess(SmtEngine& smt, TNode n);
+ static Node preprocess(SmtEngine& smt, TNode n)
+ throw(NoSuchFunctionException, AssertionException);
/**
* Adds a formula to the current context.
*/
- static void addFormula(SmtEngine& smt, TNode n);
+ static void addFormula(SmtEngine& smt, TNode n)
+ throw(NoSuchFunctionException, AssertionException);
+
+ /**
+ * Expand definitions in n.
+ */
+ static Node expandDefinitions(SmtEngine& smt, TNode n)
+ throw(NoSuchFunctionException, AssertionException);
};/* class SmtEnginePrivate */
}/* namespace CVC4::smt */
-using ::CVC4::smt::SmtEnginePrivate;
+using namespace CVC4::smt;
-SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw () :
+SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw() :
d_context(em->getContext()),
d_exprManager(em),
d_nodeManager(em->getNodeManager()),
d_theoryEngine, d_context);
d_theoryEngine->setPropEngine(d_propEngine);
- d_functions = new(true) FunctionMap(d_context);
+ d_definedFunctions = new(true) DefinedFunctionMap(d_context);
if(d_options->interactive) {
d_assertionList = new(true) AssertionList(d_context);
d_assertionList->deleteSelf();
}
- d_functions->deleteSelf();
+ d_definedFunctions->deleteSelf();
delete d_theoryEngine;
delete d_propEngine;
delete d_decisionEngine;
}
-void SmtEngine::doCommand(Command* c) {
- NodeManagerScope nms(d_nodeManager);
- c->invoke(this);
-}
-
-void SmtEngine::setInfo(const std::string& key, const SExpr& value) throw(BadOption) {
+void SmtEngine::setInfo(const string& key, const SExpr& value)
+ throw(BadOptionException) {
+ if(key == ":status") {
+ return;
+ }
// FIXME implement me
+ throw BadOptionException();
}
-const SExpr& SmtEngine::getInfo(const std::string& key) const throw(BadOption) {
+const SExpr& SmtEngine::getInfo(const string& key) const
+ throw(BadOptionException) {
// FIXME implement me
- throw BadOption();
+ throw BadOptionException();
}
-void SmtEngine::setOption(const std::string& key, const SExpr& value) throw(BadOption) {
+void SmtEngine::setOption(const string& key, const SExpr& value)
+ throw(BadOptionException) {
// FIXME implement me
+ throw BadOptionException();
}
-const SExpr& SmtEngine::getOption(const std::string& key) const throw(BadOption) {
+const SExpr& SmtEngine::getOption(const string& key) const
+ throw(BadOptionException) {
// FIXME implement me
- throw BadOption();
+ throw BadOptionException();
}
-void SmtEngine::defineFunction(const string& name,
- const vector<pair<string, Type> >& args,
- Type type,
+void SmtEngine::defineFunction(Expr func,
+ const vector<Expr>& formals,
Expr formula) {
NodeManagerScope nms(d_nodeManager);
- d_functions->insert(name, make_pair(make_pair(args, type), formula));
+ TNode funcNode = func.getTNode();
+ vector<Node> formalsNodes;
+ for(vector<Expr>::const_iterator i = formals.begin(),
+ iend = formals.end();
+ i != iend;
+ ++i) {
+ formalsNodes.push_back((*i).getNode());
+ }
+ TNode formulaNode = formula.getTNode();
+ DefinedFunction def(funcNode, formalsNodes, formulaNode);
+ d_definedFunctions->insert(funcNode, def);
}
-Node SmtEnginePrivate::preprocess(SmtEngine& smt, TNode n) {
- return smt.d_theoryEngine->preprocess(n);
+Node SmtEnginePrivate::expandDefinitions(SmtEngine& smt, TNode n)
+ throw(NoSuchFunctionException, AssertionException) {
+ if(n.getKind() == kind::APPLY) {
+ TNode func = n.getOperator();
+ SmtEngine::DefinedFunctionMap::const_iterator i =
+ smt.d_definedFunctions->find(func);
+ DefinedFunction def = (*i).second;
+ vector<Node> formals = def.getFormals();
+
+ if(Debug.isOn("expand")) {
+ Debug("expand") << "found: " << n << endl;
+ Debug("expand") << " func: " << func << endl;
+ string name = func.getAttribute(expr::VarNameAttr());
+ Debug("expand") << " : \"" << name << "\"" << endl;
+ if(i == smt.d_definedFunctions->end()) {
+ throw NoSuchFunctionException(Expr(smt.d_exprManager, new Node(func)));
+ }
+ Debug("expand") << " defn: " << def.getFunction() << endl
+ << " [";
+ if(formals.size() > 0) {
+ copy( formals.begin(), formals.end() - 1,
+ ostream_iterator<Node>(Debug("expand"), ", ") );
+ Debug("expand") << formals.back();
+ }
+ Debug("expand") << "]" << endl
+ << " " << def.getFunction().getType() << endl
+ << " " << def.getFormula() << endl;
+ }
+
+ TNode fm = def.getFormula();
+ Node instance = fm.substitute(formals.begin(), formals.end(),
+ n.begin(), n.end());
+ Debug("expand") << "made : " << instance << endl;
+
+ Node expanded = expandDefinitions(smt, instance);
+ return expanded;
+ } else if(n.getNumChildren() == 0) {
+ return n;
+ } else {
+ Debug("expand") << "cons : " << n << endl;
+ NodeBuilder<> nb(n.getKind());
+ if(n.getMetaKind() == kind::metakind::PARAMETERIZED) {
+ Debug("expand") << "op : " << n.getOperator() << endl;
+ nb << n.getOperator();
+ }
+ for(TNode::iterator i = n.begin(),
+ iend = n.end();
+ i != iend;
+ ++i) {
+ Node expanded = expandDefinitions(smt, *i);
+ Debug("expand") << "exchld: " << expanded << endl;
+ nb << expanded;
+ }
+ Node node = nb;
+ return node;
+ }
+}
+
+Node SmtEnginePrivate::preprocess(SmtEngine& smt, TNode n)
+ throw(NoSuchFunctionException, AssertionException) {
+ if(!smt.d_options->lazyDefinitionExpansion) {
+ Node node = expandDefinitions(smt, n);
+ Debug("expand") << "have: " << n << endl
+ << "made: " << node << endl;
+ return smt.d_theoryEngine->preprocess(node);
+ } else {
+ return smt.d_theoryEngine->preprocess(n);
+ }
}
Result SmtEngine::check() {
return Result(Result::VALIDITY_UNKNOWN);
}
-void SmtEnginePrivate::addFormula(SmtEngine& smt, TNode n) {
+void SmtEnginePrivate::addFormula(SmtEngine& smt, TNode n)
+ throw(NoSuchFunctionException, AssertionException) {
Debug("smt") << "push_back assertion " << n << endl;
smt.d_propEngine->assertFormula(SmtEnginePrivate::preprocess(smt, n));
}
Unimplemented();
}
-Expr SmtEngine::getValue(Expr term) {
+Expr SmtEngine::getValue(Expr term)
+ throw(NoninteractiveException, AssertionException) {
+ if(!d_options->interactive) {
+ const char* msg =
+ "Cannot query the current assertion list when not in interactive mode.";
+ throw NoninteractiveException(msg);
+ }
+
NodeManagerScope nms(d_nodeManager);
+
Unimplemented();
}
#include "util/sexpr.h"
#include "util/hash.h"
#include "smt/noninteractive_exception.h"
-#include "smt/bad_option.h"
+#include "smt/no_such_function_exception.h"
+#include "smt/bad_option_exception.h"
// In terms of abstraction, this is below (and provides services to)
// ValidityChecker and above (and requires the services of)
namespace CVC4 {
-namespace context {
- class Context;
- template <class T> class CDList;
-}/* CVC4::context namespace */
-
+template <bool ref_count> class NodeTemplate;
+typedef NodeTemplate<true> Node;
+typedef NodeTemplate<false> TNode;
+class NodeHashFunction;
class Command;
class Options;
class TheoryEngine;
class DecisionEngine;
+namespace context {
+ class Context;
+ template <class T> class CDList;
+}/* CVC4::context namespace */
+
namespace prop {
class PropEngine;
}/* CVC4::prop namespace */
namespace smt {
+ /**
+ * Representation of a defined function. We keep these around in
+ * SmtEngine to permit expanding definitions late (and lazily), to
+ * support getValue() over defined functions, to support user output
+ * in terms of defined functions, etc.
+ */
+ class DefinedFunction;
+
class SmtEnginePrivate;
}/* CVC4::smt namespace */
// The CNF conversion can go on in PropEngine.
class CVC4_PUBLIC SmtEngine {
-private:
- /** A name/type pair, used for signatures */
- typedef std::pair<std::string, Type> TypedArg;
- /** A vector of typed formals, and a return type */
- typedef std::pair<std::vector<TypedArg>, Type> FunctionSignature;
/** The type of our internal map of defined functions */
- typedef context::CDMap<std::string, std::pair<FunctionSignature, Expr>,
- StringHashFunction>
- FunctionMap;
-
+ typedef context::CDMap<Node, smt::DefinedFunction, NodeHashFunction>
+ DefinedFunctionMap;
/** The type of our internal assertion list */
typedef context::CDList<Expr> AssertionList;
/** The propositional engine */
prop::PropEngine* d_propEngine;
/** An index of our defined functions */
- FunctionMap* d_functions;
+ DefinedFunctionMap* d_definedFunctions;
/**
* The assertion list (before any conversion) for supporting
* getAssertions(). Only maintained if in interactive mode.
*/
~SmtEngine();
- /**
- * Execute a command.
- */
- void doCommand(Command*);
-
/**
* Set information about the script executing.
*/
- void setInfo(const std::string& key, const SExpr& value) throw(BadOption);
+ void setInfo(const std::string& key, const SExpr& value)
+ throw(BadOptionException);
/**
* Query information about the SMT environment.
*/
- const SExpr& getInfo(const std::string& key) const throw(BadOption);
+ const SExpr& getInfo(const std::string& key) const
+ throw(BadOptionException);
/**
* Set an aspect of the current SMT execution environment.
*/
- void setOption(const std::string& key, const SExpr& value) throw(BadOption);
+ void setOption(const std::string& key, const SExpr& value)
+ throw(BadOptionException);
/**
* Get an aspect of the current SMT execution environment.
*/
- const SExpr& getOption(const std::string& key) const throw(BadOption);
+ const SExpr& getOption(const std::string& key) const
+ throw(BadOptionException);
/**
* Add a formula to the current context: preprocess, do per-theory
* literals and conjunction of literals. Returns false iff
* inconsistent.
*/
- void defineFunction(const std::string& name,
- const std::vector<std::pair<std::string, Type> >& args,
- Type type,
+ void defineFunction(Expr func,
+ const std::vector<Expr>& formals,
Expr formula);
/**
/**
* Get the assigned value of a term (only if preceded by a SAT or
- * INVALID query).
+ * INVALID query). Only permitted if the SmtEngine is set to
+ * operate interactively.
*/
- Expr getValue(Expr term);
+ Expr getValue(Expr term) throw(NoninteractiveException, AssertionException);
/**
- * Get the current set of assertions.
+ * Get the current set of assertions. Only permitted if the
+ * SmtEngine is set to operate interactively.
*/
std::vector<Expr> getAssertions() throw(NoninteractiveException);
/** Should we strictly enforce the language standard while parsing? */
bool strictParsing;
+ /** Should we expand function definitions lazily? */
+ bool lazyDefinitionExpansion;
+
/** Whether we're in interactive mode or not */
bool interactive;
semanticChecks(true),
memoryMap(false),
strictParsing(false),
+ lazyDefinitionExpansion(false),
interactive(false),
interactiveSetByUser(false) {
}
ite4.smt2 \
simple-lra.smt2 \
simple-rdl.smt2 \
+ simple-rdl-definefun.smt2 \
simple-uf.smt2
# Regression tests for PL inputs
--- /dev/null
+(set-logic QF_RDL)
+(set-info :status unsat)
+(declare-fun x () Real)
+(declare-fun y () Real)
+(declare-sort U 0)
+(declare-sort A 2)
+(define-sort F (x) (A Real Real))
+(declare-fun x2 () (F Real))
+(define-fun minus ((x Real) (z Real)) Real (- x z))
+(define-fun less ((x Real) (z Real)) Bool (< x z))
+(define-fun foo ((x Real) (z Real)) Bool (less x z))
+(assert (not (=> (foo (minus x y) 0) (less x y))))
+(check-sat)
+(exit)
projects / cvc5.git / commitdiff