Modify cegqi heuristic for finite datatypes (#2126)

2 files changed, 251 insertions, 0 deletions

diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 83f1c0714..1866cf9f4 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1608,6 +1608,7 @@ REG2_TESTS = \
 	regress2/quantifiers/javafe.tc.CheckCompilationUnit.001.smt2 \
 	regress2/quantifiers/javafe.tc.FlowInsensitiveChecks.682.smt2 \
 	regress2/quantifiers/mutualrec2.cvc \
+	regress2/quantifiers/net-policy-no-time.smt2 \
 	regress2/quantifiers/nunchaku2309663.nun.min.smt2 \
 	regress2/simplify.javafe.ast.ArrayInit.35_without_quantification2.smt2 \
 	regress2/strings/cmu-dis-0707-3.smt2 \
diff --git a/test/regress/regress2/quantifiers/net-policy-no-time.smt2 b/test/regress/regress2/quantifiers/net-policy-no-time.smt2
new file mode 100644
index 000000000..6dcb47201
--- /dev/null
+++ b/test/regress/regress2/quantifiers/net-policy-no-time.smt2
@@ -0,0 +1,250 @@
+(set-logic UFDTLIRA)
+(set-option :fmf-bound true)
+(set-option :produce-models true)
+(set-info :status sat)
+
+;;; ----- Agents (Nodes, Packets, Channels)
+
+(declare-datatype NodeMobile ((Rnode)))
+(declare-datatype NodeInfra ((Anode) (Bnode) (Cnode)))
+(declare-datatype NodeBase ((Dnode)))
+(declare-datatype Node ((mobile (mnode NodeMobile)) (infra (inode NodeInfra)) (base (bnode NodeBase))))
+
+(define-fun R () Node (mobile Rnode))
+(define-fun A () Node (infra Anode))
+(define-fun B () Node (infra Bnode))
+(define-fun C () Node (infra Cnode))
+(define-fun D () Node (base Dnode))
+
+(declare-datatype Packet ((P1)))
+
+(declare-datatype Channel ((Ch1) (Ch2) (Ch3)))
+
+
+;;; ----- The global state 
+
+; for each packet, have we received that packet?
+(declare-fun GlobalState_prcv (Node Packet Int) Bool)
+
+; for each node, its energy consumption up to that time
+(declare-fun GlobalState_energy (Node Int) Real)
+
+;;; ----- Action, Conditionals
+
+(declare-datatype Action
+(
+(act_idle)
+(act_send (_dst Node) (_pck Packet) (_chn Channel))
+))
+
+(declare-datatype Condition
+(
+(ctrue)
+(check_rcv (_rcv_pck Packet))
+))
+
+; --- does a condition hold for a Node at a given time, given the global state
+(define-fun get-condition-holds ((c Condition) (n Node) (t Int)) Bool
+  (ite ((_ is check_rcv) c)
+    (GlobalState_prcv n (_rcv_pck c) t)
+  (ite ((_ is ctrue) c) 
+    true
+  ; ((_ is cfalse) c)
+    false)
+  )
+)
+; --- 
+
+;;; ----- Time
+
+(declare-fun max_period () Int)
+(assert (>= max_period 0))
+
+;;; ----- The global policy 
+
+; A "policy" is a sequence of conditional actions.
+; A "slot" is a line number in this sequence.
+; The two definitions below define a policy.
+
+; maps (Nodes, Slots) to the action taken in this slot
+(declare-fun GlobalPolicyAct (Node Int) Action)
+
+; maps (Nodes, Slots) to the conditional under which the action in this slot is taken
+(declare-fun GlobalPolicyCond (Node Int) Condition)
+
+; --- information about slots
+(declare-fun max_slots () Int)
+(assert (>= max_slots 0))
+
+;(declare-fun num_slots (Node) Int)
+;(assert (forall ((x Node)) (>= (num_slots x) 0)))
+;(define-fun num_slots ((x Node)) Int 5)
+
+; --- always terminate with true condition
+(assert (forall ((x Node)) (= (GlobalPolicyCond x max_slots) ctrue)))
+
+; --- get the action for a node at the given time, starting at slot s, given the GlobalPolicy
+(declare-fun get-action-for-time-slot (Node Int Int) Action)
+(assert (forall ((x Node) (t Int) (s Int))
+  (=>
+    (and 
+      (>= s 0) (<= s max_slots)
+      (>= t 0) (< t max_period)
+    )
+    (= 
+      (get-action-for-time-slot x t s)
+      (let ((c (GlobalPolicyCond x s)))
+      ; if s is the max slot for x, or the condition holds
+      (ite (get-condition-holds c x t)
+        ; if so, it is the conditional action
+        (GlobalPolicyAct x s)
+        ; otherwise, check the next slot
+        (get-action-for-time-slot x t (+ s 1))
+      ))
+    )
+  )
+))
+(define-fun get-action ((x Node) (t Int)) Action
+  ; get the action, starting from slot 0
+  (get-action-for-time-slot x t 0)
+)
+; --- 
+
+;;; ----- Utilities for how actions update the state
+
+; connected
+(declare-fun connectivity (Node Node Int) Real)
+(assert (forall ((x Node) (y Node) (t Int))
+  (=>
+    (and (>= t 0) (< t max_period))
+    (= 
+      (connectivity x y t)
+      (ite (= x R)
+        (ite (or (= y A) (= y B) (= y C)) 
+          1.0
+          0.0)
+      (ite (or (= x A) (= x B) (= x C))
+        (ite (= y D)
+          1.0
+          0.0)
+      ;; (= x D)
+        0.0))
+    )
+  )
+))
+(define-fun get-connected ((x Node) (y Node) (t Int)) Bool 
+;; TODO: take into account connectivity as a probability
+  (> (connectivity x y t) 0.0)
+)
+
+; was the action successful?
+(define-fun get-act-success ((x Node) (t Int)) Bool
+  (let ((x_act_at_t (get-action x t)))
+  (ite ((_ is act_send) x_act_at_t)
+    (and 
+      ; must be connected to destination at that time
+      (get-connected x (_dst x_act_at_t) t) 
+      ; packet must have already been received by x
+      (GlobalState_prcv x (_pck x_act_at_t) t)
+    )
+    true
+  )
+  )
+)
+
+; holds if x sends packet p to y at time t
+(define-fun get-sends ((x Node) (y Node) (p Packet) (t Int)) Bool
+  (let ((x_act_at_t (get-action x t)))
+  (and
+    (ite ((_ is act_send) x_act_at_t)
+      ; packet must be p and destination must be y
+      (and 
+        (= (_dst x_act_at_t) y)
+        (= (_pck x_act_at_t) p)
+      )
+      false
+    )
+    (get-act-success x t)
+  ))
+)
+
+; get energy consumption
+(define-fun get-energy ((x Node) (t Int)) Real
+  (let ((x_act_at_t (get-action x t)))
+  (ite ((_ is act_send) x_act_at_t)
+    1.0
+    0.05
+  ))
+)
+
+;;; ----- Initial state
+
+; R has all packets, no one else has any packet
+(assert (forall ((x Node) (p Packet)) (= (GlobalState_prcv x p 0) (= x R))))
+(assert (forall ((x Node)) (= (GlobalState_energy x 0) 0.0)))
+
+;;; ----- Transition relation 
+
+(assert 
+(forall ((x Node) (t Int))
+(=>
+  (and (>= t 0) (< t max_period))
+  (and
+    (forall ((p Packet))
+      (= 
+        (GlobalState_prcv x p (+ t 1)) 
+        (or 
+          (GlobalState_prcv x p t)
+          (exists ((y Node)) (get-sends y x p t)))
+      )
+    )
+    (=
+      (GlobalState_energy x (+ t 1))
+      (+ (GlobalState_energy x t) (get-energy x t))
+    )
+  )
+))
+)
+
+;;; ----- Validity of actions
+
+; cannot use the same channel
+(assert
+(forall ((x Node) (y Node) (t Int))
+  (let ((x_act_at_t (get-action x t)))
+  (let ((y_act_at_t (get-action y t)))
+  (=>
+    (and (>= t 0) (< t max_period) (not (= x y)))
+    (=>
+      (and ((_ is act_send) x_act_at_t) ((_ is act_send) y_act_at_t))
+      (not (= (_chn x_act_at_t) (_chn y_act_at_t)))
+    )
+  )))
+))
+
+; cannot send packets you don't have
+(assert
+(forall ((x Node) (t Int))
+  (let ((x_act_at_t (get-action x t)))
+  (=>
+    (and (>= t 0) (< t max_period))
+    (=>
+      ((_ is act_send) x_act_at_t) 
+      (GlobalState_prcv x (_pck x_act_at_t) t)
+    )
+  ))
+))
+
+
+
+;;; ----- Requirements
+
+(assert (GlobalState_prcv D P1 max_period))
+(assert (< (GlobalState_energy R max_period) 3.0))
+(assert (< (GlobalState_energy A max_period) 3.0))
+(assert (< (GlobalState_energy B max_period) 3.0))
+(assert (< (GlobalState_energy C max_period) 3.0))
+(assert (< (GlobalState_energy D max_period) 3.0))
+
+(check-sat)
+