From 8de233dec2e33951e0fcc294af6c835bfc7cb701 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 11 Apr 2022 16:06:10 -0500 Subject: [PATCH] Add oracle engine to quantifiers engine (#8589) This class is the subsolver of quantifiers engine for handling oracles in SMTO. The implementation of this class will be added in followup PRs. It also contains a utility method for constructing oracle interfaces. --- src/CMakeLists.txt | 2 + src/options/quantifiers_options.toml | 8 ++ src/theory/quantifiers/oracle_engine.cpp | 136 ++++++++++++++++++ src/theory/quantifiers/oracle_engine.h | 101 +++++++++++++ .../quantifiers/quantifiers_modules.cpp | 5 + src/theory/quantifiers/quantifiers_modules.h | 3 + src/theory/quantifiers_engine.cpp | 19 +++ src/theory/quantifiers_engine.h | 4 + 8 files changed, 278 insertions(+) create mode 100644 src/theory/quantifiers/oracle_engine.cpp create mode 100644 src/theory/quantifiers/oracle_engine.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 60627c4e8..d9d185480 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -827,6 +827,8 @@ libcvc5_add_sources( theory/quantifiers/lazy_trie.h theory/quantifiers/master_eq_notify.cpp theory/quantifiers/master_eq_notify.h + theory/quantifiers/oracle_engine.cpp + theory/quantifiers/oracle_engine.h theory/quantifiers/proof_checker.cpp theory/quantifiers/proof_checker.h theory/quantifiers/quant_bound_inference.cpp diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 199445117..bbd26f702 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -559,6 +559,14 @@ name = "Quantifiers" default = "true" help = "pool-based instantiation: instantiate with ground terms occurring in user-specified pools" +[[option]] + name = "oracles" + category = "expert" + long = "oracles" + type = "bool" + default = "false" + help = "Enable interface to external oracles" + ### Finite model finding options [[option]] diff --git a/src/theory/quantifiers/oracle_engine.cpp b/src/theory/quantifiers/oracle_engine.cpp new file mode 100644 index 000000000..19cec1de5 --- /dev/null +++ b/src/theory/quantifiers/oracle_engine.cpp @@ -0,0 +1,136 @@ +/****************************************************************************** + * 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 engine + */ + +#include "theory/quantifiers/oracle_engine.h" + +#include "expr/attribute.h" +#include "expr/skolem_manager.h" +#include "options/quantifiers_options.h" +#include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers/quantifiers_inference_manager.h" +#include "theory/quantifiers/quantifiers_registry.h" +#include "theory/quantifiers/term_registry.h" +#include "theory/quantifiers/term_tuple_enumerator.h" + +using namespace cvc5::internal::kind; +using namespace cvc5::context; + +namespace cvc5::internal { +namespace theory { +namespace quantifiers { + +/** Attribute true for input variables */ +struct OracleInputVarAttributeId +{ +}; +typedef expr::Attribute + OracleInputVarAttribute; +/** Attribute true for output variables */ +struct OracleOutputVarAttributeId +{ +}; +typedef expr::Attribute + OracleOutputVarAttribute; + +OracleEngine::OracleEngine(Env& env, + QuantifiersState& qs, + QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr, + TermRegistry& tr) + : QuantifiersModule(env, qs, qim, qr, tr), d_oracleFuns(userContext()) +{ +} + +void OracleEngine::presolve() {} + +bool OracleEngine::needsCheck(Theory::Effort e) +{ + return e == Theory::Effort::EFFORT_LAST_CALL; +} + +// the model is built at this effort level +OracleEngine::QEffort OracleEngine::needsModel(Theory::Effort e) +{ + return QEFFORT_MODEL; +} + +void OracleEngine::reset_round(Theory::Effort e) {} + +void OracleEngine::registerQuantifier(Node q) {} + +void OracleEngine::check(Theory::Effort e, QEffort quant_e) {} + +bool OracleEngine::checkCompleteFor(Node q) { return false; } + +void OracleEngine::checkOwnership(Node q) {} + +std::string OracleEngine::identify() const +{ + return std::string("OracleEngine"); +} + +void OracleEngine::declareOracleFun(Node f, const std::string& binName) +{ + OracleInterfaceAttribute oia; + f.setAttribute(oia, binName); + d_oracleFuns.push_back(f); +} + +std::vector OracleEngine::getOracleFuns() const +{ + std::vector ofuns; + for (const Node& f : d_oracleFuns) + { + ofuns.push_back(f); + } + return ofuns; +} + +Node OracleEngine::mkOracleInterface(const std::vector& inputs, + const std::vector& outputs, + Node assume, + Node constraint, + const std::string& binName) +{ + Assert(!assume.isNull()); + Assert(!constraint.isNull()); + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); + OracleInterfaceAttribute oia; + Node oiVar = sm->mkDummySkolem("oracle-interface", nm->booleanType()); + oiVar.setAttribute(oia, binName); + Node ipl = nm->mkNode(INST_PATTERN_LIST, nm->mkNode(INST_ATTRIBUTE, oiVar)); + std::vector vars; + OracleInputVarAttribute oiva; + for (Node v : inputs) + { + v.setAttribute(oiva, true); + vars.push_back(v); + } + OracleOutputVarAttribute oova; + for (Node v : outputs) + { + v.setAttribute(oova, true); + vars.push_back(v); + } + Node bvl = nm->mkNode(BOUND_VAR_LIST, vars); + Node body = nm->mkNode(ORACLE_FORMULA_GEN, assume, constraint); + return nm->mkNode(FORALL, bvl, body, ipl); +} + +} // namespace quantifiers +} // namespace theory +} // namespace cvc5::internal diff --git a/src/theory/quantifiers/oracle_engine.h b/src/theory/quantifiers/oracle_engine.h new file mode 100644 index 000000000..7b12e29e1 --- /dev/null +++ b/src/theory/quantifiers/oracle_engine.h @@ -0,0 +1,101 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Elizabeth Polgreen + * + * 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 engine for SMTO + */ + +#include "cvc5_private.h" + +#ifndef CVC5__THEORY__QUANTIFIERS__ORACLE_ENGINE_H +#define CVC5__THEORY__QUANTIFIERS__ORACLE_ENGINE_H + +#include "theory/quantifiers/quant_module.h" + +namespace cvc5::internal { +namespace theory { +namespace quantifiers { + +/** + * Oracle engine + * + * This class manages the list of declared oracle functions and asserted + * oracle interfaces. + * + * For SMT modulo oracles (SMTO) queries, this class is responsible for + * invoking oracles, as specified by oracle interface quantifiers (see + * OracleInterfaceAttribute), until all oracle functions have consistent + * definitions with respect to the current model. + * + * In detail, an oracle function f has a consistent definition with respect to + * the current model M if all invocations f(t) in assertions are such that + * we have invoked its associated oracle on t^M and that invocation returned + * the value f(t)^M. This module is complete for oracle interface quantifiers + * if their associated oracle function has a consistent definition. + * + * For details, see Polgreen et al VMCAI 2022. + */ +class OracleEngine : public QuantifiersModule +{ + public: + OracleEngine(Env& env, + QuantifiersState& qs, + QuantifiersInferenceManager& qim, + QuantifiersRegistry& qr, + TermRegistry& tr); + ~OracleEngine() {} + /** Presolve */ + void presolve() override; + /** Needs check. */ + bool needsCheck(Theory::Effort e) override; + /** Needs model. */ + QEffort needsModel(Theory::Effort e) override; + /** Reset round. */ + void reset_round(Theory::Effort e) override; + /** Register quantified formula q */ + void registerQuantifier(Node q) override; + /** Check. + * Adds instantiations for all currently asserted + * quantified formulas via calls to process(...) + */ + void check(Theory::Effort e, QEffort quant_e) override; + /** + * Check was complete for quantified formula q, return true if we can say + * "sat" provided that q is currently asserted. + */ + bool checkCompleteFor(Node q) override; + /** check ownership */ + void checkOwnership(Node q) override; + /** Identify. */ + std::string identify() const override; + + /** Declare oracle fun */ + void declareOracleFun(Node f, const std::string& binName); + /** Get the list of all declared oracle functions */ + std::vector getOracleFuns() const; + + /** Make an oracle interface quantifier */ + static Node mkOracleInterface(const std::vector& inputs, + const std::vector& outputs, + Node assume, + Node constraint, + const std::string& binName); + + private: + /** The oracle functions (user-context dependent) */ + context::CDList d_oracleFuns; +}; + +} // namespace quantifiers +} // namespace theory +} // namespace cvc5::internal + +#endif diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp index b6ba86201..243218214 100644 --- a/src/theory/quantifiers/quantifiers_modules.cpp +++ b/src/theory/quantifiers/quantifiers_modules.cpp @@ -117,6 +117,11 @@ void QuantifiersModules::initialize(Env& env, d_sygus_inst.reset(new SygusInst(env, qs, qim, qr, tr)); modules.push_back(d_sygus_inst.get()); } + if (options.quantifiers.oracles) + { + d_oracleEngine.reset(new OracleEngine(env, qs, qim, qr, tr)); + modules.push_back(d_oracleEngine.get()); + } } } // namespace quantifiers diff --git a/src/theory/quantifiers/quantifiers_modules.h b/src/theory/quantifiers/quantifiers_modules.h index c0105359c..599aaece1 100644 --- a/src/theory/quantifiers/quantifiers_modules.h +++ b/src/theory/quantifiers/quantifiers_modules.h @@ -27,6 +27,7 @@ #include "theory/quantifiers/fmf/model_engine.h" #include "theory/quantifiers/inst_strategy_enumerative.h" #include "theory/quantifiers/inst_strategy_pool.h" +#include "theory/quantifiers/oracle_engine.h" #include "theory/quantifiers/quant_conflict_find.h" #include "theory/quantifiers/quant_split.h" #include "theory/quantifiers/sygus/synth_engine.h" @@ -94,6 +95,8 @@ class QuantifiersModules std::unique_ptr d_qsplit; /** SyGuS instantiation engine */ std::unique_ptr d_sygus_inst; + /** Oracle engine */ + std::unique_ptr d_oracleEngine; }; } // namespace quantifiers diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 2e9eb1210..0eaea7fe7 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -702,5 +702,24 @@ void QuantifiersEngine::declarePool(Node p, const std::vector& initValue) d_treg.declarePool(p, initValue); } +void QuantifiersEngine::declareOracleFun(Node f, const std::string& binName) +{ + if (d_qmodules->d_oracleEngine.get() == nullptr) + { + warning() << "Cannot declare oracle function when oracles are disabled" + << std::endl; + return; + } + d_qmodules->d_oracleEngine->declareOracleFun(f, binName); +} +std::vector QuantifiersEngine::getOracleFuns() const +{ + if (d_qmodules->d_oracleEngine.get() == nullptr) + { + return {}; + } + return d_qmodules->d_oracleEngine->getOracleFuns(); +} + } // namespace theory } // namespace cvc5::internal diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 7574f77ae..9da371430 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -145,6 +145,10 @@ class QuantifiersEngine : protected EnvObj bool getSynthSolutions(std::map >& sol_map); /** Declare pool */ void declarePool(Node p, const std::vector& initValue); + /** Declare oracle fun */ + void declareOracleFun(Node f, const std::string& binName); + /** Get the list of all declared oracle functions */ + std::vector getOracleFuns() const; //----------end user interface for instantiations private: //---------------------- private initialization -- 2.30.2