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 <noetzli@amazon.com>

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 31ab49158d58f951be77f3a59ee373212f22b2bd..e58172b92cb8b65aa25fe27db8c20672097b4b52 100644 (file)
--- 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 d478163b84f722384be03bc590c76176fca99ab3..8e8080bc36d7ce23c9292a86cf8329a8876a7853 100644 (file)
--- 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 b9b7de1495675e8ee37c845fc49ee1d292841094..a226f7cbfdb6102c9c1c0f76b5ca16acec33f107 100644 (file)
--- 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<api::Term, std::string>();
   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<api::Sort> 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 a698b963368481f635c15b406d06b58c5fac7160..5fcf496374d389e976605a7bdcf54a43cdb7cfb8 100644 (file)
--- 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 34645b44129306765814d4bfe3cd30aec39e1cb9..445cac18e5c779cedb79642f970c3b4559b50c34 100644 (file)
--- 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<Node, Node>& newLambda)
 {
   NodeManager* nm = NodeManager::currentNM();
-  std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
-  std::vector<TNode> visit;
+  std::unordered_map<Node, Node, TNodeHashFunction>::iterator it;
+  std::vector<Node> 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<TNode, Node, TNodeHashFunction>::iterator it;
+  std::unordered_map<Node, Node, NodeHashFunction>::iterator it;
   std::map<Node, Node> preReplace;
   std::map<Node, Node>::iterator itr;
   std::vector<TNode> visit;
@@ -319,7 +319,7 @@ PreprocessingPassResult HoElim::applyInternal(
   {
     std::map<Node, Node> lproc = newLambda;
     newLambda.clear();
-    for (const std::pair<Node, Node>& l : lproc)
+    for (const std::pair<const Node, Node>& l : lproc)
     {
       Node lambda = l.second;
       std::vector<Node> vars;

diff --git a/src/preprocessing/passes/ho_elim.h b/src/preprocessing/passes/ho_elim.h
index 1a3142b393d1af4ec8683044a8d7a4f3d7629b48..2edc9607400b6e066308ee5a7bcdc03af5853dad 100644 (file)
--- 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<TNode, Node, TNodeHashFunction> d_visited;
+  std::unordered_map<Node, Node, NodeHashFunction> 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 cc5c911ff40fb7ca9c126de5274ed64355e01461..1eca91a5ad9fb256a94a5ab7c9601e9639c957db 100644 (file)
--- 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 (file)
index 0000000..8bb7c38
--- /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 76a37886b75728a3d6a1d75ed7172fb4230a0f4e..6ce3f4b01fcdf20a2594601490333571f272f95e 100644 (file)
--- 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 7b4006c5da324da5acbbd4ad9680732f4f959af6..244b0ecd9e085615bcb2bccd1d20eae1e86dabdc 100644 (file)
--- 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 583f94ed4b291fc66640e3bcf217f72ce72bed0d..7e349996d20d6572dd184a141ceedb62a9414baf 100644 (file)
--- 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))