mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

fix typos #4573

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-07-13 11:10:12 -07:00
parent a298091322
commit 549ef0e052
2 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/cmd_context/basic_cmds.cpp
View file

@ -767,7 +767,7 @@ public:
return m_array_fid;
}
char const * get_usage() const override { return "<symbol> (<sort>+) <func-decl-ref>"; }
char const * get_descr(cmd_context & ctx) const override { return "declare a new array map operator with name <symbol> using the given function declaration.\n<func-decl-ref> ::= <symbol>\n | (<symbol> (<sort>*) <sort>)\n | ((_ <symbol> <numeral>+) (<sort>*) <sort>)\nThe last two cases are used to disumbiguate between declarations with the same name and/or select (indexed) builtin declarations.\nFor more details about the array map operator, see 'Generalized and Efficient Array Decision Procedures' (FMCAD 2009).\nExample: (declare-map set-union (Int) (or (Bool Bool) Bool))\nDeclares a new function (declare-fun set-union ((Array Int Bool) (Array Int Bool)) (Array Int Bool)).\nThe instance of the map axiom for this new declaration is:\n(forall ((a1 (Array Int Bool)) (a2 (Array Int Bool)) (i Int)) (= (select (set-union a1 a2) i) (or (select a1 i) (select a2 i))))"; }
char const * get_descr(cmd_context & ctx) const override { return "declare a new array map operator with name <symbol> using the given function declaration.\n<func-decl-ref> ::= <symbol>\n | (<symbol> (<sort>*) <sort>)\n | ((_ <symbol> <numeral>+) (<sort>*) <sort>)\nThe last two cases are used to disambiguate between declarations with the same name and/or select (indexed) builtin declarations.\nFor more details about the array map operator, see 'Generalized and Efficient Array Decision Procedures' (FMCAD 2009).\nExample: (declare-map set-union (Int) (or (Bool Bool) Bool))\nDeclares a new function (declare-fun set-union ((Array Int Bool) (Array Int Bool)) (Array Int Bool)).\nThe instance of the map axiom for this new declaration is:\n(forall ((a1 (Array Int Bool)) (a2 (Array Int Bool)) (i Int)) (= (select (set-union a1 a2) i) (or (select a1 i) (select a2 i))))"; }
unsigned get_arity() const override { return 3; }
void prepare(cmd_context & ctx) override { m_name = symbol::null; m_domain.reset(); }
cmd_arg_kind next_arg_kind(cmd_context & ctx) const override {

2
src/cmd_context/cmd_context.cpp
View file

@ -934,7 +934,7 @@ func_decl * cmd_context::find_func_decl(symbol const & s) const {
func_decls fs;
if (m_func_decls.find(s, fs)) {
if (fs.more_than_one())
throw cmd_exception("ambiguous function declaration reference, provide full signature to disumbiguate (<symbol> (<sort>*) <sort>) ", s);
throw cmd_exception("ambiguous function declaration reference, provide full signature to disambiguate (<symbol> (<sort>*) <sort>) ", s);
return fs.first();
}
builtin_decl d;