From c6e9b167b43332464f8d066034bf4604cb37d182 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Thu, 11 Apr 2019 18:02:32 +0100
Subject: 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.
---
 src/specialize.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'src/specialize.ml')

diff --git a/src/specialize.ml b/src/specialize.ml
index 1da7208a..3063e4d5 100644
--- a/src/specialize.ml
+++ b/src/specialize.ml
@@ -485,7 +485,6 @@ let specialize_id_overloads instantiations id (Defs defs) =
 
 let initial_calls = ref (IdSet.of_list
   [ mk_id "main";
-    mk_id "check_sat";
     mk_id "__SetConfig";
     mk_id "__ListConfig";
     mk_id "execute";
-- 
cgit v1.2.3