diff options
Diffstat (limited to 'src/theory/arith/constraint.h')
-rw-r--r-- | src/theory/arith/constraint.h | 48 |
1 files changed, 20 insertions, 28 deletions
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index b32616a04..3caccdebd 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -75,9 +75,9 @@ #ifndef CVC4__THEORY__ARITH__CONSTRAINT_H #define CVC4__THEORY__ARITH__CONSTRAINT_H -#include <unordered_map> #include <list> #include <set> +#include <unordered_map> #include <vector> #include "base/configuration_private.h" @@ -85,12 +85,12 @@ #include "context/cdqueue.h" #include "context/context.h" #include "expr/node.h" -#include "proof/proof.h" #include "theory/arith/arithvar.h" #include "theory/arith/callbacks.h" #include "theory/arith/congruence_manager.h" #include "theory/arith/constraint_forward.h" #include "theory/arith/delta_rational.h" +#include "theory/arith/proof_macros.h" namespace CVC4 { namespace theory { @@ -252,11 +252,11 @@ struct PerVariableDatabase{ } }; - /** * If proofs are on, there is a vector of rationals for farkas coefficients. - * This is the owner of the memory for the vector, and calls delete upon cleanup. - * + * This is the owner of the memory for the vector, and calls delete upon + * cleanup. + * */ struct ConstraintRule { ConstraintP d_constraint; @@ -302,17 +302,13 @@ struct ConstraintRule { * We do however use all of the constraints by requiring non-zero * coefficients. */ -#if IS_PROOFS_BUILD RationalVectorCP d_farkasCoefficients; -#endif /* IS_PROOFS_BUILD */ ConstraintRule() : d_constraint(NullConstraint) , d_proofType(NoAP) , d_antecedentEnd(AntecedentIdSentinel) { -#if IS_PROOFS_BUILD d_farkasCoefficients = RationalVectorCPSentinel; -#endif /* IS_PROOFS_BUILD */ } ConstraintRule(ConstraintP con, ArithProofType pt) @@ -320,18 +316,14 @@ struct ConstraintRule { , d_proofType(pt) , d_antecedentEnd(AntecedentIdSentinel) { -#if IS_PROOFS_BUILD d_farkasCoefficients = RationalVectorCPSentinel; -#endif /* IS_PROOFS_BUILD */ } ConstraintRule(ConstraintP con, ArithProofType pt, AntecedentId antecedentEnd) : d_constraint(con) , d_proofType(pt) , d_antecedentEnd(antecedentEnd) { -#if IS_PROOFS_BUILD d_farkasCoefficients = RationalVectorCPSentinel; -#endif /* IS_PROOFS_BUILD */ } ConstraintRule(ConstraintP con, ArithProofType pt, AntecedentId antecedentEnd, RationalVectorCP coeffs) @@ -339,10 +331,8 @@ struct ConstraintRule { , d_proofType(pt) , d_antecedentEnd(antecedentEnd) { - Assert(PROOF_ON() || coeffs == RationalVectorCPSentinel); -#if IS_PROOFS_BUILD + Assert(ARITH_PROOF_ON() || coeffs == RationalVectorCPSentinel); d_farkasCoefficients = coeffs; -#endif /* IS_PROOFS_BUILD */ } void print(std::ostream& out) const; @@ -750,7 +740,7 @@ class Constraint { /** * If the constraint - * canBePropagated() and + * canBePropagated() and * !assertedToTheTheory(), * the constraint is added to the database's propagation queue. * @@ -789,9 +779,11 @@ class Constraint { ConstraintP constraint = crp->d_constraint; Assert(constraint->d_crid != ConstraintRuleIdSentinel); constraint->d_crid = ConstraintRuleIdSentinel; - - PROOF(if (crp->d_farkasCoefficients != RationalVectorCPSentinel) { - delete crp->d_farkasCoefficients; + ARITH_PROOF({ + if (crp->d_farkasCoefficients != RationalVectorCPSentinel) + { + delete crp->d_farkasCoefficients; + } }); } }; @@ -876,10 +868,11 @@ class Constraint { return getConstraintRule().d_antecedentEnd; } - inline RationalVectorCP getFarkasCoefficients() const { - return NULLPROOF(getConstraintRule().d_farkasCoefficients); + inline RationalVectorCP getFarkasCoefficients() const + { + return ARITH_NULLPROOF(getConstraintRule().d_farkasCoefficients); } - + void debugPrint() const; /** @@ -1051,8 +1044,7 @@ private: * The index in this list is the proper ordering of the proofs. */ ConstraintRuleList d_constraintProofs; - - + /** * Contains the exact list of constraints that can be used for propagation. */ @@ -1100,9 +1092,9 @@ private: const Rational d_one; const Rational d_negOne; - + friend class Constraint; - + public: ConstraintDatabase( context::Context* satContext, @@ -1209,7 +1201,7 @@ public: /** AntecendentID must be in range. */ ConstraintCP getAntecedent(AntecedentId p) const; - + private: /** returns true if cons is now in conflict. */ bool handleUnateProp(ConstraintP ant, ConstraintP cons); |