From 324ca0376c960c75f621f0102eeaa1186589dda7 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 1 Jun 2016 16:25:50 -0500 Subject: [PATCH] Fix to ignore a case of triggers with no free variables. --- src/theory/quantifiers/trigger.cpp | 11 ++- src/theory/quantifiers/trigger.h | 1 + test/regress/regress0/quantifiers/Makefile.am | 3 +- .../quantifiers/z3.620661-no-fv-trigger.smt2 | 87 +++++++++++++++++++ 4 files changed, 97 insertions(+), 5 deletions(-) create mode 100644 test/regress/regress0/quantifiers/z3.620661-no-fv-trigger.smt2 diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index c91194239..214a4d055 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -284,7 +284,7 @@ bool Trigger::isUsableEqTerms( Node q, Node n1, Node n2 ) { return true; } } - }else if( isAtomicTrigger( n1 ) && isUsable( n1, q ) ){ + }else if( isUsableAtomicTrigger( n1, q ) ){ if( options::relationalTriggers() && n2.getKind()==INST_CONSTANT && !quantifiers::TermDb::containsTerm( n1, n2 ) ){ return true; }else if( !quantifiers::TermDb::hasInstConstAttr(n2) ){ @@ -339,15 +339,18 @@ Node Trigger::getIsUsableTrigger( Node n, Node q ) { return rtr2; } }else{ - bool usable = quantifiers::TermDb::getInstConstAttr(n)==q && isAtomicTrigger( n ) && isUsable( n, q ); - Trace("trigger-debug") << n << " usable : " << (quantifiers::TermDb::getInstConstAttr(n)==q) << " " << isAtomicTrigger( n ) << " " << isUsable( n, q ) << std::endl; - if( usable ){ + Trace("trigger-debug") << n << " usable : " << ( quantifiers::TermDb::getInstConstAttr(n)==q ) << " " << isAtomicTrigger( n ) << " " << isUsable( n, q ) << std::endl; + if( isUsableAtomicTrigger( n, q ) ){ return pol ? n : NodeManager::currentNM()->mkNode( IFF, n, NodeManager::currentNM()->mkConst( true ) ).notNode(); } } return Node::null(); } +bool Trigger::isUsableAtomicTrigger( Node n, Node q ) { + return quantifiers::TermDb::getInstConstAttr( n )==q && isAtomicTrigger( n ) && isUsable( n, q ); +} + bool Trigger::isUsableTrigger( Node n, Node q ){ Node nu = getIsUsableTrigger( n, q ); return !nu.isNull(); diff --git a/src/theory/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h index 902f73e75..a3da4d398 100644 --- a/src/theory/quantifiers/trigger.h +++ b/src/theory/quantifiers/trigger.h @@ -107,6 +107,7 @@ class Trigger { /** is usable trigger */ static bool isUsableTrigger( Node n, Node q ); static Node getIsUsableTrigger( Node n, Node q ); + static bool isUsableAtomicTrigger( Node n, Node q ); static bool isAtomicTrigger( Node n ); static bool isAtomicTriggerKind( Kind k ); static bool isRelationalTrigger( Node n ); diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index f6d65958e..4c657adf1 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -82,7 +82,8 @@ TESTS = \ parametric-lists.smt2 \ partial-trigger.smt2 \ inst-max-level-segf.smt2 \ - small-bug1-fixpoint-3.smt2 + small-bug1-fixpoint-3.smt2 \ + z3.620661-no-fv-trigger.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine diff --git a/test/regress/regress0/quantifiers/z3.620661-no-fv-trigger.smt2 b/test/regress/regress0/quantifiers/z3.620661-no-fv-trigger.smt2 new file mode 100644 index 000000000..aad2a4691 --- /dev/null +++ b/test/regress/regress0/quantifiers/z3.620661-no-fv-trigger.smt2 @@ -0,0 +1,87 @@ +(set-logic AUFNIRA) +(set-info :status unsat) +(declare-sort S1 0) +(declare-sort S2 0) +(declare-sort S3 0) +(declare-sort S4 0) +(declare-sort S5 0) +(declare-sort S6 0) +(declare-sort S7 0) +(declare-sort S8 0) +(declare-sort S9 0) +(declare-sort S10 0) +(declare-sort S11 0) +(declare-sort S12 0) +(declare-sort S13 0) +(declare-fun f1 () S1) +(declare-fun f2 () S1) +(declare-fun f3 (S2 Real) Real) +(declare-fun f4 (S3 Real) S2) +(declare-fun f5 () S3) +(declare-fun f6 (S4 Int) Int) +(declare-fun f7 (S5 Int) S4) +(declare-fun f8 () S5) +(declare-fun f9 () S2) +(declare-fun f10 () Real) +(declare-fun f11 () Real) +(declare-fun f12 () S2) +(declare-fun f13 (S7 S6) Real) +(declare-fun f14 () S7) +(declare-fun f15 () S2) +(declare-fun f16 () S2) +(declare-fun f17 (S8 Int) S6) +(declare-fun f18 () S8) +(declare-fun f19 (S9 S6) Int) +(declare-fun f20 () S9) +(declare-fun f21 (S10 Real) S7) +(declare-fun f22 () S10) +(declare-fun f23 () S2) +(declare-fun f24 (S11 S6) S6) +(declare-fun f25 (S12 S6) S11) +(declare-fun f26 () S12) +(declare-fun f27 () S12) +(declare-fun f28 (S13 Int) S9) +(declare-fun f29 () S13) +(declare-fun f30 () S2) +(declare-fun f31 () S4) +(assert (not (= f1 f2))) +(assert (forall ((?v0 Real) (?v1 Real)) (= (f3 (f4 f5 ?v0) ?v1) (* ?v0 ?v1)))) +(assert (forall ((?v0 Int) (?v1 Int)) (= (f6 (f7 f8 ?v0) ?v1) (* ?v0 ?v1)))) +(assert (not (= (f3 f9 (- f10 f11)) (- (f3 f9 f10))))) +(assert (= (f3 f9 f11) 0.0)) +(assert (forall ((?v0 Real)) (= (f3 f9 (+ f11 ?v0)) (- (f3 f9 ?v0))))) +(assert (= (f3 f9 (/ f11 2.0)) 1.0)) +(assert (= (f3 f9 (/ f11 6.0)) (/ 1.0 2.0))) +(assert (= (f3 f9 (* 2.0 f11)) 0.0)) +(assert (= (f3 f9 (* (/ 3.0 2.0) f11)) (- 1.0))) +(assert (let ((?v_0 2.0)) (<= (/ f11 ?v_0) ?v_0))) +(assert (let ((?v_0 2.0)) (< (/ f11 ?v_0) ?v_0))) +(assert (< (- (* 2.0 f11)) f11)) +(assert (< (- (/ f11 2.0)) 0.0)) +(assert (<= 2.0 f11)) +(assert (<= 0.0 (/ f11 2.0))) +(assert (< 0.0 (/ f11 2.0))) +(assert (< f11 4.0)) +(assert (<= 0.0 f11)) +(assert (< 0.0 f11)) +(assert (let ((?v_0 2.0)) (not (= (/ f11 ?v_0) ?v_0)))) +(assert (not (= (/ f11 2.0) 0.0))) +(assert (not (< f11 0.0))) +(assert (not (= f11 0.0))) +(assert (forall ((?v0 S6) (?v1 S6)) (= (= (f13 f14 ?v0) (f13 f14 ?v1)) (= ?v0 ?v1)))) +(assert (forall ((?v0 S6) (?v1 S6)) (= (< (f13 f14 ?v0) (f13 f14 ?v1)) (< (f19 f20 ?v0) (f19 f20 ?v1))))) +(assert (forall ((?v0 S6) (?v1 S6)) (= (<= (f13 f14 ?v0) (f13 f14 ?v1)) (<= (f19 f20 ?v0) (f19 f20 ?v1))))) +(assert (forall ((?v0 S6) (?v1 S6)) (let ((?v_0 (f19 f20 ?v1)) (?v_1 (f19 f20 ?v0))) (=> (<= ?v_1 ?v_0) (= (f13 f14 (f17 f18 (- ?v_0 ?v_1))) (- (f13 f14 ?v1) (f13 f14 ?v0))))))) +(assert (forall ((?v0 Real) (?v1 Real)) (exists ((?v2 Real) (?v3 Real)) (and (= ?v0 (* ?v2 (f3 f15 ?v3))) (= ?v1 (* ?v2 (f3 f9 ?v3))))))) +(assert (< 1.0 (f3 f16 2.0))) +(assert (< 0.0 (f3 f16 2.0))) +(assert (<= 0.0 (f3 f16 2.0))) +(assert (forall ((?v0 Real) (?v1 Real)) (<= 0.0 (f3 f16 (+ (* ?v0 ?v0) (* ?v1 ?v1)))))) +(assert (forall ((?v0 Real) (?v1 Real)) (=> (<= ?v0 ?v1) (<= (f3 f16 ?v0) (f3 f16 ?v1))))) +(assert (forall ((?v0 Real) (?v1 Real)) (=> (< ?v0 ?v1) (< (f3 f16 ?v0) (f3 f16 ?v1))))) +(assert (forall ((?v0 Real)) (let ((?v_0 0.0)) (=> (<= ?v_0 ?v0) (=> (= (f3 f16 ?v0) ?v_0) (= ?v0 ?v_0)))))) +(assert (forall ((?v0 Real)) (=> (< 0.0 ?v0) (< (/ ?v0 (f3 f16 2.0)) ?v0)))) +(assert (forall ((?v0 Real)) (let ((?v_0 0.0)) (=> (<= ?v_0 ?v0) (<= ?v_0 (f3 f16 ?v0)))))) +(assert (forall ((?v0 Real)) (let ((?v_0 1.0)) (=> (<= ?v_0 ?v0) (<= ?v_0 (f3 f16 ?v0)))))) +(check-sat) +(exit) -- 2.30.2