- m -

• Make() : LFSCBoolRes , LFSCClausify , LFSCLraAxiom , LFSCPfLambda , LFSCProofGeneric , LFSCLraMulC , LFSCProofGeneric , LFSCClausify , LFSCLraSub , LFSCPfLet , LFSCLraPoly , LFSCLem , LFSCAssume , LFSCLraPoly , LFSCLraContra , LFSCLraAdd , LFSCProofExpr , LFSCPfVar
• Make_and_elim() : LFSCProof
• Make_CNF() : LFSCProof
• Make_i() : LFSCClausify
• make_lambda() : LFSCProof
• make_let_map() : LFSCPrinter
• make_let_proof() : LFSCConvert
• Make_mimic() : LFSCProof
• Make_not_not_elim() : LFSCProof
• make_trusted() : LFSCConvert
• MakeC() : LFSCBoolRes
• makeCopy() : CVC3::CDList< T > , CVC3::CDOmap< Key, Data, HashFcn > , CVC3::CDMapData , CVC3::CDMap< Key, Data, HashFcn > , CVC3::CDOmapOrdered< Key, Data > , CVC3::CDMapOrderedData , CVC3::CDMapOrdered< Key, Data > , CVC3::CDO< T > , CVC3::ContextObj , CVC3::CDFlags
• makeCurrent() : CVC3::ContextObj
• makeDecision() : SAT::DPLLT::Decider , CVC3::SearchSat , CVC3::SearchSatDecider
• MakeEq() : LFSCLraAxiom
• MakeLit() : SatSolver , Xchaff
• MakeStr() : LFSCProofGeneric
• MakeUnk() : LFSCProofGeneric
• MakeV() : LFSCPfVar
• mapTermsByType() : CVC3::TheoryQuant
• mark_clause_deleted() : CDatabase
• mark_var_in_new_cl() : CDatabase
• mark_vars_at_level() : CSolver
• markDeleted() : CVC3::Clause
• MarkNonSolvableEq() : CVC3::BitvectorProofRules , CVC3::BitvectorTheoremProducer
• markSat() : CVC3::Clause
• matches() : CVC3::Theorem
• matchListNew() : CVC3::TheoryQuant
• matchListOld() : CVC3::TheoryQuant
• max_dlevel() : CSolver
• mem_usage() : CSolver , CDatabase
• MemoryManagerChunks() : CVC3::MemoryManagerChunks
• MemoryManagerMalloc() : CVC3::MemoryManagerMalloc
• mergeLabels() : CVC3::TheoryDatatype , CVC3::TheoryDatatypeLazy
• min() : CVC3::TheoryBitvector
• minusExpr() : CVC3::ValidityChecker , CVC3::VCL
• minusOne() : CVC3::CompleteInstPreProcessor
• minusToPlus() : CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducerOld , CVC3::ArithProofRules
• mkClause() : Xchaff
• mkLit() : SAT::Lit , Xchaff
• mkOp() : CVC3::Expr
• mkVar() : Xchaff
• modEq() : CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducerOld
• modified() : CVC3::CLFlag
• monomialModM() : CVC3::ArithTheoremProducerOld , CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducer3
• monomialMulF() : CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducerOld , CVC3::ArithTheoremProducer
• moveSumConstantRight() : CVC3::ArithTheoremProducerOld , CVC3::ArithTheoremProducer3 , CVC3::ArithProofRules , CVC3::ArithTheoremProducer
• moveTo() : MiniSat::vec< T >
• mult_rational() : TReturn
• multEqn() : CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducerOld , CVC3::ArithProofRules
• multEqZero() : CVC3::ArithTheoremProducer3 , CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducerOld , CVC3::ArithProofRules
• multExpr() : CVC3::ValidityChecker , CVC3::VCL
• multIneqn() : CVC3::ArithTheoremProducer3 , CVC3::ArithProofRules , CVC3::ArithTheoremProducer , CVC3::ArithTheoremProducerOld
• multiplicative_inverse() : CVC3::TheoryBitvector
• multiply_coeff() : CVC3::TheoryBitvector
• multMatchChild() : CVC3::TheoryQuant
• multMatchTop() : CVC3::TheoryQuant