Fixes all -Wshadow warnings and enables the -Wshadow compile flag globally.
Co-authored-by: Clark Barrett <barrett@cs.stanford.edu>
Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>
Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
Co-authored-by: Alex Ozdemir <aozdemir@hmc.edu>
Co-authored-by: makaimann <makaim@stanford.edu>
Co-authored-by: yoni206 <yoni206@users.noreply.github.com>
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Co-authored-by: AleksandarZeljic <zeljic@stanford.edu>
Co-authored-by: Caleb Donovick <cdonovick@users.noreply.github.com>
Co-authored-by: Amalee <amaleewilson@gmail.com>
Co-authored-by: Scott Kovach <dskovach@gmail.com>
Co-authored-by: ntsis <nekuna@gmail.com>
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.
} \
++ *(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)
* @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);
}
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();
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();
// 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);
// 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();
}
// 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;
// `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() */
(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)
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())
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!
{
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;
}
// 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);
}
}
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;
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;
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;
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 = \
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 );
}
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));
}
}
( 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 );
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);
}
/* 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 */
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);
}
/* 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);
}
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;
}
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();
}
}
( 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 {
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());
}
}
}
}
( 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 {
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());
}
}
( 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(
// 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();
}
)+
( 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(
+ 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();
}
)+
// 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));
}
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();
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
{
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
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);
}
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;
{
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
{
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]
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]
}
} 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);
}
}
)
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;
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;
{
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
{
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)
}
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")
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)
{
coef[x_var].resize(6);
coef[x_var][0] = constant;
}
- asserts[x_var].push_back(*j);
+ asserts[x_var].push_back(*j1);
}
}
if (eligible)
{
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 "
continue;
}
- Debug("miplib") << " -- ELIGIBLE " << v << " , " << pos << " --"
+ Debug("miplib") << " -- ELIGIBLE " << v0 << " , " << pos << " --"
<< endl;
vector<Node> newVars;
expr::NodeSelfIterator ii, iiend;
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;
}
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;
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,
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();
// 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]);
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);
}
}
}
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;
}
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)
// 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
}
// Not yet substituted, so process
- if (stackHead.children_added)
+ if (stackHead.d_children_added)
{
// Children have been processed, so substitute
NodeBuilder<> builder(current.getKind());
// 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();
continue;
}
- for (unsigned i = 0; i < v.getNumChildren(); ++i)
+ for (i = 0; i < v.getNumChildren(); ++i)
{
updateQueue(queue, v[i], cs);
}
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;
}
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 << ", ";
}
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();
else
{
out << "(_ ";
- out << "bv" << x << " " << n;
+ out << "bv" << x << " " << width;
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();
}
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 << ")";
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";
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)
{
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])
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};
}
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());
}
}
}
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;
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 _ _ _ ";
// 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;
}
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;
}
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);
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";
}
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;
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]))
//=================================================================================================
// 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);
}
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);
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];
// 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;
}
}
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)
}
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;
}
+ }
}
}
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
}
}
}
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) {
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]);
}
}
}
// 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;
// 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();
{
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];
}
}
} else {
- Clause& c = ca[reason(x)];
+ Clause& clause = ca[reason(x)];
if(d_bvp){
if (p == trail[i]) {
d_bvp->startBVConflict(reason(var(p)));
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;
}
}
}
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");
}
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:
// 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;
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) {
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){
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(); }
//=================================================================================================
// 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),
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
// 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]));
}
}
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);
}
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;
}
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);
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;
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;
}
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);
elimclauses[first] = tmp;
// Store the length of the clause last:
- elimclauses.push(c.size());
+ elimclauses.push(clause.size());
}
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;
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);
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);)
}
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()) {
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);
// 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);
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;
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);
}
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)) {
// 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));
}
}
}
#ifdef CVC4_REPLAY
- nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextReplayDecision());
+ nextLit = MinisatSatSolver::toMinisatLit(d_proxy->getNextReplayDecision());
if (nextLit != lit_Undef) {
return nextLit;
#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")
// 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;
<< "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"
// DE requests
bool stopSearch = false;
- nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextDecisionEngineRequest(stopSearch));
+ nextLit = MinisatSatSolver::toMinisatLit(
+ d_proxy->getNextDecisionEngineRequest(stopSearch));
if(stopSearch) {
return lit_Undef;
}
// 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;
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;
}
}
} 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);
// 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;
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;
// 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;
+ }
+ }
}
}
trail.push_(p);
if (theory[var(p)]) {
// Enqueue to the theory
- proxy->enqueueTheoryLiteral(MinisatSatSolver::toSatLiteral(p));
+ d_proxy->enqueueTheoryLiteral(MinisatSatSolver::toSatLiteral(p));
}
}
confl = updateLemmas();
return confl;
} else {
- recheck = proxy->theoryNeedCheck();
+ recheck = d_proxy->theoryNeedCheck();
return confl;
}
}
{
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
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);
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?
|________________________________________________________________________________________________@*/
void Solver::theoryCheck(CVC4::theory::Theory::Effort effort)
{
- proxy->theoryCheck(effort);
+ d_proxy->theoryCheck(effort);
}
/*_________________________________________________________________________________________________
// 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;){
// 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()) ) {
cancelUntil(0);
// [mdeters] notify theory engine of restarts for deferred
// theory processing
- proxy->notifyRestart();
+ d_proxy->notifyRestart();
return l_Undef;
}
// 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;
}
#ifdef CVC4_REPLAY
- proxy->logDecision(MinisatSatSolver::toSatLiteral(next));
+ d_proxy->logDecision(MinisatSatSolver::toSatLiteral(next));
#endif /* CVC4_REPLAY */
}
assert(decisionLevel() == 0);
model.clear();
- conflict.clear();
+ d_conflict.clear();
if (!ok){
minisat_busy = false;
return l_False;
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;
}
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:
//
void Solver::push()
{
- assert(enable_incremental);
+ assert(d_enable_incremental);
assert(decisionLevel() == 0);
++assertionLevel;
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);
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());
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;
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;
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 {
} 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);
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
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;
/** 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;
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 */
// 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;
}
}
+ }
};
// 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:
//
//
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)
{}
};
//=================================================================================================
// 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());
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); }
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);
}
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;
}
}
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{
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());
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;
}
}
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>())
// 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
}
// 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);
}
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())
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())
{
Comparison cmp = Comparison::parseNormalForm(in);
Polynomial left = cmp.getLeft();
- Polynomial right = cmp.getRight();
Monomial m = left.getHead();
if (m.getVarList().singleton()){
//
// 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")) {
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);
if( relaxRes == LinFeasible ){
MipResult mipRes = MipUnknown;
{
- TimerStat::CodeTimer codeTimer(d_statistics.d_mipTimer);
+ TimerStat::CodeTimer codeTimer1(d_statistics.d_mipTimer);
mipRes = approx->solveMIP(false);
}
/* 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);
}
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);
}
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();
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;
|| 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()){
}
else
{
- TimerStat::CodeTimer codeTimer(d_statistics.d_newPropTime);
+ TimerStat::CodeTimer codeTimer1(d_statistics.d_newPropTime);
d_currentPropagationList.clear();
}
Assert(d_currentPropagationList.empty());
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;
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]));
// 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;
// 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);
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()) {
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)
{
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)
{
return RewriteResponse(REWRITE_AGAIN_FULL, res);
}
}
- else if (k == kind::DT_SIZE_BOUND)
+ else if (kind == kind::DT_SIZE_BOUND)
{
if (in[0].isConst())
{
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];
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];
return RewriteResponse(REWRITE_AGAIN_FULL, ret);
}
- if (k == kind::EQUAL)
+ if (kind == kind::EQUAL)
{
if (in[0] == in[1])
{
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 );
// 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;
}
//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 );
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 );
}
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);
}
}
}
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() ){
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);
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)
}
}
-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)
{
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))
{
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;
}
}
{
/******** Variables ********/
rm tmp(nm->mkNode(kind::ROUNDINGMODE_BITBLAST, current));
- r.insert(current, tmp);
+ d_rmMap.insert(current, tmp);
d_additionalAssertions.push_back(tmp.valid());
}
}
}
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
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]);
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";
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]);
}
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,
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));
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]);
}
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:
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]);
}
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:
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,
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()),
{
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]);
}
switch (current.getKind())
{
case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR:
- f.insert(
+ d_fpMap.insert(
current,
symfpu::convertSBVToFloat<traits>(fpt(current.getType()),
(*mode).second,
break;
case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR:
- f.insert(
+ d_fpMap.insert(
current,
symfpu::convertUBVToFloat<traits>(fpt(current.getType()),
(*mode).second,
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
}
}
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())
{
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
{
{
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]);
}
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:
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]);
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;
break;
}
- i = b.find(current);
+ i = d_boolMap.find(current);
}
result = (*i).second;
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]);
}
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;
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]);
}
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;
// (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]);
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";
}
}
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";
}
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
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 << "]";
#pragma once
-#include "expr/node.h"
#include "context/cdhashmap.h"
+#include "expr/node.h"
namespace CVC4 {
namespace theory {
* 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() {}
};
* 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;
/** Reasons constraining the individual variables */
model_reason_map d_reason;
-public:
-
+ public:
IDLModel(context::Context* context);
/** Get the model value of the variable */
/** 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
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]++;
}
}
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 );
}
{
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]);
}
#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)
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{
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{
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" : "");
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() ){
}
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;
}
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;
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();
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]);
// 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());
#include <map>
#include <memory>
#include <vector>
+
#include "expr/expr.h"
#include "expr/expr_manager.h"
#include "expr/variable_type_map.h"
// 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)
{
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
{
}
}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 ){
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 );
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))
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);
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;
{
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";
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() ){
//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]
{
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;
}
if (doRewrite)
{
- ret = nm->mkNode(ITE, children);
+ ret = nm->mkNode(ITE, childrenIte);
break;
}
}
}
}
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++) {
}
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());
}
std::map<Node, Node> subs_map;
std::map<Node, Node> subs_map_rev;
- std::vector<Node> funcs;
// normalize the invocations
if (!terms.empty())
{
// 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();
{
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;
}
}
}
- 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
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();
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())
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;
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).
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())
{
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)
// 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();
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;
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
{
// 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())
{
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())
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,
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())
{
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.
}
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
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())
// 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);
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);
}
//------ 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)
{
}
// 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;
// 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())
{
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);
}
}
}
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;
Node query,
bool& needExport)
{
- NodeManager* nm = NodeManager::currentNM();
if (options::sygusRepairConstTimeout.wasSetByUser())
{
// To support a separate timeout for the subsolver, we need to create
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;
}
}
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();
// 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")
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;
}
else
{
- np = it->second;
+ np = it2->second;
}
Trace("sygus-unif-rl-purify")
<< "PurifyLemma : purified head and transformed " << nb << " into "
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 =
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
}
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;
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");
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());
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);
}
}
}
{
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;
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)
* 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) {
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
}
// 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
// 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)
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
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();
}
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);
}
}
}
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())
{
#include <map>
#include <memory>
#include <vector>
+
#include "expr/expr_manager.h"
#include "expr/node.h"
#include "expr/variable_type_map.h"
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;
}
}
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{
}
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
{
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)
{
// 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);
}
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;
}
}
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;
}
} 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(
}
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);
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;
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;
}
}
}
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;
}
}
{
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");
}
}
}
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
{
// 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");
}
}
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
// 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;
}
// 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
// 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)
{
// 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]);
{
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];
}
}
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) {
{
// 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;
}
// 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) {
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();
// 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;
}
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()) {
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 */
// 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);
{
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;
}
// 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]));
}
#endif
- set<Node>* repSet = typeRepSet.getSet(t);
TypeNode tb = t.getBaseType();
if (!assignOne)
{
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;
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);
}
}
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);
}
}
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++];
{
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;
}
}
}
}
}
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);
}
}
- 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)) {
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;
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;
}
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;
}
}
}
//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);
}
}
}
projects / cvc5.git / commitdiff