diff options
author | Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> | 2020-02-17 08:58:42 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-17 08:58:42 -0600 |
commit | ed27cf0f854e014922f9690d967c5ff9aa73693c (patch) | |
tree | 42e1ffa003635a1a1b47dbb2ace29dce4dcdb88e /src/smt | |
parent | 6b6290e89632108f35dd24924ac62bb0d69e462a (diff) |
Support dumping Sygus commands. (#3763)
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 41 |
1 files changed, 19 insertions, 22 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 1d96fc207..f1d602bc6 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3652,16 +3652,27 @@ void SmtEngine::ensureBoolean(const Expr& e) Result SmtEngine::checkSat(const Expr& assumption, bool inUnsatCore) { + Dump("benchmark") << CheckSatCommand(assumption); return checkSatisfiability(assumption, inUnsatCore, false); } Result SmtEngine::checkSat(const vector<Expr>& assumptions, bool inUnsatCore) { + if (assumptions.empty()) + { + Dump("benchmark") << CheckSatCommand(); + } + else + { + Dump("benchmark") << CheckSatAssumingCommand(assumptions); + } + return checkSatisfiability(assumptions, inUnsatCore, false); } Result SmtEngine::query(const Expr& assumption, bool inUnsatCore) { + Dump("benchmark") << QueryCommand(assumption, inUnsatCore); return checkSatisfiability(assumption.isNull() ? std::vector<Expr>() : std::vector<Expr>{assumption}, @@ -3789,25 +3800,6 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions, d_needPostsolve = true; - // Dump the query if requested - if (Dump.isOn("benchmark")) - { - size_t size = assumptions.size(); - // the expr already got dumped out if assertion-dumping is on - if (isQuery && size == 1) - { - Dump("benchmark") << QueryCommand(assumptions[0]); - } - else if (size == 0) - { - Dump("benchmark") << CheckSatCommand(); - } - else - { - Dump("benchmark") << CheckSatAssumingCommand(d_assumptions); - } - } - // Pop the context if (didInternalPush) { @@ -3936,6 +3928,7 @@ void SmtEngine::declareSygusVar(const std::string& id, Expr var, Type type) { d_private->d_sygusVars.push_back(Node::fromExpr(var)); Trace("smt") << "SmtEngine::declareSygusVar: " << var << "\n"; + Dump("raw-benchmark") << DeclareSygusVarCommand(id, var, type); // don't need to set that the conjecture is stale } @@ -3943,6 +3936,7 @@ void SmtEngine::declareSygusPrimedVar(const std::string& id, Type type) { // do nothing (the command is spurious) Trace("smt") << "SmtEngine::declareSygusPrimedVar: " << id << "\n"; + Dump("raw-benchmark") << DeclareSygusPrimedVarCommand(id, type); // don't need to set that the conjecture is stale } @@ -3952,6 +3946,7 @@ void SmtEngine::declareSygusFunctionVar(const std::string& id, { d_private->d_sygusVars.push_back(Node::fromExpr(var)); Trace("smt") << "SmtEngine::declareSygusFunctionVar: " << var << "\n"; + Dump("raw-benchmark") << DeclareSygusFunctionCommand(id, var, type); // don't need to set that the conjecture is stale } @@ -3984,6 +3979,7 @@ void SmtEngine::declareSynthFun(const std::string& id, setUserAttribute("sygus-synth-grammar", func, attr_value, ""); } Trace("smt") << "SmtEngine::declareSynthFun: " << func << "\n"; + Dump("raw-benchmark") << SynthFunCommand(id, func, sygusType, isInv, vars); // sygus conjecture is now stale setSygusConjectureStale(); } @@ -3994,6 +3990,7 @@ void SmtEngine::assertSygusConstraint(Expr constraint) d_private->d_sygusConstraints.push_back(constraint); Trace("smt") << "SmtEngine::assertSygusConstrant: " << constraint << "\n"; + Dump("raw-benchmark") << SygusConstraintCommand(constraint); // sygus conjecture is now stale setSygusConjectureStale(); } @@ -4065,6 +4062,7 @@ void SmtEngine::assertSygusInvConstraint(const Expr& inv, d_private->d_sygusConstraints.push_back(constraint); Trace("smt") << "SmtEngine::assertSygusInvConstrant: " << constraint << "\n"; + Dump("raw-benchmark") << SygusInvConstraintCommand(inv, pre, trans, post); // sygus conjecture is now stale setSygusConjectureStale(); } @@ -4118,6 +4116,7 @@ Result SmtEngine::checkSynth() setUserAttribute("sygus", sygusVar.toExpr(), {}, ""); Trace("smt") << "Check synthesis conjecture: " << body << std::endl; + Dump("raw-benchmark") << CheckSynthCommand(); d_private->d_sygusConjectureStale = false; @@ -4195,9 +4194,7 @@ Expr SmtEngine::expandDefinitions(const Expr& ex) // Ensure expr is type-checked at this point. e.getType(true); } - if(Dump.isOn("benchmark")) { - Dump("benchmark") << ExpandDefinitionsCommand(e); - } + unordered_map<Node, Node, NodeHashFunction> cache; Node n = d_private->expandDefinitions(Node::fromExpr(e), cache, /* expandOnly = */ true); n = postprocess(n, TypeNode::fromType(e.getType())); |