diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-05-08 12:12:01 -0700 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-08 14:12:01 -0500 |
| commit | 4f3416bf998cdf3fc8b6adf6debb7e65d663bd7c (patch) | |
| tree | fb69add9a72bc40f0ec010579965070ae912186a | |
| parent | 919c30e541668ad1ada6a294be55112594a942bd (diff) | |
Fix order of preprocessing pass registration. (#1887)
| -rw-r--r-- | src/smt/smt_engine.cpp | 28 |
1 files changed, 15 insertions, 13 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 10d21a66c..c9733983a 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2586,27 +2586,29 @@ void SmtEnginePrivate::finishInit() { d_preprocessingPassContext.reset(new PreprocessingPassContext(&d_smt)); // TODO: register passes here (this will likely change when we add support for // actually assembling preprocessing pipelines). - std::unique_ptr<BVGauss> bvGauss(new BVGauss(d_preprocessingPassContext.get())); - std::unique_ptr<IntToBV> intToBV(new IntToBV(d_preprocessingPassContext.get())); + std::unique_ptr<BoolToBV> boolToBv( + new BoolToBV(d_preprocessingPassContext.get())); + std::unique_ptr<BVGauss> bvGauss( + new BVGauss(d_preprocessingPassContext.get())); + std::unique_ptr<BvIntroPow2> bvIntroPow2( + new BvIntroPow2(d_preprocessingPassContext.get())); + std::unique_ptr<BVToBool> bvToBool( + new BVToBool(d_preprocessingPassContext.get())); + std::unique_ptr<IntToBV> intToBV( + new IntToBV(d_preprocessingPassContext.get())); std::unique_ptr<PseudoBooleanProcessor> pbProc( new PseudoBooleanProcessor(d_preprocessingPassContext.get())); std::unique_ptr<RealToInt> realToInt( new RealToInt(d_preprocessingPassContext.get())); + d_preprocessingPassRegistry.registerPass("bool-to-bv", std::move(boolToBv)); d_preprocessingPassRegistry.registerPass("bv-gauss", std::move(bvGauss)); + d_preprocessingPassRegistry.registerPass("bv-intro-pow2", + std::move(bvIntroPow2)); + d_preprocessingPassRegistry.registerPass("bv-to-bool", std::move(bvToBool)); d_preprocessingPassRegistry.registerPass("int-to-bv", std::move(intToBV)); - d_preprocessingPassRegistry.registerPass("real-to-int", std::move(realToInt)); d_preprocessingPassRegistry.registerPass("pseudo-boolean-processor", std::move(pbProc)); - std::unique_ptr<BVToBool> bvToBool( - new BVToBool(d_preprocessingPassContext.get())); - d_preprocessingPassRegistry.registerPass("bv-to-bool", std::move(bvToBool)); - std::unique_ptr<BoolToBV> boolToBv( - new BoolToBV(d_preprocessingPassContext.get())); - d_preprocessingPassRegistry.registerPass("bool-to-bv", std::move(boolToBv)); - std::unique_ptr<BvIntroPow2> bvIntroPow2( - new BvIntroPow2(d_preprocessingPassContext.get())); - d_preprocessingPassRegistry.registerPass("bv-intro-pow2", - std::move(bvIntroPow2)); + d_preprocessingPassRegistry.registerPass("real-to-int", std::move(realToInt)); } Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, NodeHashFunction>& cache, bool expandOnly) |