From 8975d286f5da01112bbb9f8f7f9e357a48953314 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 17 Feb 2014 16:03:23 -0500 Subject: Fix strings preprocessing for justification heuristic --- src/smt/options_handlers.h | 7 ++++--- src/smt/smt_engine.cpp | 9 ++++++++- 2 files changed, 12 insertions(+), 4 deletions(-) (limited to 'src/smt') diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h index 51ad7b6ca..c9c3d6345 100644 --- a/src/smt/options_handlers.h +++ b/src/smt/options_handlers.h @@ -83,9 +83,9 @@ assertions\n\ + Output the assertions after preprocessing and before clausification.\n\ Can also specify \"assertions:pre-PASS\" or \"assertions:post-PASS\",\n\ where PASS is one of the preprocessing passes: definition-expansion\n\ - boolean-terms constrain-subtypes substitution skolem-quant simplify\n\ - static-learning ite-removal repeat-simplify rewrite-apply-to-const\n\ - theory-preprocessing.\n\ + boolean-terms constrain-subtypes substitution strings-pp skolem-quant\n\ + simplify static-learning ite-removal repeat-simplify\n\ + rewrite-apply-to-const theory-preprocessing.\n\ PASS can also be the special value \"everything\", in which case the\n\ assertions are printed before any preprocessing (with\n\ \"assertions:pre-everything\") or after all preprocessing completes\n\ @@ -181,6 +181,7 @@ inline void dumpMode(std::string option, std::string optarg, SmtEngine* smt) { } else if(!strcmp(p, "boolean-terms")) { } else if(!strcmp(p, "constrain-subtypes")) { } else if(!strcmp(p, "substitution")) { + } else if(!strcmp(p, "strings-pp")) { } else if(!strcmp(p, "skolem-quant")) { } else if(!strcmp(p, "simplify")) { } else if(!strcmp(p, "static-learning")) { diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index dcca1624d..ec91e566e 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3124,11 +3124,18 @@ void SmtEnginePrivate::processAssertions() { // Assertions ARE guaranteed to be rewritten by this point if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ) { + dumpAssertions("pre-strings-pp", d_assertionsToPreprocess); CVC4::theory::strings::StringsPreprocess sp; - sp.simplify( d_assertionsToPreprocess ); + std::vector newNodes; + newNodes.push_back(d_assertionsToPreprocess[d_realAssertionsEnd - 1]); + sp.simplify( d_assertionsToPreprocess, newNodes ); + if(newNodes.size() > 1) { + d_assertionsToPreprocess[d_realAssertionsEnd - 1] = NodeManager::currentNM()->mkNode(kind::AND, newNodes); + } for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) { d_assertionsToPreprocess[i] = Rewriter::rewrite( d_assertionsToPreprocess[i] ); } + dumpAssertions("post-strings-pp", d_assertionsToPreprocess); } if( d_smt.d_logic.isQuantified() ){ dumpAssertions("pre-skolem-quant", d_assertionsToPreprocess); -- cgit v1.2.3