diff options
Diffstat (limited to 'src/api/cvc4cpp.cpp')
| -rw-r--r-- | src/api/cvc4cpp.cpp | 26 |
1 files changed, 16 insertions, 10 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 2c65f1ca6..88974dc69 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -4219,7 +4219,8 @@ Sort Solver::declareSort(const std::string& symbol, uint32_t arity) const Term Solver::defineFun(const std::string& symbol, const std::vector<Term>& bound_vars, Sort sort, - Term term) const + Term term, + bool global) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(sort.isFirstClass(), sort) @@ -4253,14 +4254,15 @@ Term Solver::defineFun(const std::string& symbol, } Expr fun = d_exprMgr->mkVar(symbol, type); std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars); - d_smtEngine->defineFunction(fun, ebound_vars, *term.d_expr); + d_smtEngine->defineFunction(fun, ebound_vars, *term.d_expr, global); return Term(this, fun); CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::defineFun(Term fun, const std::vector<Term>& bound_vars, - Term term) const + Term term, + bool global) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(fun.getSort().isFunction(), fun) << "function"; @@ -4293,7 +4295,7 @@ Term Solver::defineFun(Term fun, << codomain << "'"; std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars); - d_smtEngine->defineFunction(*fun.d_expr, ebound_vars, *term.d_expr); + d_smtEngine->defineFunction(*fun.d_expr, ebound_vars, *term.d_expr, global); return fun; CVC4_API_SOLVER_TRY_CATCH_END; } @@ -4304,7 +4306,8 @@ Term Solver::defineFun(Term fun, Term Solver::defineFunRec(const std::string& symbol, const std::vector<Term>& bound_vars, Sort sort, - Term term) const + Term term, + bool global) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(sort.isFirstClass(), sort) @@ -4340,14 +4343,15 @@ Term Solver::defineFunRec(const std::string& symbol, } Expr fun = d_exprMgr->mkVar(symbol, type); std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars); - d_smtEngine->defineFunctionRec(fun, ebound_vars, *term.d_expr); + d_smtEngine->defineFunctionRec(fun, ebound_vars, *term.d_expr, global); return Term(this, fun); CVC4_API_SOLVER_TRY_CATCH_END; } Term Solver::defineFunRec(Term fun, const std::vector<Term>& bound_vars, - Term term) const + Term term, + bool global) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4_API_ARG_CHECK_EXPECTED(fun.getSort().isFunction(), fun) << "function"; @@ -4379,7 +4383,8 @@ Term Solver::defineFunRec(Term fun, << "Invalid sort of function body '" << term << "', expected '" << codomain << "'"; std::vector<Expr> ebound_vars = termVectorToExprs(bound_vars); - d_smtEngine->defineFunctionRec(*fun.d_expr, ebound_vars, *term.d_expr); + d_smtEngine->defineFunctionRec( + *fun.d_expr, ebound_vars, *term.d_expr, global); return fun; CVC4_API_SOLVER_TRY_CATCH_END; } @@ -4389,7 +4394,8 @@ Term Solver::defineFunRec(Term fun, */ void Solver::defineFunsRec(const std::vector<Term>& funs, const std::vector<std::vector<Term>>& bound_vars, - const std::vector<Term>& terms) const + const std::vector<Term>& terms, + bool global) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; size_t funs_size = funs.size(); @@ -4444,7 +4450,7 @@ void Solver::defineFunsRec(const std::vector<Term>& funs, ebound_vars.push_back(termVectorToExprs(v)); } std::vector<Expr> exprs = termVectorToExprs(terms); - d_smtEngine->defineFunctionsRec(efuns, ebound_vars, exprs); + d_smtEngine->defineFunctionsRec(efuns, ebound_vars, exprs, global); CVC4_API_SOLVER_TRY_CATCH_END; } |