d_equalityEngine.addFunctionKind(kind::APPLY_SELECTOR_TOTAL);
d_equalityEngine.addFunctionKind(kind::DT_SIZE);
d_equalityEngine.addFunctionKind(kind::APPLY_TESTER);
- d_equalityEngine.addFunctionKind(kind::APPLY_UF);
+ //d_equalityEngine.addFunctionKind(kind::APPLY_UF);
d_true = NodeManager::currentNM()->mkConst( true );
d_dtfCounter = 0;
void TheoryDatatypes::computeCareGraph(){
Trace("dt-cg") << "Compute graph for dt..." << std::endl;
+ /*
+ Trace("dt-cg") << "Look at shared terms..." << std::endl;
+ for (unsigned i = 0; i < d_sharedTerms.size(); ++ i) {
+ TNode a = d_sharedTerms[i];
+ if( a.getKind()!=APPLY_CONSTRUCTOR && a.getKind()!=APPLY_SELECTOR_TOTAL ){
+ TypeNode aType = a.getType();
+ for (unsigned j = i + 1; j < d_sharedTerms.size(); ++ j) {
+ TNode b = d_sharedTerms[j];
+ if( b.getKind()!=APPLY_CONSTRUCTOR && b.getKind()!=APPLY_SELECTOR_TOTAL ){
+ if (b.getType() != aType) {
+ // We don't care about the terms of different types
+ continue;
+ }
+ switch (d_valuation.getEqualityStatus(a, b)) {
+ case EQUALITY_TRUE_AND_PROPAGATED:
+ case EQUALITY_FALSE_AND_PROPAGATED:
+ // If we know about it, we should have propagated it, so we can skip
+ break;
+ default:
+ // Let's split on it
+ addCarePair(a, b);
+ break;
+ }
+ }
+ }
+ }
+ }
+ */
+
+ Trace("dt-cg") << "Look at theory terms..." << std::endl;
vector< pair<TNode, TNode> > currentPairs;
for( unsigned r=0; r<2; r++ ){
unsigned functionTerms = r==0 ? d_consTerms.size() : d_selTerms.size();
Trace("dt-cg") << "Arg #" << k << " is " << x << " " << y << std::endl;
if( d_equalityEngine.isTriggerTerm(x, THEORY_DATATYPES) && d_equalityEngine.isTriggerTerm(y, THEORY_DATATYPES) ){
EqualityStatus eqStatus = d_valuation.getEqualityStatus(x, y);
- if( eqStatus==EQUALITY_FALSE_AND_PROPAGATED || eqStatus==EQUALITY_FALSE || eqStatus==EQUALITY_UNKNOWN ){
+ if( eqStatus==EQUALITY_FALSE_AND_PROPAGATED || eqStatus==EQUALITY_FALSE || eqStatus==EQUALITY_FALSE_IN_MODEL ){
somePairIsDisequal = true;
break;
}else{
//for all equivalence classes that are datatypes
if( DatatypesRewriter::isTermDatatype( eqc ) ){
EqcInfo* ei = getOrMakeEqcInfo( eqc );
- if( !ei->d_constructor.get().isNull() ){
- cons.push_back( ei->d_constructor.get() );
- eqc_cons[ eqc ] = ei->d_constructor.get();
+ if( ei && !ei->d_constructor.get().isNull() ){
+ Node c = ei->d_constructor.get();
+ cons.push_back( c );
+ eqc_cons[ eqc ] = c;
}else{
- nodes.push_back( eqc );
+ //if eqc contains a symbol known to datatypes (a selector), then we must assign
+ bool containsTSym = false;
+ eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
+ while( !eqc_i.isFinished() ){
+ Node n = *eqc_i;
+ Trace("dt-cmi-debug") << n << " has kind " << n.getKind() << ", isVar = " << n.isVar() << std::endl;
+ if( n.isVar() || n.getKind()==APPLY_SELECTOR_TOTAL ){
+ containsTSym = true;
+ break;
+ }
+ ++eqc_i;
+ }
+ if( containsTSym ){
+ nodes.push_back( eqc );
+ }
}
}
++eqccs_i;
Trace("dt-cmi") << " Type : " << eqc.getType() << std::endl;
TypeNode tn = eqc.getType();
//if it is infinite, make sure it is fresh
+ // this ensures that the term that this is an argument of is distinct.
if( eqc.getType().getCardinality().isInfinite() ){
std::map< TypeNode, int >::iterator it = typ_enum_map.find( tn );
int teIndex;
}
bool TheoryDatatypes::mustCommunicateFact( Node n, Node exp ){
- //the datatypes decision procedure makes 5 "internal" inferences apart from the equality engine :
+ //the datatypes decision procedure makes "internal" inferences apart from the equality engine :
// (1) Unification : C( t1...tn ) = C( s1...sn ) => ti = si
// (2) Label : ~is_C1( t ) ... ~is_C{i-1}( t ) ~is_C{i+1}( t ) ... ~is_Cn( t ) => is_Ci( t )
// (3) Instantiate : is_C( t ) => t = C( sel_1( t ) ... sel_n( t ) )
Trace("dt-lemma-debug") << "Compute for " << exp << " => " << n << std::endl;
bool addLemma = false;
if( n.getKind()==EQUAL || n.getKind()==IFF ){
- TypeNode tn = n[0].getType();
- if( !tn.isDatatype() ){
- addLemma = true;
- }else{
- const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
- addLemma = dt.involvesExternalType();
+ for( unsigned i=0; i<2; i++ ){
+ if( n[i].getKind()!=APPLY_SELECTOR_TOTAL && n[i].getKind()!=APPLY_CONSTRUCTOR ){
+ addLemma = true;
+ }
+ }
+
+ if( !addLemma ){
+ TypeNode tn = n[0].getType();
+ if( !DatatypesRewriter::isTypeDatatype( tn ) ){
+ addLemma = true;
+ }else{
+ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ addLemma = dt.involvesExternalType();
+ }
}
//for( int j=0; j<(int)n[1].getNumChildren(); j++ ){
// if( !DatatypesRewriter::isTermDatatype( n[1][j] ) ){
}
Node bd = assertions[i][1].substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
- Trace("fmf-fun-def") << "FMF fun def: rewrite " << assertions[i] << " to ";
+ Trace("fmf-fun-def") << "FMF fun def: rewrite " << assertions[i] << std::endl;
+ Trace("fmf-fun-def") << " to " << std::endl;
assertions[i] = NodeManager::currentNM()->mkNode( FORALL, bvl, bd );
- Trace("fmf-fun-def") << assertions[i] << std::endl;
+ Trace("fmf-fun-def") << " " << assertions[i] << std::endl;
fd_assertions.push_back( i );
}
}
Assert( constraints.empty() );
if( n!=assertions[i] ){
n = Rewriter::rewrite( n );
- Trace("fmf-fun-def-rewrite") << "FMF fun def : rewrite " << assertions[i] << " to " << n << std::endl;
+ Trace("fmf-fun-def-rewrite") << "FMF fun def : rewrite " << assertions[i] << std::endl;
+ Trace("fmf-fun-def-rewrite") << " to " << std::endl;
+ Trace("fmf-fun-def-rewrite") << " " << n << std::endl;
assertions[i] = n;
}
}
}else{
//must add at higher level
}
- return c.size()==1 ? c[0] : NodeManager::currentNM()->mkNode( AND, c );
+ return c.size()==1 ? c[0] : NodeManager::currentNM()->mkNode( pol ? AND : OR, c );
}
}else{
//simplify term
}
}
+bool Trigger::isLocalTheoryExt2( Node n, std::vector< Node >& var_found, std::vector< Node >& patTerms ) {
+ if( !n.getType().isBoolean() && n.getKind()==APPLY_UF ){
+ bool hasVar = false;
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ if( n[i].getKind()==APPLY_UF ){
+ return false;
+ }else if( n[i].getKind()==INST_CONSTANT ){
+ hasVar = true;
+ //if( std::find( var_found.begin(), var_found.end(), n[i]
+ }
+ }
+ if( hasVar ){
+ patTerms.push_back( n );
+ }
+ }else{
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ if( !isLocalTheoryExt2( n, var_found, patTerms ) ){
+ return false;
+ }
+ }
+ }
+ return true;
+}
+
bool Trigger::isBooleanTermTrigger( Node n ) {
if( n.getKind()==ITE ){
//check for boolean term converted to ITE
}
}
+bool Trigger::isLocalTheoryExt( Node n, std::vector< Node >& patTerms ) {
+ std::vector< Node > var_found;
+ return isLocalTheoryExt2( n, var_found, patTerms );
+}
+
void Trigger::collectPatTerms( QuantifiersEngine* qe, Node f, Node n, std::vector< Node >& patTerms, int tstrt, std::vector< Node >& exclude, bool filterInst ){
std::map< Node, bool > patMap;
if( filterInst ){
static Node getIsUsableTrigger( Node n, Node f, bool pol = true, bool hasPol = false );
/** collect all APPLY_UF pattern terms for f in n */
static bool collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt, std::vector< Node >& exclude, bool pol, bool hasPol );
+ /** is local theory extensions term */
+ static bool isLocalTheoryExt2( Node n, std::vector< Node >& var_found, std::vector< Node >& patTerms );
public:
//different strategies for choosing trigger terms
enum {
static bool isSimpleTrigger( Node n );
static bool isBooleanTermTrigger( Node n );
static bool isPureTheoryTrigger( Node n );
+ static bool isLocalTheoryExt( Node n, std::vector< Node >& patTerms );
/** return data structure for producing matches for this trigger. */
static InstMatchGenerator* getInstMatchGenerator( Node n );
static Node getInversionVariable( Node n );
if( n[0].getKind()!=kind::CONST_RATIONAL ){
throw TypeCheckingExceptionPrivate(n, "combined cardinality constraint must be a constant");
}
- if( n[0].getConst<Rational>().getNumerator().sgn()!=1 ){
- throw TypeCheckingExceptionPrivate(n, "combined cardinality constraint must be positive");
+ if( n[0].getConst<Rational>().getNumerator().sgn()==-1 ){
+ throw TypeCheckingExceptionPrivate(n, "combined cardinality constraint must be non-negative");
}
}
return nodeManager->booleanType();
# disabled for now :
# bug0909.smt2
+# lst-no-self-rev-exp.smt2
#if CVC4_BUILD_PROFILE_COMPETITION
#else
--- /dev/null
+; COMMAND-LINE: --finite-model-find --uf-ss-fair
+; EXPECT: sat
+(set-logic ALL_SUPPORTED)
+(declare-datatypes () ((Nat (succ (pred Nat)) (zero)) (Lst (cons (hd Nat) (tl Lst)) (nil))))
+
+(declare-fun app (Lst Lst) Lst)
+(declare-fun rev (Lst) Lst)
+
+(declare-sort I_app 0)
+(declare-sort I_rev 0)
+
+(declare-fun app_0_3 (I_app) Lst)
+(declare-fun app_1_4 (I_app) Lst)
+(declare-fun rev_0_5 (I_rev) Lst)
+
+(declare-fun xs () Lst)
+
+(assert (and
+
+(forall ((?i I_app)) (= (app (app_0_3 ?i) (app_1_4 ?i)) (ite (is-cons (app_0_3 ?i)) (cons (hd (app_0_3 ?i)) (app (tl (app_0_3 ?i)) (app_1_4 ?i))) (app_1_4 ?i))) )
+
+(forall ((?i I_rev)) (= (rev (rev_0_5 ?i)) (ite (is-cons (rev_0_5 ?i)) (app (rev (tl (rev_0_5 ?i))) (cons (hd (rev_0_5 ?i)) nil)) nil)) )
+
+(forall ((?i I_rev)) (or (not (is-cons (rev_0_5 ?i))) (and (not (forall ((?z I_app)) (not (and (= (app_0_3 ?z) (rev (tl (rev_0_5 ?i)))) (= (app_1_4 ?z) (cons (hd (rev_0_5 ?i)) nil)))) )) (not (forall ((?z I_rev)) (not (= (rev_0_5 ?z) (tl (rev_0_5 ?i)) )) )))) )
+
+(not (or (= xs (rev xs)) (forall ((?z I_rev)) (not (= (rev_0_5 ?z) xs)) )))
+
+))
+
+(check-sat)
+
projects / cvc5.git / commitdiff