From: Andrew Reynolds Date: Thu, 14 Apr 2022 13:36:38 +0000 (-0500) Subject: Integrate oracle checker into quantifiers term registry (#8604) X-Git-Tag: cvc5-1.0.1~263 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=efda428a779a73e69fa853967447c82f9876d9c8;p=cvc5.git Integrate oracle checker into quantifiers term registry (#8604) Also incorporates into sygus term database. For SyMO, oracle function symbols act analogously to recursive function definitions; the oracle checker is used to rewrite terms in the same contexts as when recursive function definitions are evaluated. --- diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 1fa3fd505..4e71b2311 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -62,6 +62,11 @@ void SetDefaults::setDefaults(LogicInfo& logic, Options& opts) void SetDefaults::setDefaultsPre(Options& opts) { + + if (opts.quantifiers.oracles) + { + throw OptionException(std::string("Oracles not yet supported")); + } // implied options if (opts.smt.debugCheckModels) { diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 68fe0597a..2a5943317 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -51,12 +51,13 @@ std::ostream& operator<<(std::ostream& os, EnumeratorRole r) return os; } -TermDbSygus::TermDbSygus(Env& env, QuantifiersState& qs) +TermDbSygus::TermDbSygus(Env& env, QuantifiersState& qs, OracleChecker* oc) : EnvObj(env), d_qstate(qs), d_syexp(new SygusExplain(this)), d_funDefEval(new FunDefEvaluator(env)), - d_eval_unfold(new SygusEvalUnfold(env, this)) + d_eval_unfold(new SygusEvalUnfold(env, this)), + d_ochecker(oc) { d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); @@ -738,6 +739,7 @@ SygusTypeInfo& TermDbSygus::getTypeInfo(TypeNode tn) Node TermDbSygus::rewriteNode(Node n) const { + Trace("sygus-rewrite") << "Rewrite node: " << n << std::endl; Node res; if (options().datatypes.sygusRewriter == options::SygusRewriterMode::EXTENDED) { @@ -747,6 +749,7 @@ Node TermDbSygus::rewriteNode(Node n) const { res = rewrite(n); } + Trace("sygus-rewrite") << "Rewrite node post-rewrite: " << res << std::endl; if (res.isConst()) { // constant, we are done @@ -761,12 +764,19 @@ Node TermDbSygus::rewriteNode(Node n) const Node fres = d_funDefEval->evaluateDefinitions(res); if (!fres.isNull()) { - return fres; + res = fres; } // It may have failed, in which case there are undefined symbols in res or // we reached the limit of evaluations. In this case, we revert to the // result of rewriting in the return statement below. } + Trace("sygus-rewrite") << "Rewrite node post-rec-fun: " << res << std::endl; + } + if (d_ochecker != nullptr) + { + // evaluate oracles + res = d_ochecker->evaluate(res); + Trace("sygus-rewrite") << "Rewrite node post-oracles: " << res << std::endl; } return res; } diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index 6f9e24290..1d5471e3a 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -24,6 +24,7 @@ #include "smt/env_obj.h" #include "theory/quantifiers/extended_rewrite.h" #include "theory/quantifiers/fun_def_evaluator.h" +#include "theory/quantifiers/oracle_checker.h" #include "theory/quantifiers/sygus/sygus_eval_unfold.h" #include "theory/quantifiers/sygus/sygus_explain.h" #include "theory/quantifiers/sygus/type_info.h" @@ -56,7 +57,7 @@ std::ostream& operator<<(std::ostream& os, EnumeratorRole r); class TermDbSygus : protected EnvObj { public: - TermDbSygus(Env& env, QuantifiersState& qs); + TermDbSygus(Env& env, QuantifiersState& qs, OracleChecker* oc = nullptr); ~TermDbSygus() {} /** Finish init, which sets the inference manager */ void finishInit(QuantifiersInferenceManager* qim); @@ -83,6 +84,8 @@ class TermDbSygus : protected EnvObj FunDefEvaluator* getFunDefEvaluator() { return d_funDefEval.get(); } /** evaluation unfolding utility */ SygusEvalUnfold* getEvalUnfold() { return d_eval_unfold.get(); } + /** get the oracle checker */ + OracleChecker* getOracleChecker() { return d_ochecker; } //------------------------------end utilities //------------------------------enumerators @@ -288,7 +291,7 @@ class TermDbSygus : protected EnvObj SygusTypeInfo& getTypeInfo(TypeNode tn); /** * Rewrite the given node using the utilities in this class. This may - * involve (recursive function) evaluation. + * involve (recursive function) evaluation, and oracle evaluation. */ Node rewriteNode(Node n) const; @@ -310,6 +313,8 @@ class TermDbSygus : protected EnvObj std::unique_ptr d_funDefEval; /** evaluation function unfolding utility */ std::unique_ptr d_eval_unfold; + /** Pointer to the oracle checker */ + OracleChecker* d_ochecker; //------------------------------end utilities //------------------------------enumerators diff --git a/src/theory/quantifiers/term_registry.cpp b/src/theory/quantifiers/term_registry.cpp index 53fbc28b5..c86b7aef9 100644 --- a/src/theory/quantifiers/term_registry.cpp +++ b/src/theory/quantifiers/term_registry.cpp @@ -22,6 +22,7 @@ #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/fmf/first_order_model_fmc.h" #include "theory/quantifiers/ho_term_database.h" +#include "theory/quantifiers/oracle_checker.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/term_util.h" @@ -42,12 +43,17 @@ TermRegistry::TermRegistry(Env& env, : new TermDb(env, qs, qr)), d_echeck(new EntailmentCheck(env, qs, *d_termDb.get())), d_sygusTdb(nullptr), + d_ochecker(nullptr), d_qmodel(nullptr) { + if (options().quantifiers.oracles) + { + d_ochecker.reset(new OracleChecker(env)); + } if (options().quantifiers.sygus || options().quantifiers.sygusInst) { // must be constructed here since it is required for datatypes finistInit - d_sygusTdb.reset(new TermDbSygus(env, qs)); + d_sygusTdb.reset(new TermDbSygus(env, qs, d_ochecker.get())); } Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl; Trace("quant-engine-debug") @@ -138,6 +144,11 @@ TermDbSygus* TermRegistry::getTermDatabaseSygus() const return d_sygusTdb.get(); } +OracleChecker* TermRegistry::getOracleChecker() const +{ + return d_ochecker.get(); +} + EntailmentCheck* TermRegistry::getEntailmentCheck() const { return d_echeck.get(); diff --git a/src/theory/quantifiers/term_registry.h b/src/theory/quantifiers/term_registry.h index 73009685b..0af712985 100644 --- a/src/theory/quantifiers/term_registry.h +++ b/src/theory/quantifiers/term_registry.h @@ -34,6 +34,7 @@ namespace theory { namespace quantifiers { class FirstOrderModel; +class OracleChecker; /** * Term Registry, which manages notifying modules within quantifiers about @@ -84,6 +85,8 @@ class TermRegistry : protected EnvObj TermDb* getTermDatabase() const; /** get term database sygus */ TermDbSygus* getTermDatabaseSygus() const; + /** get oracle checker */ + OracleChecker* getOracleChecker() const; /** get entailment check utility */ EntailmentCheck* getEntailmentCheck() const; /** get term enumeration utility */ @@ -110,6 +113,8 @@ class TermRegistry : protected EnvObj std::unique_ptr d_echeck; /** sygus term database */ std::unique_ptr d_sygusTdb; + /** oracle checker */ + std::unique_ptr d_ochecker; /** extended model object */ FirstOrderModel* d_qmodel; };