Always feed getGuesses() with Vars in LHS, add a switch for big query…

… and enable the ctpop test case
google · Oct 3, 2018 · 76e2ab9 · 76e2ab9
1 parent 6c5baca
commit 76e2ab9
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 6 deletions.
diff --git 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(true));
 }
 
 // TODO
@@ -365,8 +368,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";
 
@@ -388,7 +395,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;
@@ -468,9 +475,6 @@ ExhaustiveSynthesis::synthesize(SMTLIBSolver *SMTSolver,
       }
     }
 
-    std::vector<Inst *> Vars;
-    findVars(LHS, Vars);
-
     std::map<Inst *, std::vector<llvm::APInt>> TriedVars;
     std::map<Inst *, llvm::APInt> ConstMap;
 

diff --git 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