Trivial solve method for single invocation sygus (#3328)

This short circuits CEGQI when the conjecture is solvable by simple equality reasoning. It adds two examples where we previously would have fallen back on enumeration due to not having an instantiation technique for strings, despite the conjectures being trivially solvable.

1 files changed, 45 insertions, 28 deletions

diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index 7703f01fd..5d5e23c75 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -28,36 +28,9 @@ namespace quantifiers {
 struct QAttributes;
 
 class QuantifiersRewriter {
-private:
-  static int getPurifyIdLit2( Node n, std::map< Node, int >& visited );
 public:
   static bool isLiteral( Node n );
-private:
-  static bool addCheckElimChild( std::vector< Node >& children, Node c, Kind k, std::map< Node, bool >& lit_pol, bool& childrenChanged );
-  static void addNodeToOrBuilder( Node n, NodeBuilder<>& t );
-  static void computeArgs(const std::vector<Node>& args,
-                          std::map<Node, bool>& activeMap,
-                          Node n,
-                          std::map<Node, bool>& visited);
-  static void computeArgVec(const std::vector<Node>& args,
-                            std::vector<Node>& activeArgs,
-                            Node n);
-  static void computeArgVec2(const std::vector<Node>& args,
-                             std::vector<Node>& activeArgs,
-                             Node n,
-                             Node ipl);
-  static Node computeProcessTerms2( Node body, bool hasPol, bool pol, std::map< Node, bool >& currCond, int nCurrCond,
-                                    std::map< Node, Node >& cache, std::map< Node, Node >& icache,
-                                    std::vector< Node >& new_vars, std::vector< Node >& new_conds, bool elimExtArith );
-  static void computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons, std::vector< Node >& conj );
-  /** datatype expand
-   *
-   * If v occurs in args and has a datatype type whose index^th constructor is
-   * C, this method returns a node of the form C( x1, ..., xn ), removes v from
-   * args and adds x1...xn to args.
-   */
-  static Node datatypeExpand(unsigned index, Node v, std::vector<Node>& args);
-  //-------------------------------------variable elimination
+  //-------------------------------------variable elimination utilities
   /** is variable elimination
    *
    * Returns true if v is not a subterm of s, and the type of s is a subtype of
@@ -127,6 +100,50 @@ private:
                              std::vector<Node>& bounds,
                              std::vector<Node>& subs,
                              QAttributes& qa);
+  //-------------------------------------end variable elimination utilities
+ private:
+  static int getPurifyIdLit2(Node n, std::map<Node, int>& visited);
+  static bool addCheckElimChild(std::vector<Node>& children,
+                                Node c,
+                                Kind k,
+                                std::map<Node, bool>& lit_pol,
+                                bool& childrenChanged);
+  static void addNodeToOrBuilder(Node n, NodeBuilder<>& t);
+  static void computeArgs(const std::vector<Node>& args,
+                          std::map<Node, bool>& activeMap,
+                          Node n,
+                          std::map<Node, bool>& visited);
+  static void computeArgVec(const std::vector<Node>& args,
+                            std::vector<Node>& activeArgs,
+                            Node n);
+  static void computeArgVec2(const std::vector<Node>& args,
+                             std::vector<Node>& activeArgs,
+                             Node n,
+                             Node ipl);
+  static Node computeProcessTerms2(Node body,
+                                   bool hasPol,
+                                   bool pol,
+                                   std::map<Node, bool>& currCond,
+                                   int nCurrCond,
+                                   std::map<Node, Node>& cache,
+                                   std::map<Node, Node>& icache,
+                                   std::vector<Node>& new_vars,
+                                   std::vector<Node>& new_conds,
+                                   bool elimExtArith);
+  static void computeDtTesterIteSplit(
+      Node n,
+      std::map<Node, Node>& pcons,
+      std::map<Node, std::map<int, Node> >& ncons,
+      std::vector<Node>& conj);
+  /** datatype expand
+   *
+   * If v occurs in args and has a datatype type whose index^th constructor is
+   * C, this method returns a node of the form C( x1, ..., xn ), removes v from
+   * args and adds x1...xn to args.
+   */
+  static Node datatypeExpand(unsigned index, Node v, std::vector<Node>& args);
+
+  //-------------------------------------variable elimination
   /** compute variable elimination
    *
    * This computes variable elimination rewrites for a body of a quantified