From f625c0b8dbab3830198e6ad4ea9748cecd301389 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 2 May 2014 07:11:08 -0500 Subject: Add option --dt-stc-ind for strengthening skolemization. Refactor skolemization. --- src/smt/smt_engine.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'src/smt') 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; -- cgit v1.2.3