Skip to content

Commit

Permalink
Format
Browse files Browse the repository at this point in the history
  • Loading branch information
ajreynol committed Oct 18, 2024
1 parent 3f3fbaa commit 4c49cfa
Show file tree
Hide file tree
Showing 2 changed files with 5 additions and 3 deletions.
5 changes: 3 additions & 2 deletions src/theory/quantifiers/quant_split.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -58,7 +58,8 @@ void QuantDSplit::checkOwnership(Node q)
bool doSplit = false;
QuantifiersBoundInference& qbi = d_qreg.getQuantifiersBoundInference();
Trace("quant-dsplit-debug") << "Check split quantified formula : " << q << std::endl;
for( size_t i=0, nvars = q[0].getNumChildren(); i<nvars; i++ ){
for (size_t i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
{
TypeNode tn = q[0][i].getType();
if( tn.isDatatype() ){
bool isFinite = d_env.isFiniteType(tn);
Expand Down Expand Up @@ -172,7 +173,7 @@ void QuantDSplit::check(Theory::Effort e, QEffort quant_e)
Trace("quant-dsplit") << "QuantDSplit::check finished" << std::endl;
}

Node QuantDSplit::split(NodeManager * nm, const Node& q, size_t index)
Node QuantDSplit::split(NodeManager* nm, const Node& q, size_t index)
{
std::vector<Node> bvs;
for (size_t i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
Expand Down
3 changes: 2 additions & 1 deletion src/theory/quantifiers/quant_split.h
Original file line number Diff line number Diff line change
Expand Up @@ -69,7 +69,8 @@ class QuantDSplit : public QuantifiersModule {
/** Identify this module (for debugging, dynamic configuration, etc..) */
std::string identify() const override { return "QuantDSplit"; }
/** */
static Node split(NodeManager * nm, const Node& q, size_t index);
static Node split(NodeManager* nm, const Node& q, size_t index);

private:
/** list of relevant quantifiers asserted in the current context */
NodeIntMap d_quant_to_reduce;
Expand Down

0 comments on commit 4c49cfa

Please sign in to comment.