From d6fac5f28f99464dc04d8fb604ce16e56342300e Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sun, 24 Jan 2021 12:12:10 -0600 Subject: [PATCH] (proof-new) Instantiation list utility (#5768) This is in preparation for refactoring the printing of instantiations. We will migrate the printing of instantiations (currently done in the Instantiate module within quantifiers engine) to somewhere more high level e.g. the SmtEngine or in the command layer. This will make the infrastructure for dumping instantiations much more flexible, as implemented on proof-new. --- src/CMakeLists.txt | 6 +- src/printer/printer.cpp | 28 +++++++++ src/printer/printer.h | 9 ++- src/theory/quantifiers/instantiation_list.cpp | 34 +++++++++++ src/theory/quantifiers/instantiation_list.h | 58 +++++++++++++++++++ 5 files changed, 132 insertions(+), 3 deletions(-) create mode 100644 src/theory/quantifiers/instantiation_list.cpp create mode 100644 src/theory/quantifiers/instantiation_list.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index dd944f929..632adae1e 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -694,10 +694,10 @@ libcvc4_add_sources( theory/quantifiers/inst_match_trie.h theory/quantifiers/inst_strategy_enumerative.cpp theory/quantifiers/inst_strategy_enumerative.h - theory/quantifiers/sygus_inst.cpp - theory/quantifiers/sygus_inst.h theory/quantifiers/instantiate.cpp theory/quantifiers/instantiate.h + theory/quantifiers/instantiation_list.cpp + theory/quantifiers/instantiation_list.h theory/quantifiers/lazy_trie.cpp theory/quantifiers/lazy_trie.h theory/quantifiers/proof_checker.cpp @@ -808,6 +808,8 @@ libcvc4_add_sources( theory/quantifiers/sygus/type_node_id_trie.h theory/quantifiers/sygus/transition_inference.cpp theory/quantifiers/sygus/transition_inference.h + theory/quantifiers/sygus_inst.cpp + theory/quantifiers/sygus_inst.h theory/quantifiers/sygus_sampler.cpp theory/quantifiers/sygus_sampler.h theory/quantifiers/term_database.cpp diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index be43a07cf..4e464f829 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -26,6 +26,7 @@ #include "proof/unsat_core.h" #include "smt/command.h" #include "smt/node_command.h" +#include "theory/quantifiers/instantiation_list.h" using namespace std; @@ -110,6 +111,33 @@ void Printer::toStream(std::ostream& out, const UnsatCore& core) const } }/* Printer::toStream(UnsatCore) */ +void Printer::toStream(std::ostream& out, const InstantiationList& is) const +{ + out << "(instantiations " << is.d_quant << std::endl; + for (const std::vector& i : is.d_inst) + { + out << " ( "; + for (const Node& n : i) + { + out << n << " "; + } + out << ")" << std::endl; + } + out << ")" << std::endl; +} + +void Printer::toStream(std::ostream& out, const SkolemList& sks) const +{ + out << "(skolem " << sks.d_quant << std::endl; + out << " ( "; + for (const Node& n : sks.d_sks) + { + out << n << " "; + } + out << ")" << std::endl; + out << ")" << std::endl; +} + Printer* Printer::getPrinter(OutputLanguage lang) { if(lang == language::output::LANG_AUTO) { diff --git a/src/printer/printer.h b/src/printer/printer.h index 3c53e34e6..835dbe798 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -32,8 +32,9 @@ namespace CVC4 { class Command; class CommandStatus; -class NodeCommand; class UnsatCore; +class InstantiationList; +class SkolemList; class Printer { @@ -62,6 +63,12 @@ class Printer /** Write an UnsatCore out to a stream with this Printer. */ virtual void toStream(std::ostream& out, const UnsatCore& core) const; + /** Write an instantiation list out to a stream with this Printer. */ + virtual void toStream(std::ostream& out, const InstantiationList& is) const; + + /** Write a skolem list out to a stream with this Printer. */ + virtual void toStream(std::ostream& out, const SkolemList& sks) const; + /** Print empty command */ virtual void toStreamCmdEmpty(std::ostream& out, const std::string& name) const; diff --git a/src/theory/quantifiers/instantiation_list.cpp b/src/theory/quantifiers/instantiation_list.cpp new file mode 100644 index 000000000..4bf17ebc2 --- /dev/null +++ b/src/theory/quantifiers/instantiation_list.cpp @@ -0,0 +1,34 @@ +/********************* */ +/*! \file instantiation_list.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 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.\endverbatim + ** + ** \brief list of instantiations + **/ + +#include "theory/quantifiers/instantiation_list.h" + +#include "options/base_options.h" +#include "printer/printer.h" + +namespace CVC4 { + +std::ostream& operator<<(std::ostream& out, const InstantiationList& ilist) +{ + Printer::getPrinter(options::outputLanguage())->toStream(out, ilist); + return out; +} + +std::ostream& operator<<(std::ostream& out, const SkolemList& skl) +{ + Printer::getPrinter(options::outputLanguage())->toStream(out, skl); + return out; +} + +} // namespace CVC4 diff --git a/src/theory/quantifiers/instantiation_list.h b/src/theory/quantifiers/instantiation_list.h new file mode 100644 index 000000000..6ef8e4784 --- /dev/null +++ b/src/theory/quantifiers/instantiation_list.h @@ -0,0 +1,58 @@ +/********************* */ +/*! \file instantiation_list.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 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.\endverbatim + ** + ** \brief list of instantiations + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__QUANTIFIERS__INSTANTIATION_LIST_H +#define CVC4__THEORY__QUANTIFIERS__INSTANTIATION_LIST_H + +#include +#include + +#include "expr/node.h" + +namespace CVC4 { + +/** A list of instantiations for a quantified formula */ +struct InstantiationList +{ + InstantiationList(Node q, const std::vector >& inst) + : d_quant(q), d_inst(inst) + { + } + /** The quantified formula */ + Node d_quant; + /** The instantiation list */ + std::vector > d_inst; +}; + +/** Print the instantiation list to stream out */ +std::ostream& operator<<(std::ostream& out, const InstantiationList& ilist); + +/** The list of skolemization for a quantified formula */ +struct SkolemList +{ + SkolemList(Node q, const std::vector& sks) : d_quant(q), d_sks(sks) {} + /** The quantified formula */ + Node d_quant; + /** The list of skolems for the quantified formula */ + std::vector d_sks; +}; + +/** Print the skolem list to stream out */ +std::ostream& operator<<(std::ostream& out, const SkolemList& skl); + +} // namespace CVC4 + +#endif /* CVC4__THEORY__QUANTIFIERS__INSTANTIATION_LIST_H */ -- 2.30.2