Synthesize rewrite rules from inputs (#2608)

4 files changed, 30 insertions, 18 deletions

diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h
index c32a1390c..448150d06 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.h
+++ b/src/theory/quantifiers/sygus/cegis_unif.h
@@ -88,8 +88,6 @@ class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf
    * registerEvalPtAtSize on the output channel of d_qe.
    */
   void registerEvalPts(const std::vector<Node>& eis, Node e);
-  /** Retrieves active guard for enumerator */
-  Node getActiveGuardForEnumerator(Node e);
 
  private:
   /** reference to quantifier engine */
@@ -102,9 +100,6 @@ class CegisUnifEnumDecisionStrategy : public DecisionStrategyFmf
   bool d_initialized;
   /** null node */
   Node d_null;
-  /** map from condition enumerators to active guards (in case they are
-   * enumerated indepedently of the return values) */
-  std::map<Node, Node> d_enum_to_active_guard;
   /** information per initialized type */
   class StrategyPtInfo
   {
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index eadbf766a..47c701cf6 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -126,21 +126,18 @@ Node CegGrammarConstructor::process(Node q,
         preGrammarType = preGrammarType.getRangeType();
       }
     }
-    Node sfvl = getSygusVarList(sf);
-    // sfvl may be null for constant synthesis functions
-    Trace("cegqi-debug") << "...sygus var list associated with " << sf << " is " << sfvl << std::endl;
 
     // the actual sygus datatype we will use (normalized below)
     TypeNode tn;
     std::stringstream ss;
     ss << sf;
-    if (preGrammarType.isDatatype()
-        && static_cast<DatatypeType>(preGrammarType.toType())
-               .getDatatype()
-               .isSygus())
+    Node sfvl;
+    if (preGrammarType.isDatatype() && preGrammarType.getDatatype().isSygus())
     {
+      sfvl = Node::fromExpr(preGrammarType.getDatatype().getSygusVarList());
       tn = preGrammarType;
     }else{
+      sfvl = getSygusVarList(sf);
       // check which arguments are irrelevant
       std::unordered_set<unsigned> arg_irrelevant;
       d_parent->getProcess()->getIrrelevantArgs(sf, arg_irrelevant);
@@ -156,6 +153,9 @@ Node CegGrammarConstructor::process(Node q,
       tn = mkSygusDefaultType(
           preGrammarType, sfvl, ss.str(), extra_cons, exc_cons, term_irlv);
     }
+    // sfvl may be null for constant synthesis functions
+    Trace("cegqi-debug") << "...sygus var list associated with " << sf << " is "
+                         << sfvl << std::endl;
 
     // normalize type
     SygusGrammarNorm sygus_norm(d_qe);
@@ -367,6 +367,10 @@ void CegGrammarConstructor::mkSygusConstantsForType(TypeNode type,
     ops.push_back(nm->mkConst(true));
     ops.push_back(nm->mkConst(false));
   }
+  else if (type.isString())
+  {
+    ops.push_back(nm->mkConst(String("")));
+  }
   // TODO #1178 : add other missing types
 }
 
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
index 022031bef..0c5b67656 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
@@ -108,6 +108,12 @@ public:
    * functions-to-synthesize of sygus conjecture q.
    */
   static bool hasSyntaxRestrictions(Node q);
+  /**
+   * Make the builtin constants for type "type" that should be included in a
+   * sygus grammar, add them to vector ops.
+   */
+  static void mkSygusConstantsForType(TypeNode type, std::vector<Node>& ops);
+
  private:
   /** reference to quantifier engine */
   QuantifiersEngine * d_qe;
@@ -124,8 +130,6 @@ public:
   //---------------- grammar construction
   // helper for mkSygusDefaultGrammar (makes unresolved type for mutually recursive datatype construction)
   static TypeNode mkUnresolvedType(const std::string& name, std::set<Type>& unres);
-  // make the builtin constants for type type that should be included in a sygus grammar
-  static void mkSygusConstantsForType(TypeNode type, std::vector<Node>& ops);
   // collect the list of types that depend on type range
   static void collectSygusGrammarTypesFor( TypeNode range, std::vector< TypeNode >& types, std::map< TypeNode, std::vector< DatatypeConstructorArg > >& sels );
   /** helper function for function mkSygusDefaultType
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
index b014a30c6..b5dea4c38 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
@@ -158,12 +158,21 @@ void SygusGrammarNorm::TypeObject::addConsInfo(SygusGrammarNorm* sygus_norm,
   Node sygus_op = Node::fromExpr(cons.getSygusOp());
   Trace("sygus-grammar-normalize-debug")
       << ".....operator is " << sygus_op << std::endl;
-  Node exp_sop_n = Node::fromExpr(
-      smt::currentSmtEngine()->expandDefinitions(sygus_op.toExpr()));
+  Node exp_sop_n = sygus_op;
+  // Only expand definitions if the operator is not constant, since calling
+  // expandDefinitions on them should be a no-op. This check ensures we don't
+  // try to expand e.g. bitvector extract operators, whose type is undefined,
+  // and thus should not be passed to expandDefinitions.
+  if (!sygus_op.isConst())
+  {
+    exp_sop_n = Node::fromExpr(
+        smt::currentSmtEngine()->expandDefinitions(sygus_op.toExpr()));
+  }
+  // get the kind for the operator.
+  Kind ok = NodeManager::operatorToKind(exp_sop_n);
   // if it is a builtin operator, convert to total version if necessary
-  if (exp_sop_n.getKind() == kind::BUILTIN)
+  if (ok != UNDEFINED_KIND)
   {
-    Kind ok = NodeManager::operatorToKind(sygus_op);
     Kind nk = getEliminateKind(ok);
     if (nk != ok)
     {