diff options
author | Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> | 2020-08-12 17:51:48 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-12 17:51:48 -0500 |
commit | 079a04b0b16f7caa31a15b97ddc9794ad0d8b862 (patch) | |
tree | a8c56b4ca8ed13fdfddbca7692504624069cf5e2 /src/smt/smt_engine.cpp | |
parent | 103b5ea715e532e021e91f9b03ea7d7876a3ccbf (diff) |
Refactor functions that print commands (Part 1) (#4869)
This PR is a step towards migrating commands to the Term/Sort level. The functions for printing synth-fun command and its grammar were modified to remove their dependency on command objects and use nodes instead of exprs and types. Similar changes to other functions that print commands will follow.
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 33 |
1 files changed, 30 insertions, 3 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 13865b2ec..7f6d3db9d 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1324,9 +1324,36 @@ void SmtEngine::declareSynthFun(const std::string& id, setUserAttribute("sygus-synth-grammar", func, attr_value, ""); } Trace("smt") << "SmtEngine::declareSynthFun: " << func << "\n"; - // dumping SynthFunCommand from smt-engine is currently broken (please take at - // CVC4/cvc4-projects#211) - // Dump("raw-benchmark") << SynthFunCommand(id, func, sygusType, isInv, vars); + + // !!! TEMPORARY: We cannot construct a SynthFunCommand since we cannot + // construct a Term-level Grammar from a Node-level sygus TypeNode. Thus we + // must print the command using the Node-level utility method for now. + + if (Dump.isOn("raw-benchmark")) + { + std::vector<Node> nodeVars; + nodeVars.reserve(vars.size()); + for (const Expr& var : vars) + { + nodeVars.push_back(Node::fromExpr(var)); + } + + std::stringstream ss; + + Printer::getPrinter(options::outputLanguage()) + ->toStreamCmdSynthFun( + ss, + id, + nodeVars, + func.getType().isFunction() + ? TypeNode::fromType(func.getType()).getRangeType() + : TypeNode::fromType(func.getType()), + isInv, + TypeNode::fromType(sygusType)); + + Dump("raw-benchmark") << ss.str(); + } + // sygus conjecture is now stale setSygusConjectureStale(); } |