diff options
author | Chantal Keller <Chantal.Keller@inria.fr> | 2015-01-12 16:28:10 +0100 |
---|---|---|
committer | Chantal Keller <Chantal.Keller@inria.fr> | 2015-01-12 16:28:10 +0100 |
commit | cfb4587e26623318f432c7e3e21711afc2b966e7 (patch) | |
tree | a90c6f372633458aa0766510bcfdc4682eaa8f6a /src/trace/satAtom.ml | |
parent | 1e10dcc783b82269cc3fe3bb7419b9c1cc9e0fa7 (diff) | |
download | smtcoq-cfb4587e26623318f432c7e3e21711afc2b966e7.tar.gz smtcoq-cfb4587e26623318f432c7e3e21711afc2b966e7.zip |
Initial import of SMTCoq v1.2
Diffstat (limited to 'src/trace/satAtom.ml')
-rw-r--r-- | src/trace/satAtom.ml | 65 |
1 files changed, 65 insertions, 0 deletions
diff --git a/src/trace/satAtom.ml b/src/trace/satAtom.ml new file mode 100644 index 0000000..ca72504 --- /dev/null +++ b/src/trace/satAtom.ml @@ -0,0 +1,65 @@ +(**************************************************************************) +(* *) +(* SMTCoq *) +(* Copyright (C) 2011 - 2015 *) +(* *) +(* Michaël Armand *) +(* Benjamin Grégoire *) +(* Chantal Keller *) +(* *) +(* Inria - École Polytechnique - MSR-Inria Joint Lab *) +(* *) +(* This file is distributed under the terms of the CeCILL-C licence *) +(* *) +(**************************************************************************) + +open SmtMisc +open CoqTerms + +module Atom = + struct + + type t = int + + let index a = a + + let equal a1 a2 = a1 == a2 + + let is_bool_type a = true + + type reify_tbl = + { mutable count : int; + tbl : (Term.constr, int) Hashtbl.t + } + + let create () = + { count = 0; + tbl = Hashtbl.create 17 } + + let declare reify a = + let res = reify.count in + Hashtbl.add reify.tbl a res; + reify.count <- res + 1; + res + + let get reify a = + try Hashtbl.find reify.tbl a + with Not_found -> declare reify a + + let atom_tbl reify = + let t = Array.make (reify.count + 1) (Lazy.force ctrue) in + let set c i = t.(i) <- c in + Hashtbl.iter set reify.tbl; + t + + let interp_tbl reify = + Term.mkArray (Lazy.force cbool, atom_tbl reify) + + end + +module Form = SmtForm.Make(Atom) +module Trace = SmtTrace.MakeOpt(Form) +module Cnf = SmtCnf.MakeCnf(Form) + + + |