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 1fa3fd5051cb2cc16224e8512900b924fc7b0179..4e71b231195cba76dc944590281d8ef5ed7e7c83 100644 (file)
--- 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 68fe0597a8af317e43f6f55cb6185057d0ecca28..2a5943317716cf6e939444814ef44b47ab0d99d1 100644 (file)
--- 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 6f9e24290902cad33492c8168e63c25c0db87e91..1d5471e3a5926d75db608f0e272115a22335bd2e 100644 (file)
--- 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<FunDefEvaluator> d_funDefEval;
   /** evaluation function unfolding utility */
   std::unique_ptr<SygusEvalUnfold> 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 53fbc28b5e232721cc32d65870360e26c4480dae..c86b7aef95a85d8e608de4284acb27460e97d9d0 100644 (file)
--- 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 73009685be878e32cb15b06d217dbf8d3243cb46..0af7129851d309924d80c916feb94f283f749ad8 100644 (file)
--- 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<EntailmentCheck> d_echeck;
   /** sygus term database */
   std::unique_ptr<TermDbSygus> d_sygusTdb;
+  /** oracle checker */
+  std::unique_ptr<OracleChecker> d_ochecker;
   /** extended model object */
   FirstOrderModel* d_qmodel;
 };