| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ |
| H A D | term_util.cpp | 39 TermUtil::TermUtil(QuantifiersEngine* qe) : d_quantEngine(qe) in TermUtil() function in CVC4::theory::quantifiers::TermUtil
47 TermUtil::~TermUtil(){ in ~TermUtil()
51 void TermUtil::registerQuantifier( Node q ){ in registerQuantifier()
113 Node TermUtil::getInstConstAttr( Node n ) { in getInstConstAttr()
137 bool TermUtil::hasInstConstAttr( Node n ) { in hasInstConstAttr()
141 Node TermUtil::getBoundVarAttr( Node n ) { in getBoundVarAttr()
160 bool TermUtil::hasBoundVarAttr( Node n ) { in hasBoundVarAttr()
597 int TermUtil::getTermDepth( Node n ) { in getTermDepth()
631 Node TermUtil::simpleNegate( Node n ){ in simpleNegate()
652 bool TermUtil::isNegate(Kind k) in isNegate()
[all …]
|
| H A D | quant_util.cpp | 53 quantifiers::TermUtil * QuantifiersModule::getTermUtil() { in getTermUtil()
77 if( quantifiers::TermUtil::hasInstConstAttr(it->first[0]) ){ in initialize()
78 if( !quantifiers::TermUtil::hasInstConstAttr(it->first[1]) ){ in initialize()
83 }else if( quantifiers::TermUtil::hasInstConstAttr(it->first[1]) ){ in initialize()
|
| H A D | extended_rewrite.cpp | 121 bool isNonAdditive = TermUtil::isNonAdditive(k); in extendedRewrite()
123 bool isAssoc = TermUtil::isAssoc(k, true); in extendedRewrite()
322 flip_cond = TermUtil::simpleNegate(n[0]); in extendedRewriteIte()
722 Node truen = TermUtil::mkTypeMaxValue(tn); in extendedRewriteBcp()
723 Node falsen = TermUtil::mkTypeValue(tn, 0); in extendedRewriteBcp()
842 ccs = cpol ? ccs : TermUtil::mkNegate(notk, ccs); in extendedRewriteBcp()
1192 return TermUtil::mkTypeConst(tn, gpol); in extendedRewriteEqChain()
1372 remn = TermUtil::mkNegate(notk, remn); in extendedRewriteEqChain()
1415 remn = TermUtil::mkNegate(notk, remn); in extendedRewriteEqChain()
1612 Assert(TermUtil::isNegate(n[i].getKind())); in inferSubstitution()
[all …]
|
| H A D | theory_quantifiers.cpp | 75 && TermUtil::hasInstConstAttr(n)) in preRegisterTerm()
176 if( !options::cbqi() || options::recurseCbqi() || !TermUtil::hasInstConstAttr(n) ){ in assertUniversal()
183 if( !options::cbqi() || options::recurseCbqi() || !TermUtil::hasInstConstAttr(n[0]) ){ in assertExistential()
|
| H A D | quant_util.h | 34 class TermUtil; variable
153 quantifiers::TermUtil * getTermUtil();
|
| H A D | single_inv_partition.cpp | 218 cr = TermUtil::getQuantSimplify(cr); in init()
284 TermUtil::getBoundVars(cr, bvs); in init()
315 TermUtil::getBoundVars(cr, bvs); in init()
347 TermUtil::getBoundVars(cr, d_all_vars); in init()
401 n = TermUtil::simpleNegate(n); in collectConjuncts()
|
| H A D | equality_query.cpp | 130 if( r.isConst() && quantifiers::TermUtil::containsUninterpretedConstant( r ) ){ in getInternalRepresentative()
262 if( options::cbqi() && quantifiers::TermUtil::hasInstConstAttr(n) ){ //reject in getRepScore()
281 return quantifiers::TermUtil::getTermDepth( n ); in getRepScore()
|
| H A D | term_util.h | 96 class TermUtil : public QuantifiersUtil
106 TermUtil(QuantifiersEngine * qe);
107 ~TermUtil();
|
| H A D | instantiate.h | 33 class TermUtil; variable
340 TermUtil* d_term_util;
|
| H A D | relevant_domain.cpp | 59 if( !TermUtil::hasInstConstAttr( d_terms[i] ) ){ in removeRedundantTerms()
182 …if( ( ( n.getKind()==EQUAL && !n[0].getType().isBoolean() ) || n.getKind()==GEQ ) && TermUtil::has… in computeRelevantDomain()
215 }else if( !TermUtil::hasInstConstAttr( n ) ){ in computeRelevantDomainOpCh()
300 }else if( !r_add.isNull() && !TermUtil::hasInstConstAttr( r_add ) ){ in computeRelevantDomainLit()
|
| H A D | instantiate.cpp | 131 terms[i] = quantifiers::TermUtil::ensureType(terms[i], tn); in addInstantiation()
143 if (quantifiers::TermUtil::containsUninterpretedConstant(terms[i])) in addInstantiation()
158 Node icf = quantifiers::TermUtil::getInstConstAttr(terms[i]); in addInstantiation()
167 else if (quantifiers::TermUtil::containsTerms( in addInstantiation()
|
| H A D | expr_miner.cpp | 38 TermUtil::computeVarContains(n, fvs); in convertToSkolem()
|
| H A D | term_canonize.cpp | 156 if (apply_torder && TermUtil::isComm(n.getKind())) in getCanonicalTerm()
|
| H A D | inst_strategy_enumerative.cpp | 170 || !quantifiers::TermUtil::hasInstConstAttr(gt)) in process()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ematching/ |
| H A D | trigger.cpp | 40 quantifiers::TermUtil::computeInstConstContainsForQuant(q, n, d_fv); in init()
140 quantifiers::TermUtil::computeInstConstContainsForQuant( in mkTriggerTerms()
147 Assert( quantifiers::TermUtil::getInstConstAttr(v)==q ); in mkTriggerTerms()
258 if( quantifiers::TermUtil::getInstConstAttr(n)==q ){ in isUsable()
301 if( !quantifiers::TermUtil::hasInstConstAttr(n2) ){ in isUsableEqTerms()
313 else if (!quantifiers::TermUtil::hasInstConstAttr(n2)) in isUsableEqTerms()
408 if( !quantifiers::TermUtil::hasInstConstAttr( t[1] ) ){ in isSimpleTrigger()
754 quantifiers::TermUtil::computeInstConstContains(nodes[i], fvs[i]); in filterTriggerInstances()
803 if( quantifiers::TermUtil::hasInstConstAttr(n[i]) ){ in getInversionVariable()
843 if( !quantifiers::TermUtil::hasInstConstAttr(n[i]) ){ in getInversion()
[all …]
|
| H A D | inst_match_generator.cpp | 46 Assert( quantifiers::TermUtil::hasInstConstAttr(pat) ); in InstMatchGenerator()
108 …if( !quantifiers::TermUtil::hasInstConstAttr(d_match_pattern[i]) || d_match_pattern[i].getKind()==… in initialize()
146 Node qa = quantifiers::TermUtil::getInstConstAttr(pat); in initialize()
244 Assert( !quantifiers::TermUtil::hasInstConstAttr(t) ); in getMatch()
620 quantifiers::TermUtil::computeInstConstContainsForQuant( in InstMatchGeneratorMultiLinear()
742 quantifiers::TermUtil::computeInstConstContainsForQuant( in InstMatchGeneratorMulti()
1007 Assert( !quantifiers::TermUtil::hasInstConstAttr( d_eqc ) ); in InstMatchGeneratorSimple()
1012 if( !options::cbqi() || quantifiers::TermUtil::getInstConstAttr(d_match_pattern[i])==q ){ in InstMatchGeneratorSimple()
|
| H A D | candidate_generator.cpp | 33 …return d_qe->getTermDatabase()->isTermActive( n ) && ( !options::cbqi() || !quantifiers::TermUtil:… in isLegalCandidate()
165 d_f = quantifiers::TermUtil::getInstConstAttr( mpat ); in CandidateGeneratorQEAll()
|
| H A D | ho_trigger.cpp | 165 Assert(quantifiers::TermUtil::getInstConstAttr(ret) == q); in collectHoVarApplyTerms()
205 quantifiers::TermUtil* tutil = d_quantEngine->getTermUtil(); in sendInstantiation()
473 quantifiers::TermUtil* tutil = d_quantEngine->getTermUtil(); in addHoTypeMatchPredicateLemmas()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/ |
| H A D | quantifiers_engine.h | 49 class TermUtil; variable
131 quantifiers::TermUtil* getTermUtil() const;
346 std::unique_ptr<quantifiers::TermUtil> d_term_util;
|
| /dports/math/cvc4/CVC4-1.7/src/theory/datatypes/ |
| H A D | sygus_simple_sym.h | 92 quantifiers::TermUtil* d_tutil;
|
| /dports/math/cvc4/CVC4-1.7/src/preprocessing/passes/ |
| H A D | symmetry_detect.cpp | 57 bool isComm = theory::quantifiers::TermUtil::isComm(k); in mkAssociativeNode()
646 bool isAssoc = k == kind::EQUAL || theory::quantifiers::TermUtil::isAssoc(k); in findPartitions()
650 isAssocComm = theory::quantifiers::TermUtil::isComm(k); in findPartitions()
920 Assert((k == kind::EQUAL || theory::quantifiers::TermUtil::isAssoc(k)) in collectChildren()
921 && theory::quantifiers::TermUtil::isComm(k)); in collectChildren()
1195 else if (theory::quantifiers::TermUtil::isNonAdditive(k)) in processPartitions()
|
| H A D | synth_rew_rules.cpp | 306 do_chain = theory::quantifiers::TermUtil::isAssoc(k) in applyInternal()
307 && theory::quantifiers::TermUtil::isComm(k); in applyInternal()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/ |
| H A D | ce_guided_single_inv.cpp | 104 inst = TermUtil::simpleNegate(inst); in getInitialSingleInvLemma()
148 qq = TermUtil::simpleNegate(q[1]); in initialize()
344 d_single_inv = TermUtil::simpleNegate( d_single_inv ); in finishInit()
488 cond = TermUtil::simpleNegate( cond ); in constructSolution()
955 ret = TermUtil::simpleNegate( ret ); in process()
|
| H A D | ce_guided_single_inv_sol.cpp | 103 s = NodeManager::currentNM()->mkNode( ITE, TermUtil::simpleNegate( cond ), t, rem ); in pullITEs()
131 cond = TermUtil::simpleNegate( cond ); in pullITECondition()
807 …if( min_t.getNumChildren()>dt[karg].getNumArgs() && quantifiers::TermUtil::isAssoc( min_t.getKind(… in collectReconstructNodes()
918 new_t = TermUtil::simpleNegate( curr ).negate(); in collectReconstructNodes()
920 new_t = TermUtil::simpleNegate( curr[0] ); in collectReconstructNodes()
1473 TermUtil::isComm(n.getKind()) && n.getNumChildren() == 2 ? 2 : 1; in getMatch()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/cegqi/ |
| H A D | inst_strategy_cegqi.cpp | 140 TermUtil::computeInstConstContains(q, ics); in registerCbqiLemma()
164 TermUtil::computeQuantContains( lem, quants ); in registerCbqiLemma()
557 TermUtil* tutil = d_quantEngine->getTermUtil(); in registerCounterexampleLemma()
|