diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-06-06 01:24:17 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-06 01:24:17 -0700 |
commit | fd60da4a22f02f6f5b82cef3585240c1b33595e9 (patch) | |
tree | 137d45e65f204c2f604fed65d47a7d7b4f716c78 /src/api | |
parent | 6a61c1a75b08867c7c06623b8c03084056b6bed7 (diff) |
Keep definitions when global-declarations enabled (#4572)
Fixes #4552. Fixes #4555. The SMT-LIB standard mandates that definitions
are kept when `:global-declarations` are enabled. Until now, CVC4 was
keeping track of the symbols of a definition correctly but lost the body
of the definition when the user context was popped. This commit fixes
the issue by adding a `global` parameter to
`SmtEngine::defineFunction()` and `SmtEngine::defineFunctionRec()`. If
that parameter is set, the definitions of functions are added at level 0
to `d_definedFunctions` and the lemmas for recursive function
definitions are kept in an additional list and asserted during each
`checkSat` call. The commit also updates new API, the commands, and the
parsers to reflect this change.
Diffstat (limited to 'src/api')
-rw-r--r-- | src/api/cvc4cpp.cpp | 26 | ||||
-rw-r--r-- | src/api/cvc4cpp.h | 25 | ||||
-rw-r--r-- | src/api/python/cvc4.pxd | 10 | ||||
-rw-r--r-- | src/api/python/cvc4.pxi | 24 |
4 files changed, 55 insertions, 30 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; } diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index adf3691ab..aa51a4134 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -2860,12 +2860,15 @@ class CVC4_PUBLIC Solver * @param bound_vars the parameters to this function * @param sort the sort of the return value of this function * @param term the function body + * @param global determines whether this definition is global (i.e. persists + * when popping the context) * @return the function */ Term defineFun(const std::string& symbol, const std::vector<Term>& bound_vars, Sort sort, - Term term) const; + Term term, + bool global = false) const; /** * Define n-ary function. * SMT-LIB: ( define-fun <function_def> ) @@ -2873,11 +2876,14 @@ class CVC4_PUBLIC Solver * @param fun the sorted function * @param bound_vars the parameters to this function * @param term the function body + * @param global determines whether this definition is global (i.e. persists + * when popping the context) * @return the function */ Term defineFun(Term fun, const std::vector<Term>& bound_vars, - Term term) const; + Term term, + bool global = false) const; /** * Define recursive function. @@ -2886,12 +2892,15 @@ class CVC4_PUBLIC Solver * @param bound_vars the parameters to this function * @param sort the sort of the return value of this function * @param term the function body + * @param global determines whether this definition is global (i.e. persists + * when popping the context) * @return the function */ Term defineFunRec(const std::string& symbol, const std::vector<Term>& bound_vars, Sort sort, - Term term) const; + Term term, + bool global = false) const; /** * Define recursive function. @@ -2900,11 +2909,14 @@ class CVC4_PUBLIC Solver * @param fun the sorted function * @param bound_vars the parameters to this function * @param term the function body + * @param global determines whether this definition is global (i.e. persists + * when popping the context) * @return the function */ Term defineFunRec(Term fun, const std::vector<Term>& bound_vars, - Term term) const; + Term term, + bool global = false) const; /** * Define recursive functions. @@ -2913,11 +2925,14 @@ class CVC4_PUBLIC Solver * @param funs the sorted functions * @param bound_vars the list of parameters to the functions * @param term the list of function bodies of the functions + * @param global determines whether this definition is global (i.e. persists + * when popping the context) * @return the function */ void 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 = false) const; /** * Echo a given string to the given output stream. diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd index cc998306d..624b3c365 100644 --- a/src/api/python/cvc4.pxd +++ b/src/api/python/cvc4.pxd @@ -181,14 +181,14 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": Term declareFun(const string& symbol, const vector[Sort]& sorts, Sort sort) except + Sort declareSort(const string& symbol, uint32_t arity) except + Term defineFun(const string& symbol, const vector[Term]& bound_vars, - Sort sort, Term term) except + - Term defineFun(Term fun, const vector[Term]& bound_vars, Term term) except + + Sort sort, Term term, bint glbl) except + + Term defineFun(Term fun, const vector[Term]& bound_vars, Term term, bint glbl) except + Term defineFunRec(const string& symbol, const vector[Term]& bound_vars, - Sort sort, Term term) except + + Sort sort, Term term, bint glbl) except + Term defineFunRec(Term fun, const vector[Term]& bound_vars, - Term term) except + + Term term, bint glbl) except + Term defineFunsRec(vector[Term]& funs, vector[vector[Term]]& bound_vars, - vector[Term]& terms) except + + vector[Term]& terms, bint glbl) except + vector[Term] getAssertions() except + vector[pair[Term, Term]] getAssignment() except + string getInfo(const string& flag) except + diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi index 9dd9c1cde..b7593f6f1 100644 --- a/src/api/python/cvc4.pxi +++ b/src/api/python/cvc4.pxi @@ -797,13 +797,13 @@ cdef class Solver: sort.csort = self.csolver.declareSort(symbol.encode(), arity) return sort - def defineFun(self, sym_or_fun, bound_vars, sort_or_term, t=None): + def defineFun(self, sym_or_fun, bound_vars, sort_or_term, t=None, glbl=False): ''' Supports two uses: Term defineFun(str symbol, List[Term] bound_vars, - Sort sort, Term term) + Sort sort, Term term, bool glbl) Term defineFun(Term fun, List[Term] bound_vars, - Term term) + Term term, bool glbl) ''' cdef Term term = Term() cdef vector[c_Term] v @@ -814,21 +814,23 @@ cdef class Solver: term.cterm = self.csolver.defineFun((<str?> sym_or_fun).encode(), <const vector[c_Term] &> v, (<Sort?> sort_or_term).csort, - (<Term?> t).cterm) + (<Term?> t).cterm, + <bint> glbl) else: term.cterm = self.csolver.defineFun((<Term?> sym_or_fun).cterm, <const vector[c_Term]&> v, - (<Term?> sort_or_term).cterm) + (<Term?> sort_or_term).cterm, + <bint> glbl) return term - def defineFunRec(self, sym_or_fun, bound_vars, sort_or_term, t=None): + def defineFunRec(self, sym_or_fun, bound_vars, sort_or_term, t=None, glbl=False): ''' Supports two uses: Term defineFunRec(str symbol, List[Term] bound_vars, - Sort sort, Term term) + Sort sort, Term term, bool glbl) Term defineFunRec(Term fun, List[Term] bound_vars, - Term term) + Term term, bool glbl) ''' cdef Term term = Term() cdef vector[c_Term] v @@ -839,11 +841,13 @@ cdef class Solver: term.cterm = self.csolver.defineFunRec((<str?> sym_or_fun).encode(), <const vector[c_Term] &> v, (<Sort?> sort_or_term).csort, - (<Term?> t).cterm) + (<Term?> t).cterm, + <bint> glbl) else: term.cterm = self.csolver.defineFunRec((<Term?> sym_or_fun).cterm, <const vector[c_Term]&> v, - (<Term?> sort_or_term).cterm) + (<Term?> sort_or_term).cterm, + <bint> glbl) return term |