Home
last modified time | relevance | path

Searched refs:InterpretedEvaluation (Results 1 – 5 of 5) sorted by relevance

/dports/math/vampire/vampire-4.5.1/Inferences/
H A DInterpretedEvaluation.hpp39 class InterpretedEvaluation class
43 CLASS_NAME(InterpretedEvaluation);
44 USE_ALLOCATOR(InterpretedEvaluation);
46 InterpretedEvaluation(bool doNormalize, Ordering& ordering);
47 virtual ~InterpretedEvaluation();
H A DInterpretedEvaluation.cpp53 InterpretedEvaluation::InterpretedEvaluation(bool doNormalize, Ordering& ordering) : in InterpretedEvaluation() function in Inferences::InterpretedEvaluation
60 InterpretedEvaluation::~InterpretedEvaluation() in ~InterpretedEvaluation()
69 bool InterpretedEvaluation::simplifyLiteral(Literal* lit, in simplifyLiteral()
88 Clause* InterpretedEvaluation::simplify(Clause* cl) in simplify()
/dports/math/vampire/vampire-4.5.1/UnitTests/
H A DtGaussianElimination.cpp80 static InterpretedEvaluation ev = InterpretedEvaluation(false, ord); in exhaustiveGve()
/dports/math/vampire/vampire-4.5.1/
H A DMakefile297 Inferences/InterpretedEvaluation.o\
/dports/math/vampire/vampire-4.5.1/Saturation/
H A DSaturationAlgorithm.cpp1631 res->addFront(new InterpretedEvaluation(env.options->inequalityNormalization(), ordering)); in createISE()