diff --git a/src/cmd_parser.cpp b/src/cmd_parser.cpp index b0dc1edb..6b07ac20 100644 --- a/src/cmd_parser.cpp +++ b/src/cmd_parser.cpp @@ -24,17 +24,19 @@ 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; @@ -42,9 +44,12 @@ CmdParser::CmdParser(Lexer& lex, 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(); } } diff --git a/src/cmd_parser.h b/src/cmd_parser.h index 3d661a5c..83f3e38d 100644 --- a/src/cmd_parser.h +++ b/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 d_table; /** */ + bool d_isSignature; + /** */ bool d_isReference; /** Is finished */ bool d_isFinished; diff --git a/src/parser.cpp b/src/parser.cpp index f08a1e57..e39e426d 100644 --- a/src/parser.cpp +++ b/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) { } diff --git a/src/parser.h b/src/parser.h index 53726840..26868230 100644 --- a/src/parser.h +++ b/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. diff --git a/src/state.cpp b/src/state.cpp index 39a984ed..524e3ae0 100644 --- a/src/state.cpp +++ b/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::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); } diff --git a/src/state.h b/src/state.h index 7174e273..c09a3a41 100644 --- a/src/state.h +++ b/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 d_referenceAsserts; + /** Active reference asserts and their multiplicity in the current stack */ + std::unordered_map d_referenceAssertCount; /** Reference assert list */ std::vector d_referenceAssertList; + /** Reference assert stack */ + std::vector d_referenceAssertSizeCtx; //--------------------- garbage collection /** The current set of expression values to delete */ std::vector d_toDelete; diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt index ff73914c..efe86d64 100644 --- a/tests/CMakeLists.txt +++ b/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 + $ + ${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") diff --git a/tests/push-pop.eo b/tests/push-pop-proof.pf similarity index 59% rename from tests/push-pop.eo rename to tests/push-pop-proof.pf index e024340a..08b216ac 100644 --- a/tests/push-pop.eo +++ b/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) diff --git a/tests/push-pop-setup.eo b/tests/push-pop-setup.eo new file mode 100644 index 00000000..e31f006c --- /dev/null +++ b/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) diff --git a/tests/push-pop-signature.eo b/tests/push-pop-signature.eo new file mode 100644 index 00000000..9fbb1489 --- /dev/null +++ b/tests/push-pop-signature.eo @@ -0,0 +1 @@ +(push) diff --git a/tests/reference-push-pop-setup.eo b/tests/reference-push-pop-setup.eo new file mode 100644 index 00000000..d8063906 --- /dev/null +++ b/tests/reference-push-pop-setup.eo @@ -0,0 +1,3 @@ +(declare-const Int Type) +(declare-const > (-> Int Int Bool)) +(declare-consts Int) diff --git a/tests/reference-push-pop.pf b/tests/reference-push-pop.pf new file mode 100644 index 00000000..1b2f2e5b --- /dev/null +++ b/tests/reference-push-pop.pf @@ -0,0 +1,3 @@ +(include "reference-push-pop-setup.eo") +(reference "reference-push-pop.smt2") +(assume @p0 (> x 0)) diff --git a/tests/reference-push-pop.smt2 b/tests/reference-push-pop.smt2 new file mode 100644 index 00000000..0990ae5f --- /dev/null +++ b/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) diff --git a/tests/run_expect_fail.sh b/tests/run_expect_fail.sh new file mode 100644 index 00000000..eb25feda --- /dev/null +++ b/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 diff --git a/user_manual.md b/user_manual.md index 704a0f46..9bea4df9 100644 --- a/user_manual.md +++ b/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 ?)` 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 ?)` 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 (*) *)`, defines `` 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,6 +2018,7 @@ When Ethos encounters a command of the form `(reference )`, 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 G)`, ethos will check whether `G` occurs in the set of parsed reference assertions. @@ -2021,7 +2026,7 @@ If it does not, then an error is thrown indicating that the proof is assuming a > __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 `*`. - _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 `*`. 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 (*) ? ? ? ? :conclusion *) | (define (*) *) | (include ) | + (pop ?) | (program (*) :signature (+) (( )+)) | + (push ?) | (reference ?) | (step ? :rule ? ?) | (step-pop ? :rule ? ?) | @@ -2146,6 +2154,8 @@ When streaming input to Ethos, we assume the input is being given for a proof fi (define-const ) | (define-fun (*) ) | (define-sort (*) ) | + (pop ?) | + (push ?) | (set-info ) | (set-logic ) |