Skip to content

Incomplete logic detection #225

Open
@Halbaroth

Description

@Halbaroth

The printer feature of #211 failed to convert the following file into psmt2 format:

logic x : int
logic y : int
logic z : ('a, 'b) farray

goal g : x = y

I got

ANY !
Error Uncaught exception:
File "src/typecheck/logic.ml", line 300, characters 6-12: Assertion failed
Raised at Dolmen_type__Logic.Smtlib2.to_string in file "src/typecheck/logic.ml", line 300, characters 6-18
Called from Dolmen_loop__Transform.Smtlib2.compute_logic in file "src/loop/transform.ml", line 117, characters 23-64
Called from Dolmen_loop__Transform.Smtlib2.flush in file "src/loop/transform.ml", line 168, characters 26-46
Called from Dolmen_loop__Transform.Smtlib2.accumulate_logic_aux in file "src/loop/transform.ml", line 276, characters 25-41
Called from Dolmen_loop__Transform.Smtlib2.accumulate_logic in file "src/loop/transform.ml", line 303, characters 8-37
Called from Stdlib__List.fold_left in file "[list.ml](http://list.ml/)", line 123, characters 24-34
Called from Dolmen_loop__Transform.Make.transform in file "src/loop/transform.ml", line 396, characters 23-43
Called from Dolmen_loop__Pipeline.Make.eval_op in file "src/loop/pipeline.ml", line 87, characters 8-17

I disabled the logic detection as follows:

diff --git a/src/typecheck/logic.ml b/src/typecheck/logic.ml
index 4a02f736..2cc04fe6 100644
--- a/src/typecheck/logic.ml
+++ b/src/typecheck/logic.ml
@@ -228,7 +228,7 @@ module Smtlib2 = struct
       in
       Some res
 
-  (* let to_string l =
+  let to_string l =
     (* *)
     let b = Buffer.create 13 in
     assert (List.mem `Core l.theories);
@@ -307,9 +307,8 @@ module Smtlib2 = struct
        QF_UF to be the smallest logic *)
     | "QF_", _, _ -> "QF_UF"
     (* regular cases *)
-    | _, _, _ -> s *)
+    | _, _, _ -> s
 
-  let to_string _s = "ALL"
 
   module Scan(V : Dolmen_intf.View.TFF.S) = struct

and got

(set-logic ALL)
(declare-const x Int)
(declare-const y Int)
(declare-fun z (par (|'a| |'b|) () (Array |'a| |'b|)))
(push 1)
(assert (not (= x y)))
(check-sat)
(pop 1)
(exit)

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions