diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-01 11:31:59 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-01 11:31:59 +0100 |
commit | 9df318ca1ab33001bd203c24ae57a8b5739b8f36 (patch) | |
tree | 3b104cc97f5daa2f69285056d81ace0ed7c916e9 | |
parent | 458b2b7eb5bdf09a1a886f4e2a165380d5fd918f (diff) |
Fix some mistakes in datatypes theory combination, disable two regressions. Minor fix for fun defs.
-rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 31 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 2 | ||||
-rw-r--r-- | test/regress/regress0/Makefile.am | 6 |
3 files changed, 20 insertions, 19 deletions
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 516aae0e1..77cab86a2 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -532,11 +532,11 @@ Node TheoryDatatypes::ppRewrite(TNode in) { void TheoryDatatypes::addSharedTerm(TNode t) { Debug("datatypes") << "TheoryDatatypes::addSharedTerm(): " << t << " " << t.getType().isBoolean() << endl; - if( t.getType().isBoolean() ){ + //if( t.getType().isBoolean() ){ //d_equalityEngine.addTriggerPredicate(t, THEORY_DATATYPES); - }else{ - d_equalityEngine.addTriggerTerm(t, THEORY_DATATYPES); - } + //}else{ + d_equalityEngine.addTriggerTerm(t, THEORY_DATATYPES); + //} Debug("datatypes") << "TheoryDatatypes::addSharedTerm() finished" << std::endl; } @@ -1059,15 +1059,14 @@ void TheoryDatatypes::collapseSelector( Node s, Node c ) { } EqualityStatus TheoryDatatypes::getEqualityStatus(TNode a, TNode b){ - if( d_equalityEngine.hasTerm(a) && d_equalityEngine.hasTerm(b) ){ - if (d_equalityEngine.areEqual(a, b)) { - // The terms are implied to be equal - return EQUALITY_TRUE; - } - if (d_equalityEngine.areDisequal(a, b, false)) { - // The terms are implied to be dis-equal - return EQUALITY_FALSE; - } + Assert(d_equalityEngine.hasTerm(a) && d_equalityEngine.hasTerm(b)); + if (d_equalityEngine.areEqual(a, b)) { + // The terms are implied to be equal + return EQUALITY_TRUE; + } + if (d_equalityEngine.areDisequal(a, b, false)) { + // The terms are implied to be dis-equal + return EQUALITY_FALSE; } return EQUALITY_FALSE_IN_MODEL; } @@ -1088,12 +1087,14 @@ void TheoryDatatypes::computeCareGraph(){ for (unsigned k = 0; k < f1.getNumChildren(); ++ k) { TNode x = f1[k]; TNode y = f2[k]; + Assert(d_equalityEngine.hasTerm(x)); + Assert(d_equalityEngine.hasTerm(y)); if( areDisequal(x, y) ){ somePairIsDisequal = true; break; - }else if( !areEqual( x, y ) ){ + }else if( !d_equalityEngine.areEqual( x, y ) ){ Trace("dt-cg") << "Arg #" << k << " is " << x << " " << y << std::endl; - if( d_equalityEngine.isTriggerTerm(x, THEORY_UF) && d_equalityEngine.isTriggerTerm(y, THEORY_UF) ){ + if( d_equalityEngine.isTriggerTerm(x, THEORY_DATATYPES) && d_equalityEngine.isTriggerTerm(y, THEORY_DATATYPES) ){ EqualityStatus eqStatus = d_valuation.getEqualityStatus(x, y); if( eqStatus!=EQUALITY_UNKNOWN ){ TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_DATATYPES); diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 3f6f2a6ed..392fc269a 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1001,7 +1001,7 @@ Node TermDb::getRewriteRule( Node q ) { } bool TermDb::isFunDef( Node q ) { - if( q.getKind()==FORALL && ( q[1].getKind()==EQUAL || q[1].getKind()==IFF ) && q[1][0].getKind()==APPLY_UF ){ + if( q.getKind()==FORALL && ( q[1].getKind()==EQUAL || q[1].getKind()==IFF ) && q[1][0].getKind()==APPLY_UF && q.getNumChildren()==3 ){ for( unsigned i=0; i<q[2].getNumChildren(); i++ ){ if( q[2][i].getKind()==INST_ATTRIBUTE ){ if( q[2][i][0].getAttribute(FunDefAttribute()) ){ diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index fae563973..cbaa58b3c 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -106,8 +106,7 @@ CVC_TESTS = \ wiki.20.cvc \ wiki.21.cvc \ queries0.cvc \ - print_lambda.cvc \ - trim.cvc + print_lambda.cvc # Regression tests for TPTP inputs TPTP_TESTS = @@ -145,7 +144,6 @@ BUG_TESTS = \ bug421b.smt2 \ bug425.cvc \ bug480.smt2 \ - bug484.smt2 \ bug486.cvc \ bug507.smt2 \ bug512.minimized.smt2 \ @@ -171,6 +169,8 @@ BUG_TESTS = \ TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS) # bug512 -- taking too long, --time-per not working perhaps? in any case, +# bug484.smt2 +# trim.cvc # we have a minimized version still getting tested DISABLED_TESTS = \ bug512.smt2 |