From: Andrew Reynolds Date: Mon, 9 Sep 2013 23:40:45 +0000 (-0500) Subject: Another minor fix for datatypes to repair my previous commit. X-Git-Tag: cvc5-1.0.0~7287^2~17^2~1 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f49c16dd1169d3de4bbfcdca22af1269bbd0a005;p=cvc5.git Another minor fix for datatypes to repair my previous commit. --- diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index bc6d1f839..186444e0a 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -21,6 +21,7 @@ #include "theory/rewriter.h" #include "theory/datatypes/options.h" +#include "theory/type_enumerator.h" namespace CVC4 { namespace theory { @@ -137,10 +138,16 @@ public: return RewriteResponse(REWRITE_DONE, in[0][selectorIndex]); }else{ if( options::dtRewriteErrorSel() ){ - Node gt = in.getType().mkGroundTerm(); + Node gt; + if( in.getType().isSort() ){ + TypeEnumerator te(in.getType()); + gt = *te; + }else{ + gt = in.getType().mkGroundTerm(); + } TypeNode gtt = gt.getType(); //Assert( gtt.isDatatype() || gtt.isParametricDatatype() ); - if( !gtt.isInstantiatedDatatype() ){ + if( gtt.isDatatype() && !gtt.isInstantiatedDatatype() ){ gt = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, NodeManager::currentNM()->mkConst(AscriptionType(in.getType().toType())), gt); } diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 9dc8c0028..a0651efb4 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -91,7 +91,7 @@ TheoryDatatypes::EqcInfo* TheoryDatatypes::getOrMakeEqcInfo( Node n, bool doMake } void TheoryDatatypes::check(Effort e) { - + Trace("datatypes-debug") << "Check effort " << e << std::endl; while(!done() && !d_conflict) { // Get all the assertions Assertion assertion = get(); @@ -189,20 +189,19 @@ void TheoryDatatypes::check(Effort e) { ++eqcs_i; } Trace("datatypes-debug") << "Flush pending facts..." << std::endl; - addedFact = !d_pending.empty(); + addedFact = !d_pending.empty() || !d_pending_merge.empty(); flushPendingFacts(); if( !d_conflict ){ if( options::dtRewriteErrorSel() ){ - collapseSelectors(); - flushPendingFacts(); - if( d_conflict ){ - return; - } + bool innerAddedFact = false; + do { + collapseSelectors(); + innerAddedFact = !d_pending.empty() || !d_pending_merge.empty(); + flushPendingFacts(); + }while( !d_conflict && innerAddedFact ); } - }else{ - return; } - }while( addedFact ); + }while( !d_conflict && addedFact ); Trace("datatypes-debug") << "Finished. " << d_conflict << std::endl; if( !d_conflict ){ Trace("dt-model-test") << std::endl; @@ -1019,8 +1018,8 @@ bool TheoryDatatypes::mustCommunicateFact( Node n, Node exp ){ // (3) Instantiate : is_C( t ) => t = C( sel_1( t ) ... sel_n( t ) ) //We may need to communicate (3) outwards if the conclusions involve other theories Trace("dt-lemma-debug") << "Compute for " << exp << " => " << n << std::endl; + bool addLemma = false; if( ( n.getKind()==EQUAL || n.getKind()==IFF) && n[1].getKind()==APPLY_CONSTRUCTOR && exp.getKind()!=EQUAL ){ - bool addLemma = false; #if 1 const Datatype& dt = ((DatatypeType)(n[1].getType()).toType()).getDatatype(); addLemma = dt.involvesExternalType(); @@ -1044,6 +1043,11 @@ bool TheoryDatatypes::mustCommunicateFact( Node n, Node exp ){ } } } + //else if( exp.getKind()==APPLY_TESTER ){ + //if( n.getKind()==EQUAL && !DatatypesRewriter::isTermDatatype( n[0] ) ){ + // return true; + //} + //} Trace("dt-lemma-debug") << "Do not need to communicate " << n << std::endl; return false; } diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index a367447c9..97b48c716 100755 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -24,7 +24,8 @@ TESTS = \ Arrow_Order-smtlib.778341.smt \ german73.smt2 \ PUZ001+1.smt2 \ - refcount24.cvc.smt2 + refcount24.cvc.smt2 \ + bug0909.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/fmf/bug0909.smt2 b/test/regress/regress0/fmf/bug0909.smt2 new file mode 100755 index 000000000..39862b8d6 --- /dev/null +++ b/test/regress/regress0/fmf/bug0909.smt2 @@ -0,0 +1,55 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: unsat +; EXIT: 20 +; Preamble -------------- +(set-option :produce-models true) +(set-logic ALL_SUPPORTED) +;(declare-datatypes () ((x2 (x1)))) +(declare-datatypes () ((x5 (x3) (x4)))) +(declare-sort x6 0) +(declare-fun x7 (x6) x5) +(declare-fun x8 () x6) +(assert (not (= x3 (x7 x8)))) +(declare-fun x9 () x6) +(assert (not (= x3 (x7 x9)))) +(declare-fun x11 () Int) +(declare-sort x12 0) +(declare-fun x13 () x12) +(declare-datatypes () ((x17 (x14) (x15) (x16)))) +(declare-datatypes () ((x22 (x21 (x18 Int) (x19 Int) (x20 x5))))) +(declare-datatypes () ((x29 (x28 (x23 x5) (x24 x5) (x25 Int) (x26 Int) (x27 Int))))) +(declare-sort x30 0) +(declare-sort x31 0) +(declare-fun x32 () x31) +(declare-datatypes () ((x36 (x35 (x33 Int) (x34 Int))))) +(declare-fun x37 () x36) +(declare-datatypes () ((x45 (x44 (x38 x5) (x39 x6) (x40 x6) (x41 x6) (x42 x36) (x43 x31))))) +(declare-fun x47 (x12) x31) +(declare-fun x46 (x31) x12) +(declare-datatypes () ((x54 (x49 (x48 x22)) (x51 (x50 x29)) (d53 (s52 x12))))) +(declare-fun x57 (x22) x29) +(declare-fun x56 (x12) x22) +(declare-fun x55 (x29) x22) +(declare-fun x61 () (Array x6 x5)) +(declare-fun x66 () (Array x6 x17)) +(declare-fun x64 () (Array x6 x54)) +(declare-fun x67 () (Array x6 x54)) +(declare-fun x65 () (Array x6 x54)) +(declare-fun x62 () (Array x30 x45)) +(declare-fun x70 () (Array x30 x45)) +(declare-fun x68 () (Array x30 x45)) +(declare-fun x63 () x30) +(declare-fun x59 (x22) x12) +(declare-fun x60 (x29) x12) +(declare-fun x58 (x12) x29) +(declare-fun x71 () x6) +(declare-fun x69 () x6) +(assert +(not + (=> (and + (forall ((x73 x30)) (=> (= x3 (x38 (select x62 x73))) (and (= (select x66 (x40 (select x62 x73))) x15) (= x3 (x7 (x40 (select x62 x73)))) (= (select x61 (x40 (select x62 x73))) x3) (= (x23 (ite (is-x49 (select x67 (x40 (select x62 x73)))) (let ((x74 (x48 (select x67 (x40 (select x62 x73)))))) (x57 x74)) (ite (is-x51 (select x67 (x40 (select x62 x73)))) (let ((x75 (x50 (select x67 (x40 (select x62 x73)))))) x75) (let ((x76 (s52 (select x67 (x40 (select x62 x73)))))) (x58 x76))))) x3)))) + (forall ((x72 x6)) (=> (and (= x16 (select x66 x72)) (= (x7 x72) x3) (= (select x61 x72) x3)) (= (ite (is-d53 (select x67 x72)) x3 x4) x3)))) + + (= (ite (= (x38 (select x62 x63)) x3) (ite (and (=> (= (x40 (select x62 x63)) x69) (=> (= (x41 (select x62 x63)) x71) (=> (= x65 (store x67 x71 (d53 (x46 (x43 (select x62 x63)))))) (=> (= x70 (store x62 x63 (let ((x77 (select x62 x63))) (x44 (x38 x77) (x39 x77) (x40 x77) (x41 x77) (x42 x77) x32)))) (=> (= x68 (store x70 x63 (let ((x78 (select x70 x63))) (x44 x4 (x39 x78) (x40 x78) (x41 x78) (x42 x78) (x43 x78))))) + (=> (= (store x65 x69 (x51 (let ((x82 (ite (is-x49 (select x65 x69)) (let ((x79 (x48 (select x65 x69)))) (x57 x79)) (ite (is-x51 (select x65 x69)) (let ((x80 (x50 (select x65 x69)))) x80) (let ((x81 (s52 (select x65 x69)))) (x58 x81)))))) (x28 x4 x3 (x25 x82) (x26 x82) (+ (x27 (ite (is-x49 (select x65 x69)) (let ((x83 (x48 (select x65 x69)))) (x57 x83)) (ite (is-x51 (select x65 x69)) (let ((x84 (x50 (select x65 x69)))) x84) (let ((x85 (s52 (select x65 x69)))) (x58 x85))))) 1))))) x64) (forall ((x86 x6)) (=> (and (= x3 (x7 x86)) (= x3 (select x61 x86)) (= (select x66 x86) x16)) (= (ite (is-d53 (select x64 x86)) x3 x4) x3))))))))) (= x3 (x38 (select x62 x63)))) x3 x4) (ite (forall ((x87 x6)) (=> (and (= x3 (select x61 x87)) (= x3 (x7 x87)) (= x16 (select x66 x87))) (= x3 (ite (is-d53 (select x67 x87)) x3 x4)))) x3 x4)) x3)))) +(check-sat) \ No newline at end of file