SMT: Add property and counterexample directive

Rather than generating SMT from a function called check_sat, now find
any function with a $property directive and generate SMT for it, e.g.

$property
function prop_cap_round_trip(cap: bits(128)) -> bool = {
  let cap_rt = capToBits(capBitsToCapability(true, cap));
  cap == cap_rt
}

$property
function prop_base_lteq_top(capbits: bits(128)) -> bool = {
  let c = capBitsToCapability(true, capbits);
  let (base, top) = getCapBounds(c);
  let e = unsigned(c.E);
  e >= 51 | base <= top
}

The file property.ml has a function for gathering all the properties
in a file, as well as a rewrite-pass for properties with type
quantifiers, which allows us to handle properties like

function prop forall 'n, 'n <= 100. (bv: bits('n)) -> bool = exp

by rewriting to (conceptually)

function prop(bv: bits(MAX_BIT_WIDTH)) -> bool =
  if length(bv) > 100 then true else exp

The function return is now automatically negated (i.e. always true =
unsat, sometimes false = sat), which makes sense for quickcheck-type
properties.

1 files changed, 2 insertions, 2 deletions

diff --git a/src/reporting.ml b/src/reporting.ml
index 20e44c57..c85f20ff 100644
--- a/src/reporting.ml
+++ b/src/reporting.ml
@@ -117,14 +117,14 @@ let rec simp_loc = function
   | Parse_ast.Generated l -> simp_loc l
   | Parse_ast.Range (p1, p2) -> Some (p1, p2)
   | Parse_ast.Documented (_, l) -> simp_loc l
-  
+
 let short_loc_to_string l =
   match simp_loc l with
   | None -> "unknown location"
   | Some (p1, p2) ->
      Printf.sprintf "%s %d:%d - %d:%d"
        p1.pos_fname p1.pos_lnum (p1.pos_cnum - p1.pos_bol) p2.pos_lnum (p2.pos_cnum - p2.pos_bol)
-  
+
 let print_err l m1 m2 =
   print_err_internal (Loc l) m1 m2