diff options
author | Tim King <taking@cs.nyu.edu> | 2012-04-17 16:07:22 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-04-17 16:07:22 +0000 |
commit | ccd77233892ace44fd4852999e66534d1c2283ea (patch) | |
tree | a856cacd24508a5839fcdbe728583ff055b64e34 /src/util | |
parent | 9644b6e12fbd3b649daafa43c5400d272e27bfb4 (diff) |
Merges branches/arithmetic/atom-database r2979 through 3247 into trunk. Below is a highlight of the changes:
- This introduces a new normal form to arithmetic.
-- Equalities and disequalities are in solved form.
Roughly speaking this means: (= x (+ y z)) is in normal form.
(See the comments in normal_form.h for what this formally requires.)
-- The normal form for inequality atoms always uses GEQ and GT instead of GEQ and LEQ.
Integer atoms always use GEQ.
- Constraint was added to TheoryArith.
-- A constraint is a triple of (k x v) where:
--- k is the type of the constraint (either LowerBound, UpperBound, Equality or Disequality),
--- x is an ArithVar, and
--- v is a DeltaRational value.
-- Constraints are always attached to a ConstraintDatabase.
-- A Constraint has its negation in the ConstraintDatabase [at least for now].
-- Every constraint belongs to a set of constraints for each ArithVar sorted by the delta rational values.
-- This set can be iterated over and provides efficient access to other constraints for this variable.
-- A literal may be attached to a constraint.
-- Constraints with attached literals may be marked as being asserted to the theory (sat context dependent).
-- Constraints can be propagated.
-- Every constraint has a proof (sat context dependent).
-- Proofs can be explained for either conflicts or propagations (if the node was propagated). (These proofs may be different.)
-- Equalities and disequalities can be marked as being split (user context dependent)
- This removes and replaces:
-- src/theory/arith/arith_prop_manager.*
-- src/theory/arith/atom_database.*
-- src/theory/arith/ordered_set.h
- Added isZero(), isOne() and isNegativeOne() to Rational and Integer.
- Added operator+ to CDList::const_iterator.
- Added const_iterator to CDQueue.
- Changes to regression tests.
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/integer_cln_imp.h | 12 | ||||
-rw-r--r-- | src/util/integer_gmp_imp.h | 12 | ||||
-rw-r--r-- | src/util/options.cpp | 8 | ||||
-rw-r--r-- | src/util/options.h | 12 | ||||
-rw-r--r-- | src/util/rational_cln_imp.h | 8 | ||||
-rw-r--r-- | src/util/rational_gmp_imp.h | 8 |
6 files changed, 57 insertions, 3 deletions
diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h index 9d67e8fba..d3e5c07ca 100644 --- a/src/util/integer_cln_imp.h +++ b/src/util/integer_cln_imp.h @@ -366,6 +366,18 @@ public: return cln::cl_I_to_int(sgn); } + bool isZero() const { + return cln::zerop(d_value); + } + + bool isOne() const { + return d_value == 1; + } + + bool isNegativeOne() const { + return d_value == -1; + } + //friend std::ostream& operator<<(std::ostream& os, const Integer& n); long getLong() const { diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h index ceb585852..74b4adad0 100644 --- a/src/util/integer_gmp_imp.h +++ b/src/util/integer_gmp_imp.h @@ -276,6 +276,18 @@ public: return mpz_sgn(d_value.get_mpz_t()); } + bool isZero() const { + return sgn() == 0; + } + + bool isOne() const { + return mpz_cmp_si(d_value.get_mpz_t(), 1) == 0; + } + + bool isNegativeOne() const { + return mpz_cmp_si(d_value.get_mpz_t(), -1) == 0; + } + /** * Raise this Integer to the power <code>exp</code>. * diff --git a/src/util/options.cpp b/src/util/options.cpp index b6956a31b..b6a306ee0 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -110,6 +110,7 @@ Options::Options() : ufSymmetryBreaker(false), ufSymmetryBreakerSetByUser(false), dioSolver(true), + arithRewriteEq(true), lemmaOutputChannel(NULL), lemmaInputChannel(NULL), threads(2),// default should be 1 probably, but say 2 for now @@ -183,6 +184,7 @@ Additional CVC4 options:\n\ --enable-symmetry-breaker turns on UF symmetry breaker (Deharbe et al., CADE 2011) [on by default only for QF_UF]\n\ --disable-symmetry-breaker turns off UF symmetry breaker\n\ --disable-dio-solver turns off Linear Diophantine Equation solver (Griggio, JSAT 2012)\n\ + --disable-arith-rewrite-equalities turns off the preprocessing rewrite turning equalities into a conjunction of inequalities.\n \ --threads=N sets the number of solver threads\n\ --threadN=string configures thread N (0..#threads-1)\n\ --filter-lemma-length=N don't share lemmas strictly longer than N\n\ @@ -356,6 +358,7 @@ enum OptionValue { ARITHMETIC_PIVOT_THRESHOLD, ARITHMETIC_PROP_MAX_LENGTH, ARITHMETIC_DIO_SOLVER, + ARITHMETIC_REWRITE_EQUALITIES, ENABLE_SYMMETRY_BREAKER, DISABLE_SYMMETRY_BREAKER, PARALLEL_THREADS, @@ -445,6 +448,7 @@ static struct option cmdlineOptions[] = { { "print-winner", no_argument , NULL, PRINT_WINNER }, { "disable-arithmetic-propagation", no_argument, NULL, ARITHMETIC_PROPAGATION }, { "disable-dio-solver", no_argument, NULL, ARITHMETIC_DIO_SOLVER }, + { "disable-arith-rewrite-equalities", no_argument, NULL, ARITHMETIC_REWRITE_EQUALITIES }, { "enable-symmetry-breaker", no_argument, NULL, ENABLE_SYMMETRY_BREAKER }, { "disable-symmetry-breaker", no_argument, NULL, DISABLE_SYMMETRY_BREAKER }, { "threads", required_argument, NULL, PARALLEL_THREADS }, @@ -796,6 +800,10 @@ throw(OptionException) { dioSolver = false; break; + case ARITHMETIC_REWRITE_EQUALITIES: + arithRewriteEq = false; + break; + case ENABLE_SYMMETRY_BREAKER: ufSymmetryBreaker = true; ufSymmetryBreakerSetByUser = true; diff --git a/src/util/options.h b/src/util/options.h index 4bf8b5b75..c7fbcd896 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -156,7 +156,7 @@ struct CVC4_PUBLIC Options { /** Whether we produce proofs. */ bool proof; - + /** Whether we support SmtEngine::getAssignment() for this run. */ bool produceAssignments; @@ -195,7 +195,7 @@ struct CVC4_PUBLIC Options { /** Variable activity decay factor for Minisat */ double satVarDecay; - + /** Clause activity decay factor for Minisat */ double satClauseDecay; @@ -238,6 +238,12 @@ struct CVC4_PUBLIC Options { */ bool dioSolver; + /** + * Whether to split (= x y) into (and (<= x y) (>= x y)) in + * arithmetic preprocessing. + */ + bool arithRewriteEq; + /** The output channel to receive notfication events for new lemmas */ LemmaOutputChannel* lemmaOutputChannel; LemmaInputChannel* lemmaInputChannel; @@ -251,7 +257,7 @@ struct CVC4_PUBLIC Options { /** Thread ID, for internal use in case of multi-threaded run */ int thread_id; - /** + /** * In multi-threaded setting print output of each thread at the * end of run, separated by a divider ("----"). **/ diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h index 69eede0d6..c2da0e7ed 100644 --- a/src/util/rational_cln_imp.h +++ b/src/util/rational_cln_imp.h @@ -196,6 +196,14 @@ public: return cln::zerop(d_value); } + bool isOne() const { + return d_value == 1; + } + + bool isNegativeOne() const { + return d_value == -1; + } + Rational abs() const { if(sgn() < 0){ return -(*this); diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h index 751c8f137..ef0720263 100644 --- a/src/util/rational_gmp_imp.h +++ b/src/util/rational_gmp_imp.h @@ -173,6 +173,14 @@ public: return sgn() == 0; } + bool isOne() const { + return mpq_cmp_si(d_value.get_mpq_t(), 1, 1) == 0; + } + + bool isNegativeOne() const { + return mpq_cmp_si(d_value.get_mpq_t(), -1, 1) == 0; + } + Rational abs() const { if(sgn() < 0){ return -(*this); |