diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/preprocessing/passes/anonymize_strings.cpp | 54 | ||||
-rw-r--r-- | src/smt/dump.cpp | 60 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 16 |
3 files changed, 90 insertions, 40 deletions
diff --git a/src/preprocessing/passes/anonymize_strings.cpp b/src/preprocessing/passes/anonymize_strings.cpp index af644771f..0714d61d4 100644 --- a/src/preprocessing/passes/anonymize_strings.cpp +++ b/src/preprocessing/passes/anonymize_strings.cpp @@ -265,33 +265,52 @@ PreprocessingPassResult AnonymizeStrings::applyInternal( Trace("anonymize-strings") << "Queries: " << queries << std::endl; - bool dumpBenchmark = Dump.on("benchmark"); + bool dumpBenchmark = Dump.isOn("anonymization-benchmark"); - ExprManager em(nm->getOptions()); - SmtEngine checker(&em); + SmtEngine checker(nm->toExprManager()); + checker.setIsInternalSubsolver(); { smt::SmtScope smts(&checker); - Dump.off(); + + if (Dump.isOn("anonymization-benchmark")) + { + Dump.on("raw-benchmark"); + } + else + { + Dump.off(); + } } - checker.setOption("anonymize-strings", false); - checker.setOption("preprocess-only", false); - checker.setOption("produce-models", true); + // checker.setOption("anonymize-strings", false); + // checker.setOption("preprocess-only", false); + // checker.setOption("produce-models", true); ExprManagerMapCollection varMap; for (const Node& query : queries) { - Expr equery = query.toExpr().exportTo(&em, varMap); + Expr equery = query.toExpr(); checker.assertFormula(equery); } - checker.checkSat(); + + if (dumpBenchmark) + { + // HACK + std::cout << "(check-sat)" << std::endl; + Dump.off(); + return PreprocessingPassResult::NO_CONFLICT; + } + else + { + checker.checkSat(); + } std::unordered_map<Node, Node, NodeHashFunction> substs; Trace("anonymize-strings") << "Values:" << std::endl; for (const auto& kv : lits) { - Expr esk = kv.second.toExpr().exportTo(&em, varMap); + Expr esk = kv.second.toExpr(); substs[kv.first] = Node::fromExpr(checker.getValue(esk)); Trace("anonymize-strings") << "..." << kv.second << " = " << kv.first << " -> " << checker.getValue(esk) << std::endl; @@ -304,20 +323,13 @@ PreprocessingPassResult AnonymizeStrings::applyInternal( (*assertionsToPreprocess)[i].substitute( substs.begin(), substs.end(), cache)); - if (dumpBenchmark) - { - // HACK!!!! - std::cout << "(assert " << (*assertionsToPreprocess)[i] << ")" - << std::endl; - } - } - - if (dumpBenchmark) - { // HACK!!!! - std::cout << "(check-sat)" << std::endl; + std::cout << "(assert " << (*assertionsToPreprocess)[i] << ")" << std::endl; } + // HACK!!!! + std::cout << "(check-sat)" << std::endl; + return PreprocessingPassResult::NO_CONFLICT; } diff --git a/src/smt/dump.cpp b/src/smt/dump.cpp index 90c89cd3d..cbe564d34 100644 --- a/src/smt/dump.cpp +++ b/src/smt/dump.cpp @@ -43,10 +43,19 @@ void DumpC::setDumpFromString(const std::string& optarg) { tokstr = NULL; if(!strcmp(optargPtr, "raw-benchmark")) { } else if(!strcmp(optargPtr, "benchmark")) { - } else if(!strcmp(optargPtr, "declarations")) { - } else if(!strcmp(optargPtr, "assertions")) { + } + else if (!strcmp(optargPtr, "anonymization-benchmark")) + { + } + else if (!strcmp(optargPtr, "declarations")) + { + } + else if (!strcmp(optargPtr, "assertions")) + { Dump.on("assertions:post-everything"); - } else if(!strncmp(optargPtr, "assertions:", 11)) { + } + else if (!strncmp(optargPtr, "assertions:", 11)) + { const char* p = optargPtr + 11; if(!strncmp(p, "pre-", 4)) { p += 4; @@ -66,13 +75,18 @@ void DumpC::setDumpFromString(const std::string& optarg) { optargPtr + "'. Please consult --dump help."); } Dump.on("assertions"); - } else if(!strcmp(optargPtr, "skolems")) { - } else if(!strcmp(optargPtr, "clauses")) { - } else if(!strcmp(optargPtr, "t-conflicts") || - !strcmp(optargPtr, "t-lemmas") || - !strcmp(optargPtr, "t-explanations") || - !strcmp(optargPtr, "bv-rewrites") || - !strcmp(optargPtr, "theory::fullcheck")) { + } + else if (!strcmp(optargPtr, "skolems")) + { + } + else if (!strcmp(optargPtr, "clauses")) + { + } + else if (!strcmp(optargPtr, "t-conflicts") || !strcmp(optargPtr, "t-lemmas") + || !strcmp(optargPtr, "t-explanations") + || !strcmp(optargPtr, "bv-rewrites") + || !strcmp(optargPtr, "theory::fullcheck")) + { // These are "non-state-dumping" modes. If state (SAT decisions, // propagations, etc.) is dumped, it will interfere with the validity // of these generated queries. @@ -85,10 +99,12 @@ void DumpC::setDumpFromString(const std::string& optarg) { } else { Dump.on("no-permit-state"); } - } else if(!strcmp(optargPtr, "state") || - !strcmp(optargPtr, "missed-t-conflicts") || - !strcmp(optargPtr, "t-propagations") || - !strcmp(optargPtr, "missed-t-propagations")) { + } + else if (!strcmp(optargPtr, "state") + || !strcmp(optargPtr, "missed-t-conflicts") + || !strcmp(optargPtr, "t-propagations") + || !strcmp(optargPtr, "missed-t-propagations")) + { // These are "state-dumping" modes. If state (SAT decisions, // propagations, etc.) is not dumped, it will interfere with the // validity of these generated queries. @@ -101,7 +117,9 @@ void DumpC::setDumpFromString(const std::string& optarg) { } else { Dump.on("state"); } - } else if(!strcmp(optargPtr, "help")) { + } + else if (!strcmp(optargPtr, "help")) + { puts(s_dumpHelp.c_str()); std::stringstream ss; @@ -114,11 +132,17 @@ void DumpC::setDumpFromString(const std::string& optarg) { } puts(ss.str().c_str()); exit(1); - } else if(!strcmp(optargPtr, "bv-abstraction")) { + } + else if (!strcmp(optargPtr, "bv-abstraction")) + { Dump.on("bv-abstraction"); - } else if(!strcmp(optargPtr, "bv-algebraic")) { + } + else if (!strcmp(optargPtr, "bv-algebraic")) + { Dump.on("bv-algebraic"); - } else { + } + else + { throw OptionException(std::string("unknown option for --dump: `") + optargPtr + "'. Try --dump help."); } diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 2b80badf8..191cc2a0a 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1142,6 +1142,14 @@ void SmtEngine::setLogic(const LogicInfo& logic) void SmtEngine::setLogic(const std::string& s) { SmtScope smts(this); + + // HACK + if (!d_isInternalSubsolver && options::anonymizeStrings() + && !Dump.isOn("anonymization-benchmark")) + { + Dump.setDumpFromString("declarations"); + } + try { setLogic(LogicInfo(s)); } catch(IllegalArgumentException& e) { @@ -1180,6 +1188,11 @@ void SmtEngine::setDefaults() { is_sygus = true; } + if (!d_isInternalSubsolver && options::anonymizeStrings()) + { + setOption("produce-models", SExpr("true")); + } + if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { if (options::produceModels() @@ -3148,9 +3161,10 @@ void SmtEnginePrivate::processAssertions() { return; } - if (options::anonymizeStrings()) + if (!d_smt.d_isInternalSubsolver && options::anonymizeStrings()) { d_passes["anonymize-strings"]->apply(&d_assertions); + return; } if (options::bvGaussElim()) |