Internal representation of oracle interface quantifiers (#8585)

This is the first step towards supporting SMT and synthesis modulo oracles.

It adds the kind required for specifying "oracle interface quantifiers", or, quantified formulas that specify constraints that depend on an external binary.

diff --git a/src/theory/quantifiers/kinds b/src/theory/quantifiers/kinds
index 193646c629e72ed932b766764f9a511f3a485fee..481499f2e340290c0775c99b980e440b179198b7 100644 (file)
--- a/src/theory/quantifiers/kinds
+++ b/src/theory/quantifiers/kinds
@@ -38,6 +38,8 @@ operator INST_ATTRIBUTE 1: "instantiation attribute"
 operator INST_POOL 1: "instantiation pool"
 operator INST_ADD_TO_POOL 2 "instantiation add to pool"
 operator SKOLEM_ADD_TO_POOL 2 "skolemization add to pool"
+# oracle formula generator is a pair (assumption generator, constraint generator)
+operator ORACLE_FORMULA_GEN 2 "oracle interface"
 
 sort INST_PATTERN_LIST_TYPE \
     Cardinality::INTEGERS \
@@ -51,6 +53,7 @@ typerule FORALL ::cvc5::internal::theory::quantifiers::QuantifierTypeRule
 typerule EXISTS ::cvc5::internal::theory::quantifiers::QuantifierTypeRule
 typerule BOUND_VAR_LIST ::cvc5::internal::theory::quantifiers::QuantifierBoundVarListTypeRule
 typerule INST_PATTERN_LIST ::cvc5::internal::theory::quantifiers::QuantifierInstPatternListTypeRule
+typerule ORACLE_FORMULA_GEN ::cvc5::internal::theory::quantifiers::QuantifierOracleFormulaGenTypeRule
 
 typerule INST_PATTERN ::cvc5::internal::theory::quantifiers::QuantifierInstPatternTypeRule
 typerule INST_NO_PATTERN ::cvc5::internal::theory::quantifiers::QuantifierAnnotationTypeRule

diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index 717ef1d9214a8e651ecea92aad514a7cee53572f..8775c0f79b03542258b87e9a9ad65be3f542a360 100644 (file)
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -35,7 +35,8 @@ namespace quantifiers {
 
 bool QAttributes::isStandard() const
 {
-  return !d_sygus && !d_quant_elim && !isFunDef() && !d_isQuantBounded;
+  return !d_sygus && !d_quant_elim && !isFunDef() && !isOracleInterface()
+         && !d_isQuantBounded;
 }
 
 QuantAttributes::QuantAttributes() {}
@@ -258,6 +259,14 @@ void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){
           Trace("quant-attr") << "Attribute : sygus : " << q << std::endl;
           qa.d_sygus = true;
         }
+        if (avar.hasAttribute(OracleInterfaceAttribute()))
+        {
+          qa.d_oracleInterfaceBin =
+              avar.getAttribute(OracleInterfaceAttribute());
+          Trace("quant-attr")
+              << "Attribute : oracle interface : " << qa.d_oracleInterfaceBin
+              << " : " << q << std::endl;
+        }
         if (avar.hasAttribute(SygusSideConditionAttribute()))
         {
           qa.d_sygusSideCondition =
@@ -318,18 +327,26 @@ bool QuantAttributes::isFunDef( Node q ) {
   std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
   if( it==d_qattr.end() ){
     return false;
-  }else{
-    return it->second.isFunDef();
   }
+  return it->second.isFunDef();
 }
 
 bool QuantAttributes::isSygus( Node q ) {
   std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
   if( it==d_qattr.end() ){
     return false;
-  }else{
-    return it->second.d_sygus;
   }
+  return it->second.d_sygus;
+}
+
+bool QuantAttributes::isOracleInterface(Node q)
+{
+  std::map<Node, QAttributes>::iterator it = d_qattr.find(q);
+  if (it == d_qattr.end())
+  {
+    return false;
+  }
+  return it->second.isOracleInterface();
 }
 
 int64_t QuantAttributes::getQuantInstLevel(Node q)

diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h
index 90e408922eba6a27cdb1addc7725b9c3794f4cc2..1fdbcb2fc040817c8b397458fb6f630d3aa9a15f 100644 (file)
--- a/src/theory/quantifiers/quantifiers_attributes.h
+++ b/src/theory/quantifiers/quantifiers_attributes.h
@@ -40,6 +40,27 @@ typedef expr::Attribute< QuantElimPartialAttributeId, bool > QuantElimPartialAtt
 struct SygusAttributeId {};
 typedef expr::Attribute< SygusAttributeId, bool > SygusAttribute;
 
+/**
+ * Attribute set to the name of the binary for quantifiers that are oracle
+ * interfaces. In detail, an oracle interface is a quantified formula of the
+ * form:
+ *   (FORALL
+ *     (BOUND_VAR_LIST i1 ... in o1 ... om)
+ *     (ORACLE_FORMULA_GEN A C)
+ *     (INST_PATTERN_LIST k))
+ * where i1 ... in are the inputs to the interface, o1 ... om are the outputs
+ * of the interface, A is the "assumption" formula, C is the "constraint"
+ * formula, and k is a dummy skolem that has been marked with this attribute.
+ * The string value of this attribute specifies a binary whose I/O behavior
+ * should match the types of inputs and outputs specified by i1 ... in and
+ * o1 ... om respectively.
+ */
+struct OracleInterfaceAttributeId
+{
+};
+typedef expr::Attribute<OracleInterfaceAttributeId, std::string>
+    OracleInterfaceAttribute;
+
 /**Attribute to give names to quantified formulas */
 struct QuantNameAttributeId
 {
@@ -104,6 +125,7 @@ struct QAttributes
       : d_hasPattern(false),
         d_hasPool(false),
         d_sygus(false),
+        d_oracleInterfaceBin(""),
         d_qinstLevel(-1),
         d_quant_elim(false),
         d_quant_elim_partial(false),
@@ -120,6 +142,8 @@ struct QAttributes
   Node d_fundef_f;
   /** is this formula marked as a sygus conjecture? */
   bool d_sygus;
+  /** the binary name, if this is an oracle interface quantifier */
+  std::string d_oracleInterfaceBin;
   /** side condition for sygus conjectures */
   Node d_sygusSideCondition;
   /** stores the maximum instantiation level allowed for this quantified formula
@@ -140,6 +164,8 @@ struct QAttributes
   Node d_qid_num;
   /** is this quantified formula a function definition? */
   bool isFunDef() const { return !d_fundef_f.isNull(); }
+  /** is this quantified formula an oracle interface quantifier? */
+  bool isOracleInterface() const { return !d_oracleInterfaceBin.empty(); }
   /**
    * Is this a standard quantifier? A standard quantifier is one that we can
    * perform destructive updates (variable elimination, miniscoping, etc).
@@ -198,6 +224,8 @@ class QuantAttributes
   bool isFunDef( Node q );
   /** is sygus conjecture */
   bool isSygus( Node q );
+  /** is oracle interface */
+  bool isOracleInterface(Node q);
   /** get instantiation level */
   int64_t getQuantInstLevel(Node q);
   /** is quant elim */

diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.cpp b/src/theory/quantifiers/theory_quantifiers_type_rules.cpp
index 22fa8e63ccce764b70c1f6d848a1be3d155a126c..4c851940c374311c84a4fbd97defb11e95ab6045 100644 (file)
--- a/src/theory/quantifiers/theory_quantifiers_type_rules.cpp
+++ b/src/theory/quantifiers/theory_quantifiers_type_rules.cpp
@@ -143,6 +143,25 @@ TypeNode QuantifierInstPatternListTypeRule::computeType(
   }
   return nodeManager->instPatternListType();
 }
+TypeNode QuantifierOracleFormulaGenTypeRule::computeType(
+    NodeManager* nodeManager, TNode n, bool check)
+{
+  Assert(n.getKind() == kind::ORACLE_FORMULA_GEN);
+  if (check)
+  {
+    if (!n[0].getType().isBoolean())
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "expected Boolean for oracle interface assumption");
+    }
+    if (!n[1].getType().isBoolean())
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "expected Boolean for oracle interface constraint");
+    }
+  }
+  return nodeManager->booleanType();
+}
 
 }  // namespace quantifiers
 }  // namespace theory

diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h
index e0c5eea37532038b515f03f267037800a419e321..0e6f2ef488437125496360eda9e1e8c95ee6c60a 100644 (file)
--- a/src/theory/quantifiers/theory_quantifiers_type_rules.h
+++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h
@@ -82,6 +82,16 @@ struct QuantifierInstPatternListTypeRule
   static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
+/**
+ * Type rule for oracle formula generators, which are used as the bodies
+ * of quantified formulas that specify oracle interfaces. The type rule
+ * ensures its two children are of type Boolean, and returns the Boolean type.
+ */
+struct QuantifierOracleFormulaGenTypeRule
+{
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+};
+
 }  // namespace quantifiers
 }  // namespace theory
 }  // namespace cvc5::internal