Option to treat define-fun as Eunoia definitions

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

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.

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;

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;

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;
 };
 
 /**

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

tests/reference-define-fun.eo

@@ -0,0 +1,6 @@
+(declare-const Int Type)
+(declare-const > (-> Int Int Bool))
+(declare-consts <numeral> Int)
+(set-option :reference-define-fun true)
+(reference "reference-define-fun.smt2")
+(assume @p0 (> x 0))

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)

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 <string>)`, 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.