Home
last modified time | relevance | path

Searched refs:nodeManagerOptions (Results 1 – 4 of 4) sorted by last modified time

/dports/math/cvc4/CVC4-1.7/src/smt/
H A Dsmt_engine.cpp603 nodeManagerOptions.registerForceLogicListener( in SmtEnginePrivate()
613 nodeManagerOptions.registerBeforeSearchListener( in SmtEnginePrivate()
618 nodeManagerOptions.registerSetDefaultExprDepthListener( in SmtEnginePrivate()
621 nodeManagerOptions.registerSetDefaultExprDagListener( in SmtEnginePrivate()
624 nodeManagerOptions.registerSetPrintExprTypesListener( in SmtEnginePrivate()
630 nodeManagerOptions.registerSetPrintSuccessListener( in SmtEnginePrivate()
640 nodeManagerOptions.registerDumpToFileNameListener( in SmtEnginePrivate()
643 nodeManagerOptions.registerSetReplayLogFilename( in SmtEnginePrivate()
833 nodeManagerOptions.registerUseTheoryListListener( in addUseTheoryListListener()
5325 nodeManagerOptions.setOption(key, optionarg); in setOption()
[all …]
/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/
H A Dsygus_sampler.cpp796 Options& nodeManagerOptions = NodeManager::currentNM()->getOptions(); in checkEquivalent() local
797 std::ostream* out = nodeManagerOptions.getOut(); in checkEquivalent()
H A Dsolution_filter.cpp90 Options& nodeManagerOptions = nm->getOptions(); in addTerm() local
91 std::ostream* out = nodeManagerOptions.getOut(); in addTerm()
/dports/math/cvc4/CVC4-1.7/src/theory/quantifiers/sygus/
H A Dsynth_conjecture.cpp1016 Options& nodeManagerOptions = NodeManager::currentNM()->getOptions(); in printAndContinueStream() local
1017 printSynthSolution(*nodeManagerOptions.getOut()); in printAndContinueStream()