From 51382b96a76c6ddef0c1a6aae2139203f20bced1 Mon Sep 17 00:00:00 2001 From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> Date: Tue, 2 Nov 2021 15:14:19 -0500 Subject: [PATCH] Add printing methods for some commands. (#7557) This PR is a step towards enabling -o raw-benchmark. It adds printing methods for some of the new commands and fixes some other miscellaneous issues. --- src/printer/printer.cpp | 3 +- src/printer/printer.h | 18 +++++---- src/printer/smt2/smt2_printer.cpp | 61 ++++++++++++++++++++++++++++++- src/printer/smt2/smt2_printer.h | 38 +++++++++++++++---- src/smt/command.cpp | 6 +-- 5 files changed, 106 insertions(+), 20 deletions(-) diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index ec0fdeda1..cc9df91f4 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -411,7 +411,8 @@ void Printer::toStreamCmdGetAbduct(std::ostream& out, } void Printer::toStreamCmdGetQuantifierElimination(std::ostream& out, - Node n) const + Node n, + bool doFull) const { printUnknownCommand(out, "get-quantifier-elimination"); } diff --git a/src/printer/printer.h b/src/printer/printer.h index 8c8118aa9..485cd70e6 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -179,11 +179,11 @@ class Printer virtual void toStreamCmdGetModel(std::ostream& out) const; /** Print block-model command */ - void toStreamCmdBlockModel(std::ostream& out) const; + virtual void toStreamCmdBlockModel(std::ostream& out) const; /** Print block-model-values command */ - void toStreamCmdBlockModelValues(std::ostream& out, - const std::vector& nodes) const; + virtual void toStreamCmdBlockModelValues( + std::ostream& out, const std::vector& nodes) const; /** Print get-proof command */ virtual void toStreamCmdGetProof(std::ostream& out) const; @@ -192,10 +192,10 @@ class Printer void toStreamCmdGetInstantiations(std::ostream& out) const; /** Print get-interpol command */ - void toStreamCmdGetInterpol(std::ostream& out, - const std::string& name, - Node conj, - TypeNode sygusType) const; + virtual void toStreamCmdGetInterpol(std::ostream& out, + const std::string& name, + Node conj, + TypeNode sygusType) const; /** Print get-abduct command */ virtual void toStreamCmdGetAbduct(std::ostream& out, @@ -204,7 +204,9 @@ class Printer TypeNode sygusType) const; /** Print get-quantifier-elimination command */ - void toStreamCmdGetQuantifierElimination(std::ostream& out, Node n) const; + virtual void toStreamCmdGetQuantifierElimination(std::ostream& out, + Node n, + bool doFull) const; /** Print get-unsat-assumptions command */ virtual void toStreamCmdGetUnsatAssumptions(std::ostream& out) const; diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 171f8e524..d6e6fc4eb 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1199,7 +1199,7 @@ std::string Smt2Printer::smtKindString(Kind k, Variant v) case kind::SEP_STAR: return "sep"; case kind::SEP_PTO: return "pto"; case kind::SEP_WAND: return "wand"; - case kind::SEP_EMP: return "emp"; + case kind::SEP_EMP: return "sep.emp"; // quantifiers case kind::FORALL: return "forall"; @@ -1437,6 +1437,23 @@ void Smt2Printer::toStreamCmdDeclareFunction(std::ostream& out, out << ") " << type << ')' << std::endl; } +void Smt2Printer::toStreamCmdDeclarePool( + std::ostream& out, + const std::string& id, + TypeNode type, + const std::vector& initValue) const +{ + out << "(declare-pool " << cvc5::quoteSymbol(id) << ' ' << type << " ("; + for (size_t i = 0, n = initValue.size(); i < n; ++i) + { + if (i != 0) { + out << ' '; + } + out << initValue[i]; + } + out << "))" << std::endl; +} + void Smt2Printer::toStreamCmdDefineFunction(std::ostream& out, const std::string& id, const std::vector& formals, @@ -1577,6 +1594,26 @@ void Smt2Printer::toStreamCmdGetModel(std::ostream& out) const out << "(get-model)" << std::endl; } +void Smt2Printer::toStreamCmdBlockModel(std::ostream& out) const +{ + out << "(block-model)" << std::endl; +} + +void Smt2Printer::toStreamCmdBlockModelValues( + std::ostream& out, const std::vector& nodes) const +{ + out << "(block-model-values ("; + for (size_t i = 0, n = nodes.size(); i < n; ++i) + { + if (i != 0) + { + out << ' '; + } + out << nodes[i]; + } + out << "))" << std::endl; +} + void Smt2Printer::toStreamCmdGetAssignment(std::ostream& out) const { out << "(get-assignment)" << std::endl; @@ -1858,6 +1895,20 @@ void Smt2Printer::toStreamCmdCheckSynth(std::ostream& out) const out << "(check-synth)" << std::endl; } +void Smt2Printer::toStreamCmdGetInterpol(std::ostream& out, + const std::string& name, + Node conj, + TypeNode sygusType) const +{ + out << "(get-interpol " << cvc5::quoteSymbol(name) << ' ' << conj; + if (!sygusType.isNull()) + { + out << ' '; + toStreamSygusGrammar(out, sygusType); + } + out << ')' << std::endl; +} + void Smt2Printer::toStreamCmdGetAbduct(std::ostream& out, const std::string& name, Node conj, @@ -1875,6 +1926,14 @@ void Smt2Printer::toStreamCmdGetAbduct(std::ostream& out, out << ')' << std::endl; } +void Smt2Printer::toStreamCmdGetQuantifierElimination(std::ostream& out, + Node n, + bool doFull) const +{ + out << '(' << (doFull ? "get-qe" : "get-qe-disjunct") << ' ' << n << ')' + << std::endl; +} + /* -------------------------------------------------------------------------- End of Handling SyGuS commands diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index e0b6fedbc..2af17ed59 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -74,9 +74,14 @@ class Smt2Printer : public cvc5::Printer const std::string& id, TypeNode type) const override; + /** Print declare-pool command */ + void toStreamCmdDeclarePool(std::ostream& out, + const std::string& id, + TypeNode type, + const std::vector& initValue) const override; + /** Print declare-sort command */ - void toStreamCmdDeclareType(std::ostream& out, - TypeNode type) const override; + void toStreamCmdDeclareType(std::ostream& out, TypeNode type) const override; /** Print define-sort command */ void toStreamCmdDefineType(std::ostream& out, @@ -114,11 +119,12 @@ class Smt2Printer : public cvc5::Printer TypeNode type) const override; /** Print synth-fun command */ - void toStreamCmdSynthFun(std::ostream& out, - Node f, - const std::vector& vars, - bool isInv, - TypeNode sygusType = TypeNode::null()) const override; + void toStreamCmdSynthFun( + std::ostream& out, + Node f, + const std::vector& vars, + bool isInv, + TypeNode sygusType = TypeNode::null()) const override; /** Print constraint command */ void toStreamCmdConstraint(std::ostream& out, Node n) const override; @@ -149,15 +155,33 @@ class Smt2Printer : public cvc5::Printer /** Print get-model command */ void toStreamCmdGetModel(std::ostream& out) const override; + /** Print block-model command */ + void toStreamCmdBlockModel(std::ostream& out) const override; + + /** Print block-model-values command */ + void toStreamCmdBlockModelValues( + std::ostream& out, const std::vector& nodes) const override; + /** Print get-proof command */ void toStreamCmdGetProof(std::ostream& out) const override; + /** Print get-interpol command */ + void toStreamCmdGetInterpol(std::ostream& out, + const std::string& name, + Node conj, + TypeNode sygusType) const override; + /** Print get-abduct command */ void toStreamCmdGetAbduct(std::ostream& out, const std::string& name, Node conj, TypeNode sygusType) const override; + /** Print get-quantifier-elimination command */ + void toStreamCmdGetQuantifierElimination(std::ostream& out, + Node n, + bool doFull) const override; + /** Print get-unsat-assumptions command */ void toStreamCmdGetUnsatAssumptions(std::ostream& out) const override; diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 419b925c4..c2aa1c5f9 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1168,8 +1168,8 @@ void DeclareFunctionCommand::toStream(std::ostream& out, size_t dag, Language language) const { - Printer::getPrinter(language)->toStreamCmdDeclareFunction(out, - termToNode(d_func)); + Printer::getPrinter(language)->toStreamCmdDeclareFunction( + out, d_symbol, sortToTypeNode(d_func.getSort())); } /* -------------------------------------------------------------------------- */ @@ -2221,7 +2221,7 @@ void GetQuantifierEliminationCommand::toStream(std::ostream& out, Language language) const { Printer::getPrinter(language)->toStreamCmdGetQuantifierElimination( - out, termToNode(d_term)); + out, termToNode(d_term), d_doFull); } /* -------------------------------------------------------------------------- */ -- 2.30.2