Official push/pop support

src/cmd_parser.cpp

@@ -24,27 +24,32 @@ namespace ethos {
 CmdParser::CmdParser(Lexer& lex,
                      State& state,
                      ExprParser& eparser,
+                     bool isSignature,
                      bool isReference)
     : d_lex(lex),
       d_state(state),
       d_tc(state.getTypeChecker()),
       d_sts(state.getStats()),
       d_eparser(eparser),
+      d_isSignature(isSignature),
       d_isReference(isReference),
       d_isFinished(false)
 {
   // initialize the command tokens
-  // commands supported in both inputs and proofs
+  // commands supported in proofs, references, and signatures
   d_table["declare-const"] = Token::DECLARE_CONST;
   d_table["declare-datatype"] = Token::DECLARE_DATATYPE;
   d_table["declare-datatypes"] = Token::DECLARE_DATATYPES;
   d_table["declare-sort"] = Token::DECLARE_SORT;
   d_table["echo"] = Token::ECHO;
   d_table["exit"] = Token::EXIT;
   d_table["set-option"] = Token::SET_OPTION;
-  d_table["pop"] = Token::POP;    // undocumented
-  d_table["push"] = Token::PUSH;  // undocumented
   d_table["reset"] = Token::RESET;
+  if (!d_isSignature)
+  {
+    d_table["pop"] = Token::POP;
+    d_table["push"] = Token::PUSH;
+  }
 
   if (d_isReference)
   {
@@ -1010,9 +1015,17 @@ bool CmdParser::parseNextCommand()
         if (isPush)
         {
           d_state.pushScope();
+          if (d_isReference)
+          {
+            d_state.pushReferenceScope();
+          }
         }
         else
         {
+          if (d_isReference)
+          {
+            d_state.popReferenceScope();
+          }
           d_state.popScope();
         }
       }

src/cmd_parser.h

@@ -27,6 +27,7 @@ class CmdParser
   CmdParser(Lexer& lex,
             State& state,
             ExprParser& eparser,
+            bool isSignature,
             bool isReference);
   virtual ~CmdParser() {}
   /**
@@ -49,6 +50,8 @@ class CmdParser
   /** Map strings to tokens */
   std::map<std::string, Token> d_table;
   /** */
+  bool d_isSignature;
+  /** */
   bool d_isReference;
   /** Is finished */
   bool d_isFinished;

src/parser.cpp

@@ -16,7 +16,7 @@ Parser::Parser(State& s, bool isSignature, bool isReference)
     : d_lex(!isSignature && s.getOptions().d_parseLet, isSignature),
       d_state(s),
       d_eparser(d_lex, d_state, isSignature),
-      d_cmdParser(d_lex, d_state, d_eparser, isReference)
+      d_cmdParser(d_lex, d_state, d_eparser, isSignature, isReference)
 {
 }
 

src/parser.h

@@ -30,7 +30,9 @@ class Parser
    * @param isSignature Whether we are parsing a signature file
    * @param isReference Whether we are parsing a reference file
    */
-  Parser(State& s, bool isSignature = false, bool isReference = false);
+  Parser(State& s,
+         bool isSignature = false,
+         bool isReference = false);
   virtual ~Parser() {}
 
   /** Set the input for the given file.

src/state.cpp

@@ -278,6 +278,35 @@ void State::popAssumptionScope()
   // pop the parsing scope
   popScope();
 }
+
+void State::pushReferenceScope()
+{
+  d_referenceAssertSizeCtx.push_back(d_referenceAssertList.size());
+}
+
+void State::popReferenceScope()
+{
+  if (d_referenceAssertSizeCtx.empty())
+  {
+    EO_FATAL() << "State::popReferenceScope: empty context";
+  }
+  size_t lastSize = d_referenceAssertSizeCtx.back();
+  d_referenceAssertSizeCtx.pop_back();
+  while (d_referenceAssertList.size() > lastSize)
+  {
+    Expr aa = d_referenceAssertList.back();
+    d_referenceAssertList.pop_back();
+    std::unordered_map<const ExprValue*, size_t>::iterator it =
+        d_referenceAssertCount.find(aa.getValue());
+    Assert(it != d_referenceAssertCount.end() && it->second > 0);
+    it->second--;
+    if (it->second == 0)
+    {
+      d_referenceAssertCount.erase(it);
+    }
+  }
+}
+
 bool State::includeFile(const std::string& s, bool isSignature)
 {
   return includeFile(s, isSignature, false, d_null);
@@ -462,7 +491,8 @@ bool State::addAssumption(const Expr& a)
       {
         aa = mkExpr(Kind::APPLY, {d_referenceNf, a});
       }
-      return d_referenceAsserts.find(aa.getValue()) != d_referenceAsserts.end();
+      return d_referenceAssertCount.find(aa.getValue())
+             != d_referenceAssertCount.end();
     }
   }
   return true;
@@ -475,7 +505,7 @@ void State::addReferenceAssert(const Expr& a)
   {
     aa = mkExpr(Kind::APPLY, {d_referenceNf, a});
   }
-  d_referenceAsserts.insert(aa.getValue());
+  d_referenceAssertCount[aa.getValue()]++;
   // ensure ref count
   d_referenceAssertList.push_back(aa);
 }

src/state.h

@@ -69,6 +69,10 @@ class State
   void pushAssumptionScope();
   /** Pop assumption scope */
   void popAssumptionScope();
+  /** Push reference assertion scope */
+  void pushReferenceScope();
+  /** Pop reference assertion scope */
+  void popReferenceScope();
   /** include file, if not already done, return false if error */
   bool includeFile(const std::string& s, bool isSignature);
   /** include file, possibly as a reference */
@@ -402,10 +406,12 @@ class State
   bool d_hasReference;
   /** The reference normalization function, if it exists */
   Expr d_referenceNf;
-  /** Reference asserts */
-  std::unordered_set<const ExprValue*> d_referenceAsserts;
+  /** Active reference asserts and their multiplicity in the current stack */
+  std::unordered_map<const ExprValue*, size_t> d_referenceAssertCount;
   /** Reference assert list */
   std::vector<Expr> d_referenceAssertList;
+  /** Reference assert stack */
+  std::vector<size_t> d_referenceAssertSizeCtx;
   //--------------------- garbage collection
   /** The current set of expression values to delete */
   std::vector<ExprValue*> d_toDelete;

tests/CMakeLists.txt

@@ -110,7 +110,8 @@ set(ethos_test_file_list
     opaque-inst.eo
     opaque-inst2.eo
     mutual-rec.eo
-    push-pop.eo
+    push-pop-proof.pf
+    reference-push-pop.pf
     bv-extract-smt3.eo
     distinct_value_testers.eo
     gt_eval.eo
@@ -181,7 +182,21 @@ macro(ethos_test file)
   set_tests_properties(${file} PROPERTIES TIMEOUT 40)
 endmacro()
 
+macro(ethos_fail_test file regex)
+  add_test(
+    NAME ${file}
+    COMMAND
+      bash
+      ${CMAKE_CURRENT_LIST_DIR}/run_expect_fail.sh
+      $<TARGET_FILE:ethos>
+      ${CMAKE_CURRENT_LIST_DIR}/${file}
+      ${regex}
+  )
+  set_tests_properties(${file} PROPERTIES TIMEOUT 40)
+endmacro()
+
 foreach(file ${ethos_test_file_list})
   ethos_test(${file})
 endforeach()
 
+ethos_fail_test(push-pop-signature.eo "Expected Eunoia command")

tests/push-pop.eo → tests/push-pop-proof.pf

@@ -1,14 +1,4 @@
-(include "Builtin-theory.eo")
-
-; REFL
-(declare-rule refl ((T Type) (t T))
-    :premises ()
-    :args (t)
-    :conclusion (= t t)
-)
-
-(declare-const Int Type)
-(declare-const b Int)
+(include "push-pop-setup.eo")
 
 (push)
 (declare-const a Bool)

tests/push-pop-setup.eo

@@ -0,0 +1,11 @@
+(include "Builtin-theory.eo")
+
+; REFL
+(declare-rule refl ((T Type) (t T))
+    :premises ()
+    :args (t)
+    :conclusion (= t t)
+)
+
+(declare-const Int Type)
+(declare-const b Int)

tests/push-pop-signature.eo

@@ -0,0 +1 @@
+(push)

tests/reference-push-pop-setup.eo

@@ -0,0 +1,3 @@
+(declare-const Int Type)
+(declare-const > (-> Int Int Bool))
+(declare-consts <numeral> Int)

tests/reference-push-pop.pf

@@ -0,0 +1,3 @@
+(include "reference-push-pop-setup.eo")
+(reference "reference-push-pop.smt2")
+(assume @p0 (> x 0))

tests/reference-push-pop.smt2

@@ -0,0 +1,7 @@
+(set-logic ALL)
+(push)
+(declare-fun y () Int)
+(pop)
+(declare-fun x () Int)
+(assert (> x 0))
+(check-sat)

tests/run_expect_fail.sh

@@ -0,0 +1,24 @@
+#!/usr/bin/env bash
+
+set -euo pipefail
+
+prog="$1"
+input="$2"
+pattern="$3"
+
+set +e
+output="$("$prog" "$input" 2>&1)"
+status=$?
+set -e
+
+printf '%s\n' "$output"
+
+if [ "$status" -eq 0 ]; then
+  echo "Expected failure but command succeeded" >&2
+  exit 1
+fi
+
+if ! printf '%s\n' "$output" | grep -Eq "$pattern"; then
+  echo "Expected output to match: $pattern" >&2
+  exit 1
+fi

user_manual.md

@@ -123,6 +123,10 @@ The following commands are supported for declaring and defining types and terms.
 
 - `(reset)` removes all declarations and definitions and resets the global scope. This command is similar in nature to its counterpart in SMT-LIB.
 
+- `(push <numeral>?)` pushes the current declaration scope one or more levels, where the default is `1`. This command is accepted in proof files and in reference files, but not in signature files.
+
+- `(pop <numeral>?)` pops the current declaration scope one or more levels, where the default is `1`. This command is accepted in proof files and in reference files, but not in signature files.
+
 The Eunoia language contains further commands for declaring symbols that are not standard SMT-LIB version 3.0:
 
 - `(define <symbol> (<typed-param>*) <term> <attr>*)`, defines `<symbol>` to be a lambda term whose arguments and body are given by the command, or just an arbitrary term defined by the provided the body, if the argument list is empty (i.e., it may be a non-function term). Note that in contrast to the SMT-LIB command `define-fun`, a return type is not provided. It is also possible to provide attributes to the definition: e.g. `:type`, which instructs the checker to perform type checking on the given term (see [type checking define](#tcdefine)).
@@ -2014,14 +2018,15 @@ When Ethos encounters a command of the form `(reference <string>)`, the checker
 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 commands of the form `(assert F)` will add `F` to a set of formulas we will refer to as the _reference assertions_.
+The commands `push` and `pop` update the current scope while parsing the reference file.
 Other commands in `file.smt2` (e.g. `set-logic`, `set-option`, and so on) will be ignored.
 
 If ethos has read a reference file, then for each command of the form `(assume <symbol> G)`, ethos will check whether `G` occurs in the set of parsed reference assertions.
 If it does not, then an error is thrown indicating that the proof is assuming a formula that is not a part of the original input.
 
 > __Note:__ Only one reference command can be executed for each run of ethos.
 
-> __Note:__ Incremental `*.smt2` inputs are not supported as reference files in the current version of ethos.
+> __Note:__ Full incremental `*.smt2` inputs are not supported as reference files in the current version of ethos. In particular, assumptions are matched against the assertions that remain active after the reference file finishes parsing.
 
 ### Validation up to Normalization
 
@@ -2108,6 +2113,7 @@ Their expected syntax is `<smtlib2-command>*`.
 - _Signature files_ are files that given via command line option that have extension `*.eo`, or those that are included via the command `include`. Like proof files, their expected syntax is `<eo-command>*`.
 
 As mentioned, the first two kinds of file inputs take into account options concerning the normalization of terms (e.g. `--normalize-num`), while signature files do not.
+The commands `push` and `pop` are parsed in proof files and in reference files; they are rejected in signature files.
 When streaming input to Ethos, we assume the input is being given for a proof file.
 
 ```smt
@@ -2120,7 +2126,9 @@ When streaming input to Ethos, we assume the input is being given for a proof fi
     (declare-rule <symbol> (<typed-param>*) <assumption>? <premises>? <arguments>? <reqs>? :conclusion <term> <attr>*) |
     (define <symbol> (<typed-param>*) <term> <attr>*) |
     (include <string>) |
+    (pop <numeral>?) |
     (program <symbol> (<typed-param>*) :signature (<type>+) <type> ((<term> <term>)+)) |
+    (push <numeral>?) |
     (reference <string> <symbol>?) |
     (step <symbol> <term>? :rule <symbol> <simple-premises>? <arguments>?) |
     (step-pop <symbol> <term>? :rule <symbol> <simple-premises>? <arguments>?) |
@@ -2146,6 +2154,8 @@ When streaming input to Ethos, we assume the input is being given for a proof fi
     (define-const <symbol> <term>) |
     (define-fun <symbol> (<typed-param>*) <type> <term>) |
     (define-sort <symbol> (<symbol>*) <type>) |
+    (pop <numeral>?) |
+    (push <numeral>?) |
     (set-info <attr>) |
     (set-logic <symbol>) |
     <common-command>