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.

diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index 7703f01fd3c465b429dfbef106253ab6a68c2467..5d5e23c75872c0dfb5eb47bea47a83421acc5dd5 100644 (file)
--- 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

diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index c3b9fc28b50e7953398ac01ed4a45ab4090990dd..96c79e69d86844327f6472920664ec9784cf5652 100644 (file)
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -20,25 +20,25 @@
 #include "smt/smt_statistics_registry.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 
-using namespace CVC4;
 using namespace CVC4::kind;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
-using namespace std;
 
 namespace CVC4 {
+namespace theory {
+namespace quantifiers {
 
 CegSingleInv::CegSingleInv(QuantifiersEngine* qe, SynthConjecture* p)
     : d_qe(qe),
       d_parent(p),
       d_sip(new SingleInvocationPartition),
       d_sol(new CegSingleInvSol(qe)),
+      d_isSolved(false),
       d_single_invocation(false)
 {
 
@@ -317,7 +317,11 @@ void CegSingleInv::finishInit(bool syntaxRestricted)
   CegHandledStatus status = CEG_HANDLED;
   if (d_single_inv.getKind() == FORALL)
   {
-    status = CegInstantiator::isCbqiQuant(d_single_inv);
+    // if the conjecture is not trivially solvable
+    if (!solveTrivial(d_single_inv))
+    {
+      status = CegInstantiator::isCbqiQuant(d_single_inv);
+    }
   }
   Trace("cegqi-si") << "CegHandledStatus is " << status << std::endl;
   if (status < CEG_HANDLED)
@@ -329,21 +333,8 @@ void CegSingleInv::finishInit(bool syntaxRestricted)
     d_single_invocation = false;
     d_single_inv = Node::null();
   }
-  // If we succeeded, mark the quantified formula with the quantifier
-  // elimination attribute to ensure its structure is preserved
-  if (!d_single_inv.isNull() && d_single_inv.getKind() == FORALL)
-  {
-    Node n_attr =
-        nm->mkSkolem("qe_si",
-                     nm->booleanType(),
-                     "Auxiliary variable for qe attr for single invocation.");
-    QuantElimAttribute qea;
-    n_attr.setAttribute(qea, true);
-    n_attr = nm->mkNode(INST_ATTRIBUTE, n_attr);
-    n_attr = nm->mkNode(INST_PATTERN_LIST, n_attr);
-    d_single_inv = nm->mkNode(FORALL, d_single_inv[0], d_single_inv[1], n_attr);
-  }
 }
+
 bool CegSingleInv::solve()
 {
   if (d_single_inv.isNull())
@@ -351,12 +342,32 @@ bool CegSingleInv::solve()
     // not using single invocation techniques
     return false;
   }
+  if (d_isSolved)
+  {
+    // already solved, probably via a call to solveTrivial.
+    return true;
+  }
   Trace("cegqi-si") << "Solve using single invocation..." << std::endl;
   NodeManager* nm = NodeManager::currentNM();
+  // Mark the quantified formula with the quantifier elimination attribute to
+  // ensure its structure is preserved in the query below.
+  Node siq = d_single_inv;
+  if (siq.getKind() == FORALL)
+  {
+    Node n_attr =
+        nm->mkSkolem("qe_si",
+                     nm->booleanType(),
+                     "Auxiliary variable for qe attr for single invocation.");
+    QuantElimAttribute qea;
+    n_attr.setAttribute(qea, true);
+    n_attr = nm->mkNode(INST_ATTRIBUTE, n_attr);
+    n_attr = nm->mkNode(INST_PATTERN_LIST, n_attr);
+    siq = nm->mkNode(FORALL, siq[0], siq[1], n_attr);
+  }
   // solve the single invocation conjecture using a fresh copy of SMT engine
   SmtEngine siSmt(nm->toExprManager());
   siSmt.setLogic(smt::currentSmtEngine()->getLogicInfo());
-  siSmt.assertFormula(d_single_inv.toExpr());
+  siSmt.assertFormula(siq.toExpr());
   Result r = siSmt.checkSat();
   Trace("cegqi-si") << "Result: " << r << std::endl;
   if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
@@ -405,6 +416,7 @@ bool CegSingleInv::solve()
       Trace("cegqi-si") << "  Instantiation Lemma: " << ilem << std::endl;
     }
   }
+  d_isSolved = true;
   return true;
 }
 
@@ -606,5 +618,75 @@ Node CegSingleInv::reconstructToSyntax(Node s,
 }
 
 void CegSingleInv::preregisterConjecture(Node q) { d_orig_conjecture = q; }
-  
-} //namespace CVC4
+
+bool CegSingleInv::solveTrivial(Node q)
+{
+  Assert(!d_isSolved);
+  Assert(d_inst.empty());
+  Assert(q.getKind() == FORALL);
+  // If the conjecture is forall x1...xn. ~(x1 = t1 ^ ... xn = tn), it is
+  // trivially solvable.
+  std::vector<Node> args(q[0].begin(), q[0].end());
+  // keep solving for variables until a fixed point is reached
+  std::vector<Node> vars;
+  std::vector<Node> subs;
+  Node body = q[1];
+  Node prev;
+  while (prev != body && !args.empty())
+  {
+    prev = body;
+
+    std::vector<Node> varsTmp;
+    std::vector<Node> subsTmp;
+    QuantifiersRewriter::getVarElim(body, false, args, varsTmp, subsTmp);
+    // if we eliminated a variable, update body and reprocess
+    if (!varsTmp.empty())
+    {
+      Assert(varsTmp.size() == subsTmp.size());
+      // remake with eliminated nodes
+      body = body.substitute(
+          varsTmp.begin(), varsTmp.end(), subsTmp.begin(), subsTmp.end());
+      body = Rewriter::rewrite(body);
+      // apply to subs
+      // this ensures we behave correctly if we solve x before y in
+      // x = y+1 ^ y = 2.
+      for (size_t i = 0, ssize = subs.size(); i < ssize; i++)
+      {
+        subs[i] = subs[i].substitute(
+            varsTmp.begin(), varsTmp.end(), subsTmp.begin(), subsTmp.end());
+        subs[i] = Rewriter::rewrite(subs[i]);
+      }
+      vars.insert(vars.end(), varsTmp.begin(), varsTmp.end());
+      subs.insert(subs.end(), subsTmp.begin(), subsTmp.end());
+    }
+  }
+  // if we solved all arguments
+  if (args.empty())
+  {
+    Trace("cegqi-si-trivial-solve")
+        << q << " is trivially solvable by substitution " << vars << " -> "
+        << subs << std::endl;
+    std::map<Node, Node> imap;
+    for (size_t j = 0, vsize = vars.size(); j < vsize; j++)
+    {
+      imap[vars[j]] = subs[j];
+    }
+    std::vector<Node> inst;
+    for (const Node& v : q[0])
+    {
+      Assert(imap.find(v) != imap.end());
+      inst.push_back(imap[v]);
+    }
+    d_inst.push_back(inst);
+    d_instConds.push_back(NodeManager::currentNM()->mkConst(true));
+    d_isSolved = true;
+    return true;
+  }
+  Trace("cegqi-si-trivial-solve")
+      << q << " is not trivially solvable." << std::endl;
+  return false;
+}
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4

diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h
index 00e3639f8cb3e3bb536b3f05c66cdcb27839ba28..0d5af327e7210bf35c619b7b0b3b697b373036db 100644 (file)
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h
@@ -76,7 +76,9 @@ class CegSingleInv
   Node d_orig_solution;
   Node d_solution;
   Node d_sygus_solution;
+
  public:
+  //---------------------------------representation of the solution
   /**
    * The list of instantiations that suffice to show the first-order equivalent
    * of the negated synthesis conjecture is unsatisfiable.
@@ -87,6 +89,9 @@ class CegSingleInv
    * first order conjecture for the term vectors above.
    */
   std::vector<Node> d_instConds;
+  /** is solved */
+  bool d_isSolved;
+  //---------------------------------end representation of the solution
 
  private:
   // conjecture
@@ -168,6 +173,15 @@ class CegSingleInv
       return Node::null();
     }
   }
+
+ private:
+  /** solve trivial
+   *
+   * If this method returns true, it sets d_isSolved to true and adds
+   * t1 ... tn to d_inst if it can be shown that (forall x1 ... xn. P) is
+   * unsatisfiable for instantiation {x1 -> t1 ... xn -> tn}.
+   */
+  bool solveTrivial(Node q);
 };
 
 }/* namespace CVC4::theory::quantifiers */

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index b47d22492c324e2847841766577219af1ae16c5f..ca33b45c54ad42cf35083df7a869a9b79692fe90 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -887,6 +887,8 @@ set(regress_0_tests
   regress0/sygus/array-grammar-store.sy
   regress0/sygus/c100.sy
   regress0/sygus/ccp16.lus.sy
+  regress0/sygus/cegqi-si-string-triv.sy
+  regress0/sygus/cegqi-si-string-triv-2fun.sy
   regress0/sygus/check-generic-red.sy
   regress0/sygus/const-var-test.sy
   regress0/sygus/dt-no-syntax.sy

diff --git a/test/regress/regress0/sygus/cegqi-si-string-triv-2fun.sy b/test/regress/regress0/sygus/cegqi-si-string-triv-2fun.sy
new file mode 100644 (file)
index 0000000..fc8864f
--- /dev/null
+++ b/test/regress/regress0/sygus/cegqi-si-string-triv-2fun.sy
@@ -0,0 +1,14 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic ALL)
+
+(synth-fun f ((x String) (y String)) String)
+(synth-fun g ((x String) (y String)) String)
+
+(declare-var x String)
+(declare-var y String)
+
+(constraint (= (f x y) (str.replace (str.++ x y) "A" "ABCD")))
+(constraint (= (g x y) (str.replace (f x y) "B" "CDE")))
+
+(check-synth)

diff --git a/test/regress/regress0/sygus/cegqi-si-string-triv.sy b/test/regress/regress0/sygus/cegqi-si-string-triv.sy
new file mode 100644 (file)
index 0000000..86a6857
--- /dev/null
+++ b/test/regress/regress0/sygus/cegqi-si-string-triv.sy
@@ -0,0 +1,12 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic ALL)
+
+(synth-fun f ((x String) (y String)) String)
+
+(declare-var x String)
+(declare-var y String)
+
+(constraint (= (f x y) (str.replace (str.++ x y) "A" "ABCD")))
+
+(check-synth)