From 949dc989f72c680b98a4f7c4e52616b393237b52 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 31 Aug 2017 14:26:26 +0200 Subject: [PATCH] Answer unknown when uf-ss=no-minimal is combined with cardinality constraints from user input, add regressions. (#1060) --- src/theory/theory_model.cpp | 3 +- src/theory/uf/theory_uf_strong_solver.cpp | 414 +++++++++--------- src/theory/uf/theory_uf_strong_solver.h | 2 - test/regress/regress0/fmf/Makefile.am | 4 +- .../regress0/fmf/cruanes-no-minimal-unk.smt2 | 13 + test/regress/regress0/fmf/no-minimal-sat.smt2 | 19 + 6 files changed, 254 insertions(+), 201 deletions(-) create mode 100644 test/regress/regress0/fmf/cruanes-no-minimal-unk.smt2 create mode 100644 test/regress/regress0/fmf/no-minimal-sat.smt2 diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 75bc40af7..840bbd027 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -137,8 +137,7 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars, bool useDontCares) c return (*it).second; } Node ret = n; - if(n.getKind() == kind::EXISTS || n.getKind() == kind::FORALL || n.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT || - ( n.getKind() == kind::CARDINALITY_CONSTRAINT && options::ufssMode()!=theory::uf::UF_SS_FULL ) ) { + if(n.getKind() == kind::EXISTS || n.getKind() == kind::FORALL || n.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT ) { // We should have terms, thanks to TheoryQuantifiers::collectModelInfo(). // However, if the Decision Engine stops us early, there might be a // quantifier that isn't assigned. In conjunction with miniscoping, this diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 77459715f..e7efba325 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -697,6 +697,7 @@ bool SortModel::areDisequal( Node a, Node b ) { /** check */ void SortModel::check( Theory::Effort level, OutputChannel* out ){ + Assert( options::ufssMode()==UF_SS_FULL ); if( level>=Theory::EFFORT_STANDARD && d_hasCard && !d_conflict ){ Debug("uf-ss") << "StrongSolverTheoryUF: Check " << level << " " << d_type << std::endl; if( level==Theory::EFFORT_FULL ){ @@ -723,11 +724,9 @@ void SortModel::check( Theory::Effort level, OutputChannel* out ){ if( d_regions[i]->valid() ){ std::vector< Node > clique; if( d_regions[i]->check( level, d_cardinality, clique ) ){ - if( options::ufssMode()==UF_SS_FULL ){ - //add clique lemma - addCliqueLemma( clique, out ); - return; - } + //add clique lemma + addCliqueLemma( clique, out ); + return; }else{ Trace("uf-ss-debug") << "No clique in Region #" << i << std::endl; } @@ -797,10 +796,8 @@ void SortModel::check( Theory::Effort level, OutputChannel* out ){ int fcr = forceCombineRegion( i, false ); Debug("fmf-full-check") << "Combined regions " << i << " " << fcr << std::endl; Trace("uf-ss-debug") << "Combined regions " << i << " " << fcr << std::endl; - if( options::ufssMode()==UF_SS_FULL || fcr!=-1 ){ - recheck = true; - break; - } + recheck = true; + break; } } } @@ -1045,10 +1042,8 @@ void SortModel::checkRegion( int ri, bool checkCombine ){ //now check if region is in conflict std::vector< Node > clique; if( d_regions[ri]->check( Theory::EFFORT_STANDARD, d_cardinality, clique ) ){ - if( options::ufssMode()==UF_SS_FULL ){ - //explain clique - addCliqueLemma( clique, &d_thss->getOutputChannel() ); - } + //explain clique + addCliqueLemma( clique, &d_thss->getOutputChannel() ); } } } @@ -1228,24 +1223,6 @@ int SortModel::addSplit( Region* r, OutputChannel* out ){ } } Assert( s!=Node::null() ); - }else{ - if( options::ufssMode()!=UF_SS_FULL ){ - // Since candidate clique is not reported, we may need to find - // splits manually. - for ( Region::iterator it = r->begin(); it != r->end(); ++it ){ - if ( it->second->valid() ){ - for ( Region::iterator it2 = r->begin(); it2 != r->end(); ++it2 ){ - if ( it->second!=it2->second && it2->second->valid() ){ - if( !r->isDisequal( it->first, it2->first, 1 ) ){ - Node it_node = it->first; - Node it2_node = it2->first; - s = it_node.eqNode(it2_node); - } - } - } - } - } - } } if (!s.isNull() ){ //add lemma to output channel @@ -1811,112 +1788,120 @@ void StrongSolverTheoryUF::assertNode( Node n, bool isDecision ){ #endif bool polarity = n.getKind() != kind::NOT; TNode lit = polarity ? n : n[0]; - if( lit.getKind()==CARDINALITY_CONSTRAINT ){ - TypeNode tn = lit[0].getType(); - Assert( tn.isSort() ); - Assert( d_rep_model[tn] ); - int nCard = lit[1].getConst().getNumerator().getSignedInt(); - Node ct = d_rep_model[tn]->getCardinalityTerm(); - Trace("uf-ss-debug") << "...check cardinality terms : " << lit[0] << " " << ct << std::endl; - if( lit[0]==ct ){ - if( options::ufssFairnessMonotone() ){ - Trace("uf-ss-com-card-debug") << "...set master/slave" << std::endl; - if( tn!=d_tn_mono_master ){ - std::map< TypeNode, bool >::iterator it = d_tn_mono_slave.find( tn ); - if( it==d_tn_mono_slave.end() ){ - bool isMonotonic; - if( d_th->getQuantifiersEngine() ){ - isMonotonic = getSortInference()->isMonotonic( tn ); - }else{ - //if ground, everything is monotonic - isMonotonic = true; - } - if( isMonotonic ){ - if( d_tn_mono_master.isNull() ){ - Trace("uf-ss-com-card-debug") << "uf-ss-fair-monotone: Set master : " << tn << std::endl; - d_tn_mono_master = tn; + if( options::ufssMode()==UF_SS_FULL ){ + if( lit.getKind()==CARDINALITY_CONSTRAINT ){ + TypeNode tn = lit[0].getType(); + Assert( tn.isSort() ); + Assert( d_rep_model[tn] ); + int nCard = lit[1].getConst().getNumerator().getSignedInt(); + Node ct = d_rep_model[tn]->getCardinalityTerm(); + Trace("uf-ss-debug") << "...check cardinality terms : " << lit[0] << " " << ct << std::endl; + if( lit[0]==ct ){ + if( options::ufssFairnessMonotone() ){ + Trace("uf-ss-com-card-debug") << "...set master/slave" << std::endl; + if( tn!=d_tn_mono_master ){ + std::map< TypeNode, bool >::iterator it = d_tn_mono_slave.find( tn ); + if( it==d_tn_mono_slave.end() ){ + bool isMonotonic; + if( d_th->getQuantifiersEngine() ){ + isMonotonic = getSortInference()->isMonotonic( tn ); }else{ - Trace("uf-ss-com-card-debug") << "uf-ss-fair-monotone: Set slave : " << tn << std::endl; - d_tn_mono_slave[tn] = true; + //if ground, everything is monotonic + isMonotonic = true; + } + if( isMonotonic ){ + if( d_tn_mono_master.isNull() ){ + Trace("uf-ss-com-card-debug") << "uf-ss-fair-monotone: Set master : " << tn << std::endl; + d_tn_mono_master = tn; + }else{ + Trace("uf-ss-com-card-debug") << "uf-ss-fair-monotone: Set slave : " << tn << std::endl; + d_tn_mono_slave[tn] = true; + } + }else{ + Trace("uf-ss-com-card-debug") << "uf-ss-fair-monotone: Set non-monotonic : " << tn << std::endl; + d_tn_mono_slave[tn] = false; } - }else{ - Trace("uf-ss-com-card-debug") << "uf-ss-fair-monotone: Set non-monotonic : " << tn << std::endl; - d_tn_mono_slave[tn] = false; } } - } - //set the minimum positive cardinality for master if necessary - if( polarity && tn==d_tn_mono_master ){ - Trace("uf-ss-com-card-debug") << "...set min positive cardinality" << std::endl; - if( d_min_pos_tn_master_card.get()==-1 || nCardassertCardinality( d_out, nCard, polarity ); - //check if combined cardinality is violated - checkCombinedCardinality(); - }else{ - //otherwise, make equal via lemma - if( d_card_assertions_eqv_lemma.find( lit )==d_card_assertions_eqv_lemma.end() ){ - Node eqv_lit = NodeManager::currentNM()->mkNode( CARDINALITY_CONSTRAINT, ct, lit[1] ); - eqv_lit = lit.eqNode( eqv_lit ); - Trace("uf-ss-lemma") << "*** Cardinality equiv lemma : " << eqv_lit << std::endl; - getOutputChannel().lemma( eqv_lit ); - d_card_assertions_eqv_lemma[lit] = true; - } - } - }else if( lit.getKind()==COMBINED_CARDINALITY_CONSTRAINT ){ - d_com_card_assertions[lit] = polarity; - if( polarity ){ - //safe to assume int here - int nCard = lit[0].getConst().getNumerator().getSignedInt(); - if( d_min_pos_com_card.get()==-1 || nCardassertCardinality( d_out, nCard, polarity ); + //check if combined cardinality is violated checkCombinedCardinality(); + }else{ + //otherwise, make equal via lemma + if( d_card_assertions_eqv_lemma.find( lit )==d_card_assertions_eqv_lemma.end() ){ + Node eqv_lit = NodeManager::currentNM()->mkNode( CARDINALITY_CONSTRAINT, ct, lit[1] ); + eqv_lit = lit.eqNode( eqv_lit ); + Trace("uf-ss-lemma") << "*** Cardinality equiv lemma : " << eqv_lit << std::endl; + getOutputChannel().lemma( eqv_lit ); + d_card_assertions_eqv_lemma[lit] = true; + } } - }else{ - bool needsCard = true; - if( d_min_pos_com_card.get()==-1 ){ - //check if all current combined cardinality constraints are asserted negatively - for( std::map< int, Node >::iterator it = d_com_card_literal.begin(); it != d_com_card_literal.end(); ++it ){ - if( d_com_card_assertions.find( it->second )==d_com_card_assertions.end() ){ - Trace("uf-ss-com-card-debug") << "Does not need combined cardinality : non-assertion : " << it->first << std::endl; - needsCard = false; - break; - }else{ - Assert( !d_com_card_assertions[it->second] ); - } + }else if( lit.getKind()==COMBINED_CARDINALITY_CONSTRAINT ){ + d_com_card_assertions[lit] = polarity; + if( polarity ){ + //safe to assume int here + int nCard = lit[0].getConst().getNumerator().getSignedInt(); + if( d_min_pos_com_card.get()==-1 || nCard::iterator it = d_com_card_literal.begin(); it != d_com_card_literal.end(); ++it ){ + if( d_com_card_assertions.find( it->second )==d_com_card_assertions.end() ){ + Trace("uf-ss-com-card-debug") << "Does not need combined cardinality : non-assertion : " << it->first << std::endl; + needsCard = false; + break; + }else{ + Assert( !d_com_card_assertions[it->second] ); + } + } + }else{ + Trace("uf-ss-com-card-debug") << "Does not need combined cardinality : positive assertion : " << d_min_pos_com_card.get() << std::endl; + needsCard = false; + } + if( needsCard ){ + allocateCombinedCardinality(); + } } - } - }else{ - if( Trace.isOn("uf-ss-warn") ){ - ////FIXME: this is too strict: theory propagations are showing up as isDecision=true, but - //// a theory propagation is not a decision. - if( isDecision ){ - for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){ - if( !it->second->hasCardinalityAsserted() ){ - Trace("uf-ss-warn") << "WARNING: Assert " << n << " as a decision before cardinality for " << it->first << "." << std::endl; - //Message() << "Error: constraint asserted before cardinality for " << it->first << std::endl; - //Unimplemented(); + }else{ + if( Trace.isOn("uf-ss-warn") ){ + ////FIXME: this is too strict: theory propagations are showing up as isDecision=true, but + //// a theory propagation is not a decision. + if( isDecision ){ + for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){ + if( !it->second->hasCardinalityAsserted() ){ + Trace("uf-ss-warn") << "WARNING: Assert " << n << " as a decision before cardinality for " << it->first << "." << std::endl; + //Message() << "Error: constraint asserted before cardinality for " << it->first << std::endl; + //Unimplemented(); + } } } } - } - if( lit.getKind()!=EQUAL ){ - //it is a predicate - if( options::ufssDiseqPropagation() ){ - d_deq_prop->assertPredicate(lit, polarity); + if( lit.getKind()!=EQUAL ){ + //it is a predicate + if( options::ufssDiseqPropagation() ){ + d_deq_prop->assertPredicate(lit, polarity); + } } } + }else{ + if( lit.getKind()==CARDINALITY_CONSTRAINT || lit.getKind()==COMBINED_CARDINALITY_CONSTRAINT ){ + // cardinality constraint from user input, set incomplete + Trace("uf-ss") << "Literal " << lit << " not handled when uf ss mode is not FULL, set incomplete." << std::endl; + d_out->setIncomplete(); + } } Trace("uf-ss") << "Assert: done " << n << " " << isDecision << std::endl; } @@ -1943,20 +1928,57 @@ bool StrongSolverTheoryUF::areDisequal( Node a, Node b ) { /** check */ void StrongSolverTheoryUF::check( Theory::Effort level ){ if( !d_conflict ){ - Trace("uf-ss-solver") << "StrongSolverTheoryUF: check " << level << std::endl; - if( level==Theory::EFFORT_FULL && Debug.isOn( "uf-ss-debug" ) ){ - debugPrint( "uf-ss-debug" ); - } - for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){ - it->second->check( level, d_out ); - if( it->second->isConflict() ){ - d_conflict = true; - break; + if( options::ufssMode()==UF_SS_FULL ){ + Trace("uf-ss-solver") << "StrongSolverTheoryUF: check " << level << std::endl; + if( level==Theory::EFFORT_FULL && Debug.isOn( "uf-ss-debug" ) ){ + debugPrint( "uf-ss-debug" ); + } + for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){ + it->second->check( level, d_out ); + if( it->second->isConflict() ){ + d_conflict = true; + break; + } } - } - //check symmetry breaker - if( !d_conflict && options::ufssSymBreak() ){ - d_sym_break->check( level ); + //check symmetry breaker + if( !d_conflict && options::ufssSymBreak() ){ + d_sym_break->check( level ); + } + }else if( options::ufssMode()==UF_SS_NO_MINIMAL ){ + if( level==Theory::EFFORT_FULL ){ + // split on an equality between two equivalence classes (at most one per type) + std::map< TypeNode, std::vector< Node > > eqc_list; + std::map< TypeNode, bool > type_proc; + eq::EqClassesIterator eqcs_i(d_th->getEqualityEngine()); + while( !eqcs_i.isFinished() ){ + Node a = *eqcs_i; + TypeNode tn = a.getType(); + if( tn.isSort() ){ + if( type_proc.find( tn )==type_proc.end() ){ + std::map< TypeNode, std::vector< Node > >::iterator itel = eqc_list.find( tn ); + if( itel!=eqc_list.end() ){ + for( unsigned j=0; jsecond.size(); j++ ){ + Node b = itel->second[j]; + if( !d_th->getEqualityEngine()->areDisequal( a, b, false ) ){ + Node eq = Rewriter::rewrite( a.eqNode( b ) ); + Node lem = NodeManager::currentNM()->mkNode( kind::OR, eq, eq.negate() ); + Trace("uf-ss-lemma") << "*** Split (no-minimal) : " << lem << std::endl; + d_out->lemma( lem ); + d_out->requirePhase( eq, true ); + type_proc[tn] = true; + break; + } + } + } + eqc_list[tn].push_back( a ); + } + } + ++eqcs_i; + } + } + }else{ + // unhandled uf ss mode + Assert( false ); } Trace("uf-ss-solver") << "Done StrongSolverTheoryUF: check " << level << std::endl; } @@ -1970,39 +1992,34 @@ void StrongSolverTheoryUF::presolve() { } } -/** propagate */ -void StrongSolverTheoryUF::propagate( Theory::Effort level ){ - //for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){ - // it->second->propagate( level, d_out ); - //} -} - /** get next decision request */ Node StrongSolverTheoryUF::getNextDecisionRequest( unsigned& priority ){ //request the combined cardinality as a decision literal, if not already asserted - if( options::ufssFairness() ){ - int comCard = 0; - Node com_lit; - do { - if( comCard::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){ + Node n = it->second->getNextDecisionRequest(); + if( !n.isNull() ){ + priority = 1; + return n; } - }while( !com_lit.isNull() ); - } - //otherwise, check each individual sort - for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){ - Node n = it->second->getNextDecisionRequest(); - if( !n.isNull() ){ - priority = 1; - return n; } } Trace("uf-ss-dec") << "...no UF SS decisions." << std::endl; @@ -2010,42 +2027,44 @@ Node StrongSolverTheoryUF::getNextDecisionRequest( unsigned& priority ){ } void StrongSolverTheoryUF::preRegisterTerm( TNode n ){ - //initialize combined cardinality - initializeCombinedCardinality(); - - Trace("uf-ss-register") << "Preregister " << n << "." << std::endl; - //shouldn't have to preregister this type (it may be that there are no quantifiers over tn) - TypeNode tn = n.getType(); - std::map< TypeNode, SortModel* >::iterator it = d_rep_model.find( tn ); - if( it==d_rep_model.end() ){ - SortModel* rm = NULL; - if( tn.isSort() ){ - Trace("uf-ss-register") << "Create sort model " << tn << "." << std::endl; - rm = new SortModel( n, d_th->getSatContext(), d_th->getUserContext(), this ); - //getOutputChannel().lemma( n.eqNode( rm->getCardinalityTerm() ) ); - }else{ - /* - if( tn==NodeManager::currentNM()->integerType() || tn==NodeManager::currentNM()->realType() ){ - Debug("uf-ss-na") << "Error: Cannot perform finite model finding on arithmetic quantifier"; - Debug("uf-ss-na") << " (" << f << ")"; - Debug("uf-ss-na") << std::endl; - Unimplemented("Cannot perform finite model finding on arithmetic quantifier"); - }else if( tn.isDatatype() ){ - Debug("uf-ss-na") << "Error: Cannot perform finite model finding on datatype quantifier"; - Debug("uf-ss-na") << " (" << f << ")"; - Debug("uf-ss-na") << std::endl; - Unimplemented("Cannot perform finite model finding on datatype quantifier"); + if( options::ufssMode()==UF_SS_FULL ){ + //initialize combined cardinality + initializeCombinedCardinality(); + + Trace("uf-ss-register") << "Preregister " << n << "." << std::endl; + //shouldn't have to preregister this type (it may be that there are no quantifiers over tn) + TypeNode tn = n.getType(); + std::map< TypeNode, SortModel* >::iterator it = d_rep_model.find( tn ); + if( it==d_rep_model.end() ){ + SortModel* rm = NULL; + if( tn.isSort() ){ + Trace("uf-ss-register") << "Create sort model " << tn << "." << std::endl; + rm = new SortModel( n, d_th->getSatContext(), d_th->getUserContext(), this ); + //getOutputChannel().lemma( n.eqNode( rm->getCardinalityTerm() ) ); + }else{ + /* + if( tn==NodeManager::currentNM()->integerType() || tn==NodeManager::currentNM()->realType() ){ + Debug("uf-ss-na") << "Error: Cannot perform finite model finding on arithmetic quantifier"; + Debug("uf-ss-na") << " (" << f << ")"; + Debug("uf-ss-na") << std::endl; + Unimplemented("Cannot perform finite model finding on arithmetic quantifier"); + }else if( tn.isDatatype() ){ + Debug("uf-ss-na") << "Error: Cannot perform finite model finding on datatype quantifier"; + Debug("uf-ss-na") << " (" << f << ")"; + Debug("uf-ss-na") << std::endl; + Unimplemented("Cannot perform finite model finding on datatype quantifier"); + } + */ } - */ - } - if( rm ){ - rm->initialize( d_out ); - d_rep_model[tn] = rm; - //d_rep_model_init[tn] = true; + if( rm ){ + rm->initialize( d_out ); + d_rep_model[tn] = rm; + //d_rep_model_init[tn] = true; + } + }else{ + //ensure sort model is initialized + it->second->initialize( d_out ); } - }else{ - //ensure sort model is initialized - it->second->initialize( d_out ); } } @@ -2139,6 +2158,7 @@ bool StrongSolverTheoryUF::debugModel( TheoryModel* m ){ /** initialize */ void StrongSolverTheoryUF::initializeCombinedCardinality() { + Assert( options::ufssMode()==UF_SS_FULL ); if( options::ufssFairness() ){ if( d_aloc_com_card.get()==0 ){ Trace("uf-ss-com-card-debug") << "Initialize combined cardinality" << std::endl; @@ -2149,6 +2169,7 @@ void StrongSolverTheoryUF::initializeCombinedCardinality() { /** check */ void StrongSolverTheoryUF::checkCombinedCardinality() { + Assert( options::ufssMode()==UF_SS_FULL ); if( options::ufssFairness() ){ Trace("uf-ss-com-card-debug") << "Check combined cardinality, get maximum negative cardinalities..." << std::endl; int totalCombinedCard = 0; @@ -2231,6 +2252,7 @@ void StrongSolverTheoryUF::checkCombinedCardinality() { } void StrongSolverTheoryUF::allocateCombinedCardinality() { + Assert( options::ufssMode()==UF_SS_FULL ); Trace("uf-ss-com-card") << "Allocate combined cardinality (" << d_aloc_com_card.get() << ")" << std::endl; //make node Node lem = NodeManager::currentNM()->mkNode( COMBINED_CARDINALITY_CONSTRAINT, diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h index b477a7eb5..a7239dba5 100644 --- a/src/theory/uf/theory_uf_strong_solver.h +++ b/src/theory/uf/theory_uf_strong_solver.h @@ -396,8 +396,6 @@ public: void check( Theory::Effort level ); /** presolve */ void presolve(); - /** propagate */ - void propagate( Theory::Effort level ); /** get next decision request */ Node getNextDecisionRequest( unsigned& priority ); /** preregister a term */ diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index b02443989..4f81d79aa 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -74,7 +74,9 @@ TESTS = \ bug-041417-set-options.cvc \ alg202+1.smt2 \ fmf-fun-no-elim-ext-arith.smt2 \ - fmf-fun-no-elim-ext-arith2.smt2 + fmf-fun-no-elim-ext-arith2.smt2 \ + cruanes-no-minimal-unk.smt2 \ + no-minimal-sat.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/fmf/cruanes-no-minimal-unk.smt2 b/test/regress/regress0/fmf/cruanes-no-minimal-unk.smt2 new file mode 100644 index 000000000..f38a3ce41 --- /dev/null +++ b/test/regress/regress0/fmf/cruanes-no-minimal-unk.smt2 @@ -0,0 +1,13 @@ +; COMMAND-LINE: --finite-model-find --uf-ss=no-minimal +; EXPECT: unknown +(set-logic UFC) +; generated by Nunchaku +(declare-sort i_ 0) +(declare-fun __nun_card_witness_0_ () i_) +(assert (fmf.card __nun_card_witness_0_ 2)) +(declare-fun i2_ () i_) +(declare-fun i1_ () i_) +(declare-fun i3_ () i_) +(assert (and (not (= i2_ i3_)) (not (= i1_ i2_)) (not (= i1_ i3_)))) +(check-sat) + diff --git a/test/regress/regress0/fmf/no-minimal-sat.smt2 b/test/regress/regress0/fmf/no-minimal-sat.smt2 new file mode 100644 index 000000000..dfb7899ce --- /dev/null +++ b/test/regress/regress0/fmf/no-minimal-sat.smt2 @@ -0,0 +1,19 @@ +; COMMAND-LINE: --finite-model-find --uf-ss=no-minimal +; EXPECT: sat +(set-logic UF) +(set-info :status sat) +; generated by Nunchaku +(declare-sort i_ 0) +(declare-fun i2_ () i_) +(declare-fun i1_ () i_) +(declare-fun i3_ () i_) +(assert (and (not (= i2_ i3_)) (not (= i1_ i2_)) (not (= i1_ i3_)))) +(declare-fun i4_ () i_) +(declare-fun i5_ () i_) +(declare-fun i6_ () i_) +(assert (distinct i4_ i5_ i6_)) +(declare-fun P (i_) Bool) +(declare-fun f (i_) i_) +(assert (forall ((x i_)) (P (f x)))) +(check-sat) + -- 2.30.2