From: Andrew Reynolds Date: Mon, 2 Jul 2018 17:45:48 +0000 (-0500) Subject: Modify cegqi heuristic for finite datatypes (#2126) X-Git-Tag: cvc5-1.0.0~4930 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f47f7288145e0ae5b40271e105e0f5ec52091a5f;p=cvc5.git Modify cegqi heuristic for finite datatypes (#2126) --- diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index af003ce39..4c843606b 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -73,7 +73,7 @@ std::ostream& operator<<(std::ostream& os, CegHandledStatus status) case CEG_UNHANDLED: os << "unhandled"; break; case CEG_PARTIALLY_HANDLED: os << "partially_handled"; break; case CEG_HANDLED: os << "handled"; break; - case CEG_HANDLED_UNCONDITIONAL: os << "unhandled_unc"; break; + case CEG_HANDLED_UNCONDITIONAL: os << "handled_unc"; break; default: Unreachable(); } return os; @@ -235,9 +235,9 @@ CegHandledStatus CegInstantiator::isCbqiSort( { // recursive calls to this datatype are handlable visited[tn] = CEG_HANDLED; - // if not recursive, it is finite and we can handle it regardless of body - // hence, we initialize ret to CEG_HANDLED_UNCONDITIONAL. - ret = CEG_HANDLED_UNCONDITIONAL; + // we initialize to handled, we remain handled as long as all subfields + // of this datatype are not unhandled. + ret = CEG_HANDLED; const Datatype& dt = static_cast(tn.toType()).getDatatype(); for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) { 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) +