diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-20 19:47:35 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-04-20 19:47:35 -0500 |
commit | ad7907adff119a6e25fe3c229663afecb15db7c4 (patch) | |
tree | 0cf0c1931db8d4529127806eca03cd014fcb6a42 /src/preprocessing | |
parent | 6255c0356bd78140a9cf075491c1d4608ac27704 (diff) |
Make option names related to CEGQI consistent (#4316)
This updates option names to be consistent across uses of counterexample-guided quantifier instantiation (ceqgi), which was previously called "counterexample-based quantifier instantiation" (cbqi), and sygus.
Notably, the trace "cegqi-engine" is changed to "sygus-engine" by this commit.
The changes were done by these commands in the given directories:
src/:
for f in $(find -name '.'); do sed -i 's/options::cbqi/options::cegqi/g' $f;sed -i 's/cegqi-engine/sygus-engine/g' $f; done;sed -i 's/"cbqi/"cegqi/g' $f; done
test/regress/:
for f in $(find -name '.'); do sed -i 's/--cbqi/--cegqi/g' $f; done
src/: and test/regress/:
for f in $(find -name '.'); do sed -i 's/cegqi-si/sygus-si/g' $f; done
test/regress/:
for f in $(find -name '.'); do sed -i 's/no-cbqi/no-cegqi/g' $f; done
test/regress/:
for f in $(find -name '.'); do sed -i 's/:cbqi/:cegqi/g' $f; done
And a few minor fixes afterwards.
This should be merged close to the time of the next stable release.
Diffstat (limited to 'src/preprocessing')
-rw-r--r-- | src/preprocessing/passes/global_negate.cpp | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/preprocessing/passes/global_negate.cpp b/src/preprocessing/passes/global_negate.cpp index 5e7d42632..59b5ddf6e 100644 --- a/src/preprocessing/passes/global_negate.cpp +++ b/src/preprocessing/passes/global_negate.cpp @@ -30,14 +30,14 @@ namespace passes { Node GlobalNegate::simplify(std::vector<Node>& assertions, NodeManager* nm) { Assert(!assertions.empty()); - Trace("cbqi-gn") << "Global negate : " << std::endl; + Trace("cegqi-gn") << "Global negate : " << std::endl; // collect free variables in all assertions std::vector<Node> free_vars; std::vector<TNode> visit; std::unordered_set<TNode, TNodeHashFunction> visited; for (const Node& as : assertions) { - Trace("cbqi-gn") << " " << as << std::endl; + Trace("cegqi-gn") << " " << as << std::endl; TNode cur = as; // compute free variables visit.push_back(cur); @@ -90,9 +90,9 @@ Node GlobalNegate::simplify(std::vector<Node>& assertions, NodeManager* nm) body = nm->mkNode(FORALL, bvl, body); } - Trace("cbqi-gn-debug") << "...got (pre-rewrite) : " << body << std::endl; + Trace("cegqi-gn-debug") << "...got (pre-rewrite) : " << body << std::endl; body = Rewriter::rewrite(body); - Trace("cbqi-gn") << "...got (post-rewrite) : " << body << std::endl; + Trace("cegqi-gn") << "...got (post-rewrite) : " << body << std::endl; return body; } |