From 36addc33791da4b1fbae9fbcec87ac26cfc7a270 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Thu, 8 Oct 2020 22:28:42 -0700 Subject: [PATCH] reset-assertions: Remove all non-global symbols in the parser (#5229) Fixes #5163. When `:global-declarations` is disabled (the default), then `(reset-assertions)` should remove all declared and defined symbols. Before this commit, we would remove the defined function from `SmtEngine` but the parser would not remove it from its symbol table because the symbol was defined at (what it considered) level 0. Level 0, however, is reserved for global symbols that we never want to remove. This commit adds an additional global `pushScope()`/`popScope()`, similar to what we have in `SmtEngine`. As a result, user-defined symbols are now defined at level 1 and get removed from the `SymbolTable` when `(reset-assertions)` is called. The commit also makes sure that symbols defined by the logic are asserted at level 0, so that they are not removed by `(reset-assertions)`. It adds a flag to `defineType` to ignore duplicate definitions because some symbols are defined by multiple logics, which leads to a failing assertion when inserting them both at level 0 in the hashmap of the `SymbolTable`. E.g. strings and integer arithmetic both define `Int`. The commit also fixes existing unit tests that fail with these stricter semantics of `(reset-assertions)`. Signed-off-by: Andres Noetzli --- src/parser/parser.cpp | 8 +++- src/parser/parser.h | 8 +++- src/parser/smt2/smt2.cpp | 41 +++++++++---------- src/parser/smt2/smt2.h | 2 + src/preprocessing/passes/ho_elim.cpp | 8 ++-- src/preprocessing/passes/ho_elim.h | 2 +- test/regress/CMakeLists.txt | 1 + test/regress/regress0/parser/issue5163.smt2 | 10 +++++ test/regress/regress0/smtlib/issue4077.smt2 | 1 + .../regress0/smtlib/reset-assertions1.smt2 | 1 + .../regress1/sygus/interpol_cosa_1.smt2 | 1 - 11 files changed, 52 insertions(+), 31 deletions(-) create mode 100644 test/regress/regress0/parser/issue5163.smt2 diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 31ab49158..e58172b92 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -291,8 +291,14 @@ void Parser::defineVar(const std::string& name, void Parser::defineType(const std::string& name, const api::Sort& type, - bool levelZero) + bool levelZero, + bool skipExisting) { + if (skipExisting && isDeclared(name, SYM_SORT)) + { + assert(api::Sort(d_solver, d_symtab->lookupType(name)) == type); + return; + } d_symtab->bindType(name, type.getType(), levelZero); assert(isDeclared(name, SYM_SORT)); } diff --git a/src/parser/parser.h b/src/parser/parser.h index d478163b8..8e8080bc3 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -531,11 +531,15 @@ public: * @param name The name of the type * @param type The type that should be associated with the name * @param levelZero If true, the type definition is considered global and - * cannot be removed by poppoing the user context + * cannot be removed by popping the user context + * @param skipExisting If true, the type definition is ignored if the same + * symbol has already been defined. It is assumed that + * the definition is the exact same as the existing one. */ void defineType(const std::string& name, const api::Sort& type, - bool levelZero = false); + bool levelZero = false, + bool skipExisting = false); /** * Create a new (parameterized) type definition. diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index b9b7de149..a226f7cbf 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -37,12 +37,11 @@ Smt2::Smt2(api::Solver* solver, Input* input, bool strictMode, bool parseOnly) d_logicSet(false), d_seenSetLogic(false) { - if (!strictModeEnabled()) - { - addCoreSymbols(); - } + pushScope(true); } +Smt2::~Smt2() { popScope(); } + void Smt2::addArithmeticOperators() { addOperator(api::PLUS, "+"); addOperator(api::MINUS, "-"); @@ -288,9 +287,9 @@ void Smt2::addSepOperators() { void Smt2::addCoreSymbols() { - defineType("Bool", d_solver->getBooleanSort()); - defineVar("true", d_solver->mkTrue()); - defineVar("false", d_solver->mkFalse()); + defineType("Bool", d_solver->getBooleanSort(), true, true); + defineVar("true", d_solver->mkTrue(), true, true); + defineVar("false", d_solver->mkFalse(), true, true); addOperator(api::AND, "and"); addOperator(api::DISTINCT, "distinct"); addOperator(api::EQUAL, "="); @@ -472,10 +471,7 @@ void Smt2::reset() { operatorKindMap.clear(); d_lastNamedTerm = std::pair(); this->Parser::reset(); - - if( !strictModeEnabled() ) { - addCoreSymbols(); - } + pushScope(true); } void Smt2::resetAssertions() { @@ -483,6 +479,7 @@ void Smt2::resetAssertions() { while (this->scopeLevel() > 0) { this->popScope(); } + pushScope(true); } Smt2::SynthFunFactory::SynthFunFactory( @@ -604,7 +601,7 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) if(d_logic.isTheoryEnabled(theory::THEORY_ARITH)) { if(d_logic.areIntegersUsed()) { - defineType("Int", d_solver->getIntegerSort()); + defineType("Int", d_solver->getIntegerSort(), true, true); addArithmeticOperators(); addOperator(api::INTS_DIVISION, "div"); addOperator(api::INTS_MODULUS, "mod"); @@ -614,7 +611,7 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) if (d_logic.areRealsUsed()) { - defineType("Real", d_solver->getRealSort()); + defineType("Real", d_solver->getRealSort(), true, true); addArithmeticOperators(); addOperator(api::DIVISION, "/"); if (!strictModeEnabled()) @@ -663,7 +660,7 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) if(d_logic.isTheoryEnabled(theory::THEORY_DATATYPES)) { const std::vector types; - defineType("Tuple", d_solver->mkTupleSort(types)); + defineType("Tuple", d_solver->mkTupleSort(types), true, true); addDatatypesOperators(); } @@ -708,9 +705,9 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) addOperator(api::BAG_TO_SET, "bag.to_set"); } if(d_logic.isTheoryEnabled(theory::THEORY_STRINGS)) { - defineType("String", d_solver->getStringSort()); - defineType("RegLan", d_solver->getRegExpSort()); - defineType("Int", d_solver->getIntegerSort()); + defineType("String", d_solver->getStringSort(), true, true); + defineType("RegLan", d_solver->getRegExpSort(), true, true); + defineType("Int", d_solver->getIntegerSort(), true, true); if (getLanguage() == language::input::LANG_SMTLIB_V2_6 || getLanguage() == language::input::LANG_SYGUS_V2) @@ -735,11 +732,11 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) } if (d_logic.isTheoryEnabled(theory::THEORY_FP)) { - defineType("RoundingMode", d_solver->getRoundingModeSort()); - defineType("Float16", d_solver->mkFloatingPointSort(5, 11)); - defineType("Float32", d_solver->mkFloatingPointSort(8, 24)); - defineType("Float64", d_solver->mkFloatingPointSort(11, 53)); - defineType("Float128", d_solver->mkFloatingPointSort(15, 113)); + defineType("RoundingMode", d_solver->getRoundingModeSort(), true, true); + defineType("Float16", d_solver->mkFloatingPointSort(5, 11), true, true); + defineType("Float32", d_solver->mkFloatingPointSort(8, 24), true, true); + defineType("Float64", d_solver->mkFloatingPointSort(11, 53), true, true); + defineType("Float128", d_solver->mkFloatingPointSort(15, 113), true, true); defineVar("RNE", d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN)); defineVar("roundNearestTiesToEven", diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index a698b9633..5fcf49637 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -73,6 +73,8 @@ class Smt2 : public Parser bool parseOnly = false); public: + ~Smt2(); + /** * Add core theory symbols to the parser state. */ diff --git a/src/preprocessing/passes/ho_elim.cpp b/src/preprocessing/passes/ho_elim.cpp index 34645b441..445cac18e 100644 --- a/src/preprocessing/passes/ho_elim.cpp +++ b/src/preprocessing/passes/ho_elim.cpp @@ -33,8 +33,8 @@ HoElim::HoElim(PreprocessingPassContext* preprocContext) Node HoElim::eliminateLambdaComplete(Node n, std::map& newLambda) { NodeManager* nm = NodeManager::currentNM(); - std::unordered_map::iterator it; - std::vector visit; + std::unordered_map::iterator it; + std::vector visit; TNode cur; visit.push_back(n); do @@ -148,7 +148,7 @@ Node HoElim::eliminateHo(Node n) { Trace("ho-elim-assert") << "Ho-elim assertion: " << n << std::endl; NodeManager* nm = NodeManager::currentNM(); - std::unordered_map::iterator it; + std::unordered_map::iterator it; std::map preReplace; std::map::iterator itr; std::vector visit; @@ -319,7 +319,7 @@ PreprocessingPassResult HoElim::applyInternal( { std::map lproc = newLambda; newLambda.clear(); - for (const std::pair& l : lproc) + for (const std::pair& l : lproc) { Node lambda = l.second; std::vector vars; diff --git a/src/preprocessing/passes/ho_elim.h b/src/preprocessing/passes/ho_elim.h index 1a3142b39..2edc96074 100644 --- a/src/preprocessing/passes/ho_elim.h +++ b/src/preprocessing/passes/ho_elim.h @@ -112,7 +112,7 @@ class HoElim : public PreprocessingPass * Stores the set of nodes we have current visited and their results * in steps [1] and [2] of this pass. */ - std::unordered_map d_visited; + std::unordered_map d_visited; /** * Stores the mapping from functions f to their corresponding function H(f) * in the encoding for step [2] of this pass. diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index cc5c911ff..1eca91a5a 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -644,6 +644,7 @@ set(regress_0_tests regress0/parser/declarefun-emptyset-uf.smt2 regress0/parser/force_logic_set_logic.smt2 regress0/parser/force_logic_success.smt2 + regress0/parser/issue5163.smt2 regress0/parser/shadow_fun_symbol_all.smt2 regress0/parser/shadow_fun_symbol_nirat.smt2 regress0/parser/strings20.smt2 diff --git a/test/regress/regress0/parser/issue5163.smt2 b/test/regress/regress0/parser/issue5163.smt2 new file mode 100644 index 000000000..8bb7c382f --- /dev/null +++ b/test/regress/regress0/parser/issue5163.smt2 @@ -0,0 +1,10 @@ +; SCRUBBER: grep -o "Symbol a is not declared" +; EXPECT: Symbol a is not declared +; EXIT: 1 +(set-logic ALL) +(define-fun a () Bool false) +(reset-assertions) +(declare-const x Int) +(assert (and (= (+ x x) 0) true)) +(assert a) +(check-sat) diff --git a/test/regress/regress0/smtlib/issue4077.smt2 b/test/regress/regress0/smtlib/issue4077.smt2 index 76a37886b..6ce3f4b01 100644 --- a/test/regress/regress0/smtlib/issue4077.smt2 +++ b/test/regress/regress0/smtlib/issue4077.smt2 @@ -3,6 +3,7 @@ ; Use a quantified logic to make sure that TheoryEngine creates a master ; equality engine +(set-option :global-declarations true) (set-logic BV) (declare-const x (_ BitVec 4)) (push) diff --git a/test/regress/regress0/smtlib/reset-assertions1.smt2 b/test/regress/regress0/smtlib/reset-assertions1.smt2 index 7b4006c5d..244b0ecd9 100644 --- a/test/regress/regress0/smtlib/reset-assertions1.smt2 +++ b/test/regress/regress0/smtlib/reset-assertions1.smt2 @@ -1,5 +1,6 @@ ; EXPECT: unsat ; EXPECT: sat +(set-option :global-declarations true) (set-logic QF_BV) (declare-fun v0 () (_ BitVec 4)) (set-option :produce-models true) diff --git a/test/regress/regress1/sygus/interpol_cosa_1.smt2 b/test/regress/regress1/sygus/interpol_cosa_1.smt2 index 583f94ed4..7e349996d 100644 --- a/test/regress/regress1/sygus/interpol_cosa_1.smt2 +++ b/test/regress/regress1/sygus/interpol_cosa_1.smt2 @@ -12,7 +12,6 @@ (declare-fun clk@1 () (_ BitVec 1)) (declare-fun a@1 () (_ BitVec 16)) (declare-fun b@1 () (_ BitVec 16)) -(reset-assertions) (declare-fun cfg@0 () (_ BitVec 1)) (declare-fun witness_0@0 () Bool) (declare-fun counter@0 () (_ BitVec 16)) -- 2.30.2