diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-02 07:11:08 -0500 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-02 07:11:08 -0500 |
| commit | f625c0b8dbab3830198e6ad4ea9748cecd301389 (patch) | |
| tree | 002c16f88e1f66529b32cb5e184b52567e048adf /src/smt | |
| parent | 7d3f8788309cfb241df60e6924861dd9884e1a7b (diff) | |
Add option --dt-stc-ind for strengthening skolemization. Refactor skolemization.
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/smt_engine.cpp | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 6dd1f4465..a411530e6 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2893,8 +2893,9 @@ void SmtEnginePrivate::processAssertions() { for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) { Node prev = d_assertionsToPreprocess[i]; Trace("quantifiers-rewrite-debug") << "Pre-skolemize " << prev << "..." << std::endl; - vector< Node > fvs; - d_assertionsToPreprocess[i] = Rewriter::rewrite( quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( prev, true, fvs ) ); + vector< TypeNode > fvTypes; + vector< TNode > fvs; + d_assertionsToPreprocess[i] = Rewriter::rewrite( quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( prev, true, fvTypes, fvs ) ); if( prev!=d_assertionsToPreprocess[i] ){ Trace("quantifiers-rewrite") << "*** Pre-skolemize " << prev << endl; Trace("quantifiers-rewrite") << " ...got " << d_assertionsToPreprocess[i] << endl; |