Home
last modified time | relevance | path

Searched refs:FarkasConflictBuilder (Results 1 – 6 of 6) sorted by relevance

/dports/math/cvc4/CVC4-1.7/src/theory/arith/
H A Dcallbacks.cpp69 FarkasConflictBuilder::FarkasConflictBuilder() in FarkasConflictBuilder() function in CVC4::theory::arith::FarkasConflictBuilder
78 bool FarkasConflictBuilder::underConstruction() const{ in underConstruction()
82 bool FarkasConflictBuilder::consequentIsSet() const{ in consequentIsSet()
86 void FarkasConflictBuilder::reset(){ in reset()
95 void FarkasConflictBuilder::addConstraint(ConstraintCP c, const Rational& fc){ in addConstraint()
113 void FarkasConflictBuilder::addConstraint(ConstraintCP c, const Rational& fc, const Rational& mult){ in addConstraint()
123 void FarkasConflictBuilder::makeLastConsequent(){ in makeLastConsequent()
144 ConstraintCP FarkasConflictBuilder::commitConflict(){ in commitConflict()
H A Dcallbacks.h114 class FarkasConflictBuilder {
125 FarkasConflictBuilder();
H A Dlinear_equality.h620 …ConstraintCP minimallyWeakConflict(bool aboveUpper, ArithVar basicVar, FarkasConflictBuilder& rc) …
627 …inline ConstraintCP generateConflictAboveUpperBound(ArithVar conflictVar, FarkasConflictBuilder& r… in generateConflictAboveUpperBound()
631 …inline ConstraintCP generateConflictBelowLowerBound(ArithVar conflictVar, FarkasConflictBuilder& r… in generateConflictBelowLowerBound()
H A Dsimplex.h110 FarkasConflictBuilder* d_conflictBuilder;
H A Dsimplex.cpp50 d_conflictBuilder = new FarkasConflictBuilder(); in SimplexDecisionProcedure()
H A Dlinear_equality.cpp711 …Module::minimallyWeakConflict(bool aboveUpper, ArithVar basicVar, FarkasConflictBuilder& fcs) cons… in minimallyWeakConflict()