From a8c785aaadae1f5316e8e12455b362c468db4106 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 1 Jun 2018 15:29:05 -0500 Subject: [PATCH] Apply preprocessing to counterexample lemmas in CEGQI (#2027) --- .../quantifiers/cegqi/ceg_instantiator.cpp | 7 +- test/regress/Makefile.tests | 2 + .../regress1/quantifiers/015-psyco-pp.smt2 | 344 ++++++++++++++++++ .../quantifiers/smtcomp-qbv-053118.smt2 | 22 ++ 4 files changed, 373 insertions(+), 2 deletions(-) create mode 100644 test/regress/regress1/quantifiers/015-psyco-pp.smt2 create mode 100644 test/regress/regress1/quantifiers/smtcomp-qbv-053118.smt2 diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index 72633e86f..9dd0bdb04 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -1475,6 +1475,9 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st Trace("cbqi-debug") << "Counterexample lemma (pre-rewrite) " << i << " : " << lems[i] << std::endl; Node rlem = lems[i]; rlem = Rewriter::rewrite( rlem ); + // also must preprocess to ensure that the counterexample atoms we + // collect below are identical to the atoms that we add to the CNF stream + rlem = d_qe->getTheoryEngine()->preprocess(rlem); Trace("cbqi-debug") << "Counterexample lemma (post-rewrite) " << i << " : " << rlem << std::endl; //record the literals that imply auxiliary variables to be equal to terms if( lems[i].getKind()==ITE && rlem.getKind()==ITE ){ @@ -1498,7 +1501,6 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st }*/ lems[i] = rlem; } - // determine variable order: must do Reals before Ints Trace("cbqi-debug") << "Determine variable order..." << std::endl; if (!d_vars.empty()) @@ -1546,7 +1548,8 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st } } - //collect atoms from all lemmas: we will only do bounds coming from original body + // collect atoms from all lemmas: we will only solve for literals coming from + // the original body d_is_nested_quant = false; std::map< Node, bool > visited; for( unsigned i=0; i= + (ite MW_S1_V1 S1_V1_!5081 + (+ 1 (ite MW_S1_V1 S1_V1_!5076 (ite MW_S2_V1 S2_V1_!5071 V1_0)))) + (+ (- 1) (ite MW_S1_V2 S1_V2_!5079 (ite MW_S2_V2 S2_V2_!5069 V2_0)))))) + (let ((?x19970 (ite MW_S2_V1 S2_V1_!5071 V1_0))) + (let ((?x19876 (ite MW_S1_V1 S1_V1_!5076 ?x19970))) + (let ((?x20041 (+ 1 ?x19876))) + (let ((?x20154 (ite MW_S2_V2 S2_V2_!5069 V2_0))) + (let ((?x20275 (ite MW_S1_V2 S1_V2_!5074 ?x20154))) + (let + ((?x20280 + (+ (- 1) + (ite MW_S2_V2 S2_V2_!5064 + (ite MW_S1_V2 S1_V2_!5059 + (ite MW_S2_V2 S2_V2_!5054 (ite MW_S1_V2 S1_V2_!5049 V2_0))))))) + (let + (($x20340 + (and (not (<= V2_0 V1_0)) + (not + (<= (ite MW_S2_V2 S2_V2_!5054 (ite MW_S1_V2 S1_V2_!5049 V2_0)) ?x2666)) + (>= (ite MW_S2_V1 S2_V1_!5066 ?x19816) ?x20280) + (not (<= ?x20154 ?x19970)) + (not (<= ?x20275 ?x20041)) $x19175))) + (let (($x164 (not R_S1_V3))) + (let + (($x16591 + (or $x164 + (= (ite MW_S1_V3 S1_V3_!5075 (ite MW_S2_V3 S2_V3_!5070 V3_0)) + (ite MW_S2_V3 S2_V3_!5070 V3_0))))) + (let (($x160 (not R_S1_V5))) + (let + (($x4147 + (or $x160 + (= (ite MW_S1_V5 S1_V5_!5073 (ite MW_S2_V5 S2_V5_!5068 V5_0)) + (ite MW_S2_V5 S2_V5_!5068 V5_0))))) + (let + (($x20079 + (and $x4147 (or (not R_S1_V2) (= ?x20275 ?x20154)) $x16591 + (or (not R_S1_V1) (= ?x19876 (+ (- 1) ?x19970)))))) + (let (($x1365 (not $x20079))) + (let ((?x19329 (ite MW_S2_V3 S2_V3_!5070 V3_0))) + (let ((?x20227 (ite MW_S1_V3 S1_V3_!5075 ?x19329))) + (let + ((?x19017 (ite MW_S2_V3 S2_V3_!5055 (ite MW_S1_V3 S1_V3_!5050 V3_0)))) + (let ((?x19159 (ite MW_S2_V5 S2_V5_!5068 V5_0))) + (let ((?x19823 (ite MW_S1_V5 S1_V5_!5073 ?x19159))) + (let ((?x19445 (ite MW_S1_V5 S1_V5_!5048 V5_0))) + (let ((?x19140 (ite MW_S2_V5 S2_V5_!5053 ?x19445))) + (let + (($x20082 + (and (or $x160 (= ?x19140 ?x19823)) + (or (not R_S1_V2) + (= (ite MW_S2_V2 S2_V2_!5054 (ite MW_S1_V2 S1_V2_!5049 V2_0)) ?x20275)) + (or $x164 (= ?x19017 ?x20227)) + (or (not R_S1_V1) (= ?x19735 ?x19876))))) + (let (($x20074 (not $x20082))) + (let + (($x20083 + (and (or $x160 (= ?x19140 ?x19159)) + (or (not R_S1_V2) + (= (ite MW_S2_V2 S2_V2_!5054 (ite MW_S1_V2 S1_V2_!5049 V2_0)) ?x20154)) + (or $x164 (= ?x19017 ?x19329)) + (or (not R_S1_V1) (= ?x19735 (+ (- 1) ?x19970)))))) + (let (($x20084 (not $x20083))) + (let + (($x8373 + (and (or $x160 (= ?x19140 V5_0)) + (or (not R_S1_V2) + (= (ite MW_S2_V2 S2_V2_!5054 (ite MW_S1_V2 S1_V2_!5049 V2_0)) V2_0)) + (or $x164 (= ?x19017 V3_0)) + (or (not R_S1_V1) (= ?x19735 (+ (- 1) V1_0)))))) + (let (($x19787 (not $x8373))) + (let + (($x19719 + (and (or $x160 (= V5_0 ?x19823)) + (or (not R_S1_V2) (= V2_0 ?x20275)) + (or $x164 (= V3_0 ?x20227)) + (or (not R_S1_V1) (= V1_0 ?x20041))))) + (let (($x19712 (not $x19719))) + (let + (($x1403 + (and (or $x160 (= V5_0 ?x19159)) + (or (not R_S1_V2) (= V2_0 ?x20154)) + (or $x164 (= V3_0 ?x19329)) + (or (not R_S1_V1) (= V1_0 ?x19970))))) + (let (($x1473 (not $x1403))) + (let + (($x20361 + (and (or (not R_S2_V4) (= V4_0 (ite MW_S1_V4 S1_V4_!5047 V4_0))) + (or (not R_S2_V5) (= V5_0 ?x19445)) + (or (not R_S2_V2) (= V2_0 (ite MW_S1_V2 S1_V2_!5049 V2_0))) + (or (not R_S2_V1) (= V1_0 ?x19858))))) + (let (($x19974 (not $x20361))) + (let (($x175 (not R_S2_V2))) + (let + (($x19080 + (or $x175 + (= + (ite MW_S1_V2 S1_V2_!5059 + (ite MW_S2_V2 S2_V2_!5054 (ite MW_S1_V2 S1_V2_!5049 V2_0))) V2_0)))) + (let (($x171 (not R_S2_V4))) + (let + (($x1175 + (or $x171 + (= + (ite MW_S1_V4 S1_V4_!5057 + (ite MW_S2_V4 S2_V4_!5052 (ite MW_S1_V4 S1_V4_!5047 V4_0))) V4_0)))) + (let + (($x19801 + (and $x1175 + (or (not R_S2_V5) (= (ite MW_S1_V5 S1_V5_!5058 ?x19140) V5_0)) $x19080 + (or (not R_S2_V1) (= ?x19816 V1_0))))) + (let (($x19804 (not $x19801))) + (let ((?x10718 (ite MW_S1_V2 S1_V2_!5049 V2_0))) + (let ((?x18681 (ite MW_S2_V2 S2_V2_!5054 ?x10718))) + (let ((?x19161 (ite MW_S1_V2 S1_V2_!5059 ?x18681))) + (let ((?x19599 (ite MW_S1_V4 S1_V4_!5047 V4_0))) + (let + ((?x18788 (ite MW_S1_V4 S1_V4_!5057 (ite MW_S2_V4 S2_V4_!5052 ?x19599)))) + (let + (($x3852 + (and (or $x171 (= ?x18788 ?x19599)) + (or (not R_S2_V5) (= (ite MW_S1_V5 S1_V5_!5058 ?x19140) ?x19445)) + (or $x175 (= ?x19161 ?x10718)) + (or (not R_S2_V1) (= ?x19816 ?x19858))))) + (let (($x19708 (not $x3852))) + (let + (($x20195 + (and (or $x171 (= V4_0 ?x18788)) + (or (not R_S2_V5) (= V5_0 (ite MW_S1_V5 S1_V5_!5058 ?x19140))) + (or $x175 (= V2_0 ?x19161)) + (or (not R_S2_V1) (= V1_0 ?x19816))))) + (let + (($x1440 + (and (or $x160 (= ?x19823 ?x19140)) + (or (not R_S1_V2) (= ?x20275 ?x18681)) + (or $x164 (= ?x20227 ?x19017)) + (or (not R_S1_V1) (= ?x19876 ?x19735))))) + (let + (($x1199 + (and (or $x160 (= ?x19823 V5_0)) + (or (not R_S1_V2) (= ?x20275 V2_0)) + (or $x164 (= ?x20227 V3_0)) + (or (not R_S1_V1) (= ?x19876 (+ (- 1) V1_0)))))) + (let + (($x1442 + (and (or $x160 (= ?x19159 ?x19140)) + (or (not R_S1_V2) (= ?x20154 ?x18681)) + (or $x164 (= ?x19329 ?x19017)) + (or (not R_S1_V1) (= ?x19970 ?x2666))))) + (let + (($x1484 + (and (or $x160 (= V5_0 ?x19140)) + (or (not R_S1_V2) (= V2_0 ?x18681)) + (or $x164 (= V3_0 ?x19017)) + (or (not R_S1_V1) (= V1_0 ?x2666))))) + (let + (($x19714 + (and (or $x171 (= ?x19599 ?x18788)) + (or (not R_S2_V5) (= ?x19445 (ite MW_S1_V5 S1_V5_!5058 ?x19140))) + (or $x175 (= ?x10718 ?x19161)) + (or (not R_S2_V1) (= ?x19858 ?x19816))))) + (let + (($x20189 + (and (or $x160 (= ?x19159 ?x19823)) + (or (not R_S1_V2) (= ?x20154 ?x20275)) + (or $x164 (= ?x19329 ?x20227)) + (or (not R_S1_V1) (= ?x19970 ?x20041))))) + (let + (($x19788 + (and (or $x160 (= ?x19159 V5_0)) + (or (not R_S1_V2) (= ?x20154 V2_0)) + (or $x164 (= ?x19329 V3_0)) + (or (not R_S1_V1) (= ?x19970 V1_0))))) + (let + (($x1223 + (and (or $x19712 (= S1_V4_!5047 S1_V4_!5077)) + (or $x19787 (= S1_V4_!5057 S1_V4_!5047)) + (or $x20084 (= S1_V4_!5057 S1_V4_!5072)) + (or $x20074 (= S1_V4_!5057 S1_V4_!5077)) + (or (not $x19788) (= S1_V4_!5072 S1_V4_!5047)) + (or (not $x20189) (= S1_V4_!5072 S1_V4_!5077)) + (or $x19708 (= S2_V4_!5062 S2_V4_!5052)) + (or $x19804 (= S2_V4_!5062 S2_V4_!5067)) + (or $x19974 (= S2_V4_!5067 S2_V4_!5052)) + (or (not $x19714) (= S2_V5_!5053 S2_V5_!5063)) + (or $x19974 (= S2_V5_!5068 S2_V5_!5053)) + (or (not $x20195) (= S2_V5_!5068 S2_V5_!5063)) + (or $x1473 (= S1_V1_!5051 S1_V1_!5076)) + (or $x19712 (= S1_V1_!5051 S1_V1_!5081)) + (or $x19787 (= S1_V1_!5061 S1_V1_!5051)) + (or $x20084 (= S1_V1_!5061 S1_V1_!5076)) + (or $x20074 (= S1_V1_!5061 S1_V1_!5081)) + (or $x1365 (= S1_V1_!5081 S1_V1_!5076)) + (or (not $x1484) (= S1_V3_!5050 S1_V3_!5060)) + (or $x1473 (= S1_V3_!5050 S1_V3_!5075)) + (or $x19712 (= S1_V3_!5050 S1_V3_!5080)) + (or $x20084 (= S1_V3_!5060 S1_V3_!5075)) + (or (not $x1440) (= S1_V3_!5080 S1_V3_!5060)) + (or $x1365 (= S1_V3_!5080 S1_V3_!5075)) + (or (not $x1484) (= S1_V2_!5049 S1_V2_!5059)) + (or $x1473 (= S1_V2_!5049 S1_V2_!5074)) + (or (not $x1442) (= S1_V2_!5074 S1_V2_!5059)) + (or (not $x1199) (= S1_V2_!5079 S1_V2_!5049)) + (or (not $x1440) (= S1_V2_!5079 S1_V2_!5059)) + (or $x1365 (= S1_V2_!5079 S1_V2_!5074)) + (or $x19708 (= S2_V1_!5066 S2_V1_!5056)) + (or $x19974 (= S2_V1_!5071 S2_V1_!5056)) + (or (not $x20195) (= S2_V1_!5071 S2_V1_!5066)) + (or $x19708 (= S2_V2_!5064 S2_V2_!5054)) + (or $x19804 (= S2_V2_!5064 S2_V2_!5069)) + (or $x19974 (= S2_V2_!5069 S2_V2_!5054)) + (or $x19708 (= S2_V3_!5065 S2_V3_!5055)) + (or $x19804 (= S2_V3_!5065 S2_V3_!5070)) + (or $x19974 (= S2_V3_!5070 S2_V3_!5055)) + (or $x1473 (= S1_V5_!5048 S1_V5_!5073)) + (or $x19712 (= S1_V5_!5048 S1_V5_!5078)) + (or $x19787 (= S1_V5_!5058 S1_V5_!5048)) + (or $x20084 (= S1_V5_!5058 S1_V5_!5073)) + (or $x20074 (= S1_V5_!5058 S1_V5_!5078)) + (or $x1365 (= S1_V5_!5078 S1_V5_!5073)) + (not MW_S1_V4) (or (not MW_S1_V5) W_S1_V5) + (or (not MW_S1_V2) W_S1_V2) + (or (not MW_S1_V1) W_S1_V1) + (or (not MW_S2_V5) W_S2_V5) + (not MW_S2_V2) (not MW_S2_V3) + (not MW_S2_V1)))) + (or (not $x1223) (not $x20340) + (and $x19951 $x19917 $x19931 $x20397 $x19044))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + (let (($x158 (not R_S1_V4))) + (let (($x754 (not W_S1_V4))) + (let (($x23 (and W_S1_V1 R_S1_V1))) + (let (($x18 (and W_S1_V2 R_S1_V2))) + (let (($x15 (and W_S1_V5 R_S1_V5))) + (let (($x786 (not W_S2_V1))) + (let (($x783 (not W_S2_V2))) + (and DISJ_W_S1_R_S2 DISJ_W_S1_W_S2 DISJ_W_S2_R_S1 $x783 $x786 W_S1_V3 + W_S2_V4 (= DISJ_W_S1_R_S1 (not (or $x15 $x18 R_S1_V3 $x23))) $x754 $x158 + (= DISJ_W_S2_R_S2 (not (or R_S2_V4 (and W_S2_V5 R_S2_V5)))) $x1274 + (not (and W_S1_V5 R_S2_V5)) + (not (and W_S1_V2 R_S2_V2)) $x177 + (not (and W_S1_V1 R_S2_V1)) + (not (and W_S1_V5 W_S2_V5)) $x796 + (not (and W_S2_V5 R_S1_V5)))))))))))))) +(check-sat) +(exit) diff --git a/test/regress/regress1/quantifiers/smtcomp-qbv-053118.smt2 b/test/regress/regress1/quantifiers/smtcomp-qbv-053118.smt2 new file mode 100644 index 000000000..6cbe4db5c --- /dev/null +++ b/test/regress/regress1/quantifiers/smtcomp-qbv-053118.smt2 @@ -0,0 +1,22 @@ +(set-info :smt-lib-version 2.6) +(set-logic BV) +(set-info :status sat) +(declare-fun x () (_ BitVec 32)) +(assert +(forall ((u (_ BitVec 32)) (w (_ BitVec 32)) (z (_ BitVec 32)) (m (_ BitVec 32)) (n (_ BitVec 32))) (or + (not (= + (bvadd (bvmul (_ bv2 32) w) (bvmul (_ bv2 32) n)) + (bvadd (bvneg (bvadd (bvmul (_ bv2 32) u) (bvmul (_ bv2 32) z) (bvmul (_ bv2 32) m) x)) (_ bv1 32)) + )) +)) +) +(assert (not +(and + (forall ((m (_ BitVec 32)) (n (_ BitVec 32))) + (not (= + (bvadd (bvneg (bvadd m x)) (_ bv1 32)) + (bvmul (_ bv2 32) n) + )) +)))) +(check-sat) +(exit) -- 2.30.2