--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved. See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Print benchmark utility.
+ */
+
+#include "smt/print_benchmark.h"
+
+#include "expr/dtype.h"
+#include "expr/node_algorithm.h"
+#include "printer/printer.h"
+
+using namespace cvc5::kind;
+
+namespace cvc5 {
+namespace smt {
+
+void PrintBenchmark::printAssertions(std::ostream& out,
+ const std::vector<Node>& defs,
+ const std::vector<Node>& assertions)
+{
+ std::unordered_set<TypeNode> types;
+ std::unordered_set<TNode> typeVisited;
+ for (const Node& a : defs)
+ {
+ expr::getTypes(a, types, typeVisited);
+ }
+ for (const Node& a : assertions)
+ {
+ expr::getTypes(a, types, typeVisited);
+ }
+ // print the declared types first
+ std::unordered_set<TypeNode> alreadyPrintedDeclSorts;
+ for (const TypeNode& st : types)
+ {
+ // note that we must get all "component types" of a type, so that
+ // e.g. U is printed as a sort declaration when we have type (Array U Int).
+ std::unordered_set<TypeNode> ctypes;
+ expr::getComponentTypes(st, ctypes);
+ for (const TypeNode& stc : ctypes)
+ {
+ // get all connected datatypes to this one
+ std::vector<TypeNode> connectedTypes;
+ getConnectedSubfieldTypes(stc, connectedTypes, alreadyPrintedDeclSorts);
+ // now, separate into sorts and datatypes
+ std::vector<TypeNode> datatypeBlock;
+ for (const TypeNode& ctn : connectedTypes)
+ {
+ if (stc.isSort())
+ {
+ d_printer->toStreamCmdDeclareType(out, stc);
+ }
+ else if (stc.isDatatype())
+ {
+ datatypeBlock.push_back(ctn);
+ }
+ }
+ // print the mutually recursive datatype block if necessary
+ if (!datatypeBlock.empty())
+ {
+ d_printer->toStreamCmdDatatypeDeclaration(out, datatypeBlock);
+ }
+ }
+ }
+
+ // global visited cache for expr::getSymbols calls
+ std::unordered_set<TNode> visited;
+
+ // print the definitions
+ std::unordered_map<Node, std::pair<bool, Node>> defMap;
+ std::vector<Node> defSyms;
+ // first, record all the defined symbols
+ for (const Node& a : defs)
+ {
+ bool isRec;
+ Node defSym;
+ Node defBody;
+ decomposeDefinition(a, isRec, defSym, defBody);
+ if (!defSym.isNull())
+ {
+ Assert(defMap.find(defSym) == defMap.end());
+ defMap[defSym] = std::pair<bool, Node>(isRec, defBody);
+ defSyms.push_back(defSym);
+ }
+ }
+ // go back and print the definitions
+ std::unordered_set<Node> alreadyPrintedDecl;
+ std::unordered_set<Node> alreadyPrintedDef;
+
+ std::unordered_map<Node, std::pair<bool, Node>>::const_iterator itd;
+ for (const Node& s : defSyms)
+ {
+ std::vector<Node> recDefs;
+ std::vector<Node> ordinaryDefs;
+ std::unordered_set<Node> syms;
+ getConnectedDefinitions(
+ s, recDefs, ordinaryDefs, syms, defMap, alreadyPrintedDef, visited);
+ // print the declarations that are encountered for the first time in this
+ // block
+ printDeclaredFuns(out, syms, alreadyPrintedDecl);
+ // print the ordinary definitions
+ for (const Node& f : ordinaryDefs)
+ {
+ itd = defMap.find(f);
+ Assert(itd != defMap.end());
+ Assert(!itd->second.first);
+ d_printer->toStreamCmdDefineFunction(out, f, itd->second.second);
+ // a definition is also a declaration
+ alreadyPrintedDecl.insert(f);
+ }
+ // print a recursive function definition block
+ if (!recDefs.empty())
+ {
+ std::vector<Node> lambdas;
+ for (const Node& f : recDefs)
+ {
+ lambdas.push_back(defMap[f].second);
+ // a recursive definition is also a declaration
+ alreadyPrintedDecl.insert(f);
+ }
+ d_printer->toStreamCmdDefineFunctionRec(out, recDefs, lambdas);
+ }
+ }
+
+ // print the remaining declared symbols
+ std::unordered_set<Node> syms;
+ for (const Node& a : assertions)
+ {
+ expr::getSymbols(a, syms, visited);
+ }
+ printDeclaredFuns(out, syms, alreadyPrintedDecl);
+
+ // print the assertions
+ for (const Node& a : assertions)
+ {
+ d_printer->toStreamCmdAssert(out, a);
+ }
+}
+void PrintBenchmark::printAssertions(std::ostream& out,
+ const std::vector<Node>& assertions)
+{
+ std::vector<Node> defs;
+ printAssertions(out, defs, assertions);
+}
+
+void PrintBenchmark::printDeclaredFuns(std::ostream& out,
+ const std::unordered_set<Node>& funs,
+ std::unordered_set<Node>& alreadyPrinted)
+{
+ for (const Node& f : funs)
+ {
+ Assert(f.isVar());
+ if (alreadyPrinted.find(f) == alreadyPrinted.end())
+ {
+ d_printer->toStreamCmdDeclareFunction(out, f);
+ }
+ }
+ alreadyPrinted.insert(funs.begin(), funs.end());
+}
+
+void PrintBenchmark::getConnectedSubfieldTypes(
+ TypeNode tn,
+ std::vector<TypeNode>& connectedTypes,
+ std::unordered_set<TypeNode>& processed)
+{
+ if (processed.find(tn) != processed.end())
+ {
+ return;
+ }
+ processed.insert(tn);
+ if (tn.isSort())
+ {
+ connectedTypes.push_back(tn);
+ }
+ else if (tn.isDatatype())
+ {
+ connectedTypes.push_back(tn);
+ std::unordered_set<TypeNode> subfieldTypes =
+ tn.getDType().getSubfieldTypes();
+ for (const TypeNode& ctn : subfieldTypes)
+ {
+ getConnectedSubfieldTypes(ctn, connectedTypes, processed);
+ }
+ }
+}
+
+void PrintBenchmark::getConnectedDefinitions(
+ Node n,
+ std::vector<Node>& recDefs,
+ std::vector<Node>& ordinaryDefs,
+ std::unordered_set<Node>& syms,
+ const std::unordered_map<Node, std::pair<bool, Node>>& defMap,
+ std::unordered_set<Node>& processedDefs,
+ std::unordered_set<TNode>& visited)
+{
+ // does it have a definition?
+ std::unordered_map<Node, std::pair<bool, Node>>::const_iterator it =
+ defMap.find(n);
+ if (it == defMap.end())
+ {
+ // an ordinary declared symbol
+ syms.insert(n);
+ return;
+ }
+ if (processedDefs.find(n) != processedDefs.end())
+ {
+ return;
+ }
+ processedDefs.insert(n);
+ if (!it->second.first)
+ {
+ // an ordinary define-fun symbol
+ ordinaryDefs.push_back(n);
+ }
+ else
+ {
+ // a recursively defined symbol
+ recDefs.push_back(n);
+ // get the symbols in the body
+ std::unordered_set<Node> symsBody;
+ expr::getSymbols(it->second.second, symsBody, visited);
+ for (const Node& s : symsBody)
+ {
+ getConnectedDefinitions(
+ s, recDefs, ordinaryDefs, syms, defMap, processedDefs, visited);
+ }
+ }
+}
+
+bool PrintBenchmark::decomposeDefinition(Node a,
+ bool& isRecDef,
+ Node& sym,
+ Node& body)
+{
+ if (a.getKind() == EQUAL && a[0].isVar())
+ {
+ // an ordinary define-fun
+ isRecDef = false;
+ sym = a[0];
+ body = a[1];
+ return true;
+ }
+ else if (a.getKind() == FORALL && a[1].getKind() == EQUAL
+ && a[1][0].getKind() == APPLY_UF)
+ {
+ isRecDef = true;
+ sym = a[1][0].getOperator();
+ body = NodeManager::currentNM()->mkNode(LAMBDA, a[0], a[1][1]);
+ return true;
+ }
+ else
+ {
+ Warning() << "Unhandled definition: " << a << std::endl;
+ }
+ return false;
+}
+
+void PrintBenchmark::printBenchmark(std::ostream& out,
+ const std::string& logic,
+ const std::vector<Node>& defs,
+ const std::vector<Node>& assertions)
+{
+ d_printer->toStreamCmdSetBenchmarkLogic(out, logic);
+ printAssertions(out, defs, assertions);
+ d_printer->toStreamCmdCheckSat(out);
+}
+
+} // namespace smt
+} // namespace cvc5
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved. See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Print benchmark utility.
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__SMT__PRINT_BENCHMARK_H
+#define CVC5__SMT__PRINT_BENCHMARK_H
+
+#include <iosfwd>
+#include <vector>
+
+#include "expr/node.h"
+
+namespace cvc5 {
+
+class Printer;
+
+namespace smt {
+
+/**
+ * A utility for printing a benchmark. This utility requires no bookkeeping
+ * about which commands have been executed. It reconstructs the set of
+ * commands that would have been required for generating a benchmark based on
+ * a list of nodes.
+ */
+class PrintBenchmark
+{
+ public:
+ PrintBenchmark(const Printer* p) : d_printer(p) {}
+ /**
+ * Print assertions. This prints a parsable set of commands on the output
+ * stream out that defines (recursive) functions in defs, and asserts
+ * assertions. It does not print a set-logic or check-sat command.
+ *
+ * Each node in defs is either of the form:
+ * (1) (= s t), where s is a (non-recursively) defined function, where
+ * the term t may be a lambda if s has non-zero arity.
+ * (2) (forall V (= (s V) t)), where s is a recursively defined function.
+ */
+ void printAssertions(std::ostream& out,
+ const std::vector<Node>& defs,
+ const std::vector<Node>& assertions);
+ /**
+ * Print assertions, without special handling of defined functions.
+ */
+ void printAssertions(std::ostream& out, const std::vector<Node>& assertions);
+
+ /**
+ * Print benchmark, which prints a parsable benchmark on the output stream
+ * out. It relies on the printAssertions method above, as well as printing
+ * the logic based on given string and a final check-sat command.
+ *
+ * For the best printing, defs should be given in the order in which
+ * the symbols were declared. If this is not the case, then we may e.g.
+ * group blocks of definitions that were not grouped in the input.
+ */
+ void printBenchmark(std::ostream& out,
+ const std::string& logic,
+ const std::vector<Node>& defs,
+ const std::vector<Node>& assertions);
+
+ private:
+ /**
+ * print declared symbols in funs but not processed; updates processed to
+ * include what was printed
+ */
+ void printDeclaredFuns(std::ostream& out,
+ const std::unordered_set<Node>& funs,
+ std::unordered_set<Node>& processed);
+ /**
+ * Get the connected types. This traverses subfield types of datatypes and
+ * adds to connectedTypes everything that is necessary for printing tn.
+ *
+ * @param tn The type to traverse
+ * @param connectedTypes The types that tn depends on
+ * @param process The types we have already processed. We update this set
+ * with those added to connectedTypes.
+ */
+ void getConnectedSubfieldTypes(TypeNode tn,
+ std::vector<TypeNode>& connectedTypes,
+ std::unordered_set<TypeNode>& processed);
+ /**
+ * Get connected definitions for symbol v.
+ *
+ * @param recDefs The recursive function definitions that v depends on
+ * @param ordinaryDefs The non-recursive definitions that v depends on
+ * @param syms The declared symbols that v depends on
+ * @param defMap Map from symbols to their definitions
+ * @param processedDefs The (recursive or non-recursive) definitions we have
+ * processed already. We update this with symbols we add to recDefs and
+ * ordinaryDefs.
+ * @param visited The set of terms we have already visited when searching for
+ * free symbols. This set is updated for the bodies of definitions processed
+ * in this call.
+ */
+ void getConnectedDefinitions(
+ Node v,
+ std::vector<Node>& recDefs,
+ std::vector<Node>& ordinaryDefs,
+ std::unordered_set<Node>& syms,
+ const std::unordered_map<Node, std::pair<bool, Node>>& defMap,
+ std::unordered_set<Node>& processedDefs,
+ std::unordered_set<TNode>& visited);
+ /**
+ * Decompose definition assertion a.
+ *
+ * @param a The definition assertion
+ * @param isRecDef Updated to true if a is a recursive function definition (a
+ * quantified formula)
+ * @param sym Updated to the symbol that a defines
+ * @param body Update to the term that defines sym
+ * @return true if the definition was successfully inferred
+ */
+ bool decomposeDefinition(Node a, bool& isRecDef, Node& sym, Node& body);
+ /**
+ * Pointer to the printer we are using, which is responsible for printing
+ * individual commands.
+ */
+ const Printer* d_printer;
+};
+
+} // namespace smt
+} // namespace cvc5
+
+#endif /* CVC5__SMT__PRINT_BENCHMARK_H */
projects / cvc5.git / commitdiff