From: Andrew Reynolds Date: Thu, 7 Apr 2022 21:32:07 +0000 (-0500) Subject: Internal representation of oracle interface quantifiers (#8585) X-Git-Tag: cvc5-1.0.1~285 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=134c3bf441564f32c7978ba17d581751bc457a97;p=cvc5.git 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 193646c62..481499f2e 100644 --- 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 717ef1d92..8775c0f79 100644 --- 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::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 90e408922..1fdbcb2fc 100644 --- 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 + 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 22fa8e63c..4c851940c 100644 --- 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 e0c5eea37..0e6f2ef48 100644 --- 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