From: Andrew Reynolds Date: Wed, 4 May 2022 00:15:30 +0000 (-0500) Subject: Add support for oracle constant nodes (#8707) X-Git-Tag: cvc5-1.0.1~178 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7fa4709c891bcdf5aa1d3ed4b001d0628bbc17be;p=cvc5.git Add support for oracle constant nodes (#8707) This is the beginning of a refactoring to make std::function the basis for oracles internally, not binary names. --- diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index f48536537..a72a4998a 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -60,6 +60,7 @@ libcvc5_add_sources( node_traversal.h node_value.cpp node_value.h + oracle.h oracle_caller.cpp oracle_caller.h sequence.cpp diff --git a/src/expr/node_manager_attributes.h b/src/expr/node_manager_attributes.h index 25043f146..af3d3e181 100644 --- a/src/expr/node_manager_attributes.h +++ b/src/expr/node_manager_attributes.h @@ -39,6 +39,9 @@ namespace attr { struct DatatypeIndexTag { }; + struct OracleIndexTag + { + }; } // namespace attr typedef Attribute VarNameAttr; @@ -57,5 +60,9 @@ using TupleDatatypeAttr = /** Mapping datatype types to the index of their datatype in node manager */ using DatatypeIndexAttr = Attribute; +/** Mapping oracle constant nodes to the index of their oracle in the node + * manager */ +using OracleIndexAttr = expr::Attribute; + } // namespace expr } // namespace cvc5::internal diff --git a/src/expr/node_manager_template.cpp b/src/expr/node_manager_template.cpp index 0a7ef904a..419cf5055 100644 --- a/src/expr/node_manager_template.cpp +++ b/src/expr/node_manager_template.cpp @@ -26,6 +26,7 @@ #include "expr/metakind.h" #include "expr/node_manager.h" #include "expr/node_manager_attributes.h" +#include "expr/oracle.h" #include "expr/skolem_manager.h" #include "expr/type_checker.h" #include "expr/type_properties.h" @@ -248,8 +249,9 @@ NodeManager::~NodeManager() d_rt_cache.d_children.clear(); d_rt_cache.d_data = dummy; - // clear the datatypes + // clear the datatypes and oracles d_dtypes.clear(); + d_oracles.clear(); Assert(!d_attrManager->inGarbageCollection()); @@ -950,6 +952,25 @@ TypeNode NodeManager::mkUnresolvedDatatypeSort(const std::string& name, return usort; } +Node NodeManager::mkOracle(Oracle& o) +{ + Node n = NodeBuilder(this, kind::ORACLE); + n.setAttribute(TypeAttr(), builtinOperatorType()); + n.setAttribute(TypeCheckedAttr(), true); + n.setAttribute(OracleIndexAttr(), d_oracles.size()); + // we allocate a new oracle, to take ownership + d_oracles.push_back(std::unique_ptr(new Oracle(o.getFunction()))); + return n; +} + +const Oracle& NodeManager::getOracleFor(const Node& n) const +{ + Assert(n.getKind() == kind::ORACLE); + size_t index = n.getAttribute(OracleIndexAttr()); + Assert(index < d_oracles.size()); + return *d_oracles[index]; +} + Node NodeManager::mkVar(const std::string& name, const TypeNode& type) { Node n = NodeBuilder(this, kind::VARIABLE); diff --git a/src/expr/node_manager_template.h b/src/expr/node_manager_template.h index 0ad5005ec..513742383 100644 --- a/src/expr/node_manager_template.h +++ b/src/expr/node_manager_template.h @@ -45,6 +45,7 @@ class SkolemManager; class BoundVarManager; class DType; +class Oracle; class Rational; namespace expr { @@ -741,6 +742,18 @@ class NodeManager /** Make an unresolved datatype sort */ TypeNode mkUnresolvedDatatypeSort(const std::string& name, size_t arity = 0); + /** + * Make an oracle node. This returns a constant of kind ORACLE that stores + * the given method in an Oracle object. This Oracle can later be obtained by + * getOracleFor below. + */ + Node mkOracle(Oracle& o); + + /** + * Get the oracle for an oracle node n, which should have kind ORACLE. + */ + const Oracle& getOracleFor(const Node& n) const; + private: /** * Make a set of types representing the given datatypes, which may @@ -1034,6 +1047,9 @@ class NodeManager /** A list of datatypes owned by this node manager */ std::vector> d_dtypes; + /** A list of oracles owned by this node manager */ + std::vector> d_oracles; + TupleTypeCache d_tt_cache; RecTypeCache d_rt_cache; }; /* class NodeManager */ diff --git a/src/expr/oracle.h b/src/expr/oracle.h new file mode 100644 index 000000000..90fe2ff63 --- /dev/null +++ b/src/expr/oracle.h @@ -0,0 +1,59 @@ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Oracle caller + */ + +#include "cvc5_private.h" + +#ifndef CVC5__EXPR__ORACLE_H +#define CVC5__EXPR__ORACLE_H + +#include + +#include "expr/node.h" + +namespace cvc5::internal { + +/** + * An oracle, which stores a function whose interface is from a vector of nodes + * to a vector of nodes. It is expected to serve as an oracle interface as + * described in Polgreen et al VMCAI 2022 and the SyGuS version 2.1 standard. + */ +class Oracle +{ + public: + /** Construct an oracle whose implementation is the given function. */ + Oracle(std::function(const std::vector&)> fn) + : d_fn(fn) + { + } + ~Oracle() {} + /** Run the function on the given input */ + std::vector run(const std::vector& input) const + { + return d_fn(input); + } + /** Get the function for this oracle */ + std::function(const std::vector&)> getFunction() const + { + return d_fn; + } + + private: + /** The function for this oracle */ + std::function(const std::vector&)> d_fn; +}; + +} // namespace cvc5::internal + +#endif /*CVC5__EXPR__ORACLE_H*/ diff --git a/src/theory/quantifiers/kinds b/src/theory/quantifiers/kinds index 481499f2e..7c1b9fe0f 100644 --- a/src/theory/quantifiers/kinds +++ b/src/theory/quantifiers/kinds @@ -17,6 +17,8 @@ operator EXISTS 2:3 "existentially quantified formula; first parameter is an BOU variable INST_CONSTANT "instantiation constant" +variable ORACLE "oracle" + sort BOUND_VAR_LIST_TYPE \ Cardinality::INTEGERS \ not-well-founded \