From 5e80c5741e4ece9a4c6512758775e822c39fbfc9 Mon Sep 17 00:00:00 2001
From: Zhengyang Liu <liuz@cs.utah.edu>
Date: Tue, 2 Oct 2018 19:10:36 -0600
Subject: [PATCH 1/2] Always feed getGuesses() with Vars in LHS, add a switch
 for big query and enable the ctpop test case

---
 lib/Infer/ExhaustiveSynthesis.cpp | 16 ++++++++++------
 test/Infer/popcount6-syn.opt      |  2 ++
 2 files changed, 12 insertions(+), 6 deletions(-)

diff --git a/lib/Infer/ExhaustiveSynthesis.cpp b/lib/Infer/ExhaustiveSynthesis.cpp
index bf8151e75..00ef7454a 100644
--- a/lib/Infer/ExhaustiveSynthesis.cpp
+++ b/lib/Infer/ExhaustiveSynthesis.cpp
@@ -32,6 +32,9 @@ namespace {
     "The larger the number is, the more fine-grained debug "
     "information will be printed"),
     cl::init(0));
+  static cl::opt<bool> NoBigQuery("souper-exhaustive-synthesis-no-big-query",
+    cl::desc("Disable big query in exhaustive synthesis (default=false)"),
+    cl::init(false));
 }
 
 // TODO
@@ -374,8 +377,12 @@ ExhaustiveSynthesis::synthesize(SMTLIBSolver *SMTSolver,
                                 const std::vector<InstMapping> &PCs,
                                 Inst *LHS, Inst *&RHS,
                                 InstContext &IC, unsigned Timeout) {
-  std::vector<Inst *> Inputs;
-  findCands(LHS, Inputs, /*WidthMustMatch=*/false, /*FilterVars=*/false, MaxLHSCands);
+  std::vector<Inst *> Vars;
+  findVars(LHS, Vars);
+
+  std::vector<Inst *> Inputs(Vars);
+  findCands(LHS, Inputs, /*WidthMustMatch=*/false, /*FilterVars=*/true, MaxLHSCands);
+
   if (DebugLevel > 1)
     llvm::errs() << "got " << Inputs.size() << " candidates from LHS\n";
 
@@ -397,7 +404,7 @@ ExhaustiveSynthesis::synthesize(SMTLIBSolver *SMTSolver,
 
   // Big Query
   // TODO: Need to check if big query actually saves us time or just wastes time
-  {
+  if (!NoBigQuery) {
     Inst *Ante = IC.getConst(APInt(1, true));
     BlockPCs BPCsCopy;
     std::vector<InstMapping> PCsCopy;
@@ -478,9 +485,6 @@ ExhaustiveSynthesis::synthesize(SMTLIBSolver *SMTSolver,
       }
     }
 
-    std::vector<Inst *> Vars;
-    findVars(LHS, Vars);
-
     std::map<Inst *, llvm::APInt> ConstMap;
 
     {
diff --git a/test/Infer/popcount6-syn.opt b/test/Infer/popcount6-syn.opt
index a45eb8374..2ac1b650f 100644
--- a/test/Infer/popcount6-syn.opt
+++ b/test/Infer/popcount6-syn.opt
@@ -1,7 +1,9 @@
 ; REQUIRES: solver, solver-model
 
 ; RUN: %souper-check %solver -infer-rhs -souper-infer-inst -souper-synthesis-comps=ctpop %s > %t1
+; RUN: %souper-check %solver -infer-rhs -souper-exhaustive-synthesis -souper-exhaustive-synthesis-no-big-query %s > %t2
 ; RUN: %FileCheck %s < %t1
+; RUN: %FileCheck %s < %t2
 
 ; CHECK:      %21:i32 = ctpop %0
 ; CHECK-NEXT: result %21

From 189bd13b8bfaa03519a126cd9506d686109acbcb Mon Sep 17 00:00:00 2001
From: Zhengyang Liu <liuz@cs.utah.edu>
Date: Wed, 3 Oct 2018 00:01:49 -0600
Subject: [PATCH 2/2] a updated findCands()

---
 lib/Infer/ExhaustiveSynthesis.cpp | 10 ++++++----
 lib/Inst/Inst.cpp                 | 24 ++++++++++++++++++------
 2 files changed, 24 insertions(+), 10 deletions(-)

diff --git a/lib/Infer/ExhaustiveSynthesis.cpp b/lib/Infer/ExhaustiveSynthesis.cpp
index 00ef7454a..3d774b328 100644
--- a/lib/Infer/ExhaustiveSynthesis.cpp
+++ b/lib/Infer/ExhaustiveSynthesis.cpp
@@ -377,11 +377,9 @@ ExhaustiveSynthesis::synthesize(SMTLIBSolver *SMTSolver,
                                 const std::vector<InstMapping> &PCs,
                                 Inst *LHS, Inst *&RHS,
                                 InstContext &IC, unsigned Timeout) {
-  std::vector<Inst *> Vars;
-  findVars(LHS, Vars);
 
-  std::vector<Inst *> Inputs(Vars);
-  findCands(LHS, Inputs, /*WidthMustMatch=*/false, /*FilterVars=*/true, MaxLHSCands);
+  std::vector<Inst *> Inputs;
+  findCands(LHS, Inputs, /*WidthMustMatch=*/false, /*FilterVars=*/false, MaxLHSCands);
 
   if (DebugLevel > 1)
     llvm::errs() << "got " << Inputs.size() << " candidates from LHS\n";
@@ -452,6 +450,10 @@ ExhaustiveSynthesis::synthesize(SMTLIBSolver *SMTSolver,
   // find the valid one
   int Unsat = 0;
   int GuessIndex = -1;
+
+  std::vector<Inst *> Vars;
+  findVars(LHS, Vars);
+
   for (auto I : Guesses) {
     GuessIndex++;
     if (DebugLevel > 2) {
diff --git a/lib/Inst/Inst.cpp b/lib/Inst/Inst.cpp
index 39bcdec02..244291bc9 100644
--- a/lib/Inst/Inst.cpp
+++ b/lib/Inst/Inst.cpp
@@ -783,8 +783,16 @@ void souper::findCands(Inst *Root, std::vector<Inst *> &Guesses,
                bool WidthMustMatch, bool FilterVars, int Max) {
   // breadth-first search
   std::set<Inst *> Visited;
-  std::queue<std::tuple<Inst *,int>> Q;
-  Q.push(std::make_tuple(Root, 0));
+  std::queue<std::pair<Inst *,int>> Q;
+  auto Comp = [](const std::pair<Inst *,int> A, const std::pair<Inst *,int> B)
+              {
+                return A.second < B.second;
+              };
+  std::priority_queue<std::pair<Inst *, int>,
+                      std::vector<std::pair<Inst *,int>>,
+                      decltype(Comp)> GuessesPQ(Comp);
+
+  Q.push(std::make_pair(Root, 0));
   while (!Q.empty()) {
     Inst *I;
     int Benefit;
@@ -794,7 +802,7 @@ void souper::findCands(Inst *Root, std::vector<Inst *> &Guesses,
     if (Visited.insert(I).second) {
       if (I->K != Inst::Phi) {
         for (auto Op : I->Ops)
-          Q.push(std::make_tuple(Op, Benefit));
+          Q.push(std::make_pair(Op, Benefit));
       }
       if (Benefit > 1 && I->Available && I->K != Inst::Const
           && I->K != Inst::UntypedConst) {
@@ -802,12 +810,16 @@ void souper::findCands(Inst *Root, std::vector<Inst *> &Guesses,
           continue;
         if (FilterVars && I->K == Inst::Var)
           continue;
-        Guesses.emplace_back(I);
-        if (Guesses.size() >= Max)
-          return;
+        GuessesPQ.push(std::make_pair(I, Benefit));
       }
     }
   }
+  unsigned Size = GuessesPQ.size();
+  for (unsigned T = 0 ; T < Max && T < Size ; T++) {
+    Inst *I = GuessesPQ.top().first;
+    GuessesPQ.pop();
+    Guesses.emplace_back(I);
+  }
 }
 
 Inst *souper::getInstCopy(Inst *I, InstContext &IC,