Searched refs:QuantAttributes (Results 1 – 17 of 17) sorted by relevance
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ |
| H A D | quantifiers_attributes.cpp | 37 QuantAttributes::QuantAttributes( QuantifiersEngine * qe ) : in QuantAttributes() function in CVC4::theory::quantifiers::QuantAttributes
104 Node QuantAttributes::getRewriteRule( Node q ) { in getRewriteRule()
115 bool QuantAttributes::checkFunDef( Node q ) { in checkFunDef()
132 Node QuantAttributes::getFunDefHead( Node q ) { in getFunDefHead()
147 Node QuantAttributes::getFunDefBody( Node q ) { in getFunDefBody()
317 bool QuantAttributes::isConjecture( Node q ) { in isConjecture()
326 bool QuantAttributes::isAxiom( Node q ) { in isAxiom()
335 bool QuantAttributes::isFunDef( Node q ) { in isFunDef()
344 bool QuantAttributes::isSygus( Node q ) { in isSygus()
371 bool QuantAttributes::isQuantElim( Node q ) { in isQuantElim()
[all …]
|
| H A D | quantifiers_attributes.h | 162 class QuantAttributes
165 QuantAttributes( QuantifiersEngine * qe );
166 ~QuantAttributes(){} in ~QuantAttributes()
|
| H A D | rewrite_engine.cpp | 50 Node rr = QuantAttributes::getRewriteRule( f ); in getPriority()
129 Node rr = QuantAttributes::getRewriteRule( f ); in checkRewriteRule()
220 Node rr = QuantAttributes::getRewriteRule( f ); in registerQuantifier()
|
| H A D | theory_quantifiers.cpp | 189 QuantAttributes::setUserAttribute( attr, n, node_values, str_value ); in setUserAttribute()
|
| H A D | fun_def_process.cpp | 37 Node n = QuantAttributes::getFunDefHead( assertions[i] ); in simplify()
48 Node bd = QuantAttributes::getFunDefBody( assertions[i] ); in simplify()
|
| H A D | skolemize.cpp | 290 QuantAttributes::setInstantiationLevelAttr( in mkSkolemizedBody()
|
| H A D | instantiate.cpp | 321 QuantAttributes::setInstantiationLevelAttr( in addInstantiation()
|
| H A D | quantifiers_rewriter.cpp | 173 QuantAttributes::computeQuantAttributes( in, qa ); in postRewrite()
481 Node h = QuantAttributes::getFunDefHead( q ); in computeProcessTerms()
484 Node fbody = QuantAttributes::getFunDefBody( q ); in computeProcessTerms()
|
| H A D | term_database.cpp | 146 QuantAttributes::setInstantiationLevelAttr(k, 0); in getOrMakeTypeFreshVariable()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/ |
| H A D | quantifiers_engine.h | 55 class QuantAttributes; variable
135 quantifiers::QuantAttributes* getQuantAttributes() const;
354 std::unique_ptr<quantifiers::QuantAttributes> d_quant_attr;
|
| H A D | quantifiers_engine.cpp | 87 d_quant_attr(new quantifiers::QuantAttributes(this)), in QuantifiersEngine()
337 quantifiers::QuantAttributes* QuantifiersEngine::getQuantAttributes() const in getQuantAttributes()
453 quantifiers::QuantAttributes::setInstantiationLevelAttr(assertions[i], in ppNotifyAssertions()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/cegqi/ |
| H A D | inst_strategy_cegqi.cpp | 172 QuantAttributes::computeQuantAttributes( quants[i], qa ); in registerCbqiLemma()
355 QuantAttributes::computeQuantAttributes( n, qa ); in getIdMarkedQuantNode()
491 QuantAttributes::computeQuantAttributes( n, qa ); in doNestedQERec()
|
| H A D | ceg_instantiator.cpp | 301 QuantAttributes::computeQuantAttributes(q, qa); in isCbqiQuant()
|
| /dports/math/cvc4/CVC4-1.7/src/preprocessing/passes/ |
| H A D | sygus_inference.cpp | 143 theory::quantifiers::QuantAttributes::computeQuantAttributes(pas, qa); in solveSygus()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/ |
| H A D | synth_engine.cpp | 420 if (QuantAttributes::checkSygusConjecture(n)) in preregisterAssertion()
|
| H A D | synth_conjecture.cpp | 92 QuantAttributes::computeQuantAttributes(q, qa); in assign()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ematching/ |
| H A D | inst_strategy_e_matching.cpp | 288 Node hd = QuantAttributes::getFunDefHead( f ); in generateTriggers()
|