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.
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
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]]
--- /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.
+ * ****************************************************************************
+ *
+ * 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<OracleInputVarAttributeId, bool>
+ OracleInputVarAttribute;
+/** Attribute true for output variables */
+struct OracleOutputVarAttributeId
+{
+};
+typedef expr::Attribute<OracleOutputVarAttributeId, bool>
+ 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<Node> OracleEngine::getOracleFuns() const
+{
+ std::vector<Node> ofuns;
+ for (const Node& f : d_oracleFuns)
+ {
+ ofuns.push_back(f);
+ }
+ return ofuns;
+}
+
+Node OracleEngine::mkOracleInterface(const std::vector<Node>& inputs,
+ const std::vector<Node>& 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<Node> 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
--- /dev/null
+/******************************************************************************
+ * 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<Node> getOracleFuns() const;
+
+ /** Make an oracle interface quantifier */
+ static Node mkOracleInterface(const std::vector<Node>& inputs,
+ const std::vector<Node>& outputs,
+ Node assume,
+ Node constraint,
+ const std::string& binName);
+
+ private:
+ /** The oracle functions (user-context dependent) */
+ context::CDList<Node> d_oracleFuns;
+};
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace cvc5::internal
+
+#endif
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
#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"
std::unique_ptr<QuantDSplit> d_qsplit;
/** SyGuS instantiation engine */
std::unique_ptr<SygusInst> d_sygus_inst;
+ /** Oracle engine */
+ std::unique_ptr<OracleEngine> d_oracleEngine;
};
} // namespace quantifiers
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<Node> QuantifiersEngine::getOracleFuns() const
+{
+ if (d_qmodules->d_oracleEngine.get() == nullptr)
+ {
+ return {};
+ }
+ return d_qmodules->d_oracleEngine->getOracleFuns();
+}
+
} // namespace theory
} // namespace cvc5::internal
bool getSynthSolutions(std::map<Node, std::map<Node, Node> >& sol_map);
/** Declare pool */
void declarePool(Node p, const std::vector<Node>& initValue);
+ /** Declare oracle fun */
+ void declareOracleFun(Node f, const std::string& binName);
+ /** Get the list of all declared oracle functions */
+ std::vector<Node> getOracleFuns() const;
//----------end user interface for instantiations
private:
//---------------------- private initialization
projects / cvc5.git / commitdiff