src/Tools/Metis/src/Model.sml

fixed parsing of multiple negations (e.g. ~~~p) found in Vampire proofs

(* ========================================================================= *)
(* RANDOM FINITE MODELS                                                      *)
(* Copyright (c) 2003 Joe Hurd, distributed under the BSD License            *)
(* ========================================================================= *)

structure Model :> Model =
struct

open Useful;

(* ------------------------------------------------------------------------- *)
(* Constants.                                                                *)
(* ------------------------------------------------------------------------- *)

val maxSpace = 1000;

(* ------------------------------------------------------------------------- *)
(* Helper functions.                                                         *)
(* ------------------------------------------------------------------------- *)

val multInt =
    case Int.maxInt of
      NONE => (fn x => fn y => SOME (x * y))
    | SOME m =>
      let
        val m = Real.floor (Math.sqrt (Real.fromInt m))
      in
        fn x => fn y => if x <= m andalso y <= m then SOME (x * y) else NONE
      end;

local
  fun iexp x y acc =
      if y mod 2 = 0 then iexp' x y acc
      else
        case multInt acc x of
          SOME acc => iexp' x y acc
        | NONE => NONE

  and iexp' x y acc =
      if y = 1 then SOME acc
      else
        let
          val y = y div 2
        in
          case multInt x x of
            SOME x => iexp x y acc
          | NONE => NONE
        end;
in
  fun expInt x y =
      if y <= 1 then
        if y = 0 then SOME 1
        else if y = 1 then SOME x
        else raise Bug "expInt: negative exponent"
      else if x <= 1 then
        if 0 <= x then SOME x
        else raise Bug "expInt: negative exponand"
      else iexp x y 1;
end;

fun boolToInt true = 1
  | boolToInt false = 0;

fun intToBool 1 = true
  | intToBool 0 = false
  | intToBool _ = raise Bug "Model.intToBool";

fun minMaxInterval i j = interval i (1 + j - i);

(* ------------------------------------------------------------------------- *)
(* Model size.                                                               *)
(* ------------------------------------------------------------------------- *)

type size = {size : int};

(* ------------------------------------------------------------------------- *)
(* A model of size N has integer elements 0...N-1.                           *)
(* ------------------------------------------------------------------------- *)

type element = int;

val zeroElement = 0;

fun incrementElement {size = N} i =
    let
      val i = i + 1
    in
      if i = N then NONE else SOME i
    end;

fun elementListSpace {size = N} arity =
    case expInt N arity of
      NONE => NONE
    | s as SOME m => if m <= maxSpace then s else NONE;

fun elementListIndex {size = N} =
    let
      fun f acc elts =
          case elts of
            [] => acc
          | elt :: elts => f (N * acc + elt) elts
    in
      f 0
    end;

(* ------------------------------------------------------------------------- *)
(* The parts of the model that are fixed.                                    *)
(* ------------------------------------------------------------------------- *)

type fixedFunction = size -> element list -> element option;

type fixedRelation = size -> element list -> bool option;

datatype fixed =
    Fixed of
      {functions : fixedFunction NameArityMap.map,
       relations : fixedRelation NameArityMap.map};

val uselessFixedFunction : fixedFunction = K (K NONE);

val uselessFixedRelation : fixedRelation = K (K NONE);

val emptyFunctions : fixedFunction NameArityMap.map = NameArityMap.new ();

val emptyRelations : fixedRelation NameArityMap.map = NameArityMap.new ();

fun fixed0 f sz elts =
    case elts of
      [] => f sz
    | _ => raise Bug "Model.fixed0: wrong arity";

fun fixed1 f sz elts =
    case elts of
      [x] => f sz x
    | _ => raise Bug "Model.fixed1: wrong arity";

fun fixed2 f sz elts =
    case elts of
      [x,y] => f sz x y
    | _ => raise Bug "Model.fixed2: wrong arity";

val emptyFixed =
    let
      val fns = emptyFunctions
      and rels = emptyRelations
    in
      Fixed
        {functions = fns,
         relations = rels}
    end;

fun peekFunctionFixed fix name_arity =
    let
      val Fixed {functions = fns, ...} = fix
    in
      NameArityMap.peek fns name_arity
    end;

fun peekRelationFixed fix name_arity =
    let
      val Fixed {relations = rels, ...} = fix
    in
      NameArityMap.peek rels name_arity
    end;

fun getFunctionFixed fix name_arity =
    case peekFunctionFixed fix name_arity of
      SOME f => f
    | NONE => uselessFixedFunction;

fun getRelationFixed fix name_arity =
    case peekRelationFixed fix name_arity of
      SOME rel => rel
    | NONE => uselessFixedRelation;

fun insertFunctionFixed fix name_arity_fn =
    let
      val Fixed {functions = fns, relations = rels} = fix

      val fns = NameArityMap.insert fns name_arity_fn
    in
      Fixed
        {functions = fns,
         relations = rels}
    end;

fun insertRelationFixed fix name_arity_rel =
    let
      val Fixed {functions = fns, relations = rels} = fix

      val rels = NameArityMap.insert rels name_arity_rel
    in
      Fixed
        {functions = fns,
         relations = rels}
    end;

local
  fun union _ = raise Bug "Model.unionFixed: nameArity clash";
in
  fun unionFixed fix1 fix2 =
      let
        val Fixed {functions = fns1, relations = rels1} = fix1
        and Fixed {functions = fns2, relations = rels2} = fix2

        val fns = NameArityMap.union union fns1 fns2

        val rels = NameArityMap.union union rels1 rels2
      in
        Fixed
          {functions = fns,
           relations = rels}
      end;
end;

val unionListFixed =
    let
      fun union (fix,acc) = unionFixed acc fix
    in
      List.foldl union emptyFixed
    end;

local
  fun hasTypeFn _ elts =
      case elts of
        [x,_] => SOME x
      | _ => raise Bug "Model.hasTypeFn: wrong arity";

  fun eqRel _ elts =
      case elts of
        [x,y] => SOME (x = y)
      | _ => raise Bug "Model.eqRel: wrong arity";
in
  val basicFixed =
      let
        val fns = NameArityMap.singleton (Term.hasTypeFunction,hasTypeFn)

        val rels = NameArityMap.singleton (Atom.eqRelation,eqRel)
      in
        Fixed
          {functions = fns,
           relations = rels}
      end;
end;

(* ------------------------------------------------------------------------- *)
(* Renaming fixed model parts.                                               *)
(* ------------------------------------------------------------------------- *)

type fixedMap =
     {functionMap : Name.name NameArityMap.map,
      relationMap : Name.name NameArityMap.map};

fun mapFixed fixMap fix =
    let
      val {functionMap = fnMap, relationMap = relMap} = fixMap
      and Fixed {functions = fns, relations = rels} = fix

      val fns = NameArityMap.compose fnMap fns

      val rels = NameArityMap.compose relMap rels
    in
      Fixed
        {functions = fns,
         relations = rels}
    end;

local
  fun mkEntry tag (na,n) = (tag,na,n);

  fun mkList tag m = List.map (mkEntry tag) (NameArityMap.toList m);

  fun ppEntry (tag,source_arity,target) =
      Print.blockProgram Print.Inconsistent 2
        [Print.ppString tag,
         Print.addBreak 1,
         NameArity.pp source_arity,
         Print.ppString " ->",
         Print.addBreak 1,
         Name.pp target];
in
  fun ppFixedMap fixMap =
      let
        val {functionMap = fnMap, relationMap = relMap} = fixMap
      in
        case mkList "function" fnMap @ mkList "relation" relMap of
          [] => Print.skip
        | entry :: entries =>
          Print.blockProgram Print.Consistent 0
            (ppEntry entry ::
             List.map (Print.sequence Print.addNewline o ppEntry) entries)
      end;
end;

(* ------------------------------------------------------------------------- *)
(* Standard fixed model parts.                                               *)
(* ------------------------------------------------------------------------- *)

(* Projections *)

val projectionMin = 1
and projectionMax = 9;

val projectionList = minMaxInterval projectionMin projectionMax;

fun projectionName i =
    let
      val _ = projectionMin <= i orelse
              raise Bug "Model.projectionName: less than projectionMin"

      val _ = i <= projectionMax orelse
              raise Bug "Model.projectionName: greater than projectionMax"
    in
      Name.fromString ("project" ^ Int.toString i)
    end;

fun projectionFn i _ elts = SOME (List.nth (elts, i - 1));

fun arityProjectionFixed arity =
    let
      fun mkProj i = ((projectionName i, arity), projectionFn i)

      fun addProj i acc =
          if i > arity then acc
          else addProj (i + 1) (NameArityMap.insert acc (mkProj i))

      val fns = addProj projectionMin emptyFunctions

      val rels = emptyRelations
    in
      Fixed
        {functions = fns,
         relations = rels}
    end;

val projectionFixed =
    unionListFixed (List.map arityProjectionFixed projectionList);

(* Arithmetic *)

val numeralMin = ~100
and numeralMax = 100;

val numeralList = minMaxInterval numeralMin numeralMax;

fun numeralName i =
    let
      val _ = numeralMin <= i orelse
              raise Bug "Model.numeralName: less than numeralMin"

      val _ = i <= numeralMax orelse
              raise Bug "Model.numeralName: greater than numeralMax"

      val s = if i < 0 then "negative" ^ Int.toString (~i) else Int.toString i
    in
      Name.fromString s
    end;

val addName = Name.fromString "+"
and divName = Name.fromString "div"
and dividesName = Name.fromString "divides"
and evenName = Name.fromString "even"
and expName = Name.fromString "exp"
and geName = Name.fromString ">="
and gtName = Name.fromString ">"
and isZeroName = Name.fromString "isZero"
and leName = Name.fromString "<="
and ltName = Name.fromString "<"
and modName = Name.fromString "mod"
and multName = Name.fromString "*"
and negName = Name.fromString "~"
and oddName = Name.fromString "odd"
and preName = Name.fromString "pre"
and subName = Name.fromString "-"
and sucName = Name.fromString "suc";

local
  (* Support *)

  fun modN {size = N} x = x mod N;

  fun oneN sz = modN sz 1;

  fun multN sz (x,y) = modN sz (x * y);

  (* Functions *)

  fun numeralFn i sz = SOME (modN sz i);

  fun addFn sz x y = SOME (modN sz (x + y));

  fun divFn {size = N} x y =
      let
        val y = if y = 0 then N else y
      in
        SOME (x div y)
      end;

  fun expFn sz x y = SOME (exp (multN sz) x y (oneN sz));

  fun modFn {size = N} x y =
      let
        val y = if y = 0 then N else y
      in
        SOME (x mod y)
      end;

  fun multFn sz x y = SOME (multN sz (x,y));

  fun negFn {size = N} x = SOME (if x = 0 then 0 else N - x);

  fun preFn {size = N} x = SOME (if x = 0 then N - 1 else x - 1);

  fun subFn {size = N} x y = SOME (if x < y then N + x - y else x - y);

  fun sucFn {size = N} x = SOME (if x = N - 1 then 0 else x + 1);

  (* Relations *)

  fun dividesRel _ x y = SOME (divides x y);

  fun evenRel _ x = SOME (x mod 2 = 0);

  fun geRel _ x y = SOME (x >= y);

  fun gtRel _ x y = SOME (x > y);

  fun isZeroRel _ x = SOME (x = 0);

  fun leRel _ x y = SOME (x <= y);

  fun ltRel _ x y = SOME (x < y);

  fun oddRel _ x = SOME (x mod 2 = 1);
in
  val modularFixed =
      let
        val fns =
            NameArityMap.fromList
              (List.map (fn i => ((numeralName i,0), fixed0 (numeralFn i)))
                 numeralList @
               [((addName,2), fixed2 addFn),
                ((divName,2), fixed2 divFn),
                ((expName,2), fixed2 expFn),
                ((modName,2), fixed2 modFn),
                ((multName,2), fixed2 multFn),
                ((negName,1), fixed1 negFn),
                ((preName,1), fixed1 preFn),
                ((subName,2), fixed2 subFn),
                ((sucName,1), fixed1 sucFn)])

        val rels =
            NameArityMap.fromList
              [((dividesName,2), fixed2 dividesRel),
               ((evenName,1), fixed1 evenRel),
               ((geName,2), fixed2 geRel),
               ((gtName,2), fixed2 gtRel),
               ((isZeroName,1), fixed1 isZeroRel),
               ((leName,2), fixed2 leRel),
               ((ltName,2), fixed2 ltRel),
               ((oddName,1), fixed1 oddRel)]
      in
        Fixed
          {functions = fns,
           relations = rels}
      end;
end;

local
  (* Support *)

  fun cutN {size = N} x = if x >= N then N - 1 else x;

  fun oneN sz = cutN sz 1;

  fun multN sz (x,y) = cutN sz (x * y);

  (* Functions *)

  fun numeralFn i sz = if i < 0 then NONE else SOME (cutN sz i);

  fun addFn sz x y = SOME (cutN sz (x + y));

  fun divFn _ x y = if y = 0 then NONE else SOME (x div y);

  fun expFn sz x y = SOME (exp (multN sz) x y (oneN sz));

  fun modFn {size = N} x y =
      if y = 0 orelse x = N - 1 then NONE else SOME (x mod y);

  fun multFn sz x y = SOME (multN sz (x,y));

  fun negFn _ x = if x = 0 then SOME 0 else NONE;

  fun preFn _ x = if x = 0 then NONE else SOME (x - 1);

  fun subFn {size = N} x y =
      if y = 0 then SOME x
      else if x = N - 1 orelse x < y then NONE
      else SOME (x - y);

  fun sucFn sz x = SOME (cutN sz (x + 1));

  (* Relations *)

  fun dividesRel {size = N} x y =
      if x = 1 orelse y = 0 then SOME true
      else if x = 0 then SOME false
      else if y = N - 1 then NONE
      else SOME (divides x y);

  fun evenRel {size = N} x =
      if x = N - 1 then NONE else SOME (x mod 2 = 0);

  fun geRel {size = N} y x =
      if x = N - 1 then if y = N - 1 then NONE else SOME false
      else if y = N - 1 then SOME true else SOME (x <= y);

  fun gtRel {size = N} y x =
      if x = N - 1 then if y = N - 1 then NONE else SOME false
      else if y = N - 1 then SOME true else SOME (x < y);

  fun isZeroRel _ x = SOME (x = 0);

  fun leRel {size = N} x y =
      if x = N - 1 then if y = N - 1 then NONE else SOME false
      else if y = N - 1 then SOME true else SOME (x <= y);

  fun ltRel {size = N} x y =
      if x = N - 1 then if y = N - 1 then NONE else SOME false
      else if y = N - 1 then SOME true else SOME (x < y);

  fun oddRel {size = N} x =
      if x = N - 1 then NONE else SOME (x mod 2 = 1);
in
  val overflowFixed =
      let
        val fns =
            NameArityMap.fromList
              (List.map (fn i => ((numeralName i,0), fixed0 (numeralFn i)))
                 numeralList @
               [((addName,2), fixed2 addFn),
                ((divName,2), fixed2 divFn),
                ((expName,2), fixed2 expFn),
                ((modName,2), fixed2 modFn),
                ((multName,2), fixed2 multFn),
                ((negName,1), fixed1 negFn),
                ((preName,1), fixed1 preFn),
                ((subName,2), fixed2 subFn),
                ((sucName,1), fixed1 sucFn)])

        val rels =
            NameArityMap.fromList
              [((dividesName,2), fixed2 dividesRel),
               ((evenName,1), fixed1 evenRel),
               ((geName,2), fixed2 geRel),
               ((gtName,2), fixed2 gtRel),
               ((isZeroName,1), fixed1 isZeroRel),
               ((leName,2), fixed2 leRel),
               ((ltName,2), fixed2 ltRel),
               ((oddName,1), fixed1 oddRel)]
      in
        Fixed
          {functions = fns,
           relations = rels}
      end;
end;

(* Sets *)

val cardName = Name.fromString "card"
and complementName = Name.fromString "complement"
and differenceName = Name.fromString "difference"
and emptyName = Name.fromString "empty"
and memberName = Name.fromString "member"
and insertName = Name.fromString "insert"
and intersectName = Name.fromString "intersect"
and singletonName = Name.fromString "singleton"
and subsetName = Name.fromString "subset"
and symmetricDifferenceName = Name.fromString "symmetricDifference"
and unionName = Name.fromString "union"
and universeName = Name.fromString "universe";

local
  (* Support *)

  fun eltN {size = N} =
      let
        fun f 0 acc = acc
          | f x acc = f (x div 2) (acc + 1)
      in
        f N ~1
      end;

  fun posN i = Word.<< (0w1, Word.fromInt i);

  fun univN sz = Word.- (posN (eltN sz), 0w1);

  fun setN sz x = Word.andb (Word.fromInt x, univN sz);

  (* Functions *)

  fun cardFn sz x =
      let
        fun f 0w0 acc = acc
          | f s acc =
            let
              val acc = if Word.andb (s,0w1) = 0w0 then acc else acc + 1
            in
              f (Word.>> (s,0w1)) acc
            end
      in
        SOME (f (setN sz x) 0)
      end;

  fun complementFn sz x = SOME (Word.toInt (Word.xorb (univN sz, setN sz x)));

  fun differenceFn sz x y =
      let
        val x = setN sz x
        and y = setN sz y
      in
        SOME (Word.toInt (Word.andb (x, Word.notb y)))
      end;

  fun emptyFn _ = SOME 0;

  fun insertFn sz x y =
      let
        val x = x mod eltN sz
        and y = setN sz y
      in
        SOME (Word.toInt (Word.orb (posN x, y)))
      end;

  fun intersectFn sz x y =
      SOME (Word.toInt (Word.andb (setN sz x, setN sz y)));

  fun singletonFn sz x =
      let
        val x = x mod eltN sz
      in
        SOME (Word.toInt (posN x))
      end;

  fun symmetricDifferenceFn sz x y =
      let
        val x = setN sz x
        and y = setN sz y
      in
        SOME (Word.toInt (Word.xorb (x,y)))
      end;

  fun unionFn sz x y =
      SOME (Word.toInt (Word.orb (setN sz x, setN sz y)));

  fun universeFn sz = SOME (Word.toInt (univN sz));

  (* Relations *)

  fun memberRel sz x y =
      let
        val x = x mod eltN sz
        and y = setN sz y
      in
        SOME (Word.andb (posN x, y) <> 0w0)
      end;

  fun subsetRel sz x y =
      let
        val x = setN sz x
        and y = setN sz y
      in
        SOME (Word.andb (x, Word.notb y) = 0w0)
      end;
in
  val setFixed =
      let
        val fns =
            NameArityMap.fromList
              [((cardName,1), fixed1 cardFn),
               ((complementName,1), fixed1 complementFn),
               ((differenceName,2), fixed2 differenceFn),
               ((emptyName,0), fixed0 emptyFn),
               ((insertName,2), fixed2 insertFn),
               ((intersectName,2), fixed2 intersectFn),
               ((singletonName,1), fixed1 singletonFn),
               ((symmetricDifferenceName,2), fixed2 symmetricDifferenceFn),
               ((unionName,2), fixed2 unionFn),
               ((universeName,0), fixed0 universeFn)]

        val rels =
            NameArityMap.fromList
              [((memberName,2), fixed2 memberRel),
               ((subsetName,2), fixed2 subsetRel)]
      in
        Fixed
          {functions = fns,
           relations = rels}
      end;
end;

(* Lists *)

val appendName = Name.fromString "@"
and consName = Name.fromString "::"
and lengthName = Name.fromString "length"
and nilName = Name.fromString "nil"
and nullName = Name.fromString "null"
and tailName = Name.fromString "tail";

local
  val baseFix =
      let
        val fix = unionFixed projectionFixed overflowFixed

        val sucFn = getFunctionFixed fix (sucName,1)

        fun suc2Fn sz _ x = sucFn sz [x]
      in
        insertFunctionFixed fix ((sucName,2), fixed2 suc2Fn)
      end;

  val fixMap =
      {functionMap = NameArityMap.fromList
                       [((appendName,2),addName),
                        ((consName,2),sucName),
                        ((lengthName,1), projectionName 1),
                        ((nilName,0), numeralName 0),
                        ((tailName,1),preName)],
       relationMap = NameArityMap.fromList
                       [((nullName,1),isZeroName)]};

in
  val listFixed = mapFixed fixMap baseFix;
end;

(* ------------------------------------------------------------------------- *)
(* Valuations.                                                               *)
(* ------------------------------------------------------------------------- *)

datatype valuation = Valuation of element NameMap.map;

val emptyValuation = Valuation (NameMap.new ());

fun insertValuation (Valuation m) v_i = Valuation (NameMap.insert m v_i);

fun peekValuation (Valuation m) v = NameMap.peek m v;

fun constantValuation i =
    let
      fun add (v,V) = insertValuation V (v,i)
    in
      NameSet.foldl add emptyValuation
    end;

val zeroValuation = constantValuation zeroElement;

fun getValuation V v =
    case peekValuation V v of
      SOME i => i
    | NONE => raise Error "Model.getValuation: incomplete valuation";

fun randomValuation {size = N} vs =
    let
      fun f (v,V) = insertValuation V (v, Portable.randomInt N)
    in
      NameSet.foldl f emptyValuation vs
    end;

fun incrementValuation N vars =
    let
      fun inc vs V =
          case vs of
            [] => NONE
          | v :: vs =>
            let
              val (carry,i) =
                  case incrementElement N (getValuation V v) of
                    SOME i => (false,i)
                  | NONE => (true,zeroElement)

              val V = insertValuation V (v,i)
            in
              if carry then inc vs V else SOME V
            end
    in
      inc (NameSet.toList vars)
    end;

fun foldValuation N vars f =
    let
      val inc = incrementValuation N vars

      fun fold V acc =
          let
            val acc = f (V,acc)
          in
            case inc V of
              NONE => acc
            | SOME V => fold V acc
          end

      val zero = zeroValuation vars
    in
      fold zero
    end;

(* ------------------------------------------------------------------------- *)
(* A type of random finite mapping Z^n -> Z.                                 *)
(* ------------------------------------------------------------------------- *)

val UNKNOWN = ~1;

datatype table =
    ForgetfulTable
  | ArrayTable of int Array.array;

fun newTable N arity =
    case elementListSpace {size = N} arity of
      NONE => ForgetfulTable
    | SOME space => ArrayTable (Array.array (space,UNKNOWN));

local
  fun randomResult R = Portable.randomInt R;
in
  fun lookupTable N R table elts =
      case table of
        ForgetfulTable => randomResult R
      | ArrayTable a =>
        let
          val i = elementListIndex {size = N} elts

          val r = Array.sub (a,i)
        in
          if r <> UNKNOWN then r
          else
            let
              val r = randomResult R

              val () = Array.update (a,i,r)
            in
              r
            end
        end;
end;

fun updateTable N table (elts,r) =
    case table of
      ForgetfulTable => ()
    | ArrayTable a =>
      let
        val i = elementListIndex {size = N} elts

        val () = Array.update (a,i,r)
      in
        ()
      end;

(* ------------------------------------------------------------------------- *)
(* A type of random finite mappings name * arity -> Z^arity -> Z.            *)
(* ------------------------------------------------------------------------- *)

datatype tables =
    Tables of
      {domainSize : int,
       rangeSize : int,
       tableMap : table NameArityMap.map ref};

fun newTables N R =
    Tables
      {domainSize = N,
       rangeSize = R,
       tableMap = ref (NameArityMap.new ())};

fun getTables tables n_a =
    let
      val Tables {domainSize = N, rangeSize = _, tableMap = tm} = tables

      val ref m = tm
    in
      case NameArityMap.peek m n_a of
        SOME t => t
      | NONE =>
        let
          val (_,a) = n_a

          val t = newTable N a

          val m = NameArityMap.insert m (n_a,t)

          val () = tm := m
        in
          t
        end
    end;

fun lookupTables tables (n,elts) =
    let
      val Tables {domainSize = N, rangeSize = R, ...} = tables

      val a = length elts

      val table = getTables tables (n,a)
    in
      lookupTable N R table elts
    end;

fun updateTables tables ((n,elts),r) =
    let
      val Tables {domainSize = N, ...} = tables

      val a = length elts

      val table = getTables tables (n,a)
    in
      updateTable N table (elts,r)
    end;

(* ------------------------------------------------------------------------- *)
(* A type of random finite models.                                           *)
(* ------------------------------------------------------------------------- *)

type parameters = {size : int, fixed : fixed};

datatype model =
    Model of
      {size : int,
       fixedFunctions : (element list -> element option) NameArityMap.map,
       fixedRelations : (element list -> bool option) NameArityMap.map,
       randomFunctions : tables,
       randomRelations : tables};

fun new {size = N, fixed} =
    let
      val Fixed {functions = fns, relations = rels} = fixed

      val fixFns = NameArityMap.transform (fn f => f {size = N}) fns
      and fixRels = NameArityMap.transform (fn r => r {size = N}) rels

      val rndFns = newTables N N
      and rndRels = newTables N 2
    in
      Model
        {size = N,
         fixedFunctions = fixFns,
         fixedRelations = fixRels,
         randomFunctions = rndFns,
         randomRelations = rndRels}
    end;

fun size (Model {size = N, ...}) = N;

fun peekFixedFunction M (n,elts) =
    let
      val Model {fixedFunctions = fixFns, ...} = M
    in
      case NameArityMap.peek fixFns (n, length elts) of
        NONE => NONE
      | SOME fixFn => fixFn elts
    end;

fun isFixedFunction M n_elts = Option.isSome (peekFixedFunction M n_elts);

fun peekFixedRelation M (n,elts) =
    let
      val Model {fixedRelations = fixRels, ...} = M
    in
      case NameArityMap.peek fixRels (n, length elts) of
        NONE => NONE
      | SOME fixRel => fixRel elts
    end;

fun isFixedRelation M n_elts = Option.isSome (peekFixedRelation M n_elts);

(* A default model *)

val defaultSize = 8;

val defaultFixed =
    unionListFixed
      [basicFixed,
       projectionFixed,
       modularFixed,
       setFixed,
       listFixed];

val default = {size = defaultSize, fixed = defaultFixed};

(* ------------------------------------------------------------------------- *)
(* Taking apart terms to interpret them.                                     *)
(* ------------------------------------------------------------------------- *)

fun destTerm tm =
    case tm of
      Term.Var _ => tm
    | Term.Fn f_tms =>
      case Term.stripApp tm of
        (_,[]) => tm
      | (v as Term.Var _, tms) => Term.Fn (Term.appName, v :: tms)
      | (Term.Fn (f,tms), tms') => Term.Fn (f, tms @ tms');

(* ------------------------------------------------------------------------- *)
(* Interpreting terms and formulas in the model.                             *)
(* ------------------------------------------------------------------------- *)

fun interpretFunction M n_elts =
    case peekFixedFunction M n_elts of
      SOME r => r
    | NONE =>
      let
        val Model {randomFunctions = rndFns, ...} = M
      in
        lookupTables rndFns n_elts
      end;

fun interpretRelation M n_elts =
    case peekFixedRelation M n_elts of
      SOME r => r
    | NONE =>
      let
        val Model {randomRelations = rndRels, ...} = M
      in
        intToBool (lookupTables rndRels n_elts)
      end;

fun interpretTerm M V =
    let
      fun interpret tm =
          case destTerm tm of
            Term.Var v => getValuation V v
          | Term.Fn (f,tms) => interpretFunction M (f, List.map interpret tms)
    in
      interpret
    end;

fun interpretAtom M V (r,tms) =
    interpretRelation M (r, List.map (interpretTerm M V) tms);

fun interpretFormula M =
    let
      val N = size M

      fun interpret V fm =
          case fm of
            Formula.True => true
          | Formula.False => false
          | Formula.Atom atm => interpretAtom M V atm
          | Formula.Not p => not (interpret V p)
          | Formula.Or (p,q) => interpret V p orelse interpret V q
          | Formula.And (p,q) => interpret V p andalso interpret V q
          | Formula.Imp (p,q) => interpret V (Formula.Or (Formula.Not p, q))
          | Formula.Iff (p,q) => interpret V p = interpret V q
          | Formula.Forall (v,p) => interpret' V p v N
          | Formula.Exists (v,p) =>
            interpret V (Formula.Not (Formula.Forall (v, Formula.Not p)))

      and interpret' V fm v i =
          i = 0 orelse
          let
            val i = i - 1
            val V' = insertValuation V (v,i)
          in
            interpret V' fm andalso interpret' V fm v i
          end
    in
      interpret
    end;

fun interpretLiteral M V (pol,atm) =
    let
      val b = interpretAtom M V atm
    in
      if pol then b else not b
    end;

fun interpretClause M V cl = LiteralSet.exists (interpretLiteral M V) cl;

(* ------------------------------------------------------------------------- *)
(* Check whether random groundings of a formula are true in the model.       *)
(* Note: if it's cheaper, a systematic check will be performed instead.      *)
(* ------------------------------------------------------------------------- *)

fun check interpret {maxChecks} M fv x =
    let
      val N = size M

      fun score (V,{T,F}) =
          if interpret M V x then {T = T + 1, F = F} else {T = T, F = F + 1}

      fun randomCheck acc = score (randomValuation {size = N} fv, acc)

      val maxChecks =
          case maxChecks of
            NONE => maxChecks
          | SOME m =>
            case expInt N (NameSet.size fv) of
              SOME n => if n <= m then NONE else maxChecks
            | NONE => maxChecks
    in
      case maxChecks of
        SOME m => funpow m randomCheck {T = 0, F = 0}
      | NONE => foldValuation {size = N} fv score {T = 0, F = 0}
    end;

fun checkAtom maxChecks M atm =
    check interpretAtom maxChecks M (Atom.freeVars atm) atm;

fun checkFormula maxChecks M fm =
    check interpretFormula maxChecks M (Formula.freeVars fm) fm;

fun checkLiteral maxChecks M lit =
    check interpretLiteral maxChecks M (Literal.freeVars lit) lit;

fun checkClause maxChecks M cl =
    check interpretClause maxChecks M (LiteralSet.freeVars cl) cl;

(* ------------------------------------------------------------------------- *)
(* Updating the model.                                                       *)
(* ------------------------------------------------------------------------- *)

fun updateFunction M func_elts_elt =
    let
      val Model {randomFunctions = rndFns, ...} = M

      val () = updateTables rndFns func_elts_elt
    in
      ()
    end;

fun updateRelation M (rel_elts,pol) =
    let
      val Model {randomRelations = rndRels, ...} = M

      val () = updateTables rndRels (rel_elts, boolToInt pol)
    in
      ()
    end;

(* ------------------------------------------------------------------------- *)
(* A type of terms with interpretations embedded in the subterms.            *)
(* ------------------------------------------------------------------------- *)

datatype modelTerm =
    ModelVar
  | ModelFn of Term.functionName * modelTerm list * int list;

fun modelTerm M V =
    let
      fun modelTm tm =
          case destTerm tm of
            Term.Var v => (ModelVar, getValuation V v)
          | Term.Fn (f,tms) =>
            let
              val (tms,xs) = unzip (List.map modelTm tms)
            in
              (ModelFn (f,tms,xs), interpretFunction M (f,xs))
            end
    in
      modelTm
    end;

(* ------------------------------------------------------------------------- *)
(* Perturbing the model.                                                     *)
(* ------------------------------------------------------------------------- *)

datatype perturbation =
    FunctionPerturbation of (Term.functionName * element list) * element
  | RelationPerturbation of (Atom.relationName * element list) * bool;

fun perturb M pert =
    case pert of
      FunctionPerturbation func_elts_elt => updateFunction M func_elts_elt
    | RelationPerturbation rel_elts_pol => updateRelation M rel_elts_pol;

local
  fun pertTerm _ [] _ acc = acc
    | pertTerm M target tm acc =
      case tm of
        ModelVar => acc
      | ModelFn (func,tms,xs) =>
        let
          fun onTarget ys = mem (interpretFunction M (func,ys)) target

          val func_xs = (func,xs)

          val acc =
              if isFixedFunction M func_xs then acc
              else
                let
                  fun add (y,acc) = FunctionPerturbation (func_xs,y) :: acc
                in
                  List.foldl add acc target
                end
        in
          pertTerms M onTarget tms xs acc
        end

  and pertTerms M onTarget =
      let
        val N = size M

        fun filterElements pred =
            let
              fun filt 0 acc = acc
                | filt i acc =
                  let
                    val i = i - 1
                    val acc = if pred i then i :: acc else acc
                  in
                    filt i acc
                  end
            in
              filt N []
            end

        fun pert _ [] [] acc = acc
          | pert ys (tm :: tms) (x :: xs) acc =
            let
              fun pred y =
                  y <> x andalso onTarget (List.revAppend (ys, y :: xs))

              val target = filterElements pred

              val acc = pertTerm M target tm acc
            in
              pert (x :: ys) tms xs acc
            end
          | pert _ _ _ _ = raise Bug "Model.pertTerms.pert"
      in
        pert []
      end;

  fun pertAtom M V target (rel,tms) acc =
      let
        fun onTarget ys = interpretRelation M (rel,ys) = target

        val (tms,xs) = unzip (List.map (modelTerm M V) tms)

        val rel_xs = (rel,xs)

        val acc =
            if isFixedRelation M rel_xs then acc
            else RelationPerturbation (rel_xs,target) :: acc
      in
        pertTerms M onTarget tms xs acc
      end;

  fun pertLiteral M V ((pol,atm),acc) = pertAtom M V pol atm acc;

  fun pertClause M V cl acc = LiteralSet.foldl (pertLiteral M V) acc cl;

  fun pickPerturb M perts =
      if List.null perts then ()
      else perturb M (List.nth (perts, Portable.randomInt (length perts)));
in
  fun perturbTerm M V (tm,target) =
      pickPerturb M (pertTerm M target (fst (modelTerm M V tm)) []);

  fun perturbAtom M V (atm,target) =
      pickPerturb M (pertAtom M V target atm []);

  fun perturbLiteral M V lit = pickPerturb M (pertLiteral M V (lit,[]));

  fun perturbClause M V cl = pickPerturb M (pertClause M V cl []);
end;

(* ------------------------------------------------------------------------- *)
(* Pretty printing.                                                          *)
(* ------------------------------------------------------------------------- *)

fun pp M =
    Print.program
      [Print.ppString "Model{",
       Print.ppInt (size M),
       Print.ppString "}"];

end