diff options
27 files changed, 277 insertions, 97 deletions
diff --git a/src/parser/smt1/smt1.h b/src/parser/smt1/smt1.h index f96a4e810..c19b0f872 100644 --- a/src/parser/smt1/smt1.h +++ b/src/parser/smt1/smt1.h @@ -84,7 +84,8 @@ public: THEORY_REALS, THEORY_REALS_INTS, THEORY_STRINGS, - THEORY_QUANTIFIERS + THEORY_QUANTIFIERS, + THEORY_CARDINALITY_CONSTRAINT }; private: diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 8586bc9da..36f9866f4 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1112,7 +1112,7 @@ void SmtEngine::setDefaults() { if(!options::decisionMode.wasSetByUser()) { decision::DecisionMode decMode = // ALL_SUPPORTED - d_logic.hasEverything() ? decision::DECISION_STRATEGY_INTERNAL : + d_logic.hasEverything() ? decision::DECISION_STRATEGY_JUSTIFICATION : ( // QF_BV (not d_logic.isQuantified() && d_logic.isPure(THEORY_BV) @@ -1153,9 +1153,7 @@ void SmtEngine::setDefaults() { // QF_LRA (not d_logic.isQuantified() && d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isDifferenceLogic() && !d_logic.areIntegersUsed() - ) || - // Quantifiers - d_logic.isQuantified() + ) ? true : false ); @@ -1172,12 +1170,17 @@ void SmtEngine::setDefaults() { options::instWhenMode.set( quantifiers::INST_WHEN_LAST_CALL ); } } - if ( options::fmfBoundInt() ){ + if( d_logic.hasCardinalityConstraints() ){ + //must have finite model finding on + options::finiteModelFind.set( true ); + } + if( options::fmfBoundInt() ){ //must have finite model finding on options::finiteModelFind.set( true ); - if( options::mbqiMode()!=quantifiers::MBQI_NONE && - options::mbqiMode()!=quantifiers::MBQI_FMC && - options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL ){ + if( ! options::mbqiMode.wasSetByUser() || + ( options::mbqiMode()!=quantifiers::MBQI_NONE && + options::mbqiMode()!=quantifiers::MBQI_FMC && + options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL ) ){ //if bounded integers are set, use no MBQI by default options::mbqiMode.set( quantifiers::MBQI_NONE ); } diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 0c6842222..b00b4148d 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -889,14 +889,48 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ Trace("dt-model") << std::endl; printModelDebug( "dt-model" ); Trace("dt-model") << std::endl; + + /* + bool eq_merged = false; + std::vector< Node > all_eqc; + eq::EqClassesIterator eqcs1_i = eq::EqClassesIterator( &d_equalityEngine ); + while( !eqcs1_i.isFinished() ){ + Node eqc = (*eqcs1_i); + all_eqc.push_back( eqc ); + ++eqcs1_i; + } + //check if equivalence classes have merged + for( unsigned i=0; i<all_eqc.size(); i++ ){ + for( unsigned j=(i+1); j<all_eqc.size(); j++ ){ + if( m->areEqual( all_eqc[i], all_eqc[j] ) ){ + Trace("dt-cmi") << "Pre-already forced equal : " << all_eqc[i] << " = " << all_eqc[j] << std::endl; + eq_merged = true; + } + } + } + Assert( !eq_merged ); + */ + + //combine the equality engine m->assertEqualityEngine( &d_equalityEngine ); -/* - std::vector< TypeEnumerator > vec; - std::map< TypeNode, int > tes; + + /* + //check again if equivalence classes have merged + for( unsigned i=0; i<all_eqc.size(); i++ ){ + for( unsigned j=(i+1); j<all_eqc.size(); j++ ){ + if( m->areEqual( all_eqc[i], all_eqc[j] ) ){ + Trace("dt-cmi") << "Already forced equal : " << all_eqc[i] << " = " << all_eqc[j] << std::endl; + eq_merged = true; + } + } + } + Assert( !eq_merged ); */ + //get all constructors eq::EqClassesIterator eqccs_i = eq::EqClassesIterator( &d_equalityEngine ); std::vector< Node > cons; + std::vector< Node > nodes; while( !eqccs_i.isFinished() ){ Node eqc = (*eqccs_i); //for all equivalence classes that are datatypes @@ -904,28 +938,13 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ EqcInfo* ei = getOrMakeEqcInfo( eqc ); if( !ei->d_constructor.get().isNull() ){ cons.push_back( ei->d_constructor.get() ); - } - } - ++eqccs_i; - } - - //must choose proper representatives - std::vector< Node > nodes; - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); - while( !eqcs_i.isFinished() ){ - Node eqc = (*eqcs_i); - //for all equivalence classes that are datatypes - if( DatatypesRewriter::isTermDatatype( eqc ) ){ - EqcInfo* ei = getOrMakeEqcInfo( eqc ); - if( !ei->d_constructor.get().isNull() ){ - //specify that we should use the constructor as the representative - //m->assertRepresentative( ei->d_constructor.get() ); }else{ nodes.push_back( eqc ); } } - ++eqcs_i; + ++eqccs_i; } + unsigned index = 0; while( index<nodes.size() ){ Node eqc = nodes[index]; @@ -972,44 +991,22 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ } Trace("dt-cmi") << std::endl; /* - if( tes.find( eqc.getType() )==tes.end() ){ - tes[eqc.getType()]=vec.size(); - vec.push_back( TypeEnumerator( eqc.getType() ) ); - } - bool success; - Node n; - do { - success = true; - Assert( !vec[tes[eqc.getType()]].isFinished() ); - n = *vec[tes[eqc.getType()]]; - ++vec[tes[eqc.getType()]]; - Trace("dt-cmi-debug") << "Try " << n << "..." << std::endl; - //check if it is consistent with labels - size_t constructorIndex = Datatype::indexOf(n.getOperator().toExpr()); - if( constructorIndex<pcons.size() && pcons[constructorIndex] ){ - for( unsigned i=0; i<cons.size(); i++ ){ - //check if it is modulo equality the same - if( cons[i].getOperator()==n.getOperator() ){ - bool diff = false; - for( unsigned j=0; j<cons[i].getNumChildren(); j++ ){ - if( !m->areEqual( cons[i][j], n[j] ) ){ - diff = true; - break; - } - } - if( !diff ){ - Trace("dt-cmi-debug") << "...Already equivalent modulo equality to " << cons[i] << std::endl; - success = false; - break; - } - } - } - }else{ - Trace("dt-cmi-debug") << "...Not consistent with labels" << std::endl; - success = false; + std::map< int, std::map< int, bool > > sels; + Trace("dt-cmi") << "Existing selectors : "; + NodeListMap::iterator sel_i = d_selector_apps.find( eqc ); + if( sel_i != d_selector_apps.end() ){ + NodeList* sel = (*sel_i).second; + for( NodeList::const_iterator j = sel->begin(); j != sel->end(); j++ ){ + Expr selectorExpr = (*j).getOperator().toExpr(); + unsigned cindex = Datatype::cindexOf( selectorExpr ); + unsigned index = Datatype::indexOf( selectorExpr ); + sels[cindex][index] = true; + Trace("dt-cmi") << (*j) << " (" << cindex << ", " << index << ") "; } - }while( !success ); + } + Trace("dt-cmi") << std::endl; */ + const Datatype& dt = ((DatatypeType)(eqc.getType()).toType()).getDatatype(); for( unsigned r=0; r<2; r++ ){ if( neqc.isNull() ){ @@ -1017,6 +1014,7 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ if( pcons[i] && (r==1)==dt[ i ].isFinite() ){ neqc = getInstantiateCons( eqc, dt, i, false, false ); for( unsigned j=0; j<neqc.getNumChildren(); j++ ){ + //if( sels[i].find( j )==sels[i].end() && DatatypesRewriter::isTermDatatype( neqc[j] ) ){ if( !d_equalityEngine.hasTerm( neqc[j] ) && DatatypesRewriter::isTermDatatype( neqc[j] ) ){ nodes.push_back( neqc[j] ); } @@ -1030,6 +1028,24 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ Assert( !neqc.isNull() ); Trace("dt-cmi") << "Assign : " << neqc << std::endl; m->assertEquality( eqc, neqc, true ); + /* + for( unsigned kk=0; kk<all_eqc.size(); kk++ ){ + for( unsigned ll=(kk+1); ll<all_eqc.size(); ll++ ){ + if( m->areEqual( all_eqc[kk], all_eqc[ll] ) ){ + Trace("dt-cmi") << "Forced equal : " << kk << " " << ll << " : " << all_eqc[kk] << " = " << all_eqc[ll] << std::endl; + Node r = m->getRepresentative( all_eqc[kk] ); + Trace("dt-cmi") << " { "; + eq::EqClassIterator eqc_i = eq::EqClassIterator( r, m->d_equalityEngine ); + while( !eqc_i.isFinished() ){ + Trace("dt-cmi") << (*eqc_i) << " "; + ++eqc_i; + } + Trace("dt-cmi") << "} " << std::endl; + } + Assert( !m->areEqual( all_eqc[kk], all_eqc[ll] ) ); + } + } + */ //m->assertRepresentative( neqc ); cons.push_back( neqc ); ++index; diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index c079eecf9..78f4996b8 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -37,6 +37,7 @@ LogicInfo::LogicInfo() : d_reals(true), d_linear(true),// for now, "everything enabled" doesn't include non-linear arith d_differenceLogic(false), + d_cardinalityConstraints(false), d_locked(false) { for(TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id) { @@ -52,6 +53,7 @@ LogicInfo::LogicInfo(std::string logicString) throw(IllegalArgumentException) : d_reals(false), d_linear(false), d_differenceLogic(false), + d_cardinalityConstraints(false), d_locked(false) { setLogicString(logicString); @@ -66,6 +68,7 @@ LogicInfo::LogicInfo(const char* logicString) throw(IllegalArgumentException) : d_reals(false), d_linear(false), d_differenceLogic(false), + d_cardinalityConstraints(false), d_locked(false) { setLogicString(logicString); @@ -97,6 +100,9 @@ std::string LogicInfo::getLogicString() const { ss << "UF"; ++seen; } + if( d_cardinalityConstraints ){ + ss << "C"; + } if(d_theories[THEORY_BV]) { ss << "BV"; ++seen; @@ -191,6 +197,10 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc enableTheory(THEORY_UF); p += 2; } + if(!strncmp(p, "C", 1 )) { + d_cardinalityConstraints = true; + p += 1; + } // allow BV or DT in either order if(!strncmp(p, "BV", 2)) { enableTheory(THEORY_BV); diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h index a0777ae70..1c4b69b15 100644 --- a/src/theory/logic_info.h +++ b/src/theory/logic_info.h @@ -52,6 +52,7 @@ class CVC4_PUBLIC LogicInfo { bool d_reals; /**< are reals used in this logic? */ bool d_linear; /**< linear-only arithmetic in this logic? */ bool d_differenceLogic; /**< difference-only arithmetic in this logic? */ + bool d_cardinalityConstraints; /**< cardinality constraints in this logic? */ bool d_locked; /**< is this LogicInfo instance locked (and thus immutable)? */ @@ -175,6 +176,11 @@ public: CheckArgument(isTheoryEnabled(theory::THEORY_ARITH), *this, "Arithmetic not used in this LogicInfo; cannot ask whether it's difference logic"); return d_differenceLogic; } + /** Does this logic allow cardinality constraints? */ + bool hasCardinalityConstraints() const { + CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); + return d_cardinalityConstraints; + } // MUTATORS diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index f3203da4b..54be11b44 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -656,6 +656,7 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) { Node cond = d_models[op]->d_cond[i]; std::vector< Node > children; for( unsigned j=0; j<cond.getNumChildren(); j++) { + TypeNode tn = vars[j].getType(); if (isInterval(cond[j])){ if( !isStar(cond[j][0]) ){ children.push_back( NodeManager::currentNM()->mkNode( GEQ, vars[j], cond[j][0] ) ); @@ -663,7 +664,8 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) { if( !isStar(cond[j][1]) ){ children.push_back( NodeManager::currentNM()->mkNode( LT, vars[j], cond[j][1] ) ); } - }else if (!isStar(cond[j])){ + }else if ( !isStar(cond[j]) && //handle the case where there are 0 or 1 ground representatives of this type... + d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() && d_rep_set.d_type_reps[ tn ].size()>1 ){ Node c = getUsedRepresentative( cond[j] ); children.push_back( NodeManager::currentNM()->mkNode( EQUAL, vars[j], c ) ); } @@ -673,6 +675,7 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) { curr = NodeManager::currentNM()->mkNode( ITE, cc, v, curr ); } } + Trace("fmc-model") << "Made " << curr << " for " << op << std::endl; curr = Rewriter::rewrite( curr ); return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, curr); } diff --git a/src/theory/quantifiers/modes.cpp b/src/theory/quantifiers/modes.cpp index 10185914e..8bd97a8a7 100644 --- a/src/theory/quantifiers/modes.cpp +++ b/src/theory/quantifiers/modes.cpp @@ -79,8 +79,8 @@ std::ostream& operator<<(std::ostream& out, theory::quantifiers::AxiomInstMode m std::ostream& operator<<(std::ostream& out, theory::quantifiers::MbqiMode mode) { switch(mode) { - case theory::quantifiers::MBQI_DEFAULT: - out << "MBQI_DEFAULT"; + case theory::quantifiers::MBQI_GEN_EVAL: + out << "MBQI_GEN_EVAL"; break; case theory::quantifiers::MBQI_NONE: out << "MBQI_NONE"; @@ -94,6 +94,9 @@ std::ostream& operator<<(std::ostream& out, theory::quantifiers::MbqiMode mode) case theory::quantifiers::MBQI_INTERVAL: out << "MBQI_INTERVAL"; break; + case theory::quantifiers::MBQI_TRUST: + out << "MBQI_TRUST"; + break; default: out << "MbqiMode!UNKNOWN"; } diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h index 89e10b175..80534c8b0 100644 --- a/src/theory/quantifiers/modes.h +++ b/src/theory/quantifiers/modes.h @@ -58,13 +58,13 @@ typedef enum { } AxiomInstMode; typedef enum { - /** default, mbqi from CADE 24 paper */ - MBQI_DEFAULT, + /** mbqi from CADE 24 paper */ + MBQI_GEN_EVAL, /** no mbqi */ MBQI_NONE, /** implementation that mimics inst-gen */ MBQI_INST_GEN, - /** mbqi from Section 5.4.2 of AJR thesis */ + /** default, mbqi from Section 5.4.2 of AJR thesis */ MBQI_FMC, /** mbqi with integer intervals */ MBQI_FMC_INTERVAL, diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 0865f2c0b..b7f015f47 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -71,7 +71,7 @@ option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :de option eagerInstQuant --eager-inst-quant bool :default false apply quantifier instantiation eagerly -option fullSaturateQuant --full-saturate-quant bool :default true +option fullSaturateQuant --full-saturate-quant bool :default false when all other quantifier instantiation strategies fail, instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_NONE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToLiteralMatchMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkLiteralMatchMode :predicate-include "theory/quantifiers/options_handlers.h" @@ -95,7 +95,7 @@ option internalReps /--disable-quant-internal-reps bool :default true option finiteModelFind finite-model-find --finite-model-find bool :default false :read-write use finite model finding heuristic for quantifier instantiation -option mbqiMode --mbqi=MODE CVC4::theory::quantifiers::MbqiMode :read-write :default CVC4::theory::quantifiers::MBQI_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMbqiMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkMbqiMode :predicate-include "theory/quantifiers/options_handlers.h" +option mbqiMode --mbqi=MODE CVC4::theory::quantifiers::MbqiMode :read-write :default CVC4::theory::quantifiers::MBQI_FMC :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMbqiMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkMbqiMode :predicate-include "theory/quantifiers/options_handlers.h" choose mode for model-based quantifier instantiation option fmfOneInstPerRound --mbqi-one-inst-per-round bool :default false only add one instantiation per quantifier per round for mbqi diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index e9c754d4a..164e9e643 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -82,8 +82,8 @@ static const std::string mbqiModeHelp = "\ Model-based quantifier instantiation modes currently supported by the --mbqi option:\n\ \n\ default \n\ -+ Default, use model-based quantifier instantiation algorithm from CADE 24 finite\n\ - model finding paper.\n\ ++ Use algorithm from Section 5.4.2 of thesis Finite Model Finding in Satisfiability \n\ + Modulo Theories.\n\ \n\ none \n\ + Disable model-based quantifier instantiation.\n\ @@ -91,12 +91,12 @@ none \n\ instgen \n\ + Use instantiation algorithm that mimics Inst-Gen calculus. \n\ \n\ -fmc \n\ -+ Use algorithm from Section 5.4.2 of thesis Finite Model Finding in Satisfiability \n\ - Modulo Theories.\n\ +gen-ev \n\ ++ Default, use model-based quantifier instantiation algorithm from CADE 24 finite\n\ + model finding paper.\n\ \n\ fmc-interval \n\ -+ Same as fmc, but with intervals for models of integer functions.\n\ ++ Same as default, but with intervals for models of integer functions.\n\ \n\ interval \n\ + Use algorithm that abstracts domain elements as intervals. \n\ @@ -217,13 +217,13 @@ inline AxiomInstMode stringToAxiomInstMode(std::string option, std::string optar } inline MbqiMode stringToMbqiMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "default") { - return MBQI_DEFAULT; + if(optarg == "gen-ev") { + return MBQI_GEN_EVAL; } else if(optarg == "none") { return MBQI_NONE; } else if(optarg == "instgen") { return MBQI_INST_GEN; - } else if(optarg == "fmc") { + } else if(optarg == "default" || optarg == "fmc") { return MBQI_FMC; } else if(optarg == "fmc-interval") { return MBQI_FMC_INTERVAL; diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index ea1231e7a..e6ee8f53b 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -81,7 +81,7 @@ Node TermDb::getOperator( Node n ) { } d_par_op_map[op][tn1][tn2] = n; return n; - }else if( n.getKind()==APPLY_UF ){ + }else if( inst::Trigger::isAtomicTrigger( n ) ){ return n.getOperator(); }else{ return Node::null(); diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 9db32f894..57cf9001b 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -101,7 +101,12 @@ void TheoryUF::check(Effort level) { if (atom.getKind() == kind::EQUAL) { d_equalityEngine.assertEquality(atom, polarity, fact); } else if (atom.getKind() == kind::CARDINALITY_CONSTRAINT || atom.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT) { - // do nothing + if( d_thss == NULL ){ + std::stringstream ss; + ss << "Cardinality constraint " << atom << " was asserted, but the logic does not allow it." << std::endl; + ss << "Try using a logic containing \"UFC\"." << std::endl; + throw Exception( ss.str() ); + } } else { d_equalityEngine.assertPredicate(atom, polarity, fact); } diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index 8d70e4ffc..4d45d9148 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -36,6 +36,7 @@ namespace CVC4 { namespace expr { namespace attr { struct DatatypeIndexTag {}; + struct DatatypeConsIndexTag {}; struct DatatypeFiniteTag {}; struct DatatypeWellFoundedTag {}; struct DatatypeFiniteComputedTag {}; @@ -45,6 +46,7 @@ namespace expr { }/* CVC4::expr namespace */ typedef expr::Attribute<expr::attr::DatatypeIndexTag, uint64_t> DatatypeIndexAttr; +typedef expr::Attribute<expr::attr::DatatypeConsIndexTag, uint64_t> DatatypeConsIndexAttr; typedef expr::Attribute<expr::attr::DatatypeFiniteTag, bool> DatatypeFiniteAttr; typedef expr::Attribute<expr::attr::DatatypeWellFoundedTag, bool> DatatypeWellFoundedAttr; typedef expr::Attribute<expr::attr::DatatypeFiniteComputedTag, bool> DatatypeFiniteComputedAttr; @@ -81,6 +83,20 @@ size_t Datatype::indexOf(Expr item) { } } +size_t Datatype::cindexOf(Expr item) { + ExprManagerScope ems(item); + CheckArgument(item.getType().isSelector(), + item, + "arg must be a datatype selector"); + TNode n = Node::fromExpr(item); + if( item.getKind()==kind::APPLY_TYPE_ASCRIPTION ){ + return cindexOf( item[0] ); + }else{ + Assert(n.hasAttribute(DatatypeConsIndexAttr())); + return n.getAttribute(DatatypeConsIndexAttr()); + } +} + void Datatype::resolve(ExprManager* em, const std::map<std::string, DatatypeType>& resolutions, const std::vector<Type>& placeholders, @@ -103,7 +119,7 @@ void Datatype::resolve(ExprManager* em, d_resolved = true; size_t index = 0; for(std::vector<DatatypeConstructor>::iterator i = d_constructors.begin(), i_end = d_constructors.end(); i != i_end; ++i) { - (*i).resolve(em, self, resolutions, placeholders, replacements, paramTypes, paramReplacements); + (*i).resolve(em, self, resolutions, placeholders, replacements, paramTypes, paramReplacements, index); Node::fromExpr((*i).d_constructor).setAttribute(DatatypeIndexAttr(), index); Node::fromExpr((*i).d_tester).setAttribute(DatatypeIndexAttr(), index++); } @@ -401,7 +417,7 @@ void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self, const std::vector<Type>& placeholders, const std::vector<Type>& replacements, const std::vector< SortConstructorType >& paramTypes, - const std::vector< DatatypeType >& paramReplacements) + const std::vector< DatatypeType >& paramReplacements, size_t cindex) throw(IllegalArgumentException, DatatypeResolutionException) { CheckArgument(em != NULL, em, "cannot resolve a Datatype with a NULL expression manager"); @@ -447,6 +463,7 @@ void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self, } (*i).d_selector = nm->mkSkolem((*i).d_name, nm->mkSelectorType(selfTypeNode, TypeNode::fromType(range)), "is a selector", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr(); } + Node::fromExpr((*i).d_selector).setAttribute(DatatypeConsIndexAttr(), cindex); Node::fromExpr((*i).d_selector).setAttribute(DatatypeIndexAttr(), index++); (*i).d_resolved = true; } diff --git a/src/util/datatype.h b/src/util/datatype.h index 99a303950..02e0b6be8 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -191,7 +191,7 @@ private: const std::vector<Type>& placeholders, const std::vector<Type>& replacements, const std::vector< SortConstructorType >& paramTypes, - const std::vector< DatatypeType >& paramReplacements) + const std::vector< DatatypeType >& paramReplacements, size_t cindex) throw(IllegalArgumentException, DatatypeResolutionException); friend class Datatype; @@ -434,6 +434,12 @@ public: */ static size_t indexOf(Expr item) CVC4_PUBLIC; + /** + * Get the index of constructor corresponding to selector. (Zero is + * always the first index.) + */ + static size_t cindexOf(Expr item) CVC4_PUBLIC; + /** The type for iterators over constructors. */ typedef DatatypeConstructorIterator iterator; /** The (const) type for iterators over constructors. */ diff --git a/test/regress/regress0/bug512.smt2 b/test/regress/regress0/bug512.smt2 index b0c970f37..1c8a0626a 100644 --- a/test/regress/regress0/bug512.smt2 +++ b/test/regress/regress0/bug512.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --tlimit-per 2500 -iq ; EXPECT: unknown -; EXPECT: (:reason-unknown timeout) +; EXPECT: (:reason-unknown incomplete) ; EXPECT: unsat (set-option :print-success false) (set-info :smt-lib-version 2.0) diff --git a/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt b/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt index 536bc241f..f62f057e4 100644 --- a/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt +++ b/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt @@ -1,4 +1,4 @@ -% COMMAND-LINE: --finite-model-find +% COMMAND-LINE: --finite-model-find --mbqi=gen-ev % EXPECT: unsat (benchmark Isabelle :status sat diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index b9a87231f..395054d67 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -23,18 +23,23 @@ TESTS = \ agree466.smt2 \ ALG008-1.smt2 \ german169.smt2 \ - Hoare-z3.931718.smt \ QEpres-uf.855035.smt \ agree467.smt2 \ Arrow_Order-smtlib.778341.smt \ german73.smt2 \ PUZ001+1.smt2 \ refcount24.cvc.smt2 \ - bug0909.smt2 \ - fmf-bound-int.smt2 + fmf-bound-int.smt2 \ + fc-simple.smt2 \ + fc-unsat-tot-2.smt2 \ + fc-unsat-pent.smt2 \ + fc-pigeonhole19.smt2 EXTRA_DIST = $(TESTS) +# disabled for now : +# Hoare-z3.931718.smt bug0909.smt2 + #if CVC4_BUILD_PROFILE_COMPETITION #else #TESTS += \ diff --git a/test/regress/regress0/fmf/QEpres-uf.855035.smt b/test/regress/regress0/fmf/QEpres-uf.855035.smt index 980e5fd49..2945c8f4d 100644 --- a/test/regress/regress0/fmf/QEpres-uf.855035.smt +++ b/test/regress/regress0/fmf/QEpres-uf.855035.smt @@ -1,4 +1,4 @@ -% COMMAND-LINE: --finite-model-find +% COMMAND-LINE: --finite-model-find --mbqi=gen-ev % EXPECT: sat (benchmark Isabelle :status sat diff --git a/test/regress/regress0/fmf/fc-pigeonhole19.smt2 b/test/regress/regress0/fmf/fc-pigeonhole19.smt2 new file mode 100755 index 000000000..15c36682c --- /dev/null +++ b/test/regress/regress0/fmf/fc-pigeonhole19.smt2 @@ -0,0 +1,20 @@ +(set-logic UFC)
+(set-info :status unsat)
+
+(declare-sort P 0)
+(declare-sort H 0)
+
+(declare-fun p () P)
+(declare-fun h () H)
+
+; pigeonhole using native cardinality constraints
+(assert (fmf.card p 19))
+(assert (not (fmf.card p 18)))
+(assert (fmf.card h 18))
+(assert (not (fmf.card h 17)))
+
+; each pigeon has different holes
+(declare-fun f (P) H)
+(assert (forall ((p1 P) (p2 P)) (=> (not (= p1 p2)) (not (= (f p1) (f p2))))))
+
+(check-sat)
\ No newline at end of file diff --git a/test/regress/regress0/fmf/fc-simple.smt2 b/test/regress/regress0/fmf/fc-simple.smt2 new file mode 100755 index 000000000..d1fd2301c --- /dev/null +++ b/test/regress/regress0/fmf/fc-simple.smt2 @@ -0,0 +1,12 @@ +(set-logic QF_UFC) +(set-info :status unsat) + +(declare-sort U 0) + +(declare-fun a () U) +(declare-fun c () U) + +(assert (fmf.card c 2)) +(assert (not (fmf.card a 4))) + +(check-sat) diff --git a/test/regress/regress0/fmf/fc-unsat-pent.smt2 b/test/regress/regress0/fmf/fc-unsat-pent.smt2 new file mode 100755 index 000000000..f1721cb04 --- /dev/null +++ b/test/regress/regress0/fmf/fc-unsat-pent.smt2 @@ -0,0 +1,20 @@ +(set-logic QF_UFC)
+(set-info :status unsat)
+
+(declare-sort U 0)
+
+(declare-fun a () U)
+(declare-fun b () U)
+(declare-fun c () U)
+(declare-fun d () U)
+(declare-fun e () U)
+
+(assert (not (= a b)))
+(assert (not (= b c)))
+(assert (not (= c d)))
+(assert (not (= d e)))
+(assert (not (= e a)))
+
+(assert (fmf.card c 2))
+
+(check-sat)
\ No newline at end of file diff --git a/test/regress/regress0/fmf/fc-unsat-tot-2.smt2 b/test/regress/regress0/fmf/fc-unsat-tot-2.smt2 new file mode 100755 index 000000000..d946974ed --- /dev/null +++ b/test/regress/regress0/fmf/fc-unsat-tot-2.smt2 @@ -0,0 +1,14 @@ +(set-logic UFC)
+(set-info :status unsat)
+
+(declare-sort U 0)
+
+(declare-fun a () U)
+(declare-fun b () U)
+(declare-fun c () U)
+
+(assert (not (fmf.card a 2)))
+
+(assert (forall ((x U)) (or (= x a) (= x b))))
+
+(check-sat)
\ No newline at end of file diff --git a/test/regress/regress0/quantifiers/bug269.smt2 b/test/regress/regress0/quantifiers/bug269.smt2 index 0d5aedbb3..2e50030d1 100644 --- a/test/regress/regress0/quantifiers/bug269.smt2 +++ b/test/regress/regress0/quantifiers/bug269.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: --full-saturate-quant +; EXPECT: unsat (set-logic LRA) (set-info :status unsat) (declare-fun x4 () Real) diff --git a/test/regress/regress0/quantifiers/burns13.smt2 b/test/regress/regress0/quantifiers/burns13.smt2 index ad970a2b2..3424c161e 100644 --- a/test/regress/regress0/quantifiers/burns13.smt2 +++ b/test/regress/regress0/quantifiers/burns13.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: --full-saturate-quant --decision=internal +; EXPECT: unsat (set-logic AUFLIA) (set-info :source | Burns mutual exclusion protocol. This is a benchmark of the haRVey theorem prover. It was translated to SMT-LIB by Leonardo de Moura |) (set-info :smt-lib-version 2.0) diff --git a/test/regress/regress0/rewriterules/Makefile.am b/test/regress/regress0/rewriterules/Makefile.am index 3a3a097bd..31f99905c 100644 --- a/test/regress/regress0/rewriterules/Makefile.am +++ b/test/regress/regress0/rewriterules/Makefile.am @@ -23,16 +23,16 @@ MAKEFLAGS = -k # put it below in "TESTS +=" TESTS = \ length_trick.smt2 \ - length_trick2.smt2 \ length_gen_020.smt2 \ datatypes.smt2 \ datatypes_sat.smt2 \ reachability_back_to_the_future.smt2 \ relation.smt2 \ simulate_rewriting.smt2 \ - native_arrays.smt2 + native_arrays.smt2 \ + read5.smt2 -# reachability_bbttf_eT_arrays.smt2 set_A_new_fast_tableau-base.smt2 set_A_new_fast_tableau-base_sat.smt2 +# length_trick2.smt2 reachability_bbttf_eT_arrays.smt2 set_A_new_fast_tableau-base.smt2 set_A_new_fast_tableau-base_sat.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/rewriterules/read5.smt2 b/test/regress/regress0/rewriterules/read5.smt2 new file mode 100755 index 000000000..e66df7c7e --- /dev/null +++ b/test/regress/regress0/rewriterules/read5.smt2 @@ -0,0 +1,35 @@ +(set-logic AUF) +(set-info :source | +Translated from old SVC processor verification benchmarks. Contact Clark +Barrett at barrett@cs.nyu.edu for more information. + +This benchmark was automatically translated into SMT-LIB format from +CVC format using CVC Lite +|) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status unsat) +(declare-sort Index 0) +(declare-sort Element 0)(declare-sort Arr 0)(declare-fun aselect (Arr Index) Element)(declare-fun astore (Arr Index Element) Arr)(declare-fun k (Arr Arr) Index) +(declare-fun a () Index) +(declare-fun aaa () Index) +(declare-fun aa () Index) +(declare-fun S () Arr) +(declare-fun vvv () Element) +(declare-fun v () Element) +(declare-fun vv () Element) +(declare-fun bbb () Index) +(declare-fun www () Element) +(declare-fun bb () Index) +(declare-fun ww () Element) +(declare-fun b () Index) +(declare-fun w () Element) +(declare-fun SS () Arr) +(assert (let ((?v_3 (ite (= a aa) false true)) (?v_4 (ite (= aa aaa) false true)) (?v_1 (astore (astore (astore S a v) aa vv) aaa vvv)) (?v_0 (astore S aaa vvv)) (?v_2 (astore S aa vv))) (not (ite (ite (ite (ite (= a aaa) false true) (ite ?v_3 ?v_4 false) false) (ite (= (astore (astore ?v_0 a v) aa vv) ?v_1) (ite (= (astore (astore ?v_0 aa vv) a v) ?v_1) (ite (= (astore (astore ?v_2 a v) aaa vvv) ?v_1) (= (astore (astore ?v_2 aaa vvv) a v) ?v_1) false) false) false) true) (ite (ite (= ?v_1 (astore (astore (astore S bbb www) bb ww) b w)) (ite (ite ?v_3 (ite ?v_4 (ite (ite (= aa b) false true) (ite (ite (= aa bb) false true) (ite (= aa bbb) false true) false) false) false) false) (= (aselect S aa) vv) true) true) (ite (= S (astore SS a v)) (= S (astore SS a (aselect S a))) true) false) false)))) +; rewrite rule definition of arrays theory +(assert (forall ((?x Arr) (?i Index) (?j Index) (?e Element)) (! (=> (not (= ?i ?j)) (= (aselect (astore ?x ?i ?e) ?j) (aselect ?x ?j))) :rewrite-rule))) +(assert (forall ((?x Arr) (?i Index) (?e Element)) (! (=> true (= (aselect (astore ?x ?i ?e) ?i) ?e)) :rewrite-rule))) +(assert (forall ((?x Arr) (?y Arr)) (! (=> (not (= ?x ?y)) (not (= (aselect ?x (k ?x ?y)) (aselect ?y (k ?x ?y))))) :rewrite-rule))) +(assert (forall ((?x Arr) (?y Arr)) (! (! (=> true (or (= ?x ?y) (not (= ?x ?y)))) :pattern (?x)) :rewrite-rule))) +(assert (forall ((?x Arr) (?i Index) (?j Index) (?e Element)) (! (! (=> true (or (= ?i ?j) (not (= ?i ?j)))) :pattern ((aselect (astore ?x ?i ?e) ?j))) :rewrite-rule)))(check-sat) +(exit) diff --git a/test/regress/regress0/tptp/Makefile.am b/test/regress/regress0/tptp/Makefile.am index e0c8a2b48..e9274d2ee 100644 --- a/test/regress/regress0/tptp/Makefile.am +++ b/test/regress/regress0/tptp/Makefile.am @@ -35,7 +35,6 @@ TESTS = \ tff0.p \ tff0-arith.p \ ARI086$(equals)1.p \ - BOO003-4.p \ DAT001$(equals)1.p \ KRS018+1.p \ KRS063+1.p \ @@ -62,6 +61,7 @@ TEST_DEPS_DIST = \ EXTRA_DIST = $(TESTS) \ $(TEST_DEPS_DIST) \ BOO027-1.p \ + BOO003-4.p \ MGT031-1.p \ NLP114-1.p \ SYN075+1.p |