Looping issue when attempting to represent FSM's

[shanth2600]

Hello,
We have encountered an issue in trying to represent finite state machines with no cycles(apologies in advanced for the lengthy writeup).

Setup

(set-option :produce-models true)
(set-logic ALL)


; Declarations for the demo FSM
; =============================

(declare-datatype myfsm-state (
  (myfsm-state-A) (myfsm-state-B) (myfsm-state-C) (myfsm-state-D)
))

(define-fun myfsm-state-function ((state myfsm-state) (input Bool)) myfsm-state
	(match state (
		(myfsm-state-A (ite input myfsm-state-B myfsm-state-A))
		(myfsm-state-B (ite input myfsm-state-D myfsm-state-C))
		(myfsm-state-C (ite input myfsm-state-C myfsm-state-D))
		(myfsm-state-D (ite input myfsm-state-A myfsm-state-C))
	))
)

Above:

• The type myfsm-state enumerates the states of the FSM
• The function myfsm-state-function describes the transitions between the states (parametrized by the boolean value input)

; Declarations for the generic FSM model/API
; ==========================================

(declare-datatype fsm-input ((fsm-make-input
	; List of all input signals
	(fsm-input-sig-din Bool)
)))

(declare-datatype fsm-output ((fsm-make-output
	; List of all output signals
	(fsm-output-sig-dout Bool)
)))

(declare-datatype fsm-state ((fsm-make-state
	; List of all state registers
	(fsm-state-reg-state myfsm-state)
)))

(declare-datatype fsm-time (
	; a time step can either be the initial state ...
	(fsm-time-init)
	; ... or be created from another time step and an input value
	(fsm-time-next (fsm-time-prev fsm-time) (fsm-time-input fsm-input))
))

(define-funs-rec (
	(fsm-get-depth ((t fsm-time)) Int)
	(fsm-no-loops ((t fsm-time)) Bool)
	(fsm-no-loops-worker ((t fsm-time) (s fsm-state)) Bool)
	(fsm-get-state ((t fsm-time)) fsm-state)
) (
		; fsm-get-depth
	(match t (
		(fsm-time-init 0)
		((fsm-time-next prev input) (+ 1 (fsm-get-depth prev)))
	))

	; fsm-no-loops
	(fsm-no-loops-worker t (fsm-get-state t))

	; fsm-no-loops-worker
	(match t (
		(fsm-time-init true)
		((fsm-time-next prev input) (and (distinct (fsm-get-state prev) s) (fsm-no-loops-worker prev s)))
	))

	; fsm-get-state
	(match t (
		(fsm-time-init (fsm-make-state
			; List of all initial register values
			myfsm-state-A
		))
		((fsm-time-next prev input) (fsm-make-state
			; List of all next register values
			(myfsm-state-function (fsm-state-reg-state (fsm-get-state prev)) (fsm-input-sig-din input))
		))
	))
))

Above we have:

• fsm-input and fsm-output types which represent the input to and output from the FSM respectively as lists of Bools
• fsm-state which represents the states of a user defined FSM as a list of states.
• fsm-time which is an inductive type representing a path taken through the FSM. The initial time-step contains no input, while ensuing steps are parameterized by a previous state and an input.
• fsm-get-depth which recursively computes the depth of a trace (fsm-time)
• fsm-no-loops which, given a trace, makes sure no node has been visited twice.
• fsm-get-state which given a trace, computes the final state of the FSM.

Query

(declare-const t fsm-time)
(assert (= (fsm-get-depth t) 2))

(check-sat)
(get-model)

If we then query an instance of a trace t, with of depth 2, Z3 has no issues coming up such a trace:

sat
(
  (define-fun t () fsm-time
    (fsm-time-next (fsm-time-next fsm-time-init (fsm-make-input false))
               (fsm-make-input false)))
)

The issue is, if we try to further constrain t by specifying that it has no loops:

(declare-const t fsm-time)
(assert (= (fsm-get-depth t) 2))

(assert (fsm-no-loops t))

(check-sat)
(get-model)

Z3 hangs.

Interestingly however, this code works fine before f976b16 (associated with #4679). Specifically, this is the line which causes the regression:

diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index f86cc6cb6..709886e4d 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -306,6 +306,7 @@ void cmd_context::insert_macro(symbol const& s, unsigned arity, sort*const* doma
     else {
         VERIFY(decls.insert(m(), arity, domain, t));
     }
+    model_add(s, arity, domain, t);
 }