Add special solving routine by heuristic random assignments

Test:

  $ cd examples
  $ make select
  ...
  _var758 : Bag<(Int, Int, String, Int)> = FlatMap {r -> FlatMap {s -> FlatMap {q -> Map {w -> ((r).A, (s).C, (q).B, (w).C)} (Filter {w -> (((q).B == (w).B) and ((r).A == 15))} (Ws))} (Qs)} (Ss)} (Rs)
  return _var758
  ...

cozy/random_assignment.py

@@ -0,0 +1,153 @@
+import random
+import string
+from itertools import product
+
+from cozy.common import FrozenDict
+from cozy.syntax import *
+from cozy.syntax_tools import free_vars, strip_EStateVar
+from cozy.evaluation import eval, mkval
+from cozy.target_syntax import EFlatMap, EFilter, EMap, EStateVar
+from cozy.value_types import Bag
+
+
+def random_value(t):
+    """
+    Construct a stream of values in type t
+    """
+    if isinstance(t, TBag):
+        yield Bag()
+        for v in random_value(t.elem_type):
+            yield Bag((v,))
+        for v1 in random_value(t.elem_type):
+            for v2 in random_value(t.elem_type):
+                yield Bag((v1, v2))
+    elif isinstance(t, TInt):
+        yield random.randint(0, 100)
+        yield 0
+    elif isinstance(t, TNative):
+        yield (t.name, 0)
+    elif isinstance(t, TFloat):
+        yield random.randint(0, 100) / 100.0
+        yield 0.0
+    elif isinstance(t, TBool):
+        yield True
+        yield False
+    elif isinstance(t, TString):
+        yield ''.join(random.choice(string.ascii_letters) for _ in range(8))
+    elif isinstance(t, TRecord):
+        iterables = [random_value(ty) for _, ty in t.fields]
+        for vs in product(*iterables):
+            yield FrozenDict({field[0]: v for v, field in zip(vs, t.fields)})
+    else:
+        raise Exception("Unknown type for random value construction: {}".format(t))
+
+def extract_listcomp(e):
+    """
+    Extract list comprehension components from its desugared form
+    :param e: list comprehension expression
+    :return: list comprehension structure { "P": ..., "C": ..., "V": ... }
+             (we use "lc" to refer to this type of structure).
+             "P" is pulled expressions, "C" is condition, "V" is returned value.
+             In the written form, it is { V(p0, ..., pn) | p0 <- P_0, ..., pn <- P_n, C(p0, ..., pn)}.
+             Notice that all V and C already have free variables p0 to pn.
+             If the structure doesn't follow our assumption, return None
+    """
+    if isinstance(e, EFlatMap):
+        pulled = e.e
+        f = e.transform_function
+        var = f.arg
+        ebody = f.body
+        lc = extract_listcomp(ebody)
+        if lc is not None:
+            lc["P"][var] = strip_EStateVar(pulled)
+            return lc
+    elif isinstance(e, EMap):
+        f = e.transform_function
+        ebody = f.body
+        lc = extract_listcomp(e.e)
+        if lc is not None:
+            lc["V"] = ebody
+            return lc
+    elif isinstance(e, EFilter):
+        lc = {"C": e.predicate.body, "P": {e.predicate.arg: strip_EStateVar(e.e)}}
+        return lc
+    return None
+
+
+def get_cond(lc):
+    """
+    Turn list comprehension structure into a conjunctive formula that specifies each pulled collection expression
+    is a singleton and all individual elements in singletons satisfy the condition
+    """
+    singletons = [EEq(ESingleton(var).with_type(TBag(var.type)), p) for var, p in lc["P"].items()]
+    return EAll([lc["C"]] + singletons)
+
+
+def unsatisfiable(e):
+    """
+    Heuristic to decide whether e is unsatisfiable quickly.
+    it is a partial procedure: the possible outputs are True (indicating unsatisfiability) and None (indicating unknown).
+    """
+    # It is unsatisfiable that two structurally equivalent list comprehensions are not semantically equivalent
+    if isinstance(e, EUnaryOp) and e.op == "not" and isinstance(e.e, EBinOp) and e.e.op == "==":
+        e1 = e.e.e1
+        e2 = e.e.e2
+        while isinstance(e1, EStateVar):
+            e1 = e1.e
+        while isinstance(e2, EStateVar):
+            e2 = e2.e
+        if isinstance(e1, EFlatMap) and isinstance(e2, EFlatMap):
+            lc1 = extract_listcomp(e1)
+            lc2 = extract_listcomp(e2)
+            if lc1 is not None and lc2 is not None:
+                if lc1 == lc2:
+                    return True
+    return None
+
+
+def _satisfy(e, solver, assumptions):
+    """
+    :param e: expression to test sat
+    :param solver: the default solver
+    :param assumptions: a list of expressions that are assumed true
+    Heuristic to decide whether e is satisfiable quickly.
+    it is a partial procedure: the possible outputs are a satisfying assignment or None (indicating unknown)
+    it is allowed to indicate unknown with an arbitrary exception
+    (in which case falling back to the symbolic solver is a reasonable choice)
+    """
+
+    if isinstance(e, EUnaryOp) and e.op == "not" and isinstance(e.e, EBinOp) and e.e.op == "==":
+        e1 = e.e.e1
+        e2 = e.e.e2
+        if isinstance(e1, EFlatMap) and isinstance(e2, EFlatMap):
+            lc1 = extract_listcomp(e1)
+            lc2 = extract_listcomp(e2)
+            if lc1 is not None and lc2 is not None:
+                cond1 = get_cond(lc1)
+                cond2 = get_cond(lc2)
+                sat1 = solver.satisfy(cond1)
+                sat2 = solver.satisfy(cond2)
+                if sat1 is None and sat2 is not None:
+                    return {k: v for k, v in sat2.items() if k not in lc2["P"]}
+                if sat1 is not None and sat2 is None:
+                    return {k: v for k, v in sat1.items() if k not in lc1["P"]}
+
+    iterables = [random_value(v.type) for v in free_vars(e)]
+    ids = [v.id for v in free_vars(e)]
+    for vs in product(*iterables):
+        assignments = {}
+        for id_, val in zip(ids, vs):
+            assignments[id_] = val
+        sat = eval(EAll([e] + assumptions), assignments)
+        if sat:
+            return assignments
+    return None
+
+
+def satisfy(e, solver, assumptions):
+    assignments = _satisfy(e, solver, assumptions)
+    if assignments is not None:
+        for v in solver.vars:
+            if v.id not in assignments:
+                assignments[v.id] = mkval(v.type)
+    return assignments

cozy/synthesis/core.py

@@ -18,6 +18,7 @@
 
 from multiprocessing import Value
 
+from cozy import random_assignment
 from cozy.syntax import (
     INT, BOOL, TMap,
     Op,
@@ -30,7 +31,7 @@
 from cozy.typecheck import is_collection, is_scalar
 from cozy.syntax_tools import subst, pprint, free_vars, fresh_var, alpha_equivalent, strip_EStateVar, freshen_binders, wrap_naked_statevars, break_conj, inline_lets
 from cozy.wf import exp_wf
-from cozy.common import No, OrderedSet, unique, OrderedSet, StopException
+from cozy.common import No, unique, OrderedSet, StopException
 from cozy.solver import valid, solver_for_context, ModelCachingSolver
 from cozy.evaluation import construct_value
 from cozy.cost_model import CostModel, Order, LINEAR_TIME_UOPS
@@ -96,6 +97,9 @@
     description="Applies a limit to the number of improvements cozy will run"
         + "on the specification.  (-1) means no limit.")
 
+allow_random_assignment_heuristic = Option("allow-random-assignment-heuristic", bool, True,
+    description="Use a random assignment heuristic instead of solver to solve sat/unsat problem")
+
 def never_stop():
     """Takes no arguments, always returns False."""
     return False
@@ -242,7 +246,22 @@ def improve(
 
             # 2. check
             with task("verifying candidate"):
-                counterexample = solver.satisfy(ENot(EEq(target, new_target)))
+                # try heuristic based solving first
+                e = ENot(EEq(target, new_target))
+                if allow_random_assignment_heuristic.value:
+                    if random_assignment.unsatisfiable(e):
+                        counterexample = None
+                    else:
+                        try:
+                            counterexample = random_assignment.satisfy(e, solver, assumptions)
+                        except Exception:
+                            counterexample = None
+                        if counterexample is None:
+                            event("failed assignmnents: for %s\n" % e)
+                            counterexample = solver.satisfy(e)
+                            event("counter-example: for %s\n" % counterexample)
+                else:
+                    counterexample = solver.satisfy(e)
 
             if counterexample is not None:
                 if counterexample in examples:

examples/Makefile

@@ -22,8 +22,14 @@ listcomp.h: listcomp-flatmap.ds
 select.h: select-flatmap.ds
 	cozy -t $(TIMEOUT) --allow-big-sets select-flatmap.ds --c++ select.h -p 8080 --verbose --save select.synthesized
 
+select: select.cpp select.h
+	g++ -std=c++11 -O3 -Werror '$<' -o '$@'
+
 listcomp: listcomp.cpp listcomp.h
 	g++ -std=c++11 -O3 -Werror '$<' -o '$@'
 
+run-select: select
+	time ./select
+
 run-listcomp: listcomp
 	time ./listcomp

examples/select.cpp

@@ -0,0 +1,21 @@
+#include "select.h"
+#include <iostream>
+
+void query(SelectFlatmap::_Type3508 elem) {
+    std::cout << "Found elem(" << elem._0 << "," <<
+        elem._1 << "," << elem._2 << "," << elem._3 << ")" << std::endl;
+}
+
+int main() {
+    SelectFlatmap::R r(15, "hello");
+    std::vector<SelectFlatmap::R> Rs;
+    Rs.push_back(r);
+
+    SelectFlatmap::W w("world", 100);
+    std::vector<SelectFlatmap::W> Ws;
+    Ws.push_back(w);
+
+    SelectFlatmap m(Rs, Ws, Ws, Ws);
+    m.q(query);
+    return 0;
+}