diff options
| author | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-14 19:37:31 +0000 |
|---|---|---|
| committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-14 19:37:31 +0000 |
| commit | b849eeef09465da1100cd6a94beacc893849fb25 (patch) | |
| tree | 569562d3de4aa31268a52dc14edec4e0dece7a4a /src/smt/smt_engine.cpp | |
| parent | 2581001b96a64e1d11d826cf554d378ac522bbe2 (diff) | |
New substitutions implementation - fixes performance issue seen in nonclausal
simplification for some benchmarks
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 6771b8cd5..3da8e1b33 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1004,7 +1004,7 @@ void SmtEnginePrivate::nonClausalSimplify() { Assert(!t.isConst()); Assert(constantPropagations.apply(t) == t); Assert(d_topLevelSubstitutions.apply(t) == t); - constantPropagations.addSubstitution(t, c, true, false, false); + constantPropagations.addSubstitution(t, c); // vector<pair<Node,Node> > equations;a // constantPropagations.simplifyLHS(t, c, equations, true); // if (!equations.empty()) { |