Recall that the hybrid value modifications in the backend extend the notion of a variable-value to be in four states:

- A known constant (this was the only non-hybrid possibility before)
- A value less than some bound
- A value greater than some bound
- An unknown value

Things currently aren't very optimized. Suppose we have a variable

*x*in the third state, i.e. we know*x*>= BND, where BND is some positive constant. Then, if we want to compute*x*> 0, we should return**constant-true**, not**unknown**. Similarly, if we multiply two large values, we should get another large value. There's a lot of these specialized functions -- one for every operator, and for every comparator we want to know whether it's possible, or

**known**, that e.g.*x*>*y*, or whether is possible, denoted**maybe**. Instead of writing these core and critical specializations by hand, it would be nice to sketch them. So, first consider a

**known**sketch generator. The sketch, marked by**deffcn**, takes two arguments, and checks whether these inputs being certain types of values (e.g. zero, large, unknown) will imply that the output is a certain type.(defn known [xpred op ypred testpred]

(test-hyp defaultopts (sketch

(

**deffcn**^{:tag void :type harness}**known-test**[^int**x**^int**y**] (defvar ^int opresult (op x y))

(

**skassert**(**=>**(and (xpred x) (ypred y)) (testpred opresult))) ))))

The

**test-hyp**will run the sketch, and return**true**if it succeeds, or**false**if it cannot be completed.(defn test-hyp [opts prog]

(def result (|> {:varGen (new TempVarGen) :prog prog}

(

**semantic-check-stage**opts true) (

**preproc-stage**opts) (

**hack-lowlevelc**opts))) (try

(let [backend (new

**SATBackend**opts rctrl (:varGen result)) solns (seq (. backend

**partialEvalAndSolve**(:prog result)))]**true**)

(catch

**SketchNotResolvedException**e**false**)) ) Finally, to test out some hypotheses, we can call our sketch generator with various functions,

(defn isZero [x] (== 0 x))

(defn isHigh [x] (<= 10 x))

(defn isLow [x] (<= -10 x))

(defn test1 [] (

**known**isHigh * isHigh isZero))(defn test2 [] (

**known**isLow * isHigh isLow))(defn test3 [] (

**known**isHigh * isHigh isHigh)) The first test fails, since multiplying two high numbers doesn't always [in fact, ever, though that's not what we're testing for] result in zero. The second and third tests succeed, since they do always hold. Please check out

**skclojure1.clj**in my branch (now clojurefe) if you're curious to see more.
## No comments:

## Post a Comment