From: Andrew Reynolds Date: Tue, 12 Apr 2022 18:55:05 +0000 (-0500) Subject: Add oracle checker utility (#8603) X-Git-Tag: cvc5-1.0.1~270 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=571195c8c297192dc3134edf339af2faeaba79ff;p=cvc5.git Add oracle checker utility (#8603) This is a utility that allocates oracle callers for oracle functions on demand and can be used to convert a term containing oracle function symbols into its evaluated form. It will be used for both SMTO (for checking consistency of oracle interfaces) and SyMO (as part of refinement lemma evaluation in CEGIS). --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index d9d185480..eec6ba2b1 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_checker.cpp + theory/quantifiers/oracle_checker.h theory/quantifiers/oracle_engine.cpp theory/quantifiers/oracle_engine.h theory/quantifiers/proof_checker.cpp diff --git a/src/theory/quantifiers/oracle_checker.cpp b/src/theory/quantifiers/oracle_checker.cpp new file mode 100644 index 000000000..bc0c1e40a --- /dev/null +++ b/src/theory/quantifiers/oracle_checker.cpp @@ -0,0 +1,123 @@ +/****************************************************************************** + * 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 checker + */ + +#include "theory/quantifiers/oracle_checker.h" + +#include "expr/node_algorithm.h" +#include "options/base_options.h" +#include "smt/env.h" +#include "theory/rewriter.h" + +namespace cvc5::internal { +namespace theory { +namespace quantifiers { + +bool OracleChecker::checkConsistent(Node app, + Node val, + std::vector& lemmas) +{ + Node result = evaluateApp(app); + if (result != val) + { + lemmas.push_back(result.eqNode(app)); + return false; + } + return true; +} + +Node OracleChecker::evaluateApp(Node app) +{ + Assert(app.getKind() == kind::APPLY_UF); + Node f = app.getOperator(); + Assert(OracleCaller::isOracleFunction(f)); + // get oracle caller + if (d_callers.find(f) == d_callers.end()) + { + d_callers.insert(std::pair(f, OracleCaller(f))); + } + OracleCaller& caller = d_callers.at(f); + + // get oracle result + Node ret; + int runResult; + caller.callOracle(app, ret, runResult); + Assert(!ret.isNull()); + return ret; +} + +Node OracleChecker::evaluate(Node n) +{ + // same as convert + return convert(n); +} + +Node OracleChecker::postConvert(Node n) +{ + Trace("oracle-checker-debug") << "postConvert: " << n << std::endl; + // if it is an oracle function applied to constant arguments + if (n.getKind() == kind::APPLY_UF + && OracleCaller::isOracleFunction(n.getOperator())) + { + bool allConst = true; + for (const Node& nc : n) + { + if (nc.isConst()) + { + continue; + } + // special case: assume all closed lambdas are constants + if (nc.getKind() == kind::LAMBDA) + { + // if the lambda does not have a free variable (BOUND_VARIABLE) + if (!expr::hasFreeVar(nc)) + { + // it also cannot have any free symbol + std::unordered_set syms; + expr::getSymbols(nc, syms); + if (syms.empty()) + { + continue; + } + } + } + // non-constant argument, fail + allConst = false; + break; + } + if (allConst) + { + // evaluate the application + return evaluateApp(n); + } + } + // otherwise, always rewrite + return Rewriter::rewrite(n); +} +bool OracleChecker::hasOracles() const { return !d_callers.empty(); } +bool OracleChecker::hasOracleCalls(Node f) const +{ + std::map::const_iterator it = d_callers.find(f); + return it != d_callers.end(); +} +const std::map& OracleChecker::getOracleCalls(Node f) const +{ + Assert(hasOracleCalls(f)); + std::map::const_iterator it = d_callers.find(f); + return it->second.getCachedResults(); +} + +} // namespace quantifiers +} // namespace theory +} // namespace cvc5::internal diff --git a/src/theory/quantifiers/oracle_checker.h b/src/theory/quantifiers/oracle_checker.h new file mode 100644 index 000000000..7d46ffc6a --- /dev/null +++ b/src/theory/quantifiers/oracle_checker.h @@ -0,0 +1,98 @@ +/****************************************************************************** + * 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 checker, caches oracle caller objects + */ + +#include "cvc5_private.h" + +#ifndef CVC5__THEORY__QUANTIFIERS__ORACLE_CHECKER_H +#define CVC5__THEORY__QUANTIFIERS__ORACLE_CHECKER_H + +#include + +#include "expr/node.h" +#include "expr/node_converter.h" +#include "expr/oracle_caller.h" +#include "smt/env_obj.h" + +namespace cvc5::internal { +namespace theory { +namespace quantifiers { + +/** + * Oracle checker. + * + * This maintains callers for all oracle functions, and can be used to evaluate + * terms that contain oracle functions. In particular, all oracle functions + * that are applied to "value-like" arguments only are invoked and replaced + * by their return. A term is "value-like" if it is constant (Node::isConst()) + * or a closed lambda term. + * + * For example, if f is an oracle function, where evaluating the oracle + * f on 4 returns 5, and evaluating on 7 returns 10, this class acts as a + * node converter that may transform: + * f(f(4)+2) ---> f(5+2) ---> f(7) ---> 10 + */ +class OracleChecker : protected EnvObj, public NodeConverter +{ + public: + OracleChecker(Env& env) : EnvObj(env) {} + ~OracleChecker() {} + + /** + * Check predicted io pair is consistent, generate a lemma if + * not. This is used to check whether a definition of an oracle function + * is consistent in the model. + * + * For example, calling this method with app = f(c) and val = d will + * check whether we have evalauted the oracle associated with f on input + * c. If not, we invoke the oracle; otherwise we retrieve its cached value. + * If this output d' is not d, then this method adds d' = f(c) to lemmas. + */ + bool checkConsistent(Node app, Node val, std::vector& lemmas); + /** + * Evaluate an oracle application. Given input f(c), where f is an oracle + * function symbol, this returns the result of invoking the oracle associated + * with f. This may either correspond to a cached value, or otherwise will + * invoke the oracle. + */ + Node evaluateApp(Node app); + + /** + * Evaluate all oracle function applications (recursively) in n. This is an + * alias for convert. + */ + Node evaluate(Node n); + + /** Has oracles? Have we invoked any oracle calls */ + bool hasOracles() const; + /** Has oracle calls for oracle function symbol f. */ + bool hasOracleCalls(Node f) const; + /** Get the cached results for oracle function symbol f */ + const std::map& getOracleCalls(Node f) const; + + private: + /** + * Call back to convert, which evaluates oracle function applications and + * rewrites all other nodes. + */ + Node postConvert(Node n) override; + /** map of oracle interface nodes to oracle callers **/ + std::map d_callers; +}; + +} // namespace quantifiers +} // namespace theory +} // namespace cvc5::internal + +#endif