diff options
Diffstat (limited to 'src')
42 files changed, 1013 insertions, 443 deletions
diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index 27d1249a1..427282490 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -1189,7 +1189,7 @@ void ValidityChecker::dataType(const std::vector<std::string>& names, // Set up the datatype specifications. for(unsigned i = 0; i < names.size(); ++i) { - CVC4::Datatype dt(names[i]); + CVC4::Datatype dt(names[i], false); CVC4::CheckArgument(constructors[i].size() == selectors[i].size(), "expected sub-vectors in constructors and selectors vectors to match in size"); CVC4::CheckArgument(constructors[i].size() == types[i].size(), "expected sub-vectors in constructors and types vectors to match in size"); for(unsigned j = 0; j < constructors[i].size(); ++j) { diff --git a/src/cvc4.i b/src/cvc4.i index c0042b513..fcd5a8470 100644 --- a/src/cvc4.i +++ b/src/cvc4.i @@ -71,7 +71,7 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters; %template(vectorString) std::vector< std::string >; %template(vectorPairStringType) std::vector< std::pair< std::string, CVC4::Type > >; %template(pairStringType) std::pair< std::string, CVC4::Type >; -%template(setType) std::set< CVC4::Type >; +%template(setOfType) std::set< CVC4::Type >; %template(hashmapExpr) std::hash_map< CVC4::Expr, CVC4::Expr, CVC4::ExprHashFunction >; // This is unfortunate, but seems to be necessary; if we leave NULL diff --git a/src/lib/clock_gettime.h b/src/lib/clock_gettime.h index 43c3395a4..8860e717b 100644 --- a/src/lib/clock_gettime.h +++ b/src/lib/clock_gettime.h @@ -30,7 +30,7 @@ /* otherwise, we have to define it */ -#if defined(__WIN32__) && !defined(__WIN64__) +#if defined(__WIN32__) && !defined(_W64) #ifdef __cplusplus extern "C" { @@ -45,12 +45,12 @@ struct timespec { }/* extern "C" */ #endif /* __cplusplus */ -#else /* !__WIN32__ || __WIN64__ */ +#else /* !__WIN32__ || _W64 */ /* get timespec from <time.h> */ #include <time.h> -#endif /* __WIN32__ && !__WIN64__ */ +#endif /* __WIN32__ && !_W64 */ #ifdef __cplusplus extern "C" { diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 792c3cf9d..f9055f5db 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -2018,7 +2018,7 @@ datatypeDef[std::vector<CVC4::Datatype>& datatypes] params.push_back( t ); } )* RBRACKET )? - { datatypes.push_back(Datatype(id, params)); + { datatypes.push_back(Datatype(id, params, false)); if(!PARSER_STATE->isUnresolvedType(id)) { // if not unresolved, must be undeclared PARSER_STATE->checkDeclaration(id, CHECK_UNDECLARED, SYM_SORT); 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/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 659fc97d9..8dcebc5ee 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -344,6 +344,28 @@ command returns [CVC4::Command* cmd = NULL] Expr func = PARSER_STATE->mkFunction(name, t, ExprManager::VAR_FLAG_DEFINED); $cmd = new DefineFunctionCommand(name, func, terms, expr); } + | DEFINE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); } + symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] + { PARSER_STATE->checkUserSymbol(name); } + sortSymbol[t,CHECK_DECLARED] + { /* add variables to parser state before parsing term */ + Debug("parser") << "define const: '" << name << "'" << std::endl; + PARSER_STATE->pushScope(true); + for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i = + sortedVarNames.begin(), iend = sortedVarNames.end(); + i != iend; + ++i) { + terms.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second)); + } + } + term[expr, expr2] + { PARSER_STATE->popScope(); + // declare the name down here (while parsing term, signature + // must not be extended with the name itself; no recursion + // permitted) + Expr func = PARSER_STATE->mkFunction(name, t, ExprManager::VAR_FLAG_DEFINED); + $cmd = new DefineFunctionCommand(name, func, terms, expr); + } | /* value query */ GET_VALUE_TOK { PARSER_STATE->checkThatLogicIsSet(); } ( LPAREN_TOK termList[terms,expr] RPAREN_TOK @@ -464,17 +486,8 @@ extendedCommand[CVC4::Command*& cmd] } /* Extended SMT-LIB set of commands syntax, not permitted in * --smtlib2 compliance mode. */ - : DECLARE_DATATYPES_TOK { PARSER_STATE->checkThatLogicIsSet(); } - { /* open a scope to keep the UnresolvedTypes contained */ - PARSER_STATE->pushScope(true); } - LPAREN_TOK /* parametric sorts */ - ( symbol[name,CHECK_UNDECLARED,SYM_SORT] { - sorts.push_back( PARSER_STATE->mkSort(name) ); } - )* - RPAREN_TOK - LPAREN_TOK ( LPAREN_TOK datatypeDef[dts, sorts] RPAREN_TOK )+ RPAREN_TOK - { PARSER_STATE->popScope(); - cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); } + : DECLARE_DATATYPES_TOK datatypesDefCommand[false, cmd] + | DECLARE_CODATATYPES_TOK datatypesDefCommand[true, cmd] | /* get model */ GET_MODEL_TOK { PARSER_STATE->checkThatLogicIsSet(); } { cmd = new GetModelCommand(); } @@ -496,7 +509,7 @@ extendedCommand[CVC4::Command*& cmd] sortSymbol[t,CHECK_DECLARED] { Expr c = PARSER_STATE->mkVar(name, t); $cmd = new DeclareFunctionCommand(name, c, t); } - + | DECLARE_SORTS_TOK { PARSER_STATE->checkThatLogicIsSet(); } { if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF) && !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_ARRAYS) && @@ -603,6 +616,26 @@ extendedCommand[CVC4::Command*& cmd] { cmd = new SimplifyCommand(e); } ; + +datatypesDefCommand[bool isCo, CVC4::Command*& cmd] +@declarations { + std::vector<CVC4::Datatype> dts; + std::string name; + std::vector<Type> sorts; +} + : { PARSER_STATE->checkThatLogicIsSet(); + /* open a scope to keep the UnresolvedTypes contained */ + PARSER_STATE->pushScope(true); } + LPAREN_TOK /* parametric sorts */ + ( symbol[name,CHECK_UNDECLARED,SYM_SORT] { + sorts.push_back( PARSER_STATE->mkSort(name) ); } + )* + RPAREN_TOK + LPAREN_TOK ( LPAREN_TOK datatypeDef[isCo, dts, sorts] RPAREN_TOK )+ RPAREN_TOK + { PARSER_STATE->popScope(); + cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); } + ; + rewriterulesCommand[CVC4::Command*& cmd] @declarations { std::vector<std::pair<std::string, Type> > sortedVarNames; @@ -1530,7 +1563,7 @@ nonemptyNumeralList[std::vector<uint64_t>& numerals] /** * Parses a datatype definition */ -datatypeDef[std::vector<CVC4::Datatype>& datatypes, std::vector< CVC4::Type >& params] +datatypeDef[bool isCo, std::vector<CVC4::Datatype>& datatypes, std::vector< CVC4::Type >& params] @init { std::string id; } @@ -1548,7 +1581,7 @@ datatypeDef[std::vector<CVC4::Datatype>& datatypes, std::vector< CVC4::Type >& p params.push_back( t ); } )* ']' )?*/ //AJR: this isn't necessary if we use z3's style - { datatypes.push_back(Datatype(id,params)); + { datatypes.push_back(Datatype(id,params,isCo)); if(!PARSER_STATE->isUnresolvedType(id)) { // if not unresolved, must be undeclared PARSER_STATE->checkDeclaration(id, CHECK_UNDECLARED, SYM_SORT); @@ -1623,6 +1656,7 @@ AS_TOK : 'as'; // extended commands DECLARE_DATATYPES_TOK : 'declare-datatypes'; +DECLARE_CODATATYPES_TOK : 'declare-codatatypes'; GET_MODEL_TOK : 'get-model'; ECHO_TOK : 'echo'; REWRITE_RULE_TOK : 'assert-rewrite'; @@ -1633,6 +1667,7 @@ DECLARE_FUNS_TOK : 'declare-funs'; DECLARE_PREDS_TOK : 'declare-preds'; DEFINE_TOK : 'define'; DECLARE_CONST_TOK : 'declare-const'; +DEFINE_CONST_TOK : 'define-const'; SIMPLIFY_TOK : 'simplify'; INCLUDE_TOK : 'include'; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 64b321613..e9e6ba857 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -158,6 +158,7 @@ void Smt2::addTheory(Theory theory) { Parser::addOperator(kind::APPLY_CONSTRUCTOR); Parser::addOperator(kind::APPLY_TESTER); Parser::addOperator(kind::APPLY_SELECTOR); + Parser::addOperator(kind::APPLY_SELECTOR_TOTAL); break; case THEORY_STRINGS: diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 4d784c383..63529c2a5 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -316,6 +316,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo break; case kind::APPLY_CONSTRUCTOR: case kind::APPLY_SELECTOR: + case kind::APPLY_SELECTOR_TOTAL: case kind::APPLY_TESTER: toStream(op, n.getOperator(), depth, types, false); break; diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index ea335f2e5..1250bc659 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -424,6 +424,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::APPLY_TESTER: case kind::APPLY_CONSTRUCTOR: case kind::APPLY_SELECTOR: + case kind::APPLY_SELECTOR_TOTAL: case kind::PARAMETRIC_DATATYPE: break; diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index 4555aac51..c779af4ff 100644 --- a/src/smt/boolean_terms.cpp +++ b/src/smt/boolean_terms.cpp @@ -46,7 +46,8 @@ BooleanTermConverter::BooleanTermConverter(SmtEngine& smt) : d_varCache(smt.d_userContext), d_termCache(smt.d_userContext), d_typeCache(), - d_datatypeCache() { + d_datatypeCache(), + d_datatypeReverseCache() { // set up our "false" and "true" conversions based on command-line option if(options::booleanTermConversionMode() == BOOLEAN_TERM_CONVERT_TO_BITVECTORS || @@ -116,6 +117,10 @@ static inline bool isBoolean(TNode top, unsigned i) { // to be for model-substitution, so the "in" is a Boolean-term-converted // node, and "as" is the original. See how it's used in function // handling, below. +// +// Note this isn't the case any longer, and parts of what's below have +// been repurposed for *forward* conversion, meaning this works in either +// direction. Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as) throw() { if(in.getType() == as) { return in; @@ -133,7 +138,12 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as) throw() { } Assert(as.isDatatype()); const Datatype* dt2 = &as.getDatatype(); - const Datatype* dt1 = d_datatypeCache[dt2]; + const Datatype* dt1; + if(d_datatypeCache.find(dt2) != d_datatypeCache.end()) { + dt1 = d_datatypeCache[dt2]; + } else { + dt1 = d_datatypeReverseCache[dt2]; + } Assert(dt1 != NULL, "expected datatype in cache"); Assert(*dt1 == in.getType().getDatatype(), "improper rewriteAs() between datatypes"); Node out; @@ -142,7 +152,7 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as) throw() { NodeBuilder<> appctorb(kind::APPLY_CONSTRUCTOR); appctorb << (*dt2)[i].getConstructor(); for(size_t j = 0; j < ctor.getNumArgs(); ++j) { - appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, ctor[j].getSelector(), in), TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType())); + appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, ctor[j].getSelector(), in), TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType())); } Node appctor = appctorb; if(i == 0) { @@ -165,7 +175,12 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as) throw() { fromParams.push_back(TypeNode::fromType(dt2->getParameter(i))); toParams.push_back(as[i + 1]); } - const Datatype* dt1 = d_datatypeCache[dt2]; + const Datatype* dt1; + if(d_datatypeCache.find(dt2) != d_datatypeCache.end()) { + dt1 = d_datatypeCache[dt2]; + } else { + dt1 = d_datatypeReverseCache[dt2]; + } Assert(dt1 != NULL, "expected datatype in cache"); Assert(*dt1 == in.getType()[0].getDatatype(), "improper rewriteAs() between datatypes"); Node out; @@ -176,7 +191,7 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as) throw() { for(size_t j = 0; j < ctor.getNumArgs(); ++j) { TypeNode asType = TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType()); asType = asType.substitute(fromParams.begin(), fromParams.end(), toParams.begin(), toParams.end()); - appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, ctor[j].getSelector(), in), asType); + appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, ctor[j].getSelector(), in), asType); } Node appctor = appctorb; if(i == 0) { @@ -213,9 +228,9 @@ const Datatype& BooleanTermConverter::convertDatatype(const Datatype& dt) throw( } vector<Datatype> newDtVector; if(dt.isParametric()) { - newDtVector.push_back(Datatype(dt.getName() + "'", dt.getParameters())); + newDtVector.push_back(Datatype(dt.getName() + "'", dt.getParameters(), false)); } else { - newDtVector.push_back(Datatype(dt.getName() + "'")); + newDtVector.push_back(Datatype(dt.getName() + "'", false)); } Datatype& newDt = newDtVector.front(); Debug("boolean-terms") << "found a Boolean arg in constructor " << (*c).getName() << endl; @@ -259,11 +274,13 @@ const Datatype& BooleanTermConverter::convertDatatype(const Datatype& dt) throw( } } out = &newD; + d_datatypeReverseCache[&newD] = &dt; return newD; } } } + // this is identity; don't need the reverse cache out = &dt; return dt; diff --git a/src/smt/boolean_terms.h b/src/smt/boolean_terms.h index b289e3469..bdd9ff839 100644 --- a/src/smt/boolean_terms.h +++ b/src/smt/boolean_terms.h @@ -69,6 +69,8 @@ class BooleanTermConverter { BooleanTermTypeCache d_typeCache; /** The cache used during Boolean term datatype conversion */ BooleanTermDatatypeCache d_datatypeCache; + /** A (reverse) cache for Boolean term datatype conversion */ + BooleanTermDatatypeCache d_datatypeReverseCache; Node rewriteAs(TNode in, TypeNode as) throw(); 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/smt/smt_engine_check_proof.cpp b/src/smt/smt_engine_check_proof.cpp index a731ff024..4c218b48c 100644 --- a/src/smt/smt_engine_check_proof.cpp +++ b/src/smt/smt_engine_check_proof.cpp @@ -57,10 +57,11 @@ void SmtEngine::checkProof() { Chat() << "checking proof..." << endl; - if(!d_logic.isPure(theory::THEORY_BOOL) && - !d_logic.isPure(theory::THEORY_UF)) { + if( ! ( d_logic.isPure(theory::THEORY_BOOL) || + ( d_logic.isPure(theory::THEORY_UF) && + ! d_logic.hasCardinalityConstraints() ) ) ) { // no checking for these yet - Notice() << "Notice: no proof-checking for non-UF proofs yet" << endl; + Notice() << "Notice: no proof-checking for non-UF/Bool proofs yet" << endl; return; } diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index b3383e6c4..d140d1990 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -302,6 +302,7 @@ variable SKOLEM "skolem var" operator SEXPR 0: "a symbolic expression" operator LAMBDA 2 "lambda" +operator MU 2 "mu" parameterized CHAIN CHAIN_OP 2: "chained operator" constant CHAIN_OP \ @@ -334,6 +335,7 @@ typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule typerule SEXPR ::CVC4::theory::builtin::SExprTypeRule typerule LAMBDA ::CVC4::theory::builtin::LambdaTypeRule +typerule MU ::CVC4::theory::builtin::MuTypeRule typerule CHAIN ::CVC4::theory::builtin::ChainTypeRule typerule CHAIN_OP ::CVC4::theory::builtin::ChainedOperatorTypeRule diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 0ebcb31e8..3c8953e15 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -164,6 +164,24 @@ public: } };/* class LambdaTypeRule */ +class MuTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { + if( n[0].getType(check) != nodeManager->boundVarListType() ) { + std::stringstream ss; + ss << "expected a bound var list for MU expression, got `" + << n[0].getType().toString() << "'"; + throw TypeCheckingExceptionPrivate(n, ss.str()); + } + std::vector<TypeNode> argTypes; + for(TNode::iterator i = n[0].begin(); i != n[0].end(); ++i) { + argTypes.push_back((*i).getType()); + } + TypeNode rangeType = n[1].getType(check); + return nodeManager->mkFunctionType(argTypes, rangeType); + } +};/* class MuTypeRule */ + class ChainTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index 37a656555..dc85d0cd6 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -88,7 +88,7 @@ public: const Record& rec = in[0].getType().getAttribute(expr::DatatypeRecordAttr()).getConst<Record>(); return RewriteResponse(REWRITE_DONE, in[0][rec.getIndex(in.getOperator().getConst<RecordSelect>().getField())]); } - if(in.getKind() == kind::APPLY_SELECTOR && + if(in.getKind() == kind::APPLY_SELECTOR_TOTAL && (in[0].getKind() == kind::TUPLE || in[0].getKind() == kind::RECORD)) { // These strange (half-tuple-converted) terms can be created by // the system if you have something like "foo.1" for a tuple @@ -118,7 +118,7 @@ public: Debug("tuprec") << "==> returning " << in[0][selectorIndex] << std::endl; return RewriteResponse(REWRITE_DONE, in[0][selectorIndex]); } - if(in.getKind() == kind::APPLY_SELECTOR && + if(in.getKind() == kind::APPLY_SELECTOR_TOTAL && in[0].getKind() == kind::APPLY_CONSTRUCTOR) { // Have to be careful not to rewrite well-typed expressions // where the selector doesn't match the constructor, @@ -138,26 +138,25 @@ public: << std::endl; return RewriteResponse(REWRITE_DONE, in[0][selectorIndex]); }else{ - if( options::dtRewriteErrorSel() ){ - 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.isDatatype() && !gtt.isInstantiatedDatatype() ){ - gt = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, - NodeManager::currentNM()->mkConst(AscriptionType(in.getType().toType())), gt); - } - Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: " - << "Rewrite trivial selector " << in - << " to distinguished ground term " - << in.getType().mkGroundTerm() << std::endl; - return RewriteResponse(REWRITE_DONE,gt ); + //typically should not be called + 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.isDatatype() && !gtt.isInstantiatedDatatype() ){ + gt = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, + NodeManager::currentNM()->mkConst(AscriptionType(in.getType().toType())), gt); + } + Trace("datatypes-rewrite") << "DatatypesRewriter::postRewrite: " + << "Rewrite trivial selector " << in + << " to distinguished ground term " + << in.getType().mkGroundTerm() << std::endl; + return RewriteResponse(REWRITE_DONE,gt ); } } if(in.getKind() == kind::TUPLE_SELECT && @@ -204,11 +203,17 @@ public: return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true)); } - if(in.getKind() == kind::EQUAL && - checkClash(in[0], in[1])) { - Trace("datatypes-rewrite") << "Rewrite clashing equality " << in << " to false" << std::endl; - return RewriteResponse(REWRITE_DONE, - NodeManager::currentNM()->mkConst(false)); + if(in.getKind() == kind::EQUAL ) { + std::vector< Node > rew; + if( checkClash(in[0], in[1], rew) ){ + Trace("datatypes-rewrite") << "Rewrite clashing equality " << in << " to false" << std::endl; + return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(false)); + }else if( rew.size()==1 && rew[0]!=in ){ + Trace("datatypes-rewrite") << "Rewrite equality " << in << " to " << rew[0] << std::endl; + return RewriteResponse(REWRITE_AGAIN_FULL, rew[0] ); + }else{ + Trace("datatypes-rewrite-debug") << "Did not rewrite equality " << in << " " << in[0].getKind() << " " << in[1].getKind() << std::endl; + } } return RewriteResponse(REWRITE_DONE, in); @@ -222,7 +227,7 @@ public: static inline void init() {} static inline void shutdown() {} - static bool checkClash( Node n1, Node n2 ) { + static bool checkClash( Node n1, Node n2, std::vector< Node >& rew ) { if( (n1.getKind() == kind::APPLY_CONSTRUCTOR && n2.getKind() == kind::APPLY_CONSTRUCTOR) || (n1.getKind() == kind::TUPLE && n2.getKind() == kind::TUPLE) || (n1.getKind() == kind::RECORD && n2.getKind() == kind::RECORD) ) { @@ -231,21 +236,73 @@ public: } else { Assert( n1.getNumChildren() == n2.getNumChildren() ); for( int i=0; i<(int)n1.getNumChildren(); i++ ) { - if( checkClash( n1[i], n2[i] ) ) { + if( checkClash( n1[i], n2[i], rew ) ) { return true; } } } - }else if( !isTermDatatype( n1 ) ){ - //also check for clashes between non-datatypes - Node eq = NodeManager::currentNM()->mkNode( n1.getType().isBoolean() ? kind::IFF : kind::EQUAL, n1, n2 ); - eq = Rewriter::rewrite( eq ); - if( eq==NodeManager::currentNM()->mkConst(false) ){ + }else if( n1!=n2 ){ + if( n1.isConst() && n2.isConst() ){ + return true; + }else{ + Node eq = NodeManager::currentNM()->mkNode( n1.getType().isBoolean() ? kind::IFF : kind::EQUAL, n1, n2 ); + rew.push_back( eq ); + } + } + return false; + } + /** get instantiate cons */ + static Node getInstCons( Node n, const Datatype& dt, int index, bool mkVar = false ) { + Type tspec; + if( dt.isParametric() ){ + tspec = dt[index].getSpecializedConstructorType(n.getType().toType()); + } + std::vector< Node > children; + children.push_back( Node::fromExpr( dt[index].getConstructor() ) ); + for( int i=0; i<(int)dt[index].getNumArgs(); i++ ){ + Node nc = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[index][i].getSelector() ), n ); + if( mkVar ){ + TypeNode tn = nc.getType(); + if( dt.isParametric() ){ + tn = TypeNode::fromType( tspec )[i]; + } + nc = NodeManager::currentNM()->mkSkolem( "m_$$", tn, "created for inst cons" ); + } + children.push_back( nc ); + } + Node n_ic = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, children ); + //add type ascription for ambiguous constructor types + if(!n_ic.getType().isComparableTo(n.getType())) { + Assert( dt.isParametric() ); + Debug("datatypes-parametric") << "DtInstantiate: ambiguous type for " << n_ic << ", ascribe to " << n.getType() << std::endl; + Debug("datatypes-parametric") << "Constructor is " << dt[index] << std::endl; + Type tspec = dt[index].getSpecializedConstructorType(n.getType().toType()); + Debug("datatypes-parametric") << "Type specification is " << tspec << std::endl; + children[0] = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, + NodeManager::currentNM()->mkConst(AscriptionType(tspec)), children[0] ); + n_ic = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, children ); + Assert( n_ic.getType()==n.getType() ); + } + Assert( isInstCons( n_ic, dt, index ) ); + //n_ic = Rewriter::rewrite( n_ic ); + return n_ic; + } + static bool isInstCons( Node n, const Datatype& dt, int index ){ + if( n.getKind()==kind::APPLY_CONSTRUCTOR ){ + const DatatypeConstructor& c = dt[index]; + if( n.getOperator()==Node::fromExpr( c.getConstructor() ) ){ + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + if( n[i].getKind()!=kind::APPLY_SELECTOR_TOTAL || + n[i].getOperator()!=Node::fromExpr( c[i].getSelector() ) ){ + return false; + } + } return true; } } return false; } + /** is this term a datatype */ static bool isTermDatatype( Node n ){ TypeNode tn = n.getType(); diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index bb6fd4373..b222738ae 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -39,6 +39,7 @@ cardinality TESTER_TYPE \ parameterized APPLY_CONSTRUCTOR APPLY_TYPE_ASCRIPTION 0: "constructor application" parameterized APPLY_SELECTOR SELECTOR_TYPE 1: "selector application" +parameterized APPLY_SELECTOR_TOTAL [SELECTOR_TYPE] 1: "selector application (total)" parameterized APPLY_TESTER TESTER_TYPE 1: "tester application" @@ -82,6 +83,7 @@ constant ASCRIPTION_TYPE \ typerule APPLY_CONSTRUCTOR ::CVC4::theory::datatypes::DatatypeConstructorTypeRule typerule APPLY_SELECTOR ::CVC4::theory::datatypes::DatatypeSelectorTypeRule +typerule APPLY_SELECTOR_TOTAL ::CVC4::theory::datatypes::DatatypeSelectorTypeRule typerule APPLY_TESTER ::CVC4::theory::datatypes::DatatypeTesterTypeRule typerule APPLY_TYPE_ASCRIPTION ::CVC4::theory::datatypes::DatatypeAscriptionTypeRule diff --git a/src/theory/datatypes/options b/src/theory/datatypes/options index 1daa30981..fcf36648d 100644 --- a/src/theory/datatypes/options +++ b/src/theory/datatypes/options @@ -9,8 +9,8 @@ module DATATYPES "theory/datatypes/options.h" Datatypes theory # then we do not rewrite such a selector term to an arbitrary ground term. # For example, by default cvc4 considers cdr( nil ) = nil. If this option is set, then # cdr( nil ) has no set value. -expert-option dtRewriteErrorSel /--disable-dt-rewrite-error-sel bool :default true - disable rewriting incorrectly applied selectors to arbitrary ground term +expert-option dtRewriteErrorSel --dt-rewrite-error-sel bool :default false + rewrite incorrectly applied selectors to arbitrary ground term option dtForceAssignment /--dt-force-assignment bool :default false :read-write force the datatypes solver to give specific values to all datatypes terms before answering sat diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 8396e563e..eef25ca80 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -50,12 +50,15 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, d_labels( c ), d_selector_apps( c ), d_conflict( c, false ), - d_collectTermsCache( c ){ + d_collectTermsCache( c ), + d_consTerms( c ), + d_selTerms( c ){ // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR); - d_equalityEngine.addFunctionKind(kind::APPLY_SELECTOR); + d_equalityEngine.addFunctionKind(kind::APPLY_SELECTOR_TOTAL); d_equalityEngine.addFunctionKind(kind::APPLY_TESTER); + d_equalityEngine.addFunctionKind(kind::APPLY_UF); } TheoryDatatypes::~TheoryDatatypes() { @@ -123,13 +126,19 @@ void TheoryDatatypes::check(Effort e) { if( e == EFFORT_FULL ) { //check for cycles - checkCycles(); - if( d_conflict ){ - return; - } + bool addedFact; + do { + checkCycles(); + addedFact = !d_pending.empty() || !d_pending_merge.empty(); + flushPendingFacts(); + if( d_conflict ){ + return; + } + }while( addedFact ); + //check for splits Debug("datatypes-split") << "Check for splits " << e << endl; - bool addedFact = false; + addedFact = false; do { eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); while( !eqcs_i.isFinished() ){ @@ -141,61 +150,63 @@ void TheoryDatatypes::check(Effort e) { if( eqc->d_constructor.get().isNull() && !hasLabel( eqc, n ) ) { Trace("datatypes-debug") << "No constructor..." << std::endl; const Datatype& dt = ((DatatypeType)(n.getType()).toType()).getDatatype(); - //if only one constructor, then this term must be this constructor - if( dt.getNumConstructors()==1 ){ - Node t = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[0].getTester() ), n ); - d_pending.push_back( t ); - d_pending_exp[ t ] = NodeManager::currentNM()->mkConst( true ); - Trace("datatypes-infer") << "DtInfer : " << t << ", trivial" << std::endl; - d_infer.push_back( t ); - }else{ - std::vector< bool > pcons; - getPossibleCons( eqc, n, pcons ); - //std::cout << "pcons " << n << " = "; - //for( int i=0; i<(int)pcons.size(); i++ ){ //std::cout << pcons[i] << " "; } - //std::cout << std::endl; - //check if we do not need to resolve the constructor type for this equivalence class. - // this is if there are no selectors for this equivalence class, its possible values are infinite, - // and we are not producing a model, then do not split. - int consIndex = -1; - bool needSplit = true; - for( unsigned int j=0; j<pcons.size(); j++ ) { - if( pcons[j] ) { - if( consIndex==-1 ){ - consIndex = j; - } - if( !dt[ j ].isFinite() && !eqc->d_selectors ) { - needSplit = false; - } + + std::vector< bool > pcons; + getPossibleCons( eqc, n, pcons ); + //std::cout << "pcons " << n << " = "; + //for( int i=0; i<(int)pcons.size(); i++ ){ //std::cout << pcons[i] << " "; } + //std::cout << std::endl; + //check if we do not need to resolve the constructor type for this equivalence class. + // this is if there are no selectors for this equivalence class, its possible values are infinite, + // and we are not producing a model, then do not split. + int consIndex = -1; + bool needSplit = true; + for( unsigned int j=0; j<pcons.size(); j++ ) { + if( pcons[j] ) { + if( consIndex==-1 ){ + consIndex = j; } - } - /* - if( !needSplit && mustSpecifyAssignment() ){ - //for the sake of termination, we must choose the constructor of a ground term - //NEED GUARENTEE: groundTerm should not contain any subterms of the same type - // TODO: this is probably not good enough, actually need fair enumeration strategy - Node groundTerm = n.getType().mkGroundTerm(); - int index = Datatype::indexOf( groundTerm.getOperator().toExpr() ); - if( pcons[index] ){ - consIndex = index; + if( !dt[ j ].isFinite() && !eqc->d_selectors ) { + needSplit = false; } - needSplit = true; } - */ - if( needSplit && consIndex!=-1 ) { - Node test = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[consIndex].getTester() ), n ); - Trace("dt-split") << "*************Split for possible constructor " << dt[consIndex] << " for " << n << endl; - test = Rewriter::rewrite( test ); - NodeBuilder<> nb(kind::OR); - nb << test << test.notNode(); - Node lemma = nb; - d_out->lemma( lemma ); - d_out->requirePhase( test, true ); - return; + } + /* + if( !needSplit && mustSpecifyAssignment() ){ + //for the sake of termination, we must choose the constructor of a ground term + //NEED GUARENTEE: groundTerm should not contain any subterms of the same type + // TODO: this is probably not good enough, actually need fair enumeration strategy + Node groundTerm = n.getType().mkGroundTerm(); + int index = Datatype::indexOf( groundTerm.getOperator().toExpr() ); + if( pcons[index] ){ + consIndex = index; + } + needSplit = true; + } + */ + if( needSplit && consIndex!=-1 ) { + //if only one constructor, then this term must be this constructor + if( dt.getNumConstructors()==1 ){ + Node t = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[0].getTester() ), n ); + d_pending.push_back( t ); + d_pending_exp[ t ] = NodeManager::currentNM()->mkConst( true ); + Trace("datatypes-infer") << "DtInfer : 1-cons : " << t << std::endl; + d_infer.push_back( t ); }else{ - Trace("dt-split-debug") << "Do not split constructor for " << n << std::endl; + Node test = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[consIndex].getTester() ), n ); + Trace("dt-split") << "*************Split for possible constructor " << dt[consIndex] << " for " << n << endl; + test = Rewriter::rewrite( test ); + NodeBuilder<> nb(kind::OR); + nb << test << test.notNode(); + Node lemma = nb; + d_out->lemma( lemma ); + d_out->requirePhase( test, true ); + return; } + }else{ + Trace("dt-split-debug") << "Do not split constructor for " << n << " : " << n.getType() << " " << dt.getNumConstructors() << std::endl; } + }else{ Trace("datatypes-debug") << "Has constructor " << eqc->d_constructor.get() << std::endl; } @@ -318,6 +329,51 @@ void TheoryDatatypes::preRegisterTerm(TNode n) { flushPendingFacts(); } +Node TheoryDatatypes::expandDefinition(LogicRequest &logicRequest, Node n) { + switch( n.getKind() ){ + case kind::APPLY_SELECTOR: { + Node selector = n.getOperator(); + Expr selectorExpr = selector.toExpr(); + Node sel = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( selectorExpr ), n[0] ); + if( options::dtRewriteErrorSel() ){ + return sel; + }else{ + size_t selectorIndex = Datatype::cindexOf(selectorExpr); + const Datatype& dt = Datatype::datatypeOf(selectorExpr); + const DatatypeConstructor& c = dt[selectorIndex]; + Expr tester = c.getTester(); + Node tst = NodeManager::currentNM()->mkNode( kind::APPLY_TESTER, Node::fromExpr( tester ), n[0] ); + tst = Rewriter::rewrite( tst ); + Node n_ret; + if( tst==NodeManager::currentNM()->mkConst( true ) ){ + n_ret = sel; + }else{ + if( d_exp_def_skolem.find( selector )==d_exp_def_skolem.end() ){ + std::stringstream ss; + ss << selector << "_uf"; + d_exp_def_skolem[ selector ] = NodeManager::currentNM()->mkSkolem( ss.str().c_str(), + NodeManager::currentNM()->mkFunctionType( n[0].getType(), n.getType() ) ); + } + Node sk = NodeManager::currentNM()->mkNode( kind::APPLY_UF, d_exp_def_skolem[ selector ], n[0] ); + if( tst==NodeManager::currentNM()->mkConst( false ) ){ + n_ret = sk; + }else{ + n_ret = NodeManager::currentNM()->mkNode( kind::ITE, tst, sel, sk ); + } + } + //n_ret = Rewriter::rewrite( n_ret ); + Trace("dt-expand") << "Expand def : " << n << " to " << n_ret << std::endl; + return n_ret; + } + } + break; + default: + return n; + break; + } + Unreachable(); +} + void TheoryDatatypes::presolve() { Debug("datatypes") << "TheoryDatatypes::presolve()" << endl; } @@ -332,7 +388,7 @@ Node TheoryDatatypes::ppRewrite(TNode in) { } TypeNode dtt = NodeManager::currentNM()->getDatatypeForTupleRecord(t); const Datatype& dt = DatatypeType(dtt.toType()).getDatatype(); - return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, Node::fromExpr(dt[0][in.getOperator().getConst<TupleSelect>().getIndex()].getSelector()), in[0]); + return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, Node::fromExpr(dt[0][in.getOperator().getConst<TupleSelect>().getIndex()].getSelector()), in[0]); } else if(in.getKind() == kind::RECORD_SELECT) { TypeNode t = in[0].getType(); if(t.hasAttribute(expr::DatatypeRecordAttr())) { @@ -340,7 +396,7 @@ Node TheoryDatatypes::ppRewrite(TNode in) { } TypeNode dtt = NodeManager::currentNM()->getDatatypeForTupleRecord(t); const Datatype& dt = DatatypeType(dtt.toType()).getDatatype(); - return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, Node::fromExpr(dt[0][in.getOperator().getConst<RecordSelect>().getField()].getSelector()), in[0]); + return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, Node::fromExpr(dt[0][in.getOperator().getConst<RecordSelect>().getField()].getSelector()), in[0]); } TypeNode t = in.getType(); @@ -361,6 +417,19 @@ Node TheoryDatatypes::ppRewrite(TNode in) { NodeManager::currentNM()->getDatatypeForTupleRecord(t).setAttribute(expr::DatatypeRecordAttr(), NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeRecordAttr())); } } + + if( in.getKind()==EQUAL ){ + Node nn; + std::vector< Node > rew; + if( DatatypesRewriter::checkClash(in[0], in[1], rew) ){ + nn = NodeManager::currentNM()->mkConst(false); + }else{ + nn = rew.size()==0 ? NodeManager::currentNM()->mkConst( true ) : + ( rew.size()==1 ? rew[0] : NodeManager::currentNM()->mkNode( kind::AND, rew ) ); + } + return nn; + } + // nothing to do return in; } @@ -404,7 +473,7 @@ Node TheoryDatatypes::ppRewrite(TNode in) { b << in[1]; Debug("tuprec") << "arg " << i << " gets updated to " << in[1] << std::endl; } else { - b << NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, Node::fromExpr(dt[0][i].getSelector()), in[0]); + b << NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, Node::fromExpr(dt[0][i].getSelector()), in[0]); Debug("tuprec") << "arg " << i << " copies " << b[b.getNumChildren() - 1] << std::endl; } } @@ -414,6 +483,7 @@ Node TheoryDatatypes::ppRewrite(TNode in) { Assert(!n.isNull()); + Debug("tuprec") << "REWROTE " << in << " to " << n << std::endl; return n; @@ -452,21 +522,37 @@ bool TheoryDatatypes::propagate(TNode literal){ return ok; } +void TheoryDatatypes::addAssumptions( std::vector<TNode>& assumptions, std::vector<TNode>& tassumptions ) { + for( unsigned i=0; i<tassumptions.size(); i++ ){ + if( std::find( assumptions.begin(), assumptions.end(), tassumptions[i] )==assumptions.end() ){ + assumptions.push_back( tassumptions[i] ); + } + } +} + +void TheoryDatatypes::explainEquality( TNode a, TNode b, bool polarity, std::vector<TNode>& assumptions ) { + if( a!=b ){ + std::vector<TNode> tassumptions; + d_equalityEngine.explainEquality(a, b, polarity, tassumptions); + addAssumptions( assumptions, tassumptions ); + } +} + +void TheoryDatatypes::explainPredicate( TNode p, bool polarity, std::vector<TNode>& assumptions ) { + std::vector<TNode> tassumptions; + d_equalityEngine.explainPredicate(p, polarity, tassumptions); + addAssumptions( assumptions, tassumptions ); +} + /** explain */ void TheoryDatatypes::explain(TNode literal, std::vector<TNode>& assumptions){ Debug("datatypes-explain") << "Explain " << literal << std::endl; bool polarity = literal.getKind() != kind::NOT; TNode atom = polarity ? literal : literal[0]; - std::vector<TNode> tassumptions; if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) { - d_equalityEngine.explainEquality(atom[0], atom[1], polarity, tassumptions); + explainEquality( atom[0], atom[1], polarity, assumptions ); } else { - d_equalityEngine.explainPredicate(atom, polarity, tassumptions); - } - for( unsigned i=0; i<tassumptions.size(); i++ ){ - if( std::find( assumptions.begin(), assumptions.end(), tassumptions[i] )==assumptions.end() ){ - assumptions.push_back( tassumptions[i] ); - } + explainPredicate( atom, polarity, assumptions ); } } @@ -544,7 +630,7 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ Node eq = cons1[i].getType().isBoolean() ? cons1[i].iffNode( cons2[i] ) : cons1[i].eqNode( cons2[i] ); d_pending.push_back( eq ); d_pending_exp[ eq ] = unifEq; - Trace("datatypes-infer") << "DtInfer : " << eq << " by " << unifEq << std::endl; + Trace("datatypes-infer") << "DtInfer : cons-inj : " << eq << " by " << unifEq << std::endl; d_infer.push_back( eq ); d_infer_exp.push_back( unifEq ); } @@ -696,7 +782,7 @@ void TheoryDatatypes::addTester( Node t, EqcInfo* eqc, Node n ){ //conflict because equivalence class contains a constructor std::vector< TNode > assumptions; explain( t, assumptions ); - explain( eqc->d_constructor.get().eqNode( tt[0] ), assumptions ); + explainEquality( eqc->d_constructor.get(), tt[0], true, assumptions ); d_conflictNode = mkAnd( assumptions ); Trace("dt-conflict") << "CONFLICT: Tester eq conflict : " << d_conflictNode << std::endl; d_out->conflict( d_conflictNode ); @@ -767,7 +853,7 @@ void TheoryDatatypes::addTester( Node t, EqcInfo* eqc, Node n ){ Node t_concl_exp = ( nb.getNumChildren() == 1 ) ? nb.getChild( 0 ) : nb; d_pending.push_back( t_concl ); d_pending_exp[ t_concl ] = t_concl_exp; - Trace("datatypes-infer") << "DtInfer : " << t_concl << " by " << t_concl_exp << std::endl; + Trace("datatypes-infer") << "DtInfer : label : " << t_concl << " by " << t_concl_exp << std::endl; d_infer.push_back( t_concl ); d_infer_exp.push_back( t_concl_exp ); return; @@ -781,7 +867,7 @@ void TheoryDatatypes::addTester( Node t, EqcInfo* eqc, Node n ){ std::vector< TNode > assumptions; explain( j, assumptions ); explain( t, assumptions ); - explain( jt[0].eqNode( tt[0] ), assumptions ); + explainEquality( jt[0], tt[0], true, assumptions ); d_conflictNode = mkAnd( assumptions ); Trace("dt-conflict") << "CONFLICT: Tester conflict : " << d_conflictNode << std::endl; d_out->conflict( d_conflictNode ); @@ -825,7 +911,7 @@ void TheoryDatatypes::addConstructor( Node c, EqcInfo* eqc, Node n ){ Node n = *i; std::vector< TNode > assumptions; explain( *i, assumptions ); - explain( c.eqNode( (*i)[0][0] ), assumptions ); + explainEquality( c, (*i)[0][0], true, assumptions ); d_conflictNode = mkAnd( assumptions ); Trace("dt-conflict") << "CONFLICT: Tester merge eq conflict : " << d_conflictNode << std::endl; d_out->conflict( d_conflictNode ); @@ -848,7 +934,7 @@ void TheoryDatatypes::addConstructor( Node c, EqcInfo* eqc, Node n ){ } void TheoryDatatypes::collapseSelector( Node s, Node c ) { - Node r = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR, s.getOperator(), c ); + Node r = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, s.getOperator(), c ); Node rr = Rewriter::rewrite( r ); //if( r!=rr ){ //Node eq_exp = NodeManager::currentNM()->mkConst(true); @@ -860,7 +946,7 @@ void TheoryDatatypes::collapseSelector( Node s, Node c ) { d_pending.push_back( eq ); d_pending_exp[ eq ] = eq_exp; - Trace("datatypes-infer") << "DtInfer : " << eq << " by " << eq_exp << " (collapse selector)" << std::endl; + Trace("datatypes-infer") << "DtInfer : collapse sel : " << eq << " by " << eq_exp << std::endl; d_infer.push_back( eq ); d_infer_exp.push_back( eq_exp ); } @@ -881,7 +967,49 @@ EqualityStatus TheoryDatatypes::getEqualityStatus(TNode a, TNode b){ } void TheoryDatatypes::computeCareGraph(){ - Theory::computeCareGraph(); + Trace("dt-cg") << "Compute graph for dt..." << std::endl; + vector< pair<TNode, TNode> > currentPairs; + for( unsigned r=0; r<2; r++ ){ + unsigned functionTerms = r==0 ? d_consTerms.size() : d_selTerms.size(); + for( unsigned i=0; i<functionTerms; i++ ){ + TNode f1 = r==0 ? d_consTerms[i] : d_selTerms[i]; + for( unsigned j=i+1; j<functionTerms; j++ ){ + TNode f2 = r==0 ? d_consTerms[j] : d_selTerms[j]; + if( f1.getOperator()==f2.getOperator() && !areEqual( f1, f2 ) ){ + Trace("dt-cg") << "Check " << f1 << " and " << f2 << std::endl; + bool somePairIsDisequal = false; + currentPairs.clear(); + for (unsigned k = 0; k < f1.getNumChildren(); ++ k) { + TNode x = f1[k]; + TNode y = f2[k]; + if( areDisequal(x, y) ){ + somePairIsDisequal = true; + break; + }else if( !areEqual( x, y ) ){ + Trace("dt-cg") << "Arg #" << k << " is " << x << " " << y << std::endl; + //check if they are definately disequal + + if( d_equalityEngine.isTriggerTerm(x, THEORY_UF) && d_equalityEngine.isTriggerTerm(y, THEORY_UF) ){ + TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_DATATYPES); + TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_DATATYPES); + Trace("dt-cg") << "Arg #" << k << " shared term is " << x_shared << " " << y_shared << std::endl; + //EqualityStatus eqStatus = d_valuation.getEqualityStatus(x_shared, y_shared); + //if( eqStatus!=EQUALITY_UNKNOWN ){ + currentPairs.push_back(make_pair(x_shared, y_shared)); + } + } + } + if (!somePairIsDisequal) { + for (unsigned c = 0; c < currentPairs.size(); ++ c) { + Trace("dt-cg-pair") << "Pair : " << currentPairs[c].first << " " << currentPairs[c].second << std::endl; + addCarePair(currentPairs[c].first, currentPairs[c].second); + } + } + } + } + } + } + Trace("dt-cg") << "Done Compute graph for dt." << std::endl; } void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ @@ -889,14 +1017,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 +1066,14 @@ 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 orig_size = nodes.size(); unsigned index = 0; while( index<nodes.size() ){ Node eqc = nodes[index]; @@ -942,21 +1090,24 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ neqc = *te; Trace("dt-cmi-debug") << "Try " << neqc << " ... " << std::endl; ++te; - for( unsigned i=0; i<cons.size(); i++ ){ - //check if it is modulo equality the same - if( cons[i].getOperator()==neqc.getOperator() ){ - bool diff = false; - for( unsigned j=0; j<cons[i].getNumChildren(); j++ ){ - if( !m->areEqual( cons[i][j], neqc[j] ) ){ - diff = true; + //if it is infinite or we are assigning to terms known by datatypes, make sure it is fresh + if( eqc.getType().getCardinality().isInfinite() || index<orig_size ){ + for( unsigned i=0; i<cons.size(); i++ ){ + //check if it is modulo equality the same + if( cons[i].getOperator()==neqc.getOperator() ){ + bool diff = false; + for( unsigned j=0; j<cons[i].getNumChildren(); j++ ){ + if( !m->areEqual( cons[i][j], neqc[j] ) ){ + diff = true; + break; + } + } + if( !diff ){ + Trace("dt-cmi-debug") << "...Already equivalent modulo equality to " << cons[i] << std::endl; + success = false; break; } } - if( !diff ){ - Trace("dt-cmi-debug") << "...Already equivalent modulo equality to " << cons[i] << std::endl; - success = false; - break; - } } } }while( !success ); @@ -972,51 +1123,31 @@ 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() ){ for( unsigned i=0; i<pcons.size(); i++ ){ + //must try the infinite ones first 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 +1161,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; @@ -1045,6 +1194,7 @@ void TheoryDatatypes::collectTerms( Node n ) { collectTerms( n[i] ); } if( n.getKind() == APPLY_CONSTRUCTOR ){ + d_consTerms.push_back( n ); /* //we must take into account subterm relation when checking for cycles for( int i=0; i<(int)n.getNumChildren(); i++ ) { @@ -1059,7 +1209,8 @@ void TheoryDatatypes::collectTerms( Node n ) { //eqc->d_selectors = true; } */ - }else if( n.getKind() == APPLY_SELECTOR ){ + }else if( n.getKind() == APPLY_SELECTOR_TOTAL ){ + d_selTerms.push_back( n ); //we must also record which selectors exist Debug("datatypes") << " Found selector " << n << endl; if (n.getType().isBoolean()) { @@ -1084,57 +1235,29 @@ void TheoryDatatypes::processNewTerm( Node n ){ Node eq = n.getType().isBoolean() ? rn.iffNode( n ) : rn.eqNode( n ); d_pending.push_back( eq ); d_pending_exp[ eq ] = NodeManager::currentNM()->mkConst( true ); - Trace("datatypes-infer") << "DtInfer : " << eq << ", trivial" << std::endl; + Trace("datatypes-infer") << "DtInfer : rewrite : " << eq << std::endl; d_infer.push_back( eq ); } } Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index, bool mkVar, bool isActive ){ - //if( !d_inst_map[n][index].isNull() ){ - // return d_inst_map[n][index]; - //}else{ + std::map< int, Node >::iterator it = d_inst_map[n].find( index ); + if( it!=d_inst_map[n].end() ){ + return it->second; + }else{ //add constructor to equivalence class - Type tspec; - if( dt.isParametric() ){ - tspec = dt[index].getSpecializedConstructorType(n.getType().toType()); - } - std::vector< Node > children; - children.push_back( Node::fromExpr( dt[index].getConstructor() ) ); - for( int i=0; i<(int)dt[index].getNumArgs(); i++ ){ - Node nc = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, Node::fromExpr( dt[index][i].getSelector() ), n ); - if( mkVar ){ - TypeNode tn = nc.getType(); - if( dt.isParametric() ){ - tn = TypeNode::fromType( tspec )[i]; - } - nc = NodeManager::currentNM()->mkSkolem( "m", tn, "created during model gen" ); - } - children.push_back( nc ); - if( isActive ){ - processNewTerm( nc ); - } - } - Node n_ic = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children ); + Node n_ic = DatatypesRewriter::getInstCons( n, dt, index, mkVar ); if( isActive ){ + for( unsigned i = 0; i<n_ic.getNumChildren(); i++ ){ + processNewTerm( n_ic[i] ); + } collectTerms( n_ic ); } - //add type ascription for ambiguous constructor types - if(!n_ic.getType().isComparableTo(n.getType())) { - Assert( dt.isParametric() ); - Debug("datatypes-parametric") << "DtInstantiate: ambiguous type for " << n_ic << ", ascribe to " << n.getType() << std::endl; - Debug("datatypes-parametric") << "Constructor is " << dt[index] << std::endl; - Type tspec = dt[index].getSpecializedConstructorType(n.getType().toType()); - Debug("datatypes-parametric") << "Type specification is " << tspec << std::endl; - children[0] = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, - NodeManager::currentNM()->mkConst(AscriptionType(tspec)), children[0] ); - n_ic = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children ); - Assert( n_ic.getType()==n.getType() ); - } n_ic = Rewriter::rewrite( n_ic ); Debug("dt-enum") << "Made instantiate cons " << n_ic << std::endl; - //d_inst_map[n][index] = n_ic; + d_inst_map[n][index] = n_ic; return n_ic; - //} + } } void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){ @@ -1155,14 +1278,14 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){ //if( eqc->d_selectors || dt[ index ].isFinite() ){ // || mustSpecifyAssignment() //instantiate this equivalence class eqc->d_inst = true; - Node tt_cons = getInstantiateCons( tt, dt, index ); + Node tt_cons = getInstantiateCons( tt, dt, index, false, true ); Node eq; if( tt!=tt_cons ){ eq = tt.eqNode( tt_cons ); Debug("datatypes-inst") << "DtInstantiate : " << eqc << " " << eq << std::endl; d_pending.push_back( eq ); d_pending_exp[ eq ] = exp; - Trace("datatypes-infer") << "DtInfer : " << eq << " by " << exp << std::endl; + Trace("datatypes-infer") << "DtInfer : instantiate : " << eq << " by " << exp << std::endl; //eqc->d_inst.set( eq ); d_infer.push_back( eq ); d_infer_exp.push_back( exp ); @@ -1176,33 +1299,201 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){ void TheoryDatatypes::checkCycles() { Debug("datatypes-cycle-check") << "Check cycles" << std::endl; + std::vector< Node > cod_eqc; eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); while( !eqcs_i.isFinished() ){ Node eqc = (*eqcs_i); if( DatatypesRewriter::isTermDatatype( eqc ) ) { - map< Node, bool > visited; - std::vector< TNode > expl; - Node cn = searchForCycle( eqc, eqc, visited, expl ); - //if we discovered a different cycle while searching this one - if( !cn.isNull() && cn!=eqc ){ - visited.clear(); - expl.clear(); - Node prev = cn; - cn = searchForCycle( cn, cn, visited, expl ); - Assert( prev==cn ); - } + const Datatype& dt = ((DatatypeType)(eqc.getType()).toType()).getDatatype(); + if( !dt.isCodatatype() ){ + //do cycle checks + map< Node, bool > visited; + std::vector< TNode > expl; + Node cn = searchForCycle( eqc, eqc, visited, expl ); + //if we discovered a different cycle while searching this one + if( !cn.isNull() && cn!=eqc ){ + visited.clear(); + expl.clear(); + Node prev = cn; + cn = searchForCycle( cn, cn, visited, expl ); + Assert( prev==cn ); + } - if( !cn.isNull() ) { - Assert( expl.size()>0 ); - d_conflictNode = mkAnd( expl ); - Trace("dt-conflict") << "CONFLICT: Cycle conflict : " << d_conflictNode << std::endl; - d_out->conflict( d_conflictNode ); - d_conflict = true; - return; + if( !cn.isNull() ) { + Assert( expl.size()>0 ); + d_conflictNode = mkAnd( expl ); + Trace("dt-conflict") << "CONFLICT: Cycle conflict : " << d_conflictNode << std::endl; + d_out->conflict( d_conflictNode ); + d_conflict = true; + return; + } + }else{ + //indexing + cod_eqc.push_back( eqc ); } } ++eqcs_i; } + //process codatatypes + if( cod_eqc.size()>1 ){ + std::vector< std::vector< Node > > part_out; + std::vector< TNode > exp; + std::map< Node, Node > cn; + std::map< Node, std::map< Node, int > > dni; + for( unsigned i=0; i<cod_eqc.size(); i++ ){ + cn[cod_eqc[i]] = cod_eqc[i]; + } + separateBisimilar( cod_eqc, part_out, exp, cn, dni, 0, false ); + if( !part_out.empty() ){ + for( unsigned i=0; i<part_out.size(); i++ ){ + std::vector< Node > part; + part.push_back( part_out[i][0] ); + for( unsigned j=1; j<part_out[i].size(); j++ ){ + Trace("dt-cod") << "Codatatypes : " << part_out[i][0] << " and " << part_out[i][j] << " must be equal!!" << std::endl; + part.push_back( part_out[i][j] ); + std::vector< std::vector< Node > > tpart_out; + exp.clear(); + cn.clear(); + cn[part_out[i][0]] = part_out[i][0]; + cn[part_out[i][j]] = part_out[i][j]; + dni.clear(); + separateBisimilar( part, tpart_out, exp, cn, dni, 0, true ); + Assert( tpart_out.size()==1 && tpart_out[0].size()==2 ); + part.pop_back(); + //merge based on explanation + Trace("dt-cod") << " exp is : "; + for( unsigned k=0; k<exp.size(); k++ ){ + Trace("dt-cod") << exp[k] << " "; + } + Trace("dt-cod") << std::endl; + Node eq = part_out[i][0].eqNode( part_out[i][j] ); + Node eqExp = mkAnd( exp ); + d_pending.push_back( eq ); + d_pending_exp[ eq ] = eqExp; + Trace("datatypes-infer") << "DtInfer : cod-bisimilar : " << eq << " by " << eqExp << std::endl; + d_infer.push_back( eq ); + d_infer_exp.push_back( eqExp ); + } + } + } + } +} + +//everything is in terms of representatives +void TheoryDatatypes::separateBisimilar( std::vector< Node >& part, std::vector< std::vector< Node > >& part_out, + std::vector< TNode >& exp, + std::map< Node, Node >& cn, + std::map< Node, std::map< Node, int > >& dni, int dniLvl, bool mkExp ){ + if( !mkExp ){ + Trace("dt-cod-debug") << "Separate bisimilar : " << std::endl; + for( unsigned i=0; i<part.size(); i++ ){ + Trace("dt-cod-debug") << " " << part[i] << ", current = " << cn[part[i]] << std::endl; + } + } + Assert( part.size()>1 ); + std::map< Node, std::vector< Node > > new_part; + std::map< Node, std::vector< Node > > new_part_c; + std::map< int, std::vector< Node > > new_part_rec; + + std::map< Node, Node > cn_cons; + for( unsigned j=0; j<part.size(); j++ ){ + Node c = cn[part[j]]; + std::map< Node, int >::iterator it_rec = dni[part[j]].find( c ); + if( it_rec!=dni[part[j]].end() ){ + //looped + if( !mkExp ){ Trace("dt-cod-debug") << " - " << part[j] << " is looping at index " << it_rec->second << std::endl; } + new_part_rec[ it_rec->second ].push_back( part[j] ); + }else{ + if( DatatypesRewriter::isTermDatatype( c ) ){ + bool foundCons = false; + EqcInfo* eqc = getOrMakeEqcInfo( c, false ); + if( eqc ){ + Node ncons = eqc->d_constructor.get(); + if( !ncons.isNull() ) { + foundCons = true; + Node cc = ncons.getOperator(); + cn_cons[part[j]] = ncons; + if( mkExp ){ + explainEquality( c, ncons, true, exp ); + } + new_part[cc].push_back( part[j] ); + if( !mkExp ){ Trace("dt-cod-debug") << " - " << part[j] << " is datatype " << ncons << "." << std::endl; } + } + } + if( !foundCons ){ + new_part_c[c].push_back( part[j] ); + if( !mkExp ){ Trace("dt-cod-debug") << " - " << part[j] << " is unspecified datatype." << std::endl; } + } + }else{ + //add equivalences + if( !mkExp ){ Trace("dt-cod-debug") << " - " << part[j] << " is term " << c << "." << std::endl; } + new_part_c[c].push_back( part[j] ); + } + } + } + //direct add for constants + for( std::map< Node, std::vector< Node > >::iterator it = new_part_c.begin(); it != new_part_c.end(); ++it ){ + if( it->second.size()>1 ){ + std::vector< Node > vec; + vec.insert( vec.begin(), it->second.begin(), it->second.end() ); + part_out.push_back( vec ); + } + } + //direct add for recursive + for( std::map< int, std::vector< Node > >::iterator it = new_part_rec.begin(); it != new_part_rec.end(); ++it ){ + if( it->second.size()>1 ){ + std::vector< Node > vec; + vec.insert( vec.begin(), it->second.begin(), it->second.end() ); + part_out.push_back( vec ); + }else{ + //add back : could match a datatype? + } + } + //recurse for the datatypes + for( std::map< Node, std::vector< Node > >::iterator it = new_part.begin(); it != new_part.end(); ++it ){ + if( it->second.size()>1 ){ + //set dni to check for loops + std::map< Node, Node > dni_rem; + for( unsigned i=0; i<it->second.size(); i++ ){ + Node n = it->second[i]; + dni[n][cn[n]] = dniLvl; + dni_rem[n] = cn[n]; + } + + //we will split based on the arguments of the datatype + std::vector< std::vector< Node > > split_new_part; + split_new_part.push_back( it->second ); + + unsigned nChildren = cn_cons[it->second[0]].getNumChildren(); + //for each child of constructor + unsigned cindex = 0; + while( cindex<nChildren && !split_new_part.empty() ){ + if( !mkExp ){ Trace("dt-cod-debug") << "Split argument #" << cindex << " of " << it->first << "..." << std::endl; } + std::vector< std::vector< Node > > next_split_new_part; + for( unsigned j=0; j<split_new_part.size(); j++ ){ + //set current node + for( unsigned k=0; k<split_new_part[j].size(); k++ ){ + Node n = split_new_part[j][k]; + cn[n] = getRepresentative( cn_cons[n][cindex] ); + if( mkExp ){ + explainEquality( cn[n], cn_cons[n][cindex], true, exp ); + } + } + std::vector< std::vector< Node > > c_part_out; + separateBisimilar( split_new_part[j], c_part_out, exp, cn, dni, dniLvl+1, mkExp ); + next_split_new_part.insert( next_split_new_part.end(), c_part_out.begin(), c_part_out.end() ); + } + split_new_part.clear(); + split_new_part.insert( split_new_part.end(), next_split_new_part.begin(), next_split_new_part.end() ); + cindex++; + } + part_out.insert( part_out.end(), split_new_part.begin(), split_new_part.end() ); + + for( std::map< Node, Node >::iterator it2 = dni_rem.begin(); it2 != dni_rem.end(); ++it2 ){ + dni[it2->first].erase( it2->second ); + } + } + } } //postcondition: if cycle detected, explanation is why n is a subterm of on @@ -1215,8 +1506,7 @@ Node TheoryDatatypes::searchForCycle( Node n, Node on, if( !firstTime ){ nn = getRepresentative( n ); if( nn==on ){ - Node lit = NodeManager::currentNM()->mkNode( EQUAL, n, nn ); - explain( lit, explanation ); + explainEquality( n, nn, true, explanation ); return on; } }else{ @@ -1236,8 +1526,7 @@ Node TheoryDatatypes::searchForCycle( Node n, Node on, //} //add explanation for why the constructor is connected if( n != ncons ) { - Node lit = NodeManager::currentNM()->mkNode( EQUAL, n, ncons ); - explain( lit, explanation ); + explainEquality( n, ncons, true, explanation ); } return on; }else if( !cn.isNull() ){ @@ -1249,7 +1538,13 @@ Node TheoryDatatypes::searchForCycle( Node n, Node on, visited.erase( nn ); return Node::null(); }else{ - return nn; + if( DatatypesRewriter::isTermDatatype( nn ) ) { + const Datatype& dt = ((DatatypeType)(nn.getType()).toType()).getDatatype(); + if( !dt.isCodatatype() ){ + return nn; + } + } + return Node::null(); } } @@ -1303,11 +1598,11 @@ bool TheoryDatatypes::mustCommunicateFact( Node n, Node exp ){ return false; } -bool TheoryDatatypes::hasTerm( Node a ){ +bool TheoryDatatypes::hasTerm( TNode a ){ return d_equalityEngine.hasTerm( a ); } -bool TheoryDatatypes::areEqual( Node a, Node b ){ +bool TheoryDatatypes::areEqual( TNode a, TNode b ){ if( a==b ){ return true; }else if( hasTerm( a ) && hasTerm( b ) ){ @@ -1317,7 +1612,7 @@ bool TheoryDatatypes::areEqual( Node a, Node b ){ } } -bool TheoryDatatypes::areDisequal( Node a, Node b ){ +bool TheoryDatatypes::areDisequal( TNode a, TNode b ){ if( a==b ){ return false; }else if( hasTerm( a ) && hasTerm( b ) ){ @@ -1327,7 +1622,7 @@ bool TheoryDatatypes::areDisequal( Node a, Node b ){ } } -Node TheoryDatatypes::getRepresentative( Node a ){ +Node TheoryDatatypes::getRepresentative( TNode a ){ if( hasTerm( a ) ){ return d_equalityEngine.getRepresentative( a ); }else{ diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 3a29433f8..eb86c3f76 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -166,6 +166,12 @@ private: std::vector< Node > d_pending; std::map< Node, Node > d_pending_exp; std::vector< Node > d_pending_merge; + /** expand definition skolem functions */ + std::map< Node, Node > d_exp_def_skolem; + /** All the constructor terms that the theory has seen */ + context::CDList<TNode> d_consTerms; + /** All the selector terms that the theory has seen */ + context::CDList<TNode> d_selTerms; private: /** assert fact */ void assertFact( Node fact, Node exp ); @@ -193,6 +199,9 @@ public: /** propagate */ bool propagate(TNode literal); /** explain */ + void addAssumptions( std::vector<TNode>& assumptions, std::vector<TNode>& tassumptions ); + void explainEquality( TNode a, TNode b, bool polarity, std::vector<TNode>& assumptions ); + void explainPredicate( TNode p, bool polarity, std::vector<TNode>& assumptions ); void explain( TNode literal, std::vector<TNode>& assumptions ); Node explain( TNode literal ); /** Conflict when merging two constants */ @@ -208,6 +217,7 @@ public: void check(Effort e); void preRegisterTerm(TNode n); + Node expandDefinition(LogicRequest &logicRequest, Node n); Node ppRewrite(TNode n); void presolve(); void addSharedTerm(TNode t); @@ -233,10 +243,15 @@ private: Node searchForCycle( Node n, Node on, std::map< Node, bool >& visited, std::vector< TNode >& explanation, bool firstTime = true ); + /** for checking whether two codatatype terms must be equal */ + void separateBisimilar( std::vector< Node >& part, std::vector< std::vector< Node > >& part_out, + std::vector< TNode >& exp, + std::map< Node, Node >& cn, + std::map< Node, std::map< Node, int > >& dni, int dniLvl, bool mkExp ); /** collect terms */ void collectTerms( Node n ); /** get instantiate cons */ - Node getInstantiateCons( Node n, const Datatype& dt, int index, bool mkVar = false, bool isActive = true ); + Node getInstantiateCons( Node n, const Datatype& dt, int index, bool mkVar, bool isActive ); /** process new term that was created internally */ void processNewTerm( Node n ); /** check instantiate */ @@ -250,10 +265,10 @@ private: bool mustCommunicateFact( Node n, Node exp ); private: //equality queries - bool hasTerm( Node a ); - bool areEqual( Node a, Node b ); - bool areDisequal( Node a, Node b ); - Node getRepresentative( Node a ); + bool hasTerm( TNode a ); + bool areEqual( TNode a, TNode b ); + bool areDisequal( TNode a, TNode b ); + Node getRepresentative( TNode a ); public: /** get equality engine */ eq::EqualityEngine* getEqualityEngine() { return &d_equalityEngine; } diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index 527d110e0..d08b511dd 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -98,7 +98,7 @@ struct DatatypeConstructorTypeRule { struct DatatypeSelectorTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw(TypeCheckingExceptionPrivate) { - Assert(n.getKind() == kind::APPLY_SELECTOR); + Assert(n.getKind() == kind::APPLY_SELECTOR || n.getKind() == kind::APPLY_SELECTOR_TOTAL ); TypeNode selType = n.getOperator().getType(check); Type t = selType[0].toType(); Assert( t.isDatatype() ); 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 d815e0ee8..098a7819a 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -648,7 +648,18 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) { Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, vars); Node curr; for( int i=(d_models[op]->d_cond.size()-1); i>=0; i--) { - Node v = getRepresentative( d_models[op]->d_value[i] ); + Node v = d_models[op]->d_value[i]; + if( !hasTerm( v ) ){ + //can happen when the model basis term does not exist in ground assignment + TypeNode tn = v.getType(); + if( d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() && !d_rep_set.d_type_reps[ tn ].empty() ){ + //see full_model_check.cpp line 366 + v = d_rep_set.d_type_reps[tn][ d_rep_set.d_type_reps[tn].size()-1 ]; + }else{ + Assert( false ); + } + } + v = getRepresentative( v ); if( curr.isNull() ){ curr = v; }else{ @@ -656,6 +667,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 +675,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 eqc 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 +686,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/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 3b6c8e492..0f3e53827 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -937,7 +937,7 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n void FullModelChecker::doNegate( Def & dc ) { for (unsigned i=0; i<dc.d_cond.size(); i++) { if (!dc.d_value[i].isNull()) { - dc.d_value[i] = dc.d_value[i]==d_true ? d_false : d_true; + dc.d_value[i] = dc.d_value[i]==d_true ? d_false : ( dc.d_value[i]==d_false ? d_true : dc.d_value[i] ); } } } 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..e733764f0 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -67,11 +67,13 @@ option registerQuantBodyTerms --register-quant-body-terms bool :default false option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToInstWhenMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkInstWhenMode :predicate-include "theory/quantifiers/options_handlers.h" when to apply instantiation +option instMaxLevel --inst-max-level=N int :default -1 + maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default) 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 +97,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 @@ -112,7 +114,7 @@ option fmfFreshDistConst --fmf-fresh-dc bool :default false use fresh distinguished representative when applying Inst-Gen techniques option fmfFmcSimple /--disable-fmf-fmc-simple bool :default true disable simple models in full model check for finite model finding -option fmfBoundInt --fmf-bound-int bool :default false :read-write +option fmfBoundInt fmf-bound-int --fmf-bound-int bool :default false :read-write finite model finding on bounded integer quantification option axiomInstMode --axiom-inst=MODE CVC4::theory::quantifiers::AxiomInstMode :default CVC4::theory::quantifiers::AXIOM_INST_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToAxiomInstMode :handler-include "theory/quantifiers/options_handlers.h" diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index e9c754d4a..b7e624a66 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\ ++ Use model-based quantifier instantiation algorithm from CADE 24 finite\n\ + model finding paper based on generalizing evaluations.\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\ @@ -131,9 +131,6 @@ conflict \n\ partial \n\ + Apply QCF algorithm to instantiate heuristically as well. \n\ \n\ -partial \n\ -+ Apply QCF to instantiate heuristically as well. \n\ -\n\ mc \n\ + Apply QCF algorithm in a complete way, so that a model is ensured when it fails. \n\ \n\ @@ -217,21 +214,21 @@ 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; - } else if(optarg == "none") { + if(optarg == "gen-ev") { + return MBQI_GEN_EVAL; + } else if(optarg == "none") { return MBQI_NONE; - } else if(optarg == "instgen") { + } 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") { + } else if(optarg == "fmc-interval") { return MBQI_FMC_INTERVAL; - } else if(optarg == "interval") { + } else if(optarg == "interval") { return MBQI_INTERVAL; - } else if(optarg == "trust") { + } else if(optarg == "trust") { return MBQI_TRUST; - } else if(optarg == "help") { + } else if(optarg == "help") { puts(mbqiModeHelp.c_str()); exit(1); } else { diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index c0b318f23..e27d438be 100755 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -1488,7 +1488,7 @@ bool MatchGen::isHandledBoolConnective( TNode n ) { bool MatchGen::isHandledUfTerm( TNode n ) {
return n.getKind()==APPLY_UF || n.getKind()==STORE || n.getKind()==SELECT ||
- n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR || n.getKind()==APPLY_TESTER;// || n.getKind()==GEQ;
+ n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR_TOTAL || n.getKind()==APPLY_TESTER;
}
Node MatchGen::getOperator( QuantConflictFind * p, Node n ) {
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index cf183dd18..3168d21a0 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/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 6912c9e89..3de12b9c9 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -324,7 +324,7 @@ bool Trigger::isUsableTrigger( Node n, Node f ){ bool Trigger::isAtomicTrigger( Node n ){ return ( n.getKind()==APPLY_UF && !n.getOperator().getAttribute(NoMatchAttribute()) ) || n.getKind()==SELECT || n.getKind()==STORE || - n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR || n.getKind()==APPLY_TESTER; + n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR_TOTAL || n.getKind()==APPLY_TESTER; } bool Trigger::isSimpleTrigger( Node n ){ if( isAtomicTrigger( n ) ){ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index eaf5e8228..63697f5e7 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -319,7 +319,6 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std Trace("inst") << " " << terms[i]; Trace("inst") << std::endl; } - //uint64_t maxInstLevel = 0; if( options::cbqi() ){ for( int i=0; i<(int)terms.size(); i++ ){ if( quantifiers::TermDb::hasInstConstAttr(terms[i]) ){ @@ -328,22 +327,21 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std Debug("inst") << " " << terms[i] << std::endl; } Unreachable("Bad instantiation"); - }else{ - Trace("inst") << " " << terms[i]; - //Debug("inst-engine") << " " << terms[i].getAttribute(InstLevelAttribute()); - Trace("inst") << std::endl; - //if( terms[i].hasAttribute(InstLevelAttribute()) ){ - //if( terms[i].getAttribute(InstLevelAttribute())>maxInstLevel ){ - // maxInstLevel = terms[i].getAttribute(InstLevelAttribute()); - //} - //}else{ - //setInstantiationLevelAttr( terms[i], 0 ); - //} } } } + if( options::instMaxLevel()!=-1 ){ + uint64_t maxInstLevel = 0; + for( int i=0; i<(int)terms.size(); i++ ){ + if( terms[i].hasAttribute(InstLevelAttribute()) ){ + if( terms[i].getAttribute(InstLevelAttribute())>maxInstLevel ){ + maxInstLevel = terms[i].getAttribute(InstLevelAttribute()); + } + } + } + setInstantiationLevelAttr( body, maxInstLevel+1 ); + } Trace("inst-debug") << "*** Lemma is " << lem << std::endl; - //setInstantiationLevelAttr( body, maxInstLevel+1 ); ++(d_statistics.d_instantiations); return true; }else{ @@ -504,6 +502,17 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bo } Trace("inst-add-debug") << std::endl; + if( options::instMaxLevel()!=-1 ){ + for( unsigned i=0; i<terms.size(); i++ ){ + if( terms[i].hasAttribute(InstLevelAttribute()) && + (int)terms[i].getAttribute(InstLevelAttribute())>options::instMaxLevel() ){ + Trace("inst-add-debug") << "Term " << terms[i] << " has instantiation level " << terms[i].getAttribute(InstLevelAttribute()); + Trace("inst-add-debug") << ", which is more than maximum allowed level " << options::instMaxLevel() << std::endl; + return false; + } + } + } + //check for duplication ///* bool alreadyExists = false; diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index 8c07b679d..16bb7e694 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -41,10 +41,6 @@ RegExpOpr::RegExpOpr() { d_emptySingleton = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, d_emptyString );
std::vector< Node > nvec;
d_emptyRegexp = NodeManager::currentNM()->mkNode( kind::REGEXP_EMPTY, nvec );
- // All Charactors = all printable ones 32-126
- //d_char_start = 'a';//' ';
- //d_char_end = 'c';//'~';
- //d_sigma = mkAllExceptOne( '\0' );
d_sigma = NodeManager::currentNM()->mkNode( kind::REGEXP_SIGMA, nvec );
d_sigma_star = NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, d_sigma );
d_card = 256;
@@ -896,15 +892,13 @@ void RegExpOpr::simplifyNRegExp( Node s, Node r, std::vector< Node > &new_nodes }
case kind::REGEXP_CONCAT: {
//TODO: rewrite empty
+ Node lens = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s);
Node b1 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1);
Node g1 = NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode(kind::GEQ, b1, d_zero),
NodeManager::currentNM()->mkNode( kind::GEQ, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s), b1 ) );
- Node s1 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());
- Node s2 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());
- Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, s1, s2);
- Node s12 = s.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s1, s2));
- Node s1len = b1.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s1));
+ Node s1 = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, s, d_zero, b1));
+ Node s2 = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, s, b1, NodeManager::currentNM()->mkNode(kind::MINUS, lens, b1)));
Node s1r1 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s1, r[0]).negate();
if(r[0].getKind() == kind::STRING_TO_REGEXP) {
s1r1 = s1.eqNode(r[0][0]).negate();
@@ -928,8 +922,6 @@ void RegExpOpr::simplifyNRegExp( Node s, Node r, std::vector< Node > &new_nodes }
conc = NodeManager::currentNM()->mkNode(kind::OR, s1r1, s2r2);
- conc = NodeManager::currentNM()->mkNode(kind::AND, s12, s1len, conc);
- conc = NodeManager::currentNM()->mkNode(kind::EXISTS, b2v, conc);
conc = NodeManager::currentNM()->mkNode(kind::IMPLIES, g1, conc);
conc = NodeManager::currentNM()->mkNode(kind::FORALL, b1v, conc);
break;
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index ac5a97167..d44f38bc3 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -65,7 +65,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu d_curr_cardinality(c, 0) { // The kinds we are treating as function application in congruence - //d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP); + d_equalityEngine.addFunctionKind(kind::STRING_IN_REGEXP); d_equalityEngine.addFunctionKind(kind::STRING_LENGTH); d_equalityEngine.addFunctionKind(kind::STRING_CONCAT); d_equalityEngine.addFunctionKind(kind::STRING_STRCTN); @@ -418,7 +418,7 @@ void TheoryStrings::preRegisterTerm(TNode n) { break; case kind::STRING_IN_REGEXP: //do not add trigger here - //d_equalityEngine.addTriggerPredicate(n); + d_equalityEngine.addTriggerPredicate(n); break; case kind::STRING_SUBSTR_TOTAL: { Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ, @@ -560,7 +560,7 @@ void TheoryStrings::check(Effort e) { //must record string in regular expressions if ( atom.getKind() == kind::STRING_IN_REGEXP ) { addMembership(assertion); - //d_equalityEngine.assertPredicate(atom, polarity, fact); + d_equalityEngine.assertPredicate(atom, polarity, fact); } else if (atom.getKind() == kind::STRING_STRCTN) { if(polarity) { d_str_pos_ctn.push_back( atom ); @@ -1232,18 +1232,37 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms Assert( other_str.getKind()!=kind::CONST_STRING, "Other string is not constant." ); Assert( other_str.getKind()!=kind::STRING_CONCAT, "Other string is not CONCAT." ); antec.insert(antec.end(), curr_exp.begin(), curr_exp.end() ); - Node firstChar = const_str.getConst<String>().size() == 1 ? const_str : - NodeManager::currentNM()->mkConst( const_str.getConst<String>().substr(0, 1) ); - //split the string - Node eq1 = Rewriter::rewrite( other_str.eqNode( d_emptyString ) ); - Node eq2 = mkSplitEq( "c_spt", "created for v/c split", other_str, firstChar, false ); - d_pending_req_phase[ eq1 ] = true; - conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 ); - Trace("strings-solve-debug") << "Break normal form constant/variable " << std::endl; - - Node ant = mkExplain( antec ); - sendLemma( ant, conc, "CST-SPLIT" ); - ++(d_statistics.d_eq_splits); + //Opt + bool optflag = false; + if( normal_forms[nconst_k].size() > nconst_index_k + 1 && + normal_forms[nconst_k][nconst_index_k + 1].isConst() ) { + CVC4::String stra = const_str.getConst<String>(); + CVC4::String strb = normal_forms[nconst_k][nconst_index_k + 1].getConst<String>(); + CVC4::String fc = strb.substr(0, 1); + if( stra.find(fc) == std::string::npos || + (stra.find(strb) == std::string::npos && + !stra.overlap(strb)) ) { + Node sk = NodeManager::currentNM()->mkSkolem( "sopt", NodeManager::currentNM()->stringType(), "created for string sp" ); + Node eq = other_str.eqNode( mkConcat(const_str, sk) ); + Node ant = mkExplain( antec ); + sendLemma(ant, eq, "CST-EPS"); + optflag = true; + } + } + if(!optflag){ + Node firstChar = const_str.getConst<String>().size() == 1 ? const_str : + NodeManager::currentNM()->mkConst( const_str.getConst<String>().substr(0, 1) ); + //split the string + Node eq1 = Rewriter::rewrite( other_str.eqNode( d_emptyString ) ); + Node eq2 = mkSplitEq( "c_spt", "created for v/c split", other_str, firstChar, false ); + d_pending_req_phase[ eq1 ] = true; + conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 ); + Trace("strings-solve-debug") << "Break normal form constant/variable " << std::endl; + + Node ant = mkExplain( antec ); + sendLemma( ant, conc, "CST-SPLIT" ); + ++(d_statistics.d_eq_splits); + } return true; } else { std::vector< Node > antec_new_lits; @@ -1785,10 +1804,7 @@ void TheoryStrings::sendSplit( Node a, Node b, const char * c, bool preq ) { } Node TheoryStrings::mkConcat( Node n1, Node n2 ) { - std::vector< Node > c; - c.push_back( n1 ); - c.push_back( n2 ); - return mkConcat( c ); + return NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, n1, n2 ); } Node TheoryStrings::mkConcat( std::vector< Node >& c ) { @@ -2888,6 +2904,11 @@ void TheoryStrings::addMembership(Node assertion) { d_regexp_memberships.push_back( assertion ); } +Node TheoryStrings::instantiateSymRegExp(Node r) { + //TODO: + return r; +} + //// Finite Model Finding Node TheoryStrings::getNextDecisionRequest() { diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 9f99012df..33283d1cf 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -272,8 +272,8 @@ protected: void sendInfer( Node eq_exp, Node eq, const char * c ); void sendSplit( Node a, Node b, const char * c, bool preq = true ); /** mkConcat **/ - Node mkConcat( Node n1, Node n2 ); - Node mkConcat( std::vector< Node >& c ); + inline Node mkConcat( Node n1, Node n2 ); + inline Node mkConcat( std::vector< Node >& c ); /** mkExplain **/ Node mkExplain( std::vector< Node >& a ); Node mkExplain( std::vector< Node >& a, std::vector< Node >& an ); @@ -323,6 +323,7 @@ private: bool splitRegExp( Node x, Node r, Node ant ); bool addMembershipLength(Node atom); void addMembership(Node assertion); + Node instantiateSymRegExp(Node r); // Finite Model Finding diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 405fceb6f..f207bdb8e 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -41,7 +41,7 @@ TheoryModel::TheoryModel( context::Context* c, std::string name, bool enableFunc d_equalityEngine->addFunctionKind(kind::SELECT); // d_equalityEngine->addFunctionKind(kind::STORE); d_equalityEngine->addFunctionKind(kind::APPLY_CONSTRUCTOR); - d_equalityEngine->addFunctionKind(kind::APPLY_SELECTOR); + d_equalityEngine->addFunctionKind(kind::APPLY_SELECTOR_TOTAL); d_equalityEngine->addFunctionKind(kind::APPLY_TESTER); d_eeContext->push(); } @@ -422,7 +422,7 @@ TheoryEngineModelBuilder::TheoryEngineModelBuilder( TheoryEngine* te ) : d_te( t bool TheoryEngineModelBuilder::isAssignable(TNode n) { - return (n.isVar() || n.getKind() == kind::APPLY_UF || n.getKind() == kind::SELECT || n.getKind() == kind::APPLY_SELECTOR); + return (n.isVar() || n.getKind() == kind::APPLY_UF || n.getKind() == kind::SELECT || n.getKind() == kind::APPLY_SELECTOR_TOTAL); } 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..a8f3b404a 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. */ @@ -442,6 +448,7 @@ public: private: std::string d_name; std::vector<Type> d_params; + bool d_isCo; std::vector<DatatypeConstructor> d_constructors; bool d_resolved; Type d_self; @@ -488,13 +495,13 @@ private: public: /** Create a new Datatype of the given name. */ - inline explicit Datatype(std::string name); + inline explicit Datatype(std::string name, bool isCo = false); /** * Create a new Datatype of the given name, with the given * parameterization. */ - inline Datatype(std::string name, const std::vector<Type>& params); + inline Datatype(std::string name, const std::vector<Type>& params, bool isCo = false); /** * Add a constructor to this Datatype. Constructor names need not @@ -520,6 +527,9 @@ public: /** Get parameters */ inline std::vector<Type> getParameters() const; + /** is this a co-datatype? */ + inline bool isCodatatype() const; + /** * Return the cardinality of this datatype (the sum of the * cardinalities of its constructors). The Datatype must be @@ -656,18 +666,20 @@ inline std::string DatatypeUnresolvedType::getName() const throw() { return d_name; } -inline Datatype::Datatype(std::string name) : +inline Datatype::Datatype(std::string name, bool isCo) : d_name(name), d_params(), + d_isCo(isCo), d_constructors(), d_resolved(false), d_self(), d_card(CardinalityUnknown()) { } -inline Datatype::Datatype(std::string name, const std::vector<Type>& params) : +inline Datatype::Datatype(std::string name, const std::vector<Type>& params, bool isCo) : d_name(name), d_params(params), + d_isCo(isCo), d_constructors(), d_resolved(false), d_self(), @@ -701,6 +713,10 @@ inline std::vector<Type> Datatype::getParameters() const { return d_params; } +inline bool Datatype::isCodatatype() const { + return d_isCo; +} + inline bool Datatype::operator!=(const Datatype& other) const throw() { return !(*this == other); } diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp index b6db624d5..3bc17b050 100644 --- a/src/util/regexp.cpp +++ b/src/util/regexp.cpp @@ -23,6 +23,71 @@ using namespace std; namespace CVC4 {
+void String::toInternal(const std::string &s) {
+ d_str.clear();
+ unsigned i=0;
+ while(i < s.size()) {
+ if(s[i] == '\\') {
+ i++;
+ if(i < s.size()) {
+ switch(s[i]) {
+ case 'n': {d_str.push_back( convertCharToUnsignedInt('\n') );i++;} break;
+ case 't': {d_str.push_back( convertCharToUnsignedInt('\t') );i++;} break;
+ case 'v': {d_str.push_back( convertCharToUnsignedInt('\v') );i++;} break;
+ case 'b': {d_str.push_back( convertCharToUnsignedInt('\b') );i++;} break;
+ case 'r': {d_str.push_back( convertCharToUnsignedInt('\r') );i++;} break;
+ case 'f': {d_str.push_back( convertCharToUnsignedInt('\f') );i++;} break;
+ case 'a': {d_str.push_back( convertCharToUnsignedInt('\a') );i++;} break;
+ case '\\': {d_str.push_back( convertCharToUnsignedInt('\\') );i++;} break;
+ case 'x': {
+ if(i + 2 < s.size()) {
+ if((isdigit(s[i+1]) || (s[i+1] >= 'a' && s[i+1] >= 'f') || (s[i+1] >= 'A' && s[i+1] >= 'F')) &&
+ (isdigit(s[i+2]) || (s[i+2] >= 'a' && s[i+2] >= 'f') || (s[i+2] >= 'A' && s[i+2] >= 'F'))) {
+ d_str.push_back( convertCharToUnsignedInt( hexToDec(s[i+1]) * 16 + hexToDec(s[i+2]) ) );
+ i += 3;
+ } else {
+ throw CVC4::Exception( "Error String Literal: \"" + s + "\"" );
+ }
+ } else {
+ throw CVC4::Exception( "Error String Literal: \"" + s + "\"" );
+ }
+ }
+ break;
+ default: {
+ if(isdigit(s[i])) {
+ int num = (int)s[i] - (int)'0';
+ bool flag = num < 4;
+ if(i+1 < s.size() && num < 8 && isdigit(s[i+1]) && s[i+1] < '8') {
+ num = num * 8 + (int)s[i+1] - (int)'0';
+ if(flag && i+2 < s.size() && isdigit(s[i+2]) && s[i+2] < '8') {
+ num = num * 8 + (int)s[i+2] - (int)'0';
+ d_str.push_back( convertCharToUnsignedInt((char)num) );
+ i += 3;
+ } else {
+ d_str.push_back( convertCharToUnsignedInt((char)num) );
+ i += 2;
+ }
+ } else {
+ d_str.push_back( convertCharToUnsignedInt((char)num) );
+ i++;
+ }
+ } else {
+ d_str.push_back( convertCharToUnsignedInt(s[i]) );
+ i++;
+ }
+ }
+ }
+ } else {
+ throw CVC4::Exception( "should be handled by lexer: \"" + s + "\"" );
+ //d_str.push_back( convertCharToUnsignedInt('\\') );
+ }
+ } else {
+ d_str.push_back( convertCharToUnsignedInt(s[i]) );
+ i++;
+ }
+ }
+}
+
void String::getCharSet(std::set<unsigned int> &cset) const {
for(std::vector<unsigned int>::const_iterator itr = d_str.begin();
itr != d_str.end(); itr++) {
@@ -30,6 +95,21 @@ void String::getCharSet(std::set<unsigned int> &cset) const { }
}
+bool String::overlap(String &y) const {
+ unsigned n = y.size();
+ if(d_str.size() < y.size()) {
+ n = d_str.size();
+ }
+ for(unsigned i=1; i<n; i++) {
+ String s = suffix(i);
+ String p = y.prefix(i);
+ if(s == p) {
+ return true;
+ }
+ }
+ return false;
+}
+
std::string String::toString() const {
std::string str;
for(unsigned int i=0; i<d_str.size(); ++i) {
diff --git a/src/util/regexp.h b/src/util/regexp.h index 8c4a3922d..2bb2b5c4c 100644 --- a/src/util/regexp.h +++ b/src/util/regexp.h @@ -70,70 +70,7 @@ private: } } - void toInternal(const std::string &s) { - d_str.clear(); - unsigned i=0; - while(i < s.size()) { - if(s[i] == '\\') { - i++; - if(i < s.size()) { - switch(s[i]) { - case 'n': {d_str.push_back( convertCharToUnsignedInt('\n') );i++;} break; - case 't': {d_str.push_back( convertCharToUnsignedInt('\t') );i++;} break; - case 'v': {d_str.push_back( convertCharToUnsignedInt('\v') );i++;} break; - case 'b': {d_str.push_back( convertCharToUnsignedInt('\b') );i++;} break; - case 'r': {d_str.push_back( convertCharToUnsignedInt('\r') );i++;} break; - case 'f': {d_str.push_back( convertCharToUnsignedInt('\f') );i++;} break; - case 'a': {d_str.push_back( convertCharToUnsignedInt('\a') );i++;} break; - case '\\': {d_str.push_back( convertCharToUnsignedInt('\\') );i++;} break; - case 'x': { - if(i + 2 < s.size()) { - if((isdigit(s[i+1]) || (s[i+1] >= 'a' && s[i+1] >= 'f') || (s[i+1] >= 'A' && s[i+1] >= 'F')) && - (isdigit(s[i+2]) || (s[i+2] >= 'a' && s[i+2] >= 'f') || (s[i+2] >= 'A' && s[i+2] >= 'F'))) { - d_str.push_back( convertCharToUnsignedInt( hexToDec(s[i+1]) * 16 + hexToDec(s[i+2]) ) ); - i += 3; - } else { - throw CVC4::Exception( "Error String Literal: \"" + s + "\"" ); - } - } else { - throw CVC4::Exception( "Error String Literal: \"" + s + "\"" ); - } - } - break; - default: { - if(isdigit(s[i])) { - int num = (int)s[i] - (int)'0'; - bool flag = num < 4; - if(i+1 < s.size() && num < 8 && isdigit(s[i+1]) && s[i+1] < '8') { - num = num * 8 + (int)s[i+1] - (int)'0'; - if(flag && i+2 < s.size() && isdigit(s[i+2]) && s[i+2] < '8') { - num = num * 8 + (int)s[i+2] - (int)'0'; - d_str.push_back( convertCharToUnsignedInt((char)num) ); - i += 3; - } else { - d_str.push_back( convertCharToUnsignedInt((char)num) ); - i += 2; - } - } else { - d_str.push_back( convertCharToUnsignedInt((char)num) ); - i++; - } - } else { - d_str.push_back( convertCharToUnsignedInt(s[i]) ); - i++; - } - } - } - } else { - throw CVC4::Exception( "should be handled by lexer: \"" + s + "\"" ); - //d_str.push_back( convertCharToUnsignedInt('\\') ); - } - } else { - d_str.push_back( convertCharToUnsignedInt(s[i]) ); - i++; - } - } - } + void toInternal(const std::string &s); public: String() {} @@ -316,6 +253,15 @@ public: ret_vec.insert( ret_vec.end(), itr, itr + j ); return String(ret_vec); } + + String prefix(unsigned i) const { + return substr(0, i); + } + String suffix(unsigned i) const { + return substr(d_str.size() - i, i); + } + bool overlap(String &y) const; + bool isNumber() const { if(d_str.size() == 0) return false; for(unsigned int i=0; i<d_str.size(); ++i) { |