summaryrefslogtreecommitdiff
path: root/src/preprocessing
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2020-10-08 22:28:42 -0700
committerGitHub <noreply@github.com>2020-10-08 22:28:42 -0700
commit36addc33791da4b1fbae9fbcec87ac26cfc7a270 (patch)
treec7eee80da27439ed684a12afe22382bae43b4e35 /src/preprocessing
parente5913461e103bd1c7740e88f748524ae66672b53 (diff)
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>
Diffstat (limited to 'src/preprocessing')
-rw-r--r--src/preprocessing/passes/ho_elim.cpp8
-rw-r--r--src/preprocessing/passes/ho_elim.h2
2 files changed, 5 insertions, 5 deletions
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<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 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<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.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback