summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/preprocessing/passes/anonymize_strings.cpp54
-rw-r--r--src/smt/dump.cpp60
-rw-r--r--src/smt/smt_engine.cpp16
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())
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback