diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/arith_static_learner.cpp | 3 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 31 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_algebraic.cpp | 5 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_normalization.h | 5 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/trigger.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/fmf/bounded_integers.cpp | 42 | ||||
-rw-r--r-- | src/theory/quantifiers/quant_conflict_find.cpp | 74 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 9 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_single_inv.cpp | 17 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp | 7 | ||||
-rw-r--r-- | src/theory/quantifiers/term_util.cpp | 5 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 18 | ||||
-rw-r--r-- | src/theory/substitutions.cpp | 10 | ||||
-rw-r--r-- | src/theory/theory.cpp | 10 |
14 files changed, 154 insertions, 86 deletions
diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp index f26f45449..4bfc1a4f9 100644 --- a/src/theory/arith/arith_static_learner.cpp +++ b/src/theory/arith/arith_static_learner.cpp @@ -111,7 +111,8 @@ void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet if (expr::hasBoundVar(n)) { // Unsafe with non-ground ITEs; do nothing - Debug("arith::static") << "(potentially) non-ground ITE, ignoring..." << endl; + Debug("arith::static") + << "(potentially) non-ground ITE, ignoring..." << endl; break; } diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 777e99912..968970049 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -1355,26 +1355,37 @@ Theory::PPAssertStatus TheoryArithPrivate::ppAssert(TNode in, SubstitutionMap& o // Add the substitution if not recursive Assert(elim == Rewriter::rewrite(elim)); - - if(right.size() > options::ppAssertMaxSubSize()){ - Debug("simplify") << "TheoryArithPrivate::solve(): did not substitute due to the right hand side containing too many terms: " << minVar << ":" << elim << endl; + if (right.size() > options::ppAssertMaxSubSize()) + { + Debug("simplify") + << "TheoryArithPrivate::solve(): did not substitute due to the " + "right hand side containing too many terms: " + << minVar << ":" << elim << endl; Debug("simplify") << right.size() << endl; } else if (expr::hasSubterm(elim, minVar)) { - Debug("simplify") << "TheoryArithPrivate::solve(): can't substitute due to recursive pattern with sharing: " << minVar << ":" << elim << endl; - - }else if (!minVar.getType().isInteger() || right.isIntegral()) { + Debug("simplify") << "TheoryArithPrivate::solve(): can't substitute " + "due to recursive pattern with sharing: " + << minVar << ":" << elim << endl; + } + else if (!minVar.getType().isInteger() || right.isIntegral()) + { Assert(!expr::hasSubterm(elim, minVar)); // cannot eliminate integers here unless we know the resulting // substitution is integral - Debug("simplify") << "TheoryArithPrivate::solve(): substitution " << minVar << " |-> " << elim << endl; + Debug("simplify") << "TheoryArithPrivate::solve(): substitution " + << minVar << " |-> " << elim << endl; outSubstitutions.addSubstitution(minVar, elim); return Theory::PP_ASSERT_STATUS_SOLVED; - } else { - Debug("simplify") << "TheoryArithPrivate::solve(): can't substitute b/c it's integer: " << minVar << ":" << minVar.getType() << " |-> " << elim << ":" << elim.getType() << endl; - + } + else + { + Debug("simplify") << "TheoryArithPrivate::solve(): can't substitute " + "b/c it's integer: " + << minVar << ":" << minVar.getType() << " |-> " + << elim << ":" << elim.getType() << endl; } } } diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp index 8c95abe01..0150264fd 100644 --- a/src/theory/bv/bv_subtheory_algebraic.cpp +++ b/src/theory/bv/bv_subtheory_algebraic.cpp @@ -493,7 +493,7 @@ bool AlgebraicSolver::solve(TNode fact, TNode reason, SubstitutionEx& subst) { if (left.isVar() && !expr::hasSubterm(right, left)) { - bool changed = subst.addSubstitution(left, right, reason); + bool changed = subst.addSubstitution(left, right, reason); return changed; } if (right.isVar() && !expr::hasSubterm(left, right)) @@ -590,7 +590,8 @@ bool AlgebraicSolver::solve(TNode fact, TNode reason, SubstitutionEx& subst) { return false; } -bool AlgebraicSolver::isSubstitutableIn(TNode node, TNode in) { +bool AlgebraicSolver::isSubstitutableIn(TNode node, TNode in) +{ if (node.getMetaKind() == kind::metakind::VARIABLE && !expr::hasSubterm(in, node)) return true; diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index 65cb53e7e..1293f8311 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -602,8 +602,9 @@ inline Node RewriteRule<ConcatToMult>::apply(TNode node) return NodeManager::currentNM()->mkNode(kind::BITVECTOR_MULT, factor, coef); } -template<> inline -bool RewriteRule<SolveEq>::applies(TNode node) { +template <> +inline bool RewriteRule<SolveEq>::applies(TNode node) +{ if (node.getKind() != kind::EQUAL || (node[0].isVar() && !expr::hasSubterm(node[1], node[0])) || (node[1].isVar() && !expr::hasSubterm(node[0], node[1]))) diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index 44f37a30e..3615ef6f4 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -309,7 +309,9 @@ bool Trigger::isUsableEqTerms( Node q, Node n1, Node n2 ) { && !expr::hasSubterm(n1, n2)) { return true; - }else if( !quantifiers::TermUtil::hasInstConstAttr(n2) ){ + } + else if (!quantifiers::TermUtil::hasInstConstAttr(n2)) + { return true; } } diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index 8dd609e42..f0789a503 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -437,18 +437,23 @@ void BoundedIntegers::checkOwnership(Node f) << bound_lit_map[2][v] << std::endl; } }else if( it->second==BOUND_FIXED_SET ){ - setBoundedVar( f, v, BOUND_FIXED_SET ); + setBoundedVar(f, v, BOUND_FIXED_SET); setBoundVar = true; - for( unsigned i=0; i<bound_fixed_set[v].size(); i++ ){ + for (unsigned i = 0; i < bound_fixed_set[v].size(); i++) + { Node t = bound_fixed_set[v][i]; if (expr::hasBoundVar(t)) { - d_fixed_set_ngr_range[f][v].push_back( t ); - }else{ - d_fixed_set_gr_range[f][v].push_back( t ); + d_fixed_set_ngr_range[f][v].push_back(t); + } + else + { + d_fixed_set_gr_range[f][v].push_back(t); } - } - Trace("bound-int") << "Variable " << v << " is bound because of disequality conjunction " << bound_lit_map[3][v] << std::endl; + } + Trace("bound-int") << "Variable " << v + << " is bound because of disequality conjunction " + << bound_lit_map[3][v] << std::endl; } if( setBoundVar ){ success = true; @@ -547,8 +552,9 @@ void BoundedIntegers::checkOwnership(Node f) bool isProxy = false; if (expr::hasBoundVar(r)) { - //introduce a new bound - Node new_range = NodeManager::currentNM()->mkSkolem( "bir", r.getType(), "bound for term" ); + // introduce a new bound + Node new_range = NodeManager::currentNM()->mkSkolem( + "bir", r.getType(), "bound for term"); d_nground_range[f][v] = r; d_range[f][v] = new_range; r = new_range; @@ -648,14 +654,21 @@ void BoundedIntegers::getBoundValues( Node f, Node v, RepSetIterator * rsi, Node return; } -bool BoundedIntegers::isGroundRange( Node q, Node v ) { - if( isBoundVar(q,v) ){ - if( d_bound_type[q][v]==BOUND_INT_RANGE ){ +bool BoundedIntegers::isGroundRange(Node q, Node v) +{ + if (isBoundVar(q, v)) + { + if (d_bound_type[q][v] == BOUND_INT_RANGE) + { return !expr::hasBoundVar(getLowerBound(q, v)) && !expr::hasBoundVar(getUpperBound(q, v)); - }else if( d_bound_type[q][v]==BOUND_SET_MEMBER ){ + } + else if (d_bound_type[q][v] == BOUND_SET_MEMBER) + { return !expr::hasBoundVar(d_setm_range[q][v]); - }else if( d_bound_type[q][v]==BOUND_FIXED_SET ){ + } + else if (d_bound_type[q][v] == BOUND_FIXED_SET) + { return !d_fixed_set_ngr_range[q][v].empty(); } } @@ -919,4 +932,3 @@ bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node return true; } } - diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 8df24d626..3006a07bf 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -182,22 +182,32 @@ void QuantInfo::registerNode( Node n, bool hasPol, bool pol, bool beneathQuant ) if( !MatchGen::isHandledBoolConnective( n ) ){ if (expr::hasBoundVar(n)) { - //literals - if( n.getKind()==EQUAL ){ - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - flatten( n[i], beneathQuant ); + // literals + if (n.getKind() == EQUAL) + { + for (unsigned i = 0; i < n.getNumChildren(); i++) + { + flatten(n[i], beneathQuant); } - }else if( MatchGen::isHandledUfTerm( n ) ){ - flatten( n, beneathQuant ); - }else if( n.getKind()==ITE ){ - for( unsigned i=1; i<=2; i++ ){ - flatten( n[i], beneathQuant ); + } + else if (MatchGen::isHandledUfTerm(n)) + { + flatten(n, beneathQuant); + } + else if (n.getKind() == ITE) + { + for (unsigned i = 1; i <= 2; i++) + { + flatten(n[i], beneathQuant); } - registerNode( n[0], false, pol, beneathQuant ); - }else if( options::qcfTConstraint() ){ - //a theory-specific predicate - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - flatten( n[i], beneathQuant ); + registerNode(n[0], false, pol, beneathQuant); + } + else if (options::qcfTConstraint()) + { + // a theory-specific predicate + for (unsigned i = 0; i < n.getNumChildren(); i++) + { + flatten(n[i], beneathQuant); } } } @@ -1016,22 +1026,28 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ) Assert( d_n.getType().isBoolean() ); d_type = typ_bool_var; }else if( d_n.getKind()==EQUAL || options::qcfTConstraint() ){ - for( unsigned i=0; i<d_n.getNumChildren(); i++ ){ + for (unsigned i = 0; i < d_n.getNumChildren(); i++) + { if (expr::hasBoundVar(d_n[i])) { - if( !qi->isVar( d_n[i] ) ){ - Trace("qcf-qregister-debug") << "ERROR : not var " << d_n[i] << std::endl; + if (!qi->isVar(d_n[i])) + { + Trace("qcf-qregister-debug") + << "ERROR : not var " << d_n[i] << std::endl; } - Assert( qi->isVar( d_n[i] ) ); - if( d_n.getKind()!=EQUAL && qi->isVar( d_n[i] ) ){ - d_qni_var_num[i+1] = qi->d_var_num[d_n[i]]; + Assert(qi->isVar(d_n[i])); + if (d_n.getKind() != EQUAL && qi->isVar(d_n[i])) + { + d_qni_var_num[i + 1] = qi->d_var_num[d_n[i]]; } - }else{ + } + else + { d_qni_gterm[i] = d_n[i]; - qi->setGroundSubterm( d_n[i] ); + qi->setGroundSubterm(d_n[i]); } } - d_type = d_n.getKind()==EQUAL ? typ_eq : typ_tconstraint; + d_type = d_n.getKind() == EQUAL ? typ_eq : typ_tconstraint; Trace("qcf-tconstraint") << "T-Constraint : " << d_n << std::endl; } } @@ -1185,13 +1201,17 @@ void MatchGen::reset_round( QuantConflictFind * p ) { } } }else if( d_type==typ_eq ){ - for( unsigned i=0; i<d_n.getNumChildren(); i++ ){ + for (unsigned i = 0; i < d_n.getNumChildren(); i++) + { if (!expr::hasBoundVar(d_n[i])) { - TNode t = p->getTermDatabase()->getEntailedTerm( d_n[i] ); - if( t.isNull() ){ + TNode t = p->getTermDatabase()->getEntailedTerm(d_n[i]); + if (t.isNull()) + { d_ground_eval[i] = d_n[i]; - }else{ + } + else + { d_ground_eval[i] = t; } } diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 9ed6e766d..37451b776 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -775,8 +775,10 @@ bool QuantifiersRewriter::isConditionalVariableElim( Node n, int pol ){ } } }else if( n.getKind()==EQUAL ){ - for( unsigned i=0; i<2; i++ ){ - if( n[i].getKind()==BOUND_VARIABLE ){ + for (unsigned i = 0; i < 2; i++) + { + if (n[i].getKind() == BOUND_VARIABLE) + { if (!expr::hasSubterm(n[1 - i], n[i])) { return true; @@ -875,7 +877,8 @@ Node QuantifiersRewriter::computeCondSplit( Node body, QAttributes& qa ){ return body; } -bool QuantifiersRewriter::isVariableElim( Node v, Node s ) { +bool QuantifiersRewriter::isVariableElim(Node v, Node s) +{ return !expr::hasSubterm(s, v) && s.getType().isSubtypeOf(v.getType()); } diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index d374f25d0..5f5a84a6b 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -727,12 +727,14 @@ void TransitionInference::getConstantSubstitution( std::vector< Node >& vars, st // check if it is a variable equality TNode v; Node s; - for( unsigned r=0; r<2; r++ ){ - if( std::find( vars.begin(), vars.end(), slit[r] )!=vars.end() ){ + for (unsigned r = 0; r < 2; r++) + { + if (std::find(vars.begin(), vars.end(), slit[r]) != vars.end()) + { if (!expr::hasSubterm(slit[1 - r], slit[r])) { v = slit[r]; - s = slit[1-r]; + s = slit[1 - r]; break; } } @@ -742,8 +744,12 @@ void TransitionInference::getConstantSubstitution( std::vector< Node >& vars, st std::map< Node, Node > msum; if (ArithMSum::getMonomialSumLit(slit, msum)) { - for( std::map< Node, Node >::iterator itm = msum.begin(); itm != msum.end(); ++itm ){ - if( std::find( vars.begin(), vars.end(), itm->first )!=vars.end() ){ + for (std::map<Node, Node>::iterator itm = msum.begin(); + itm != msum.end(); + ++itm) + { + if (std::find(vars.begin(), vars.end(), itm->first) != vars.end()) + { Node veq_c; Node val; int ires = @@ -1079,4 +1085,3 @@ Node TransitionInference::constructFormulaTrace( DetTrace& dt ) { } } //namespace CVC4 - diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp index 43465270d..2ee120211 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp @@ -297,9 +297,10 @@ bool CegConjectureSingleInvSol::getAssignEquality( Node eq, std::vector< Node >& Node eqro = eq[r==0 ? 1 : 0 ]; if (!expr::hasSubterm(eqro, eq[r])) { - Trace("csi-simp-debug") << "---equality " << eq[r] << " = " << eqro << std::endl; - new_vars.push_back( eq[r] ); - new_subs.push_back( eqro ); + Trace("csi-simp-debug") + << "---equality " << eq[r] << " = " << eqro << std::endl; + new_vars.push_back(eq[r]); + new_subs.push_back(eqro); return true; } } diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index afa4935d6..7d91e9812 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -596,7 +596,7 @@ Node TermUtil::rewriteVtsSymbols( Node n ) { subs_lhs.push_back( rew_vts_inf ); n = n.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() ); n = Rewriter::rewrite( n ); - //may have cancelled + // may have cancelled if (!expr::hasSubterm(n, rew_vts_inf)) { rew_vts_inf = Node::null(); @@ -604,7 +604,8 @@ Node TermUtil::rewriteVtsSymbols( Node n ) { } } } - if( rew_vts_inf.isNull() ){ + if (rew_vts_inf.isNull()) + { if (!d_vts_delta.isNull() && expr::hasSubterm(n, d_vts_delta)) { rew_delta = true; diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 3c75bd98f..9346970d1 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -2201,11 +2201,13 @@ Theory::PPAssertStatus TheorySetsPrivate::ppAssert(TNode in, SubstitutionMap& ou //this is based off of Theory::ppAssert Node var; - if (in.getKind() == kind::EQUAL) { + if (in.getKind() == kind::EQUAL) + { if (in[0].isVar() && !expr::hasSubterm(in[1], in[0]) && (in[1].getType()).isSubtypeOf(in[0].getType())) { - if( !in[0].getType().isSet() || !options::setsExt() ){ + if (!in[0].getType().isSet() || !options::setsExt()) + { outSubstitutions.addSubstitution(in[0], in[1]); var = in[0]; status = Theory::PP_ASSERT_STATUS_SOLVED; @@ -2214,18 +2216,22 @@ Theory::PPAssertStatus TheorySetsPrivate::ppAssert(TNode in, SubstitutionMap& ou else if (in[1].isVar() && !expr::hasSubterm(in[0], in[1]) && (in[0].getType()).isSubtypeOf(in[1].getType())) { - if( !in[1].getType().isSet() || !options::setsExt() ){ + if (!in[1].getType().isSet() || !options::setsExt()) + { outSubstitutions.addSubstitution(in[1], in[0]); var = in[1]; status = Theory::PP_ASSERT_STATUS_SOLVED; } - }else if (in[0].isConst() && in[1].isConst()) { - if (in[0] != in[1]) { + } + else if (in[0].isConst() && in[1].isConst()) + { + if (in[0] != in[1]) + { status = Theory::PP_ASSERT_STATUS_CONFLICT; } } } - + if( status==Theory::PP_ASSERT_STATUS_SOLVED ){ Trace("sets-var-elim") << "Sets : ppAssert variable eliminated : " << in << ", var = " << var << std::endl; /* diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp index 01a3c3572..036bb4ada 100644 --- a/src/theory/substitutions.cpp +++ b/src/theory/substitutions.cpp @@ -210,13 +210,15 @@ void SubstitutionMap::addSubstitutions(SubstitutionMap& subMap, bool invalidateC } } - -static bool check(TNode node, const SubstitutionMap::NodeMap& substitutions) CVC4_UNUSED; -static bool check(TNode node, const SubstitutionMap::NodeMap& substitutions) { +static bool check(TNode node, + const SubstitutionMap::NodeMap& substitutions) CVC4_UNUSED; +static bool check(TNode node, const SubstitutionMap::NodeMap& substitutions) +{ SubstitutionMap::NodeMap::const_iterator it = substitutions.begin(); SubstitutionMap::NodeMap::const_iterator it_end = substitutions.end(); Debug("substitution") << "checking " << node << endl; - for (; it != it_end; ++ it) { + for (; it != it_end; ++it) + { Debug("substitution") << "-- hasSubterm( " << (*it).first << " ) ?" << endl; if (expr::hasSubterm(node, (*it).first)) { diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index e2a61de26..eedf0ff52 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -284,11 +284,11 @@ void Theory::computeRelevantTerms(set<Node>& termSet, } } - Theory::PPAssertStatus Theory::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { - if (in.getKind() == kind::EQUAL) { + if (in.getKind() == kind::EQUAL) + { // (and (= x t) phi) can be replaced by phi[x/t] if // 1) x is a variable // 2) x is not in the term t @@ -305,8 +305,10 @@ Theory::PPAssertStatus Theory::ppAssert(TNode in, outSubstitutions.addSubstitution(in[1], in[0]); return PP_ASSERT_STATUS_SOLVED; } - if (in[0].isConst() && in[1].isConst()) { - if (in[0] != in[1]) { + if (in[0].isConst() && in[1].isConst()) + { + if (in[0] != in[1]) + { return PP_ASSERT_STATUS_CONFLICT; } } |