From 7acc2844df65ab6fdbf8166653c71eaa26d4d151 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 11 Feb 2016 15:07:37 -0600 Subject: [PATCH] More aggressive conditional rewriting for quantified formulas. Bug fix set incomplete for fmc. --- src/theory/quantifiers/full_model_check.cpp | 4 +- src/theory/quantifiers/quant_util.cpp | 3 + .../quantifiers/quantifiers_rewriter.cpp | 136 ++++-- test/regress/regress0/quantifiers/Makefile.am | 7 +- .../regress0/quantifiers/agg-rew-test-cf.smt2 | 5 + .../regress0/quantifiers/agg-rew-test.smt2 | 5 + .../regress0/quantifiers/psyco-196.smt2 | 420 ++++++++++++++++++ .../regress0/quantifiers/rew-to-0211-dd.smt2 | 259 +++++++++++ .../regress0/quantifiers/rew-to-scala.smt2 | 13 + 9 files changed, 805 insertions(+), 47 deletions(-) create mode 100644 test/regress/regress0/quantifiers/agg-rew-test-cf.smt2 create mode 100644 test/regress/regress0/quantifiers/agg-rew-test.smt2 create mode 100644 test/regress/regress0/quantifiers/psyco-196.smt2 create mode 100644 test/regress/regress0/quantifiers/rew-to-0211-dd.smt2 create mode 100644 test/regress/regress0/quantifiers/rew-to-scala.smt2 diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 00a5241f5..ff0da13e1 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -819,8 +819,8 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No } } d_addedLemmas += addedLemmas; - Trace("fmc-exh") << "----Finished Exhaustive instantiate, lemmas = " << addedLemmas << std::endl; - return true; + Trace("fmc-exh") << "----Finished Exhaustive instantiate, lemmas = " << addedLemmas << ", incomplete=" << riter.d_incomplete << std::endl; + return addedLemmas>0 || !riter.d_incomplete; }else{ Trace("fmc-exh") << "----Finished Exhaustive instantiate, failed." << std::endl; return false; diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index fc1f052c3..bf91f74c6 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -349,6 +349,9 @@ void QuantPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool& }else if( n.getKind()==ITE ){ newHasPol = (child!=0) && hasPol; newPol = pol; + }else if( n.getKind()==FORALL ){ + newHasPol = (child==1) && hasPol; + newPol = pol; }else{ newHasPol = false; newPol = pol; diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 462f8377f..afe8cd598 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -391,7 +391,7 @@ Node QuantifiersRewriter::computeNNF( Node body ){ void QuantifiersRewriter::computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons, std::vector< Node >& conj ){ if( n.getKind()==ITE && n[0].getKind()==APPLY_TESTER && n[1].getType().isBoolean() ){ - Trace("quantifiers-rewrite-ite-debug") << "Split tester condition : " << n << std::endl; + Trace("quantifiers-rewrite-ite-debug") << "Split tester condition : " << n << std::endl; Node x = n[0][0]; std::map< Node, Node >::iterator itp = pcons.find( x ); if( itp!=pcons.end() ){ @@ -506,35 +506,42 @@ int getEntailedCond( Node n, std::map< Node, bool >& currCond ){ return 0; } -bool addEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::vector< Node >& new_cond ) { +bool addEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::vector< Node >& new_cond, bool& conflict ) { std::map< Node, bool >::iterator it = currCond.find( n ); if( it==currCond.end() ){ - Trace("quantifiers-rewrite-ite-debug") << "ITE cond : " << n << " -> " << pol << std::endl; + Trace("quantifiers-rewrite-term-debug") << "cond : " << n << " -> " << pol << std::endl; new_cond.push_back( n ); currCond[n] = pol; return true; }else{ - Assert( it->second==pol ); + if( it->second!=pol ){ + Trace("quantifiers-rewrite-term-debug") << "CONFLICTING cond : " << n << " -> " << pol << std::endl; + conflict = true; + } return false; } } -void setEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::vector< Node >& new_cond ) { +void setEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::vector< Node >& new_cond, bool& conflict ) { if( ( n.getKind()==AND && pol ) || ( n.getKind()==OR && !pol ) ){ for( unsigned i=0; i& currCond, std::v for( unsigned i=0; imkNode( APPLY_TESTER, Node::fromExpr( dt[i].getTester() ), n[0] ); - addEntailedCond( t, false, currCond, new_cond ); + addEntailedCond( t, false, currCond, new_cond, conflict ); } } }else{ if( dt.getNumConstructors()==2 ){ int oindex = 1-index; Node t = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[oindex].getTester() ), n[0] ); - addEntailedCond( t, true, currCond, new_cond ); + addEntailedCond( t, true, currCond, new_cond, conflict ); } } } @@ -577,59 +584,100 @@ Node QuantifiersRewriter::computeProcessTerms( Node body, std::vector< Node >& n Node QuantifiersRewriter::computeProcessTerms2( Node body, bool hasPol, bool pol, std::map< Node, bool >& currCond, int nCurrCond, std::map< Node, Node >& cache, std::map< Node, Node >& icache, std::vector< Node >& new_vars, std::vector< Node >& new_conds ) { + Trace("quantifiers-rewrite-term-debug2") << "computeProcessTerms " << body << " " << hasPol << " " << pol << std::endl; Node ret; std::map< Node, Node >::iterator iti = cache.find( body ); if( iti!=cache.end() ){ ret = iti->second; + Trace("quantifiers-rewrite-term-debug2") << "Return (cached) " << ret << " for " << body << std::endl; }else{ - bool do_ite = false; - //only do context dependent processing up to ITE depth 8 - if( body.getKind()==ITE && nCurrCond<8 ){ - do_ite = true; - nCurrCond = nCurrCond + 1; - } + bool firstTimeCD = true; bool changed = false; std::vector< Node > children; for( size_t i=0; i new_cond; - if( do_ite && i>0 ){ - setEntailedCond( children[0], i==1, currCond, new_cond ); - cache.clear(); + bool conflict = false; + //only do context dependent processing up to depth 8 + if( nCurrCond<8 ){ + if( firstTimeCD ){ + firstTimeCD = false; + nCurrCond = nCurrCond + 1; + } + if( Trace.isOn("quantifiers-rewrite-term-debug") ){ + //if( ( body.getKind()==ITE && i>0 ) || ( hasPol && ( ( body.getKind()==OR && pol ) || (body.getKind()==AND && !pol ) ) ) ){ + if( ( body.getKind()==ITE && i>0 ) || body.getKind()==OR || body.getKind()==AND ){ + Trace("quantifiers-rewrite-term-debug") << "---rewrite " << body[i] << " under conditions:----" << std::endl; + } + } + if( body.getKind()==ITE && i>0 ){ + setEntailedCond( children[0], i==1, currCond, new_cond, conflict ); + //should not conflict (entailment check failed) + Assert( !conflict ); + } + //if( hasPol && ( ( body.getKind()==OR && pol ) || ( body.getKind()==AND && !pol ) ) ){ + // bool use_pol = !pol; + if( body.getKind()==OR || body.getKind()==AND ){ + bool use_pol = body.getKind()==AND; + for( unsigned j=0; ji ){ + setEntailedCond( body[j], use_pol, currCond, new_cond, conflict ); + } + } + if( conflict ){ + Trace("quantifiers-rewrite-term-debug") << "-------conflict, return " << !use_pol << std::endl; + ret = NodeManager::currentNM()->mkConst( !use_pol ); + } + } + if( !new_cond.empty() ){ + cache.clear(); + } + if( Trace.isOn("quantifiers-rewrite-term-debug") ){ + //if( ( body.getKind()==ITE && i>0 ) || ( hasPol && ( ( body.getKind()==OR && pol ) || (body.getKind()==AND && !pol ) ) ) ){ + if( ( body.getKind()==ITE && i>0 ) || body.getKind()==OR || body.getKind()==AND ){ + Trace("quantifiers-rewrite-term-debug") << "-------" << std::endl; + } + } } - bool newHasPol; - bool newPol; - QuantPhaseReq::getPolarity( body, i, hasPol, pol, newHasPol, newPol ); - Node nn = computeProcessTerms2( body[i], newHasPol, newPol, currCond, nCurrCond, cache, icache, new_vars, new_conds ); - if( body.getKind()==ITE ){ - if( i==0 ){ + if( !conflict ){ + bool newHasPol; + bool newPol; + QuantPhaseReq::getPolarity( body, i, hasPol, pol, newHasPol, newPol ); + Node nn = computeProcessTerms2( body[i], newHasPol, newPol, currCond, nCurrCond, cache, icache, new_vars, new_conds ); + if( body.getKind()==ITE && i==0 ){ int res = getEntailedCond( nn, currCond ); + Trace("quantifiers-rewrite-term-debug") << "Condition for " << body << " is " << nn << ", entailment check=" << res << std::endl; if( res==1 ){ ret = computeProcessTerms2( body[1], hasPol, pol, currCond, nCurrCond, cache, icache, new_vars, new_conds ); - break; }else if( res==-1 ){ ret = computeProcessTerms2( body[2], hasPol, pol, currCond, nCurrCond, cache, icache, new_vars, new_conds ); - break; - } - }else{ - if( !new_cond.empty() ){ - for( unsigned j=0; jmkNode( body.getKind(), children ); + }else{ + ret = body; } - ret = NodeManager::currentNM()->mkNode( body.getKind(), children ); - }else{ - ret = body; } + Trace("quantifiers-rewrite-term-debug2") << "Returning " << ret << " for " << body << std::endl; cache[body] = ret; } diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index 3fff9b0de..df146752e 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -65,7 +65,12 @@ TESTS = \ ext-ex-deq-trigger.smt2 \ matching-lia-1arg.smt2 \ RND_4_16.smt2 \ - cdt-0208-to.smt2 + cdt-0208-to.smt2 \ + psyco-196.smt2 \ + agg-rew-test.smt2 \ + agg-rew-test-cf.smt2 \ + rew-to-0211-dd.smt2 \ + rew-to-scala.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine diff --git a/test/regress/regress0/quantifiers/agg-rew-test-cf.smt2 b/test/regress/regress0/quantifiers/agg-rew-test-cf.smt2 new file mode 100644 index 000000000..44f475d83 --- /dev/null +++ b/test/regress/regress0/quantifiers/agg-rew-test-cf.smt2 @@ -0,0 +1,5 @@ +(set-logic UFLIA) +(set-info :status sat) +(declare-fun Q (Int Int) Bool) +(assert (forall ((x Int)) (or (and (or (Q 0 x) (Q 1 x)) (Q 2 x)) (not (Q 2 x)) (not (Q 1 x))))) +(check-sat) diff --git a/test/regress/regress0/quantifiers/agg-rew-test.smt2 b/test/regress/regress0/quantifiers/agg-rew-test.smt2 new file mode 100644 index 000000000..d1159278e --- /dev/null +++ b/test/regress/regress0/quantifiers/agg-rew-test.smt2 @@ -0,0 +1,5 @@ +(set-logic UFLIA) +(set-info :status sat) +(declare-fun Q (Int Int) Bool) +(assert (forall ((x Int)) (=> (Q 0 x) (or (ite (Q 0 x) (not (Q 2 x)) (Q 3 x)) (Q 2 x))))) +(check-sat) diff --git a/test/regress/regress0/quantifiers/psyco-196.smt2 b/test/regress/regress0/quantifiers/psyco-196.smt2 new file mode 100644 index 000000000..356e62752 --- /dev/null +++ b/test/regress/regress0/quantifiers/psyco-196.smt2 @@ -0,0 +1,420 @@ +(set-logic LIA) +(set-info :status sat) +(declare-fun W_S1_V5 () Bool) +(declare-fun W_S1_V4 () Bool) +(declare-fun W_S1_V6 () Bool) +(declare-fun W_S1_V1 () Bool) +(declare-fun W_S1_V3 () Bool) +(declare-fun W_S1_V2 () Bool) +(declare-fun R_S1_V5 () Bool) +(declare-fun R_S1_V4 () Bool) +(declare-fun R_S1_V6 () Bool) +(declare-fun R_S1_V1 () Bool) +(declare-fun R_S1_V3 () Bool) +(declare-fun R_S1_V2 () Bool) +(declare-fun R_E2_V1 () Bool) +(declare-fun R_E1_V1 () Bool) +(declare-fun R_E1_V3 () Bool) +(declare-fun R_E2_V3 () Bool) +(assert + (let + (($x62242 + (forall + ((V2_0 Int) (V6_0 Int) + (V4_0 Int) (V5_0 Int) + (S1_V3_!5556 Int) (S1_V3_!5562 Int) + (S1_V3_!5571 Int) (S1_V3_!5577 Int) + (E1_!5552 Int) (E1_!5567 Int) + (E1_!5569 Int) (S1_V2_!5555 Int) + (S1_V2_!5561 Int) (S1_V2_!5570 Int) + (S1_V2_!5576 Int) (S1_V5_!5560 Int) + (S1_V5_!5566 Int) (S1_V5_!5575 Int) + (S1_V5_!5581 Int) (S1_V4_!5559 Int) + (S1_V4_!5565 Int) (S1_V4_!5574 Int) + (S1_V4_!5580 Int) (S1_V6_!5558 Int) + (S1_V6_!5564 Int) (S1_V6_!5573 Int) + (S1_V6_!5579 Int) (E2_!5553 Int) + (E2_!5554 Int) (E2_!5568 Int) + (S1_V1_!5557 Int) (S1_V1_!5563 Int) + (S1_V1_!5572 Int) (S1_V1_!5578 Int)) + (let (($x59864 (= S1_V5_!5566 S1_V5_!5581))) + (let (($x59925 (not W_S1_V5))) + (let (($x62779 (or $x59925 $x59864))) + (let (($x62200 (= S1_V4_!5565 S1_V4_!5580))) + (let (($x59923 (not W_S1_V4))) + (let (($x62447 (or $x59923 $x62200))) + (let (($x62602 (= S1_V6_!5564 S1_V6_!5579))) + (let (($x62610 (not W_S1_V6))) + (let (($x62230 (or $x62610 $x62602))) + (let (($x61214 (= S1_V1_!5563 S1_V1_!5578))) + (let (($x60986 (= S1_V3_!5562 S1_V3_!5577))) + (let (($x62444 (= S1_V2_!5561 S1_V2_!5576))) + (let (($x62507 (not W_S1_V2))) + (let (($x62441 (or $x62507 $x62444))) + (let + (($x62532 + (and $x62441 + (ite W_S1_V3 $x60986 + (= (ite W_S1_V3 S1_V3_!5556 E2_!5554) (+ (- 1) E2_!5568))) + (ite W_S1_V1 $x61214 + (= E1_!5552 (+ 1 (ite W_S1_V1 S1_V1_!5572 E1_!5569)))) $x62230 $x62447 + $x62779))) + (let ((?x62367 (ite W_S1_V1 S1_V1_!5572 E1_!5569))) + (let ((?x60865 (+ 1 ?x62367))) + (let ((?x62511 (ite W_S1_V1 S1_V1_!5578 ?x60865))) + (let ((?x60218 (ite W_S1_V3 S1_V3_!5556 E2_!5554))) + (let ((?x60222 (+ 1 ?x60218))) + (let ((?x62533 (ite W_S1_V3 S1_V3_!5562 ?x60222))) + (let + (($x62746 + (and (not (<= V4_0 E2_!5553)) + (not (<= V2_0 E1_!5552)) + (not (<= V4_0 E2_!5554)) + (not (<= (ite W_S1_V4 S1_V4_!5559 V4_0) ?x60222)) + (>= ?x62533 (+ (- 1) (ite W_S1_V4 S1_V4_!5565 V4_0))) + (>= (ite W_S1_V1 S1_V1_!5563 E1_!5552) + (+ (- 1) (ite W_S1_V2 S1_V2_!5561 V2_0))) + (not (<= V2_0 E1_!5567)) + (not (<= V4_0 E2_!5568)) + (not (<= V2_0 E1_!5569)) + (not (<= (ite W_S1_V2 S1_V2_!5570 V2_0) ?x60865)) + (>= ?x62511 (+ (- 1) (ite W_S1_V2 S1_V2_!5576 V2_0))) + (>= (ite W_S1_V3 S1_V3_!5577 E2_!5568) + (+ (- 1) (ite W_S1_V4 S1_V4_!5580 V4_0)))))) + (let (($x62780 (= S1_V1_!5578 S1_V1_!5572))) + (let (($x161 (not R_S1_V5))) + (let (($x62589 (or $x161 (= (ite W_S1_V5 S1_V5_!5575 V5_0) V5_0)))) + (let (($x159 (not R_S1_V4))) + (let (($x62548 (or $x159 (= (ite W_S1_V4 S1_V4_!5574 V4_0) V4_0)))) + (let (($x157 (not R_S1_V6))) + (let (($x62737 (or $x157 (= (ite W_S1_V6 S1_V6_!5573 V6_0) V6_0)))) + (let (($x153 (not R_S1_V3))) + (let + (($x62224 (or $x153 (= (ite W_S1_V3 S1_V3_!5571 E2_!5568) E2_!5568)))) + (let (($x151 (not R_S1_V2))) + (let (($x62641 (or $x151 (= (ite W_S1_V2 S1_V2_!5570 V2_0) V2_0)))) + (let + (($x60228 + (and $x62641 $x62224 + (or (not R_S1_V1) (= ?x62367 (+ (- 1) E1_!5569))) $x62737 $x62548 + $x62589))) + (let (($x62356 (not $x60228))) + (let (($x62680 (= S1_V1_!5578 S1_V1_!5563))) + (let (($x62272 (or $x161 $x59925 (= S1_V5_!5575 S1_V5_!5560)))) + (let (($x61083 (= S1_V4_!5574 S1_V4_!5559))) + (let (($x62455 (or $x159 $x59923 $x61083))) + (let (($x60917 (= S1_V6_!5573 S1_V6_!5558))) + (let (($x62584 (or $x157 $x62610 $x60917))) + (let (($x59905 (= S1_V2_!5570 S1_V2_!5555))) + (let (($x62549 (or $x151 $x62507 $x59905))) + (let + (($x62675 + (and $x62549 (or $x153 (= (ite W_S1_V3 S1_V3_!5571 E2_!5568) ?x60222)) + (or (not R_S1_V1) + (= ?x62367 (+ (- 1) (ite W_S1_V1 S1_V1_!5557 E1_!5552)))) $x62584 + $x62455 $x62272))) + (let (($x59892 (= S1_V1_!5578 S1_V1_!5557))) + (let + (($x60942 (or $x153 (= (ite W_S1_V3 S1_V3_!5571 E2_!5568) E2_!5554)))) + (let + (($x62564 + (and $x62641 $x60942 + (or (not R_S1_V1) (= ?x62367 (+ (- 1) E1_!5552))) $x62737 $x62548 + $x62589))) + (let (($x59819 (not $x62564))) + (let (($x60234 (= S1_V1_!5563 S1_V1_!5572))) + (let (($x61232 (or $x161 (= (ite W_S1_V5 S1_V5_!5560 V5_0) V5_0)))) + (let (($x61254 (or $x159 (= (ite W_S1_V4 S1_V4_!5559 V4_0) V4_0)))) + (let (($x59994 (or $x157 (= (ite W_S1_V6 S1_V6_!5558 V6_0) V6_0)))) + (let (($x155 (not R_S1_V1))) + (let + (($x62420 (or $x155 (= (ite W_S1_V1 S1_V1_!5557 E1_!5552) E1_!5569)))) + (let (($x62368 (or $x151 (= (ite W_S1_V2 S1_V2_!5555 V2_0) V2_0)))) + (let + (($x62830 + (not + (and $x62368 (or $x153 (= ?x60218 (+ (- 1) E2_!5568))) $x62420 $x59994 + $x61254 $x61232)))) + (let (($x62636 (= S1_V1_!5563 S1_V1_!5557))) + (let + (($x59733 (or $x155 (= (ite W_S1_V1 S1_V1_!5557 E1_!5552) E1_!5552)))) + (let + (($x62306 + (not + (and $x62368 (or $x153 (= ?x60218 (+ (- 1) E2_!5554))) $x59733 $x59994 + $x61254 $x61232)))) + (let (($x60134 (= S1_V1_!5557 S1_V1_!5572))) + (let + (($x59719 + (not + (and (or $x153 (= E2_!5554 E2_!5568)) (or $x155 (= E1_!5552 E1_!5569)))))) + (let (($x61406 (= E2_!5554 E2_!5568))) + (let (($x59878 (not (or (not R_E2_V1) (= E1_!5552 E1_!5567))))) + (let (($x59949 (or $x59878 $x61406))) + (let (($x62775 (or $x59878 (= E2_!5553 E2_!5568)))) + (let (($x59743 (= E2_!5553 E2_!5554))) + (let (($x62428 (= S1_V6_!5573 S1_V6_!5579))) + (let (($x60152 (or $x161 (= V5_0 (ite W_S1_V5 S1_V5_!5575 V5_0))))) + (let (($x60212 (or $x159 (= V4_0 (ite W_S1_V4 S1_V4_!5574 V4_0))))) + (let (($x61260 (or $x157 (= V6_0 (ite W_S1_V6 S1_V6_!5573 V6_0))))) + (let + (($x60887 (or $x153 (= E2_!5568 (ite W_S1_V3 S1_V3_!5571 E2_!5568))))) + (let (($x62275 (or $x151 (= V2_0 (ite W_S1_V2 S1_V2_!5570 V2_0))))) + (let + (($x61258 + (or + (not + (and $x62275 $x60887 + (or $x155 (= E1_!5569 ?x60865)) $x61260 $x60212 $x60152)) $x62428))) + (let + (($x61266 + (not + (and (or $x153 (= E2_!5568 E2_!5554)) (or $x155 (= E1_!5569 E1_!5552)))))) + (let (($x61122 (= S1_V5_!5560 S1_V5_!5575))) + (let (($x59790 (or $x161 $x59925 $x61122))) + (let (($x62797 (or $x159 $x59923 (= S1_V4_!5559 S1_V4_!5574)))) + (let (($x62684 (or $x157 $x62610 (= S1_V6_!5558 S1_V6_!5573)))) + (let (($x62354 (or $x151 $x62507 (= S1_V2_!5555 S1_V2_!5570)))) + (let + (($x60910 + (and $x62354 + (or $x153 (= ?x60218 (+ (- 1) (ite W_S1_V3 S1_V3_!5571 E2_!5568)))) + (or $x155 (= (ite W_S1_V1 S1_V1_!5557 E1_!5552) ?x60865)) $x62684 + $x62797 $x59790))) + (let (($x59844 (not $x60910))) + (let (($x62494 (= S1_V5_!5560 S1_V5_!5581))) + (let + (($x62623 (or $x153 (= E2_!5554 (ite W_S1_V3 S1_V3_!5571 E2_!5568))))) + (let + (($x61100 + (or + (not + (and $x62275 $x62623 + (or $x155 (= E1_!5552 ?x60865)) $x61260 $x60212 $x60152)) $x62494))) + (let (($x60862 (= S1_V5_!5560 S1_V5_!5566))) + (let (($x62353 (or $x161 (= V5_0 (ite W_S1_V5 S1_V5_!5560 V5_0))))) + (let (($x60875 (or $x159 (= V4_0 (ite W_S1_V4 S1_V4_!5559 V4_0))))) + (let (($x62491 (or $x157 (= V6_0 (ite W_S1_V6 S1_V6_!5558 V6_0))))) + (let + (($x62399 (or $x155 (= E1_!5552 (ite W_S1_V1 S1_V1_!5557 E1_!5552))))) + (let (($x62431 (or $x151 (= V2_0 (ite W_S1_V2 S1_V2_!5555 V2_0))))) + (let + (($x62297 + (or + (not + (and $x62431 (or $x153 (= E2_!5554 ?x60222)) $x62399 $x62491 $x60875 + $x62353)) $x60862))) + (let (($x60874 (= S1_V2_!5570 S1_V2_!5576))) + (let + (($x62369 + (or + (not + (and $x62275 $x60887 + (or $x155 (= E1_!5569 ?x60865)) $x61260 $x60212 $x60152)) $x60874))) + (let (($x62594 (= S1_V2_!5555 S1_V2_!5576))) + (let + (($x59910 + (or + (not + (and $x62275 $x62623 + (or $x155 (= E1_!5552 ?x60865)) $x61260 $x60212 $x60152)) $x62594))) + (let (($x62531 (= E1_!5569 E1_!5567))) + (let (($x59835 (= E1_!5552 E1_!5569))) + (let (($x62312 (= E1_!5552 E1_!5567))) + (let + (($x62715 + (and (or $x59719 (= S1_V3_!5556 S1_V3_!5571)) + (or $x62306 (= S1_V3_!5562 S1_V3_!5556)) + (or $x62830 (= S1_V3_!5562 S1_V3_!5571)) + (or $x59819 (= S1_V3_!5577 S1_V3_!5556)) + (or (not $x62675) (= S1_V3_!5577 S1_V3_!5562)) + (or $x62356 (= S1_V3_!5577 S1_V3_!5571)) $x62312 $x59835 $x62531 + $x59910 (or $x62306 (= S1_V2_!5561 S1_V2_!5555)) + (or $x62830 (= S1_V2_!5561 S1_V2_!5570)) + (or $x59844 $x62444) + (or $x61266 $x59905) $x62369 $x62297 + (or $x59719 $x61122) $x61100 + (or $x62830 (= S1_V5_!5566 S1_V5_!5575)) + (or $x59844 $x59864) + (or $x62356 (= S1_V5_!5581 S1_V5_!5575)) + (or $x62306 (= S1_V4_!5565 S1_V4_!5559)) + (or $x62830 (= S1_V4_!5565 S1_V4_!5574)) + (or $x59844 $x62200) + (or $x61266 $x61083) + (or $x59819 (= S1_V4_!5580 S1_V4_!5559)) + (or $x62356 (= S1_V4_!5580 S1_V4_!5574)) + (or $x62306 (= S1_V6_!5564 S1_V6_!5558)) + (or $x62830 (= S1_V6_!5564 S1_V6_!5573)) + (or $x59844 $x62602) + (or $x61266 $x60917) $x61258 + (or $x59819 (= S1_V6_!5579 S1_V6_!5558)) $x59743 $x62775 $x59949 + (or $x59719 $x60134) + (or $x62306 $x62636) + (or $x62830 $x60234) + (or $x59819 $x59892) + (or (not $x62675) $x62680) + (or $x62356 $x62780)))) + (or (not $x62715) (not $x62746) $x62532))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + (let (($x13 (or W_S1_V2 W_S1_V3 W_S1_V1 W_S1_V6 W_S1_V4 W_S1_V5))) + (let (($x65 (not R_E1_V1))) + (let (($x63 (not R_E1_V3))) + (let (($x84 (not R_E2_V3))) (and $x84 $x63 $x65 $x13 $x62242))))))) +(assert (not (and (not W_S1_V4) (not W_S1_V3)))) +(assert (not (and (not W_S1_V1) (not W_S1_V2)))) +(assert (not (and (not R_S1_V3) (not R_S1_V1) (not W_S1_V4) (not W_S1_V2)))) +(assert + (let (($x62714 (not W_S1_V3))) + (let (($x161 (not R_S1_V5))) + (let (($x159 (not R_S1_V4))) + (let (($x157 (not R_S1_V6))) + (let (($x155 (not R_S1_V1))) + (let (($x151 (not R_S1_V2))) + (not (and $x151 $x155 $x157 $x159 $x161 $x62714))))))))) +(assert + (let (($x62610 (not W_S1_V6))) + (let (($x62507 (not W_S1_V2))) + (let (($x59925 (not W_S1_V5))) + (let (($x159 (not R_S1_V4))) + (let (($x155 (not R_S1_V1))) + (let (($x153 (not R_S1_V3))) + (not (and $x153 $x155 $x159 $x59925 $x62507 $x62610))))))))) +(assert + (let (($x161 (not R_S1_V5))) + (let (($x159 (not R_S1_V4))) + (let (($x157 (not R_S1_V6))) + (let (($x155 (not R_S1_V1))) + (let (($x153 (not R_S1_V3))) + (let (($x151 (not R_S1_V2))) + (not (and $x151 $x153 $x155 $x157 $x159 $x161))))))))) +(assert (not (and W_S1_V3 (not R_S1_V3) (not R_S1_V1) (not W_S1_V2)))) +(assert (not (and W_S1_V3 W_S1_V1 (not R_S1_V3) (not R_S1_V1)))) +(assert + (let (($x62232 (not W_S1_V1))) + (let (($x59925 (not W_S1_V5))) + (let (($x159 (not R_S1_V4))) + (let (($x157 (not R_S1_V6))) + (let (($x153 (not R_S1_V3))) + (let (($x151 (not R_S1_V2))) + (not (and $x151 $x153 $x157 $x159 $x59925 $x62232))))))))) +(assert + (let (($x62610 (not W_S1_V6))) + (let (($x62232 (not W_S1_V1))) + (let (($x59925 (not W_S1_V5))) + (let (($x159 (not R_S1_V4))) + (let (($x153 (not R_S1_V3))) + (let (($x151 (not R_S1_V2))) + (not (and $x151 $x153 $x159 $x59925 $x62232 $x62610))))))))) +(assert + (let (($x62610 (not W_S1_V6))) + (let (($x59923 (not W_S1_V4))) + (let (($x161 (not R_S1_V5))) + (let (($x155 (not R_S1_V1))) + (let (($x153 (not R_S1_V3))) + (let (($x151 (not R_S1_V2))) + (not (and $x151 $x153 $x155 $x161 $x59923 $x62610))))))))) +(assert + (let (($x62610 (not W_S1_V6))) + (let (($x62232 (not W_S1_V1))) + (let (($x161 (not R_S1_V5))) + (let (($x159 (not R_S1_V4))) + (let (($x153 (not R_S1_V3))) + (let (($x151 (not R_S1_V2))) + (not (and $x151 $x153 $x159 $x161 $x62232 $x62610))))))))) +(assert + (let (($x62232 (not W_S1_V1))) + (let (($x59925 (not W_S1_V5))) + (let (($x59923 (not W_S1_V4))) + (let (($x157 (not R_S1_V6))) + (let (($x153 (not R_S1_V3))) + (let (($x151 (not R_S1_V2))) + (not (and $x151 $x153 $x157 $x59923 $x59925 $x62232))))))))) +(assert + (let (($x62610 (not W_S1_V6))) + (let (($x59925 (not W_S1_V5))) + (let (($x59923 (not W_S1_V4))) + (let (($x155 (not R_S1_V1))) + (let (($x153 (not R_S1_V3))) + (let (($x151 (not R_S1_V2))) + (not (and $x151 $x153 $x155 $x59923 $x59925 $x62610))))))))) +(assert + (let (($x59923 (not W_S1_V4))) + (let (($x161 (not R_S1_V5))) + (let (($x157 (not R_S1_V6))) + (let (($x155 (not R_S1_V1))) + (let (($x153 (not R_S1_V3))) + (let (($x151 (not R_S1_V2))) + (not (and $x151 $x153 $x155 $x157 $x161 $x59923))))))))) +(assert + (let (($x62232 (not W_S1_V1))) + (let (($x59923 (not W_S1_V4))) + (let (($x161 (not R_S1_V5))) + (let (($x157 (not R_S1_V6))) + (let (($x153 (not R_S1_V3))) + (let (($x151 (not R_S1_V2))) + (not (and $x151 $x153 $x157 $x161 $x59923 $x62232))))))))) +(assert + (let (($x62714 (not W_S1_V3))) + (let (($x62507 (not W_S1_V2))) + (let (($x161 (not R_S1_V5))) + (let (($x159 (not R_S1_V4))) + (let (($x157 (not R_S1_V6))) + (let (($x155 (not R_S1_V1))) + (not (and $x155 $x157 $x159 $x161 $x62507 $x62714))))))))) +(assert + (let (($x62714 (not W_S1_V3))) + (let (($x62610 (not W_S1_V6))) + (let (($x161 (not R_S1_V5))) + (let (($x159 (not R_S1_V4))) + (let (($x155 (not R_S1_V1))) + (let (($x151 (not R_S1_V2))) + (not (and $x151 $x155 $x159 $x161 $x62610 $x62714))))))))) +(assert + (let (($x62714 (not W_S1_V3))) + (let (($x62610 (not W_S1_V6))) + (let (($x62507 (not W_S1_V2))) + (let (($x161 (not R_S1_V5))) + (let (($x159 (not R_S1_V4))) + (let (($x155 (not R_S1_V1))) + (not (and $x155 $x159 $x161 $x62507 $x62610 $x62714))))))))) +(assert + (let (($x62714 (not W_S1_V3))) + (let (($x59925 (not W_S1_V5))) + (let (($x159 (not R_S1_V4))) + (let (($x157 (not R_S1_V6))) + (let (($x155 (not R_S1_V1))) + (let (($x151 (not R_S1_V2))) + (not (and $x151 $x155 $x157 $x159 $x59925 $x62714))))))))) +(assert + (let (($x62714 (not W_S1_V3))) + (let (($x62507 (not W_S1_V2))) + (let (($x59925 (not W_S1_V5))) + (let (($x159 (not R_S1_V4))) + (let (($x157 (not R_S1_V6))) + (let (($x155 (not R_S1_V1))) + (not (and $x155 $x157 $x159 $x59925 $x62507 $x62714))))))))) +(assert + (let (($x62714 (not W_S1_V3))) + (let (($x62610 (not W_S1_V6))) + (let (($x59925 (not W_S1_V5))) + (let (($x159 (not R_S1_V4))) + (let (($x155 (not R_S1_V1))) + (let (($x151 (not R_S1_V2))) + (not (and $x151 $x155 $x159 $x59925 $x62610 $x62714))))))))) +(assert + (let (($x62714 (not W_S1_V3))) + (let (($x62610 (not W_S1_V6))) + (let (($x62507 (not W_S1_V2))) + (let (($x59925 (not W_S1_V5))) + (let (($x159 (not R_S1_V4))) + (let (($x155 (not R_S1_V1))) + (not (and $x155 $x159 $x59925 $x62507 $x62610 $x62714))))))))) +(assert + (let (($x62232 (not W_S1_V1))) + (let (($x161 (not R_S1_V5))) + (let (($x159 (not R_S1_V4))) + (let (($x157 (not R_S1_V6))) + (let (($x153 (not R_S1_V3))) + (let (($x151 (not R_S1_V2))) + (not (and $x151 $x153 $x157 $x159 $x161 $x62232))))))))) +(check-sat) + diff --git a/test/regress/regress0/quantifiers/rew-to-0211-dd.smt2 b/test/regress/regress0/quantifiers/rew-to-0211-dd.smt2 new file mode 100644 index 000000000..ec49231e3 --- /dev/null +++ b/test/regress/regress0/quantifiers/rew-to-0211-dd.smt2 @@ -0,0 +1,259 @@ +(set-logic UFLIA) +(set-info :smt-lib-version 2.0) +(set-info :category "industrial") +(set-info :status unsat) +(declare-fun boolIff (Int Int) Int) +(declare-fun PeerGroupPlaceholder_ () Int) +(declare-fun intGreater (Int Int) Int) +(declare-fun IfThenElse_ (Int Int Int) Int) +(declare-fun System.IConvertible () Int) +(declare-fun CONCVARSYM (Int) Int) +(declare-fun throwException_in () Int) +(declare-fun SharingMode_Unshared_ () Int) +(declare-fun System.Reflection.IReflect () Int) +(declare-fun result_0_ () Int) +(declare-fun block3502_2_block3553_correct () Int) +(declare-fun int_m2147483648 () Int) +(declare-fun local0_0 () Int) +(declare-fun System.Int32 () Int) +(declare-fun local0_1 () Int) +(declare-fun block3536_2_block3553_correct () Int) +(declare-fun block3553_correct () Int) +(declare-fun intAtMost (Int Int) Int) +(declare-fun multiply (Int Int) Int) +(declare-fun Is_ (Int Int) Int) +(declare-fun Smt.true () Int) +(declare-fun ElementType_ (Int) Int) +(declare-fun divide (Int Int) Int) +(declare-fun int_m9223372036854775808 () Int) +(declare-fun divides (Int Int) Int) +(declare-fun stack0b_0 () Int) +(declare-fun select1 (Int Int) Int) +(declare-fun stack0b_1 () Int) +(declare-fun store1 (Int Int Int) Int) +(declare-fun select2 (Int Int Int) Int) +(declare-fun nullObject () Int) +(declare-fun store2 (Int Int Int Int) Int) +(declare-fun false3451to3468_correct () Int) +(declare-fun modulo (Int Int) Int) +(declare-fun System.IComparable () Int) +(declare-fun ownerRef_ () Int) +(declare-fun StructSet_ (Int Int Int) Int) +(declare-fun AsDirectSubClass (Int Int) Int) +(declare-fun System.IEquatable_1...System.String () Int) +(declare-fun System.Boolean () Int) +(declare-fun shl_ (Int Int) Int) +(declare-fun DimLength_ (Int Int) Int) +(declare-fun anyEqual (Int Int) Int) +(declare-fun System.Array () Int) +(declare-fun block3451_correct () Int) +(declare-fun System.Collections.Generic.IEnumerable_1...System.Char () Int) +(declare-fun System.Reflection.ICustomAttributeProvider () Int) +(declare-fun SharingMode_LockProtected_ () Int) +(declare-fun IsMemberlessType_ (Int) Int) +(declare-fun PartOfLine () Int) +(declare-fun System.UInt16 () Int) +(declare-fun false3434to3451_correct () Int) +(declare-fun ClassRepr (Int) Int) +(declare-fun System.Runtime.InteropServices._Type () Int) +(declare-fun boolNot (Int) Int) +(declare-fun Microsoft.Contracts.ICheckedException () Int) +(declare-fun System.Exception () Int) +(declare-fun System.Runtime.InteropServices._MemberInfo () Int) +(declare-fun boolAnd (Int Int) Int) +(declare-fun boolImplies (Int Int) Int) +(declare-fun Unbox (Int) Int) +(declare-fun intAtLeast (Int Int) Int) +(declare-fun ownerFrame_ () Int) +(declare-fun int_4294967295 () Int) +(declare-fun IsAllocated (Int Int) Int) +(declare-fun TypeName (Int) Int) +(declare-fun AsPeerField (Int) Int) +(declare-fun int_9223372036854775807 () Int) +(declare-fun AsRepField (Int Int) Int) +(declare-fun System.Reflection.MemberInfo () Int) +(declare-fun ArrayCategoryValue_ () Int) +(declare-fun is (Int Int) Int) +(declare-fun Microsoft.Contracts.GuardException () Int) +(declare-fun InRange (Int Int) Bool) +(declare-fun AsOwner (Int Int) Int) +(declare-fun System.Int64 () Int) +(declare-fun System.Runtime.InteropServices._Exception () Int) +(declare-fun or_ (Int Int) Int) +(declare-fun As_ (Int Int) Int) +(declare-fun exposeVersion_ () Int) +(declare-fun true3434to3536_correct () Int) +(declare-fun System.Type () Int) +(declare-fun intLess (Int Int) Int) +(declare-fun AsImmutable_ (Int) Int) +(declare-fun NonNullFieldsAreInitialized_ () Int) +(declare-fun block3417_correct () Int) +(declare-fun LBound_ (Int Int) Int) +(declare-fun System.Object () Int) +(declare-fun System.UInt32 () Int) +(declare-fun localinv_ () Int) +(declare-fun inv_ () Int) +(declare-fun Interval () Int) +(declare-fun stack50000o_0 () Int) +(declare-fun stack50000o_1 () Int) +(declare-fun Heap_0_ () Int) +(declare-fun entry_correct () Int) +(declare-fun FirstConsistentOwner_ () Int) +(declare-fun UnboxedType (Int) Int) +(declare-fun AsRefField (Int Int) Int) +(declare-fun System.Byte () Int) +(declare-fun this () Int) +(declare-fun stack1o_0 () Int) +(declare-fun int_2147483647 () Int) +(declare-fun ArrayCategoryRef_ () Int) +(declare-fun Interval.a () Int) +(declare-fun Interval.b () Int) +(declare-fun stack1i_0 () Int) +(declare-fun Heap_ () Int) +(declare-fun Length_ (Int) Int) +(declare-fun System.Runtime.Serialization.ISerializable () Int) +(declare-fun AsNonNullRefField (Int Int) Int) +(declare-fun IsHeap (Int) Int) +(declare-fun Heap_1_ () Int) +(declare-fun UBound_ (Int Int) Int) +(declare-fun Cell () Int) +(declare-fun System.String () Int) +(declare-fun System.String.IsInterned_System.String_notnull_ (Int) Int) +(declare-fun Rank_ (Int) Int) +(declare-fun UnknownRef_ () Int) +(declare-fun RefArraySet (Int Int Int) Int) +(declare-fun ValueArraySet (Int Int Int) Int) +(declare-fun stack50000o () Int) +(declare-fun boolOr (Int Int) Int) +(declare-fun sharingMode_ () Int) +(declare-fun subtypes (Int Int) Bool) +(declare-fun System.IComparable_1...System.String () Int) +(declare-fun System.String.Equals_System.String_System.String_ (Int Int) Int) +(declare-fun block3434_correct () Int) +(declare-fun anyNeq (Int Int) Int) +(declare-fun IsStaticField (Int) Int) +(declare-fun SS_Display.Return.Local_0 () Int) +(declare-fun IsNotNull_ (Int Int) Int) +(declare-fun typeof_ (Int) Int) +(declare-fun ArrayCategoryNonNullRef_ () Int) +(declare-fun RefArrayGet (Int Int) Int) +(declare-fun ValueArrayGet (Int Int) Int) +(declare-fun TypeObject (Int) Int) +(declare-fun and_ (Int Int) Int) +(declare-fun BoxTester (Int Int) Int) +(declare-fun Microsoft.Contracts.ObjectInvariantException () Int) +(declare-fun block3468_correct () Int) +(declare-fun IsValueType_ (Int) Int) +(declare-fun Heap_2_ () Int) +(declare-fun AsRangeField (Int Int) Int) +(declare-fun System.SByte () Int) +(declare-fun BeingConstructed_ () Int) +(declare-fun block3502_correct () Int) +(declare-fun FieldDependsOnFCO_ (Int Int Int) Int) +(declare-fun NonNullRefArray (Int Int) Int) +(declare-fun RefArray (Int Int) Int) +(declare-fun ArrayCategory_ (Int) Int) +(declare-fun stack0b () Int) +(declare-fun Cell.Value () Int) +(declare-fun AsPureObject_ (Int) Int) +(declare-fun System.String.Equals_System.String_ (Int Int) Int) +(declare-fun System.Int16 () Int) +(declare-fun block3536_correct () Int) +(declare-fun AsMutable_ (Int) Int) +(declare-fun System.Char () Int) +(declare-fun System.UInt64 () Int) +(declare-fun StructGet_ (Int Int) Int) +(declare-fun OneClassDown (Int Int) Int) +(declare-fun ArrayIndex (Int Int Int Int) Int) +(declare-fun stack0o_0 () Int) +(declare-fun Box (Int Int) Int) +(declare-fun stack0o_1 () Int) +(declare-fun int_18446744073709551615 () Int) +(declare-fun shr_ (Int Int) Int) +(declare-fun stack0i_0 () Int) +(declare-fun block3553_2_GeneratedUnifiedExit_correct () Int) +(declare-fun System.ICloneable () Int) +(declare-fun IsDirectlyModifiableField (Int) Int) +(declare-fun StringLength_ (Int) Int) +(declare-fun allocated_ () Int) +(declare-fun BaseClass_ (Int) Int) +(declare-fun ValueArray (Int Int) Int) +(declare-fun Smt.false () Int) +(declare-fun true3451to3502_correct () Int) +(declare-fun IsImmutable_ (Int) Int) +(declare-fun elements_ () Int) +(declare-fun DeclType (Int) Int) +(declare-fun System.Collections.IEnumerable () Int) +(declare-fun ReallyLastGeneratedExit_correct () Int) +(assert (forall ((?o Int) (?T Int)) (! (= (= (IsNotNull_ ?o ?T) Smt.true) (and (not (= ?o nullObject)) (= (Is_ ?o ?T) Smt.true))) :pattern ((IsNotNull_ ?o ?T)) ))) +(assert (forall ((?h Int) (?o Int) (?f Int) (?T Int)) (! (=> (and (= (IsHeap ?h) Smt.true) (not (= ?o nullObject)) (or (not (= ?o BeingConstructed_)) (= (= (select2 ?h BeingConstructed_ NonNullFieldsAreInitialized_) Smt.true) true))) (not (= (select2 ?h ?o (AsNonNullRefField ?f ?T)) nullObject))) :pattern ((select2 ?h ?o (AsNonNullRefField ?f ?T))) ))) +(assert (forall ((?o Int) (?T Int)) (! (=> (and (not (= ?o nullObject)) (not (= ?o BeingConstructed_)) (subtypes (typeof_ ?o) (AsImmutable_ ?T))) (forall ((?h Int)) (! (let ((?v_0 (typeof_ ?o))) (=> (= (IsHeap ?h) Smt.true) (and (= (select2 ?h ?o inv_) ?v_0) (= (select2 ?h ?o localinv_) ?v_0) (= (select2 ?h ?o ownerFrame_) PeerGroupPlaceholder_) (= (AsOwner ?o (select2 ?h ?o ownerRef_)) ?o) (forall ((?t Int)) (! (=> (= (AsOwner ?o (select2 ?h ?t ownerRef_)) ?o) (or (= ?t ?o) (not (= (select2 ?h ?t ownerFrame_) PeerGroupPlaceholder_)))) :pattern ((AsOwner ?o (select2 ?h ?t ownerRef_))) ))))) :pattern ((IsHeap ?h)) ))) :pattern ((subtypes (typeof_ ?o) (AsImmutable_ ?T))) ))) +(assert (= (IsValueType_ System.SByte) Smt.true)) +(assert (= (IsValueType_ System.Byte) Smt.true)) +(assert (= (IsValueType_ System.Int16) Smt.true)) +(assert (= (IsValueType_ System.UInt16) Smt.true)) +(assert (= (IsValueType_ System.Int32) Smt.true)) +(assert (= (IsValueType_ System.UInt32) Smt.true)) +(assert (= (IsValueType_ System.Int64) Smt.true)) +(assert (= (IsValueType_ System.UInt64) Smt.true)) +(assert (= (IsValueType_ System.Char) Smt.true)) +(assert (< int_m9223372036854775808 int_m2147483648)) +(assert (< int_m2147483648 (- 0 100000))) +(assert (< 100000 int_2147483647)) +(assert (< int_2147483647 int_4294967295)) +(assert (< int_4294967295 int_9223372036854775807)) +(assert (< int_9223372036854775807 int_18446744073709551615)) +(assert (not (= (IsStaticField Cell.Value) Smt.true))) +(assert (= (IsDirectlyModifiableField Cell.Value) Smt.true)) +(assert (= (DeclType Cell.Value) Cell)) +(assert (= (AsRangeField Cell.Value System.Int32) Cell.Value)) +(assert (not (= (IsStaticField Interval.a) Smt.true))) +(assert (= (IsDirectlyModifiableField Interval.a) Smt.true)) +(assert (= (AsRepField Interval.a Interval) Interval.a)) +(assert (= (DeclType Interval.a) Interval)) +(assert (= (AsNonNullRefField Interval.a Cell) Interval.a)) +(assert (not (= (IsStaticField Interval.b) Smt.true))) +(assert (= (IsDirectlyModifiableField Interval.b) Smt.true)) +(assert (= (AsRepField Interval.b Interval) Interval.b)) +(assert (= (DeclType Interval.b) Interval)) +(assert (= (AsNonNullRefField Interval.b Cell) Interval.b)) +(assert (subtypes Cell Cell)) +(assert (= (BaseClass_ Cell) System.Object)) +(assert (subtypes Cell (BaseClass_ Cell))) +(assert (= (AsDirectSubClass Cell (BaseClass_ Cell)) Cell)) +(assert (not (= (IsImmutable_ Cell) Smt.true))) +(assert (= (AsMutable_ Cell) Cell)) +(assert (subtypes System.Type System.Type)) +(assert (subtypes System.Reflection.MemberInfo System.Reflection.MemberInfo)) +(assert (= (BaseClass_ System.Reflection.MemberInfo) System.Object)) +(assert (subtypes System.Reflection.MemberInfo (BaseClass_ System.Reflection.MemberInfo))) +(assert (= (AsDirectSubClass System.Reflection.MemberInfo (BaseClass_ System.Reflection.MemberInfo)) System.Reflection.MemberInfo)) +(assert (= (IsImmutable_ System.Reflection.MemberInfo) Smt.true)) +(assert (= (AsImmutable_ System.Reflection.MemberInfo) System.Reflection.MemberInfo)) +(assert (subtypes System.Reflection.ICustomAttributeProvider System.Object)) +(assert (= (IsMemberlessType_ System.Reflection.ICustomAttributeProvider) Smt.true)) +(assert (subtypes System.Reflection.MemberInfo System.Reflection.ICustomAttributeProvider)) +(assert (subtypes System.Runtime.InteropServices._MemberInfo System.Object)) +(assert (= (IsMemberlessType_ System.Runtime.InteropServices._MemberInfo) Smt.true)) +(assert (subtypes System.Reflection.MemberInfo System.Runtime.InteropServices._MemberInfo)) +(assert (= (IsMemberlessType_ System.Reflection.MemberInfo) Smt.true)) +(assert (= (BaseClass_ System.Type) System.Reflection.MemberInfo)) +(assert (subtypes System.Type (BaseClass_ System.Type))) +(assert (= (AsDirectSubClass System.Type (BaseClass_ System.Type)) System.Type)) +(assert (= (IsImmutable_ System.Type) Smt.true)) +(assert (= (AsImmutable_ System.Type) System.Type)) +(assert (subtypes System.Runtime.InteropServices._Type System.Object)) +(assert (= (IsMemberlessType_ System.Runtime.InteropServices._Type) Smt.true)) +(assert (subtypes System.Type System.Runtime.InteropServices._Type)) +(assert (subtypes System.Reflection.IReflect System.Object)) +(assert (= (IsMemberlessType_ System.Reflection.IReflect) Smt.true)) +(assert (subtypes System.Type System.Reflection.IReflect)) +(assert (= (IsMemberlessType_ System.Type) Smt.true)) +(assert (subtypes PartOfLine PartOfLine)) +(assert (= (BaseClass_ PartOfLine) System.Object)) +(assert (subtypes PartOfLine (BaseClass_ PartOfLine))) +(assert (= (AsDirectSubClass PartOfLine (BaseClass_ PartOfLine)) PartOfLine)) +(assert (distinct Smt.false Smt.true)) +(assert (let ((?v_0 (select2 Heap_ this ownerFrame_)) (?v_1 (select2 Heap_ this ownerRef_)) (?v_2 (not (= this nullObject))) (?v_3 (not (= stack0o_0 nullObject))) (?v_4 (not (= stack1o_0 nullObject))) (?v_5 (forall ((?o_ Int)) (=> (and (not (= ?o_ nullObject)) (= (= (select2 Heap_ ?o_ allocated_) Smt.true) true)) (and (= (select2 Heap_ ?o_ ownerRef_) (select2 Heap_2_ ?o_ ownerRef_)) (= (select2 Heap_ ?o_ ownerFrame_) (select2 Heap_2_ ?o_ ownerFrame_)))))) (?v_12 (=> true true)) (?v_6 (= ReallyLastGeneratedExit_correct Smt.true)) (?v_7 (= block3553_2_GeneratedUnifiedExit_correct Smt.true)) (?v_15 (= block3553_correct Smt.true)) (?v_14 (= throwException_in Smt.true)) (?v_8 (not (= stack50000o_0 nullObject))) (?v_11 (typeof_ stack50000o_0)) (?v_9 (select2 Heap_1_ stack50000o_0 ownerFrame_)) (?v_10 (select2 Heap_1_ stack50000o_0 ownerRef_)) (?v_13 (= block3468_correct Smt.true)) (?v_19 (= false3451to3468_correct Smt.true))) (let ((?v_21 (=> true ?v_15)) (?v_16 (= block3502_2_block3553_correct Smt.true)) (?v_17 (= block3502_correct Smt.true)) (?v_18 (= true3451to3502_correct Smt.true)) (?v_20 (= block3451_correct Smt.true)) (?v_25 (= false3434to3451_correct Smt.true)) (?v_22 (= block3536_2_block3553_correct Smt.true)) (?v_23 (= block3536_correct Smt.true)) (?v_24 (= true3434to3536_correct Smt.true)) (?v_26 (= block3434_correct Smt.true)) (?v_27 (= block3417_correct Smt.true)) (?v_28 (= entry_correct Smt.true))) (not (=> (=> (=> true (=> (= (IsHeap Heap_) Smt.true) (=> true (=> (= BeingConstructed_ nullObject) (=> (and (or (= ?v_0 PeerGroupPlaceholder_) (not (subtypes (select2 Heap_ ?v_1 inv_) ?v_0)) (= (select2 Heap_ ?v_1 localinv_) (BaseClass_ ?v_0))) (forall ((?pc_ Int)) (let ((?v_29 (typeof_ ?pc_))) (=> (and (not (= ?pc_ nullObject)) (= (= (select2 Heap_ ?pc_ allocated_) Smt.true) true) (= (select2 Heap_ ?pc_ ownerRef_) ?v_1) (= (select2 Heap_ ?pc_ ownerFrame_) ?v_0)) (and (= (select2 Heap_ ?pc_ inv_) ?v_29) (= (select2 Heap_ ?pc_ localinv_) ?v_29)))))) (=> true (=> true (=> (= (IsNotNull_ this Interval) Smt.true) (=> (= (= (select2 Heap_ this allocated_) Smt.true) true) (=> true (=> (=> (=> true (=> true (=> true (=> (=> (=> true (=> true (and ?v_2 (=> ?v_2 (=> (= stack0o_0 (select2 Heap_ this Interval.a)) (and ?v_3 (=> ?v_3 (=> (= stack0i_0 (select2 Heap_ stack0o_0 Cell.Value)) (and ?v_2 (=> ?v_2 (=> (= stack1o_0 (select2 Heap_ this Interval.b)) (and ?v_4 (=> ?v_4 (=> (= stack1i_0 (select2 Heap_ stack1o_0 Cell.Value)) (=> true (=> (and (=> (=> true (=> true (=> true (=> (=> (=> true (=> (= SS_Display.Return.Local_0 local0_0) (=> (= result_0_ local0_0) (=> (= stack50000o_1 stack50000o) (=> (= stack0b_1 local0_0) (=> (= stack0o_1 stack0o_0) (=> (= local0_1 local0_0) (=> (= Heap_2_ Heap_) (=> (=> (=> true (and ?v_5 (=> ?v_5 ?v_12))) ?v_6) ?v_6))))))))) ?v_7) ?v_7)))) ?v_15) (=> (=> true (=> true (=> (> stack0i_0 stack1i_0) (=> true (=> (=> (=> true (=> true (=> true (=> (and (=> (=> true (=> true (=> ?v_14 (=> true (=> (=> (=> true (=> true (=> false (=> (and (= (= (select2 Heap_ stack50000o_0 allocated_) Smt.true) false) ?v_8 (= ?v_11 Microsoft.Contracts.ObjectInvariantException)) (=> (and (= (select2 Heap_ stack50000o_0 ownerRef_) stack50000o_0) (= (select2 Heap_ stack50000o_0 ownerFrame_) PeerGroupPlaceholder_)) (=> (= Heap_0_ (store2 Heap_ stack50000o_0 allocated_ Smt.true)) (and ?v_8 (=> ?v_8 (=> (= (IsHeap Heap_1_) Smt.true) (=> (and (or (= ?v_9 PeerGroupPlaceholder_) (not (subtypes (select2 Heap_1_ ?v_10 inv_) ?v_9)) (= (select2 Heap_1_ ?v_10 localinv_) (BaseClass_ ?v_9))) (= (select2 Heap_1_ stack50000o_0 inv_) Microsoft.Contracts.ObjectInvariantException) (= (select2 Heap_1_ stack50000o_0 localinv_) ?v_11)) (=> (and (= ?v_10 (select2 Heap_0_ stack50000o_0 ownerRef_)) (= ?v_9 (select2 Heap_0_ stack50000o_0 ownerFrame_))) (=> (= (select2 Heap_1_ stack50000o_0 sharingMode_) SharingMode_Unshared_) (=> (forall ((?o_ Int)) (let ((?v_30 (typeof_ ?o_))) (=> (and (not (= ?o_ nullObject)) (= (= (select2 Heap_0_ ?o_ allocated_) Smt.true) (not true)) (= (= (select2 Heap_1_ ?o_ allocated_) Smt.true) true)) (and (= (select2 Heap_1_ ?o_ inv_) ?v_30) (= (select2 Heap_1_ ?o_ localinv_) ?v_30))))) (=> (forall ((?o_ Int)) (! (let ((?v_31 (select2 Heap_0_ ?o_ FirstConsistentOwner_))) (=> (= (select2 Heap_0_ ?v_31 exposeVersion_) (select2 Heap_1_ ?v_31 exposeVersion_)) (= ?v_31 (select2 Heap_1_ ?o_ FirstConsistentOwner_)))) :pattern ((select2 Heap_1_ ?o_ FirstConsistentOwner_)) )) (=> (forall ((?o_ Int)) (=> (and (not (= ?o_ nullObject)) (= (= (select2 Heap_0_ ?o_ allocated_) Smt.true) true)) (and (= (select2 Heap_0_ ?o_ ownerRef_) (select2 Heap_1_ ?o_ ownerRef_)) (= (select2 Heap_0_ ?o_ ownerFrame_) (select2 Heap_1_ ?o_ ownerFrame_))))) (=> (forall ((?o_ Int) (?f_ Int)) (! (let ((?v_32 (select2 Heap_0_ ?o_ ownerFrame_)) (?v_33 (select2 Heap_0_ ?o_ ownerRef_))) (=> (and (not (= ?f_ inv_)) (not (= ?f_ localinv_)) (not (= ?f_ FirstConsistentOwner_)) (or (not (= (IsStaticField ?f_) Smt.true)) (not (= (IsDirectlyModifiableField ?f_) Smt.true))) (not (= ?o_ nullObject)) (= (= (select2 Heap_0_ ?o_ allocated_) Smt.true) true) (or (= ?v_32 PeerGroupPlaceholder_) (not (subtypes (select2 Heap_0_ ?v_33 inv_) ?v_32)) (= (select2 Heap_0_ ?v_33 localinv_) (BaseClass_ ?v_32))) (or (not (= ?o_ stack50000o_0)) (not (subtypes Microsoft.Contracts.ObjectInvariantException (DeclType ?f_)))) true) (= (select2 Heap_0_ ?o_ ?f_) (select2 Heap_1_ ?o_ ?f_)))) :pattern ((select2 Heap_1_ ?o_ ?f_)) )) (=> (forall ((?o_ Int)) (or (= ?o_ stack50000o_0) (and (= (select2 Heap_0_ ?o_ inv_) (select2 Heap_1_ ?o_ inv_)) (= (select2 Heap_0_ ?o_ localinv_) (select2 Heap_1_ ?o_ localinv_))) (= (= (select2 Heap_0_ ?o_ allocated_) Smt.true) (not true)))) (=> (and (forall ((?o_ Int)) (=> (= (= (select2 Heap_0_ ?o_ allocated_) Smt.true) true) (= (= (select2 Heap_1_ ?o_ allocated_) Smt.true) true))) (forall ((?ot_ Int)) (let ((?v_34 (select2 Heap_0_ ?ot_ ownerFrame_))) (=> (and (= (= (select2 Heap_0_ ?ot_ allocated_) Smt.true) true) (not (= ?v_34 PeerGroupPlaceholder_))) (and (= (select2 Heap_1_ ?ot_ ownerRef_) (select2 Heap_0_ ?ot_ ownerRef_)) (= (select2 Heap_1_ ?ot_ ownerFrame_) ?v_34))))) (= (= (select2 Heap_0_ BeingConstructed_ NonNullFieldsAreInitialized_) Smt.true) (= (select2 Heap_1_ BeingConstructed_ NonNullFieldsAreInitialized_) Smt.true))) (=> (forall ((?o_ Int)) (or (= ?o_ stack50000o_0) (= (select2 Heap_0_ ?o_ sharingMode_) (select2 Heap_1_ ?o_ sharingMode_)))) (and ?v_8 (=> ?v_8 (=> false (=> true ?v_12))))))))))))))))))))))) ?v_13) ?v_13))))) ?v_19) (=> (=> true (=> true (=> (not ?v_14) (=> true (=> (=> (=> true (=> true (=> true (=> (=> (=> true (=> (= stack0b_0 throwException_in) (=> (= local0_0 Smt.false) ?v_21))) ?v_16) ?v_16)))) ?v_17) ?v_17))))) ?v_18)) (and ?v_18 ?v_19))))) ?v_20) ?v_20))))) ?v_25) (=> (=> true (=> true (=> (<= stack0i_0 stack1i_0) (=> true (=> (=> (=> true (=> true (=> true (=> (=> (=> true (=> (= stack0b_0 stack0b) (=> (= local0_0 Smt.true) ?v_21))) ?v_22) ?v_22)))) ?v_23) ?v_23))))) ?v_24)) (and ?v_24 ?v_25))))))))))))))))) ?v_26) ?v_26)))) ?v_27) ?v_27))))))))))) ?v_28) ?v_28))))) +(check-sat) +(exit) diff --git a/test/regress/regress0/quantifiers/rew-to-scala.smt2 b/test/regress/regress0/quantifiers/rew-to-scala.smt2 new file mode 100644 index 000000000..1e29241eb --- /dev/null +++ b/test/regress/regress0/quantifiers/rew-to-scala.smt2 @@ -0,0 +1,13 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(declare-datatypes () ((Formula!953 (And!954 (lhs!955 Formula!953) (rhs!956 Formula!953)) (Not!957 (f!958 Formula!953)) (Or!959 (lhs!960 Formula!953) (rhs!961 Formula!953)) (Variable!962 (id!963 (_ BitVec 32)))) +)) +(declare-fun error_value!964 () Bool) +(declare-fun isNNF!208 (Formula!953) Bool) +(declare-fun error_value!965 () Formula!953) +(declare-fun nnf!206 (Formula!953) Formula!953) +(declare-fun error_value!966 () Formula!953) +(assert (forall ((f!207 Formula!953)) (= (isNNF!208 f!207) (ite (is-And!954 f!207) (and (and (isNNF!208 (lhs!955 f!207)) (isNNF!208 (lhs!955 f!207))) (isNNF!208 (rhs!956 f!207))) (ite (is-Or!959 f!207) (and (and (isNNF!208 (lhs!960 f!207)) (isNNF!208 (lhs!960 f!207))) (isNNF!208 (rhs!961 f!207))) (ite (is-Not!957 f!207) false (ite (is-Variable!962 f!207) true error_value!964))))) )) +(assert (forall ((formula!205 Formula!953)) (= (nnf!206 formula!205) (ite (is-And!954 formula!205) (And!954 (nnf!206 (lhs!955 formula!205)) (nnf!206 (rhs!956 formula!205))) (ite (is-Or!959 formula!205) (Or!959 (nnf!206 (lhs!960 formula!205)) (nnf!206 (rhs!961 formula!205))) (ite (and (and (is-Not!957 formula!205) (is-Not!957 formula!205)) (is-And!954 (f!958 formula!205))) (Or!959 (nnf!206 (Not!957 (lhs!955 (f!958 formula!205)))) (nnf!206 (Not!957 (rhs!956 (f!958 formula!205))))) (ite (and (and (is-Not!957 formula!205) (is-Not!957 formula!205)) (is-Or!959 (f!958 formula!205))) (And!954 (nnf!206 (Not!957 (lhs!960 (f!958 formula!205)))) (nnf!206 (Not!957 (rhs!961 (f!958 formula!205))))) (ite (and (and (is-Not!957 formula!205) (is-Not!957 formula!205)) (is-Not!957 (f!958 formula!205))) (nnf!206 (f!958 (f!958 formula!205))) (ite (is-Not!957 formula!205) formula!205 (ite (is-Variable!962 formula!205) formula!205 error_value!965)))))))) )) +(assert (exists ((formula!205 Formula!953)) (not (=> (is-Variable!962 formula!205) (isNNF!208 (ite (is-And!954 formula!205) (And!954 (nnf!206 (lhs!955 formula!205)) (nnf!206 (rhs!956 formula!205))) (ite (is-Or!959 formula!205) (Or!959 (nnf!206 (lhs!960 formula!205)) (nnf!206 (rhs!961 formula!205))) (ite (and (and (is-Not!957 formula!205) (is-Not!957 formula!205)) (is-And!954 (f!958 formula!205))) (Or!959 (nnf!206 (Not!957 (lhs!955 (f!958 formula!205)))) (nnf!206 (Not!957 (rhs!956 (f!958 formula!205))))) (ite (and (and (is-Not!957 formula!205) (is-Not!957 formula!205)) (is-Or!959 (f!958 formula!205))) (And!954 (nnf!206 (Not!957 (lhs!960 (f!958 formula!205)))) (nnf!206 (Not!957 (rhs!961 (f!958 formula!205))))) (ite (and (and (is-Not!957 formula!205) (is-Not!957 formula!205)) (is-Not!957 (f!958 formula!205))) (nnf!206 (f!958 (f!958 formula!205))) (ite (is-Not!957 formula!205) formula!205 (ite (is-Variable!962 formula!205) formula!205 error_value!966)))))))))) )) +(check-sat) -- 2.30.2