summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--NEWS3
-rw-r--r--examples/api/python/sygus-inv.py6
-rw-r--r--src/api/cpp/cvc5.cpp33
-rw-r--r--src/api/cpp/cvc5.h18
-rw-r--r--src/api/cpp/cvc5_checks.h2
-rw-r--r--src/api/java/io/github/cvc5/api/Solver.java41
-rw-r--r--src/api/java/jni/solver.cpp25
-rw-r--r--src/api/python/cvc5.pxd1
-rw-r--r--src/api/python/cvc5.pxi33
-rw-r--r--src/main/command_executor.cpp6
-rw-r--r--src/parser/smt2/Smt2.g67
-rw-r--r--src/smt/command.cpp62
-rw-r--r--src/smt/command.h32
-rw-r--r--test/python/unit/api/test_solver.py31
-rw-r--r--test/regress/regress0/push-pop/inc-define.smt22
-rw-r--r--test/regress/regress0/smtlib/issue4552.smt24
-rw-r--r--test/unit/api/java/SolverTest.java27
-rw-r--r--test/unit/api/solver_black.cpp30
18 files changed, 86 insertions, 337 deletions
diff --git a/NEWS b/NEWS
index f01643643..c9716b33f 100644
--- a/NEWS
+++ b/NEWS
@@ -31,7 +31,8 @@ Improvements:
Changes:
* SyGuS: Removed support for SyGuS-IF 1.0.
-* Removed Java and Python bindings for the legacy API
+* Removed support for the (non-standard) `define` command.
+* Removed Java and Python bindings for the legacy API.
* Interactive shell: the GPL-licensed Readline library has been replaced the
BSD-licensed Editline. Compiling with `--best` now enables Editline, instead
of Readline. Without selecting optional GPL components, Editline-enabled CVC4
diff --git a/examples/api/python/sygus-inv.py b/examples/api/python/sygus-inv.py
index 8273aa298..50fa3f04f 100644
--- a/examples/api/python/sygus-inv.py
+++ b/examples/api/python/sygus-inv.py
@@ -48,9 +48,9 @@ if __name__ == "__main__":
slv.mkTerm(kinds.Equal, xp, x))
# define the pre-conditions, transition relations, and post-conditions
- pre_f = slv.defineFun("pre-f", {x}, boolean, slv.mkTerm(kinds.Equal, x, zero))
- trans_f = slv.defineFun("trans-f", {x, xp}, boolean, ite)
- post_f = slv.defineFun("post-f", {x}, boolean, slv.mkTerm(kinds.Leq, x, ten))
+ pre_f = slv.defineFun("pre-f", [x], boolean, slv.mkTerm(kinds.Equal, x, zero))
+ trans_f = slv.defineFun("trans-f", [x, xp], boolean, ite)
+ post_f = slv.defineFun("post-f", [x], boolean, slv.mkTerm(kinds.Leq, x, ten))
# declare the invariant-to-synthesize
inv_f = slv.synthInv("inv-f", {x})
diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index a342cea53..addfeb0da 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -6716,7 +6716,7 @@ Term Solver::defineFun(const std::string& symbol,
CVC5_API_TRY_CATCH_BEGIN;
CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(sort);
CVC5_API_SOLVER_CHECK_TERM(term);
- CVC5_API_CHECK(sort == term.getSort())
+ CVC5_API_CHECK(term.getSort().isSubsortOf(sort))
<< "Invalid sort of function body '" << term << "', expected '" << sort
<< "'";
@@ -6743,37 +6743,6 @@ Term Solver::defineFun(const std::string& symbol,
CVC5_API_TRY_CATCH_END;
}
-Term Solver::defineFun(const Term& fun,
- const std::vector<Term>& bound_vars,
- const Term& term,
- bool global) const
-{
- CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_SOLVER_CHECK_TERM(fun);
- CVC5_API_SOLVER_CHECK_TERM(term);
- if (fun.getSort().isFunction())
- {
- std::vector<Sort> domain_sorts = fun.getSort().getFunctionDomainSorts();
- CVC5_API_SOLVER_CHECK_BOUND_VARS_DEF_FUN(fun, bound_vars, domain_sorts);
- Sort codomain = fun.getSort().getFunctionCodomainSort();
- CVC5_API_CHECK(codomain == term.getSort())
- << "Invalid sort of function body '" << term << "', expected '"
- << codomain << "'";
- }
- else
- {
- CVC5_API_SOLVER_CHECK_BOUND_VARS(bound_vars);
- CVC5_API_ARG_CHECK_EXPECTED(bound_vars.size() == 0, fun)
- << "function or nullary symbol";
- }
- //////// all checks before this line
- std::vector<Node> ebound_vars = Term::termVectorToNodes(bound_vars);
- d_slv->defineFunction(*fun.d_node, ebound_vars, *term.d_node, global);
- return fun;
- ////////
- CVC5_API_TRY_CATCH_END;
-}
-
Term Solver::defineFunRec(const std::string& symbol,
const std::vector<Term>& bound_vars,
const Sort& sort,
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index f0a36b792..63dadaef6 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -3813,24 +3813,6 @@ class CVC5_EXPORT Solver
const Sort& sort,
const Term& term,
bool global = false) const;
- /**
- * Define n-ary function.
- * SMT-LIB:
- * \verbatim
- * ( define-fun <function_def> )
- * \endverbatim
- * Create parameter 'fun' with mkConst().
- * @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(const Term& fun,
- const std::vector<Term>& bound_vars,
- const Term& term,
- bool global = false) const;
/**
* Define recursive function.
diff --git a/src/api/cpp/cvc5_checks.h b/src/api/cpp/cvc5_checks.h
index c30237ecd..35c21df9c 100644
--- a/src/api/cpp/cvc5_checks.h
+++ b/src/api/cpp/cvc5_checks.h
@@ -438,8 +438,6 @@ namespace api {
CVC5_API_ARG_CHECK_NOT_NULL(sort); \
CVC5_API_CHECK(this == sort.d_solver) \
<< "Given sort is not associated with this solver"; \
- CVC5_API_ARG_CHECK_EXPECTED(sort.isFirstClass(), sort) \
- << "first-class sort as codomain sort"; \
CVC5_API_ARG_CHECK_EXPECTED(!sort.isFunction(), sort) \
<< "function sort as codomain sort"; \
} while (0)
diff --git a/src/api/java/io/github/cvc5/api/Solver.java b/src/api/java/io/github/cvc5/api/Solver.java
index 3a9f450a4..c57ba48b8 100644
--- a/src/api/java/io/github/cvc5/api/Solver.java
+++ b/src/api/java/io/github/cvc5/api/Solver.java
@@ -1594,47 +1594,6 @@ public class Solver implements IPointer
boolean global);
/**
- * Define n-ary function in the current context.
- * SMT-LIB:
- * {@code
- * ( define-fun <function_def> )
- * }
- * Create parameter 'fun' with mkConst().
- * @param fun the sorted function
- * @param boundVars the parameters to this function
- * @param term the function body
- * @return the function
- */
- public Term defineFun(Term fun, Term[] boundVars, Term term)
- {
- return defineFun(fun, boundVars, term, false);
- }
- /**
- * Define n-ary function.
- * SMT-LIB:
- * {@code
- * ( define-fun <function_def> )
- * }
- * Create parameter 'fun' with mkConst().
- * @param fun the sorted function
- * @param boundVars 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
- */
- public Term defineFun(Term fun, Term[] boundVars, Term term, boolean global)
- {
- long[] boundVarPointers = Utils.getPointers(boundVars);
- long termPointer =
- defineFun(pointer, fun.getPointer(), boundVarPointers, term.getPointer(), global);
- return new Term(this, termPointer);
- }
-
- private native long defineFun(
- long pointer, long funPointer, long[] boundVarPointers, long termPointer, boolean global);
-
- /**
* Define recursive function in the current context.
* SMT-LIB:
* {@code
diff --git a/src/api/java/jni/solver.cpp b/src/api/java/jni/solver.cpp
index af3d7e59e..bc4d7ff43 100644
--- a/src/api/java/jni/solver.cpp
+++ b/src/api/java/jni/solver.cpp
@@ -1705,31 +1705,6 @@ Java_io_github_cvc5_api_Solver_defineFun__JLjava_lang_String_2_3JJJZ(
/*
* Class: io_github_cvc5_api_Solver
- * Method: defineFun
- * Signature: (JJ[JJZ)J
- */
-JNIEXPORT jlong JNICALL
-Java_io_github_cvc5_api_Solver_defineFun__JJ_3JJZ(JNIEnv* env,
- jobject,
- jlong pointer,
- jlong funPointer,
- jlongArray jVars,
- jlong termPointer,
- jboolean global)
-{
- CVC5_JAVA_API_TRY_CATCH_BEGIN;
- Solver* solver = reinterpret_cast<Solver*>(pointer);
- Term* fun = reinterpret_cast<Term*>(funPointer);
- Term* term = reinterpret_cast<Term*>(termPointer);
- std::vector<Term> vars = getObjectsFromPointers<Term>(env, jVars);
- Term* retPointer =
- new Term(solver->defineFun(*fun, vars, *term, (bool)global));
- return reinterpret_cast<jlong>(retPointer);
- CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
-}
-
-/*
- * Class: io_github_cvc5_api_Solver
* Method: defineFunRec
* Signature: (JLjava/lang/String;[JJJZ)J
*/
diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index 42aee08b0..9504bccae 100644
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -266,7 +266,6 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
Sort declareSort(const string& symbol, uint32_t arity) except +
Term defineFun(const string& symbol, const vector[Term]& bound_vars,
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, bint glbl) except +
Term defineFunRec(Term fun, const vector[Term]& bound_vars,
diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 3367bf47b..6f50b8401 100644
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -1811,14 +1811,8 @@ 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, glbl=False):
- """
- Define n-ary function.
- Supports two uses:
-
- - ``Term defineFun(str symbol, List[Term] bound_vars, Sort sort, Term term, bool glbl)``
- - ``Term defineFun(Term fun, List[Term] bound_vars, Term term, bool glbl)``
-
+ def defineFun(self, str symbol, list bound_vars, Sort sort, Term term, glbl=False):
+ """Define n-ary function.
SMT-LIB:
@@ -1830,27 +1824,20 @@ cdef class 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)
+ :param glbl: determines whether this definition is global (i.e. persists when popping the context)
:return: the function
"""
- cdef Term term = Term(self)
+ cdef Term fun = Term(self)
cdef vector[c_Term] v
for bv in bound_vars:
v.push_back((<Term?> bv).cterm)
- if t is not None:
- term.cterm = self.csolver.defineFun((<str?> sym_or_fun).encode(),
- <const vector[c_Term] &> v,
- (<Sort?> sort_or_term).csort,
- (<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,
- <bint> glbl)
-
- return term
+ fun.cterm = self.csolver.defineFun(symbol.encode(),
+ <const vector[c_Term] &> v,
+ sort.csort,
+ term.cterm,
+ <bint> glbl)
+ return fun
def defineFunRec(self, sym_or_fun, bound_vars, sort_or_term, t=None, glbl=False):
"""Define recursive functions.
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 8188f247f..f08d9adde 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -204,7 +204,11 @@ bool solverInvoke(api::Solver* solver,
cmd->toStream(ss);
}
- if (solver->getOptionInfo("parse-only").boolValue())
+ // In parse-only mode, we do not invoke any of the commands except define-fun
+ // commands. We invoke define-fun commands because they add function names
+ // to the symbol table.
+ if (solver->getOptionInfo("parse-only").boolValue()
+ && dynamic_cast<DefineFunctionCommand*>(cmd) == nullptr)
{
return true;
}
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 696eb6ad4..bf58e786d 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -314,6 +314,10 @@ command [std::unique_ptr<cvc5::Command>* cmd]
}
t = PARSER_STATE->mkFlatFunctionType(sorts, t, flattenVars);
+ if (t.isFunction())
+ {
+ t = t.getFunctionCodomainSort();
+ }
if (sortedVarNames.size() > 0)
{
PARSER_STATE->pushScope();
@@ -332,13 +336,7 @@ command [std::unique_ptr<cvc5::Command>* cmd]
{
PARSER_STATE->popScope();
}
- // declare the name down here (while parsing term, signature
- // must not be extended with the name itself; no recursion
- // permitted)
- // we allow overloading for function definitions
- api::Term func = PARSER_STATE->bindVar(name, t, false, true);
- cmd->reset(new DefineFunctionCommand(
- name, func, terms, expr, SYM_MAN->getGlobalDeclarations()));
+ cmd->reset(new DefineFunctionCommand(name, terms, t, expr));
}
| DECLARE_DATATYPE_TOK datatypeDefCommand[false, cmd]
| DECLARE_DATATYPES_TOK datatypesDefCommand[false, cmd]
@@ -834,8 +832,7 @@ smt25Command[std::unique_ptr<cvc5::Command>* cmd]
if( !flattenVars.empty() ){
expr = PARSER_STATE->mkHoApply( expr, flattenVars );
}
- cmd->reset(new DefineFunctionRecCommand(
- func, bvs, expr, SYM_MAN->getGlobalDeclarations()));
+ cmd->reset(new DefineFunctionRecCommand(func, bvs, expr));
}
| DEFINE_FUNS_REC_TOK
{ PARSER_STATE->checkThatLogicIsSet();}
@@ -898,8 +895,7 @@ smt25Command[std::unique_ptr<cvc5::Command>* cmd]
"Number of functions defined does not match number listed in "
"define-funs-rec"));
}
- cmd->reset(new DefineFunctionRecCommand(
- funcs, formals, func_defs, SYM_MAN->getGlobalDeclarations()));
+ cmd->reset(new DefineFunctionRecCommand(funcs, formals, func_defs));
}
;
@@ -984,48 +980,6 @@ extendedCommand[std::unique_ptr<cvc5::Command>* cmd]
)+
RPAREN_TOK
{ cmd->reset(seq.release()); }
-
- | DEFINE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
- ( // (define f t)
- symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
- { PARSER_STATE->checkUserSymbol(name); }
- term[e,e2]
- {
- api::Term func = PARSER_STATE->bindVar(name, e.getSort());
- cmd->reset(new DefineFunctionCommand(
- name, func, e, SYM_MAN->getGlobalDeclarations()));
- }
- | // (define (f (v U) ...) t)
- LPAREN_TOK
- symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
- { PARSER_STATE->checkUserSymbol(name); }
- sortedVarList[sortedVarNames] RPAREN_TOK
- { /* add variables to parser state before parsing term */
- Debug("parser") << "define fun: '" << name << "'" << std::endl;
- PARSER_STATE->pushScope();
- terms = PARSER_STATE->bindBoundVars(sortedVarNames);
- }
- term[e,e2]
- {
- PARSER_STATE->popScope();
- // declare the name down here (while parsing term, signature
- // must not be extended with the name itself; no recursion
- // permitted)
- api::Sort tt = e.getSort();
- if( sortedVarNames.size() > 0 ) {
- sorts.reserve(sortedVarNames.size());
- for(std::vector<std::pair<std::string, api::Sort> >::const_iterator
- i = sortedVarNames.begin(), iend = sortedVarNames.end();
- i != iend; ++i) {
- sorts.push_back((*i).second);
- }
- tt = SOLVER->mkFunctionSort(sorts, tt);
- }
- api::Term func = PARSER_STATE->bindVar(name, tt);
- cmd->reset(new DefineFunctionCommand(
- name, func, terms, e, SYM_MAN->getGlobalDeclarations()));
- }
- )
| // (define-const x U t)
DEFINE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); }
symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
@@ -1036,9 +990,7 @@ extendedCommand[std::unique_ptr<cvc5::Command>* cmd]
// declare the name down here (while parsing term, signature
// must not be extended with the name itself; no recursion
// permitted)
- api::Term func = PARSER_STATE->bindVar(name, t);
- cmd->reset(new DefineFunctionCommand(
- name, func, terms, e, SYM_MAN->getGlobalDeclarations()));
+ cmd->reset(new DefineFunctionCommand(name, t, e));
}
| SIMPLIFY_TOK { PARSER_STATE->checkThatLogicIsSet(); }
@@ -1850,6 +1802,8 @@ attribute[cvc5::api::Term& expr, cvc5::api::Term& retExpr]
| ATTRIBUTE_NAMED_TOK symbol[s,CHECK_UNDECLARED,SYM_VARIABLE]
{
// notify that expression was given a name
+ PARSER_STATE->preemptCommand(
+ new DefineFunctionCommand(s, expr.getSort(), expr));
PARSER_STATE->notifyNamedExpression(expr, s);
}
;
@@ -2277,7 +2231,6 @@ ECHO_TOK : 'echo';
DECLARE_SORTS_TOK : 'declare-sorts';
DECLARE_FUNS_TOK : 'declare-funs';
DECLARE_PREDS_TOK : 'declare-preds';
-DEFINE_TOK : 'define';
DECLARE_CONST_TOK : 'declare-const';
DEFINE_CONST_TOK : 'define-const';
SIMPLIFY_TOK : 'simplify';
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index e8ee6d59c..419b925c4 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -1313,46 +1313,44 @@ void DefineSortCommand::toStream(std::ostream& out,
/* -------------------------------------------------------------------------- */
DefineFunctionCommand::DefineFunctionCommand(const std::string& id,
- api::Term func,
- api::Term formula,
- bool global)
+ api::Sort sort,
+ api::Term formula)
: DeclarationDefinitionCommand(id),
- d_func(func),
d_formals(),
- d_formula(formula),
- d_global(global)
+ d_sort(sort),
+ d_formula(formula)
{
}
DefineFunctionCommand::DefineFunctionCommand(
const std::string& id,
- api::Term func,
const std::vector<api::Term>& formals,
- api::Term formula,
- bool global)
+ api::Sort sort,
+ api::Term formula)
: DeclarationDefinitionCommand(id),
- d_func(func),
d_formals(formals),
- d_formula(formula),
- d_global(global)
+ d_sort(sort),
+ d_formula(formula)
{
}
-api::Term DefineFunctionCommand::getFunction() const { return d_func; }
const std::vector<api::Term>& DefineFunctionCommand::getFormals() const
{
return d_formals;
}
+api::Sort DefineFunctionCommand::getSort() const { return d_sort; }
+
api::Term DefineFunctionCommand::getFormula() const { return d_formula; }
+
void DefineFunctionCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
try
{
- if (!d_func.isNull())
- {
- solver->defineFun(d_func, d_formals, d_formula, d_global);
- }
+ bool global = sm->getGlobalDeclarations();
+ api::Term fun =
+ solver->defineFun(d_symbol, d_formals, d_sort, d_formula, global);
+ sm->getSymbolTable()->bind(fun.toString(), fun, global);
d_commandStatus = CommandSuccess::instance();
}
catch (exception& e)
@@ -1363,8 +1361,7 @@ void DefineFunctionCommand::invoke(api::Solver* solver, SymbolManager* sm)
Command* DefineFunctionCommand::clone() const
{
- return new DefineFunctionCommand(
- d_symbol, d_func, d_formals, d_formula, d_global);
+ return new DefineFunctionCommand(d_symbol, d_formals, d_sort, d_formula);
}
std::string DefineFunctionCommand::getCommandName() const
@@ -1377,16 +1374,11 @@ void DefineFunctionCommand::toStream(std::ostream& out,
size_t dag,
Language language) const
{
- TypeNode rangeType = termToNode(d_func).getType();
- if (rangeType.isFunction())
- {
- rangeType = rangeType.getRangeType();
- }
Printer::getPrinter(language)->toStreamCmdDefineFunction(
out,
- d_func.toString(),
+ d_symbol,
termVectorToNodes(d_formals),
- rangeType,
+ sortToTypeNode(d_sort),
termToNode(d_formula));
}
@@ -1395,12 +1387,7 @@ void DefineFunctionCommand::toStream(std::ostream& out,
/* -------------------------------------------------------------------------- */
DefineFunctionRecCommand::DefineFunctionRecCommand(
-
- api::Term func,
- const std::vector<api::Term>& formals,
- api::Term formula,
- bool global)
- : d_global(global)
+ api::Term func, const std::vector<api::Term>& formals, api::Term formula)
{
d_funcs.push_back(func);
d_formals.push_back(formals);
@@ -1408,12 +1395,10 @@ DefineFunctionRecCommand::DefineFunctionRecCommand(
}
DefineFunctionRecCommand::DefineFunctionRecCommand(
-
const std::vector<api::Term>& funcs,
const std::vector<std::vector<api::Term>>& formals,
- const std::vector<api::Term>& formulas,
- bool global)
- : d_funcs(funcs), d_formals(formals), d_formulas(formulas), d_global(global)
+ const std::vector<api::Term>& formulas)
+ : d_funcs(funcs), d_formals(formals), d_formulas(formulas)
{
}
@@ -1437,7 +1422,8 @@ void DefineFunctionRecCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
try
{
- solver->defineFunsRec(d_funcs, d_formals, d_formulas, d_global);
+ bool global = sm->getGlobalDeclarations();
+ solver->defineFunsRec(d_funcs, d_formals, d_formulas, global);
d_commandStatus = CommandSuccess::instance();
}
catch (exception& e)
@@ -1448,7 +1434,7 @@ void DefineFunctionRecCommand::invoke(api::Solver* solver, SymbolManager* sm)
Command* DefineFunctionRecCommand::clone() const
{
- return new DefineFunctionRecCommand(d_funcs, d_formals, d_formulas, d_global);
+ return new DefineFunctionRecCommand(d_funcs, d_formals, d_formulas);
}
std::string DefineFunctionRecCommand::getCommandName() const
diff --git a/src/smt/command.h b/src/smt/command.h
index 400f3492e..5733eb3e5 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -494,17 +494,15 @@ class CVC5_EXPORT DefineFunctionCommand : public DeclarationDefinitionCommand
{
public:
DefineFunctionCommand(const std::string& id,
- api::Term func,
- api::Term formula,
- bool global);
+ api::Sort sort,
+ api::Term formula);
DefineFunctionCommand(const std::string& id,
- api::Term func,
const std::vector<api::Term>& formals,
- api::Term formula,
- bool global);
+ api::Sort sort,
+ api::Term formula);
- api::Term getFunction() const;
const std::vector<api::Term>& getFormals() const;
+ api::Sort getSort() const;
api::Term getFormula() const;
void invoke(api::Solver* solver, SymbolManager* sm) override;
@@ -516,17 +514,12 @@ class CVC5_EXPORT DefineFunctionCommand : public DeclarationDefinitionCommand
Language language = Language::LANG_AUTO) const override;
protected:
- /** The function we are defining */
- api::Term d_func;
/** The formal arguments for the function we are defining */
std::vector<api::Term> d_formals;
+ /** The co-domain sort of the function we are defining */
+ api::Sort d_sort;
/** The formula corresponding to the body of the function we are defining */
api::Term d_formula;
- /**
- * Stores whether this definition is global (i.e. should persist when
- * popping the user context.
- */
- bool d_global;
}; /* class DefineFunctionCommand */
/**
@@ -539,12 +532,10 @@ class CVC5_EXPORT DefineFunctionRecCommand : public Command
public:
DefineFunctionRecCommand(api::Term func,
const std::vector<api::Term>& formals,
- api::Term formula,
- bool global);
+ api::Term formula);
DefineFunctionRecCommand(const std::vector<api::Term>& funcs,
const std::vector<std::vector<api::Term> >& formals,
- const std::vector<api::Term>& formula,
- bool global);
+ const std::vector<api::Term>& formula);
const std::vector<api::Term>& getFunctions() const;
const std::vector<std::vector<api::Term> >& getFormals() const;
@@ -565,11 +556,6 @@ class CVC5_EXPORT DefineFunctionRecCommand : public Command
std::vector<std::vector<api::Term> > d_formals;
/** formulas corresponding to the bodies of the functions we are defining */
std::vector<api::Term> d_formulas;
- /**
- * Stores whether this definition is global (i.e. should persist when
- * popping the user context.
- */
- bool d_global;
}; /* class DefineFunctionRecCommand */
/**
diff --git a/test/python/unit/api/test_solver.py b/test/python/unit/api/test_solver.py
index 04a275741..8e8ed0d9b 100644
--- a/test/python/unit/api/test_solver.py
+++ b/test/python/unit/api/test_solver.py
@@ -950,42 +950,23 @@ def test_declare_sort(solver):
def test_define_fun(solver):
bvSort = solver.mkBitVectorSort(32)
- funSort1 = solver.mkFunctionSort([bvSort, bvSort], bvSort)
- funSort2 = solver.mkFunctionSort(solver.mkUninterpretedSort("u"),\
- solver.getIntegerSort())
+ funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"),
+ solver.getIntegerSort())
b1 = solver.mkVar(bvSort, "b1")
- b11 = solver.mkVar(bvSort, "b1")
b2 = solver.mkVar(solver.getIntegerSort(), "b2")
- b3 = solver.mkVar(funSort2, "b3")
+ b3 = solver.mkVar(funSort, "b3")
v1 = solver.mkConst(bvSort, "v1")
- v2 = solver.mkConst(solver.getIntegerSort(), "v2")
- v3 = solver.mkConst(funSort2, "v3")
- f1 = solver.mkConst(funSort1, "f1")
- f2 = solver.mkConst(funSort2, "f2")
- f3 = solver.mkConst(bvSort, "f3")
+ v2 = solver.mkConst(funSort, "v2")
solver.defineFun("f", [], bvSort, v1)
solver.defineFun("ff", [b1, b2], bvSort, v1)
- solver.defineFun(f1, [b1, b11], v1)
with pytest.raises(RuntimeError):
solver.defineFun("ff", [v1, b2], bvSort, v1)
with pytest.raises(RuntimeError):
- solver.defineFun("fff", [b1], bvSort, v3)
+ solver.defineFun("fff", [b1], bvSort, v2)
with pytest.raises(RuntimeError):
- solver.defineFun("ffff", [b1], funSort2, v3)
+ solver.defineFun("ffff", [b1], funSort, v2)
# b3 has function sort, which is allowed as an argument
solver.defineFun("fffff", [b1, b3], bvSort, v1)
- with pytest.raises(RuntimeError):
- solver.defineFun(f1, [v1, b11], v1)
- with pytest.raises(RuntimeError):
- solver.defineFun(f1, [b1], v1)
- with pytest.raises(RuntimeError):
- solver.defineFun(f1, [b1, b11], v2)
- with pytest.raises(RuntimeError):
- solver.defineFun(f1, [b1, b11], v3)
- with pytest.raises(RuntimeError):
- solver.defineFun(f2, [b1], v2)
- with pytest.raises(RuntimeError):
- solver.defineFun(f3, [b1], v1)
slv = pycvc5.Solver()
bvSort2 = slv.mkBitVectorSort(32)
diff --git a/test/regress/regress0/push-pop/inc-define.smt2 b/test/regress/regress0/push-pop/inc-define.smt2
index 27261eff6..57f4d711c 100644
--- a/test/regress/regress0/push-pop/inc-define.smt2
+++ b/test/regress/regress0/push-pop/inc-define.smt2
@@ -4,6 +4,6 @@
(set-logic QF_LIA)
(declare-fun x () Int)
(check-sat)
-(define t (not (= x 0)))
+(define-const t Bool (not (= x 0)))
(assert t)
(check-sat)
diff --git a/test/regress/regress0/smtlib/issue4552.smt2 b/test/regress/regress0/smtlib/issue4552.smt2
index af8e0b948..8fcfabd5e 100644
--- a/test/regress/regress0/smtlib/issue4552.smt2
+++ b/test/regress/regress0/smtlib/issue4552.smt2
@@ -6,8 +6,8 @@
(set-option :global-declarations true)
(push)
-(define a true)
-(define (f (b Bool)) b)
+(define-const a Bool true)
+(define-fun f ((b Bool)) Bool b)
(define-const a2 Bool true)
(define-fun a3 () Bool true)
diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java
index 1f88add2d..58b8d03aa 100644
--- a/test/unit/api/java/SolverTest.java
+++ b/test/unit/api/java/SolverTest.java
@@ -959,38 +959,25 @@ class SolverTest
@Test void defineFun() throws CVC5ApiException
{
Sort bvSort = d_solver.mkBitVectorSort(32);
- Sort funSort1 = d_solver.mkFunctionSort(new Sort[] {bvSort, bvSort}, bvSort);
- Sort funSort2 =
+ Sort funSort =
d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort());
Term b1 = d_solver.mkVar(bvSort, "b1");
- Term b11 = d_solver.mkVar(bvSort, "b1");
Term b2 = d_solver.mkVar(d_solver.getIntegerSort(), "b2");
- Term b3 = d_solver.mkVar(funSort2, "b3");
+ Term b3 = d_solver.mkVar(funSort, "b3");
Term v1 = d_solver.mkConst(bvSort, "v1");
- Term v2 = d_solver.mkConst(d_solver.getIntegerSort(), "v2");
- Term v3 = d_solver.mkConst(funSort2, "v3");
- Term f1 = d_solver.mkConst(funSort1, "f1");
- Term f2 = d_solver.mkConst(funSort2, "f2");
- Term f3 = d_solver.mkConst(bvSort, "f3");
+ Term v2 = d_solver.mkConst(funSort, "v2");
assertDoesNotThrow(() -> d_solver.defineFun("f", new Term[] {}, bvSort, v1));
assertDoesNotThrow(() -> d_solver.defineFun("ff", new Term[] {b1, b2}, bvSort, v1));
- assertDoesNotThrow(() -> d_solver.defineFun(f1, new Term[] {b1, b11}, v1));
assertThrows(
CVC5ApiException.class, () -> d_solver.defineFun("ff", new Term[] {v1, b2}, bvSort, v1));
assertThrows(
- CVC5ApiException.class, () -> d_solver.defineFun("fff", new Term[] {b1}, bvSort, v3));
+ CVC5ApiException.class, () -> d_solver.defineFun("fff", new Term[] {b1}, bvSort, v2));
assertThrows(
- CVC5ApiException.class, () -> d_solver.defineFun("ffff", new Term[] {b1}, funSort2, v3));
+ CVC5ApiException.class, () -> d_solver.defineFun("ffff", new Term[] {b1}, funSort2, v2));
// b3 has function sort, which is allowed as an argument
assertDoesNotThrow(() -> d_solver.defineFun("fffff", new Term[] {b1, b3}, bvSort, v1));
- assertThrows(CVC5ApiException.class, () -> d_solver.defineFun(f1, new Term[] {v1, b11}, v1));
- assertThrows(CVC5ApiException.class, () -> d_solver.defineFun(f1, new Term[] {b1}, v1));
- assertThrows(CVC5ApiException.class, () -> d_solver.defineFun(f1, new Term[] {b1, b11}, v2));
- assertThrows(CVC5ApiException.class, () -> d_solver.defineFun(f1, new Term[] {b1, b11}, v3));
- assertThrows(CVC5ApiException.class, () -> d_solver.defineFun(f2, new Term[] {b1}, v2));
- assertThrows(CVC5ApiException.class, () -> d_solver.defineFun(f3, new Term[] {b1}, v1));
Solver slv = new Solver();
Sort bvSort2 = slv.mkBitVectorSort(32);
@@ -1012,15 +999,13 @@ class SolverTest
@Test void defineFunGlobal()
{
Sort bSort = d_solver.getBooleanSort();
- Sort fSort = d_solver.mkFunctionSort(bSort, bSort);
Term bTrue = d_solver.mkBoolean(true);
// (define-fun f () Bool true)
Term f = d_solver.defineFun("f", new Term[] {}, bSort, bTrue, true);
Term b = d_solver.mkVar(bSort, "b");
- Term gSym = d_solver.mkConst(fSort, "g");
// (define-fun g (b Bool) Bool b)
- Term g = d_solver.defineFun(gSym, new Term[] {b}, b, true);
+ Term g = d_solver.defineFun("g", new Term[] {b}, bSort, b, true);
// (assert (or (not f) (not (g true))))
d_solver.assertFormula(
diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp
index 8dcb0fde6..8435a63be 100644
--- a/test/unit/api/solver_black.cpp
+++ b/test/unit/api/solver_black.cpp
@@ -922,35 +922,21 @@ TEST_F(TestApiBlackSolver, defineSort)
TEST_F(TestApiBlackSolver, defineFun)
{
Sort bvSort = d_solver.mkBitVectorSort(32);
- Sort funSort1 = d_solver.mkFunctionSort({bvSort, bvSort}, bvSort);
- Sort funSort2 = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
- d_solver.getIntegerSort());
+ Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"),
+ d_solver.getIntegerSort());
Term b1 = d_solver.mkVar(bvSort, "b1");
- Term b11 = d_solver.mkVar(bvSort, "b1");
Term b2 = d_solver.mkVar(d_solver.getIntegerSort(), "b2");
- Term b3 = d_solver.mkVar(funSort2, "b3");
+ Term b3 = d_solver.mkVar(funSort, "b3");
Term v1 = d_solver.mkConst(bvSort, "v1");
- Term v2 = d_solver.mkConst(d_solver.getIntegerSort(), "v2");
- Term v3 = d_solver.mkConst(funSort2, "v3");
- Term f1 = d_solver.mkConst(funSort1, "f1");
- Term f2 = d_solver.mkConst(funSort2, "f2");
- Term f3 = d_solver.mkConst(bvSort, "f3");
+ Term v2 = d_solver.mkConst(funSort, "v2");
ASSERT_NO_THROW(d_solver.defineFun("f", {}, bvSort, v1));
ASSERT_NO_THROW(d_solver.defineFun("ff", {b1, b2}, bvSort, v1));
- ASSERT_NO_THROW(d_solver.defineFun(f1, {b1, b11}, v1));
ASSERT_THROW(d_solver.defineFun("ff", {v1, b2}, bvSort, v1),
CVC5ApiException);
- ASSERT_THROW(d_solver.defineFun("fff", {b1}, bvSort, v3), CVC5ApiException);
- ASSERT_THROW(d_solver.defineFun("ffff", {b1}, funSort2, v3),
- CVC5ApiException);
+ ASSERT_THROW(d_solver.defineFun("fff", {b1}, bvSort, v2), CVC5ApiException);
+ ASSERT_THROW(d_solver.defineFun("ffff", {b1}, funSort, v2), CVC5ApiException);
// b3 has function sort, which is allowed as an argument
ASSERT_NO_THROW(d_solver.defineFun("fffff", {b1, b3}, bvSort, v1));
- ASSERT_THROW(d_solver.defineFun(f1, {v1, b11}, v1), CVC5ApiException);
- ASSERT_THROW(d_solver.defineFun(f1, {b1}, v1), CVC5ApiException);
- ASSERT_THROW(d_solver.defineFun(f1, {b1, b11}, v2), CVC5ApiException);
- ASSERT_THROW(d_solver.defineFun(f1, {b1, b11}, v3), CVC5ApiException);
- ASSERT_THROW(d_solver.defineFun(f2, {b1}, v2), CVC5ApiException);
- ASSERT_THROW(d_solver.defineFun(f3, {b1}, v1), CVC5ApiException);
Solver slv;
Sort bvSort2 = slv.mkBitVectorSort(32);
@@ -968,15 +954,13 @@ TEST_F(TestApiBlackSolver, defineFun)
TEST_F(TestApiBlackSolver, defineFunGlobal)
{
Sort bSort = d_solver.getBooleanSort();
- Sort fSort = d_solver.mkFunctionSort(bSort, bSort);
Term bTrue = d_solver.mkBoolean(true);
// (define-fun f () Bool true)
Term f = d_solver.defineFun("f", {}, bSort, bTrue, true);
Term b = d_solver.mkVar(bSort, "b");
- Term gSym = d_solver.mkConst(fSort, "g");
// (define-fun g (b Bool) Bool b)
- Term g = d_solver.defineFun(gSym, {b}, b, true);
+ Term g = d_solver.defineFun("g", {b}, bSort, b, true);
// (assert (or (not f) (not (g true))))
d_solver.assertFormula(d_solver.mkTerm(
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback