diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-07-26 09:00:18 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-07-26 09:00:18 -0700 |
commit | c7be9ef42f06a721ba87ad2b0f0e4e3b66d45e06 (patch) | |
tree | acbaa3ba9e4d28d79c83d96331b1c3eff75c72cf /src/api | |
parent | 12f062a502e25978700cca0d1abb09a8ba81e543 (diff) |
New C++ API: Second batch of commands (SMT-LIB). (#2201)
Diffstat (limited to 'src/api')
-rw-r--r-- | src/api/cvc4cpp.cpp | 223 |
1 files changed, 223 insertions, 0 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index dbaac4f8c..eefa8f7e1 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -2353,5 +2353,228 @@ Sort Solver::declareDatatype( return mkDatatypeSort(dtdecl); } +/** + * ( declare-fun <symbol> () <sort> ) + */ +Term Solver::declareFun(const std::string& symbol, Sort sort) const +{ + // CHECK: sort exists + // CHECK: + // sort.isFirstClass() + // else "can not create function type for range type that is not first class" + // CHECK: + // !sort.isFunction() + // else "must flatten function types" + Type type = *sort.d_type; + // CHECK: + // !t.isFunction() || THEORY_UF not enabled + // else "Functions (of non-zero arity) cannot be declared in logic" + return d_exprMgr->mkVar(symbol, type); +} + +/** + * ( declare-fun <symbol> ( <sort>* ) <sort> ) + */ +Term Solver::declareFun(const std::string& symbol, + const std::vector<Sort>& sorts, + Sort sort) const +{ + // CHECK: for all s in sorts, s exists + // CHECK: sort exists + // CHECK: + // for (unsigned i = 0; i < sorts.size(); ++ i) + // sorts[i].isFirstClass() + // else "can not create function type for argument type that is not + // first class" + // CHECK: + // sort.isFirstClass() + // else "can not create function type for range type that is not first class" + // CHECK: + // !sort.isFunction() + // else "must flatten function types" + Type type = *sort.d_type; + if (!sorts.empty()) + { + std::vector<Type> types = sortVectorToTypes(sorts); + type = d_exprMgr->mkFunctionType(types, type); + } + // CHECK: + // !t.isFunction() || THEORY_UF not enabled + // else "Functions (of non-zero arity) cannot be declared in logic" + return d_exprMgr->mkVar(symbol, type); +} + +/** + * ( declare-sort <symbol> <numeral> ) + */ +Sort Solver::declareSort(const std::string& symbol, uint32_t arity) const +{ + // CHECK: + // - logic set? + // - !THEORY_UF && !THEORY_ARRAYS && !THEORY_DATATYPES && !THEORY_SETS + // else "Free sort symbols not allowed in logic" + if (arity == 0) return d_exprMgr->mkSort(symbol); + return d_exprMgr->mkSortConstructor(symbol, arity); +} + +/** + * ( define-fun <function_def> ) + */ +Term Solver::defineFun(const std::string& symbol, + const std::vector<Term>& bound_vars, + Sort sort, + Term term) const +{ + // CHECK: + // for bv in bound_vars: + // NodeManager::fromExprManager(d_exprMgr) + // == NodeManager::fromExprManager(bv.getExprManager()) + // NodeManager::fromExprManager(d_exprMgr) + // == NodeManager::fromExprManager(expr.getExprManager()) + // CHECK: sort exists + // CHECK: not recursive + // CHECK: + // sort.isFirstClass() + // else "can not create function type for range type that is not first class" + // !sort.isFunction() + // else "must flatten function types" + // CHECK: + // for v in bound_vars: is bound var + std::vector<Type> types; + for (const Term& v : bound_vars) + { + types.push_back(v.d_expr->getType()); + } + // CHECK: + // for (unsigned i = 0; i < types.size(); ++ i) + // sorts[i].isFirstClass() + // else "can not create function type for argument type that is not + // first class" + Type type = *sort.d_type; + if (!types.empty()) + { + type = d_exprMgr->mkFunctionType(types, type); + } + Expr fun = d_exprMgr->mkVar(symbol, type); + std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars); + d_smtEngine->defineFunction(fun, ebound_vars, *term.d_expr); + return fun; +} + +Term Solver::defineFun(Term fun, + const std::vector<Term>& bound_vars, + Term term) const +{ + // CHECK: + // NodeManager::fromExprManager(d_exprMgr) + // == NodeManager::fromExprManager(bv.getExprManager()) + // NodeManager::fromExprManager(d_exprMgr) + // == NodeManager::fromExprManager(expr.getExprManager()) + // CHECK: + // - bound_vars matches sort of fun + // - expr matches sort of fun + // CHECK: not recursive + // CHECK: + // for v in bound_vars: is bound var + std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars); + d_smtEngine->defineFunction(*fun.d_expr, ebound_vars, *term.d_expr); + return fun; +} + +/** + * ( define-fun-rec <function_def> ) + */ +Term Solver::defineFunRec(const std::string& symbol, + const std::vector<Term>& bound_vars, + Sort sort, + Term term) const +{ + // CHECK: + // for bv in bound_vars: + // NodeManager::fromExprManager(d_exprMgr) + // == NodeManager::fromExprManager(bv.getExprManager()) + // NodeManager::fromExprManager(d_exprMgr) + // == NodeManager::fromExprManager(expr.getExprManager()) + // CHECK: sort exists + // CHECK: + // sort.isFirstClass() + // else "can not create function type for range type that is not first class" + // !sort.isFunction() + // else "must flatten function types" + // CHECK: + // for v in bound_vars: is bound var + std::vector<Type> types; + for (const Term& v : bound_vars) + { + types.push_back(v.d_expr->getType()); + } + // CHECK: + // for (unsigned i = 0; i < types.size(); ++ i) + // sorts[i].isFirstClass() + // else "can not create function type for argument type that is not + // first class" + Type type = *sort.d_type; + if (!types.empty()) + { + type = d_exprMgr->mkFunctionType(types, type); + } + Expr fun = d_exprMgr->mkVar(symbol, type); + std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars); + d_smtEngine->defineFunctionRec(fun, ebound_vars, *term.d_expr); + return fun; +} + +Term Solver::defineFunRec(Term fun, + const std::vector<Term>& bound_vars, + Term term) const +{ + // CHECK: + // for bv in bound_vars: + // NodeManager::fromExprManager(d_exprMgr) + // == NodeManager::fromExprManager(bv.getExprManager()) + // NodeManager::fromExprManager(d_exprMgr) + // == NodeManager::fromExprManager(expr.getExprManager()) + // CHECK: + // - bound_vars matches sort of fun + // - expr matches sort of fun + // CHECK: + // for v in bound_vars: is bound var + std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars); + d_smtEngine->defineFunctionRec(*fun.d_expr, ebound_vars, *term.d_expr); + return fun; +} + +/** + * ( define-funs-rec ( <function_decl>^{n+1} ) ( <term>^{n+1} ) ) + */ +void Solver::defineFunsRec(const std::vector<Term>& funs, + const std::vector<std::vector<Term>>& bound_vars, + const std::vector<Term>& terms) const +{ + // CHECK: + // for f in funs: + // NodeManager::fromExprManager(d_exprMgr) + // == NodeManager::fromExprManager(f.getExprManager()) + // for bv in bound_vars: + // NodeManager::fromExprManager(d_exprMgr) + // == NodeManager::fromExprManager(bv.getExprManager()) + // NodeManager::fromExprManager(d_exprMgr) + // == NodeManager::fromExprManager(expr.getExprManager()) + // CHECK: + // - bound_vars matches sort of funs + // - exprs matches sort of funs + // CHECK: + // CHECK: + // for bv in bound_vars (for v in bv): is bound var + std::vector<Expr> efuns = termVectorToExprs(funs); + std::vector<std::vector<Expr>> ebound_vars; + for (const auto& v : bound_vars) + { + ebound_vars.push_back(termVectorToExprs(v)); + } + std::vector<Expr> exprs = termVectorToExprs(terms); + d_smtEngine->defineFunctionsRec(efuns, ebound_vars, exprs); +} + } // namespace api } // namespace CVC4 |