Blue3 port

[bathan1]

Features added

1. Dedicated solver loop for handling easy formulas:

• solve.ml

2. Integer Difference Logic solver:

• integer.ml

3. Boolean text parser

• boolean.ml

Overview

I want to merge in my toy SMT solver ("Blue3") into the concolic evaluator so it can attempt to fast-solve certain formulas. The IDL solver and Boolean text parser are more-or-less ported over 1-to-1. The primary change from the port is writing out a basic DPLL (T) solver loop.

Benchmarks

Here are the benchmark results you can find by inputting analysis.sql into an SQLite database
after running the benchmark script:

What were the average runtimes from both solvers?

avg_blue3	avg_z3
292.0μs	304.0μs

Rows with the MIN times from both solvers

trial_num	formula_id	formula	time_us_blue3	time_us_z3	which_min
0	64	(0 < a) ^ (a < 0)	3.814697	112.056732	blue3_min
2	30	(6 <= a) ^ (a < 0)	3.814697	122.070312	blue3_min
3	36	(2 < a) ^ (a < 0)	3.814697	133.037567	blue3_min
3	89	(1 <= a) ^ (0 < a) ^ (not ((a % 1) = 0))	113.010406	69.856644	z3_min
4	30	(6 <= a) ^ (a < 0)	3.814697	111.103058	blue3_min

Rows with the MAX times from both solvers

trial_num	formula_id	formula	time_us_blue3	time_us_z3	which_min
0	108	(c <= (b % a)) ^ (c <= a) ^ (0 < c) ^ (0 < a) ^ (0 < b) ^ (n	8136.034012	3366.947174	blue3_min
		ot ((b % a) = 0)) ^ (not (c = 0)) ^ (not (a = 0)) ^ (((b * a
		) / c) < b)

How much faster were the fast cases on average?

num_fast_cases	avg_faster_by	avg_percent_faster
345	110.83μs	49.6%

How much slower were the slow cases on average?

num_slow_cases	avg_slower_by	avg_percent_slower
548	50.25μs	9.81%

What was the max time difference blue3 beat z3 by?

max_diff
836.0μs

What was the max time difference z3 beat blue3 by?

max_diff
4769.0μs

[brandonzstride]

My comments are getting higher and higher level. I responded to an existing comment on to_propositional that will be especially impactful, I believe. To save energy in expectation of somewhat drastic changes in the wake of that comment, my review of integer.ml and solve.ml was rather quick.

I can really see this coming along now. Good work in handling so many of the comments from last time!

[brandonzstride]

The change only covers not, which was strictly an example. The point is that this is not comprehensive, for example, And is not explored.

[brandonzstride]

This suggestion applies to many cases above where convenient. The current code is reconstructing formulas when not necessary.

Suggested change

	| Binop
	( ((Less_than_eq | Less_than | Equal) as binop),
	Const_int c,
	Binop (((Plus | Minus) as op), Key (I a), Key (I b)) ) -> (
	match op with
	| Plus ->
	(* c <= a + b ==> c - b <= a *)
	Formula.binop binop
	(Formula.binop Minus (Formula.const_int c) (int_symbol b))
	(int_symbol a)
	| Minus ->
	(* c <= a - b ==> c + b <= a *)
	Formula.binop binop
	(Formula.binop Plus (Formula.const_int c) (int_symbol b))
	(int_symbol a)
	| _ -> failwith "unreachable")
	| Binop
	( ((Less_than_eq | Less_than | Equal) as binop),
	Const_int c,
	Binop (((Plus | Minus) as op), (Key _ as a), (Key _ as b)) ) -> (
	match op with
	| Plus ->
	(* c <= a + b ==> c - b <= a *)
	Formula.binop binop
	(Formula.binop Minus (Formula.const_int c) b)
	a
	| Minus ->
	(* c <= a - b ==> c + b <= a *)
	Formula.binop binop
	(Formula.binop Plus (Formula.const_int c) b)
	a
	| _ -> failwith "unreachable")

[bathan1]

So that was what I was trying to do initially as well, but for cases where I explicitly reconstruct, it's because I come across an error like this:

The value b has type ($a1, 'a) Formula.t
   but an expression was expected of type (int, 'b) Formula.t
   Type $a1 is not compatible with type int
   Hint: $a1 is an existential type bound by the constructor Binop.

I agree with your approach since that also reduces the number of total function calls that need to be made using my solver. How can we make this work?

[brandonzstride]

The output is a pure SAT boolean formula whose symbols are associated with SMT formulas, then you should have a pure SAT boolean formula type to represent this. That way there is no mixing. This also would mean we can take out Or from the "occurs" binary operations, as we discussed offline at one point. So please make a boolean formula type instead of reusing Formula.t.

The current assumptions you make do not hold. For example, it seems like if k0 is the way I write a key with uid 0, then the following formula has a conflict. (k0) ^ (k1 = k2). The first formula falls into the | expr -> expr case and is untouched, and the second formula can be called k0 via to_symbol. If you argue that this Char.code 'p' thing changes anything, then just consider if k0 was replaced by whatever to_symbol 0 returns. Hence to_propositional (k0 ^ (k1 = k2)) returns (k0 ^ k0), which is bad.

[brandonzstride]

This isn't especially important, but it is worth noting that this level of polymorphism on the key type k is not needed. The type k. syntax is necessary for polymorphic recursion, which means the type that k takes on may change within recursive calls. Here though, k just needs to be a standard polymorphic type variable. A locally abstract type (with (type k)) suffices to enforce the polymorphism necessary.

It may be helpful to some readers (including myself) to use exactly the required amount of polymorphic annotations.

Suggested change

	let rec is_idl_solvable : type k. (bool, k) Formula.t -> bool =
	fun formula ->
	match formula with
	| Formula.And clauses ->
	List.for_all is_idl_solvable clauses
	| clause ->
	is_idl_clause clause
	let rec is_idl_solvable (type k) (formula : (bool, k) Formula.t) : bool =
	match formula with
	| Formula.And clauses -> List.for_all is_idl_solvable clauses
	| clause -> is_idl_clause clause

P.S. a simple 'k here (without the full (type k)) may even be best, but because it doesn't actually enforce any polymorphism, it technically is not the minimally required annotation. Some would say (type k) should be reserved for GADTs, and 'k. (bool, 'k) Formula.t -> bool here is the most appropriate if you annotate types at all.

[bathan1]

Ended up having to use the : type k ... = fun syntax

[brandonzstride]

Huh. Yeah I think that relates a certain OCaml issue that I don't want to link for sake of avoiding noise. But this works:

let rec is_idl_solvable (e : (bool, 'k) Formula.t) : bool =
  match e with
  | Formula.And clauses -> List.for_all is_idl_solvable clauses
  | clause -> is_idl_clause clause

Sorry for the originally wrong suggestion.

[brandonzstride]

This function can only print either the int or bool mappings from the model. Did you mean to have a polymorphic uid function? Like this?

let to_string
  (model : 'k t)
  ~(uid : 'a. Uid.t -> ('a, 'k) Symbol.t * string)
  : string =

Alternatively, you may just make an assumption that the uid is packed into a key as-is, quite like is done in Grammar.Input_env.of_model. I think that makes usage easiest.

[bathan1]

I moved the packing logic from Grammar to be owned by Model:

type 'k key =
  | Bool_key : (bool, 'k) Symbol.t -> 'k key
  | Int_key : (int, 'k) Symbol.t -> 'k key

type 'k t =
  { value : 'a. ('a, 'k) Symbol.t -> 'a option
  ; domain : 'k key list }

Now the to_string looks like this:

let to_string
  (type k)
  (model : k t)
  ~(key : k key -> string)
  : string =
  let indent = "  " in

Let me know if I did that wrong.