diff options
| -rw-r--r-- | src/options/datatypes_options.toml | 15 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.cpp | 215 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.h | 47 |
3 files changed, 254 insertions, 23 deletions
diff --git a/src/options/datatypes_options.toml b/src/options/datatypes_options.toml index b74244fe1..0c521bb93 100644 --- a/src/options/datatypes_options.toml +++ b/src/options/datatypes_options.toml @@ -101,7 +101,16 @@ header = "options/datatypes_options.h" type = "bool" default = "true" read_only = true - help = "simple sygus sym break lemmas" + help = "simple sygus symmetry breaking lemmas" + +[[option]] + name = "sygusSymBreakAgg" + category = "regular" + long = "sygus-sym-break-agg" + type = "bool" + default = "true" + read_only = true + help = "use aggressive checks for simple sygus symmetry breaking lemmas" [[option]] name = "sygusSymBreakDynamic" @@ -110,7 +119,7 @@ header = "options/datatypes_options.h" type = "bool" default = "true" read_only = true - help = "dynamic sygus sym break lemmas" + help = "dynamic sygus symmetry breaking lemmas" [[option]] name = "sygusSymBreakPbe" @@ -118,7 +127,7 @@ header = "options/datatypes_options.h" long = "sygus-sym-break-pbe" type = "bool" default = "true" - help = "sygus sym break lemmas based on pbe conjectures" + help = "sygus symmetry breaking lemmas based on pbe conjectures" [[option]] name = "sygusOpt1" diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index c6976ac62..99ab54a2c 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -119,9 +119,20 @@ Node TermDbSygus::getProxyVariable(TypeNode tn, Node c) std::map<Node, Node>::iterator it = d_proxy_vars[tn].find(c); if (it == d_proxy_vars[tn].end()) { - Node k = NodeManager::currentNM()->mkSkolem("sy", tn, "sygus proxy"); - SygusPrintProxyAttribute spa; - k.setAttribute(spa, c); + int anyC = getAnyConstantConsNum(tn); + Node k; + if (anyC == -1) + { + k = NodeManager::currentNM()->mkSkolem("sy", tn, "sygus proxy"); + SygusPrintProxyAttribute spa; + k.setAttribute(spa, c); + } + else + { + const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype(); + k = NodeManager::currentNM()->mkNode( + APPLY_CONSTRUCTOR, Node::fromExpr(dt[anyC].getConstructor()), c); + } d_proxy_vars[tn][c] = k; return k; } @@ -174,6 +185,66 @@ Node TermDbSygus::mkGeneric(const Datatype& dt, int c) return mkGeneric(dt, c, pre); } +struct CanonizeBuiltinAttributeId +{ +}; +using CanonizeBuiltinAttribute = + expr::Attribute<CanonizeBuiltinAttributeId, Node>; + +Node TermDbSygus::canonizeBuiltin(Node n) +{ + std::map<TypeNode, int> var_count; + return canonizeBuiltin(n, var_count); +} + +Node TermDbSygus::canonizeBuiltin(Node n, std::map<TypeNode, int>& var_count) +{ + // has it already been computed? + if (var_count.empty() && n.hasAttribute(CanonizeBuiltinAttribute())) + { + Node ret = n.getAttribute(CanonizeBuiltinAttribute()); + Trace("sygus-db-canon") << "cached " << n << " : " << ret << "\n"; + return ret; + } + Trace("sygus-db-canon") << " CanonizeBuiltin : compute for " << n << "\n"; + Node ret = n; + // it is symbolic if it represents "any constant" + if (n.getKind() == APPLY_SELECTOR_TOTAL) + { + ret = getFreeVarInc(n[0].getType(), var_count, true); + } + else if (n.getKind() != APPLY_CONSTRUCTOR) + { + ret = n; + } + else + { + Assert(n.getKind() == APPLY_CONSTRUCTOR); + bool childChanged = false; + std::vector<Node> children; + children.push_back(n.getOperator()); + for (unsigned j = 0, size = n.getNumChildren(); j < size; ++j) + { + Node child = canonizeBuiltin(n[j], var_count); + children.push_back(child); + childChanged = childChanged || child != n[j]; + } + if (childChanged) + { + ret = NodeManager::currentNM()->mkNode(APPLY_CONSTRUCTOR, children); + } + } + // cache if we had a fresh variable count + if (var_count.empty()) + { + n.setAttribute(CanonizeBuiltinAttribute(), ret); + } + Trace("sygus-db-canon") << " ...normalized " << n << " --> " << ret + << std::endl; + Assert(ret.getType().isComparableTo(n.getType())); + return ret; +} + struct SygusToBuiltinAttributeId { }; @@ -182,7 +253,7 @@ typedef expr::Attribute<SygusToBuiltinAttributeId, Node> Node TermDbSygus::sygusToBuiltin(Node n, TypeNode tn) { - Assert( n.getType()==tn ); + Assert(n.getType().isComparableTo(tn)); if (!tn.isDatatype()) { return n; @@ -291,26 +362,24 @@ public: if( d_req_kind!=UNDEFINED_KIND ){ Trace("sygus-sb-debug") << "- check if " << tn << " has " << d_req_kind << std::endl; - int c = tdb->getKindConsNum( tn, d_req_kind ); - if( c!=-1 ){ + std::vector<TypeNode> argts; + if (tdb->canConstructKind(tn, d_req_kind, argts)) + { bool ret = true; - const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); for( std::map< unsigned, ReqTrie >::iterator it = d_children.begin(); it != d_children.end(); ++it ){ - if( it->first<dt[c].getNumArgs() ){ - TypeNode tnc = tdb->getArgType( dt[c], it->first ); + if (it->first < argts.size()) + { + TypeNode tnc = argts[it->first]; if( !it->second.satisfiedBy( tdb, tnc ) ){ - ret = false; - break; + return false; } }else{ - ret = false; - break; + return false; } } if( !ret ){ return false; } - // TODO : commutative operators try both? }else{ return false; } @@ -799,14 +868,13 @@ void TermDbSygus::registerEnumerator(Node e, d_enum_to_using_sym_cons[e] = useSymbolicCons; // depending on if we are using symbolic constructors, introduce symmetry // breaking lemma templates for each relevant subtype of the grammar - std::map<TypeNode, std::map<TypeNode, unsigned> >::iterator it = - d_min_type_depth.find(et); - Assert(it != d_min_type_depth.end()); - // for each type of subterm of this enumerator - for (const std::pair<const TypeNode, unsigned>& st : it->second) + std::vector<TypeNode> sf_types; + getSubfieldTypes(et, sf_types); + // for each type of subfield type of this enumerator + for (unsigned i = 0, ntypes = sf_types.size(); i < ntypes; i++) { std::vector<unsigned> rm_indices; - TypeNode stn = st.first; + TypeNode stn = sf_types[i]; Assert(stn.isDatatype()); const Datatype& dt = static_cast<DatatypeType>(stn.toType()).getDatatype(); std::map<TypeNode, unsigned>::iterator itsa = @@ -971,6 +1039,16 @@ TypeNode TermDbSygus::sygusToBuiltinType( TypeNode tn ) { return d_register[tn]; } +void TermDbSygus::toStreamSygus(const char* c, Node n) +{ + if (Trace.isOn(c)) + { + std::stringstream ss; + Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, n); + Trace(c) << ss.str(); + } +} + void TermDbSygus::computeMinTypeDepthInternal( TypeNode root_tn, TypeNode tn, unsigned type_depth ) { std::map< TypeNode, unsigned >::iterator it = d_min_type_depth[root_tn].find( tn ); if( it==d_min_type_depth[root_tn].end() || type_depth<it->second ){ @@ -1071,6 +1149,17 @@ unsigned TermDbSygus::getSelectorWeight(TypeNode tn, Node sel) return itsw->second[sel]; } +void TermDbSygus::getSubfieldTypes(TypeNode tn, std::vector<TypeNode>& sf_types) +{ + std::map<TypeNode, std::map<TypeNode, unsigned> >::iterator it = + d_min_type_depth.find(tn); + Assert(it != d_min_type_depth.end()); + for (const std::pair<const TypeNode, unsigned>& st : it->second) + { + sf_types.push_back(st.first); + } +} + int TermDbSygus::getKindConsNum( TypeNode tn, Kind k ) { Assert( isRegistered( tn ) ); std::map< TypeNode, std::map< Kind, int > >::iterator itt = d_kinds.find( tn ); @@ -1228,6 +1317,92 @@ bool TermDbSygus::isSymbolicConsApp(Node n) const return sygusOp.getAttribute(SygusAnyConstAttribute()); } +bool TermDbSygus::canConstructKind(TypeNode tn, + Kind k, + std::vector<TypeNode>& argts, + bool aggr) +{ + int c = getKindConsNum(tn, k); + const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype(); + if (c != -1) + { + for (unsigned i = 0, nargs = dt[c].getNumArgs(); i < nargs; i++) + { + argts.push_back(TypeNode::fromType(dt[c].getArgType(i))); + } + return true; + } + if (!options::sygusSymBreakAgg()) + { + return false; + } + if (sygusToBuiltinType(tn).isBoolean()) + { + if (k == ITE) + { + // ite( b1, b2, b3 ) <---- and( or( ~b1, b2 ), or( b1, b3 ) ) + std::vector<TypeNode> conj_types; + if (canConstructKind(tn, AND, conj_types, true) && conj_types.size() == 2) + { + bool success = true; + std::vector<TypeNode> disj_types[2]; + for (unsigned c = 0; c < 2; c++) + { + if (!canConstructKind(conj_types[c], OR, disj_types[c], true) + || disj_types[c].size() != 2) + { + success = false; + break; + } + } + if (success) + { + for (unsigned r = 0; r < 2; r++) + { + for (unsigned d = 0, size = disj_types[r].size(); d < size; d++) + { + TypeNode dtn = disj_types[r][d]; + // must have negation that occurs in the other conjunct + std::vector<TypeNode> ntypes; + if (canConstructKind(dtn, NOT, ntypes) && ntypes.size() == 1) + { + TypeNode ntn = ntypes[0]; + for (unsigned dd = 0, size = disj_types[1 - r].size(); + dd < size; + dd++) + { + if (disj_types[1 - r][dd] == ntn) + { + argts.push_back(ntn); + argts.push_back(disj_types[r][d]); + argts.push_back(disj_types[1 - r][1 - dd]); + if (Trace.isOn("sygus-cons-kind")) + { + Trace("sygus-cons-kind") + << "Can construct kind " << k << " in " << tn + << " via child types:" << std::endl; + for (unsigned i = 0; i < 3; i++) + { + Trace("sygus-cons-kind") + << " " << argts[i] << std::endl; + } + } + return true; + } + } + } + } + } + } + } + } + } + // could try aggressive inferences here, such as + // (and b1 b2) <---- (not (or (not b1) (not b2))) + // (or b1 b2) <---- (not (and (not b1) (not b2))) + return false; +} + Node TermDbSygus::minimizeBuiltinTerm( Node n ) { if( ( n.getKind()==EQUAL || n.getKind()==LEQ || n.getKind()==LT || n.getKind()==GEQ || n.getKind()==GT ) && ( n[0].getType().isInteger() || n[0].getType().isReal() ) ){ diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index 44139cf0d..3631ee520 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -171,6 +171,15 @@ class TermDbSygus { Node mkGeneric(const Datatype& dt, int c, std::map<int, Node>& pre); /** same as above, but with empty pre */ Node mkGeneric(const Datatype& dt, int c); + /** makes a symbolic term concrete + * + * Given a sygus datatype term n of type tn with holes (symbolic constructor + * applications), this function returns a term in which holes are replaced by + * unique variables. To track counters for introducing unique variables, we + * use the var_count map. + */ + Node canonizeBuiltin(Node n); + Node canonizeBuiltin(Node n, std::map<TypeNode, int>& var_count); /** sygus to builtin * * Given a sygus datatype term n of type tn, this function returns its analog, @@ -184,6 +193,9 @@ class TermDbSygus { * bn is a term of some sygus datatype tn. This function returns the rewritten * form of bn [ args / vars(tn) ], where vars(tn) is the sygus variable * list for type tn (see Datatype::getSygusVarList). + * + * If the argument tryEval is true, we consult the evaluator before the + * rewriter, for performance reasons. */ Node evaluateBuiltin(TypeNode tn, Node bn, @@ -219,6 +231,9 @@ class TermDbSygus { TypeNode sygusToBuiltinType(TypeNode tn); //-----------------------------end conversion from sygus to builtin + /** print to sygus stream n on trace c */ + static void toStreamSygus(const char* c, Node n); + private: /** reference to the quantifiers engine */ QuantifiersEngine* d_quantEngine; @@ -340,6 +355,14 @@ class TermDbSygus { unsigned getMinConsTermSize( TypeNode tn, unsigned cindex ); /** get the weight of the selector, where tn is the domain of sel */ unsigned getSelectorWeight(TypeNode tn, Node sel); + /** get subfield types + * + * This adds all "subfield types" of tn to sf_types. A type tnc is a subfield + * type of tn if there exists a selector chain S1( ... Sn( x )...) that has + * type tnc, where x has type tn. In other words, tnc is the type of some + * subfield of terms of type tn, at any depth. + */ + void getSubfieldTypes(TypeNode tn, std::vector<TypeNode>& sf_types); public: int getKindConsNum( TypeNode tn, Kind k ); @@ -371,6 +394,30 @@ class TermDbSygus { bool hasSubtermSymbolicCons(TypeNode tn) const; /** return whether n is an application of a symbolic constructor */ bool isSymbolicConsApp(Node n) const; + /** can construct kind + * + * Given a sygus datatype type tn, if this method returns true, then there + * exists values of tn whose builtin analog is equivalent to + * <k>( t1, ..., tn ). The sygus types of t1...tn are added to arg_types. + * + * For example, if: + * A -> A+A | ite( B, A, A ) | x | 1 | 0 + * B -> and( B, B ) | not( B ) | or( B, B ) | A = A + * - canConstructKind( A, +, ... ) returns true and adds {A,A} to arg_types, + * - canConstructKind( B, not, ... ) returns true and adds { B } to arg types. + * + * We also may infer that operator is constructable. For example, + * - canConstructKind( B, ite, ... ) may return true, adding { B, B, B } to + * arg_types, noting that the term + * (and (or (not b1) b2) (or b1 b3)) is equivalent to (ite b1 b2 b3) + * The argument aggr is whether we use aggressive techniques like the one + * above to infer a kind is constructable. If this flag is false, we only + * check if the kind is literally a constructor of the grammar. + */ + bool canConstructKind(TypeNode tn, + Kind k, + std::vector<TypeNode>& argts, + bool aggr = false); TypeNode getSygusTypeForVar( Node v ); Node sygusSubstituted( TypeNode tn, Node n, std::vector< Node >& args ); |