diff options
author | Tim King <taking@cs.nyu.edu> | 2014-03-07 18:00:37 -0500 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2014-03-07 18:00:52 -0500 |
commit | 9ccdea06edbc72e3ecd282e9e015f6fc4b2e7173 (patch) | |
tree | cde6138cb9ab6ef0b7c15edf42e3e8cc53637002 /src/theory/arith/error_set.h | |
parent | 42be934ef4d4430944ae9074c7202a7d130c75bb (diff) |
Merging a squash of the branch timothy-king/CVC4/glpknecfix c95bf7d4f1 into master. See the CAV14 submission for an explanation of the changes to the integer solver's behavior. If compiled against the our custom extension of glpk, https://github.com/timothy-king/glpk-cut-log, this should have substantial differences in behavior. This should have moderate performance differences for linear real and integer arithmetic even if these features are disabled.
Diffstat (limited to 'src/theory/arith/error_set.h')
-rw-r--r-- | src/theory/arith/error_set.h | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/theory/arith/error_set.h b/src/theory/arith/error_set.h index d1b692cb4..b87282ba0 100644 --- a/src/theory/arith/error_set.h +++ b/src/theory/arith/error_set.h @@ -120,7 +120,7 @@ private: * This needs to be saved in case that the * violated constraint */ - Constraint d_violated; + ConstraintP d_violated; /** * This is the sgn of the first derivate the variable must move to satisfy @@ -155,12 +155,12 @@ private: public: ErrorInformation(); - ErrorInformation(ArithVar var, Constraint vio, int sgn); + ErrorInformation(ArithVar var, ConstraintP vio, int sgn); ~ErrorInformation(); ErrorInformation(const ErrorInformation& ei); ErrorInformation& operator=(const ErrorInformation& ei); - void reset(Constraint c, int sgn); + void reset(ConstraintP c, int sgn); inline ArithVar getVariable() const { return d_variable; } @@ -192,7 +192,7 @@ public: } inline const FocusSetHandle& getHandle() const{ return d_handle; } - inline Constraint getViolated() const { return d_violated; } + inline ConstraintP getViolated() const { return d_violated; } bool debugInitialized() const { return @@ -389,7 +389,7 @@ public: return d_errInfo[a].getMetric(); } - Constraint getViolated(ArithVar a) const { + ConstraintP getViolated(ArithVar a) const { return d_errInfo[a].getViolated(); } |