From cbf7821fcf44429aabfbba582304614863e74fcb Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 13 Apr 2026 13:11:19 -0500 Subject: [PATCH 1/2] Option for define-fun --- src/cmd_parser.cpp | 5 ++++- src/main.cpp | 1 + src/state.cpp | 5 +++++ src/state.h | 5 +++++ tests/CMakeLists.txt | 1 + tests/reference-define-fun.eo | 6 ++++++ tests/reference-define-fun.smt2 | 6 ++++++ user_manual.md | 5 ++++- 8 files changed, 32 insertions(+), 2 deletions(-) create mode 100644 tests/reference-define-fun.eo create mode 100644 tests/reference-define-fun.smt2 diff --git a/src/cmd_parser.cpp b/src/cmd_parser.cpp index 044db608..94f2ceca 100644 --- a/src/cmd_parser.cpp +++ b/src/cmd_parser.cpp @@ -608,7 +608,10 @@ bool CmdParser::parseNextCommand() { d_eparser.typeCheck(expr, ret); } - if (tok == Token::DEFINE_FUN) + bool defineFunAsReferenceAssert = + tok == Token::DEFINE_FUN && d_isReference + && !d_state.getOptions().d_referenceDefineFun; + if (defineFunAsReferenceAssert) { // This is for reference checking only. Note that = and lambda are // not builtin symbols, thus we must assume they are defined by the user. diff --git a/src/main.cpp b/src/main.cpp index dff12d3c..63d1e7fa 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -67,6 +67,7 @@ int main( int argc, char* argv[] ) out << " --no-print-dag: do not dagify the output of terms in error messages and trace messages." << std::endl; out << "--no-rule-sym-table: do not use a separate symbol table for proof rules and declared terms." << std::endl; out << " --reference=X: includes the file specified by X as a reference file." << std::endl; + out << "--reference-define-fun: in reference files, treat define-fun as a definition instead of a reference assertion." << std::endl; out << " --show-config: displays the build information for this binary." << std::endl; out << " --stats: enables detailed statistics." << std::endl; out << " --stats-all: enables all available statistics." << std::endl; diff --git a/src/state.cpp b/src/state.cpp index 75131268..5c52f186 100644 --- a/src/state.cpp +++ b/src/state.cpp @@ -28,6 +28,7 @@ Options::Options() d_normalizeDecimal = true; d_normalizeHexadecimal = true; d_normalizeNumeral = false; + d_referenceDefineFun = false; } bool Options::setOption(const std::string& key, bool val) @@ -72,6 +73,10 @@ bool Options::setOption(const std::string& key, bool val) { d_normalizeHexadecimal = val; } + else if (key == "reference-define-fun") + { + d_referenceDefineFun = val; + } else { return false; diff --git a/src/state.h b/src/state.h index 5500ff79..6cbb85f0 100644 --- a/src/state.h +++ b/src/state.h @@ -45,6 +45,11 @@ class Options bool d_normalizeHexadecimal; /** Treat numerals as rational literals */ bool d_normalizeNumeral; + /** + * In reference files, parse SMT-LIB define-fun commands as Eunoia-style + * definitions instead of translating them to reference assertions. + */ + bool d_referenceDefineFun; }; /** diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt index 40a6467f..b5e4b54a 100644 --- a/tests/CMakeLists.txt +++ b/tests/CMakeLists.txt @@ -125,6 +125,7 @@ set(ethos_test_file_list implicit-then-var.eo is_eq.eo simple-reference.eo + reference-define-fun.eo simple-quant-reference.eo simple-lra-reference.eo left-cons.eo diff --git a/tests/reference-define-fun.eo b/tests/reference-define-fun.eo new file mode 100644 index 00000000..a691ccf1 --- /dev/null +++ b/tests/reference-define-fun.eo @@ -0,0 +1,6 @@ +(declare-const Int Type) +(declare-const > (-> Int Int Bool)) +(declare-consts Int) +(set-option :reference-define-fun true) +(reference "reference-define-fun.smt2") +(assume @p0 (> x 0)) diff --git a/tests/reference-define-fun.smt2 b/tests/reference-define-fun.smt2 new file mode 100644 index 00000000..de220146 --- /dev/null +++ b/tests/reference-define-fun.smt2 @@ -0,0 +1,6 @@ +; regression: parse reference-file define-fun as a Eunoia definition when enabled +(set-logic ALL) +(declare-fun x () Int) +(define-fun gt0 ((y Int)) Bool (> y 0)) +(assert (gt0 x)) +(check-sat) diff --git a/user_manual.md b/user_manual.md index 3d099448..d7153f75 100644 --- a/user_manual.md +++ b/user_manual.md @@ -2014,7 +2014,9 @@ Additionally, files may be included or referenced on the command line with the o When Ethos encounters a command of the form `(reference )`, the checker enables a further set of checks that ensures that all assumptions in proofs correspond to assertions from the file referenced by the given string. In particular, when the command `(reference "file.smt2")` is read, Ethos will parse `file.smt2`. -The definitions and declaration commands in this file will be treated as normal, that is, they will populate the symbol table of Ethos as they normally would if they were to appear in an `*.eo` input. +The declaration commands in this file will be treated as normal, that is, they will populate the symbol table of Ethos as they normally would if they were to appear in an `*.eo` input. +By default, `define-fun` commands in reference files are interpreted as reference assertions equating the defined symbol with its body. +If the option `reference-define-fun` is enabled, they are instead parsed as Eunoia definitions. The commands of the form `(assert F)` will add `F` to a set of formulas we will refer to as the _reference assertions_. Other commands in `file.smt2` (e.g. `set-logic`, `set-option`, and so on) will be ignored. @@ -2089,6 +2091,7 @@ They do not impact how signature files (*.eo) are parsed: - `--no-normalize-dec`: do not treat decimal literals as syntax sugar for rational literals. - `--no-normalize-hex`: do not treat hexadecimal literals as syntax sugar for binary literals. - `--no-parse-let`: do not treat `let` as a builtin symbol for specifying a macro. +- `--reference-define-fun`: when parsing reference files, treat `define-fun` commands as Eunoia definitions instead of reference assertions. Most of the above options can also be set via `set-option` commands within proofs or Eunoia scripts. For example, the command `(set-option normalize-num true)` tells Ethos to normalize numerals always. From b50eec466b41d6ed1a5af548d0429b13e6a9f148 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 13 Apr 2026 13:15:27 -0500 Subject: [PATCH 2/2] News --- NEWS.md | 1 + 1 file changed, 1 insertion(+) diff --git a/NEWS.md b/NEWS.md index d6707e55..af6ecd9b 100644 --- a/NEWS.md +++ b/NEWS.md @@ -7,6 +7,7 @@ ethos 0.2.3 prerelease - Updates to the external plugin interface. - The identifier `Type` is no longer treated as a keyword in proofs and reference files. - The command `declare-sort` is now allowed in proof files. +- Adds the option `--reference-define-fun` to parse `define-fun` in reference files as Eunoia definitions instead of reference assertions. - The builtin `eo::to_str` no longer prints rationals, decimals, or bitvectors. It now only evaluates on strings and numeral code points. - Adds support for an attribute `:is_eq` to test whether a defined term is equal to another. - Fixes a bug where the character code point `\u{30000}` was incorrectly