diff options
100 files changed, 1977 insertions, 1618 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt index 0cc1174d9..885577260 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -237,6 +237,7 @@ add_check_c_cxx_flag("-Wno-deprecated") add_check_cxx_flag("-Wsuggest-override") add_check_cxx_flag("-Wnon-virtual-dtor") add_check_c_cxx_flag("-Wimplicit-fallthrough") +add_check_c_cxx_flag("-Wshadow") # Temporarily disable -Wclass-memaccess to suppress 'no trivial copy-assignment' # cdlist.h warnings. Remove when fixed. diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 76992e1ba..21d7ff0ea 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -43,21 +43,32 @@ ${includes} } \ ++ *(d_exprStatistics[kind]); \ } - #define INC_STAT_VAR(type, bound_var) \ - { \ - TypeNode* typeNode = Type::getTypeNode(type); \ - TypeConstant type = typeNode->getKind() == kind::TYPE_CONSTANT ? typeNode->getConst<TypeConstant>() : LAST_TYPE; \ - if (d_exprStatisticsVars[type] == NULL) { \ - stringstream statName; \ - if (type == LAST_TYPE) { \ - statName << "expr::ExprManager::" << ((bound_var) ? "BOUND_VARIABLE" : "VARIABLE") << ":Parameterized type"; \ - } else { \ - statName << "expr::ExprManager::" << ((bound_var) ? "BOUND_VARIABLE" : "VARIABLE") << ":" << type; \ - } \ - d_exprStatisticsVars[type] = new IntStat(statName.str(), 0); \ - d_nodeManager->getStatisticsRegistry()->registerStat(d_exprStatisticsVars[type]); \ - } \ - ++ *(d_exprStatisticsVars[type]); \ +#define INC_STAT_VAR(type, bound_var) \ + { \ + TypeNode* isv_typeNode = Type::getTypeNode(type); \ + TypeConstant isv_type = isv_typeNode->getKind() == kind::TYPE_CONSTANT \ + ? isv_typeNode->getConst<TypeConstant>() \ + : LAST_TYPE; \ + if (d_exprStatisticsVars[isv_type] == NULL) \ + { \ + stringstream statName; \ + if (isv_type == LAST_TYPE) \ + { \ + statName << "expr::ExprManager::" \ + << ((bound_var) ? "BOUND_VARIABLE" : "VARIABLE") \ + << ":Parameterized isv_type"; \ + } \ + else \ + { \ + statName << "expr::ExprManager::" \ + << ((bound_var) ? "BOUND_VARIABLE" : "VARIABLE") << ":" \ + << isv_type; \ + } \ + d_exprStatisticsVars[isv_type] = new IntStat(statName.str(), 0); \ + d_nodeManager->getStatisticsRegistry()->registerStat( \ + d_exprStatisticsVars[isv_type]); \ + } \ + ++*(d_exprStatisticsVars[isv_type]); \ } #else #define INC_STAT(kind) @@ -882,13 +893,13 @@ SortConstructorType ExprManager::mkSortConstructor(const std::string& name, * @param check whether we should check the type as we compute it * (default: false) */ -Type ExprManager::getType(Expr e, bool check) +Type ExprManager::getType(Expr expr, bool check) { NodeManagerScope nms(d_nodeManager); Type t; try { t = Type(d_nodeManager, - new TypeNode(d_nodeManager->getType(e.getNode(), check))); + new TypeNode(d_nodeManager->getType(expr.getNode(), check))); } catch (const TypeCheckingExceptionPrivate& e) { throw TypeCheckingException(this, &e); } diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 998f58d0c..3ed72e03e 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -156,13 +156,20 @@ static Node exportConstant(TNode n, NodeManager* to, ExprManagerMapCollection& v class ExportPrivate { private: typedef std::unordered_map <NodeTemplate<false>, NodeTemplate<true>, TNodeHashFunction> ExportCache; - ExprManager* from; - ExprManager* to; - ExprManagerMapCollection& vmap; - uint32_t flags; - ExportCache exportCache; -public: - ExportPrivate(ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap, uint32_t flags) : from(from), to(to), vmap(vmap), flags(flags) {} + ExprManager* d_from; + ExprManager* d_to; + ExprManagerMapCollection& d_vmap; + uint32_t d_flags; + ExportCache d_exportCache; + + public: + ExportPrivate(ExprManager* from, + ExprManager* to, + ExprManagerMapCollection& vmap, + uint32_t flags) + : d_from(from), d_to(to), d_vmap(vmap), d_flags(flags) + { + } Node exportInternal(TNode n) { if(n.isNull()) return Node::null(); @@ -173,17 +180,18 @@ public: if(n.getMetaKind() == metakind::CONSTANT) { if(n.getKind() == kind::EMPTYSET) { - Type type = from->exportType(n.getConst< ::CVC4::EmptySet >().getType(), to, vmap); - return to->mkConst(::CVC4::EmptySet(type)); + Type type = d_from->exportType( + n.getConst< ::CVC4::EmptySet>().getType(), d_to, d_vmap); + return d_to->mkConst(::CVC4::EmptySet(type)); } - return exportConstant(n, NodeManager::fromExprManager(to), vmap); + return exportConstant(n, NodeManager::fromExprManager(d_to), d_vmap); } else if(n.getMetaKind() == metakind::NULLARY_OPERATOR ){ - Expr from_e(from, new Node(n)); - Type type = from->exportType(from_e.getType(), to, vmap); - return to->mkNullaryOperator(type, n.getKind()); // FIXME thread safety + Expr from_e(d_from, new Node(n)); + Type type = d_from->exportType(from_e.getType(), d_to, d_vmap); + return d_to->mkNullaryOperator(type, n.getKind()); // FIXME thread safety } else if(n.getMetaKind() == metakind::VARIABLE) { - Expr from_e(from, new Node(n)); - Expr& to_e = vmap.d_typeMap[from_e]; + Expr from_e(d_from, new Node(n)); + Expr& to_e = d_vmap.d_typeMap[from_e]; if(! to_e.isNull()) { Debug("export") << "+ mapped `" << from_e << "' to `" << to_e << "'" << std::endl; return to_e.getNode(); @@ -191,20 +199,20 @@ public: // construct new variable in other manager: // to_e is a ref, so this inserts from_e -> to_e std::string name; - Type type = from->exportType(from_e.getType(), to, vmap); + Type type = d_from->exportType(from_e.getType(), d_to, d_vmap); if(Node::fromExpr(from_e).getAttribute(VarNameAttr(), name)) { if (n.getKind() == kind::BOUND_VARIABLE) { // bound vars are only available at the Node level (not the Expr // level) TypeNode typeNode = TypeNode::fromType(type); - NodeManager* to_nm = NodeManager::fromExprManager(to); - Node n = to_nm->mkBoundVar(name, typeNode); // FIXME thread safety + NodeManager* to_nm = NodeManager::fromExprManager(d_to); + Node nn = to_nm->mkBoundVar(name, typeNode); // FIXME thread safety // Make sure that the correct `NodeManager` is in scope while // converting the node to an expression. NodeManagerScope to_nms(to_nm); - to_e = n.toExpr(); + to_e = nn.toExpr(); } else if(n.getKind() == kind::VARIABLE) { bool isGlobal; Node::fromExpr(from_e).getAttribute(GlobalVarAttr(), isGlobal); @@ -212,17 +220,24 @@ public: // Temporarily set the node manager to nullptr; this gets around // a check that mkVar isn't called internally NodeManagerScope nullScope(nullptr); - to_e = to->mkVar(name, type, isGlobal ? ExprManager::VAR_FLAG_GLOBAL : flags);// FIXME thread safety + to_e = d_to->mkVar(name, + type, + isGlobal ? ExprManager::VAR_FLAG_GLOBAL + : d_flags); // FIXME thread safety } else if(n.getKind() == kind::SKOLEM) { // skolems are only available at the Node level (not the Expr level) TypeNode typeNode = TypeNode::fromType(type); - NodeManager* to_nm = NodeManager::fromExprManager(to); - Node n = to_nm->mkSkolem(name, typeNode, "is a skolem variable imported from another ExprManager");// FIXME thread safety + NodeManager* to_nm = NodeManager::fromExprManager(d_to); + Node nn = + to_nm->mkSkolem(name, + typeNode, + "is a skolem variable imported from another " + "ExprManager"); // FIXME thread safety // Make sure that the correct `NodeManager` is in scope while // converting the node to an expression. NodeManagerScope to_nms(to_nm); - to_e = n.toExpr(); + to_e = nn.toExpr(); } else { Unhandled(); } @@ -234,38 +249,39 @@ public: // bound vars are only available at the Node level (not the Expr // level) TypeNode typeNode = TypeNode::fromType(type); - NodeManager* to_nm = NodeManager::fromExprManager(to); - Node n = to_nm->mkBoundVar(typeNode); // FIXME thread safety + NodeManager* to_nm = NodeManager::fromExprManager(d_to); + Node nn = to_nm->mkBoundVar(typeNode); // FIXME thread safety // Make sure that the correct `NodeManager` is in scope while // converting the node to an expression. NodeManagerScope to_nms(to_nm); - to_e = n.toExpr(); + to_e = nn.toExpr(); } else { // Temporarily set the node manager to nullptr; this gets around // a check that mkVar isn't called internally NodeManagerScope nullScope(nullptr); - to_e = to->mkVar(type); // FIXME thread safety + to_e = d_to->mkVar(type); // FIXME thread safety } Debug("export") << "+ exported unnamed var `" << from_e << "' with type `" << from_e.getType() << "' to `" << to_e << "' with type `" << type << "'" << std::endl; } uint64_t to_int = (uint64_t)(to_e.getNode().d_nv); uint64_t from_int = (uint64_t)(from_e.getNode().d_nv); - vmap.d_from[to_int] = from_int; - vmap.d_to[from_int] = to_int; - vmap.d_typeMap[to_e] = from_e;// insert other direction too + d_vmap.d_from[to_int] = from_int; + d_vmap.d_to[from_int] = to_int; + d_vmap.d_typeMap[to_e] = from_e; // insert other direction too // Make sure that the expressions are associated with the correct // `ExprManager`s. - Assert(from_e.getExprManager() == from); - Assert(to_e.getExprManager() == to); + Assert(from_e.getExprManager() == d_from); + Assert(to_e.getExprManager() == d_to); return Node::fromExpr(to_e); } } else { - if(exportCache.find(n) != exportCache.end()) { - return exportCache[n]; + if (d_exportCache.find(n) != d_exportCache.end()) + { + return d_exportCache[n]; } std::vector<Node> children; @@ -286,16 +302,17 @@ public: // `n` belongs to the `from` ExprManager, so begin ExprManagerScope // after printing `n` - ExprManagerScope ems(*to); + ExprManagerScope ems(*d_to); for(std::vector<Node>::iterator i = children.begin(), i_end = children.end(); i != i_end; ++i) { Debug("export") << " child: " << *i << std::endl; } } // FIXME thread safety - Node ret = NodeManager::fromExprManager(to)->mkNode(n.getKind(), children); + Node ret = + NodeManager::fromExprManager(d_to)->mkNode(n.getKind(), children); - exportCache[n] = ret; + d_exportCache[n] = ret; return ret; } }/* exportInternal() */ diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp index 595adda55..0c572f615 100644 --- a/src/expr/node_algorithm.cpp +++ b/src/expr/node_algorithm.cpp @@ -517,8 +517,7 @@ Node substituteCaptureAvoiding(TNode n, (std::distance(src.begin(), itt.base()) - 1) >= 0 && static_cast<unsigned>(std::distance(src.begin(), itt.base()) - 1) < dest.size()); - Node n = dest[std::distance(src.begin(), itt.base()) - 1]; - visited[curr] = n; + visited[curr] = dest[std::distance(src.begin(), itt.base()) - 1]; continue; } if (curr.getNumChildren() == 0) @@ -568,8 +567,7 @@ Node substituteCaptureAvoiding(TNode n, Assert(visited.find(curr[i]) != visited.end()); nb << visited[curr[i]]; } - Node n = nb; - visited[curr] = n; + visited[curr] = nb; // remove renaming if (curr.isClosure()) diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 367162420..5d409f748 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -330,8 +330,9 @@ void NodeManager::reclaimZombies() { TNode n; n.d_nv = nv; nv->d_rc = 1; // so that TNode doesn't assert-fail - for(vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { - (*i)->nmNotifyDeleteNode(n); + for (NodeManagerListener* listener : d_listeners) + { + listener->nmNotifyDeleteNode(n); } // this would mean that one of the listeners stowed away // a reference to this node! diff --git a/src/expr/type_matcher.cpp b/src/expr/type_matcher.cpp index 516870e9c..f99c8a2da 100644 --- a/src/expr/type_matcher.cpp +++ b/src/expr/type_matcher.cpp @@ -86,9 +86,9 @@ bool TypeMatcher::doMatching(TypeNode pattern, TypeNode tn) { return false; } - for (size_t i = 0, nchild = pattern.getNumChildren(); i < nchild; i++) + for (size_t j = 0, nchild = pattern.getNumChildren(); j < nchild; j++) { - if (!doMatching(pattern[i], tn[i])) + if (!doMatching(pattern[j], tn[j])) { return false; } diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 945462dd6..0aa622bfb 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -46,14 +46,15 @@ TypeNode TypeNode::substitute(const TypeNode& type, // push the operator nb << TypeNode(d_nv->d_children[0]); } - for(TypeNode::const_iterator i = begin(), - iend = end(); - i != iend; - ++i) { - if(*i == type) { + for (TypeNode::const_iterator j = begin(), iend = end(); j != iend; ++j) + { + if (*j == type) + { nb << replacement; - } else { - (*i).substitute(type, replacement); + } + else + { + (*j).substitute(type, replacement); } } diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index c4800a3ac..b999fe4b0 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -324,13 +324,14 @@ int runCvc4(int argc, char* argv[], Options& opts) { if (interrupted) break; for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j) { - Command* cmd = allCommands[i][j]->clone(); - cmd->setMuted(true); - pExecutor->doCommand(cmd); - if(cmd->interrupted()) { + Command* ccmd = allCommands[i][j]->clone(); + ccmd->setMuted(true); + pExecutor->doCommand(ccmd); + if (ccmd->interrupted()) + { interrupted = true; } - delete cmd; + delete ccmd; } } needReset = 0; @@ -350,13 +351,14 @@ int runCvc4(int argc, char* argv[], Options& opts) { for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) { for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j) { - Command* cmd = allCommands[i][j]->clone(); - cmd->setMuted(true); - pExecutor->doCommand(cmd); - if(cmd->interrupted()) { + Command* ccmd = allCommands[i][j]->clone(); + ccmd->setMuted(true); + pExecutor->doCommand(ccmd); + if (ccmd->interrupted()) + { interrupted = true; } - delete cmd; + delete ccmd; } } if (interrupted) continue; @@ -376,13 +378,14 @@ int runCvc4(int argc, char* argv[], Options& opts) { for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) { for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j) { - Command* cmd = allCommands[i][j]->clone(); - cmd->setMuted(true); - pExecutor->doCommand(cmd); - if(cmd->interrupted()) { + Command* ccmd = allCommands[i][j]->clone(); + ccmd->setMuted(true); + pExecutor->doCommand(ccmd); + if (ccmd->interrupted()) + { interrupted = true; } - delete cmd; + delete ccmd; } } needReset = 0; diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py index 0dab2ed76..d9bc1a0bd 100755 --- a/src/options/mkoptions.py +++ b/src/options/mkoptions.py @@ -239,24 +239,24 @@ enum class {type} TPL_DECL_MODE_FUNC = \ """ std::ostream& -operator<<(std::ostream& out, {type} mode) CVC4_PUBLIC;""" +operator<<(std::ostream& os, {type} mode) CVC4_PUBLIC;""" TPL_IMPL_MODE_FUNC = TPL_DECL_MODE_FUNC[:-len(" CVC4_PUBLIC;")] + \ """ {{ - out << "{type}::"; + os << "{type}::"; switch(mode) {{{cases} default: Unreachable(); }} - return out; + return os; }} """ TPL_IMPL_MODE_CASE = \ """ case {type}::{enum}: - out << "{enum}"; + os << "{enum}"; break;""" TPL_DECL_MODE_HANDLER = \ diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 94904f6d9..637603997 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1483,7 +1483,6 @@ prefixFormula[CVC4::Expr& f] boundVarDeclsReturn[terms,types] RPAREN COLON formula[f] { PARSER_STATE->popScope(); - Type t = EXPR_MANAGER->mkFunctionType(types, f.getType()); Expr bvl = EXPR_MANAGER->mkExpr( kind::BOUND_VAR_LIST, terms ); f = EXPR_MANAGER->mkExpr( kind::LAMBDA, bvl, f ); } @@ -1770,9 +1769,9 @@ postfixTerm[CVC4::Expr& f] if(left) { f = MK_EXPR(kind::BITVECTOR_CONCAT, f, MK_CONST(BitVector(k))); } else { - unsigned n = BitVectorType(f.getType()).getSize(); + unsigned bv_size = BitVectorType(f.getType()).getSize(); f = MK_EXPR(kind::BITVECTOR_CONCAT, MK_CONST(BitVector(k)), - MK_EXPR(MK_CONST(BitVectorExtract(n - 1, k)), f)); + MK_EXPR(MK_CONST(BitVectorExtract(bv_size - 1, k)), f)); } } @@ -1782,41 +1781,41 @@ postfixTerm[CVC4::Expr& f] ( COMMA formula[f] { args.push_back(f); } )* RPAREN { PARSER_STATE->checkFunctionLike(args.front()); - Kind k = PARSER_STATE->getKindForFunction(args.front()); + Kind kind = PARSER_STATE->getKindForFunction(args.front()); Debug("parser") << "expr is " << args.front() << std::endl; - Debug("parser") << "kind is " << k << std::endl; - f = MK_EXPR(k, args); + Debug("parser") << "kind is " << kind << std::endl; + f = MK_EXPR(kind, args); } /* record / tuple select */ | DOT ( identifier[id,CHECK_NONE,SYM_VARIABLE] - { Type t = f.getType(); - if(! t.isRecord()) { + { Type type = f.getType(); + if(! type.isRecord()) { PARSER_STATE->parseError("record-select applied to non-record"); } - const Record& rec = ((DatatypeType)t).getRecord(); + const Record& rec = ((DatatypeType)type).getRecord(); if(!rec.contains(id)){ PARSER_STATE->parseError(std::string("no such field `") + id + "' in record"); } - const Datatype & dt = ((DatatypeType)t).getDatatype(); + const Datatype & dt = ((DatatypeType)type).getDatatype(); std::vector<Expr> sargs; sargs.push_back( dt[0][id].getSelector() ); sargs.push_back( f ); f = MK_EXPR(CVC4::kind::APPLY_SELECTOR,sargs); } | k=numeral - { Type t = f.getType(); - if(! t.isTuple()) { + { Type type = f.getType(); + if(! type.isTuple()) { PARSER_STATE->parseError("tuple-select applied to non-tuple"); } - size_t length = ((DatatypeType)t).getTupleLength(); + size_t length = ((DatatypeType)type).getTupleLength(); if(k >= length) { std::stringstream ss; ss << "tuple is of length " << length << "; cannot access index " << k; PARSER_STATE->parseError(ss.str()); } - const Datatype & dt = ((DatatypeType)t).getDatatype(); + const Datatype & dt = ((DatatypeType)type).getDatatype(); std::vector<Expr> sargs; sargs.push_back( dt[0][k].getSelector() ); sargs.push_back( f ); @@ -2095,8 +2094,8 @@ simpleTerm[CVC4::Expr& f] for(std::vector<Expr>::const_iterator i = args.begin(); i != args.end(); ++i) { types.push_back((*i).getType()); } - DatatypeType t = EXPR_MANAGER->mkTupleType(types); - const Datatype& dt = t.getDatatype(); + DatatypeType dtype = EXPR_MANAGER->mkTupleType(types); + const Datatype& dt = dtype.getDatatype(); args.insert( args.begin(), dt[0].getConstructor() ); f = MK_EXPR(kind::APPLY_CONSTRUCTOR, args); } @@ -2105,14 +2104,14 @@ simpleTerm[CVC4::Expr& f] /* empty tuple literal */ | LPAREN RPAREN { std::vector<Type> types; - DatatypeType t = EXPR_MANAGER->mkTupleType(types); - const Datatype& dt = t.getDatatype(); + DatatypeType dtype = EXPR_MANAGER->mkTupleType(types); + const Datatype& dt = dtype.getDatatype(); f = MK_EXPR(kind::APPLY_CONSTRUCTOR, dt[0].getConstructor()); } /* empty record literal */ | PARENHASH HASHPAREN - { DatatypeType t = EXPR_MANAGER->mkRecordType(std::vector< std::pair<std::string, Type> >()); - const Datatype& dt = t.getDatatype(); + { DatatypeType dtype = EXPR_MANAGER->mkRecordType(std::vector< std::pair<std::string, Type> >()); + const Datatype& dt = dtype.getDatatype(); f = MK_EXPR(kind::APPLY_CONSTRUCTOR, dt[0].getConstructor()); } /* empty set literal */ @@ -2197,8 +2196,8 @@ simpleTerm[CVC4::Expr& f] for(unsigned i = 0; i < names.size(); ++i) { typeIds.push_back(std::make_pair(names[i], args[i].getType())); } - DatatypeType t = EXPR_MANAGER->mkRecordType(typeIds); - const Datatype& dt = t.getDatatype(); + DatatypeType dtype = EXPR_MANAGER->mkRecordType(typeIds); + const Datatype& dt = dtype.getDatatype(); args.insert( args.begin(), dt[0].getConstructor() ); f = MK_EXPR(kind::APPLY_CONSTRUCTOR, args); } @@ -2208,8 +2207,8 @@ simpleTerm[CVC4::Expr& f] /* ascriptions will be required for parameterized zero-ary constructors */ { f = PARSER_STATE->getVariable(name); // datatypes: zero-ary constructors - Type t2 = f.getType(); - if(t2.isConstructor() && ConstructorType(t2).getArity() == 0) { + Type dtype = f.getType(); + if(dtype.isConstructor() && ConstructorType(dtype).getArity() == 0) { // don't require parentheses, immediately turn it into an apply f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, f); } diff --git a/src/parser/line_buffer.cpp b/src/parser/line_buffer.cpp index 35263f3ac..6e7614d88 100644 --- a/src/parser/line_buffer.cpp +++ b/src/parser/line_buffer.cpp @@ -69,8 +69,10 @@ bool LineBuffer::isPtrBefore(uint8_t* ptr, size_t line, size_t pos_in_line) { return false; } -bool LineBuffer::readToLine(size_t line) { - while (line >= d_lines.size()) { +bool LineBuffer::readToLine(size_t line_size) +{ + while (line_size >= d_lines.size()) + { if (!(*d_stream)) { return false; } diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 5beec6565..eae9636a2 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -536,7 +536,6 @@ api::Term Parser::applyTypeAscription(api::Term t, api::Sort s) api::Sort etype = t.getSort(); if (etype.isConstructor()) { - api::Sort etype = t.getSort(); // get the datatype that t belongs to api::Sort etyped = etype.getConstructorCodomainSort(); api::Datatype d = etyped.getDatatype(); diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index a47d58944..9ae9f7261 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -441,10 +441,10 @@ command [std::unique_ptr<CVC4::Command>* cmd] } } ( k=INTEGER_LITERAL - { unsigned n = AntlrInput::tokenToUnsigned(k); - if(n == 0) { + { unsigned num = AntlrInput::tokenToUnsigned(k); + if(num == 0) { cmd->reset(new EmptyCommand()); - } else if(n == 1) { + } else if(num == 1) { PARSER_STATE->pushScope(); cmd->reset(new PushCommand()); } else { @@ -452,10 +452,10 @@ command [std::unique_ptr<CVC4::Command>* cmd] do { PARSER_STATE->pushScope(); Command* push_cmd = new PushCommand(); - push_cmd->setMuted(n > 1); + push_cmd->setMuted(num > 1); seq->addCommand(push_cmd); - --n; - } while(n > 0); + --num; + } while(num > 0); cmd->reset(seq.release()); } } @@ -474,14 +474,14 @@ command [std::unique_ptr<CVC4::Command>* cmd] } } ( k=INTEGER_LITERAL - { unsigned n = AntlrInput::tokenToUnsigned(k); - if(n > PARSER_STATE->scopeLevel()) { + { unsigned num = AntlrInput::tokenToUnsigned(k); + if(num > PARSER_STATE->scopeLevel()) { PARSER_STATE->parseError("Attempted to pop above the top stack " "frame."); } - if(n == 0) { + if(num == 0) { cmd->reset(new EmptyCommand()); - } else if(n == 1) { + } else if(num == 1) { PARSER_STATE->popScope(); cmd->reset(new PopCommand()); } else { @@ -489,10 +489,10 @@ command [std::unique_ptr<CVC4::Command>* cmd] do { PARSER_STATE->popScope(); Command* pop_command = new PopCommand(); - pop_command->setMuted(n > 1); + pop_command->setMuted(num > 1); seq->addCommand(pop_command); - --n; - } while(n > 0); + --num; + } while(num > 0); cmd->reset(seq.release()); } } @@ -1263,7 +1263,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd] ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] { PARSER_STATE->checkUserSymbol(name); } nonemptySortList[sorts] RPAREN_TOK - { Type t; + { Type tt; if(sorts.size() > 1) { if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) { PARSER_STATE->parseError( @@ -1275,13 +1275,13 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd] // must flatten Type range = sorts.back(); sorts.pop_back(); - t = PARSER_STATE->mkFlatFunctionType(sorts, range); + tt = PARSER_STATE->mkFlatFunctionType(sorts, range); } else { - t = sorts[0]; + tt = sorts[0]; } // allow overloading - Expr func = PARSER_STATE->mkVar(name, t, ExprManager::VAR_FLAG_NONE, true); - seq->addCommand(new DeclareFunctionCommand(name, func, t)); + Expr func = PARSER_STATE->mkVar(name, tt, ExprManager::VAR_FLAG_NONE, true); + seq->addCommand(new DeclareFunctionCommand(name, func, tt)); sorts.clear(); } )+ @@ -1293,7 +1293,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd] ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] { PARSER_STATE->checkUserSymbol(name); } sortList[sorts] RPAREN_TOK - { Type t = EXPR_MANAGER->booleanType(); + { Type boolType = EXPR_MANAGER->booleanType(); if(sorts.size() > 0) { if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) { PARSER_STATE->parseError( @@ -1302,11 +1302,11 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd] + PARSER_STATE->getLogic().getLogicString() + " unless option --uf-ho is used"); } - t = EXPR_MANAGER->mkFunctionType(sorts, t); + boolType = EXPR_MANAGER->mkFunctionType(sorts, boolType); } // allow overloading - Expr func = PARSER_STATE->mkVar(name, t, ExprManager::VAR_FLAG_NONE, true); - seq->addCommand(new DeclareFunctionCommand(name, func, t)); + Expr func = PARSER_STATE->mkVar(name, boolType, ExprManager::VAR_FLAG_NONE, true); + seq->addCommand(new DeclareFunctionCommand(name, func, boolType)); sorts.clear(); } )+ @@ -1335,18 +1335,18 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd] // declare the name down here (while parsing term, signature // must not be extended with the name itself; no recursion // permitted) - Type t = e.getType(); + Type tt = e.getType(); if( sortedVarNames.size() > 0 ) { - std::vector<CVC4::Type> sorts; - sorts.reserve(sortedVarNames.size()); + std::vector<CVC4::Type> types; + types.reserve(sortedVarNames.size()); for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i = sortedVarNames.begin(), iend = sortedVarNames.end(); i != iend; ++i) { - sorts.push_back((*i).second); + types.push_back((*i).second); } - t = EXPR_MANAGER->mkFunctionType(sorts, t); + tt = EXPR_MANAGER->mkFunctionType(types, tt); } - Expr func = PARSER_STATE->mkVar(name, t, + Expr func = PARSER_STATE->mkVar(name, tt, ExprManager::VAR_FLAG_DEFINED); cmd->reset(new DefineFunctionCommand(name, func, terms, e)); } @@ -1750,8 +1750,8 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] cargs.push_back(f); cargs.insert(cargs.end(),args.begin(),args.end()); Expr c = MK_EXPR(kind::APPLY_CONSTRUCTOR,cargs); - Expr bvl = MK_EXPR(kind::BOUND_VAR_LIST,args); - Expr mc = MK_EXPR(kind::MATCH_BIND_CASE, bvl, c, f3); + Expr bvla = MK_EXPR(kind::BOUND_VAR_LIST,args); + Expr mc = MK_EXPR(kind::MATCH_BIND_CASE, bvla, c, f3); matchcases.push_back(mc); // now, pop the scope PARSER_STATE->popScope(); @@ -1781,8 +1781,8 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] Expr mc; if (f.getKind() == kind::BOUND_VARIABLE) { - Expr bvl = MK_EXPR(kind::BOUND_VAR_LIST, f); - mc = MK_EXPR(kind::MATCH_BIND_CASE, bvl, f, f3); + Expr bvlf = MK_EXPR(kind::BOUND_VAR_LIST, f); + mc = MK_EXPR(kind::MATCH_BIND_CASE, bvlf, f, f3); } else { @@ -2116,8 +2116,8 @@ attribute[CVC4::Expr& expr, CVC4::Expr& retExpr, std::string& attr] avar = expr[0]; } }else{ - Type t = EXPR_MANAGER->booleanType(); - avar = PARSER_STATE->mkVar(attr_name, t); + Type boolType = EXPR_MANAGER->booleanType(); + avar = PARSER_STATE->mkVar(attr_name, boolType); } if( success ){ //Will set the attribute on auxiliary var (preserves attribute on @@ -2151,8 +2151,8 @@ attribute[CVC4::Expr& expr, CVC4::Expr& retExpr, std::string& attr] values.push_back( n ); std::string attr_name(AntlrInput::tokenText($tok)); attr_name.erase( attr_name.begin() ); - Type t = EXPR_MANAGER->booleanType(); - Expr avar = PARSER_STATE->mkVar(attr_name, t); + Type boolType = EXPR_MANAGER->booleanType(); + Expr avar = PARSER_STATE->mkVar(attr_name, boolType); retExpr = MK_EXPR(kind::INST_ATTRIBUTE, avar); Command* c = new SetUserAttributeCommand( attr_name, avar, values ); c->setMuted(true); diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 94a273193..15fdd8461 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1376,9 +1376,9 @@ void Smt2::mkSygusDatatype(CVC4::Datatype& dt, } else { - std::stringstream ss; - ss << "unexpected parse operator for sygus constructor" << ops[i]; - parseError(ss.str()); + std::stringstream ess; + ess << "unexpected parse operator for sygus constructor" << ops[i]; + parseError(ess.str()); } Debug("parser-sygus") << " finished constructing the datatype" << std::endl; @@ -1696,12 +1696,12 @@ Expr Smt2::applyParseOp(ParseOp& p, std::vector<Expr>& args) { argTypes.push_back((*i).getType()); } - Expr op = getOverloadedFunctionForTypes(p.d_name, argTypes); - if (!op.isNull()) + Expr fop = getOverloadedFunctionForTypes(p.d_name, argTypes); + if (!fop.isNull()) { - checkFunctionLike(op); - kind = getKindForFunction(op); - args.insert(args.begin(), op); + checkFunctionLike(fop); + kind = getKindForFunction(fop); + args.insert(args.begin(), fop); } else { diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index 873fde25c..afa072e6d 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -965,8 +965,8 @@ thfAtomTyping[CVC4::Command*& cmd] else { // as yet, it's undeclared - Type type = PARSER_STATE->mkSort(name); - cmd = new DeclareTypeCommand(name, 0, type); + Type atype = PARSER_STATE->mkSort(name); + cmd = new DeclareTypeCommand(name, 0, atype); } } | parseThfType[type] @@ -1317,8 +1317,8 @@ tffTypedAtom[CVC4::Command*& cmd] PARSER_STATE->parseError("Symbol `" + name + "' previously declared as a constant; cannot also be a sort"); } else { // as yet, it's undeclared - Type type = PARSER_STATE->mkSort(name); - cmd = new DeclareTypeCommand(name, 0, type); + Type atype = PARSER_STATE->mkSort(name); + cmd = new DeclareTypeCommand(name, 0, atype); } } | parseType[type] @@ -1336,8 +1336,8 @@ tffTypedAtom[CVC4::Command*& cmd] } } else { // as yet, it's undeclared - CVC4::Expr expr = PARSER_STATE->mkVar(name, type); - cmd = new DeclareFunctionCommand(name, expr, type); + CVC4::Expr aexpr = PARSER_STATE->mkVar(name, type); + cmd = new DeclareFunctionCommand(name, aexpr, type); } } ) diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp index d6259294a..debb4d2ac 100644 --- a/src/preprocessing/passes/miplib_trick.cpp +++ b/src/preprocessing/passes/miplib_trick.cpp @@ -195,50 +195,50 @@ PreprocessingPassResult MipLibTrick::applyInternal( Node trueNode = nm->mkConst(true); unordered_map<TNode, Node, TNodeHashFunction> intVars; - for (TNode v : d_boolVars) + for (TNode v0 : d_boolVars) { - if (propagator->isAssigned(v)) + if (propagator->isAssigned(v0)) { - Debug("miplib") << "ineligible: " << v << " because assigned " - << propagator->getAssignment(v) << endl; + Debug("miplib") << "ineligible: " << v0 << " because assigned " + << propagator->getAssignment(v0) << endl; continue; } vector<TNode> assertions; - booleans::CircuitPropagator::BackEdgesMap::const_iterator j = - backEdges.find(v); + booleans::CircuitPropagator::BackEdgesMap::const_iterator j0 = + backEdges.find(v0); // if not in back edges map, the bool var is unconstrained, showing up in no // assertions. if maps to an empty vector, that means the bool var was // asserted itself. - if (j != backEdges.end()) + if (j0 != backEdges.end()) { - if (!(*j).second.empty()) + if (!(*j0).second.empty()) { - traceBackToAssertions(propagator, (*j).second, assertions); + traceBackToAssertions(propagator, (*j0).second, assertions); } else { - assertions.push_back(v); + assertions.push_back(v0); } } - Debug("miplib") << "for " << v << endl; + Debug("miplib") << "for " << v0 << endl; bool eligible = true; map<pair<Node, Node>, uint64_t> marks; map<pair<Node, Node>, vector<Rational> > coef; map<pair<Node, Node>, vector<Rational> > checks; map<pair<Node, Node>, vector<TNode> > asserts; - for (vector<TNode>::const_iterator j = assertions.begin(); - j != assertions.end(); - ++j) + for (vector<TNode>::const_iterator j1 = assertions.begin(); + j1 != assertions.end(); + ++j1) { - Debug("miplib") << " found: " << *j << endl; - if ((*j).getKind() != kind::IMPLIES) + Debug("miplib") << " found: " << *j1 << endl; + if ((*j1).getKind() != kind::IMPLIES) { eligible = false; Debug("miplib") << " -- INELIGIBLE -- (not =>)" << endl; break; } - Node conj = BooleanSimplification::simplify((*j)[0]); + Node conj = BooleanSimplification::simplify((*j1)[0]); if (conj.getKind() == kind::AND && conj.getNumChildren() > 6) { eligible = false; @@ -252,11 +252,11 @@ PreprocessingPassResult MipLibTrick::applyInternal( Debug("miplib") << " -- INELIGIBLE -- (not /\\ or literal)" << endl; break; } - if ((*j)[1].getKind() != kind::EQUAL - || !(((*j)[1][0].isVar() - && (*j)[1][1].getKind() == kind::CONST_RATIONAL) - || ((*j)[1][0].getKind() == kind::CONST_RATIONAL - && (*j)[1][1].isVar()))) + if ((*j1)[1].getKind() != kind::EQUAL + || !(((*j1)[1][0].isVar() + && (*j1)[1][1].getKind() == kind::CONST_RATIONAL) + || ((*j1)[1][0].getKind() == kind::CONST_RATIONAL + && (*j1)[1][1].isVar()))) { eligible = false; Debug("miplib") << " -- INELIGIBLE -- (=> (and X X) X)" << endl; @@ -273,13 +273,13 @@ PreprocessingPassResult MipLibTrick::applyInternal( { posv.push_back(*ii); neg[*ii] = false; - found_x = found_x || v == *ii; + found_x = found_x || v0 == *ii; } else if ((*ii).getKind() == kind::NOT && (*ii)[0].isVar()) { posv.push_back((*ii)[0]); neg[(*ii)[0]] = true; - found_x = found_x || v == (*ii)[0]; + found_x = found_x || v0 == (*ii)[0]; } else { @@ -303,20 +303,20 @@ PreprocessingPassResult MipLibTrick::applyInternal( if (!found_x) { eligible = false; - Debug("miplib") << " --INELIGIBLE -- (couldn't find " << v + Debug("miplib") << " --INELIGIBLE -- (couldn't find " << v0 << " in conjunction)" << endl; break; } sort(posv.begin(), posv.end()); const Node pos = NodeManager::currentNM()->mkNode(kind::AND, posv); - const TNode var = ((*j)[1][0].getKind() == kind::CONST_RATIONAL) - ? (*j)[1][1] - : (*j)[1][0]; + const TNode var = ((*j1)[1][0].getKind() == kind::CONST_RATIONAL) + ? (*j1)[1][1] + : (*j1)[1][0]; const pair<Node, Node> pos_var(pos, var); const Rational& constant = - ((*j)[1][0].getKind() == kind::CONST_RATIONAL) - ? (*j)[1][0].getConst<Rational>() - : (*j)[1][1].getConst<Rational>(); + ((*j1)[1][0].getKind() == kind::CONST_RATIONAL) + ? (*j1)[1][0].getConst<Rational>() + : (*j1)[1][1].getConst<Rational>(); uint64_t mark = 0; unsigned countneg = 0, thepos = 0; for (unsigned ii = 0; ii < pos.getNumChildren(); ++ii) @@ -368,12 +368,12 @@ PreprocessingPassResult MipLibTrick::applyInternal( } checks[pos_var][mark] = constant; } - asserts[pos_var].push_back(*j); + asserts[pos_var].push_back(*j1); } else { TNode x = conj; - if (x != v && x != (v).notNode()) + if (x != v0 && x != (v0).notNode()) { eligible = false; Debug("miplib") @@ -383,14 +383,14 @@ PreprocessingPassResult MipLibTrick::applyInternal( const bool xneg = (x.getKind() == kind::NOT); x = xneg ? x[0] : x; Debug("miplib") << " x:" << x << " " << xneg << endl; - const TNode var = ((*j)[1][0].getKind() == kind::CONST_RATIONAL) - ? (*j)[1][1] - : (*j)[1][0]; + const TNode var = ((*j1)[1][0].getKind() == kind::CONST_RATIONAL) + ? (*j1)[1][1] + : (*j1)[1][0]; const pair<Node, Node> x_var(x, var); const Rational& constant = - ((*j)[1][0].getKind() == kind::CONST_RATIONAL) - ? (*j)[1][0].getConst<Rational>() - : (*j)[1][1].getConst<Rational>(); + ((*j1)[1][0].getKind() == kind::CONST_RATIONAL) + ? (*j1)[1][0].getConst<Rational>() + : (*j1)[1][1].getConst<Rational>(); unsigned mark = (xneg ? 0 : 1); if ((marks[x_var] & (1u << mark)) != 0) { @@ -414,7 +414,7 @@ PreprocessingPassResult MipLibTrick::applyInternal( coef[x_var].resize(6); coef[x_var][0] = constant; } - asserts[x_var].push_back(*j); + asserts[x_var].push_back(*j1); } } if (eligible) @@ -454,14 +454,15 @@ PreprocessingPassResult MipLibTrick::applyInternal( { Rational sum = 0; Debug("miplib") << k << " => " << checks[pos_var][k] << endl; - for (size_t v = 1, kk = k; kk != 0; ++v, kk >>= 1) + for (size_t v1 = 1, kk = k; kk != 0; ++v1, kk >>= 1) { if ((kk & 0x1) == 1) { Assert(pos.getKind() == kind::AND); - Debug("miplib") << "var " << v << " : " << pos[v - 1] - << " coef:" << coef[pos_var][v - 1] << endl; - sum += coef[pos_var][v - 1]; + Debug("miplib") + << "var " << v1 << " : " << pos[v1 - 1] + << " coef:" << coef[pos_var][v1 - 1] << endl; + sum += coef[pos_var][v1 - 1]; } } Debug("miplib") << "checkSum is " << sum << " input says " @@ -490,7 +491,7 @@ PreprocessingPassResult MipLibTrick::applyInternal( continue; } - Debug("miplib") << " -- ELIGIBLE " << v << " , " << pos << " --" + Debug("miplib") << " -- ELIGIBLE " << v0 << " , " << pos << " --" << endl; vector<Node> newVars; expr::NodeSelfIterator ii, iiend; @@ -549,10 +550,10 @@ PreprocessingPassResult MipLibTrick::applyInternal( if (pos.getKind() == kind::AND) { NodeBuilder<> sumb(kind::PLUS); - for (size_t ii = 0; ii < pos.getNumChildren(); ++ii) + for (size_t jj = 0; jj < pos.getNumChildren(); ++jj) { sumb << nm->mkNode( - kind::MULT, nm->mkConst(coef[pos_var][ii]), newVars[ii]); + kind::MULT, nm->mkConst(coef[pos_var][jj]), newVars[jj]); } sum = sumb; } diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp index 24484359a..41bb226a3 100644 --- a/src/preprocessing/passes/sygus_inference.cpp +++ b/src/preprocessing/passes/sygus_inference.cpp @@ -328,10 +328,10 @@ bool SygusInference::solveSygus(std::vector<Node>& assertions, if (itffv != ff_var_to_ff.end()) { Node ff = itffv->second; - Node body = Node::fromExpr(it->second); - Trace("sygus-infer") << "Define " << ff << " as " << body << std::endl; + Node body2 = Node::fromExpr(it->second); + Trace("sygus-infer") << "Define " << ff << " as " << body2 << std::endl; funs.push_back(ff); - sols.push_back(body); + sols.push_back(body2); } } return true; diff --git a/src/preprocessing/passes/symmetry_detect.cpp b/src/preprocessing/passes/symmetry_detect.cpp index 8d0d04149..d0327263b 100644 --- a/src/preprocessing/passes/symmetry_detect.cpp +++ b/src/preprocessing/passes/symmetry_detect.cpp @@ -374,24 +374,24 @@ bool PartitionMerger::mergeNewVar(unsigned curr_index, Assert(d_base_indices.find(i) == d_base_indices.end()); d_base_indices.insert(i); Trace("sym-dt-debug") << i << " "; - const Partition& p = partitions[i]; - children.push_back(p.d_term); - schildren.push_back(p.d_sterm); + const Partition& p2 = partitions[i]; + children.push_back(p2.d_term); + schildren.push_back(p2.d_sterm); Assert(active_indices.find(i) != active_indices.end()); active_indices.erase(i); } Trace("sym-dt-debug") << "}" << std::endl; Trace("sym-dt-debug") << "Reconstruct master partition " << d_master_base_index << std::endl; - Partition& p = partitions[d_master_base_index]; + Partition& p3 = partitions[d_master_base_index]; // reconstruct the master partition - p.d_term = mkAssociativeNode(d_kind, children); - p.d_sterm = mkAssociativeNode(d_kind, schildren); - Assert(p.d_subvar_to_vars.size() == 1); - Node sb_v = p.d_subvar_to_vars.begin()->first; + p3.d_term = mkAssociativeNode(d_kind, children); + p3.d_sterm = mkAssociativeNode(d_kind, schildren); + Assert(p3.d_subvar_to_vars.size() == 1); + Node sb_v = p3.d_subvar_to_vars.begin()->first; Trace("sym-dt-debug") << "- set var to svar: " << merge_var << " -> " << sb_v << std::endl; - p.addVariable(sb_v, merge_var); + p3.addVariable(sb_v, merge_var); return true; } if (mergeNewVar(curr_index + 1, @@ -1139,7 +1139,7 @@ void SymmetryDetect::processPartitions( k, partitions, svee.second, active_indices, fixedSVar, fixedVar); // remove the list of fixed variables - for (unsigned k = 0; k < nfvars; k++) + for (unsigned i = 0; i < nfvars; i++) { fixedVar.pop_back(); fixedSVar.pop_back(); @@ -1218,7 +1218,7 @@ void SymmetryDetect::processPartitions( // if still active if (active_indices.find(index) != active_indices.end()) { - for (unsigned i = 0, size = fixedSVar.size(); i < size; i++) + for (unsigned i = 0, size2 = fixedSVar.size(); i < size2; i++) { // add variable partitions[index].addVariable(fixedSVar[i], fixedVar[i]); diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp index f3ca65b79..7b8e61359 100644 --- a/src/preprocessing/passes/synth_rew_rules.cpp +++ b/src/preprocessing/passes/synth_rew_rules.cpp @@ -310,11 +310,11 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal( std::map<TypeNode, bool> hasArgType; for (unsigned j = 0, size = argListTmp.size(); j < size; j++) { - TypeNode t = argListTmp[j]; - if (hasArgType.find(t) == hasArgType.end()) + TypeNode tn = argListTmp[j]; + if (hasArgType.find(tn) == hasArgType.end()) { - hasArgType[t] = true; - argList.push_back(t); + hasArgType[tn] = true; + argList.push_back(tn); } } } diff --git a/src/preprocessing/util/ite_utilities.cpp b/src/preprocessing/util/ite_utilities.cpp index 9c3db0b0d..c609eebd7 100644 --- a/src/preprocessing/util/ite_utilities.cpp +++ b/src/preprocessing/util/ite_utilities.cpp @@ -1252,7 +1252,6 @@ Node ITESimplifier::attemptEagerRemoval(TNode atom) Assert(leaves != NULL); if (!std::binary_search(leaves->begin(), leaves->end(), constant)) { - std::pair<Node, Node> pair = make_pair(cite, constant); d_constantIteEqualsConstantCache[pair] = d_false; return d_false; } @@ -1534,9 +1533,11 @@ Node ITESimplifier::simpITEAtom(TNode atom) struct preprocess_stack_element { - TNode node; - bool children_added; - preprocess_stack_element(TNode node) : node(node), children_added(false) {} + TNode d_node; + bool d_children_added; + preprocess_stack_element(TNode node) : d_node(node), d_children_added(false) + { + } }; /* struct preprocess_stack_element */ Node ITESimplifier::simpITE(TNode assertion) @@ -1555,7 +1556,7 @@ Node ITESimplifier::simpITE(TNode assertion) // cout << "call " << call << " : " << iteration << endl; // The current node we are processing preprocess_stack_element& stackHead = toVisit.back(); - TNode current = stackHead.node; + TNode current = stackHead.d_node; // If node has no ITE's or already in the cache we're done, pop from the // stack @@ -1577,7 +1578,7 @@ Node ITESimplifier::simpITE(TNode assertion) } // Not yet substituted, so process - if (stackHead.children_added) + if (stackHead.d_children_added) { // Children have been processed, so substitute NodeBuilder<> builder(current.getKind()); @@ -1617,7 +1618,7 @@ Node ITESimplifier::simpITE(TNode assertion) // Mark that we have added the children if any if (current.getNumChildren() > 0) { - stackHead.children_added = true; + stackHead.d_children_added = true; // We need to add the children for (TNode::iterator child_it = current.begin(); child_it != current.end(); @@ -1875,7 +1876,7 @@ Node ITECareSimplifier::simplifyWithCare(TNode e) continue; } - for (unsigned i = 0; i < v.getNumChildren(); ++i) + for (i = 0; i < v.getNumChildren(); ++i) { updateQueue(queue, v[i], cs); } diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 70324d313..3120fe8f1 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -144,9 +144,10 @@ void CvcPrinter::toStream( const BitVector& bv = n.getConst<BitVector>(); const Integer& x = bv.getValue(); out << "0bin"; - unsigned n = bv.getSize(); - while(n-- > 0) { - out << (x.testBit(n) ? '1' : '0'); + unsigned size = bv.getSize(); + while (size-- > 0) + { + out << (x.testBit(size) ? '1' : '0'); } break; } @@ -1495,12 +1496,16 @@ static void toStream(std::ostream& out, out << " | "; } firstConstructor = false; - const DatatypeConstructor& c = *j; - out << c.getName(); - if(c.getNumArgs() > 0) { + const DatatypeConstructor& cons = *j; + out << cons.getName(); + if (cons.getNumArgs() > 0) + { out << '('; bool firstSelector = true; - for(DatatypeConstructor::const_iterator k = c.begin(); k != c.end(); ++k) { + for (DatatypeConstructor::const_iterator k = cons.begin(); + k != cons.end(); + ++k) + { if(! firstSelector) { out << ", "; } diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 87ddf6168..0334c97b6 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -152,7 +152,7 @@ void Smt2Printer::toStream(std::ostream& out, case kind::CONST_BITVECTOR: { const BitVector& bv = n.getConst<BitVector>(); const Integer& x = bv.getValue(); - unsigned n = bv.getSize(); + unsigned width = bv.getSize(); if (d_variant == sygus_variant || options::bvPrintConstsInBinary()) { out << "#b" << bv.toString(); @@ -160,7 +160,7 @@ void Smt2Printer::toStream(std::ostream& out, else { out << "(_ "; - out << "bv" << x << " " << n; + out << "bv" << x << " " << width; out << ")"; } @@ -232,15 +232,15 @@ void Smt2Printer::toStream(std::ostream& out, n.getConst<DatatypeIndexConstant>().getIndex())); if (dt.isTuple()) { - unsigned int n = dt[0].getNumArgs(); - if (n == 0) + unsigned int nargs = dt[0].getNumArgs(); + if (nargs == 0) { out << "Tuple"; } else { out << "(Tuple"; - for (unsigned int i = 0; i < n; i++) + for (unsigned int i = 0; i < nargs; i++) { out << " " << dt[0][i].getRangeType(); } @@ -2027,9 +2027,9 @@ static void toStream(std::ostream& out, i != i_end; ++i) { - const Datatype& d = i->getDatatype(); - out << "(" << CVC4::quoteSymbol(d.getName()) << " "; - toStream(out, d); + const Datatype& dt = i->getDatatype(); + out << "(" << CVC4::quoteSymbol(dt.getName()) << " "; + toStream(out, dt); out << ")"; } out << ")"; diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp index 75b7b7f1b..32dcaf5b2 100644 --- a/src/proof/array_proof.cpp +++ b/src/proof/array_proof.cpp @@ -475,7 +475,6 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, pf.d_children[0]->d_node = simplifyBooleanNode(pf.d_children[0]->d_node); Node n1 = toStreamRecLFSC(ss, tp, *(pf.d_children[0]), tb + 1, map); - Node n2; Debug("mgd") << "\ndoing trans proof, got n1 " << n1 << "\n"; if(tb == 1) { Debug("mgdx") << "\ntrans proof[0], got n1 " << n1 << "\n"; @@ -489,7 +488,6 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, std::map<size_t, Node> childToStream; - std::stringstream ss1(ss.str()), ss2; std::pair<Node, Node> nodePair; for (size_t i = 1; i < pf.d_children.size(); ++i) { @@ -562,9 +560,9 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, while (j < pf.d_children.size() && !sequenceOver) { - std::stringstream dontCare; - nodeAfterEqualitySequence = toStreamRecLFSC( - dontCare, tp, *(pf.d_children[j]), tb + 1, map); + std::stringstream ignore; + nodeAfterEqualitySequence = + toStreamRecLFSC(ignore, tp, *(pf.d_children[j]), tb + 1, map); if (((nodeAfterEqualitySequence[0] == n1[0]) && (nodeAfterEqualitySequence[1] == n1[1])) || ((nodeAfterEqualitySequence[0] == n1[1]) diff --git a/src/proof/clausal_bitvector_proof.cpp b/src/proof/clausal_bitvector_proof.cpp index 6b0a57725..6a5009b1f 100644 --- a/src/proof/clausal_bitvector_proof.cpp +++ b/src/proof/clausal_bitvector_proof.cpp @@ -196,11 +196,11 @@ void ClausalBitVectorProof::optimizeDratProof() if (options::bvOptimizeSatProof() == options::BvOptimizeSatProof::FORMULA) { - std::ifstream optFormulaStream{optFormulaFilename}; - const int64_t startPos = static_cast<int64_t>(optFormulaStream.tellg()); - std::vector<prop::SatClause> core = parseDimacs(optFormulaStream); + std::ifstream optFormulaInStream{optFormulaFilename}; + const int64_t startPos = static_cast<int64_t>(optFormulaInStream.tellg()); + std::vector<prop::SatClause> core = parseDimacs(optFormulaInStream); d_dratOptimizationStatistics.d_optimizedFormulaSize.setData( - static_cast<int64_t>(optFormulaStream.tellg()) - startPos); + static_cast<int64_t>(optFormulaInStream.tellg()) - startPos); CodeTimer clauseMatchingTimer{ d_dratOptimizationStatistics.d_clauseMatchingTime}; diff --git a/src/proof/drat/drat_proof.cpp b/src/proof/drat/drat_proof.cpp index 162efc3e5..e35741cde 100644 --- a/src/proof/drat/drat_proof.cpp +++ b/src/proof/drat/drat_proof.cpp @@ -215,12 +215,12 @@ DratProof DratProof::fromBinary(const std::string& s) } default: { - std::ostringstream s; - s << "Invalid instruction in Drat proof. Instruction bits: " - << std::bitset<8>(*i) - << ". Expected 'a' (01100001) or 'd' " - "(01100100)."; - throw InvalidDratProofException(s.str()); + std::ostringstream errmsg; + errmsg << "Invalid instruction in Drat proof. Instruction bits: " + << std::bitset<8>(*i) + << ". Expected 'a' (01100001) or 'd' " + "(01100100)."; + throw InvalidDratProofException(errmsg.str()); } } } diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index fda3f7424..33f284bf8 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -682,11 +682,9 @@ void LFSCProof::toStream(std::ostream& out) const d_cnfProof->collectAtomsForClauses(used_lemmas, atoms); // collects the atoms in the assertions - for (NodeSet::const_iterator it = used_assertions.begin(); - it != used_assertions.end(); - ++it) + for (TNode used_assertion : used_assertions) { - utils::collectAtoms(*it, atoms); + utils::collectAtoms(used_assertion, atoms); } std::set<Node>::iterator atomIt; diff --git a/src/proof/resolution_bitvector_proof.cpp b/src/proof/resolution_bitvector_proof.cpp index 8d4b56d54..120397d08 100644 --- a/src/proof/resolution_bitvector_proof.cpp +++ b/src/proof/resolution_bitvector_proof.cpp @@ -366,10 +366,8 @@ void LfscResolutionBitVectorProof::printTheoryLemmaProof( if (possibleMatch.getKind() == kind::OR) { - for (unsigned i = 0; i < possibleMatch.getNumChildren(); ++i) + for (const Expr& lit : possibleMatch) { - Expr lit = possibleMatch[i]; - if (lit.getKind() == kind::NOT) { os << "(intro_assump_t _ _ _ "; @@ -434,13 +432,13 @@ void LfscResolutionBitVectorProof::printTheoryLemmaProof( // conflict has a FALSE assertion in it; this can happen in some corner // cases, where the FALSE is the result of a rewrite. - for (unsigned i = 0; i < lemma.size(); ++i) + for (const Expr& lit : lemma) { - if (lemma[i].getKind() == kind::NOT && lemma[i][0] == utils::mkFalse()) + if (lit.getKind() == kind::NOT && lit[0] == utils::mkFalse()) { Debug("pf::bv") << "Lemma has a (not false) literal" << std::endl; os << "(clausify_false "; - os << ProofManager::getLitName(lemma[i]); + os << ProofManager::getLitName(lit); os << ")"; return; } diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h index d9c959ae4..8c65d42e7 100644 --- a/src/proof/sat_proof_implementation.h +++ b/src/proof/sat_proof_implementation.h @@ -285,8 +285,8 @@ bool TSatProof<Solver>::checkResolution(ClauseId id) { typename Solver::TLit var = steps[i].lit; LitSet clause2; createLitSet(steps[i].id, clause2); - bool res = resolve<Solver>(var, clause1, clause2, steps[i].sign); - if (res == false) { + if (!resolve<Solver>(var, clause1, clause2, steps[i].sign)) + { validRes = false; break; } diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index 7e2ed84b1..e746a6315 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -1026,7 +1026,7 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term, for (unsigned i = 0; i < term.getNumChildren(); ++i) { for (unsigned j = i + 1; j < term.getNumChildren(); ++j) { - TypeNode armType = equalityType(term[i], term[j]); + armType = equalityType(term[i], term[j]); if ((i != 0) || (j != 1)) { os << "(not (= "; printSort(term[0].getType(), os); diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp index 214198756..225cb6aa4 100644 --- a/src/proof/uf_proof.cpp +++ b/src/proof/uf_proof.cpp @@ -337,7 +337,6 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, Node n1 = toStreamRecLFSC(ss, tp, *(pf.d_children[0]), tb + 1, map); Debug("pf::uf") << "\ndoing trans proof, got n1 " << n1 << "\n"; - Node n2; if(tb == 1) { Debug("pf::uf") << "\ntrans proof[0], got n1 " << n1 << "\n"; } @@ -349,7 +348,6 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, toStreamRecLFSC(dontCare, tp, *(pf.d_children[0]), tb + 1, map); std::map<size_t, Node> childToStream; - std::stringstream ss1(ss.str()), ss2; std::pair<Node, Node> nodePair; for(size_t i = 1; i < pf.d_children.size(); ++i) { std::stringstream ss1(ss.str()), ss2; @@ -410,9 +408,9 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, while (j < pf.d_children.size() && !sequenceOver) { - std::stringstream dontCare; - nodeAfterEqualitySequence = toStreamRecLFSC( - dontCare, tp, *(pf.d_children[j]), tb + 1, map); + std::stringstream ignore; + nodeAfterEqualitySequence = + toStreamRecLFSC(ignore, tp, *(pf.d_children[j]), tb + 1, map); if (((nodeAfterEqualitySequence[0] == n1[0]) && (nodeAfterEqualitySequence[1] == n1[1])) diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc index 25b6a3da2..84ab62fd8 100644 --- a/src/prop/bvminisat/core/Solver.cc +++ b/src/prop/bvminisat/core/Solver.cc @@ -86,70 +86,92 @@ CRef Solver::TCRef_Lazy = CRef_Undef - 1; // no real lazy ref here //================================================================================================= // Constructor/Destructor: - -Solver::Solver(CVC4::context::Context* c) : - - // Parameters (user settable): - // - d_notify(nullptr) - , c(c) - , verbosity (0) - , var_decay (opt_var_decay) - , clause_decay (opt_clause_decay) - , random_var_freq (opt_random_var_freq) - , random_seed (opt_random_seed) - , luby_restart (opt_luby_restart) - , ccmin_mode (opt_ccmin_mode) - , phase_saving (opt_phase_saving) - , rnd_pol (false) - , rnd_init_act (opt_rnd_init_act) - , garbage_frac (opt_garbage_frac) - , restart_first (opt_restart_first) - , restart_inc (opt_restart_inc) - - // Parameters (the rest): - // - , learntsize_factor((double)1/(double)3), learntsize_inc(1.5) - - // Parameters (experimental): - // - , learntsize_adjust_start_confl (100) - , learntsize_adjust_inc (1.5) - - // Statistics: (formerly in 'SolverStats') - // - , solves(0), starts(0), decisions(0), rnd_decisions(0), propagations(0), conflicts(0) - , dec_vars(0), clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0) - - , need_to_propagate(false) - , only_bcp(false) - , clause_added(false) - , ok (true) - , cla_inc (1) - , var_inc (1) - , watches (WatcherDeleted(ca)) - , qhead (0) - , simpDB_assigns (-1) - , simpDB_props (0) - , order_heap (VarOrderLt(activity)) - , progress_estimate (0) - , remove_satisfied (true) - - , ca () - - // even though these are temporaries and technically should be set - // before calling, lets initialize them. this will reduces chances of - // non-determinism in portfolio (parallel) solver if variables are - // being (incorrectly) used without initialization. - , seen(), analyze_stack(), analyze_toclear(), add_tmp() - , max_learnts(0.0), learntsize_adjust_confl(0.0), learntsize_adjust_cnt(0) - - // Resource constraints: - // - , conflict_budget (-1) - , propagation_budget (-1) - , asynch_interrupt (false) - , d_bvp (NULL) +Solver::Solver(CVC4::context::Context* context) + : + + // Parameters (user settable): + // + d_notify(nullptr), + c(context), + verbosity(0), + var_decay(opt_var_decay), + clause_decay(opt_clause_decay), + random_var_freq(opt_random_var_freq), + random_seed(opt_random_seed), + luby_restart(opt_luby_restart), + ccmin_mode(opt_ccmin_mode), + phase_saving(opt_phase_saving), + rnd_pol(false), + rnd_init_act(opt_rnd_init_act), + garbage_frac(opt_garbage_frac), + restart_first(opt_restart_first), + restart_inc(opt_restart_inc) + + // Parameters (the rest): + // + , + learntsize_factor((double)1 / (double)3), + learntsize_inc(1.5) + + // Parameters (experimental): + // + , + learntsize_adjust_start_confl(100), + learntsize_adjust_inc(1.5) + + // Statistics: (formerly in 'SolverStats') + // + , + solves(0), + starts(0), + decisions(0), + rnd_decisions(0), + propagations(0), + conflicts(0), + dec_vars(0), + clauses_literals(0), + learnts_literals(0), + max_literals(0), + tot_literals(0) + + , + need_to_propagate(false), + only_bcp(false), + clause_added(false), + ok(true), + cla_inc(1), + var_inc(1), + watches(WatcherDeleted(ca)), + qhead(0), + simpDB_assigns(-1), + simpDB_props(0), + order_heap(VarOrderLt(activity)), + progress_estimate(0), + remove_satisfied(true) + + , + ca() + + // even though these are temporaries and technically should be set + // before calling, lets initialize them. this will reduces chances of + // non-determinism in portfolio (parallel) solver if variables are + // being (incorrectly) used without initialization. + , + seen(), + analyze_stack(), + analyze_toclear(), + add_tmp(), + max_learnts(0.0), + learntsize_adjust_confl(0.0), + learntsize_adjust_cnt(0) + + // Resource constraints: + // + , + conflict_budget(-1), + propagation_budget(-1), + asynch_interrupt(false), + d_bvp(NULL) { // Create the constant variables varTrue = newVar(true, false); @@ -304,65 +326,73 @@ bool Solver::addClause_(vec<Lit>& ps, ClauseId& id) } void Solver::attachClause(CRef cr) { - const Clause& c = ca[cr]; - assert(c.size() > 1); - watches[~c[0]].push(Watcher(cr, c[1])); - watches[~c[1]].push(Watcher(cr, c[0])); - if (c.learnt()) learnts_literals += c.size(); - else clauses_literals += c.size(); } - + const Clause& clause = ca[cr]; + assert(clause.size() > 1); + watches[~clause[0]].push(Watcher(cr, clause[1])); + watches[~clause[1]].push(Watcher(cr, clause[0])); + if (clause.learnt()) + learnts_literals += clause.size(); + else + clauses_literals += clause.size(); +} void Solver::detachClause(CRef cr, bool strict) { - const Clause& c = ca[cr]; - if(d_bvp){ d_bvp->getSatProof()->markDeleted(cr); } - - assert(c.size() > 1); - - if (strict){ - remove(watches[~c[0]], Watcher(cr, c[1])); - remove(watches[~c[1]], Watcher(cr, c[0])); + const Clause& clause = ca[cr]; + if (d_bvp) + { + d_bvp->getSatProof()->markDeleted(cr); } + + assert(clause.size() > 1); + + if (strict) + { + remove(watches[~clause[0]], Watcher(cr, clause[1])); + remove(watches[~clause[1]], Watcher(cr, clause[0])); }else{ // Lazy detaching: (NOTE! Must clean all watcher lists before garbage collecting this clause) - watches.smudge(~c[0]); - watches.smudge(~c[1]); + watches.smudge(~clause[0]); + watches.smudge(~clause[1]); } - if (c.learnt()) learnts_literals -= c.size(); - else clauses_literals -= c.size(); } - + if (clause.learnt()) + learnts_literals -= clause.size(); + else + clauses_literals -= clause.size(); +} void Solver::removeClause(CRef cr) { - Clause& c = ca[cr]; - detachClause(cr); - // Don't leave pointers to free'd memory! - if (locked(c)) vardata[var(c[0])].reason = CRef_Undef; - c.mark(1); - ca.free(cr); + Clause& clause = ca[cr]; + detachClause(cr); + // Don't leave pointers to free'd memory! + if (locked(clause)) vardata[var(clause[0])].reason = CRef_Undef; + clause.mark(1); + ca.free(cr); } - -bool Solver::satisfied(const Clause& c) const { - for (int i = 0; i < c.size(); i++) - if (value(c[i]) == l_True) - return true; - return false; } - +bool Solver::satisfied(const Clause& clause) const +{ + for (int i = 0; i < clause.size(); i++) + if (value(clause[i]) == l_True) return true; + return false; +} // Revert to the state at given level (keeping all assignment at 'level' but not beyond). // void Solver::cancelUntil(int level) { if (decisionLevel() > level){ Debug("bvminisat::explain") << OUTPUT_TAG << " backtracking to " << level << std::endl; - for (int c = trail.size()-1; c >= trail_lim[level]; c--){ - Var x = var(trail[c]); - assigns [x] = l_Undef; - if (marker[x] == 2) marker[x] = 1; - if (phase_saving > 1 - || ((phase_saving == 1) && c > trail_lim.last())) - { - polarity[x] = sign(trail[c]); - } - insertVarOrder(x); } + for (int clause = trail.size() - 1; clause >= trail_lim[level]; clause--) + { + Var x = var(trail[clause]); + assigns[x] = l_Undef; + if (marker[x] == 2) marker[x] = 1; + if (phase_saving > 1 + || ((phase_saving == 1) && clause > trail_lim.last())) + { + polarity[x] = sign(trail[clause]); + } + insertVarOrder(x); + } qhead = trail_lim[level]; trail.shrink(trail.size() - trail_lim[level]); trail_lim.shrink(trail_lim.size() - level); @@ -429,28 +459,33 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip do{ assert(confl != CRef_Undef); // (otherwise should be UIP) - Clause& c = ca[confl]; - - if (c.learnt()) - claBumpActivity(c); - - for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++){ - Lit q = c[j]; + Clause& clause = ca[confl]; + + if (clause.learnt()) claBumpActivity(clause); + + for (int j = (p == lit_Undef) ? 0 : 1; j < clause.size(); j++) + { + Lit q = clause[j]; + + if (!seen[var(q)] && level(var(q)) > 0) + { + varBumpActivity(var(q)); + seen[var(q)] = 1; + if (level(var(q)) >= decisionLevel()) + pathC++; + else + out_learnt.push(q); + } - if (!seen[var(q)] && level(var(q)) > 0) { - varBumpActivity(var(q)); - seen[var(q)] = 1; - if (level(var(q)) >= decisionLevel()) - pathC++; - else - out_learnt.push(q); - } - - if (level(var(q)) == 0) { - if(d_bvp){ d_bvp->getSatProof()->resolveOutUnit(q); } + if (level(var(q)) == 0) + { + if (d_bvp) + { + d_bvp->getSatProof()->resolveOutUnit(q); } + } } - + // Select next clause to look at: while (!seen[var(trail[index--])]); p = trail[index+1]; @@ -478,51 +513,68 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip // Simplify conflict clause: // - int i, j; + int i1, j; out_learnt.copyTo(analyze_toclear); if (ccmin_mode == 2){ uint32_t abstract_level = 0; - for (i = 1; i < out_learnt.size(); i++) - abstract_level |= abstractLevel(var(out_learnt[i])); // (maintain an abstraction of levels involved in conflict) - - for (i = j = 1; i < out_learnt.size(); i++) { - if (reason(var(out_learnt[i])) == CRef_Undef) { - out_learnt[j++] = out_learnt[i]; - } else { - // Check if the literal is redundant - if (!litRedundant(out_learnt[i], abstract_level)) { - // Literal is not redundant - out_learnt[j++] = out_learnt[i]; - } else { - if(d_bvp){ d_bvp->getSatProof()->storeLitRedundant(out_learnt[i]); } + for (i1 = 1; i1 < out_learnt.size(); i1++) + abstract_level |= abstractLevel( + var(out_learnt[i1])); // (maintain an abstraction of levels + // involved in conflict) + + for (i1 = j = 1; i1 < out_learnt.size(); i1++) + { + if (reason(var(out_learnt[i1])) == CRef_Undef) + { + out_learnt[j++] = out_learnt[i1]; + } + else + { + // Check if the literal is redundant + if (!litRedundant(out_learnt[i1], abstract_level)) + { + // Literal is not redundant + out_learnt[j++] = out_learnt[i1]; + } + else + { + if (d_bvp) + { + d_bvp->getSatProof()->storeLitRedundant(out_learnt[i1]); } } + } } - }else if (ccmin_mode == 1){ Unreachable(); - for (i = j = 1; i < out_learnt.size(); i++){ - Var x = var(out_learnt[i]); - - if (reason(x) == CRef_Undef) - out_learnt[j++] = out_learnt[i]; - else{ - Clause& c = ca[reason(var(out_learnt[i]))]; - for (int k = 1; k < c.size(); k++) - if (!seen[var(c[k])] && level(var(c[k])) > 0){ - out_learnt[j++] = out_learnt[i]; - break; } - } + for (i1 = j = 1; i1 < out_learnt.size(); i1++) + { + Var x = var(out_learnt[i1]); + + if (reason(x) == CRef_Undef) + out_learnt[j++] = out_learnt[i1]; + else + { + Clause& clause = ca[reason(var(out_learnt[i1]))]; + for (int k = 1; k < clause.size(); k++) + if (!seen[var(clause[k])] && level(var(clause[k])) > 0) + { + out_learnt[j++] = out_learnt[i1]; + break; + } + } } }else - i = j = out_learnt.size(); + i1 = j = out_learnt.size(); max_literals += out_learnt.size(); - out_learnt.shrink(i - j); + out_learnt.shrink(i1 - j); tot_literals += out_learnt.size(); - for (int i = 0; i < out_learnt.size(); ++ i) { - if (marker[var(out_learnt[i])] == 0) { + for (int i2 = 0; i2 < out_learnt.size(); ++i2) + { + if (marker[var(out_learnt[i2])] == 0) + { break; } } @@ -535,17 +587,18 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip else{ int max_i = 1; // Find the first literal assigned at the next-highest level: - for (int i = 2; i < out_learnt.size(); i++) - if (level(var(out_learnt[i])) > level(var(out_learnt[max_i]))) - max_i = i; - // Swap-in this literal at index 1: - Lit p = out_learnt[max_i]; + for (int i3 = 2; i3 < out_learnt.size(); i3++) + if (level(var(out_learnt[i3])) > level(var(out_learnt[max_i]))) + max_i = i3; + // Swap-in this literal at i1 1: + Lit p2 = out_learnt[max_i]; out_learnt[max_i] = out_learnt[1]; - out_learnt[1] = p; - out_btlevel = level(var(p)); + out_learnt[1] = p2; + out_btlevel = level(var(p2)); } - for (int j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0; // ('seen[]' is now cleared) + for (int j2 = 0; j2 < analyze_toclear.size(); j2++) + seen[var(analyze_toclear[j2])] = 0; // ('seen[]' is now cleared) } @@ -558,24 +611,29 @@ bool Solver::litRedundant(Lit p, uint32_t abstract_levels) while (analyze_stack.size() > 0){ CRef c_reason = reason(var(analyze_stack.last())); assert(c_reason != CRef_Undef); - Clause& c = ca[c_reason]; - int c_size = c.size(); + Clause& clause = ca[c_reason]; + int c_size = clause.size(); analyze_stack.pop(); for (int i = 1; i < c_size; i++){ - Lit p = c[i]; - if (!seen[var(p)] && level(var(p)) > 0){ - if (reason(var(p)) != CRef_Undef && (abstractLevel(var(p)) & abstract_levels) != 0){ - seen[var(p)] = 1; - analyze_stack.push(p); - analyze_toclear.push(p); - }else{ - for (int j = top; j < analyze_toclear.size(); j++) - seen[var(analyze_toclear[j])] = 0; - analyze_toclear.shrink(analyze_toclear.size() - top); - return false; - } + Lit p2 = clause[i]; + if (!seen[var(p2)] && level(var(p2)) > 0) + { + if (reason(var(p2)) != CRef_Undef + && (abstractLevel(var(p2)) & abstract_levels) != 0) + { + seen[var(p2)] = 1; + analyze_stack.push(p2); + analyze_toclear.push(p2); + } + else + { + for (int j = top; j < analyze_toclear.size(); j++) + seen[var(analyze_toclear[j])] = 0; + analyze_toclear.shrink(analyze_toclear.size() - top); + return false; } + } } } @@ -619,16 +677,18 @@ void Solver::analyzeFinal2(Lit p, CRef confl_clause, vec<Lit>& out_conflict) { if(d_bvp){d_bvp->getSatProof()->resolveOutUnit(~p);} } } else { - Clause& c = ca[reason(x)]; + Clause& clause = ca[reason(x)]; if(d_bvp){d_bvp->getSatProof()->addResolutionStep(trail[i],reason(x), sign(trail[i]));} - for (int j = 1; j < c.size(); j++) { - if (level(var(c[j])) > 0) - seen[var(c[j])] = 1; + for (int j = 1; j < clause.size(); j++) + { + if (level(var(clause[j])) > 0) seen[var(clause[j])] = 1; if(d_bvp){ - if (level(var(c[j])) == 0) { - d_bvp->getSatProof()->resolveOutUnit(c[j]); - seen[var(c[j])] = 0; // we don't need to resolve it out again + if (level(var(clause[j])) == 0) + { + d_bvp->getSatProof()->resolveOutUnit(clause[j]); + seen[var(clause[j])] = + 0; // we don't need to resolve it out again } } } @@ -683,7 +743,7 @@ void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict) out_conflict.push(~trail[i]); } } else { - Clause& c = ca[reason(x)]; + Clause& clause = ca[reason(x)]; if(d_bvp){ if (d_bvp->isAssumptionConflict() && trail[i] == p) { @@ -692,13 +752,16 @@ void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict) d_bvp->getSatProof()->addResolutionStep(trail[i], reason(x), sign(trail[i])); } } - for (int j = 1; j < c.size(); j++) { - if (level(var(c[j])) > 0) { - seen[var(c[j])] = 1; + for (int j = 1; j < clause.size(); j++) + { + if (level(var(clause[j])) > 0) + { + seen[var(clause[j])] = 1; } if(d_bvp){ - if (level(var(c[j])) == 0) { - d_bvp->getSatProof()->resolveOutUnit(c[j]); + if (level(var(clause[j])) == 0) + { + d_bvp->getSatProof()->resolveOutUnit(clause[j]); } } } @@ -813,25 +876,28 @@ CRef Solver::propagate() // Make sure the false literal is data[1]: CRef cr = i->cref; - Clause& c = ca[cr]; + Clause& clause = ca[cr]; Lit false_lit = ~p; - if (c[0] == false_lit) - c[0] = c[1], c[1] = false_lit; - assert(c[1] == false_lit); + if (clause[0] == false_lit) + clause[0] = clause[1], clause[1] = false_lit; + assert(clause[1] == false_lit); i++; // If 0th watch is true, then clause is already satisfied. - Lit first = c[0]; + Lit first = clause[0]; Watcher w = Watcher(cr, first); if (first != blocker && value(first) == l_True){ *j++ = w; continue; } // Look for new watch: - for (int k = 2; k < c.size(); k++) - if (value(c[k]) != l_False){ - c[1] = c[k]; c[k] = false_lit; - watches[~c[1]].push(w); - goto NextClause; } + for (int k = 2; k < clause.size(); k++) + if (value(clause[k]) != l_False) + { + clause[1] = clause[k]; + clause[k] = false_lit; + watches[~clause[1]].push(w); + goto NextClause; + } // Did not find watch -- clause is unit under assignment: *j++ = w; @@ -878,11 +944,12 @@ void Solver::reduceDB() // Don't delete binary or locked clauses. From the rest, delete clauses from the first half // and clauses with activity smaller than 'extra_lim': for (i = j = 0; i < learnts.size(); i++){ - Clause& c = ca[learnts[i]]; - if (c.size() > 2 && !locked(c) && (i < learnts.size() / 2 || c.activity() < extra_lim)) - removeClause(learnts[i]); - else - learnts[j++] = learnts[i]; + Clause& clause = ca[learnts[i]]; + if (clause.size() > 2 && !locked(clause) + && (i < learnts.size() / 2 || clause.activity() < extra_lim)) + removeClause(learnts[i]); + else + learnts[j++] = learnts[i]; } learnts.shrink(i - j); checkGarbage(); @@ -893,14 +960,19 @@ void Solver::removeSatisfied(vec<CRef>& cs) { int i, j; for (i = j = 0; i < cs.size(); i++){ - Clause& c = ca[cs[i]]; - if (satisfied(c)) { - if (locked(c)) { - // store a resolution of the literal c propagated - if(d_bvp){ d_bvp->getSatProof()->storeUnitResolution(c[0]); } + Clause& clause = ca[cs[i]]; + if (satisfied(clause)) + { + if (locked(clause)) + { + // store a resolution of the literal clause propagated + if (d_bvp) + { + d_bvp->getSatProof()->storeUnitResolution(clause[0]); } - removeClause(cs[i]); } + removeClause(cs[i]); + } else cs[j++] = cs[i]; } @@ -1290,7 +1362,7 @@ void Solver::explain(Lit p, std::vector<Lit>& explanation) { } } else { - Clause& c = ca[reason(x)]; + Clause& clause = ca[reason(x)]; if(d_bvp){ if (p == trail[i]) { d_bvp->startBVConflict(reason(var(p))); @@ -1298,9 +1370,11 @@ void Solver::explain(Lit p, std::vector<Lit>& explanation) { d_bvp->getSatProof()->addResolutionStep(trail[i], reason(x), sign(trail[i])); } } - for (int j = 1; j < c.size(); j++) { - if (level(var(c[j])) > 0 || options::proof()) { - seen[var(c[j])] = 1; + for (int j = 1; j < clause.size(); j++) + { + if (level(var(clause[j])) > 0 || options::proof()) + { + seen[var(clause[j])] = 1; } } } @@ -1341,15 +1415,17 @@ static Var mapVar(Var x, vec<Var>& map, Var& max) return map[x]; } - -void Solver::toDimacs(FILE* f, Clause& c, vec<Var>& map, Var& max) +void Solver::toDimacs(FILE* f, Clause& clause, vec<Var>& map, Var& max) { - if (satisfied(c)) return; - - for (int i = 0; i < c.size(); i++) - if (value(c[i]) != l_False) - fprintf(f, "%s%d ", sign(c[i]) ? "-" : "", mapVar(var(c[i]), map, max)+1); - fprintf(f, "0\n"); + if (satisfied(clause)) return; + + for (int i = 0; i < clause.size(); i++) + if (value(clause[i]) != l_False) + fprintf(f, + "%s%d ", + sign(clause[i]) ? "-" : "", + mapVar(var(clause[i]), map, max) + 1); + fprintf(f, "0\n"); } @@ -1381,10 +1457,9 @@ void Solver::toDimacs(FILE* f, const vec<Lit>& assumps) for (int i = 0; i < clauses.size(); i++) if (!satisfied(ca[clauses[i]])){ - Clause& c = ca[clauses[i]]; - for (int j = 0; j < c.size(); j++) - if (value(c[j]) != l_False) - mapVar(var(c[j]), map, max); + Clause& clause = ca[clauses[i]]; + for (int j = 0; j < clause.size(); j++) + if (value(clause[j]) != l_False) mapVar(var(clause[j]), map, max); } // Assumptions are added as unit clauses: diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h index 2197d030f..7fad72d6d 100644 --- a/src/prop/bvminisat/core/Solver.h +++ b/src/prop/bvminisat/core/Solver.h @@ -365,11 +365,11 @@ public: // Less than for literals in an added clause when proofs are on. struct assign_lt { - Solver& solver; - assign_lt(Solver& solver) : solver(solver) {} + Solver& d_solver; + assign_lt(Solver& solver) : d_solver(solver) {} bool operator () (Lit x, Lit y) { - lbool x_value = solver.value(x); - lbool y_value = solver.value(y); + lbool x_value = d_solver.value(x); + lbool y_value = d_solver.value(y); // Two unassigned literals are sorted arbitrarily if (x_value == l_Undef && y_value == l_Undef) { return x < y; @@ -379,7 +379,7 @@ public: if (y_value == l_Undef) return false; // Literals of the same value are sorted by decreasing levels if (x_value == y_value) { - return solver.level(var(x)) > solver.level(var(y)); + return d_solver.level(var(x)) > d_solver.level(var(y)); } else { // True literals go up front if (x_value == l_True) { @@ -417,12 +417,15 @@ inline void Solver::varBumpActivity(Var v, double inc) { order_heap.decrease(v); } inline void Solver::claDecayActivity() { cla_inc *= (1 / clause_decay); } -inline void Solver::claBumpActivity (Clause& c) { - if ( (c.activity() += cla_inc) > 1e20 ) { - // Rescale: - for (int i = 0; i < learnts.size(); i++) - ca[learnts[i]].activity() *= 1e-20; - cla_inc *= 1e-20; } } +inline void Solver::claBumpActivity(Clause& clause) +{ + if ((clause.activity() += cla_inc) > 1e20) + { + // Rescale: + for (int i = 0; i < learnts.size(); i++) ca[learnts[i]].activity() *= 1e-20; + cla_inc *= 1e-20; + } +} inline void Solver::checkGarbage(void){ return checkGarbage(garbage_frac); } inline void Solver::checkGarbage(double gf){ @@ -436,7 +439,11 @@ inline bool Solver::addEmptyClause () { add_tmp.clear( inline bool Solver::addClause (Lit p, ClauseId& id) { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, id); } inline bool Solver::addClause (Lit p, Lit q, ClauseId& id) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, id); } inline bool Solver::addClause (Lit p, Lit q, Lit r, ClauseId& id) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, id); } -inline bool Solver::locked (const Clause& c) const { return value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && ca.lea(reason(var(c[0]))) == &c; } +inline bool Solver::locked(const Clause& clause) const +{ + return value(clause[0]) == l_True && reason(var(clause[0])) != CRef_Undef + && ca.lea(reason(var(clause[0]))) == &clause; +} inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); } inline int Solver::decisionLevel () const { return trail_lim.size(); } diff --git a/src/prop/bvminisat/simp/SimpSolver.cc b/src/prop/bvminisat/simp/SimpSolver.cc index 9e50433ef..b003342c6 100644 --- a/src/prop/bvminisat/simp/SimpSolver.cc +++ b/src/prop/bvminisat/simp/SimpSolver.cc @@ -48,8 +48,8 @@ static DoubleOption opt_simp_garbage_frac(_cat, "simp-gc-frac", "The fraction of //================================================================================================= // Constructor/Destructor: -SimpSolver::SimpSolver(CVC4::context::Context* c) - : Solver(c), +SimpSolver::SimpSolver(CVC4::context::Context* context) + : Solver(context), grow(opt_grow), clause_lim(opt_clause_lim), subsumption_lim(opt_subsumption_lim), @@ -181,7 +181,7 @@ bool SimpSolver::addClause_(vec<Lit>& ps, ClauseId& id) if (use_simplification && clauses.size() == nclauses + 1){ CRef cr = clauses.last(); - const Clause& c = ca[cr]; + const Clause& clause = ca[cr]; // NOTE: the clause is added to the queue immediately and then // again during 'gatherTouchedClauses()'. If nothing happens @@ -190,13 +190,14 @@ bool SimpSolver::addClause_(vec<Lit>& ps, ClauseId& id) // consequence of how backward subsumption is used to mimic // forward subsumption. subsumption_queue.insert(cr); - for (int i = 0; i < c.size(); i++){ - occurs[var(c[i])].push(cr); - n_occ[toInt(c[i])]++; - touched[var(c[i])] = 1; - n_touched++; - if (elim_heap.inHeap(var(c[i]))) - elim_heap.increase(var(c[i])); + for (int i = 0; i < clause.size(); i++) + { + occurs[var(clause[i])].push(cr); + n_occ[toInt(clause[i])]++; + touched[var(clause[i])] = 1; + n_touched++; + if (elim_heap.inHeap(var(clause[i]))) + elim_heap.increase(var(clause[i])); } } @@ -206,14 +207,15 @@ bool SimpSolver::addClause_(vec<Lit>& ps, ClauseId& id) void SimpSolver::removeClause(CRef cr) { - const Clause& c = ca[cr]; + const Clause& clause = ca[cr]; - if (use_simplification) - for (int i = 0; i < c.size(); i++){ - n_occ[toInt(c[i])]--; - updateElimHeap(var(c[i])); - occurs.smudge(var(c[i])); - } + if (use_simplification) + for (int i = 0; i < clause.size(); i++) + { + n_occ[toInt(clause[i])]--; + updateElimHeap(var(clause[i])); + occurs.smudge(var(clause[i])); + } Solver::removeClause(cr); } @@ -221,27 +223,31 @@ void SimpSolver::removeClause(CRef cr) bool SimpSolver::strengthenClause(CRef cr, Lit l) { - Clause& c = ca[cr]; - assert(decisionLevel() == 0); - assert(use_simplification); - - // FIX: this is too inefficient but would be nice to have (properly implemented) - // if (!find(subsumption_queue, &c)) - subsumption_queue.insert(cr); - - if (c.size() == 2){ - removeClause(cr); - c.strengthen(l); - }else{ - detachClause(cr, true); - c.strengthen(l); - attachClause(cr); - remove(occurs[var(l)], cr); - n_occ[toInt(l)]--; - updateElimHeap(var(l)); - } - - return c.size() == 1 ? enqueue(c[0]) && propagate() == CRef_Undef : true; + Clause& clause = ca[cr]; + assert(decisionLevel() == 0); + assert(use_simplification); + + // FIX: this is too inefficient but would be nice to have (properly + // implemented) if (!find(subsumption_queue, &clause)) + subsumption_queue.insert(cr); + + if (clause.size() == 2) + { + removeClause(cr); + clause.strengthen(l); + } + else + { + detachClause(cr, true); + clause.strengthen(l); + attachClause(cr); + remove(occurs[var(l)], cr); + n_occ[toInt(l)]--; + updateElimHeap(var(l)); + } + + return clause.size() == 1 ? enqueue(clause[0]) && propagate() == CRef_Undef + : true; } @@ -345,20 +351,22 @@ void SimpSolver::gatherTouchedClauses() n_touched = 0; } - -bool SimpSolver::implied(const vec<Lit>& c) +bool SimpSolver::implied(const vec<Lit>& clause) { assert(decisionLevel() == 0); trail_lim.push(trail.size()); - for (int i = 0; i < c.size(); i++) - if (value(c[i]) == l_True){ - cancelUntil(0); - return false; - }else if (value(c[i]) != l_False){ - assert(value(c[i]) == l_Undef); - uncheckedEnqueue(~c[i]); - } + for (int i = 0; i < clause.size(); i++) + if (value(clause[i]) == l_True) + { + cancelUntil(0); + return false; + } + else if (value(clause[i]) != l_False) + { + assert(value(clause[i]) == l_Undef); + uncheckedEnqueue(~clause[i]); + } bool result = propagate() != CRef_Undef; cancelUntil(0); @@ -390,44 +398,49 @@ bool SimpSolver::backwardSubsumptionCheck(bool verbose) subsumption_queue.insert(bwdsub_tmpunit); } CRef cr = subsumption_queue.peek(); subsumption_queue.pop(); - Clause& c = ca[cr]; + Clause& clause = ca[cr]; - if (c.mark()) continue; + if (clause.mark()) continue; if (verbose && verbosity >= 2 && cnt++ % 1000 == 0) printf("subsumption left: %10d (%10d subsumed, %10d deleted literals)\r", subsumption_queue.size(), subsumed, deleted_literals); - assert(c.size() > 1 || value(c[0]) == l_True); // Unit-clauses should have been propagated before this point. + assert(clause.size() > 1 + || value(clause[0]) == l_True); // Unit-clauses should have been + // propagated before this point. // Find best variable to scan: - Var best = var(c[0]); - for (int i = 1; i < c.size(); i++) - if (occurs[var(c[i])].size() < occurs[best].size()) - best = var(c[i]); + Var best = var(clause[0]); + for (int i = 1; i < clause.size(); i++) + if (occurs[var(clause[i])].size() < occurs[best].size()) + best = var(clause[i]); // Search all candidates: vec<CRef>& _cs = occurs.lookup(best); CRef* cs = (CRef*)_cs; for (int j = 0; j < _cs.size(); j++) - if (c.mark()) - break; - else if (!ca[cs[j]].mark() && cs[j] != cr && (subsumption_lim == -1 || ca[cs[j]].size() < subsumption_lim)){ - Lit l = c.subsumes(ca[cs[j]]); - - if (l == lit_Undef) - subsumed++, removeClause(cs[j]); - else if (l != lit_Error){ - deleted_literals++; - - if (!strengthenClause(cs[j], ~l)) - return false; - - // Did current candidate get deleted from cs? Then check candidate at index j again: - if (var(l) == best) - j--; - } + if (clause.mark()) + break; + else if (!ca[cs[j]].mark() && cs[j] != cr + && (subsumption_lim == -1 + || ca[cs[j]].size() < subsumption_lim)) + { + Lit l = clause.subsumes(ca[cs[j]]); + + if (l == lit_Undef) + subsumed++, removeClause(cs[j]); + else if (l != lit_Error) + { + deleted_literals++; + + if (!strengthenClause(cs[j], ~l)) return false; + + // Did current candidate get deleted from cs? Then check candidate + // at index j again: + if (var(l) == best) j--; } + } } return true; @@ -436,28 +449,29 @@ bool SimpSolver::backwardSubsumptionCheck(bool verbose) bool SimpSolver::asymm(Var v, CRef cr) { - Clause& c = ca[cr]; - assert(decisionLevel() == 0); + Clause& clause = ca[cr]; + assert(decisionLevel() == 0); - if (c.mark() || satisfied(c)) return true; + if (clause.mark() || satisfied(clause)) return true; - trail_lim.push(trail.size()); - Lit l = lit_Undef; - for (int i = 0; i < c.size(); i++) - if (var(c[i]) != v && value(c[i]) != l_False) - uncheckedEnqueue(~c[i]); - else - l = c[i]; - - if (propagate() != CRef_Undef){ - cancelUntil(0); - asymm_lits++; - if (!strengthenClause(cr, l)) - return false; - }else - cancelUntil(0); + trail_lim.push(trail.size()); + Lit l = lit_Undef; + for (int i = 0; i < clause.size(); i++) + if (var(clause[i]) != v && value(clause[i]) != l_False) + uncheckedEnqueue(~clause[i]); + else + l = clause[i]; - return true; + if (propagate() != CRef_Undef) + { + cancelUntil(0); + asymm_lits++; + if (!strengthenClause(cr, l)) return false; + } + else + cancelUntil(0); + + return true; } @@ -484,18 +498,17 @@ static void mkElimClause(vec<uint32_t>& elimclauses, Lit x) elimclauses.push(1); } - -static void mkElimClause(vec<uint32_t>& elimclauses, Var v, Clause& c) +static void mkElimClause(vec<uint32_t>& elimclauses, Var v, Clause& clause) { int first = elimclauses.size(); int v_pos = -1; // Copy clause to elimclauses-vector. Remember position where the // variable 'v' occurs: - for (int i = 0; i < c.size(); i++){ - elimclauses.push(toInt(c[i])); - if (var(c[i]) == v) - v_pos = i + first; + for (int i = 0; i < clause.size(); i++) + { + elimclauses.push(toInt(clause[i])); + if (var(clause[i]) == v) v_pos = i + first; } assert(v_pos != -1); @@ -506,7 +519,7 @@ static void mkElimClause(vec<uint32_t>& elimclauses, Var v, Clause& c) elimclauses[first] = tmp; // Store the length of the clause last: - elimclauses.push(c.size()); + elimclauses.push(clause.size()); } @@ -590,13 +603,14 @@ bool SimpSolver::substitute(Var v, Lit x) vec<Lit>& subst_clause = add_tmp; for (int i = 0; i < cls.size(); i++){ - Clause& c = ca[cls[i]]; + Clause& clause = ca[cls[i]]; - subst_clause.clear(); - for (int j = 0; j < c.size(); j++){ - Lit p = c[j]; - subst_clause.push(var(p) == v ? x ^ sign(p) : p); - } + subst_clause.clear(); + for (int j = 0; j < clause.size(); j++) + { + Lit p = clause[j]; + subst_clause.push(var(p) == v ? x ^ sign(p) : p); + } removeClause(cls[i]); ClauseId id; diff --git a/src/prop/bvminisat/simp/SimpSolver.h b/src/prop/bvminisat/simp/SimpSolver.h index 246bb7152..9d3a51c02 100644 --- a/src/prop/bvminisat/simp/SimpSolver.h +++ b/src/prop/bvminisat/simp/SimpSolver.h @@ -37,42 +37,55 @@ class SimpSolver : public Solver { public: // Constructor/Destructor: // - SimpSolver(CVC4::context::Context* c); - ~SimpSolver(); - - // Problem specification: - // - Var newVar (bool polarity = true, bool dvar = true, bool freeze = false); - bool addClause (const vec<Lit>& ps, ClauseId& id); - bool addEmptyClause(); // Add the empty clause to the solver. - bool addClause (Lit p, ClauseId& id); // Add a unit clause to the solver. - bool addClause (Lit p, Lit q, ClauseId& id); // Add a binary clause to the solver. - bool addClause (Lit p, Lit q, Lit r, ClauseId& id); // Add a ternary clause to the solver. - bool addClause_( vec<Lit>& ps, ClauseId& id); - bool substitute(Var v, Lit x); // Replace all occurences of v with x (may cause a contradiction). - - // Variable mode: - // - void setFrozen (Var v, bool b); // If a variable is frozen it will not be eliminated. - bool isEliminated(Var v) const; - - // Solving: - // - lbool solve (const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false); - lbool solveLimited(const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false); - lbool solveLimited(bool do_simp = true, bool turn_off_simp = false); - lbool solve ( bool do_simp = true, bool turn_off_simp = false); - lbool solve (Lit p , bool do_simp = true, bool turn_off_simp = false); - lbool solve (Lit p, Lit q, bool do_simp = true, bool turn_off_simp = false); - lbool solve (Lit p, Lit q, Lit r, bool do_simp = true, bool turn_off_simp = false); - bool eliminate (bool turn_off_elim = false); // Perform variable elimination based simplification. - - // Memory managment: - // - void garbageCollect() override; - - // Generate a (possibly simplified) DIMACS file: - // + SimpSolver(CVC4::context::Context* context); + ~SimpSolver(); + + // Problem specification: + // + Var newVar(bool polarity = true, bool dvar = true, bool freeze = false); + bool addClause(const vec<Lit>& ps, ClauseId& id); + bool addEmptyClause(); // Add the empty clause to the solver. + bool addClause(Lit p, ClauseId& id); // Add a unit clause to the solver. + bool addClause(Lit p, + Lit q, + ClauseId& id); // Add a binary clause to the solver. + bool addClause(Lit p, + Lit q, + Lit r, + ClauseId& id); // Add a ternary clause to the solver. + bool addClause_(vec<Lit>& ps, ClauseId& id); + bool substitute(Var v, Lit x); // Replace all occurences of v with x (may + // cause a contradiction). + + // Variable mode: + // + void setFrozen(Var v, + bool b); // If a variable is frozen it will not be eliminated. + bool isEliminated(Var v) const; + + // Solving: + // + lbool solve(const vec<Lit>& assumps, + bool do_simp = true, + bool turn_off_simp = false); + lbool solveLimited(const vec<Lit>& assumps, + bool do_simp = true, + bool turn_off_simp = false); + lbool solveLimited(bool do_simp = true, bool turn_off_simp = false); + lbool solve(bool do_simp = true, bool turn_off_simp = false); + lbool solve(Lit p, bool do_simp = true, bool turn_off_simp = false); + lbool solve(Lit p, Lit q, bool do_simp = true, bool turn_off_simp = false); + lbool solve( + Lit p, Lit q, Lit r, bool do_simp = true, bool turn_off_simp = false); + bool eliminate(bool turn_off_elim = false); // Perform variable elimination + // based simplification. + + // Memory managment: + // + void garbageCollect() override; + + // Generate a (possibly simplified) DIMACS file: + // #if 0 void toDimacs (const char* file, const vec<Lit>& assumps); void toDimacs (const char* file); diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 6e5dc664e..6abaa30c6 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -129,75 +129,93 @@ static DoubleOption opt_garbage_frac (_cat, "gc-frac", "The fraction o CRef Solver::TCRef_Undef = CRef_Undef; CRef Solver::TCRef_Lazy = CRef_Lazy; -class ScopedBool { - bool& watch; - bool oldValue; -public: - ScopedBool(bool& watch, bool newValue) - : watch(watch), oldValue(watch) { +class ScopedBool +{ + bool& d_watch; + bool d_oldValue; + + public: + ScopedBool(bool& watch, bool newValue) : d_watch(watch), d_oldValue(watch) + { watch = newValue; } - ~ScopedBool() { - watch = oldValue; - } + ~ScopedBool() { d_watch = d_oldValue; } }; - //================================================================================================= // Constructor/Destructor: -Solver::Solver(CVC4::prop::TheoryProxy* proxy, CVC4::context::Context* context, bool enable_incremental) : - proxy(proxy) - , context(context) - , assertionLevel(0) - , enable_incremental(enable_incremental) - , minisat_busy(false) - // Parameters (user settable): - // - , verbosity (0) - , var_decay (opt_var_decay) - , clause_decay (opt_clause_decay) - , random_var_freq (opt_random_var_freq) - , random_seed (opt_random_seed) - , luby_restart (opt_luby_restart) - , ccmin_mode (opt_ccmin_mode) - , phase_saving (opt_phase_saving) - , rnd_pol (false) - , rnd_init_act (opt_rnd_init_act) - , garbage_frac (opt_garbage_frac) - , restart_first (opt_restart_first) - , restart_inc (opt_restart_inc) - - // Parameters (the rest): - // - , learntsize_factor(1), learntsize_inc(1.5) - - // Parameters (experimental): - // - , learntsize_adjust_start_confl (100) - , learntsize_adjust_inc (1.5) - - // Statistics: (formerly in 'SolverStats') - // - , solves(0), starts(0), decisions(0), rnd_decisions(0), propagations(0), conflicts(0), resources_consumed(0) - , dec_vars(0), clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0) - - , ok (true) - , cla_inc (1) - , var_inc (1) - , watches (WatcherDeleted(ca)) - , qhead (0) - , simpDB_assigns (-1) - , simpDB_props (0) - , order_heap (VarOrderLt(activity)) - , progress_estimate (0) - , remove_satisfied (!enable_incremental) - - // Resource constraints: - // - , conflict_budget (-1) - , propagation_budget (-1) - , asynch_interrupt (false) +Solver::Solver(CVC4::prop::TheoryProxy* proxy, + CVC4::context::Context* context, + bool enable_incremental) + : d_proxy(proxy), + d_context(context), + assertionLevel(0), + d_enable_incremental(enable_incremental), + minisat_busy(false) + // Parameters (user settable): + // + , + verbosity(0), + var_decay(opt_var_decay), + clause_decay(opt_clause_decay), + random_var_freq(opt_random_var_freq), + random_seed(opt_random_seed), + luby_restart(opt_luby_restart), + ccmin_mode(opt_ccmin_mode), + phase_saving(opt_phase_saving), + rnd_pol(false), + rnd_init_act(opt_rnd_init_act), + garbage_frac(opt_garbage_frac), + restart_first(opt_restart_first), + restart_inc(opt_restart_inc) + + // Parameters (the rest): + // + , + learntsize_factor(1), + learntsize_inc(1.5) + + // Parameters (experimental): + // + , + learntsize_adjust_start_confl(100), + learntsize_adjust_inc(1.5) + + // Statistics: (formerly in 'SolverStats') + // + , + solves(0), + starts(0), + decisions(0), + rnd_decisions(0), + propagations(0), + conflicts(0), + resources_consumed(0), + dec_vars(0), + clauses_literals(0), + learnts_literals(0), + max_literals(0), + tot_literals(0) + + , + ok(true), + cla_inc(1), + var_inc(1), + watches(WatcherDeleted(ca)), + qhead(0), + simpDB_assigns(-1), + simpDB_props(0), + order_heap(VarOrderLt(activity)), + progress_estimate(0), + remove_satisfied(!enable_incremental) + + // Resource constraints: + // + , + conflict_budget(-1), + propagation_budget(-1), + asynch_interrupt(false) { PROOF(ProofManager::currentPM()->initSatProof(this);) @@ -257,7 +275,7 @@ Var Solver::newVar(bool sign, bool dvar, bool isTheoryAtom, bool preRegister, bo } void Solver::resizeVars(int newSize) { - assert(enable_incremental); + assert(d_enable_incremental); assert(decisionLevel() == 0); Assert(newSize >= 2) << "always keep true/false"; if (newSize < nVars()) { @@ -288,7 +306,7 @@ CRef Solver::reason(Var x) { Debug("pf::sat") << "Solver::reason(" << x << ")" << std::endl; // If we already have a reason, just return it - if (vardata[x].reason != CRef_Lazy) return vardata[x].reason; + if (vardata[x].d_reason != CRef_Lazy) return vardata[x].d_reason; // What's the literal we are trying to explain Lit l = mkLit(x, value(x) != l_True); @@ -296,7 +314,8 @@ CRef Solver::reason(Var x) { // Get the explanation from the theory SatClause explanation_cl; // FIXME: at some point return a tag with the theory that spawned you - proxy->explainPropagation(MinisatSatSolver::toSatLiteral(l), explanation_cl); + d_proxy->explainPropagation(MinisatSatSolver::toSatLiteral(l), + explanation_cl); vec<Lit> explanation; MinisatSatSolver::toMinisatClause(explanation_cl, explanation); @@ -352,9 +371,9 @@ CRef Solver::reason(Var x) { explanation.shrink(i - j); Debug("pf::sat") << "Solver::reason: explanation = "; - for (int i = 0; i < explanation.size(); ++i) + for (int k = 0; k < explanation.size(); ++k) { - Debug("pf::sat") << explanation[i] << " "; + Debug("pf::sat") << explanation[k] << " "; } Debug("pf::sat") << std::endl; @@ -578,7 +597,7 @@ void Solver::removeClause(CRef cr) { Debug("minisat::remove-clause") << "Solver::removeClause(" << c << ")" << std::endl; detachClause(cr); // Don't leave pointers to free'd memory! - if (locked(c)) vardata[var(c[0])].reason = CRef_Undef; + if (locked(c)) vardata[var(c[0])].d_reason = CRef_Undef; c.mark(1); ca.free(cr); } @@ -599,15 +618,15 @@ void Solver::cancelUntil(int level) { if (decisionLevel() > level){ // Pop the SMT context for (int l = trail_lim.size() - level; l > 0; --l) { - context->pop(); + d_context->pop(); if(Dump.isOn("state")) { - proxy->dumpStatePop(); + d_proxy->dumpStatePop(); } } for (int c = trail.size()-1; c >= trail_lim[level]; c--){ Var x = var(trail[c]); assigns [x] = l_Undef; - vardata[x].trail_index = -1; + vardata[x].d_trail_index = -1; if ((phase_saving > 1 || ((phase_saving == 1) && c > trail_lim.last()) ) && ((polarity[x] & 0x2) == 0)) { @@ -622,9 +641,13 @@ void Solver::cancelUntil(int level) { // Register variables that have not been registered yet int currentLevel = decisionLevel(); - for(int i = variables_to_register.size() - 1; i >= 0 && variables_to_register[i].level > currentLevel; --i) { - variables_to_register[i].level = currentLevel; - proxy->variableNotify(MinisatSatSolver::toSatVariable(variables_to_register[i].var)); + for (int i = variables_to_register.size() - 1; + i >= 0 && variables_to_register[i].d_level > currentLevel; + --i) + { + variables_to_register[i].d_level = currentLevel; + d_proxy->variableNotify( + MinisatSatSolver::toSatVariable(variables_to_register[i].d_var)); } } } @@ -641,7 +664,7 @@ Lit Solver::pickBranchLit() #ifdef CVC4_REPLAY - nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextReplayDecision()); + nextLit = MinisatSatSolver::toMinisatLit(d_proxy->getNextReplayDecision()); if (nextLit != lit_Undef) { return nextLit; @@ -649,7 +672,8 @@ Lit Solver::pickBranchLit() #endif /* CVC4_REPLAY */ // Theory requests - nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextTheoryDecisionRequest()); + nextLit = + MinisatSatSolver::toMinisatLit(d_proxy->getNextTheoryDecisionRequest()); while (nextLit != lit_Undef) { if(value(var(nextLit)) == l_Undef) { Debug("theoryDecision") @@ -660,14 +684,15 @@ Lit Solver::pickBranchLit() // org-mode tracing -- theory decision if (Trace.isOn("dtview")) { - dtviewDecisionHelper(context->getLevel(), - proxy->getNode(MinisatSatSolver::toSatLiteral(nextLit)), - "THEORY"); + dtviewDecisionHelper( + d_context->getLevel(), + d_proxy->getNode(MinisatSatSolver::toSatLiteral(nextLit)), + "THEORY"); } if (Trace.isOn("dtview::prop")) { - dtviewPropagationHeaderHelper(context->getLevel()); + dtviewPropagationHeaderHelper(d_context->getLevel()); } return nextLit; @@ -676,7 +701,8 @@ Lit Solver::pickBranchLit() << "getNextTheoryDecisionRequest(): would decide on " << nextLit << " but it already has an assignment" << std::endl; } - nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextTheoryDecisionRequest()); + nextLit = MinisatSatSolver::toMinisatLit( + d_proxy->getNextTheoryDecisionRequest()); } Debug("theoryDecision") << "getNextTheoryDecisionRequest(): decide on another literal" @@ -684,7 +710,8 @@ Lit Solver::pickBranchLit() // DE requests bool stopSearch = false; - nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextDecisionEngineRequest(stopSearch)); + nextLit = MinisatSatSolver::toMinisatLit( + d_proxy->getNextDecisionEngineRequest(stopSearch)); if(stopSearch) { return lit_Undef; } @@ -700,14 +727,15 @@ Lit Solver::pickBranchLit() // org-mode tracing -- decision engine decision if (Trace.isOn("dtview")) { - dtviewDecisionHelper(context->getLevel(), - proxy->getNode(MinisatSatSolver::toSatLiteral(nextLit)), - "DE"); + dtviewDecisionHelper( + d_context->getLevel(), + d_proxy->getNode(MinisatSatSolver::toSatLiteral(nextLit)), + "DE"); } if (Trace.isOn("dtview::prop")) { - dtviewPropagationHeaderHelper(context->getLevel()); + dtviewPropagationHeaderHelper(d_context->getLevel()); } return nextLit; @@ -732,7 +760,9 @@ Lit Solver::pickBranchLit() if(!decision[next]) continue; // Check with decision engine about relevancy - if(proxy->isDecisionRelevant(MinisatSatSolver::toSatVariable(next)) == false ) { + if (d_proxy->isDecisionRelevant(MinisatSatSolver::toSatVariable(next)) + == false) + { next = var_Undef; } } @@ -742,8 +772,8 @@ Lit Solver::pickBranchLit() } else { decisions++; // Check with decision engine if it can tell polarity - lbool dec_pol = MinisatSatSolver::toMinisatlbool - (proxy->getDecisionPolarity(MinisatSatSolver::toSatVariable(next))); + lbool dec_pol = MinisatSatSolver::toMinisatlbool( + d_proxy->getDecisionPolarity(MinisatSatSolver::toSatVariable(next))); Lit decisionLit; if(dec_pol != l_Undef) { Assert(dec_pol == l_True || dec_pol == l_False); @@ -759,14 +789,15 @@ Lit Solver::pickBranchLit() // org-mode tracing -- decision engine decision if (Trace.isOn("dtview")) { - dtviewDecisionHelper(context->getLevel(), - proxy->getNode(MinisatSatSolver::toSatLiteral(decisionLit)), - "DE"); + dtviewDecisionHelper( + d_context->getLevel(), + d_proxy->getNode(MinisatSatSolver::toSatLiteral(decisionLit)), + "DE"); } if (Trace.isOn("dtview::prop")) { - dtviewPropagationHeaderHelper(context->getLevel()); + dtviewPropagationHeaderHelper(d_context->getLevel()); } return decisionLit; @@ -920,17 +951,18 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) else{ int max_i = 1; // Find the first literal assigned at the next-highest level: - for (int i = 2; i < out_learnt.size(); i++) - if (level(var(out_learnt[i])) > level(var(out_learnt[max_i]))) - max_i = i; + for (int k = 2; k < out_learnt.size(); k++) + if (level(var(out_learnt[k])) > level(var(out_learnt[max_i]))) + max_i = k; // Swap-in this literal at index 1: - Lit p = out_learnt[max_i]; + Lit p2 = out_learnt[max_i]; out_learnt[max_i] = out_learnt[1]; - out_learnt[1] = p; - out_btlevel = level(var(p)); + out_learnt[1] = p2; + out_btlevel = level(var(p2)); } - for (int j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0; // ('seen[]' is now cleared) + for (int k = 0; k < analyze_toclear.size(); k++) + seen[var(analyze_toclear[k])] = 0; // ('seen[]' is now cleared) // Return the maximal resolution level return max_resolution_level; @@ -953,19 +985,24 @@ bool Solver::litRedundant(Lit p, uint32_t abstract_levels) // Since calling reason might relocate to resize, c is not necesserily the right reference, we must // use the allocator each time for (int i = 1; i < c_size; i++){ - Lit p = ca[c_reason][i]; - if (!seen[var(p)] && level(var(p)) > 0){ - if (reason(var(p)) != CRef_Undef && (abstractLevel(var(p)) & abstract_levels) != 0){ - seen[var(p)] = 1; - analyze_stack.push(p); - analyze_toclear.push(p); - }else{ - for (int j = top; j < analyze_toclear.size(); j++) - seen[var(analyze_toclear[j])] = 0; - analyze_toclear.shrink(analyze_toclear.size() - top); - return false; - } + Lit p2 = ca[c_reason][i]; + if (!seen[var(p2)] && level(var(p2)) > 0) + { + if (reason(var(p2)) != CRef_Undef + && (abstractLevel(var(p2)) & abstract_levels) != 0) + { + seen[var(p2)] = 1; + analyze_stack.push(p2); + analyze_toclear.push(p2); } + else + { + for (int j = top; j < analyze_toclear.size(); j++) + seen[var(analyze_toclear[j])] = 0; + analyze_toclear.shrink(analyze_toclear.size() - top); + return false; + } + } } } @@ -1022,7 +1059,7 @@ void Solver::uncheckedEnqueue(Lit p, CRef from) trail.push_(p); if (theory[var(p)]) { // Enqueue to the theory - proxy->enqueueTheoryLiteral(MinisatSatSolver::toSatLiteral(p)); + d_proxy->enqueueTheoryLiteral(MinisatSatSolver::toSatLiteral(p)); } } @@ -1057,7 +1094,7 @@ CRef Solver::propagate(TheoryCheckType type) confl = updateLemmas(); return confl; } else { - recheck = proxy->theoryNeedCheck(); + recheck = d_proxy->theoryNeedCheck(); return confl; } } @@ -1087,7 +1124,7 @@ CRef Solver::propagate(TheoryCheckType type) { if (confl != CRef_Undef) { - dtviewPropConflictHelper(decisionLevel(), ca[confl], proxy); + dtviewPropConflictHelper(decisionLevel(), ca[confl], d_proxy); } } // Even though in conflict, we still need to discharge the lemmas @@ -1116,7 +1153,7 @@ void Solver::propagateTheory() { SatClause propagatedLiteralsClause; // Doesn't actually call propagate(); that's done in theoryCheck() now that combination // is online. This just incorporates those propagations previously discovered. - proxy->theoryPropagate(propagatedLiteralsClause); + d_proxy->theoryPropagate(propagatedLiteralsClause); vec<Lit> propagatedLiterals; MinisatSatSolver::toMinisatClause(propagatedLiteralsClause, propagatedLiterals); @@ -1133,7 +1170,8 @@ void Solver::propagateTheory() { if (value(p) == l_False) { Debug("minisat") << "Conflict in theory propagation" << std::endl; SatClause explanation_cl; - proxy->explainPropagation(MinisatSatSolver::toSatLiteral(p), explanation_cl); + d_proxy->explainPropagation(MinisatSatSolver::toSatLiteral(p), + explanation_cl); vec<Lit> explanation; MinisatSatSolver::toMinisatClause(explanation_cl, explanation); ClauseId id; // FIXME: mark it as explanation here somehow? @@ -1158,7 +1196,7 @@ void Solver::propagateTheory() { |________________________________________________________________________________________________@*/ void Solver::theoryCheck(CVC4::theory::Theory::Effort effort) { - proxy->theoryCheck(effort); + d_proxy->theoryCheck(effort); } /*_________________________________________________________________________________________________ @@ -1187,7 +1225,7 @@ CRef Solver::propagateBool() // if propagation tracing enabled, print boolean propagation if (Trace.isOn("dtview::prop")) { - dtviewBoolPropagationHelper(decisionLevel(), p, proxy); + dtviewBoolPropagationHelper(decisionLevel(), p, d_proxy); } for (i = j = (Watcher*)ws, end = i + ws.size(); i != end;){ @@ -1443,7 +1481,7 @@ lbool Solver::search(int nof_conflicts) // If this was a final check, we are satisfiable if (check_type == CHECK_FINAL) { - bool decisionEngineDone = proxy->isDecisionEngineDone(); + bool decisionEngineDone = d_proxy->isDecisionEngineDone(); // Unless a lemma has added more stuff to the queues if (!decisionEngineDone && (!order_heap.empty() || qhead < trail.size()) ) { @@ -1468,7 +1506,7 @@ lbool Solver::search(int nof_conflicts) cancelUntil(0); // [mdeters] notify theory engine of restarts for deferred // theory processing - proxy->notifyRestart(); + d_proxy->notifyRestart(); return l_Undef; } @@ -1490,8 +1528,8 @@ lbool Solver::search(int nof_conflicts) // Dummy decision level: newDecisionLevel(); } else if (value(p) == l_False) { - analyzeFinal(~p, conflict); - return l_False; + analyzeFinal(~p, d_conflict); + return l_False; } else { next = p; break; @@ -1511,7 +1549,7 @@ lbool Solver::search(int nof_conflicts) } #ifdef CVC4_REPLAY - proxy->logDecision(MinisatSatSolver::toSatLiteral(next)); + d_proxy->logDecision(MinisatSatSolver::toSatLiteral(next)); #endif /* CVC4_REPLAY */ } @@ -1575,7 +1613,7 @@ lbool Solver::solve_() assert(decisionLevel() == 0); model.clear(); - conflict.clear(); + d_conflict.clear(); if (!ok){ minisat_busy = false; return l_False; @@ -1619,8 +1657,9 @@ lbool Solver::solve_() model[i] = value(i); Debug("minisat") << i << " = " << model[i] << std::endl; } - }else if (status == l_False && conflict.size() == 0) - ok = false; + } + else if (status == l_False && d_conflict.size() == 0) + ok = false; return status; } @@ -1728,7 +1767,7 @@ void Solver::relocAll(ClauseAllocator& to) if (hasReasonClause(v) && (ca[reason(v)].reloced() || locked(ca[reason(v)]))) ca.reloc( - vardata[v].reason, to, NULLPROOF(ProofManager::getSatProof())); + vardata[v].d_reason, to, NULLPROOF(ProofManager::getSatProof())); } // All learnt: // @@ -1761,7 +1800,7 @@ void Solver::garbageCollect() void Solver::push() { - assert(enable_incremental); + assert(d_enable_incremental); assert(decisionLevel() == 0); ++assertionLevel; @@ -1769,14 +1808,14 @@ void Solver::push() trail_ok.push(ok); assigns_lim.push(assigns.size()); - context->push(); // SAT context for CVC4 + d_context->push(); // SAT context for CVC4 Debug("minisat") << "MINISAT PUSH assertionLevel is " << assertionLevel << ", trail.size is " << trail.size() << std::endl; } void Solver::pop() { - assert(enable_incremental); + assert(d_enable_incremental); assert(decisionLevel() == 0); @@ -1804,7 +1843,7 @@ void Solver::pop() removeClausesAboveLevel(clauses_removable, assertionLevel); // Pop the SAT context to notify everyone - context->pop(); // SAT context for CVC4 + d_context->pop(); // SAT context for CVC4 // Pop the created variables resizeVars(assigns_lim.last()); @@ -1821,7 +1860,7 @@ CRef Solver::updateLemmas() { Debug("minisat::lemmas") << "Solver::updateLemmas() begin" << std::endl; // Avoid adding lemmas indefinitely without resource-out - proxy->spendResource(ResourceManager::Resource::LemmaStep); + d_proxy->spendResource(ResourceManager::Resource::LemmaStep); CRef conflict = CRef_Undef; @@ -1881,11 +1920,11 @@ CRef Solver::updateLemmas() { PROOF(Assert(lemmas.size() == (int)lemmas_cnf_assertion.size());); // Attach all the clauses and enqueue all the propagations - for (int i = 0; i < lemmas.size(); ++ i) + for (int j = 0; j < lemmas.size(); ++j) { // The current lemma - vec<Lit>& lemma = lemmas[i]; - bool removable = lemmas_removable[i]; + vec<Lit>& lemma = lemmas[j]; + bool removable = lemmas_removable[j]; // Attach it if non-unit CRef lemma_ref = CRef_Undef; @@ -1895,22 +1934,22 @@ CRef Solver::updateLemmas() { if (removable && !assertionLevelOnly()) { clauseLevel = 0; - for (int i = 0; i < lemma.size(); ++ i) { - clauseLevel = std::max(clauseLevel, intro_level(var(lemma[i]))); + for (int k = 0; k < lemma.size(); ++k) + { + clauseLevel = std::max(clauseLevel, intro_level(var(lemma[k]))); } } lemma_ref = ca.alloc(clauseLevel, lemma, removable); - PROOF - ( - TNode cnf_assertion = lemmas_cnf_assertion[i].first; - TNode cnf_def = lemmas_cnf_assertion[i].second; - - Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (2)" << std::endl; - ClauseId id = ProofManager::getSatProof()->registerClause(lemma_ref, THEORY_LEMMA); - ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion); - ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def); - ); + PROOF(TNode cnf_assertion = lemmas_cnf_assertion[j].first; + TNode cnf_def = lemmas_cnf_assertion[j].second; + + Debug("pf::sat") + << "Minisat::Solver registering a THEORY_LEMMA (2)" << std::endl; + ClauseId id = ProofManager::getSatProof()->registerClause( + lemma_ref, THEORY_LEMMA); + ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion); + ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def);); if (removable) { clauses_removable.push(lemma_ref); } else { @@ -1920,8 +1959,8 @@ CRef Solver::updateLemmas() { } else { PROOF ( - Node cnf_assertion = lemmas_cnf_assertion[i].first; - Node cnf_def = lemmas_cnf_assertion[i].second; + Node cnf_assertion = lemmas_cnf_assertion[j].first; + Node cnf_def = lemmas_cnf_assertion[j].second; Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (3)" << std::endl; ClauseId id = ProofManager::getSatProof()->registerUnitClause(lemma[0], THEORY_LEMMA); @@ -1993,10 +2032,10 @@ void ClauseAllocator::reloc(CRef& cr, inline bool Solver::withinBudget(ResourceManager::Resource r) const { - Assert(proxy); + Assert(d_proxy); // spendResource sets async_interrupt or throws UnsafeInterruptException // depending on whether hard-limit is enabled - proxy->spendResource(r); + d_proxy->spendResource(r); bool within_budget = !asynch_interrupt diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 0cec30d24..508947456 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -66,14 +66,13 @@ public: typedef Clause TClause; typedef CRef TCRef; typedef vec<Lit> TLitVec; - -protected: + protected: /** The pointer to the proxy that provides interfaces to the SMT engine */ - CVC4::prop::TheoryProxy* proxy; + CVC4::prop::TheoryProxy* d_proxy; /** The context from the SMT solver */ - CVC4::context::Context* context; + CVC4::context::Context* d_context; /** The current assertion level (user) */ int assertionLevel; @@ -84,21 +83,22 @@ protected: /** Variable representing false */ Var varFalse; -public: + public: /** Returns the current user assertion level */ int getAssertionLevel() const { return assertionLevel; } -protected: + + protected: /** Do we allow incremental solving */ - bool enable_incremental; + bool d_enable_incremental; /** Literals propagated by lemmas */ - vec< vec<Lit> > lemmas; + vec<vec<Lit> > lemmas; /** Is the lemma removable */ vec<bool> lemmas_removable; /** Nodes being converted to CNF */ - std::vector< std::pair<CVC4::Node, CVC4::Node > >lemmas_cnf_assertion; + std::vector<std::pair<CVC4::Node, CVC4::Node> > lemmas_cnf_assertion; /** Do a another check if FULL_EFFORT was the last one */ bool recheck; @@ -110,11 +110,11 @@ protected: bool minisat_busy; // Information about registration of variables - struct VarIntroInfo { - Var var; - int level; - VarIntroInfo(Var var, int level) - : var(var), level(level) {} + struct VarIntroInfo + { + Var d_var; + int d_level; + VarIntroInfo(Var var, int level) : d_var(var), d_level(level) {} }; /** Variables to re-register with theory solvers on backtracks */ @@ -138,30 +138,38 @@ public: // Less than for literals in a lemma struct lemma_lt { - Solver& solver; - lemma_lt(Solver& solver) : solver(solver) {} - bool operator () (Lit x, Lit y) { - lbool x_value = solver.value(x); - lbool y_value = solver.value(y); - // Two unassigned literals are sorted arbitrarily - if (x_value == l_Undef && y_value == l_Undef) { - return x < y; + Solver& d_solver; + lemma_lt(Solver& solver) : d_solver(solver) {} + bool operator()(Lit x, Lit y) + { + lbool x_value = d_solver.value(x); + lbool y_value = d_solver.value(y); + // Two unassigned literals are sorted arbitrarily + if (x_value == l_Undef && y_value == l_Undef) + { + return x < y; + } + // Unassigned literals are put to front + if (x_value == l_Undef) return true; + if (y_value == l_Undef) return false; + // Literals of the same value are sorted by decreasing levels + if (x_value == y_value) + { + return d_solver.trail_index(var(x)) > d_solver.trail_index(var(y)); + } + else + { + // True literals go up front + if (x_value == l_True) + { + return true; } - // Unassigned literals are put to front - if (x_value == l_Undef) return true; - if (y_value == l_Undef) return false; - // Literals of the same value are sorted by decreasing levels - if (x_value == y_value) { - return solver.trail_index(var(x)) > solver.trail_index(var(y)); - } else { - // True literals go up front - if (x_value == l_True) { - return true; - } else { - return false; - } + else + { + return false; } } + } }; @@ -246,8 +254,9 @@ public: // Extra results: (read-only member variable) // vec<lbool> model; // If problem is satisfiable, this vector contains the model (if any). - vec<Lit> conflict; // If problem is unsatisfiable (possibly under assumptions), - // this vector represent the final conflict clause expressed in the assumptions. + vec<Lit> d_conflict; // If problem is unsatisfiable (possibly under + // assumptions), this vector represent the final + // conflict clause expressed in the assumptions. // Mode of operation: // @@ -282,22 +291,26 @@ protected: // struct VarData { // Reason for the literal being in the trail - CRef reason; + CRef d_reason; // Sat level when the literal was added to the trail - int level; + int d_level; // User level when the literal was added to the trail - int user_level; + int d_user_level; // User level at which this literal was introduced - int intro_level; + int d_intro_level; // The index in the trail - int trail_index; - - VarData(CRef reason, int level, int user_level, int intro_level, int trail_index) - : reason(reason) - , level(level) - , user_level(user_level) - , intro_level(intro_level) - , trail_index(trail_index) + int d_trail_index; + + VarData(CRef reason, + int level, + int user_level, + int intro_level, + int trail_index) + : d_reason(reason), + d_level(level), + d_user_level(user_level), + d_intro_level(intro_level), + d_trail_index(trail_index) {} }; @@ -464,21 +477,53 @@ public: //================================================================================================= // Implementation of inline methods: -inline bool Solver::hasReasonClause(Var x) const { return vardata[x].reason != CRef_Undef && vardata[x].reason != CRef_Lazy; } +inline bool Solver::hasReasonClause(Var x) const +{ + return vardata[x].d_reason != CRef_Undef && vardata[x].d_reason != CRef_Lazy; +} -inline bool Solver::isPropagated(Var x) const { return vardata[x].reason != CRef_Undef; } +inline bool Solver::isPropagated(Var x) const +{ + return vardata[x].d_reason != CRef_Undef; +} -inline bool Solver::isPropagatedBy(Var x, const Clause& c) const { return vardata[x].reason != CRef_Undef && vardata[x].reason != CRef_Lazy && ca.lea(vardata[var(c[0])].reason) == &c; } +inline bool Solver::isPropagatedBy(Var x, const Clause& c) const +{ + return vardata[x].d_reason != CRef_Undef && vardata[x].d_reason != CRef_Lazy + && ca.lea(vardata[var(c[0])].d_reason) == &c; +} -inline bool Solver::isDecision(Var x) const { Debug("minisat") << "var " << x << " is a decision iff " << (vardata[x].reason == CRef_Undef) << " && " << level(x) << " > 0" << std::endl; return vardata[x].reason == CRef_Undef && level(x) > 0; } +inline bool Solver::isDecision(Var x) const +{ + Debug("minisat") << "var " << x << " is a decision iff " + << (vardata[x].d_reason == CRef_Undef) << " && " << level(x) + << " > 0" << std::endl; + return vardata[x].d_reason == CRef_Undef && level(x) > 0; +} -inline int Solver::level (Var x) const { assert(x < vardata.size()); return vardata[x].level; } +inline int Solver::level(Var x) const +{ + assert(x < vardata.size()); + return vardata[x].d_level; +} -inline int Solver::user_level(Var x) const { assert(x < vardata.size()); return vardata[x].user_level; } +inline int Solver::user_level(Var x) const +{ + assert(x < vardata.size()); + return vardata[x].d_user_level; +} -inline int Solver::intro_level(Var x) const { assert(x < vardata.size()); return vardata[x].intro_level; } +inline int Solver::intro_level(Var x) const +{ + assert(x < vardata.size()); + return vardata[x].d_intro_level; +} -inline int Solver::trail_index(Var x) const { assert(x < vardata.size()); return vardata[x].trail_index; } +inline int Solver::trail_index(Var x) const +{ + assert(x < vardata.size()); + return vardata[x].d_trail_index; +} inline void Solver::insertVarOrder(Var x) { assert(x < vardata.size()); @@ -522,7 +567,16 @@ inline bool Solver::addClause (Lit p, Lit q, bool removable, ClauseId& inline bool Solver::addClause (Lit p, Lit q, Lit r, bool removable, ClauseId& id) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable, id); } inline bool Solver::locked (const Clause& c) const { return value(c[0]) == l_True && isPropagatedBy(var(c[0]), c); } -inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); flipped.push(false); context->push(); if(Dump.isOn("state")) { Dump("state") << CVC4::PushCommand(); } } +inline void Solver::newDecisionLevel() +{ + trail_lim.push(trail.size()); + flipped.push(false); + d_context->push(); + if (Dump.isOn("state")) + { + Dump("state") << CVC4::PushCommand(); + } +} inline int Solver::decisionLevel () const { return trail_lim.size(); } inline uint32_t Solver::abstractLevel (Var x) const { return 1 << (level(x) & 31); } diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index cde85a186..3e9b81263 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3184,8 +3184,7 @@ void SmtEnginePrivate::collectSkolems(TNode n, set<TNode>& skolemSet, unordered_ size_t sz = n.getNumChildren(); if (sz == 0) { - IteSkolemMap::iterator it = getIteSkolemMap().find(n); - if (it != getIteSkolemMap().end()) + if (getIteSkolemMap().find(n) != getIteSkolemMap().end()) { skolemSet.insert(n); } @@ -3210,11 +3209,12 @@ bool SmtEnginePrivate::checkForBadSkolems(TNode n, TNode skolem, unordered_map<N size_t sz = n.getNumChildren(); if (sz == 0) { - IteSkolemMap::iterator it = getIteSkolemMap().find(n); + IteSkolemMap::iterator iit = getIteSkolemMap().find(n); bool bad = false; - if (it != getIteSkolemMap().end()) + if (iit != getIteSkolemMap().end()) { - if (!((*it).first < n)) { + if (!((*iit).first < n)) + { bad = true; } } diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp index 11cf55354..438e11511 100644 --- a/src/theory/arith/dio_solver.cpp +++ b/src/theory/arith/dio_solver.cpp @@ -513,8 +513,8 @@ SumPair DioSolver::purifyIndex(TrailIndex i){ Constant negOne = Constant::mkConstant(-1); for(uint32_t revIter = d_subs.size(); revIter > 0; --revIter){ - uint32_t i = revIter - 1; - Node freshNode = d_subs[i].d_fresh; + uint32_t i2 = revIter - 1; + Node freshNode = d_subs[i2].d_fresh; if(freshNode.isNull()){ continue; }else{ @@ -523,7 +523,7 @@ SumPair DioSolver::purifyIndex(TrailIndex i){ Constant a = vsum.getCoefficient(VarList(var)); if(!a.isZero()){ - const SumPair& sj = d_trail[d_subs[i].d_constraint].d_eq; + const SumPair& sj = d_trail[d_subs[i2].d_constraint].d_eq; Assert(sj.getPolynomial().getCoefficient(VarList(var)).isOne()); SumPair newSi = (curr * negOne) + (sj * a); Assert(newSi.getPolynomial().getCoefficient(VarList(var)).isZero()); diff --git a/src/theory/arith/nl_model.cpp b/src/theory/arith/nl_model.cpp index 3c1d5f1e9..d09a138fe 100644 --- a/src/theory/arith/nl_model.cpp +++ b/src/theory/arith/nl_model.cpp @@ -45,9 +45,9 @@ void NlModel::reset(TheoryModel* m, std::map<Node, Node>& arithModel) d_arithVal.clear(); // process arithModel std::map<Node, Node>::iterator it; - for (const std::pair<const Node, Node>& m : arithModel) + for (const std::pair<const Node, Node>& m2 : arithModel) { - d_arithVal[m.first] = m.second; + d_arithVal[m2.first] = m2.second; } } @@ -700,14 +700,14 @@ bool NlModel::solveEqualitySimple(Node eq, Assert(m_var.isConst()); for (unsigned r = 0; r < 2; r++) { - for (unsigned b = 0; b < 2; b++) + for (unsigned b2 = 0; b2 < 2; b2++) { - Node val = b == 0 ? l : u; + Node val = b2 == 0 ? l : u; // (-b +- approx_sqrt( b^2 - 4ac ))/2a Node approx = nm->mkNode( MULT, coeffa, nm->mkNode(r == 0 ? MINUS : PLUS, negb, val)); approx = Rewriter::rewrite(approx); - bounds[r][b] = approx; + bounds[r][b2] = approx; Assert(approx.isConst()); } if (bounds[r][0].getConst<Rational>() > bounds[r][1].getConst<Rational>()) @@ -776,13 +776,13 @@ bool NlModel::simpleCheckModelLit(Node lit) // x = a is ( x >= a ^ x <= a ) for (unsigned i = 0; i < 2; i++) { - Node lit = nm->mkNode(GEQ, atom[i], atom[1 - i]); + Node lit2 = nm->mkNode(GEQ, atom[i], atom[1 - i]); if (!pol) { - lit = lit.negate(); + lit2 = lit2.negate(); } - lit = Rewriter::rewrite(lit); - bool success = simpleCheckModelLit(lit); + lit2 = Rewriter::rewrite(lit2); + bool success = simpleCheckModelLit(lit2); if (success != pol) { // false != true -> one conjunct of equality is false, we fail @@ -1167,7 +1167,7 @@ bool NlModel::simpleCheckModelMsum(const std::map<Node, Node>& msum, bool pol) } // must over/under approximate based on vc_set_lower, computed above Node vb = vc_set_lower ? l : u; - for (unsigned i = 0; i < vcfact; i++) + for (unsigned i2 = 0; i2 < vcfact; i2++) { vbs.push_back(vb); } @@ -1317,7 +1317,7 @@ void NlModel::getModelValueRepair( Node v = cb.first; if (l != u) { - Node pred = nm->mkNode(AND, nm->mkNode(GEQ, v, l), nm->mkNode(GEQ, u, v)); + pred = nm->mkNode(AND, nm->mkNode(GEQ, v, l), nm->mkNode(GEQ, u, v)); Trace("nl-model") << v << " approximated as " << pred << std::endl; Node witness; if (options::modelWitnessChoice()) diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp index 2d530d602..cd9352b3a 100644 --- a/src/theory/arith/nonlinear_extension.cpp +++ b/src/theory/arith/nonlinear_extension.cpp @@ -3828,9 +3828,9 @@ std::pair<Node, Node> NonlinearExtension::getTfModelBounds(Node tf, unsigned d) std::vector<Node> bounds; TNode tfv = d_taylor_real_fv; TNode tfs = tf[0]; - for (unsigned d = 0; d < 2; d++) + for (unsigned d2 = 0; d2 < 2; d2++) { - int index = d == 0 ? (isNeg ? 1 : 0) : (isNeg ? 3 : 2); + int index = d2 == 0 ? (isNeg ? 1 : 0) : (isNeg ? 3 : 2); Node pab = pbounds[index]; if (!pab.isNull()) { diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 0ddded6bf..037f0892a 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -1329,7 +1329,6 @@ Theory::PPAssertStatus TheoryArithPrivate::ppAssert(TNode in, SubstitutionMap& o Comparison cmp = Comparison::parseNormalForm(in); Polynomial left = cmp.getLeft(); - Polynomial right = cmp.getRight(); Monomial m = left.getHead(); if (m.getVarList().singleton()){ @@ -2173,11 +2172,11 @@ void TheoryArithPrivate::outputConflicts(){ // // Anyways, we reverse the children in `conflict` here. NodeBuilder<> conflictInFarkasCoefficientOrder(kind::AND); - for (size_t i = 0, nchildren = conflict.getNumChildren(); i < nchildren; - ++i) + for (size_t j = 0, nchildren = conflict.getNumChildren(); j < nchildren; + ++j) { conflictInFarkasCoefficientOrder - << conflict[conflict.getNumChildren() - i - 1]; + << conflict[conflict.getNumChildren() - j - 1]; } if (Debug.isOn("arith::pf::tree")) { @@ -3103,7 +3102,7 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){ if(!safeToCallApprox()) { return; } Assert(safeToCallApprox()); - TimerStat::CodeTimer codeTimer(d_statistics.d_solveIntTimer); + TimerStat::CodeTimer codeTimer0(d_statistics.d_solveIntTimer); ++(d_statistics.d_solveIntCalls); d_statistics.d_inSolveInteger.setData(1); @@ -3145,7 +3144,7 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){ if( relaxRes == LinFeasible ){ MipResult mipRes = MipUnknown; { - TimerStat::CodeTimer codeTimer(d_statistics.d_mipTimer); + TimerStat::CodeTimer codeTimer1(d_statistics.d_mipTimer); mipRes = approx->solveMIP(false); } @@ -3183,7 +3182,7 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){ /* All integer branches closed */ approx->setPivotLimit(2*mipLimit); { - TimerStat::CodeTimer codeTimer(d_statistics.d_mipTimer); + TimerStat::CodeTimer codeTimer2(d_statistics.d_mipTimer); mipRes = approx->solveMIP(true); } @@ -3215,7 +3214,7 @@ void TheoryArithPrivate::solveInteger(Theory::Effort effortLevel){ approx->setPivotLimit(2*mipLimit); approx->setBranchingDepth(2); { - TimerStat::CodeTimer codeTimer(d_statistics.d_mipTimer); + TimerStat::CodeTimer codeTimer3(d_statistics.d_mipTimer); mipRes = approx->solveMIP(true); } replayLemmas(approx); @@ -3316,7 +3315,7 @@ bool TheoryArithPrivate::solveRelaxationOrPanic(Theory::Effort effortLevel){ } bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){ - TimerStat::CodeTimer codeTimer(d_statistics.d_solveRealRelaxTimer); + TimerStat::CodeTimer codeTimer0(d_statistics.d_solveRealRelaxTimer); Assert(d_qflraStatus != Result::SAT); d_partialModel.stopQueueingBoundCounts(); @@ -3370,7 +3369,7 @@ bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){ ApproximateSimplex::Solution relaxSolution; LinResult relaxRes = LinUnknown; { - TimerStat::CodeTimer codeTimer(d_statistics.d_lpTimer); + TimerStat::CodeTimer codeTimer1(d_statistics.d_lpTimer); relaxRes = approxSolver->solveRelaxation(); } Debug("solveRealRelaxation") << "solve relaxation? " << endl; @@ -3770,7 +3769,7 @@ void TheoryArithPrivate::check(Theory::Effort effortLevel){ || options::arithPropagationMode() == options::ArithPropagationMode::BOTH_PROP)) { - TimerStat::CodeTimer codeTimer(d_statistics.d_newPropTime); + TimerStat::CodeTimer codeTimer0(d_statistics.d_newPropTime); Assert(d_qflraStatus != Result::UNSAT); while(!d_currentPropagationList.empty() && !anyConflict()){ @@ -3823,7 +3822,7 @@ void TheoryArithPrivate::check(Theory::Effort effortLevel){ } else { - TimerStat::CodeTimer codeTimer(d_statistics.d_newPropTime); + TimerStat::CodeTimer codeTimer1(d_statistics.d_newPropTime); d_currentPropagationList.clear(); } Assert(d_currentPropagationList.empty()); @@ -5810,11 +5809,11 @@ std::pair<Node, DeltaRational> TheoryArithPrivate::entailmentCheckSimplex(int sg const Tableau::Entry& entry = *ri; ArithVar v = entry.getColVar(); if(v != optVar){ - int sgn = entry.getCoefficient().sgn(); - Assert(sgn != 0); - bool candidate = (sgn > 0) - ? (d_partialModel.cmpAssignmentUpperBound(v) != 0) - : (d_partialModel.cmpAssignmentLowerBound(v) != 0); + int sgn1 = entry.getCoefficient().sgn(); + Assert(sgn1 != 0); + bool candidate = (sgn1 > 0) + ? (d_partialModel.cmpAssignmentUpperBound(v) != 0) + : (d_partialModel.cmpAssignmentLowerBound(v) != 0); if(candidate && (entering == ARITHVAR_SENTINEL || entering > v)){ entering = v; enteringEntry = &entry; diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index d721b7e7a..dcf82e6b4 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -1476,18 +1476,21 @@ void TheoryArrays::check(Effort e) { mayRep = d_mayEqualEqualityEngine.getRepresentative(r[0]); iRep = d_equalityEngine.getRepresentative(r[1]); std::pair<TNode, TNode> key(mayRep, iRep); - ReadBucketMap::iterator it = d_readBucketTable.find(key); - if (it == d_readBucketTable.end()) { + ReadBucketMap::iterator rbm_it = d_readBucketTable.find(key); + if (rbm_it == d_readBucketTable.end()) + { bucketList = new(true) CTNodeList(d_readTableContext); d_readBucketAllocations.push_back(bucketList); d_readBucketTable[key] = bucketList; } else { - bucketList = it->second; + bucketList = rbm_it->second; } - CTNodeList::const_iterator it2 = bucketList->begin(), iend = bucketList->end(); - for (; it2 != iend; ++it2) { - const TNode& r2 = *it2; + CTNodeList::const_iterator ctnl_it = bucketList->begin(), + ctnl_iend = bucketList->end(); + for (; ctnl_it != ctnl_iend; ++ctnl_it) + { + const TNode& r2 = *ctnl_it; Assert(r2.getKind() == kind::SELECT); Assert(mayRep == d_mayEqualEqualityEngine.getRepresentative(r2[0])); Assert(iRep == d_equalityEngine.getRepresentative(r2[1])); diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp index d3aeb5c37..f2f12a548 100644 --- a/src/theory/bv/abstraction.cpp +++ b/src/theory/bv/abstraction.cpp @@ -95,10 +95,10 @@ bool AbstractionModule::applyAbstraction(const std::vector<Node>& assertions, // we did not change anything return false; } - NodeNodeMap seen; + NodeNodeMap seen_rev; for (unsigned i = 0; i < new_assertions.size(); ++i) { - new_assertions[i] = reverseAbstraction(new_assertions[i], seen); + new_assertions[i] = reverseAbstraction(new_assertions[i], seen_rev); } // we undo the abstraction functions so the logic is QF_BV still return true; @@ -235,13 +235,15 @@ void AbstractionModule::skolemizeArguments(std::vector<Node>& assertions) // enumerate arguments assignments std::vector<Node> or_assignments; - for (ArgsTableEntry::iterator it = args.begin(); it != args.end(); ++it) + for (const ArgsVec& av : args) + // for (ArgsTableEntry::iterator it = args.begin(); it != args.end(); + // ++it) { NodeBuilder<> arg_assignment(kind::AND); - ArgsVec& args = *it; - for (unsigned k = 0; k < args.size(); ++k) + // ArgsVec& args = *it; + for (unsigned k = 0; k < av.size(); ++k) { - Node eq = nm->mkNode(kind::EQUAL, args[k], skolem_args[k]); + Node eq = nm->mkNode(kind::EQUAL, av[k], skolem_args[k]); arg_assignment << eq; } or_assignments.push_back(arg_assignment); diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp index 14753deec..de8a0e11e 100644 --- a/src/theory/bv/bv_subtheory_algebraic.cpp +++ b/src/theory/bv/bv_subtheory_algebraic.cpp @@ -984,10 +984,9 @@ Node mergeExplanations(const std::vector<Node>& expls) { TNode expl = expls[i]; Assert(expl.getType().isBoolean()); if (expl.getKind() == kind::AND) { - for (unsigned i = 0; i < expl.getNumChildren(); ++i) { - TNode child = expl[i]; - if (child == utils::mkTrue()) - continue; + for (const TNode& child : expl) + { + if (child == utils::mkTrue()) continue; literals.insert(child); } } else if (expl != utils::mkTrue()) { diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp index 42f4d3e06..77cb45f36 100644 --- a/src/theory/datatypes/datatypes_rewriter.cpp +++ b/src/theory/datatypes/datatypes_rewriter.cpp @@ -32,21 +32,21 @@ namespace datatypes { RewriteResponse DatatypesRewriter::postRewrite(TNode in) { Trace("datatypes-rewrite-debug") << "post-rewriting " << in << std::endl; - Kind k = in.getKind(); + Kind kind = in.getKind(); NodeManager* nm = NodeManager::currentNM(); - if (k == kind::APPLY_CONSTRUCTOR) + if (kind == kind::APPLY_CONSTRUCTOR) { return rewriteConstructor(in); } - else if (k == kind::APPLY_SELECTOR_TOTAL || k == kind::APPLY_SELECTOR) + else if (kind == kind::APPLY_SELECTOR_TOTAL || kind == kind::APPLY_SELECTOR) { return rewriteSelector(in); } - else if (k == kind::APPLY_TESTER) + else if (kind == kind::APPLY_TESTER) { return rewriteTester(in); } - else if (k == kind::DT_SIZE) + else if (kind == kind::DT_SIZE) { if (in[0].getKind() == kind::APPLY_CONSTRUCTOR) { @@ -72,7 +72,7 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in) return RewriteResponse(REWRITE_AGAIN_FULL, res); } } - else if (k == kind::DT_HEIGHT_BOUND) + else if (kind == kind::DT_HEIGHT_BOUND) { if (in[0].getKind() == kind::APPLY_CONSTRUCTOR) { @@ -106,7 +106,7 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in) return RewriteResponse(REWRITE_AGAIN_FULL, res); } } - else if (k == kind::DT_SIZE_BOUND) + else if (kind == kind::DT_SIZE_BOUND) { if (in[0].isConst()) { @@ -114,7 +114,7 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in) return RewriteResponse(REWRITE_AGAIN_FULL, res); } } - else if (k == DT_SYGUS_EVAL) + else if (kind == DT_SYGUS_EVAL) { // sygus evaluation function Node ev = in[0]; @@ -134,7 +134,7 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in) return RewriteResponse(REWRITE_AGAIN_FULL, ret); } } - else if (k == MATCH) + else if (kind == MATCH) { Trace("dt-rewrite-match") << "Rewrite match: " << in << std::endl; Node h = in[0]; @@ -223,7 +223,7 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in) return RewriteResponse(REWRITE_AGAIN_FULL, ret); } - if (k == kind::EQUAL) + if (kind == kind::EQUAL) { if (in[0] == in[1]) { diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp index 95b73b2fe..76832e369 100644 --- a/src/theory/datatypes/sygus_extension.cpp +++ b/src/theory/datatypes/sygus_extension.cpp @@ -271,9 +271,10 @@ void SygusExtension::assertTesterInternal( int tindex, TNode n, Node exp, std::v if( xa==a ){ IntMap::const_iterator ittv = d_testers.find( x ); Assert(ittv != d_testers.end()); - int tindex = (*ittv).second; + int tidx = (*ittv).second; const DType& dti = x.getType().getDType(); - if( dti[tindex].getNumArgs()>0 ){ + if (dti[tidx].getNumArgs() > 0) + { NodeMap::const_iterator itt = d_testers_exp.find( x ); Assert(itt != d_testers_exp.end()); conflict.push_back( (*itt).second ); diff --git a/src/theory/datatypes/sygus_simple_sym.cpp b/src/theory/datatypes/sygus_simple_sym.cpp index 21fb71bf7..06f1ea79c 100644 --- a/src/theory/datatypes/sygus_simple_sym.cpp +++ b/src/theory/datatypes/sygus_simple_sym.cpp @@ -178,8 +178,8 @@ bool SygusSimpleSymBreak::considerArgKind( // the argument types of the child must be the parent's type for (unsigned i = 0, nargs = dt[c].getNumArgs(); i < nargs; i++) { - TypeNode tn = dt[c].getArgType(i); - if (tn != tnp) + TypeNode type = dt[c].getArgType(i); + if (type != tnp) { return true; } diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 141c9476f..fc8dedbd3 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -226,20 +226,20 @@ void TheoryDatatypes::check(Effort e) { //otherwise, if the logic is quantified, under the assumption that all uninterpreted sorts have cardinality one, // infer the equality. for( unsigned i=0; i<dt.getNumRecursiveSingletonArgTypes( tt ); i++ ){ - TypeNode tn = dt.getRecursiveSingletonArgType(tt, i); + TypeNode type = dt.getRecursiveSingletonArgType(tt, i); if( getQuantifiersEngine() ){ // under the assumption that the cardinality of this type is one - Node a = getSingletonLemma( tn, true ); + Node a = getSingletonLemma(type, true); assumptions.push_back( a.negate() ); }else{ success = false; // assert that the cardinality of this type is more than one - getSingletonLemma( tn, false ); + getSingletonLemma(type, false); } } if( success ){ - Node eq = n.eqNode( itrs->second ); - assumptions.push_back( eq ); + Node assumption = n.eqNode(itrs->second); + assumptions.push_back(assumption); Node lemma = assumptions.size()==1 ? assumptions[0] : NodeManager::currentNM()->mkNode( OR, assumptions ); Trace("dt-singleton") << "*************Singleton equality lemma " << lemma << std::endl; doSendLemma( lemma ); @@ -414,8 +414,9 @@ void TheoryDatatypes::flushPendingFacts(){ lem = fact; }else{ std::vector< Node > children; - for( unsigned i=0; i<assumptions.size(); i++ ){ - children.push_back( assumptions[i].negate() ); + for (const TNode& assumption : assumptions) + { + children.push_back(assumption.negate()); } children.push_back( fact ); lem = NodeManager::currentNM()->mkNode( OR, children ); @@ -1341,19 +1342,19 @@ void TheoryDatatypes::collapseSelector( Node s, Node c ) { } if( use_s!=rrs ){ Node eq = use_s.eqNode( rrs ); - Node eq_exp; + Node peq; if( options::dtRefIntro() ){ - eq_exp = d_true; + peq = d_true; }else{ - eq_exp = c.eqNode( s[0] ); + peq = c.eqNode(s[0]); } Trace("datatypes-infer") << "DtInfer : collapse sel"; //Trace("datatypes-infer") << ( wrong ? " wrong" : ""); - Trace("datatypes-infer") << " : " << eq << " by " << eq_exp << std::endl; + Trace("datatypes-infer") << " : " << eq << " by " << peq << std::endl; d_pending.push_back( eq ); - d_pending_exp[ eq ] = eq_exp; + d_pending_exp[eq] = peq; d_infer.push_back( eq ); - d_infer_exp.push_back( eq_exp ); + d_infer_exp.push_back(peq); } } } @@ -2039,14 +2040,18 @@ Node TheoryDatatypes::searchForCycle( TNode n, TNode on, if( visited.find( nn ) == visited.end() ) { Trace("datatypes-cycle-check2") << " visit : " << nn << std::endl; visited[nn] = true; - TNode ncons = getEqcConstructor( nn ); - if( ncons.getKind()==APPLY_CONSTRUCTOR ) { - for( unsigned i=0; i<ncons.getNumChildren(); i++ ) { - TNode cn = searchForCycle( ncons[i], on, visited, proc, explanation, false ); + TNode nncons = getEqcConstructor(nn); + if (nncons.getKind() == APPLY_CONSTRUCTOR) + { + for (unsigned i = 0; i < nncons.getNumChildren(); i++) + { + TNode cn = + searchForCycle(nncons[i], on, visited, proc, explanation, false); if( cn==on ) { //add explanation for why the constructor is connected - if( n != ncons ) { - explainEquality( n, ncons, true, explanation ); + if (n != nncons) + { + explainEquality(n, nncons, true, explanation); } return on; }else if( !cn.isNull() ){ diff --git a/src/theory/datatypes/theory_datatypes_utils.cpp b/src/theory/datatypes/theory_datatypes_utils.cpp index cb9ab1e30..13cc8fc19 100644 --- a/src/theory/datatypes/theory_datatypes_utils.cpp +++ b/src/theory/datatypes/theory_datatypes_utils.cpp @@ -501,8 +501,8 @@ Node sygusToBuiltinEval(Node n, const std::vector<Node>& args) if (!svarsInit) { svarsInit = true; - TypeNode tn = cur.getType(); - Node varList = tn.getDType().getSygusVarList(); + TypeNode type = cur.getType(); + Node varList = type.getDType().getSygusVarList(); for (const Node& v : varList) { svars.push_back(v); diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp index e4e485fd9..665635c38 100644 --- a/src/theory/fp/fp_converter.cpp +++ b/src/theory/fp/fp_converter.cpp @@ -731,10 +731,10 @@ symbolicBitVector<isSigned> symbolicBitVector<isSigned>::extract( return symbolicBitVector<isSigned>(construct); } -floatingPointTypeInfo::floatingPointTypeInfo(const TypeNode t) - : FloatingPointSize(t.getConst<FloatingPointSize>()) +floatingPointTypeInfo::floatingPointTypeInfo(const TypeNode type) + : FloatingPointSize(type.getConst<FloatingPointSize>()) { - PRECONDITION(t.isFloatingPoint()); + PRECONDITION(type.isFloatingPoint()); } floatingPointTypeInfo::floatingPointTypeInfo(unsigned exp, unsigned sig) : FloatingPointSize(exp, sig) @@ -751,14 +751,14 @@ TypeNode floatingPointTypeInfo::getTypeNode(void) const } } -FpConverter::FpConverter(context::UserContext *user) +FpConverter::FpConverter(context::UserContext* user) : #ifdef CVC4_USE_SYMFPU - f(user), - r(user), - b(user), - u(user), - s(user), + d_fpMap(user), + d_rmMap(user), + d_boolMap(user), + d_ubvMap(user), + d_sbvMap(user), #endif d_additionalAssertions(user) { @@ -863,9 +863,9 @@ Node FpConverter::convert(TNode node) if (t.isRoundingMode()) { - rmMap::const_iterator i(r.find(current)); + rmMap::const_iterator i(d_rmMap.find(current)); - if (i == r.end()) + if (i == d_rmMap.end()) { if (Theory::isLeafOf(current, THEORY_FP)) { @@ -875,14 +875,20 @@ Node FpConverter::convert(TNode node) switch (current.getConst<RoundingMode>()) { case roundNearestTiesToEven: - r.insert(current, traits::RNE()); + d_rmMap.insert(current, traits::RNE()); break; case roundNearestTiesToAway: - r.insert(current, traits::RNA()); + d_rmMap.insert(current, traits::RNA()); + break; + case roundTowardPositive: + d_rmMap.insert(current, traits::RTP()); + break; + case roundTowardNegative: + d_rmMap.insert(current, traits::RTN()); + break; + case roundTowardZero: + d_rmMap.insert(current, traits::RTZ()); break; - case roundTowardPositive: r.insert(current, traits::RTP()); break; - case roundTowardNegative: r.insert(current, traits::RTN()); break; - case roundTowardZero: r.insert(current, traits::RTZ()); break; default: Unreachable() << "Unknown rounding mode"; break; } } @@ -890,7 +896,7 @@ Node FpConverter::convert(TNode node) { /******** Variables ********/ rm tmp(nm->mkNode(kind::ROUNDINGMODE_BITBLAST, current)); - r.insert(current, tmp); + d_rmMap.insert(current, tmp); d_additionalAssertions.push_back(tmp.valid()); } } @@ -903,23 +909,23 @@ Node FpConverter::convert(TNode node) } else if (t.isFloatingPoint()) { - fpMap::const_iterator i(f.find(current)); + fpMap::const_iterator i(d_fpMap.find(current)); - if (i == f.end()) + if (i == d_fpMap.end()) { if (Theory::isLeafOf(current, THEORY_FP)) { if (current.getKind() == kind::CONST_FLOATINGPOINT) { /******** Constants ********/ - f.insert(current, - symfpu::unpackedFloat<traits>( - current.getConst<FloatingPoint>().getLiteral())); + d_fpMap.insert(current, + symfpu::unpackedFloat<traits>( + current.getConst<FloatingPoint>().getLiteral())); } else { /******** Variables ********/ - f.insert(current, buildComponents(current)); + d_fpMap.insert(current, buildComponents(current)); } } else @@ -937,9 +943,9 @@ Node FpConverter::convert(TNode node) case kind::FLOATINGPOINT_ABS: case kind::FLOATINGPOINT_NEG: { - fpMap::const_iterator arg1(f.find(current[0])); + fpMap::const_iterator arg1(d_fpMap.find(current[0])); - if (arg1 == f.end()) + if (arg1 == d_fpMap.end()) { workStack.push_back(current); workStack.push_back(current[0]); @@ -949,14 +955,14 @@ Node FpConverter::convert(TNode node) switch (current.getKind()) { case kind::FLOATINGPOINT_ABS: - f.insert(current, - symfpu::absolute<traits>(fpt(current.getType()), - (*arg1).second)); + d_fpMap.insert(current, + symfpu::absolute<traits>( + fpt(current.getType()), (*arg1).second)); break; case kind::FLOATINGPOINT_NEG: - f.insert(current, - symfpu::negate<traits>(fpt(current.getType()), - (*arg1).second)); + d_fpMap.insert(current, + symfpu::negate<traits>(fpt(current.getType()), + (*arg1).second)); break; default: Unreachable() << "Unknown unary floating-point function"; @@ -968,18 +974,19 @@ Node FpConverter::convert(TNode node) case kind::FLOATINGPOINT_SQRT: case kind::FLOATINGPOINT_RTI: { - rmMap::const_iterator mode(r.find(current[0])); - fpMap::const_iterator arg1(f.find(current[1])); - bool recurseNeeded = (mode == r.end()) || (arg1 == f.end()); + rmMap::const_iterator mode(d_rmMap.find(current[0])); + fpMap::const_iterator arg1(d_fpMap.find(current[1])); + bool recurseNeeded = + (mode == d_rmMap.end()) || (arg1 == d_fpMap.end()); if (recurseNeeded) { workStack.push_back(current); - if (mode == r.end()) + if (mode == d_rmMap.end()) { workStack.push_back(current[0]); } - if (arg1 == f.end()) + if (arg1 == d_fpMap.end()) { workStack.push_back(current[1]); } @@ -989,13 +996,13 @@ Node FpConverter::convert(TNode node) switch (current.getKind()) { case kind::FLOATINGPOINT_SQRT: - f.insert(current, - symfpu::sqrt<traits>(fpt(current.getType()), - (*mode).second, - (*arg1).second)); + d_fpMap.insert(current, + symfpu::sqrt<traits>(fpt(current.getType()), + (*mode).second, + (*arg1).second)); break; case kind::FLOATINGPOINT_RTI: - f.insert( + d_fpMap.insert( current, symfpu::roundToIntegral<traits>(fpt(current.getType()), (*mode).second, @@ -1011,25 +1018,26 @@ Node FpConverter::convert(TNode node) case kind::FLOATINGPOINT_REM: { - fpMap::const_iterator arg1(f.find(current[0])); - fpMap::const_iterator arg2(f.find(current[1])); - bool recurseNeeded = (arg1 == f.end()) || (arg2 == f.end()); + fpMap::const_iterator arg1(d_fpMap.find(current[0])); + fpMap::const_iterator arg2(d_fpMap.find(current[1])); + bool recurseNeeded = + (arg1 == d_fpMap.end()) || (arg2 == d_fpMap.end()); if (recurseNeeded) { workStack.push_back(current); - if (arg1 == f.end()) + if (arg1 == d_fpMap.end()) { workStack.push_back(current[0]); } - if (arg2 == f.end()) + if (arg2 == d_fpMap.end()) { workStack.push_back(current[1]); } continue; // i.e. recurse! } - f.insert( + d_fpMap.insert( current, symfpu::remainder<traits>( fpt(current.getType()), (*arg1).second, (*arg2).second)); @@ -1039,20 +1047,21 @@ Node FpConverter::convert(TNode node) case kind::FLOATINGPOINT_MIN_TOTAL: case kind::FLOATINGPOINT_MAX_TOTAL: { - fpMap::const_iterator arg1(f.find(current[0])); - fpMap::const_iterator arg2(f.find(current[1])); + fpMap::const_iterator arg1(d_fpMap.find(current[0])); + fpMap::const_iterator arg2(d_fpMap.find(current[1])); // current[2] is a bit-vector so we do not need to recurse down it - bool recurseNeeded = (arg1 == f.end()) || (arg2 == f.end()); + bool recurseNeeded = + (arg1 == d_fpMap.end()) || (arg2 == d_fpMap.end()); if (recurseNeeded) { workStack.push_back(current); - if (arg1 == f.end()) + if (arg1 == d_fpMap.end()) { workStack.push_back(current[0]); } - if (arg2 == f.end()) + if (arg2 == d_fpMap.end()) { workStack.push_back(current[1]); } @@ -1062,19 +1071,19 @@ Node FpConverter::convert(TNode node) switch (current.getKind()) { case kind::FLOATINGPOINT_MAX_TOTAL: - f.insert(current, - symfpu::max<traits>(fpt(current.getType()), - (*arg1).second, - (*arg2).second, - prop(current[2]))); + d_fpMap.insert(current, + symfpu::max<traits>(fpt(current.getType()), + (*arg1).second, + (*arg2).second, + prop(current[2]))); break; case kind::FLOATINGPOINT_MIN_TOTAL: - f.insert(current, - symfpu::min<traits>(fpt(current.getType()), - (*arg1).second, - (*arg2).second, - prop(current[2]))); + d_fpMap.insert(current, + symfpu::min<traits>(fpt(current.getType()), + (*arg1).second, + (*arg2).second, + prop(current[2]))); break; default: @@ -1090,24 +1099,25 @@ Node FpConverter::convert(TNode node) case kind::FLOATINGPOINT_MULT: case kind::FLOATINGPOINT_DIV: { - rmMap::const_iterator mode(r.find(current[0])); - fpMap::const_iterator arg1(f.find(current[1])); - fpMap::const_iterator arg2(f.find(current[2])); - bool recurseNeeded = - (mode == r.end()) || (arg1 == f.end()) || (arg2 == f.end()); + rmMap::const_iterator mode(d_rmMap.find(current[0])); + fpMap::const_iterator arg1(d_fpMap.find(current[1])); + fpMap::const_iterator arg2(d_fpMap.find(current[2])); + bool recurseNeeded = (mode == d_rmMap.end()) + || (arg1 == d_fpMap.end()) + || (arg2 == d_fpMap.end()); if (recurseNeeded) { workStack.push_back(current); - if (mode == r.end()) + if (mode == d_rmMap.end()) { workStack.push_back(current[0]); } - if (arg1 == f.end()) + if (arg1 == d_fpMap.end()) { workStack.push_back(current[1]); } - if (arg2 == f.end()) + if (arg2 == d_fpMap.end()) { workStack.push_back(current[2]); } @@ -1117,12 +1127,12 @@ Node FpConverter::convert(TNode node) switch (current.getKind()) { case kind::FLOATINGPOINT_PLUS: - f.insert(current, - symfpu::add<traits>(fpt(current.getType()), - (*mode).second, - (*arg1).second, - (*arg2).second, - prop(true))); + d_fpMap.insert(current, + symfpu::add<traits>(fpt(current.getType()), + (*mode).second, + (*arg1).second, + (*arg2).second, + prop(true))); break; case kind::FLOATINGPOINT_SUB: @@ -1133,22 +1143,23 @@ Node FpConverter::convert(TNode node) break; case kind::FLOATINGPOINT_MULT: - f.insert(current, - symfpu::multiply<traits>(fpt(current.getType()), - (*mode).second, - (*arg1).second, - (*arg2).second)); + d_fpMap.insert( + current, + symfpu::multiply<traits>(fpt(current.getType()), + (*mode).second, + (*arg1).second, + (*arg2).second)); break; case kind::FLOATINGPOINT_DIV: - f.insert(current, - symfpu::divide<traits>(fpt(current.getType()), - (*mode).second, - (*arg1).second, - (*arg2).second)); + d_fpMap.insert(current, + symfpu::divide<traits>(fpt(current.getType()), + (*mode).second, + (*arg1).second, + (*arg2).second)); break; case kind::FLOATINGPOINT_REM: /* - f.insert(current, + d_fpMap.insert(current, symfpu::remainder<traits>(fpt(current.getType()), (*mode).second, (*arg1).second, @@ -1169,66 +1180,68 @@ Node FpConverter::convert(TNode node) case kind::FLOATINGPOINT_FMA: { - rmMap::const_iterator mode(r.find(current[0])); - fpMap::const_iterator arg1(f.find(current[1])); - fpMap::const_iterator arg2(f.find(current[2])); - fpMap::const_iterator arg3(f.find(current[3])); - bool recurseNeeded = (mode == r.end()) || (arg1 == f.end()) - || (arg2 == f.end() || (arg3 == f.end())); + rmMap::const_iterator mode(d_rmMap.find(current[0])); + fpMap::const_iterator arg1(d_fpMap.find(current[1])); + fpMap::const_iterator arg2(d_fpMap.find(current[2])); + fpMap::const_iterator arg3(d_fpMap.find(current[3])); + bool recurseNeeded = + (mode == d_rmMap.end()) || (arg1 == d_fpMap.end()) + || (arg2 == d_fpMap.end() || (arg3 == d_fpMap.end())); if (recurseNeeded) { workStack.push_back(current); - if (mode == r.end()) + if (mode == d_rmMap.end()) { workStack.push_back(current[0]); } - if (arg1 == f.end()) + if (arg1 == d_fpMap.end()) { workStack.push_back(current[1]); } - if (arg2 == f.end()) + if (arg2 == d_fpMap.end()) { workStack.push_back(current[2]); } - if (arg3 == f.end()) + if (arg3 == d_fpMap.end()) { workStack.push_back(current[3]); } continue; // i.e. recurse! } - f.insert(current, - symfpu::fma<traits>(fpt(current.getType()), - (*mode).second, - (*arg1).second, - (*arg2).second, - (*arg3).second)); + d_fpMap.insert(current, + symfpu::fma<traits>(fpt(current.getType()), + (*mode).second, + (*arg1).second, + (*arg2).second, + (*arg3).second)); } break; /******** Conversions ********/ case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT: { - rmMap::const_iterator mode(r.find(current[0])); - fpMap::const_iterator arg1(f.find(current[1])); - bool recurseNeeded = (mode == r.end()) || (arg1 == f.end()); + rmMap::const_iterator mode(d_rmMap.find(current[0])); + fpMap::const_iterator arg1(d_fpMap.find(current[1])); + bool recurseNeeded = + (mode == d_rmMap.end()) || (arg1 == d_fpMap.end()); if (recurseNeeded) { workStack.push_back(current); - if (mode == r.end()) + if (mode == d_rmMap.end()) { workStack.push_back(current[0]); } - if (arg1 == f.end()) + if (arg1 == d_fpMap.end()) { workStack.push_back(current[1]); } continue; // i.e. recurse! } - f.insert( + d_fpMap.insert( current, symfpu::convertFloatToFloat<traits>(fpt(current[1].getType()), fpt(current.getType()), @@ -1241,27 +1254,28 @@ Node FpConverter::convert(TNode node) { Node IEEEBV(nm->mkNode( kind::BITVECTOR_CONCAT, current[0], current[1], current[2])); - f.insert(current, - symfpu::unpack<traits>(fpt(current.getType()), IEEEBV)); + d_fpMap.insert( + current, + symfpu::unpack<traits>(fpt(current.getType()), IEEEBV)); } break; case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: - f.insert(current, - symfpu::unpack<traits>(fpt(current.getType()), - ubv(current[0]))); + d_fpMap.insert(current, + symfpu::unpack<traits>(fpt(current.getType()), + ubv(current[0]))); break; case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: { - rmMap::const_iterator mode(r.find(current[0])); - bool recurseNeeded = (mode == r.end()); + rmMap::const_iterator mode(d_rmMap.find(current[0])); + bool recurseNeeded = (mode == d_rmMap.end()); if (recurseNeeded) { workStack.push_back(current); - if (mode == r.end()) + if (mode == d_rmMap.end()) { workStack.push_back(current[0]); } @@ -1271,7 +1285,7 @@ Node FpConverter::convert(TNode node) switch (current.getKind()) { case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: - f.insert( + d_fpMap.insert( current, symfpu::convertSBVToFloat<traits>(fpt(current.getType()), (*mode).second, @@ -1279,7 +1293,7 @@ Node FpConverter::convert(TNode node) break; case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: - f.insert( + d_fpMap.insert( current, symfpu::convertUBVToFloat<traits>(fpt(current.getType()), (*mode).second, @@ -1296,7 +1310,7 @@ Node FpConverter::convert(TNode node) case kind::FLOATINGPOINT_TO_FP_REAL: { - f.insert(current, buildComponents(current)); + d_fpMap.insert(current, buildComponents(current)); // Rely on the real theory and theory combination // to handle the value } @@ -1316,9 +1330,9 @@ Node FpConverter::convert(TNode node) } else if (t.isBoolean()) { - boolMap::const_iterator i(b.find(current)); + boolMap::const_iterator i(d_boolMap.find(current)); - if (i == b.end()) + if (i == d_boolMap.end()) { switch (current.getKind()) { @@ -1329,49 +1343,52 @@ Node FpConverter::convert(TNode node) if (childType.isFloatingPoint()) { - fpMap::const_iterator arg1(f.find(current[0])); - fpMap::const_iterator arg2(f.find(current[1])); - bool recurseNeeded = (arg1 == f.end()) || (arg2 == f.end()); + fpMap::const_iterator arg1(d_fpMap.find(current[0])); + fpMap::const_iterator arg2(d_fpMap.find(current[1])); + bool recurseNeeded = + (arg1 == d_fpMap.end()) || (arg2 == d_fpMap.end()); if (recurseNeeded) { workStack.push_back(current); - if (arg1 == f.end()) + if (arg1 == d_fpMap.end()) { workStack.push_back(current[0]); } - if (arg2 == f.end()) + if (arg2 == d_fpMap.end()) { workStack.push_back(current[1]); } continue; // i.e. recurse! } - b.insert(current, - symfpu::smtlibEqual<traits>( - fpt(childType), (*arg1).second, (*arg2).second)); + d_boolMap.insert( + current, + symfpu::smtlibEqual<traits>( + fpt(childType), (*arg1).second, (*arg2).second)); } else if (childType.isRoundingMode()) { - rmMap::const_iterator arg1(r.find(current[0])); - rmMap::const_iterator arg2(r.find(current[1])); - bool recurseNeeded = (arg1 == r.end()) || (arg2 == r.end()); + rmMap::const_iterator arg1(d_rmMap.find(current[0])); + rmMap::const_iterator arg2(d_rmMap.find(current[1])); + bool recurseNeeded = + (arg1 == d_rmMap.end()) || (arg2 == d_rmMap.end()); if (recurseNeeded) { workStack.push_back(current); - if (arg1 == r.end()) + if (arg1 == d_rmMap.end()) { workStack.push_back(current[0]); } - if (arg2 == r.end()) + if (arg2 == d_rmMap.end()) { workStack.push_back(current[1]); } continue; // i.e. recurse! } - b.insert(current, (*arg1).second == (*arg2).second); + d_boolMap.insert(current, (*arg1).second == (*arg2).second); } else { @@ -1386,18 +1403,19 @@ Node FpConverter::convert(TNode node) { TypeNode childType(current[0].getType()); - fpMap::const_iterator arg1(f.find(current[0])); - fpMap::const_iterator arg2(f.find(current[1])); - bool recurseNeeded = (arg1 == f.end()) || (arg2 == f.end()); + fpMap::const_iterator arg1(d_fpMap.find(current[0])); + fpMap::const_iterator arg2(d_fpMap.find(current[1])); + bool recurseNeeded = + (arg1 == d_fpMap.end()) || (arg2 == d_fpMap.end()); if (recurseNeeded) { workStack.push_back(current); - if (arg1 == f.end()) + if (arg1 == d_fpMap.end()) { workStack.push_back(current[0]); } - if (arg2 == f.end()) + if (arg2 == d_fpMap.end()) { workStack.push_back(current[1]); } @@ -1407,15 +1425,17 @@ Node FpConverter::convert(TNode node) switch (current.getKind()) { case kind::FLOATINGPOINT_LEQ: - b.insert(current, - symfpu::lessThanOrEqual<traits>( - fpt(childType), (*arg1).second, (*arg2).second)); + d_boolMap.insert( + current, + symfpu::lessThanOrEqual<traits>( + fpt(childType), (*arg1).second, (*arg2).second)); break; case kind::FLOATINGPOINT_LT: - b.insert(current, - symfpu::lessThan<traits>( - fpt(childType), (*arg1).second, (*arg2).second)); + d_boolMap.insert( + current, + symfpu::lessThan<traits>( + fpt(childType), (*arg1).second, (*arg2).second)); break; default: @@ -1434,9 +1454,9 @@ Node FpConverter::convert(TNode node) case kind::FLOATINGPOINT_ISPOS: { TypeNode childType(current[0].getType()); - fpMap::const_iterator arg1(f.find(current[0])); + fpMap::const_iterator arg1(d_fpMap.find(current[0])); - if (arg1 == f.end()) + if (arg1 == d_fpMap.end()) { workStack.push_back(current); workStack.push_back(current[0]); @@ -1446,42 +1466,43 @@ Node FpConverter::convert(TNode node) switch (current.getKind()) { case kind::FLOATINGPOINT_ISN: - b.insert( + d_boolMap.insert( current, symfpu::isNormal<traits>(fpt(childType), (*arg1).second)); break; case kind::FLOATINGPOINT_ISSN: - b.insert(current, - symfpu::isSubnormal<traits>(fpt(childType), - (*arg1).second)); + d_boolMap.insert(current, + symfpu::isSubnormal<traits>(fpt(childType), + (*arg1).second)); break; case kind::FLOATINGPOINT_ISZ: - b.insert( + d_boolMap.insert( current, symfpu::isZero<traits>(fpt(childType), (*arg1).second)); break; case kind::FLOATINGPOINT_ISINF: - b.insert( + d_boolMap.insert( current, symfpu::isInfinite<traits>(fpt(childType), (*arg1).second)); break; case kind::FLOATINGPOINT_ISNAN: - b.insert(current, - symfpu::isNaN<traits>(fpt(childType), (*arg1).second)); + d_boolMap.insert( + current, + symfpu::isNaN<traits>(fpt(childType), (*arg1).second)); break; case kind::FLOATINGPOINT_ISPOS: - b.insert( + d_boolMap.insert( current, symfpu::isPositive<traits>(fpt(childType), (*arg1).second)); break; case kind::FLOATINGPOINT_ISNEG: - b.insert( + d_boolMap.insert( current, symfpu::isNegative<traits>(fpt(childType), (*arg1).second)); break; @@ -1513,7 +1534,7 @@ Node FpConverter::convert(TNode node) break; } - i = b.find(current); + i = d_boolMap.find(current); } result = (*i).second; @@ -1526,22 +1547,23 @@ Node FpConverter::convert(TNode node) case kind::FLOATINGPOINT_TO_UBV_TOTAL: { TypeNode childType(current[1].getType()); - ubvMap::const_iterator i(u.find(current)); + ubvMap::const_iterator i(d_ubvMap.find(current)); - if (i == u.end()) + if (i == d_ubvMap.end()) { - rmMap::const_iterator mode(r.find(current[0])); - fpMap::const_iterator arg1(f.find(current[1])); - bool recurseNeeded = (mode == r.end()) || (arg1 == f.end()); + rmMap::const_iterator mode(d_rmMap.find(current[0])); + fpMap::const_iterator arg1(d_fpMap.find(current[1])); + bool recurseNeeded = + (mode == d_rmMap.end()) || (arg1 == d_fpMap.end()); if (recurseNeeded) { workStack.push_back(current); - if (mode == r.end()) + if (mode == d_rmMap.end()) { workStack.push_back(current[0]); } - if (arg1 == f.end()) + if (arg1 == d_fpMap.end()) { workStack.push_back(current[1]); } @@ -1551,13 +1573,13 @@ Node FpConverter::convert(TNode node) FloatingPointToUBVTotal info = current.getOperator().getConst<FloatingPointToUBVTotal>(); - u.insert(current, - symfpu::convertFloatToUBV<traits>(fpt(childType), - (*mode).second, - (*arg1).second, - info.bvs, - ubv(current[2]))); - i = u.find(current); + d_ubvMap.insert(current, + symfpu::convertFloatToUBV<traits>(fpt(childType), + (*mode).second, + (*arg1).second, + info.bvs, + ubv(current[2]))); + i = d_ubvMap.find(current); } result = (*i).second; @@ -1567,22 +1589,23 @@ Node FpConverter::convert(TNode node) case kind::FLOATINGPOINT_TO_SBV_TOTAL: { TypeNode childType(current[1].getType()); - sbvMap::const_iterator i(s.find(current)); + sbvMap::const_iterator i(d_sbvMap.find(current)); - if (i == s.end()) + if (i == d_sbvMap.end()) { - rmMap::const_iterator mode(r.find(current[0])); - fpMap::const_iterator arg1(f.find(current[1])); - bool recurseNeeded = (mode == r.end()) || (arg1 == f.end()); + rmMap::const_iterator mode(d_rmMap.find(current[0])); + fpMap::const_iterator arg1(d_fpMap.find(current[1])); + bool recurseNeeded = + (mode == d_rmMap.end()) || (arg1 == d_fpMap.end()); if (recurseNeeded) { workStack.push_back(current); - if (mode == r.end()) + if (mode == d_rmMap.end()) { workStack.push_back(current[0]); } - if (arg1 == f.end()) + if (arg1 == d_fpMap.end()) { workStack.push_back(current[1]); } @@ -1592,14 +1615,14 @@ Node FpConverter::convert(TNode node) FloatingPointToSBVTotal info = current.getOperator().getConst<FloatingPointToSBVTotal>(); - s.insert(current, - symfpu::convertFloatToSBV<traits>(fpt(childType), - (*mode).second, - (*arg1).second, - info.bvs, - sbv(current[2]))); + d_sbvMap.insert(current, + symfpu::convertFloatToSBV<traits>(fpt(childType), + (*mode).second, + (*arg1).second, + info.bvs, + sbv(current[2]))); - i = s.find(current); + i = d_sbvMap.find(current); } result = (*i).second; @@ -1639,9 +1662,9 @@ Node FpConverter::convert(TNode node) // (via auxiliary constraints) TypeNode childType(current[0].getType()); - fpMap::const_iterator arg1(f.find(current[0])); + fpMap::const_iterator arg1(d_fpMap.find(current[0])); - if (arg1 == f.end()) + if (arg1 == d_fpMap.end()) { workStack.push_back(current); workStack.push_back(current[0]); @@ -1689,9 +1712,9 @@ Node FpConverter::getValue(Valuation &val, TNode var) if (t.isRoundingMode()) { - rmMap::const_iterator i(r.find(var)); + rmMap::const_iterator i(d_rmMap.find(var)); - if (i == r.end()) + if (i == d_rmMap.end()) { Unreachable() << "Asking for the value of an unregistered expression"; } @@ -1703,9 +1726,9 @@ Node FpConverter::getValue(Valuation &val, TNode var) } else if (t.isFloatingPoint()) { - fpMap::const_iterator i(f.find(var)); + fpMap::const_iterator i(d_fpMap.find(var)); - if (i == f.end()) + if (i == d_fpMap.end()) { Unreachable() << "Asking for the value of an unregistered expression"; } diff --git a/src/theory/fp/fp_converter.h b/src/theory/fp/fp_converter.h index 8ff5293e2..344dcf926 100644 --- a/src/theory/fp/fp_converter.h +++ b/src/theory/fp/fp_converter.h @@ -318,11 +318,11 @@ class FpConverter typedef context::CDHashMap<Node, ubv, NodeHashFunction> ubvMap; typedef context::CDHashMap<Node, sbv, NodeHashFunction> sbvMap; - fpMap f; - rmMap r; - boolMap b; - ubvMap u; - sbvMap s; + fpMap d_fpMap; + rmMap d_rmMap; + boolMap d_boolMap; + ubvMap d_ubvMap; + sbvMap d_sbvMap; /* These functions take a symfpu object and convert it to a node. * These should ensure that constant folding it will give a diff --git a/src/theory/idl/idl_model.cpp b/src/theory/idl/idl_model.cpp index 729a18ee4..4a3426222 100644 --- a/src/theory/idl/idl_model.cpp +++ b/src/theory/idl/idl_model.cpp @@ -22,42 +22,52 @@ using namespace theory; using namespace idl; IDLModel::IDLModel(context::Context* context) -: d_model(context) -, d_reason(context) -{} + : d_model(context), d_reason(context) +{ +} -Integer IDLModel::getValue(TNode var) const { +Integer IDLModel::getValue(TNode var) const +{ model_value_map::const_iterator find = d_model.find(var); - if (find != d_model.end()) { + if (find != d_model.end()) + { return (*find).second; - } else { + } + else + { return 0; } } -void IDLModel::setValue(TNode var, Integer value, IDLReason reason) { - Assert(!reason.constraint.isNull()); +void IDLModel::setValue(TNode var, Integer value, IDLReason reason) +{ + Assert(!reason.d_constraint.isNull()); d_model[var] = value; d_reason[var] = reason; } -void IDLModel::getReasonCycle(TNode var, std::vector<TNode>& reasons) { +void IDLModel::getReasonCycle(TNode var, std::vector<TNode>& reasons) +{ TNode current = var; - do { + do + { Debug("theory::idl::model") << "processing: " << var << std::endl; Assert(d_reason.find(current) != d_reason.end()); IDLReason reason = d_reason[current]; - Debug("theory::idl::model") << "adding reason: " << reason.constraint << std::endl; - reasons.push_back(reason.constraint); - current = reason.x; + Debug("theory::idl::model") + << "adding reason: " << reason.d_constraint << std::endl; + reasons.push_back(reason.d_constraint); + current = reason.d_x; } while (current != var); } -void IDLModel::toStream(std::ostream& out) const { +void IDLModel::toStream(std::ostream& out) const +{ model_value_map::const_iterator it = d_model.begin(); model_value_map::const_iterator it_end = d_model.end(); out << "Model[" << std::endl; - for (; it != it_end; ++ it) { + for (; it != it_end; ++it) + { out << (*it).first << " -> " << (*it).second << std::endl; } out << "]"; diff --git a/src/theory/idl/idl_model.h b/src/theory/idl/idl_model.h index 87e67edea..610b90695 100644 --- a/src/theory/idl/idl_model.h +++ b/src/theory/idl/idl_model.h @@ -17,8 +17,8 @@ #pragma once -#include "expr/node.h" #include "context/cdhashmap.h" +#include "expr/node.h" namespace CVC4 { namespace theory { @@ -30,14 +30,14 @@ namespace idl { * value of x is 0, then the variable x and the constraint (y > 0) are a reason * for the y taking the value 1. */ -struct IDLReason { +struct IDLReason +{ /** The variable of the reason */ - TNode x; + TNode d_x; /** The constraint of the reason */ - TNode constraint; + TNode d_constraint; - IDLReason(TNode x, TNode constraint) - : x(x), constraint(constraint) {} + IDLReason(TNode x, TNode constraint) : d_x(x), d_constraint(constraint) {} IDLReason() {} }; @@ -45,10 +45,11 @@ struct IDLReason { * A model maps variables to integer values and backs them up with reasons. * Default values (if not set with setValue) for all variables are 0. */ -class IDLModel { - +class IDLModel +{ typedef context::CDHashMap<TNode, Integer, TNodeHashFunction> model_value_map; - typedef context::CDHashMap<TNode, IDLReason, TNodeHashFunction> model_reason_map; + typedef context::CDHashMap<TNode, IDLReason, TNodeHashFunction> + model_reason_map; /** Values assigned to individual variables */ model_value_map d_model; @@ -56,8 +57,7 @@ class IDLModel { /** Reasons constraining the individual variables */ model_reason_map d_reason; -public: - + public: IDLModel(context::Context* context); /** Get the model value of the variable */ @@ -71,14 +71,14 @@ public: /** Output to the given stream */ void toStream(std::ostream& out) const; - }; -inline std::ostream& operator << (std::ostream& out, const IDLModel& model) { +inline std::ostream& operator<<(std::ostream& out, const IDLModel& model) +{ model.toStream(out); return out; } -} -} -} +} // namespace idl +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp index 9e6e4842f..f9bf9335e 100644 --- a/src/theory/quantifiers/alpha_equivalence.cpp +++ b/src/theory/quantifiers/alpha_equivalence.cpp @@ -39,31 +39,40 @@ Node AlphaEquivalenceNode::registerNode(Node q, Node t) std::map< Node, bool > visited; while( !tt.empty() ){ if( tt.size()==arg_index.size()+1 ){ - Node t = tt.back(); + Node tb = tt.back(); Node op; - if( t.hasOperator() ){ - if( visited.find( t )==visited.end() ){ - visited[t] = true; - op = t.getOperator(); + if (tb.hasOperator()) + { + if (visited.find(tb) == visited.end()) + { + visited[tb] = true; + op = tb.getOperator(); arg_index.push_back( 0 ); - }else{ - op = t; + } + else + { + op = tb; arg_index.push_back( -1 ); } - }else{ - op = t; + } + else + { + op = tb; arg_index.push_back( 0 ); } Trace("aeq-debug") << op << " "; - aen = &(aen->d_children[op][t.getNumChildren()]); + aen = &(aen->d_children[op][tb.getNumChildren()]); }else{ - Node t = tt.back(); + Node tb = tt.back(); int i = arg_index.back(); - if( i==-1 || i==(int)t.getNumChildren() ){ + if (i == -1 || i == (int)tb.getNumChildren()) + { tt.pop_back(); arg_index.pop_back(); - }else{ - tt.push_back( t[i] ); + } + else + { + tt.push_back(tb[i]); arg_index[arg_index.size()-1]++; } } diff --git a/src/theory/quantifiers/anti_skolem.cpp b/src/theory/quantifiers/anti_skolem.cpp index cdb15b349..5604d5760 100644 --- a/src/theory/quantifiers/anti_skolem.cpp +++ b/src/theory/quantifiers/anti_skolem.cpp @@ -229,10 +229,10 @@ bool QuantAntiSkolem::sendAntiSkolemizeLemma( std::vector< Node >& quants, bool std::vector< Node > outer_vars; std::vector< Node > inner_vars; - Node q = quants[0]; - for (unsigned i = 0, size = d_ask_types[q].size(); i < size; i++) + Node q0 = quants[0]; + for (unsigned i = 0, size = d_ask_types[q0].size(); i < size; i++) { - Node v = NodeManager::currentNM()->mkBoundVar( d_ask_types[q][i] ); + Node v = NodeManager::currentNM()->mkBoundVar(d_ask_types[q0][i]); Trace("anti-sk-debug") << "Outer var " << i << " : " << v << std::endl; outer_vars.push_back( v ); } diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp index 24e3a85b5..c349e05b0 100644 --- a/src/theory/quantifiers/bv_inverter.cpp +++ b/src/theory/quantifiers/bv_inverter.cpp @@ -150,7 +150,7 @@ Node BvInverter::getPathToPv( { children.push_back(lit.getOperator()); } - for (size_t j = 0, num = lit.getNumChildren(); j < num; j++) + for (size_t j = 0, num2 = lit.getNumChildren(); j < num2; j++) { children.push_back(j == ii ? litc : lit[j]); } diff --git a/src/theory/quantifiers/candidate_rewrite_filter.cpp b/src/theory/quantifiers/candidate_rewrite_filter.cpp index 8db0501f5..43edb89bf 100644 --- a/src/theory/quantifiers/candidate_rewrite_filter.cpp +++ b/src/theory/quantifiers/candidate_rewrite_filter.cpp @@ -248,9 +248,9 @@ bool CandidateRewriteFilter::notify(Node s, #endif // must convert the inferred substitution to original form std::vector<Node> esubs; - for (const Node& s : subs) + for (const Node& sb : subs) { - esubs.push_back(d_drewrite->toExternal(s)); + esubs.push_back(d_drewrite->toExternal(sb)); } Assert(it != d_pairs.end()); for (const Node& nr : it->second) diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index bdab6810c..b82b958af 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -265,24 +265,32 @@ TNode ConjectureGenerator::getUniversalRepresentative( TNode n, bool add ) { if( !eq_terms.empty() ){ Trace("thm-ee-add") << "UEE : Based on ground EE/theorem DB, it is equivalent to " << eq_terms.size() << " terms : " << std::endl; //add equivalent terms as equalities to universal engine - for( unsigned i=0; i<eq_terms.size(); i++ ){ - Trace("thm-ee-add") << " " << eq_terms[i] << std::endl; + for (const Node& eqt : eq_terms) + { + Trace("thm-ee-add") << " " << eqt << std::endl; bool assertEq = false; - if( d_urelevant_terms.find( eq_terms[i] )!=d_urelevant_terms.end() ){ + if (d_urelevant_terms.find(eqt) != d_urelevant_terms.end()) + { assertEq = true; - }else{ - Assert(eq_terms[i].getType() == tn); - registerPattern( eq_terms[i], tn ); - if( isUniversalLessThan( eq_terms[i], t ) || ( options::conjectureUeeIntro() && d_pattern_fun_sum[t]>=d_pattern_fun_sum[eq_terms[i]] ) ){ - setUniversalRelevant( eq_terms[i] ); + } + else + { + Assert(eqt.getType() == tn); + registerPattern(eqt, tn); + if (isUniversalLessThan(eqt, t) + || (options::conjectureUeeIntro() + && d_pattern_fun_sum[t] >= d_pattern_fun_sum[eqt])) + { + setUniversalRelevant(eqt); assertEq = true; } } if( assertEq ){ Node exp; - d_uequalityEngine.assertEquality( t.eqNode( eq_terms[i] ), true, exp ); + d_uequalityEngine.assertEquality(t.eqNode(eqt), true, exp); }else{ - Trace("thm-ee-no-add") << "Do not add : " << t << " == " << eq_terms[i] << std::endl; + Trace("thm-ee-no-add") + << "Do not add : " << t << " == " << eqt << std::endl; } } }else{ @@ -467,8 +475,9 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e) if( n.hasOperator() ){ Trace("sg-gen-eqc") << " (" << n.getOperator(); getTermDatabase()->computeArgReps( n ); - for( unsigned i=0; i<getTermDatabase()->d_arg_reps[n].size(); i++ ){ - Trace("sg-gen-eqc") << " e" << d_em[getTermDatabase()->d_arg_reps[n][i]]; + for (TNode ar : getTermDatabase()->d_arg_reps[n]) + { + Trace("sg-gen-eqc") << " e" << d_em[ar]; } Trace("sg-gen-eqc") << ") :: " << n << std::endl; }else{ @@ -549,16 +558,20 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e) inEe = d_ee_conjectures.find( q[1] )!=d_ee_conjectures.end(); if( !inEe ){ //add to universal equality engine - Node nl = getUniversalRepresentative( eq[0], true ); - Node nr = getUniversalRepresentative( eq[1], true ); - if( areUniversalEqual( nl, nr ) ){ + Node nlu = getUniversalRepresentative(eq[0], true); + Node nru = getUniversalRepresentative(eq[1], true); + if (areUniversalEqual(nlu, nru)) + { isSubsume = true; //set inactive (will be ignored by other modules) d_quantEngine->getModel()->setQuantifierActive( q, false ); - }else{ + } + else + { Node exp; d_ee_conjectures[q[1]] = true; - d_uequalityEngine.assertEquality( nl.eqNode( nr ), true, exp ); + d_uequalityEngine.assertEquality( + nlu.eqNode(nru), true, exp); } } Trace("sg-conjecture") << "*** CONJECTURE : currently proven" << (isSubsume ? " and subsumed" : ""); @@ -589,8 +602,7 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e) std::vector< Node > ce; for (unsigned j = 0; j < skolems.size(); j++) { - TNode k = skolems[j]; - TNode rk = getRepresentative( k ); + TNode rk = getRepresentative(skolems[j]); std::map< TNode, Node >::iterator git = d_ground_eqc_map.find( rk ); //check if it is a ground term if( git==d_ground_eqc_map.end() ){ @@ -613,8 +625,9 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e) } if( disproven ){ Trace("sg-conjecture") << "disproven : " << q << " : "; - for( unsigned i=0; i<ce.size(); i++ ){ - Trace("sg-conjecture") << q[0][i] << " -> " << ce[i] << " "; + for (unsigned j = 0, ceSize = ce.size(); j < ceSize; j++) + { + Trace("sg-conjecture") << q[0][j] << " -> " << ce[j] << " "; } Trace("sg-conjecture") << std::endl; } @@ -900,9 +913,9 @@ unsigned ConjectureGenerator::flushWaitingConjectures( unsigned& addedLemmas, in for (const std::pair<TypeNode, unsigned>& lhs_pattern : d_pattern_var_id[lhs]) { - for (unsigned i = 0; i <= lhs_pattern.second; i++) + for (unsigned j = 0; j <= lhs_pattern.second; j++) { - bvs.push_back(getFreeVar(lhs_pattern.first, i)); + bvs.push_back(getFreeVar(lhs_pattern.first, j)); } } Node rsg; @@ -1159,9 +1172,10 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector< children.push_back( nn ); } children.push_back( lc ); - Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children ); - Trace("sg-gt-enum") << "Ground term enumerate : " << n << std::endl; - terms.push_back( n ); + Node nenum = NodeManager::currentNM()->mkNode(APPLY_UF, children); + Trace("sg-gt-enum") + << "Ground term enumerate : " << nenum << std::endl; + terms.push_back(nenum); } // pop the index for the last child vec.pop_back(); diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp index b01d5e1df..953121167 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.cpp +++ b/src/theory/quantifiers/ematching/ho_trigger.cpp @@ -112,7 +112,7 @@ void HigherOrderTrigger::collectHoVarApplyTerms( bool curWithinApply = withinApply[cur]; visited[cur] = Node::null(); visit.push_back(cur); - for (unsigned j = 0, size = cur.getNumChildren(); j < size; j++) + for (unsigned j = 0, sizec = cur.getNumChildren(); j < sizec; j++) { withinApply[cur[j]] = curWithinApply && j == 0; visit.push_back(cur[j]); @@ -486,7 +486,7 @@ int HigherOrderTrigger::addHoTypeMatchPredicateLemmas() // for each function type suffix of the type of f, for example if // f : (Int -> (Int -> Int)) // we iterate with stn = (Int -> (Int -> Int)) and (Int -> Int) - for (unsigned a = 0, size = argTypes.size(); a < size; a++) + for (unsigned a = 0, arg_size = argTypes.size(); a < arg_size; a++) { std::vector<TypeNode> sargts; sargts.insert(sargts.begin(), argTypes.begin() + a, argTypes.end()); diff --git a/src/theory/quantifiers/expr_miner.h b/src/theory/quantifiers/expr_miner.h index 4625e762a..08d7f40b1 100644 --- a/src/theory/quantifiers/expr_miner.h +++ b/src/theory/quantifiers/expr_miner.h @@ -20,6 +20,7 @@ #include <map> #include <memory> #include <vector> + #include "expr/expr.h" #include "expr/expr_manager.h" #include "expr/variable_type_map.h" diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp index 9e924f34d..44d3666e8 100644 --- a/src/theory/quantifiers/extended_rewrite.cpp +++ b/src/theory/quantifiers/extended_rewrite.cpp @@ -1254,7 +1254,7 @@ Node ExtendedRewriter::extendedRewriteEqChain( // x = ( y & x ) ---> y | ~x // x = ( y & ~x ) ---> ~y & ~x std::vector<Node> new_children; - for (unsigned k = 0, nchild = c.getNumChildren(); k < nchild; k++) + for (unsigned k = 0, nchildc = c.getNumChildren(); k < nchildc; k++) { if (j != k) { @@ -1515,10 +1515,10 @@ Node ExtendedRewriter::partialSubstitute(Node n, if (it == visited.end()) { - std::map<Node, Node>::iterator it = assign.find(cur); - if (it != assign.end()) + std::map<Node, Node>::iterator ita = assign.find(cur); + if (ita != assign.end()) { - visited[cur] = it->second; + visited[cur] = ita->second; } else { diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index 2bcb154a0..601452c1f 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -437,11 +437,13 @@ void BoundedIntegers::checkOwnership(Node f) } }else if( d_bound_type[f][v]==BOUND_FIXED_SET ){ Trace("bound-int") << " " << v << " in { "; - for( unsigned i=0; i<d_fixed_set_ngr_range[f][v].size(); i++ ){ - Trace("bound-int") << d_fixed_set_ngr_range[f][v][i] << " "; + for (TNode fnr : d_fixed_set_ngr_range[f][v]) + { + Trace("bound-int") << fnr << " "; } - for( unsigned i=0; i<d_fixed_set_gr_range[f][v].size(); i++ ){ - Trace("bound-int") << d_fixed_set_gr_range[f][v][i] << " "; + for (TNode fgr : d_fixed_set_gr_range[f][v]) + { + Trace("bound-int") << fgr << " "; } Trace("bound-int") << "}" << std::endl; }else if( d_bound_type[f][v]==BOUND_FINITE ){ @@ -705,9 +707,9 @@ bool BoundedIntegers::getRsiSubsitution( Node q, Node v, std::vector< Node >& va for( int i=0; i<vindex; i++) { Assert(d_set_nums[q][d_set[q][i]] == i); Trace("bound-int-rsi") << "Look up the value for " << d_set[q][i] << " " << i << std::endl; - int v = rsi->getVariableOrder( i ); - Assert(q[0][v] == d_set[q][i]); - Node t = rsi->getCurrentTerm(v, true); + int vo = rsi->getVariableOrder(i); + Assert(q[0][vo] == d_set[q][i]); + Node t = rsi->getCurrentTerm(vo, true); Trace("bound-int-rsi") << "term : " << t << std::endl; vars.push_back( d_set[q][i] ); subs.push_back( t ); diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index 206c8f9dd..3e5d36a7d 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -431,8 +431,9 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){ children.push_back(op); entry_children.push_back(op); bool hasNonStar = false; - for( unsigned i=0; i<c.getNumChildren(); i++) { - Node ri = fm->getRepresentative( c[i] ); + for (const Node& ci : c) + { + Node ri = fm->getRepresentative(ci); children.push_back(ri); bool isStar = false; if (fm->isModelBasisTerm(ri)) @@ -445,7 +446,9 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){ hasNonStar = true; } if( !isStar && !ri.isConst() ){ - Trace("fmc-warn") << "Warning : model for " << op << " has non-constant argument in model " << ri << " (from " << c[i] << ")" << std::endl; + Trace("fmc-warn") << "Warning : model for " << op + << " has non-constant argument in model " << ri + << " (from " << ci << ")" << std::endl; Assert(false); } entry_children.push_back(ri); diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp index a6e1a369c..5ae05f2a7 100644 --- a/src/theory/quantifiers/fmf/model_builder.cpp +++ b/src/theory/quantifiers/fmf/model_builder.cpp @@ -64,8 +64,9 @@ bool QModelBuilder::preProcessBuildModelStd(TheoryModel* m) { if( fm->isQuantifierActive( q ) ){ //check if any of these quantified formulas can be set inactive if( options::fmfEmptySorts() ){ - for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ - TypeNode tn = q[0][i].getType(); + for (const Node& var : q[0]) + { + TypeNode tn = var.getType(); //we are allowed to assume the type is empty if( tn.isSort() && eqc_usort.find( tn )==eqc_usort.end() ){ Trace("model-engine-debug") << "Empty domain quantified formula : " << q << std::endl; diff --git a/src/theory/quantifiers/fun_def_evaluator.cpp b/src/theory/quantifiers/fun_def_evaluator.cpp index c2baf8be6..0b48b3995 100644 --- a/src/theory/quantifiers/fun_def_evaluator.cpp +++ b/src/theory/quantifiers/fun_def_evaluator.cpp @@ -187,9 +187,9 @@ Node FunDefEvaluator::evaluate(Node n) const { Trace("fd-eval-debug2") << "FunDefEvaluator: evaluation with args:\n"; - for (const Node& child : children) + for (const Node& ch : children) { - Trace("fd-eval-debug2") << "..." << child << "\n"; + Trace("fd-eval-debug2") << "..." << ch << "\n"; } Trace("fd-eval-debug2") << "FunDefEvaluator: results in " << sbody << "\n"; diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp index fecefb8e1..0339b54f5 100644 --- a/src/theory/quantifiers/fun_def_process.cpp +++ b/src/theory/quantifiers/fun_def_process.cpp @@ -33,6 +33,7 @@ void FunDefFmf::simplify( std::vector< Node >& assertions ) { std::vector< int > fd_assertions; std::map< int, Node > subs_head; //first pass : find defined functions, transform quantifiers + NodeManager* nm = NodeManager::currentNM(); for( unsigned i=0; i<assertions.size(); i++ ){ Node n = QuantAttributes::getFunDefHead( assertions[i] ); if( !n.isNull() ){ @@ -62,9 +63,10 @@ void FunDefFmf::simplify( std::vector< Node >& assertions ) { //create functions f1...fn mapping from this sort to concrete elements for( unsigned j=0; j<n.getNumChildren(); j++ ){ TypeNode typ = NodeManager::currentNM()->mkFunctionType( iType, n[j].getType() ); - std::stringstream ss; - ss << f << "_arg_" << j; - d_input_arg_inj[f].push_back( NodeManager::currentNM()->mkSkolem( ss.str(), typ, "op created during fun def fmf" ) ); + std::stringstream ssf; + ssf << f << "_arg_" << j; + d_input_arg_inj[f].push_back( + nm->mkSkolem(ssf.str(), typ, "op created during fun def fmf")); } //construct new quantifier forall S. F[f1(S)/x1....fn(S)/xn] diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index aed2ae429..1607dc0dc 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -474,14 +474,14 @@ Node QuantifiersRewriter::computeProcessTerms2(Node body, { bool doRewrite = options::iteLiftQuant() == options::IteLiftQuantMode::ALL; - std::vector<Node> children; - children.push_back(ret[i][0]); + std::vector<Node> childrenIte; + childrenIte.push_back(ret[i][0]); for (size_t j = 1; j <= 2; j++) { // check if it rewrites to a constant Node nn = nm->mkNode(EQUAL, no, ret[i][j]); nn = Rewriter::rewrite(nn); - children.push_back(nn); + childrenIte.push_back(nn); if (nn.isConst()) { doRewrite = true; @@ -489,7 +489,7 @@ Node QuantifiersRewriter::computeProcessTerms2(Node body, } if (doRewrite) { - ret = nm->mkNode(ITE, children); + ret = nm->mkNode(ITE, childrenIte); break; } } @@ -1588,6 +1588,7 @@ Node QuantifiersRewriter::computeSplit( std::vector< Node >& args, Node body, QA } } if ( eqc_active>1 || !lits.empty() || var_to_eqc.size()!=args.size() ){ + NodeManager* nm = NodeManager::currentNM(); Trace("clause-split-debug") << "Split quantified formula with body " << body << std::endl; Trace("clause-split-debug") << " Ground literals: " << std::endl; for( size_t i=0; i<lits.size(); i++) { @@ -1607,8 +1608,9 @@ Node QuantifiersRewriter::computeSplit( std::vector< Node >& args, Node body, QA } Trace("clause-split-debug") << std::endl; Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, eqc_to_var[eqc]); - Node body = it->second.size()==1 ? it->second[0] : NodeManager::currentNM()->mkNode( OR, it->second ); - Node fa = NodeManager::currentNM()->mkNode( FORALL, bvl, body ); + Node bd = + it->second.size() == 1 ? it->second[0] : nm->mkNode(OR, it->second); + Node fa = nm->mkNode(FORALL, bvl, bd); lits.push_back(fa); } Assert(!lits.empty()); diff --git a/src/theory/quantifiers/single_inv_partition.cpp b/src/theory/quantifiers/single_inv_partition.cpp index 6c7a06ebe..a0e25b756 100644 --- a/src/theory/quantifiers/single_inv_partition.cpp +++ b/src/theory/quantifiers/single_inv_partition.cpp @@ -243,7 +243,6 @@ bool SingleInvocationPartition::init(std::vector<Node>& funcs, } std::map<Node, Node> subs_map; std::map<Node, Node> subs_map_rev; - std::vector<Node> funcs; // normalize the invocations if (!terms.empty()) { @@ -314,8 +313,8 @@ bool SingleInvocationPartition::init(std::vector<Node>& funcs, // rename bound variables with maximal overlap with si_vars std::unordered_set<Node, NodeHashFunction> fvs; expr::getFreeVariables(cr, fvs); - std::vector<Node> terms; - std::vector<Node> subs; + std::vector<Node> termsNs; + std::vector<Node> subsNs; for (const Node& v : fvs) { TypeNode tn = v.getType(); @@ -325,11 +324,11 @@ bool SingleInvocationPartition::init(std::vector<Node>& funcs, { if (tn == d_arg_types[k]) { - if (std::find(subs.begin(), subs.end(), d_si_vars[k]) - == subs.end()) + if (std::find(subsNs.begin(), subsNs.end(), d_si_vars[k]) + == subsNs.end()) { - terms.push_back(v); - subs.push_back(d_si_vars[k]); + termsNs.push_back(v); + subsNs.push_back(d_si_vars[k]); Trace("si-prt-debug") << " ...use " << d_si_vars[k] << std::endl; break; @@ -337,9 +336,9 @@ bool SingleInvocationPartition::init(std::vector<Node>& funcs, } } } - Assert(terms.size() == subs.size()); - cr = - cr.substitute(terms.begin(), terms.end(), subs.begin(), subs.end()); + Assert(termsNs.size() == subsNs.size()); + cr = cr.substitute( + termsNs.begin(), termsNs.end(), subsNs.begin(), subsNs.end()); } cr = Rewriter::rewrite(cr); Trace("si-prt") << ".....got si=" << singleInvocation diff --git a/src/theory/quantifiers/solution_filter.cpp b/src/theory/quantifiers/solution_filter.cpp index 8c664fec5..5e1bf54f4 100644 --- a/src/theory/quantifiers/solution_filter.cpp +++ b/src/theory/quantifiers/solution_filter.cpp @@ -89,9 +89,9 @@ bool SolutionFilterStrength::addTerm(Node n, std::ostream& out) else { Options& nodeManagerOptions = nm->getOptions(); - std::ostream* out = nodeManagerOptions.getOut(); - (*out) << "; (filtered " << (d_isStrong ? s : s.negate()) << ")" - << std::endl; + std::ostream* nodeManagerOut = nodeManagerOptions.getOut(); + (*nodeManagerOut) << "; (filtered " << (d_isStrong ? s : s.negate()) + << ")" << std::endl; } } d_curr_sols.clear(); diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp index 113da2acb..908dde528 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp @@ -158,16 +158,19 @@ Node CegSingleInvSol::reconstructSolution(Node sol, do { std::vector< TypeNode > to_erase; for( std::map< TypeNode, bool >::iterator it = active.begin(); it != active.end(); ++it ){ - TypeNode stn = it->first; - Node ns = d_qe->getTermEnumeration()->getEnumerateTerm(stn, index); + TypeNode tn = it->first; + Node ns = d_qe->getTermEnumeration()->getEnumerateTerm(tn, index); if( ns.isNull() ){ - to_erase.push_back( stn ); + to_erase.push_back(tn); }else{ - Node nb = d_qe->getTermDatabaseSygus()->sygusToBuiltin( ns, stn ); - Node nr = Rewriter::rewrite( nb );//d_qe->getTermDatabaseSygus()->getNormalized( stn, nb, false, false ); - Trace("csi-rcons-debug2") << " - try " << ns << " -> " << nr << " for " << stn << " " << nr.getKind() << std::endl; - std::map< Node, int >::iterator itt = d_rcons_to_id[stn].find( nr ); - if (itt != d_rcons_to_id[stn].end()) + Node nb = d_qe->getTermDatabaseSygus()->sygusToBuiltin(ns, tn); + Node nr = Rewriter::rewrite(nb); // d_qe->getTermDatabaseSygus()->getNormalized( + // tn, nb, false, false ); + Trace("csi-rcons-debug2") + << " - try " << ns << " -> " << nr << " for " << tn << " " + << nr.getKind() << std::endl; + std::map<Node, int>::iterator itt = d_rcons_to_id[tn].find(nr); + if (itt != d_rcons_to_id[tn].end()) { // if it is not already reconstructed if (d_reconstruct.find(itt->second) == d_reconstruct.end()) diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp index cae5cd823..cc6c051cd 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp +++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp @@ -209,8 +209,8 @@ bool CegisCoreConnective::processInitialize(Node conj, SygusTypeInfo& gti = d_tds->getTypeInfo(gt); for (unsigned r = 0; r < 2; r++) { - Node f = prePost[r]; - if (f.isConst()) + Node node = prePost[r]; + if (node.isConst()) { // this direction is trivial, ignore continue; @@ -225,7 +225,7 @@ bool CegisCoreConnective::processInitialize(Node conj, Trace("sygus-ccore-init") << " will do " << (r == 0 ? "pre" : "post") << "condition." << std::endl; Node cons = gdt[i].getConstructor(); - c.initialize(f, cons); + c.initialize(node, cons); // Register the symmetry breaking lemma: do not do top-level solutions // with this constructor (e.g. we want to enumerate literals, not // conjunctions). @@ -667,8 +667,7 @@ Node CegisCoreConnective::evaluate(Node n, Node cn = d_eval.eval(n, d_vars, mvs); if (cn.isNull()) { - Node cn = - n.substitute(d_vars.begin(), d_vars.end(), mvs.begin(), mvs.end()); + cn = n.substitute(d_vars.begin(), d_vars.end(), mvs.begin(), mvs.end()); cn = Rewriter::rewrite(cn); } if (!id.isNull()) diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp index 3923361b1..5a3df28f5 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp +++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp @@ -74,17 +74,17 @@ void SygusEnumerator::initialize(Node e) { sblc.push_back(slem); } - for (const Node& sbl : sblc) + for (const Node& sblemma : sblc) { Trace("sygus-enum") - << " symmetry breaking lemma : " << sbl << std::endl; + << " symmetry breaking lemma : " << sblemma << std::endl; // if its a negation of a unit top-level tester, then this specifies // that we should not enumerate terms whose top symbol is that // constructor - if (sbl.getKind() == NOT) + if (sblemma.getKind() == NOT) { Node a; - int tst = datatypes::utils::isTester(sbl[0], a); + int tst = datatypes::utils::isTester(sblemma[0], a); if (tst >= 0) { if (a == e) @@ -205,8 +205,8 @@ void SygusEnumerator::TermCache::initialize(SygusStatistics* s, // record type information for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++) { - TypeNode tn = dt[i].getArgType(j); - argTypes[i].push_back(tn); + TypeNode type = dt[i].getArgType(j); + argTypes[i].push_back(type); } } NodeManager* nm = NodeManager::currentNM(); diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp index 0cc57e0ec..9d327bfe1 100644 --- a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp +++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp @@ -122,9 +122,9 @@ void SygusEvalUnfold::registerModelValue(Node a, Trace("sygus-eval-unfold") << "Built-in term : " << bTerm << std::endl; std::vector<Node> vars; Node var_list = dt.getSygusVarList(); - for (const Node& v : var_list) + for (const Node& var : var_list) { - vars.push_back(v); + vars.push_back(var); } // evaluation children std::vector<Node> eval_children; diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index a1b46f1ac..259f9c642 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -562,12 +562,12 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( std::string dbname = ssb.str(); sdts.push_back(SygusDatatypeGenerator(dbname)); unsigned boolIndex = types.size(); - TypeNode btype = nm->booleanType(); + TypeNode bool_type = nm->booleanType(); TypeNode unres_bt = mkUnresolvedType(ssb.str(), unres); - types.push_back(btype); + types.push_back(bool_type); unres_types.push_back(unres_bt); - type_to_unres[btype] = unres_bt; - sygus_to_builtin[unres_bt] = btype; + type_to_unres[bool_type] = unres_bt; + sygus_to_builtin[unres_bt] = bool_type; // We ensure an ordering on types such that parametric types are processed // before their consitituents. Since parametric types were added before their @@ -689,13 +689,13 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( { // Add PLUS, MINUS Kind kinds[2] = {PLUS, MINUS}; - for (const Kind k : kinds) + for (const Kind kind : kinds) { - Trace("sygus-grammar-def") << "...add for " << k << std::endl; + Trace("sygus-grammar-def") << "...add for " << kind << std::endl; std::vector<TypeNode> cargsOp; cargsOp.push_back(unres_t); cargsOp.push_back(unres_t); - sdts[i].addConstructor(k, cargsOp); + sdts[i].addConstructor(kind, cargsOp); } if (!types[i].isInteger()) { @@ -716,22 +716,22 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( std::vector<TypeNode> cargsEmpty; sdts.back().addConstructor(nm->mkConst(Rational(1)), "1", cargsEmpty); /* Add operator PLUS */ - Kind k = PLUS; + Kind kind = PLUS; Trace("sygus-grammar-def") << "\t...add for PLUS to Pos_Int\n"; std::vector<TypeNode> cargsPlus; cargsPlus.push_back(unresPosInt); cargsPlus.push_back(unresPosInt); - sdts.back().addConstructor(k, cargsPlus); + sdts.back().addConstructor(kind, cargsPlus); sdts.back().d_sdt.initializeDatatype(types[i], bvl, true, true); Trace("sygus-grammar-def") << " ...built datatype " << sdts.back().d_sdt.getDatatype() << " "; /* Adding division at root */ - k = DIVISION; - Trace("sygus-grammar-def") << "\t...add for " << k << std::endl; + kind = DIVISION; + Trace("sygus-grammar-def") << "\t...add for " << kind << std::endl; std::vector<TypeNode> cargsDiv; cargsDiv.push_back(unres_t); cargsDiv.push_back(unresPosInt); - sdts[i].addConstructor(k, cargsDiv); + sdts[i].addConstructor(kind, cargsDiv); } } else if (types[i].isBitVector()) @@ -740,10 +740,10 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( std::vector<Kind> un_kinds = {BITVECTOR_NOT, BITVECTOR_NEG}; std::vector<TypeNode> cargsUnary; cargsUnary.push_back(unres_t); - for (const Kind k : un_kinds) + for (const Kind kind : un_kinds) { - Trace("sygus-grammar-def") << "...add for " << k << std::endl; - sdts[i].addConstructor(k, cargsUnary); + Trace("sygus-grammar-def") << "...add for " << kind << std::endl; + sdts[i].addConstructor(kind, cargsUnary); } // binary apps std::vector<Kind> bin_kinds = {BITVECTOR_AND, @@ -762,10 +762,10 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( std::vector<TypeNode> cargsBinary; cargsBinary.push_back(unres_t); cargsBinary.push_back(unres_t); - for (const Kind k : bin_kinds) + for (const Kind kind : bin_kinds) { - Trace("sygus-grammar-def") << "...add for " << k << std::endl; - sdts[i].addConstructor(k, cargsBinary); + Trace("sygus-grammar-def") << "...add for " << kind << std::endl; + sdts[i].addConstructor(kind, cargsBinary); } } else if (types[i].isString()) @@ -828,11 +828,11 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( { Trace("sygus-grammar-def") << "...add for constructors" << std::endl; const DType& dt = types[i].getDType(); - for (unsigned k = 0, size_k = dt.getNumConstructors(); k < size_k; ++k) + for (unsigned l = 0, size_l = dt.getNumConstructors(); l < size_l; ++l) { - Trace("sygus-grammar-def") << "...for " << dt[k].getName() << std::endl; - Node cop = dt[k].getConstructor(); - if (dt[k].getNumArgs() == 0) + Trace("sygus-grammar-def") << "...for " << dt[l].getName() << std::endl; + Node cop = dt[l].getConstructor(); + if (dt[l].getNumArgs() == 0) { // Nullary constructors are interpreted as terms, not operators. // Thus, we apply them to no arguments here. @@ -840,11 +840,11 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( } std::vector<TypeNode> cargsCons; Trace("sygus-grammar-def") << "...add for selectors" << std::endl; - for (unsigned j = 0, size_j = dt[k].getNumArgs(); j < size_j; ++j) + for (unsigned j = 0, size_j = dt[l].getNumArgs(); j < size_j; ++j) { Trace("sygus-grammar-def") - << "...for " << dt[k][j].getName() << std::endl; - TypeNode crange = dt[k][j].getRangeType(); + << "...for " << dt[l][j].getName() << std::endl; + TypeNode crange = dt[l][j].getRangeType(); Assert(type_to_unres.find(crange) != type_to_unres.end()); cargsCons.push_back(type_to_unres[crange]); // add to the selector type the selector operator @@ -852,15 +852,15 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( Assert(std::find(types.begin(), types.end(), crange) != types.end()); unsigned i_selType = std::distance( types.begin(), std::find(types.begin(), types.end(), crange)); - TypeNode arg_type = dt[k][j].getType(); + TypeNode arg_type = dt[l][j].getType(); arg_type = arg_type.getSelectorDomainType(); Assert(type_to_unres.find(arg_type) != type_to_unres.end()); std::vector<TypeNode> cargsSel; cargsSel.push_back(type_to_unres[arg_type]); - Node sel = dt[k][j].getSelector(); - sdts[i_selType].addConstructor(sel, dt[k][j].getName(), cargsSel); + Node sel = dt[l][j].getSelector(); + sdts[i_selType].addConstructor(sel, dt[l][j].getName(), cargsSel); } - sdts[i].addConstructor(cop, dt[k].getName(), cargsCons); + sdts[i].addConstructor(cop, dt[l].getName(), cargsCons); } } else if (types[i].isSort() || types[i].isFunction()) @@ -1047,9 +1047,9 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( // use a print callback since we do not want to print the lambda std::shared_ptr<SygusPrintCallback> spc; std::vector<Expr> opLArgsExpr; - for (unsigned i = 0, nvars = opLArgs.size(); i < nvars; i++) + for (unsigned j = 0, nvars = opLArgs.size(); j < nvars; j++) { - opLArgsExpr.push_back(opLArgs[i].toExpr()); + opLArgsExpr.push_back(opLArgs[j].toExpr()); } spc = std::make_shared<printer::SygusExprPrintCallback>( monomial.toExpr(), opLArgsExpr); @@ -1076,9 +1076,9 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( Node op = nm->mkNode(LAMBDA, nm->mkNode(BOUND_VAR_LIST, lambdaVars), ops); std::shared_ptr<SygusPrintCallback> spc; std::vector<Expr> lambdaVarsExpr; - for (unsigned i = 0, nvars = lambdaVars.size(); i < nvars; i++) + for (unsigned j = 0, nvars = lambdaVars.size(); j < nvars; j++) { - lambdaVarsExpr.push_back(lambdaVars[i].toExpr()); + lambdaVarsExpr.push_back(lambdaVars[j].toExpr()); } spc = std::make_shared<printer::SygusExprPrintCallback>(ops.toExpr(), lambdaVarsExpr); @@ -1118,7 +1118,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( } //------ make Boolean type SygusDatatypeGenerator& sdtBool = sdts[boolIndex]; - Trace("sygus-grammar-def") << "Make grammar for " << btype << std::endl; + Trace("sygus-grammar-def") << "Make grammar for " << bool_type << std::endl; //add variables for (unsigned i = 0, size = sygus_vars.size(); i < size; ++i) { @@ -1133,7 +1133,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( } // add constants std::vector<Node> consts; - mkSygusConstantsForType(btype, consts); + mkSygusConstantsForType(bool_type, consts); for (unsigned i = 0, size = consts.size(); i < size; ++i) { std::stringstream ss; @@ -1170,15 +1170,15 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( // type specific predicates if (types[i].isReal()) { - Kind k = LEQ; - Trace("sygus-grammar-def") << "...add for " << k << std::endl; - sdtBool.addConstructor(k, cargsBinary); + Kind kind = LEQ; + Trace("sygus-grammar-def") << "...add for " << kind << std::endl; + sdtBool.addConstructor(kind, cargsBinary); } else if (types[i].isBitVector()) { - Kind k = BITVECTOR_ULT; - Trace("sygus-grammar-def") << "...add for " << k << std::endl; - sdtBool.addConstructor(k, cargsBinary); + Kind kind = BITVECTOR_ULT; + Trace("sygus-grammar-def") << "...add for " << kind << std::endl; + sdtBool.addConstructor(kind, cargsBinary); } else if (types[i].isDatatype()) { @@ -1187,13 +1187,14 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( const DType& dt = types[i].getDType(); std::vector<TypeNode> cargsTester; cargsTester.push_back(unres_types[iuse]); - for (unsigned k = 0, size_k = dt.getNumConstructors(); k < size_k; ++k) + for (unsigned kind = 0, size_k = dt.getNumConstructors(); kind < size_k; + ++kind) { Trace("sygus-grammar-def") - << "...for " << dt[k].getTester() << std::endl; + << "...for " << dt[kind].getTester() << std::endl; std::stringstream sst; - sst << dt[k].getTester(); - sdtBool.addConstructor(dt[k].getTester(), sst.str(), cargsTester); + sst << dt[kind].getTester(); + sdtBool.addConstructor(dt[kind].getTester(), sst.str(), cargsTester); } } } @@ -1225,10 +1226,11 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( sdtBool.addConstructor(k, cargs); } } - if( range==btype ){ + if (range == bool_type) + { startIndex = boolIndex; } - sdtBool.d_sdt.initializeDatatype(btype, bvl, true, true); + sdtBool.d_sdt.initializeDatatype(bool_type, bvl, true, true); Trace("sygus-grammar-def") << "...built datatype for Bool " << sdtBool.d_sdt.getDatatype() << " "; Trace("sygus-grammar-def") << "...finished make default grammar for " << fun << " " << range << std::endl; diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index 5874104ce..df41672e2 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -106,7 +106,6 @@ void SygusRepairConst::initializeChecker(std::unique_ptr<SmtEngine>& checker, Node query, bool& needExport) { - NodeManager* nm = NodeManager::currentNM(); if (options::sygusRepairConstTimeout.wasSetByUser()) { // To support a separate timeout for the subsolver, we need to create diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index e3e94ba44..dc21107b1 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -1343,9 +1343,9 @@ Node SygusUnifIo::constructSol( if (snode.d_strats[i]->d_this == strat_ITE) { // flip the two - EnumTypeInfoStrat* etis = snode.d_strats[i]; + EnumTypeInfoStrat* etis_i = snode.d_strats[i]; snode.d_strats[i] = snode.d_strats[0]; - snode.d_strats[0] = etis; + snode.d_strats[0] = etis_i; break; } } diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp index 2b85595cd..1bdae0b20 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp @@ -79,11 +79,12 @@ Node SygusUnifRl::purifyLemma(Node n, BoolNodePairMap& cache) { Trace("sygus-unif-rl-purify") << "PurifyLemma : " << n << "\n"; - BoolNodePairMap::const_iterator it = cache.find(BoolNodePair(ensureConst, n)); - if (it != cache.end()) + BoolNodePairMap::const_iterator it0 = + cache.find(BoolNodePair(ensureConst, n)); + if (it0 != cache.end()) { Trace("sygus-unif-rl-purify-debug") << "... already visited " << n << "\n"; - return it->second; + return it0->second; } // Recurse unsigned size = n.getNumChildren(); @@ -105,14 +106,14 @@ Node SygusUnifRl::purifyLemma(Node n, // occurring under a unification function-to-synthesize if (ensureConst) { - std::map<Node, Node>::iterator it = d_cand_to_sol.find(n[0]); + std::map<Node, Node>::iterator it1 = d_cand_to_sol.find(n[0]); // if function-to-synthesize, retrieve its built solution to replace in // the application before computing the model value - AlwaysAssert(!u_fapp || it != d_cand_to_sol.end()); - if (it != d_cand_to_sol.end()) + AlwaysAssert(!u_fapp || it1 != d_cand_to_sol.end()); + if (it1 != d_cand_to_sol.end()) { TNode cand = n[0]; - Node tmp = n.substitute(cand, it->second); + Node tmp = n.substitute(cand, it1->second); // should be concrete, can just use the rewriter nv = Rewriter::rewrite(tmp); Trace("sygus-unif-rl-purify") @@ -174,8 +175,8 @@ Node SygusUnifRl::purifyLemma(Node n, if (u_fapp) { Node np; - std::map<Node, Node>::const_iterator it = d_app_to_purified.find(nb); - if (it == d_app_to_purified.end()) + std::map<Node, Node>::const_iterator it2 = d_app_to_purified.find(nb); + if (it2 == d_app_to_purified.end()) { // Build purified head with fresh skolem and recreate node std::stringstream ss; @@ -210,7 +211,7 @@ Node SygusUnifRl::purifyLemma(Node n, } else { - np = it->second; + np = it2->second; } Trace("sygus-unif-rl-purify") << "PurifyLemma : purified head and transformed " << nb << " into " @@ -1069,10 +1070,10 @@ void SygusUnifRl::DecisionTreeInfo::buildDtInfoGain(std::vector<Node>& hds, unsigned picked_cond = 0; std::vector<std::pair<std::vector<Node>, std::vector<Node>>> splits; double current_set_entropy = getEntropy(hds, hd_mv, ind); - for (unsigned i = 0, size = conds.size(); i < size; ++i) + for (unsigned j = 0, conds_size = conds.size(); j < conds_size; ++j) { std::pair<std::vector<Node>, std::vector<Node>> split = - evaluateCond(hds, conds[i]); + evaluateCond(hds, conds[j]); splits.push_back(split); Assert(hds.size() == split.first.size() + split.second.size()); double gain = @@ -1083,12 +1084,12 @@ void SygusUnifRl::DecisionTreeInfo::buildDtInfoGain(std::vector<Node>& hds, indent("sygus-unif-dt-debug", ind); Trace("sygus-unif-dt-debug") << "..gain of " - << d_unif->d_tds->sygusToBuiltin(conds[i], conds[i].getType()) << " is " + << d_unif->d_tds->sygusToBuiltin(conds[j], conds[j].getType()) << " is " << gain << "\n"; if (gain > maxgain) { maxgain = gain; - picked_cond = i; + picked_cond = j; } } // add picked condition diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp index 052546c0e..c2448abb4 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp @@ -870,8 +870,8 @@ void SygusUnifStrategy::staticLearnRedundantOps( } if (op.getKind() == kind::BUILTIN) { - Kind k = NodeManager::operatorToKind(op); - if (k == NOT || k == OR || k == AND || k == ITE) + Kind kind = NodeManager::operatorToKind(op); + if (kind == NOT || kind == OR || kind == AND || kind == ITE) { // can eliminate if their argument types are simple loops to this type bool type_ok = true; diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index a77d3681b..978e31545 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -159,9 +159,9 @@ void SynthEngine::assignConjecture(Node q) Trace("cegqi-qep") << "Compute single invocation for " << q << "..." << std::endl; quantifiers::SingleInvocationPartition sip; - std::vector<Node> funcs; - funcs.insert(funcs.end(), q[0].begin(), q[0].end()); - sip.init(funcs, body); + std::vector<Node> funcs0; + funcs0.insert(funcs0.end(), q[0].begin(), q[0].end()); + sip.init(funcs0, body); Trace("cegqi-qep") << "...finished, got:" << std::endl; sip.debugPrint("cegqi-qep"); @@ -204,11 +204,11 @@ void SynthEngine::assignConjecture(Node q) Trace("cegqi-qep") << " subs : " << nqe_vars[i] << " -> " << k << std::endl; } - std::vector<Node> funcs; - sip.getFunctions(funcs); - for (unsigned i = 0, size = funcs.size(); i < size; i++) + std::vector<Node> funcs1; + sip.getFunctions(funcs1); + for (unsigned i = 0, size = funcs1.size(); i < size; i++) { - Node f = funcs[i]; + Node f = funcs1[i]; Node fi = sip.getFunctionInvocationFor(f); Node fv = sip.getFirstOrderVariableForFunction(f); Assert(!fi.isNull()); diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 0b3428c9d..a1b250142 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -404,17 +404,17 @@ void TermDbSygus::registerEnumerator(Node e, SygusTypeInfo& sti = getTypeInfo(stn); const DType& dt = stn.getDType(); int anyC = sti.getAnyConstantConsNum(); - for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) + for (unsigned j = 0, ncons = dt.getNumConstructors(); j < ncons; j++) { - bool isAnyC = static_cast<int>(i) == anyC; + bool isAnyC = static_cast<int>(j) == anyC; if (anyC != -1 && !isAnyC) { // if we are using the any constant constructor, do not use any // concrete constant - Node c_op = sti.getConsNumConst(i); + Node c_op = sti.getConsNumConst(j); if (!c_op.isNull()) { - rm_indices.push_back(i); + rm_indices.push_back(j); } } } @@ -844,10 +844,10 @@ bool TermDbSygus::canConstructKind(TypeNode tn, { bool success = true; std::vector<TypeNode> disj_types[2]; - for (unsigned c = 0; c < 2; c++) + for (unsigned cc = 0; cc < 2; cc++) { - if (!canConstructKind(conj_types[c], OR, disj_types[c], true) - || disj_types[c].size() != 2) + if (!canConstructKind(conj_types[cc], OR, disj_types[cc], true) + || disj_types[cc].size() != 2) { success = false; break; @@ -865,8 +865,8 @@ bool TermDbSygus::canConstructKind(TypeNode tn, if (canConstructKind(dtn, NOT, ntypes) && ntypes.size() == 1) { TypeNode ntn = ntypes[0]; - for (unsigned dd = 0, size = disj_types[1 - r].size(); - dd < size; + for (unsigned dd = 0, inner_size = disj_types[1 - r].size(); + dd < inner_size; dd++) { if (disj_types[1 - r][dd] == ntn) diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index e5d6748aa..765c2b4c8 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -52,33 +52,33 @@ struct RewriteStackElement { * Construct a fresh stack element. */ RewriteStackElement(TNode node, TheoryId theoryId) - : node(node), - original(node), - theoryId(theoryId), - originalTheoryId(theoryId), - nextChild(0) + : d_node(node), + d_original(node), + d_theoryId(theoryId), + d_originalTheoryId(theoryId), + d_nextChild(0) { } - TheoryId getTheoryId() { return static_cast<TheoryId>(theoryId); } + TheoryId getTheoryId() { return static_cast<TheoryId>(d_theoryId); } TheoryId getOriginalTheoryId() { - return static_cast<TheoryId>(originalTheoryId); + return static_cast<TheoryId>(d_originalTheoryId); } /** The node we're currently rewriting */ - Node node; + Node d_node; /** Original node */ - Node original; + Node d_original; /** Id of the theory that's currently rewriting this node */ - unsigned theoryId : 8; + unsigned d_theoryId : 8; /** Id of the original theory that started the rewrite */ - unsigned originalTheoryId : 8; + unsigned d_originalTheoryId : 8; /** Index of the child this node is done rewriting */ - unsigned nextChild : 32; + unsigned d_nextChild : 32; /** Builder for this node */ - NodeBuilder<> builder; + NodeBuilder<> d_builder; }; Node Rewriter::rewrite(TNode node) { @@ -140,71 +140,73 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { Trace("rewriter") << "Rewriter::rewriting: " << rewriteStackTop.getTheoryId() << "," - << rewriteStackTop.node << std::endl; + << rewriteStackTop.d_node << std::endl; // Before rewriting children we need to do a pre-rewrite of the node - if (rewriteStackTop.nextChild == 0) { - + if (rewriteStackTop.d_nextChild == 0) + { // Check if the pre-rewrite has already been done (it's in the cache) - Node cached = getPreRewriteCache(rewriteStackTop.getTheoryId(), - rewriteStackTop.node); + cached = getPreRewriteCache(rewriteStackTop.getTheoryId(), + rewriteStackTop.d_node); if (cached.isNull()) { // Rewrite until fix-point is reached for(;;) { // Perform the pre-rewrite RewriteResponse response = d_theoryRewriters[rewriteStackTop.getTheoryId()]->preRewrite( - rewriteStackTop.node); + rewriteStackTop.d_node); // Put the rewritten node to the top of the stack - rewriteStackTop.node = response.d_node; - TheoryId newTheory = theoryOf(rewriteStackTop.node); + rewriteStackTop.d_node = response.d_node; + TheoryId newTheory = theoryOf(rewriteStackTop.d_node); // In the pre-rewrite, if changing theories, we just call the other theories pre-rewrite if (newTheory == rewriteStackTop.getTheoryId() && response.d_status == REWRITE_DONE) { break; } - rewriteStackTop.theoryId = newTheory; + rewriteStackTop.d_theoryId = newTheory; } // Cache the rewrite setPreRewriteCache(rewriteStackTop.getOriginalTheoryId(), - rewriteStackTop.original, - rewriteStackTop.node); + rewriteStackTop.d_original, + rewriteStackTop.d_node); } // Otherwise we're have already been pre-rewritten (in pre-rewrite cache) else { // Continue with the cached version - rewriteStackTop.node = cached; - rewriteStackTop.theoryId = theoryOf(cached); + rewriteStackTop.d_node = cached; + rewriteStackTop.d_theoryId = theoryOf(cached); } } - rewriteStackTop.original =rewriteStackTop.node; + rewriteStackTop.d_original = rewriteStackTop.d_node; // Now it's time to rewrite the children, check if this has already been done - Node cached = getPostRewriteCache(rewriteStackTop.getTheoryId(), - rewriteStackTop.node); + cached = getPostRewriteCache(rewriteStackTop.getTheoryId(), + rewriteStackTop.d_node); // If not, go through the children if(cached.isNull()) { // The child we need to rewrite - unsigned child = rewriteStackTop.nextChild++; + unsigned child = rewriteStackTop.d_nextChild++; // To build the rewritten expression we set up the builder if(child == 0) { - if (rewriteStackTop.node.getNumChildren() > 0) { + if (rewriteStackTop.d_node.getNumChildren() > 0) + { // The children will add themselves to the builder once they're done - rewriteStackTop.builder << rewriteStackTop.node.getKind(); - kind::MetaKind metaKind = rewriteStackTop.node.getMetaKind(); + rewriteStackTop.d_builder << rewriteStackTop.d_node.getKind(); + kind::MetaKind metaKind = rewriteStackTop.d_node.getMetaKind(); if (metaKind == kind::metakind::PARAMETERIZED) { - rewriteStackTop.builder << rewriteStackTop.node.getOperator(); + rewriteStackTop.d_builder << rewriteStackTop.d_node.getOperator(); } } } // Process the next child - if(child < rewriteStackTop.node.getNumChildren()) { + if (child < rewriteStackTop.d_node.getNumChildren()) + { // The child node - Node childNode = rewriteStackTop.node[child]; + Node childNode = rewriteStackTop.d_node[child]; // Push the rewrite request to the stack (NOTE: rewriteStackTop might be a bad reference now) rewriteStack.push_back(RewriteStackElement(childNode, theoryOf(childNode))); // Go on with the rewriting @@ -212,10 +214,11 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { } // Incorporate the children if necessary - if (rewriteStackTop.node.getNumChildren() > 0) { - Node rewritten = rewriteStackTop.builder; - rewriteStackTop.node = rewritten; - rewriteStackTop.theoryId = theoryOf(rewriteStackTop.node); + if (rewriteStackTop.d_node.getNumChildren() > 0) + { + Node rewritten = rewriteStackTop.d_builder; + rewriteStackTop.d_node = rewritten; + rewriteStackTop.d_theoryId = theoryOf(rewriteStackTop.d_node); } // Done with all pre-rewriting, so let's do the post rewrite @@ -223,14 +226,14 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { // Do the post-rewrite RewriteResponse response = d_theoryRewriters[rewriteStackTop.getTheoryId()]->postRewrite( - rewriteStackTop.node); + rewriteStackTop.d_node); // We continue with the response we got TheoryId newTheoryId = theoryOf(response.d_node); if (newTheoryId != rewriteStackTop.getTheoryId() || response.d_status == REWRITE_AGAIN_FULL) { // In the post rewrite if we've changed theories, we must do a full rewrite - Assert(response.d_node != rewriteStackTop.node); + Assert(response.d_node != rewriteStackTop.d_node); //TODO: this is not thread-safe - should make this assertion dependent on sequential build #ifdef CVC4_ASSERTIONS Assert(d_rewriteStack->find(response.d_node) @@ -238,7 +241,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { d_rewriteStack->insert(response.d_node); #endif Node rewritten = rewriteTo(newTheoryId, response.d_node); - rewriteStackTop.node = rewritten; + rewriteStackTop.d_node = rewritten; #ifdef CVC4_ASSERTIONS d_rewriteStack->erase(response.d_node); #endif @@ -251,36 +254,36 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { d_theoryRewriters[newTheoryId]->postRewrite(response.d_node); Assert(r2.d_node == response.d_node); #endif - rewriteStackTop.node = response.d_node; + rewriteStackTop.d_node = response.d_node; break; } // Check for trivial rewrite loops of size 1 or 2 - Assert(response.d_node != rewriteStackTop.node); + Assert(response.d_node != rewriteStackTop.d_node); Assert(d_theoryRewriters[rewriteStackTop.getTheoryId()] ->postRewrite(response.d_node) .d_node - != rewriteStackTop.node); - rewriteStackTop.node = response.d_node; + != rewriteStackTop.d_node); + rewriteStackTop.d_node = response.d_node; } // We're done with the post rewrite, so we add to the cache setPostRewriteCache(rewriteStackTop.getOriginalTheoryId(), - rewriteStackTop.original, - rewriteStackTop.node); + rewriteStackTop.d_original, + rewriteStackTop.d_node); } else { // We were already in cache, so just remember it - rewriteStackTop.node = cached; - rewriteStackTop.theoryId = theoryOf(cached); + rewriteStackTop.d_node = cached; + rewriteStackTop.d_theoryId = theoryOf(cached); } // If this is the last node, just return if (rewriteStack.size() == 1) { - Assert(!isEquality || rewriteStackTop.node.getKind() == kind::EQUAL - || rewriteStackTop.node.isConst()); - return rewriteStackTop.node; + Assert(!isEquality || rewriteStackTop.d_node.getKind() == kind::EQUAL + || rewriteStackTop.d_node.isConst()); + return rewriteStackTop.d_node; } // We're done with this node, append it to the parent - rewriteStack[rewriteStack.size() - 2].builder << rewriteStackTop.node; + rewriteStack[rewriteStack.size() - 2].d_builder << rewriteStackTop.d_node; rewriteStack.pop_back(); } diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 1a798414e..866c80863 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -304,24 +304,25 @@ bool TheorySetsPrivate::assertFact(Node fact, Node exp) Node s = e->d_singleton; if (!s.isNull()) { - Node exp = NodeManager::currentNM()->mkNode( + Node pexp = NodeManager::currentNM()->mkNode( kind::AND, atom, atom[1].eqNode(s)); - d_keep.insert(exp); + d_keep.insert(pexp); if (s.getKind() == kind::SINGLETON) { if (s[0] != atom[0]) { - Trace("sets-prop") << "Propagate mem-eq : " << exp << std::endl; + Trace("sets-prop") + << "Propagate mem-eq : " << pexp << std::endl; Node eq = s[0].eqNode(atom[0]); d_keep.insert(eq); - assertFact(eq, exp); + assertFact(eq, pexp); } } else { Trace("sets-prop") - << "Propagate mem-eq conflict : " << exp << std::endl; - d_state.setConflict(exp); + << "Propagate mem-eq conflict : " << pexp << std::endl; + d_state.setConflict(pexp); } } } @@ -774,8 +775,8 @@ void TheorySetsPrivate::checkUpwardsClosure() std::vector<Node> exp; exp.push_back(itm2m.second); d_state.addEqualityToExp(term[1], itm2m.second[1], exp); - Node k = d_state.getProxy(term); - Node fact = nm->mkNode(kind::MEMBER, x, k); + Node r = d_state.getProxy(term); + Node fact = nm->mkNode(kind::MEMBER, x, r); d_im.assertInference(fact, exp, "upc2"); if (d_state.isInConflict()) { diff --git a/src/theory/smt_engine_subsolver.h b/src/theory/smt_engine_subsolver.h index 135175665..a1fc67385 100644 --- a/src/theory/smt_engine_subsolver.h +++ b/src/theory/smt_engine_subsolver.h @@ -21,6 +21,7 @@ #include <map> #include <memory> #include <vector> + #include "expr/expr_manager.h" #include "expr/node.h" #include "expr/variable_type_map.h" diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp index 343f6e4f8..c23041914 100644 --- a/src/theory/strings/base_solver.cpp +++ b/src/theory/strings/base_solver.cpp @@ -155,19 +155,19 @@ void BaseSolver::checkInit() std::vector<Node> exp; // explain empty components bool foundNEmpty = false; - for (const Node& nc : n) + for (const Node& nnc : n) { - if (d_state.areEqual(nc, d_emptyString)) + if (d_state.areEqual(nnc, d_emptyString)) { - if (nc != d_emptyString) + if (nnc != d_emptyString) { - exp.push_back(nc.eqNode(d_emptyString)); + exp.push_back(nnc.eqNode(d_emptyString)); } } else { Assert(!foundNEmpty); - ns = nc; + ns = nnc; foundNEmpty = true; } } diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index 723520b67..5414c9b98 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -485,10 +485,10 @@ Node CoreSolver::checkCycles( Node eqc, std::vector< Node >& curr, std::vector< if( eqc==d_emptyString ){ //for empty eqc, ensure all components are empty if( nr!=d_emptyString ){ - std::vector< Node > exp; - exp.push_back( n.eqNode( d_emptyString ) ); + std::vector<Node> exps; + exps.push_back(n.eqNode(d_emptyString)); d_im.sendInference( - exp, n[i].eqNode(d_emptyString), "I_CYCLE_E"); + exps, n[i].eqNode(d_emptyString), "I_CYCLE_E"); return Node::null(); } }else{ @@ -1576,9 +1576,9 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi, } Node split_eq; - for (unsigned r = 0; r < 2; r++) + for (unsigned i = 0; i < 2; i++) { - Node t = r == 0 ? veci[loop_index] : t_yz; + Node t = i == 0 ? veci[loop_index] : t_yz; split_eq = t.eqNode(d_emptyString); Node split_eqr = Rewriter::rewrite(split_eq); // the equality could rewrite to false diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp index b04b88b31..af114e361 100644 --- a/src/theory/strings/extf_solver.cpp +++ b/src/theory/strings/extf_solver.cpp @@ -570,16 +570,16 @@ void ExtfSolver::checkExtfInference(Node n, { bool do_infer = false; conc = conc.negate(); - bool pol = conc.getKind() != NOT; - Node lit = pol ? conc : conc[0]; + bool pol2 = conc.getKind() != NOT; + Node lit = pol2 ? conc : conc[0]; if (lit.getKind() == EQUAL) { - do_infer = pol ? !d_state.areEqual(lit[0], lit[1]) - : !d_state.areDisequal(lit[0], lit[1]); + do_infer = pol2 ? !d_state.areEqual(lit[0], lit[1]) + : !d_state.areDisequal(lit[0], lit[1]); } else { - do_infer = !d_state.areEqual(lit, pol ? d_true : d_false); + do_infer = !d_state.areEqual(lit, pol2 ? d_true : d_false); } if (do_infer) { diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp index 1942938c3..86995736e 100644 --- a/src/theory/strings/regexp_elim.cpp +++ b/src/theory/strings/regexp_elim.cpp @@ -303,15 +303,15 @@ Node RegExpElimination::eliminateConcat(Node atom) // process the non-greedy find variables if (!non_greedy_find_vars.empty()) { - std::vector<Node> children; + std::vector<Node> children2; for (const Node& v : non_greedy_find_vars) { Node bound = nm->mkNode( AND, nm->mkNode(LEQ, d_zero, v), nm->mkNode(LT, v, lenx)); - children.push_back(bound); + children2.push_back(bound); } - children.push_back(res); - Node body = nm->mkNode(AND, children); + children2.push_back(res); + Node body = nm->mkNode(AND, children2); Node bvl = nm->mkNode(BOUND_VAR_LIST, non_greedy_find_vars); res = nm->mkNode(EXISTS, bvl, body); } diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index 0e8347281..530564a35 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -772,8 +772,8 @@ void RegExpOpr::firstChars(Node r, std::set<unsigned> &pcset, SetNodes &pvset) firstChars(r[i], cset, vset); Node n = r[i]; Node exp; - int r = delta( n, exp ); - if(r != 1) { + if (delta(n, exp) != 1) + { break; } } @@ -826,15 +826,15 @@ void RegExpOpr::firstChars(Node r, std::set<unsigned> &pcset, SetNodes &pvset) if(Trace.isOn("regexp-fset")) { Trace("regexp-fset") << "END FSET(" << mkString(r) << ") = {"; - for (std::set<unsigned>::const_iterator itr = pcset.begin(); - itr != pcset.end(); - ++itr) + for (std::set<unsigned>::const_iterator it = pcset.begin(); + it != pcset.end(); + ++it) { - if (itr != pcset.begin()) + if (it != pcset.begin()) { Trace("regexp-fset") << ","; } - Trace("regexp-fset") << (*itr); + Trace("regexp-fset") << (*it); } Trace("regexp-fset") << "}" << std::endl; } @@ -1191,7 +1191,6 @@ void RegExpOpr::simplifyPRegExp( Node s, Node r, std::vector< Node > &new_nodes } else if(r[0].getKind() == kind::REGEXP_SIGMA) { conc = d_true; } else { - NodeManager* nm = NodeManager::currentNM(); Node se = s.eqNode(d_emptyString); Node sinr = nm->mkNode(kind::STRING_IN_REGEXP, s, r[0]); Node sk1 = nm->mkSkolem( @@ -1495,24 +1494,25 @@ Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< PairNodes, Node > } if(Trace.isOn("regexp-int-debug")) { Trace("regexp-int-debug") << "Try CSET(" << cset.size() << ") = {"; - for (std::vector<unsigned>::const_iterator itr = cset.begin(); - itr != cset.end(); - ++itr) + for (std::vector<unsigned>::const_iterator it = cset.begin(); + it != cset.end(); + ++it) { - if(itr != cset.begin()) { + if (it != cset.begin()) + { Trace("regexp-int-debug") << ", "; } - Trace("regexp-int-debug") << ( *itr ); + Trace("regexp-int-debug") << (*it); } Trace("regexp-int-debug") << std::endl; } std::map< PairNodes, Node > cacheX; - for (std::vector<unsigned>::const_iterator itr = cset.begin(); - itr != cset.end(); - ++itr) + for (std::vector<unsigned>::const_iterator it = cset.begin(); + it != cset.end(); + ++it) { std::vector<unsigned> cvec; - cvec.push_back(String::convertCodeToUnsignedInt(*itr)); + cvec.push_back(String::convertCodeToUnsignedInt(*it)); String c(cvec); Trace("regexp-int-debug") << "Try character " << c << " ... " << std::endl; Node r1l = derivativeSingle(r1, c); diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp index 5b41feacb..9d9c66ec2 100644 --- a/src/theory/strings/regexp_solver.cpp +++ b/src/theory/strings/regexp_solver.cpp @@ -100,15 +100,15 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems) Trace("regexp-process") << "Checking Memberships ... " << std::endl; for (const std::pair<const Node, std::vector<Node> >& mr : mems) { - std::vector<Node> mems = mr.second; + std::vector<Node> mems2 = mr.second; Trace("regexp-process") << "Memberships(" << mr.first << ") = " << mr.second << std::endl; - if (!checkEqcInclusion(mems)) + if (!checkEqcInclusion(mems2)) { // conflict discovered, return return; } - if (!checkEqcIntersect(mems)) + if (!checkEqcIntersect(mems2)) { // conflict discovered, return return; diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 26721229f..f05c9165b 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -195,8 +195,9 @@ Node TheoryStringsRewriter::simpleRegexpConsume( std::vector< Node >& mchildren, std::reverse( mchildren_ss.begin(), mchildren_ss.end() ); std::reverse( children_ss.begin(), children_ss.end() ); } - Node ret = simpleRegexpConsume( mchildren_ss, children_ss, t ); - if( ret.isNull() ){ + if (simpleRegexpConsume(mchildren_ss, children_ss, t) + .isNull()) + { can_skip = true; } } @@ -1252,10 +1253,13 @@ bool TheoryStringsRewriter::testConstStringInRegExp( CVC4::String &s, unsigned i } case kind::REGEXP_STAR: { if( s.size() != index_start ) { - for(unsigned k=s.size() - index_start; k>0; --k) { - CVC4::String t = s.substr(index_start, k); + for (unsigned i = s.size() - index_start; i > 0; --i) + { + CVC4::String t = s.substr(index_start, i); if( testConstStringInRegExp( t, 0, r[0] ) ) { - if( index_start + k == s.size() || testConstStringInRegExp( s, index_start + k, r ) ) { + if (index_start + i == s.size() + || testConstStringInRegExp(s, index_start + i, r)) + { return true; } } @@ -1409,8 +1413,8 @@ Node TheoryStringsRewriter::rewriteMembership(TNode node) { { nb << nm->mkNode(STRING_IN_REGEXP, xc, r); } - Node retNode = nb.constructNode(); - return returnRewrite(node, retNode, "re-in-dist-char-star"); + return returnRewrite( + node, nb.constructNode(), "re-in-dist-char-star"); } } } @@ -2245,19 +2249,19 @@ Node TheoryStringsRewriter::rewriteContains( Node node ) { if (nc2.size() > 1) { Node emp = nm->mkConst(CVC4::String("")); - NodeBuilder<> nb(kind::AND); + NodeBuilder<> nb2(kind::AND); for (const Node& n2 : nc2) { if (n2 == n) { - nb << nm->mkNode(kind::EQUAL, node[0], node[1]); + nb2 << nm->mkNode(kind::EQUAL, node[0], node[1]); } else { - nb << nm->mkNode(kind::EQUAL, emp, n2); + nb2 << nm->mkNode(kind::EQUAL, emp, n2); } } - ret = nb.constructNode(); + ret = nb2.constructNode(); } else { @@ -2770,14 +2774,14 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) { // str.replace( str.++( x, "ab" ), "a", y ) ---> // str.++( str.replace( str.++( x, "a" ), "a", y ), "b" ) // this is independent of whether the second argument may be empty - std::vector<Node> cc; - cc.push_back(NodeManager::currentNM()->mkNode( + std::vector<Node> scc; + scc.push_back(NodeManager::currentNM()->mkNode( kind::STRING_STRREPL, utils::mkConcat(STRING_CONCAT, children0), node[1], node[2])); - cc.insert(cc.end(), ce.begin(), ce.end()); - Node ret = utils::mkConcat(STRING_CONCAT, cc); + scc.insert(scc.end(), ce.begin(), ce.end()); + Node ret = utils::mkConcat(STRING_CONCAT, scc); return returnRewrite(node, ret, "rpl-cctn"); } } @@ -2968,8 +2972,8 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) { return returnRewrite(node, node[0], "repl-repl2-inv-id"); } bool dualReplIteSuccess = false; - Node cmp_con = checkEntailContains(node[1][0], node[1][2]); - if (!cmp_con.isNull() && !cmp_con.getConst<bool>()) + Node cmp_con2 = checkEntailContains(node[1][0], node[1][2]); + if (!cmp_con2.isNull() && !cmp_con2.getConst<bool>()) { // str.contains( x, z ) ---> false // implies @@ -2983,11 +2987,11 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) { // implies // str.replace( x, str.replace( x, y, z ), w ) ---> // ite( str.contains( x, y ), x, w ) - cmp_con = checkEntailContains(node[1][1], node[1][2]); - if (!cmp_con.isNull() && !cmp_con.getConst<bool>()) + cmp_con2 = checkEntailContains(node[1][1], node[1][2]); + if (!cmp_con2.isNull() && !cmp_con2.getConst<bool>()) { - cmp_con = checkEntailContains(node[1][2], node[1][1]); - if (!cmp_con.isNull() && !cmp_con.getConst<bool>()) + cmp_con2 = checkEntailContains(node[1][2], node[1][1]); + if (!cmp_con2.isNull() && !cmp_con2.getConst<bool>()) { dualReplIteSuccess = true; } @@ -3016,8 +3020,8 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) { // str.contains(y, z) ----> false and ( y == w or x == w ) implies // implies // str.replace(x, str.replace(y, x, z), w) ---> str.replace(x, y, w) - Node cmp_con = checkEntailContains(node[1][0], node[1][2]); - invSuccess = !cmp_con.isNull() && !cmp_con.getConst<bool>(); + Node cmp_con2 = checkEntailContains(node[1][0], node[1][2]); + invSuccess = !cmp_con2.isNull() && !cmp_con2.getConst<bool>(); } } else @@ -3025,11 +3029,11 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) { // str.contains(x, z) ----> false and str.contains(x, w) ----> false // implies // str.replace(x, str.replace(y, z, w), u) ---> str.replace(x, y, u) - Node cmp_con = checkEntailContains(node[0], node[1][1]); - if (!cmp_con.isNull() && !cmp_con.getConst<bool>()) + Node cmp_con2 = checkEntailContains(node[0], node[1][1]); + if (!cmp_con2.isNull() && !cmp_con2.getConst<bool>()) { - cmp_con = checkEntailContains(node[0], node[1][2]); - invSuccess = !cmp_con.isNull() && !cmp_con.getConst<bool>(); + cmp_con2 = checkEntailContains(node[0], node[1][2]); + invSuccess = !cmp_con2.isNull() && !cmp_con2.getConst<bool>(); } } if (invSuccess) @@ -3044,8 +3048,8 @@ Node TheoryStringsRewriter::rewriteReplace( Node node ) { { // str.contains( z, w ) ----> false implies // str.replace( x, w, str.replace( z, x, y ) ) ---> str.replace( x, w, z ) - Node cmp_con = checkEntailContains(node[1], node[2][0]); - if (!cmp_con.isNull() && !cmp_con.getConst<bool>()) + Node cmp_con2 = checkEntailContains(node[1], node[2][0]); + if (!cmp_con2.isNull() && !cmp_con2.getConst<bool>()) { Node res = nm->mkNode(kind::STRING_STRREPL, node[0], node[1], node[2][0]); diff --git a/src/theory/subs_minimize.cpp b/src/theory/subs_minimize.cpp index c16fab4a9..21862a251 100644 --- a/src/theory/subs_minimize.cpp +++ b/src/theory/subs_minimize.cpp @@ -194,15 +194,15 @@ bool SubstitutionMinimize::findInternal(Node n, { if (cur.isVar()) { - const std::vector<Node>::const_iterator& it = + const std::vector<Node>::const_iterator& iit = std::find(vars.begin(), vars.end(), cur); - if (it == vars.end()) + if (iit == vars.end()) { value[cur] = cur; } else { - ptrdiff_t pos = std::distance(vars.begin(), it); + ptrdiff_t pos = std::distance(vars.begin(), iit); value[cur] = subs[pos]; } } diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp index 333f09d2d..7728456a7 100644 --- a/src/theory/substitutions.cpp +++ b/src/theory/substitutions.cpp @@ -24,10 +24,11 @@ namespace CVC4 { namespace theory { struct substitution_stack_element { - TNode node; - bool children_added; - substitution_stack_element(TNode node) - : node(node), children_added(false) {} + TNode d_node; + bool d_children_added; + substitution_stack_element(TNode node) : d_node(node), d_children_added(false) + { + } };/* struct substitution_stack_element */ Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& cache) { @@ -46,7 +47,7 @@ Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& cache) { { // The current node we are processing substitution_stack_element& stackHead = toVisit.back(); - TNode current = stackHead.node; + TNode current = stackHead.d_node; Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): processing " << current << endl; @@ -77,7 +78,8 @@ Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& cache) { } // Not yet substituted, so process - if (stackHead.children_added) { + if (stackHead.d_children_added) + { // Children have been processed, so substitute NodeBuilder<> builder(current.getKind()); if (current.getMetaKind() == kind::metakind::PARAMETERIZED) { @@ -109,10 +111,12 @@ Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& cache) { Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): setting " << current << " -> " << result << endl; cache[current] = result; toVisit.pop_back(); - } else { + } + else + { // Mark that we have added the children if any if (current.getNumChildren() > 0 || current.getMetaKind() == kind::metakind::PARAMETERIZED) { - stackHead.children_added = true; + stackHead.d_children_added = true; // We need to add the operator, if any if(current.getMetaKind() == kind::metakind::PARAMETERIZED) { TNode opNode = current.getOperator(); diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp index 6a404104f..2b6a847dc 100644 --- a/src/theory/term_registration_visitor.cpp +++ b/src/theory/term_registration_visitor.cpp @@ -88,9 +88,9 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) { // The current theory has already visited it, so now it depends on the parent and the type if (Theory::setContains(parentTheoryId, visitedTheories)) { if (useType) { - TheoryId typeTheoryId = Theory::theoryOf(current.getType()); - d_theories = Theory::setInsert(typeTheoryId, d_theories); - return Theory::setContains(typeTheoryId, visitedTheories); + TheoryId typeTheoryId2 = Theory::theoryOf(current.getType()); + d_theories = Theory::setInsert(typeTheoryId2, d_theories); + return Theory::setContains(typeTheoryId2, visitedTheories); } else { return true; } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index e15641bb4..a39c014a6 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -470,17 +470,22 @@ void TheoryEngine::printAssertions(const char* tag) { if (theory && d_logicInfo.isTheoryEnabled(theoryId)) { Trace(tag) << "--------------------------------------------" << endl; Trace(tag) << "Assertions of " << theory->getId() << ": " << endl; - context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end(); - for (unsigned i = 0; it != it_end; ++ it, ++i) { - if ((*it).d_isPreregistered) - { - Trace(tag) << "[" << i << "]: "; - } - else + { + context::CDList<Assertion>::const_iterator it = theory->facts_begin(), + it_end = + theory->facts_end(); + for (unsigned i = 0; it != it_end; ++it, ++i) { - Trace(tag) << "(" << i << "): "; + if ((*it).d_isPreregistered) + { + Trace(tag) << "[" << i << "]: "; + } + else + { + Trace(tag) << "(" << i << "): "; + } + Trace(tag) << (*it).d_assertion << endl; } - Trace(tag) << (*it).d_assertion << endl; } if (d_logicInfo.isSharingEnabled()) { @@ -1146,8 +1151,7 @@ void TheoryEngine::preprocessStart() struct preprocess_stack_element { TNode node; bool children_added; - preprocess_stack_element(TNode node) - : node(node), children_added(false) {} + preprocess_stack_element(TNode n) : node(n), children_added(false) {} };/* struct preprocess_stack_element */ diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 399695131..bf0a82a20 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -267,9 +267,9 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const // choice z. P(z). Node v = nm->mkBoundVar(n.getType()); Node bvl = nm->mkNode(BOUND_VAR_LIST, v); - Node ret = nm->mkNode(CHOICE, bvl, ita->second.substitute(n, v)); - d_modelCache[n] = ret; - return ret; + Node answer = nm->mkNode(CHOICE, bvl, ita->second.substitute(n, v)); + d_modelCache[n] = answer; + return answer; } // must rewrite the term at this point ret = Rewriter::rewrite(n); @@ -315,11 +315,11 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const { if (d_enableFuncModels) { - std::map<Node, Node>::const_iterator it = d_uf_models.find(n); - if (it != d_uf_models.end()) + std::map<Node, Node>::const_iterator entry = d_uf_models.find(n); + if (entry != d_uf_models.end()) { // Existing function - ret = it->second; + ret = entry->second; d_modelCache[n] = ret; return ret; } @@ -327,7 +327,6 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const // constant in the enumeration of the range type vector<TypeNode> argTypes = t.getArgTypes(); vector<Node> args; - NodeManager* nm = NodeManager::currentNM(); for (unsigned i = 0, size = argTypes.size(); i < size; ++i) { args.push_back(nm->mkBoundVar(argTypes[i])); diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index a96f29ada..68ad25490 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -736,7 +736,6 @@ bool TheoryEngineModelBuilder::buildModel(Model* m) } #endif - set<Node>* repSet = typeRepSet.getSet(t); TypeNode tb = t.getBaseType(); if (!assignOne) { @@ -755,6 +754,7 @@ bool TheoryEngineModelBuilder::buildModel(Model* m) bool assignable, evaluable CVC4_UNUSED; std::map<Node, Assigner>::iterator itAssigner; std::map<Node, Node>::iterator itAssignerM; + set<Node>* repSet = typeRepSet.getSet(t); for (i = noRepSet.begin(); i != noRepSet.end();) { i2 = i; @@ -928,11 +928,10 @@ bool TheoryEngineModelBuilder::buildModel(Model* m) for (it = typeNoRepSet.begin(); it != typeNoRepSet.end(); ++it) { set<Node>& noRepSet = TypeSet::getSet(it); - set<Node>::iterator i; - for (i = noRepSet.begin(); i != noRepSet.end(); ++i) + for (const Node& node : noRepSet) { - tm->d_reps[*i] = *i; - tm->d_rep_set.add((*i).getType(), *i); + tm->d_reps[node] = node; + tm->d_rep_set.add(node.getType(), node); } } diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 63aa81097..479e3400d 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -1002,15 +1002,22 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, if (eqpc->d_id == eq::MERGED_THROUGH_TRANS) { std::vector<std::shared_ptr<EqProof>> orderedChildren; bool nullCongruenceFound = false; - for (unsigned i = 0; i < eqpc->d_children.size(); ++i) { - if (eqpc->d_children[i]->d_id==eq::MERGED_THROUGH_CONGRUENCE && - eqpc->d_children[i]->d_node.isNull()) { + for (const auto& child : eqpc->d_children) + { + if (child->d_id == eq::MERGED_THROUGH_CONGRUENCE + && child->d_node.isNull()) + { nullCongruenceFound = true; - Debug("pf::ee") << "Have congruence with empty d_node. Splitting..." << std::endl; - orderedChildren.insert(orderedChildren.begin(), eqpc->d_children[i]->d_children[0]); - orderedChildren.push_back(eqpc->d_children[i]->d_children[1]); - } else { - orderedChildren.push_back(eqpc->d_children[i]); + Debug("pf::ee") + << "Have congruence with empty d_node. Splitting..." + << std::endl; + orderedChildren.insert(orderedChildren.begin(), + child->d_children[0]); + orderedChildren.push_back(child->d_children[1]); + } + else + { + orderedChildren.push_back(child); } } @@ -1935,11 +1942,12 @@ void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag) newSetTriggersSize = 0; // Copy into to new one, and insert the new tag/id unsigned i = 0; - Theory::Set tags = newSetTags; + Theory::Set tags2 = newSetTags; TheoryId current; - while ((current = Theory::setPop(tags)) != THEORY_LAST) { + while ((current = Theory::setPop(tags2)) != THEORY_LAST) + { // Remove from the tags - tags = Theory::setRemove(current, tags); + tags2 = Theory::setRemove(current, tags2); // Insert the id into the triggers newSetTriggers[newSetTriggersSize++] = current == tag ? eqNodeId : triggerSet.d_triggers[i++]; diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp index 6d6f49c7f..23b7b9217 100644 --- a/src/theory/uf/ho_extension.cpp +++ b/src/theory/uf/ho_extension.cpp @@ -336,8 +336,8 @@ unsigned HoExtension::checkAppCompletion() { if (n[k].getType().isFunction()) { - TNode rop = ee->getRepresentative(n[k]); - curr_rops[rop] = true; + TNode rop2 = ee->getRepresentative(n[k]); + curr_rops[rop2] = true; } } } diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp index 49ceebfd6..27d045120 100644 --- a/src/theory/uf/symmetry_breaker.cpp +++ b/src/theory/uf/symmetry_breaker.cpp @@ -400,18 +400,17 @@ void SymmetryBreaker::assertFormula(TNode phi) { } } unordered_map<TNode, set<TNode>, TNodeHashFunction>& ps = t.partitions(); - for(unordered_map<TNode, set<TNode>, TNodeHashFunction>::iterator i = ps.begin(); - i != ps.end(); - ++i) { - Debug("ufsymm") << "UFSYMM partition*: " << (*i).first; - set<TNode>& p = (*i).second; + for (auto& kv : ps) + { + Debug("ufsymm") << "UFSYMM partition*: " << kv.first; + set<TNode>& p = kv.second; for(set<TNode>::iterator j = p.begin(); j != p.end(); ++j) { Debug("ufsymm") << " " << *j; } Debug("ufsymm") << endl; - p.insert((*i).first); + p.insert(kv.first); Permutations::iterator pi = d_permutations.find(p); if(pi == d_permutations.end()) { d_permutations.insert(p); @@ -473,11 +472,9 @@ void SymmetryBreaker::apply(std::vector<Node>& newClauses) { } } - for(Permutations::iterator i = d_permutations.begin(); - i != d_permutations.end(); - ++i) { + for (const Permutation& p : d_permutations) + { ++(d_stats.d_permutationSetsConsidered); - const Permutation& p = *i; Debug("ufsymm") << "UFSYMM looking at permutation: " << p << endl; size_t n = p.size() - 1; if(invariantByPermutations(p)) { @@ -529,11 +526,12 @@ void SymmetryBreaker::apply(std::vector<Node>& newClauses) { if(i != p.end() || p.size() != cts.size()) { Debug("ufsymm") << "UFSYMM cts != p" << endl; NodeBuilder<> disj(kind::OR); - for(set<Node>::const_iterator i = cts.begin(); - i != cts.end(); - ++i) { - if(t != *i) { - disj << NodeManager::currentNM()->mkNode(kind::EQUAL, t, *i); + NodeManager* nm = NodeManager::currentNM(); + for (const Node& nn : cts) + { + if (t != nn) + { + disj << nm->mkNode(kind::EQUAL, t, nn); } } Node d; @@ -596,20 +594,29 @@ bool SymmetryBreaker::invariantByPermutations(const Permutation& p) { subs.push_back(p1); repls.push_back(p1); repls.push_back(p0); - for(vector<Node>::iterator i = d_phi.begin(); i != d_phi.end(); ++i) { - Node s = (*i).substitute(subs.begin(), subs.end(), repls.begin(), repls.end()); + for (const Node nn : d_phi) + { + Node s = + nn.substitute(subs.begin(), subs.end(), repls.begin(), repls.end()); Node n = norm(s); - if(*i != n && d_phiSet.find(n) == d_phiSet.end()) { - Debug("ufsymm") << "UFSYMM P_swap is NOT an inv perm op for " << p << endl - << "UFSYMM because this node: " << *i << endl - << "UFSYMM rewrite-norms to : " << n << endl - << "UFSYMM which is not in our set of normalized assertions" << endl; + if (nn != n && d_phiSet.find(n) == d_phiSet.end()) + { + Debug("ufsymm") + << "UFSYMM P_swap is NOT an inv perm op for " << p << endl + << "UFSYMM because this node: " << nn << endl + << "UFSYMM rewrite-norms to : " << n << endl + << "UFSYMM which is not in our set of normalized assertions" << endl; return false; - } else if(Debug.isOn("ufsymm:p")) { - if(*i == s) { - Debug("ufsymm:p") << "UFSYMM P_swap passes trivially: " << *i << endl; - } else { - Debug("ufsymm:p") << "UFSYMM P_swap passes: " << *i << endl + } + else if (Debug.isOn("ufsymm:p")) + { + if (nn == s) + { + Debug("ufsymm:p") << "UFSYMM P_swap passes trivially: " << nn << endl; + } + else + { + Debug("ufsymm:p") << "UFSYMM P_swap passes: " << nn << endl << "UFSYMM rewrites: " << s << endl << "UFSYMM norms: " << n << endl; } @@ -622,30 +629,41 @@ bool SymmetryBreaker::invariantByPermutations(const Permutation& p) { subs.clear(); repls.clear(); bool first = true; - for(Permutation::const_iterator i = p.begin(); i != p.end(); ++i) { - subs.push_back(*i); + for (const Node& nn : p) + { + subs.push_back(nn); if(!first) { - repls.push_back(*i); + repls.push_back(nn); } else { first = false; } } repls.push_back(*p.begin()); Assert(subs.size() == repls.size()); - for(vector<Node>::iterator i = d_phi.begin(); i != d_phi.end(); ++i) { - Node s = (*i).substitute(subs.begin(), subs.end(), repls.begin(), repls.end()); + for (const Node& nn : d_phi) + { + Node s = + nn.substitute(subs.begin(), subs.end(), repls.begin(), repls.end()); Node n = norm(s); - if(*i != n && d_phiSet.find(n) == d_phiSet.end()) { - Debug("ufsymm") << "UFSYMM P_circ is NOT an inv perm op for " << p << endl - << "UFSYMM because this node: " << *i << endl - << "UFSYMM rewrite-norms to : " << n << endl - << "UFSYMM which is not in our set of normalized assertions" << endl; + if (nn != n && d_phiSet.find(n) == d_phiSet.end()) + { + Debug("ufsymm") + << "UFSYMM P_circ is NOT an inv perm op for " << p << endl + << "UFSYMM because this node: " << nn << endl + << "UFSYMM rewrite-norms to : " << n << endl + << "UFSYMM which is not in our set of normalized assertions" + << endl; return false; - } else if(Debug.isOn("ufsymm:p")) { - if(*i == s) { - Debug("ufsymm:p") << "UFSYMM P_circ passes trivially: " << *i << endl; - } else { - Debug("ufsymm:p") << "UFSYMM P_circ passes: " << *i << endl + } + else if (Debug.isOn("ufsymm:p")) + { + if (nn == s) + { + Debug("ufsymm:p") << "UFSYMM P_circ passes trivially: " << nn << endl; + } + else + { + Debug("ufsymm:p") << "UFSYMM P_circ passes: " << nn << endl << "UFSYMM rewrites: " << s << endl << "UFSYMM norms: " << n << endl; } diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp index ffe3730c4..d667aea7e 100644 --- a/src/theory/uf/theory_uf_model.cpp +++ b/src/theory/uf/theory_uf_model.cpp @@ -153,14 +153,20 @@ void UfModelTreeNode::simplify( Node op, Node defaultVal, int argIndex ){ } } //now see if any children can be removed, and simplify the ones that cannot - for( std::map< Node, UfModelTreeNode >::iterator it = d_data.begin(); it != d_data.end(); ++it ){ - if( !it->first.isNull() ){ - if( !defaultVal.isNull() && it->second.d_value==defaultVal ){ - eraseData.push_back( it->first ); - }else{ - it->second.simplify( op, defaultVal, argIndex+1 ); - if( it->second.isEmpty() ){ - eraseData.push_back( it->first ); + for (auto& kv : d_data) + { + if (!kv.first.isNull()) + { + if (!defaultVal.isNull() && kv.second.d_value == defaultVal) + { + eraseData.push_back(kv.first); + } + else + { + kv.second.simplify(op, defaultVal, argIndex + 1); + if (kv.second.isEmpty()) + { + eraseData.push_back(kv.first); } } } |