#include "theory/rewriter.h"
#include "theory/datatypes/options.h"
+#include "theory/type_enumerator.h"
namespace CVC4 {
namespace theory {
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);
}
}
void TheoryDatatypes::check(Effort e) {
-
+ Trace("datatypes-debug") << "Check effort " << e << std::endl;
while(!done() && !d_conflict) {
// Get all the assertions
Assertion assertion = get();
++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;
// (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();
}
}
}
+ //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;
}
--- /dev/null
+; 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
projects / cvc5.git / commitdiff