| /dports/math/cvc4/CVC4-1.7/test/unit/theory/ |
| H A D | logic_info_white.h | 47 TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); in testSmtlibLogics()
48 TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) ); in testSmtlibLogics()
49 TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); in testSmtlibLogics()
51 TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); in testSmtlibLogics()
64 TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); in testSmtlibLogics()
66 TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); in testSmtlibLogics()
81 TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); in testSmtlibLogics()
83 TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) ); in testSmtlibLogics()
119 TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) ); in testSmtlibLogics()
129 TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) ); in testSmtlibLogics()
[all …]
|
| /dports/math/cvc4/CVC4-1.7/src/theory/ |
| H A D | logic_info.cpp | 94 bool LogicInfo::isTheoryEnabled(theory::TheoryId theory) const { in isTheoryEnabled() function in CVC4::LogicInfo
104 return isTheoryEnabled(theory::THEORY_QUANTIFIERS); in isQuantified()
139 return isTheoryEnabled(theory) && !isSharingEnabled() && in isPure()
148 isTheoryEnabled(theory::THEORY_ARITH), *this, in areIntegersUsed()
157 isTheoryEnabled(theory::THEORY_ARITH), *this, in areRealsUsed()
167 PrettyCheckArgument(isTheoryEnabled(theory::THEORY_ARITH), in areTranscendentalsUsed()
178 isTheoryEnabled(theory::THEORY_ARITH), *this, in isLinear()
187 isTheoryEnabled(theory::THEORY_ARITH), *this, in isDifferenceLogic()
210 if(isTheoryEnabled(theory::THEORY_ARITH)) { in operator ==()
230 if(isTheoryEnabled(theory::THEORY_ARITH) && other.isTheoryEnabled(theory::THEORY_ARITH)) { in operator <=()
[all …]
|
| H A D | theory_engine.cpp | 410 if(!d_logicInfo.isTheoryEnabled(i)) { in preRegister()
440 if (theory && d_logicInfo.isTheoryEnabled(theoryId)) { in printAssertions()
470 if (theory && d_logicInfo.isTheoryEnabled(theoryId)) { in dumpAssertions()
522 if (theory::TheoryTraits<THEORY>::hasCheck && d_logicInfo.isTheoryEnabled(THEORY)) { \ in check()
603 if (theory && d_logicInfo.isTheoryEnabled(theoryId)) { in check()
852 if(d_logicInfo.isTheoryEnabled(theoryId)) { in collectModelInfo()
886 if(d_logicInfo.isTheoryEnabled(theoryId)) { in postProcessModel()
1034 if(! d_logicInfo.isTheoryEnabled(Theory::theoryOf(atom)) && in solve()
1130 if(! d_logicInfo.isTheoryEnabled(Theory::theoryOf(current)) && in preprocess()
1235 ! d_logicInfo.isTheoryEnabled(toTheoryId)) { in assertToTheory()
[all …]
|
| H A D | logic_info.h | 117 bool isTheoryEnabled(theory::TheoryId theory) const;
|
| H A D | theory_engine.h | 803 inline bool isTheoryEnabled(theory::TheoryId theoryId) const { in isTheoryEnabled() function
804 return d_logicInfo.isTheoryEnabled(theoryId); in isTheoryEnabled()
|
| /dports/math/cvc4/CVC4-1.7/src/smt/ |
| H A D | smt_engine.cpp | 1510 !d_logic.isTheoryEnabled(THEORY_BV) && in setDefaults()
1522 if(!d_logic.isTheoryEnabled(THEORY_UF)) { in setDefaults()
1535 …if(d_logic.isTheoryEnabled(THEORY_ARRAYS) || d_logic.isTheoryEnabled(THEORY_DATATYPES) || d_logic.… in setDefaults()
1536 if(!d_logic.isTheoryEnabled(THEORY_UF)) { in setDefaults()
1568 d_logic.isTheoryEnabled(THEORY_UF) && in setDefaults()
1569 d_logic.isTheoryEnabled(THEORY_BV); in setDefaults()
1594 d_logic.isTheoryEnabled(THEORY_UF) && in setDefaults()
1595 d_logic.isTheoryEnabled(THEORY_BV); in setDefaults()
1672 d_logic.isTheoryEnabled(THEORY_BV)) { in setDefaults()
1797 …if( d_logic.isTheoryEnabled(THEORY_STRINGS) || (d_logic.isTheoryEnabled(THEORY_ARITH) && !d_logic.… in setDefaults()
[all …]
|
| /dports/math/cvc4/CVC4-1.7/src/parser/smt2/ |
| H A D | smt2.cpp | 339 bool Smt2::isTheoryEnabled(Theory theory) const { in isTheoryEnabled() function in CVC4::parser::Smt2
344 return d_logic.isTheoryEnabled(theory::THEORY_BV); in isTheoryEnabled()
365 return d_logic.isTheoryEnabled(theory::THEORY_UF); in isTheoryEnabled()
367 return d_logic.isTheoryEnabled(theory::THEORY_FP); in isTheoryEnabled()
492 if(d_logic.isTheoryEnabled(theory::THEORY_UF)) { in setLogic()
496 if(d_logic.isTheoryEnabled(theory::THEORY_ARITH)) { in setLogic()
513 if(d_logic.isTheoryEnabled(theory::THEORY_ARRAYS)) { in setLogic()
517 if(d_logic.isTheoryEnabled(theory::THEORY_BV)) { in setLogic()
525 if(d_logic.isTheoryEnabled(theory::THEORY_SETS)) { in setLogic()
537 if (d_logic.isTheoryEnabled(theory::THEORY_FP)) { in setLogic()
[all …]
|
| H A D | Smt2.g | 299 { if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF) &&
300 !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_ARRAYS) &&
301 !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) &&
302 !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS)) {
1223 { if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF) &&
1224 !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_ARRAYS) &&
1225 !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) &&
1226 !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS)) {
1249 if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) {
1276 if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) {
[all …]
|
| H A D | smt2.h | 94 bool isTheoryEnabled(Theory theory) const;
|
| /dports/math/cvc4/CVC4-1.7/src/preprocessing/passes/ |
| H A D | ite_simp.cpp | 155 if (theory_engine->getLogicInfo().isTheoryEnabled(theory::THEORY_ARITH) in doneSimpITE()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/ |
| H A D | sygus_repair_const.cpp | 225 if (logic.isTheoryEnabled(THEORY_ARITH) && logic.isLinear()) in repairSolution()
603 bool restrictLA = logic.isTheoryEnabled(THEORY_ARITH) && logic.isLinear(); in getFitToLogicExcludeVar()
|
| /dports/math/cvc4/CVC4-1.7/examples/sets-translate/ |
| H A D | sets_translate.cpp | 306 if(!logicinfo.isTheoryEnabled(theory::THEORY_SETS)) { in main()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/uf/ |
| H A D | theory_uf.cpp | 85 if (getLogicInfo().isTheoryEnabled(THEORY_UF) && options::finiteModelFind() in finishInit()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/ |
| H A D | term_database.cpp | 933 if (theory && d_quantEngine->getTheoryEngine()->d_logicInfo.isTheoryEnabled(theoryId)) { in reset()
|
| /dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/cegqi/ |
| H A D | ceg_instantiator.cpp | 1307 if( theory && d_qe->getTheoryEngine()->isTheoryEnabled(tid) ){ in processAssertions()
|