From 487e610b88f2a634e3285886ff96717c103338de Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 2 Sep 2011 17:56:43 +0000 Subject: [PATCH] Partial merge of integers work; this is simple B&B and some pseudoboolean infrastructure, and takes care not to affect CVC4's performance on LRA benchmarks. --- src/expr/node_manager.h | 10 +- src/expr/type.cpp | 18 ++ src/expr/type.h | 24 +++ src/expr/type_node.cpp | 18 +- src/expr/type_node.h | 3 + src/parser/cvc/Cvc.g | 4 + src/printer/cvc/cvc_printer.cpp | 3 + src/prop/cnf_stream.cpp | 7 +- src/smt/smt_engine.cpp | 2 +- src/theory/arith/Makefile.am | 4 +- src/theory/arith/arith_rewriter.cpp | 1 - src/theory/arith/arith_static_learner.cpp | 127 ++++++++++++- src/theory/arith/arith_static_learner.h | 19 +- src/theory/arith/arith_utilities.h | 2 +- src/theory/arith/arithvar_node_map.h | 19 ++ src/theory/arith/arithvar_set.h | 19 +- src/theory/arith/dio_solver.cpp | 118 ++++++++++++ src/theory/arith/dio_solver.h | 72 ++++++++ src/theory/arith/kinds | 12 +- src/theory/arith/normal_form.cpp | 63 ++++++- src/theory/arith/normal_form.h | 16 ++ src/theory/arith/ordered_set.h | 8 +- src/theory/arith/partial_model.h | 12 +- src/theory/arith/tableau.cpp | 6 +- src/theory/arith/tableau.h | 16 +- src/theory/arith/theory_arith.cpp | 174 ++++++++++++++++-- src/theory/arith/theory_arith.h | 35 +++- src/theory/booleans/theory_bool_type_rules.h | 5 +- .../builtin/theory_builtin_type_rules.h | 2 +- src/theory/output_channel.h | 2 +- src/theory/substitutions.cpp | 4 +- src/theory/substitutions.h | 20 ++ src/theory/theory.h | 6 +- src/theory/theory_engine.h | 2 +- src/util/Makefile.am | 2 + src/util/integer_cln_imp.h | 18 +- src/util/integer_gmp_imp.h | 19 +- src/util/pseudoboolean.cpp | 49 +++++ src/util/pseudoboolean.h | 54 ++++++ src/util/rational_cln_imp.h | 11 +- src/util/rational_gmp_imp.h | 18 +- test/Makefile.am | 2 +- test/regress/regress0/arith/Makefile | 8 + test/regress/regress0/arith/Makefile.am | 3 + test/regress/regress0/arith/integers/Makefile | 8 + .../regress0/arith/integers/Makefile.am | 130 +++++++++++++ .../regress0/arith/integers/arith-int-001.cvc | 15 ++ .../regress0/arith/integers/arith-int-002.cvc | 15 ++ .../regress0/arith/integers/arith-int-003.cvc | 15 ++ .../regress0/arith/integers/arith-int-004.cvc | 16 ++ .../regress0/arith/integers/arith-int-005.cvc | 15 ++ .../regress0/arith/integers/arith-int-006.cvc | 11 ++ .../regress0/arith/integers/arith-int-007.cvc | 11 ++ .../regress0/arith/integers/arith-int-008.cvc | 11 ++ .../regress0/arith/integers/arith-int-009.cvc | 11 ++ .../regress0/arith/integers/arith-int-010.cvc | 11 ++ .../regress0/arith/integers/arith-int-011.cvc | 6 + .../regress0/arith/integers/arith-int-012.cvc | 6 + .../regress0/arith/integers/arith-int-013.cvc | 6 + .../regress0/arith/integers/arith-int-014.cvc | 6 + .../regress0/arith/integers/arith-int-015.cvc | 6 + .../regress0/arith/integers/arith-int-016.cvc | 21 +++ .../regress0/arith/integers/arith-int-017.cvc | 21 +++ .../regress0/arith/integers/arith-int-018.cvc | 21 +++ .../regress0/arith/integers/arith-int-019.cvc | 21 +++ .../regress0/arith/integers/arith-int-020.cvc | 21 +++ .../regress0/arith/integers/arith-int-021.cvc | 5 + .../regress0/arith/integers/arith-int-022.cvc | 5 + .../regress0/arith/integers/arith-int-023.cvc | 5 + .../regress0/arith/integers/arith-int-024.cvc | 5 + .../regress0/arith/integers/arith-int-025.cvc | 5 + .../regress0/arith/integers/arith-int-026.cvc | 22 +++ .../regress0/arith/integers/arith-int-027.cvc | 22 +++ .../regress0/arith/integers/arith-int-028.cvc | 22 +++ .../regress0/arith/integers/arith-int-029.cvc | 22 +++ .../regress0/arith/integers/arith-int-030.cvc | 22 +++ .../regress0/arith/integers/arith-int-031.cvc | 20 ++ .../regress0/arith/integers/arith-int-032.cvc | 20 ++ .../regress0/arith/integers/arith-int-033.cvc | 20 ++ .../regress0/arith/integers/arith-int-034.cvc | 20 ++ .../regress0/arith/integers/arith-int-035.cvc | 20 ++ .../regress0/arith/integers/arith-int-036.cvc | 17 ++ .../regress0/arith/integers/arith-int-037.cvc | 17 ++ .../regress0/arith/integers/arith-int-038.cvc | 17 ++ .../regress0/arith/integers/arith-int-039.cvc | 17 ++ .../regress0/arith/integers/arith-int-040.cvc | 17 ++ .../regress0/arith/integers/arith-int-041.cvc | 10 + .../regress0/arith/integers/arith-int-042.cvc | 10 + .../arith/integers/arith-int-042.min.cvc | 5 + .../regress0/arith/integers/arith-int-043.cvc | 10 + .../regress0/arith/integers/arith-int-044.cvc | 11 ++ .../regress0/arith/integers/arith-int-045.cvc | 10 + .../regress0/arith/integers/arith-int-046.cvc | 7 + .../regress0/arith/integers/arith-int-047.cvc | 7 + .../regress0/arith/integers/arith-int-048.cvc | 7 + .../regress0/arith/integers/arith-int-049.cvc | 7 + .../regress0/arith/integers/arith-int-050.cvc | 7 + .../regress0/arith/integers/arith-int-051.cvc | 13 ++ .../regress0/arith/integers/arith-int-052.cvc | 13 ++ .../regress0/arith/integers/arith-int-053.cvc | 13 ++ .../regress0/arith/integers/arith-int-054.cvc | 13 ++ .../regress0/arith/integers/arith-int-055.cvc | 13 ++ .../regress0/arith/integers/arith-int-056.cvc | 16 ++ .../regress0/arith/integers/arith-int-057.cvc | 16 ++ .../regress0/arith/integers/arith-int-058.cvc | 16 ++ .../regress0/arith/integers/arith-int-059.cvc | 16 ++ .../regress0/arith/integers/arith-int-060.cvc | 16 ++ .../regress0/arith/integers/arith-int-061.cvc | 24 +++ .../regress0/arith/integers/arith-int-062.cvc | 24 +++ .../regress0/arith/integers/arith-int-063.cvc | 24 +++ .../regress0/arith/integers/arith-int-064.cvc | 24 +++ .../regress0/arith/integers/arith-int-065.cvc | 24 +++ .../regress0/arith/integers/arith-int-066.cvc | 18 ++ .../regress0/arith/integers/arith-int-067.cvc | 18 ++ .../regress0/arith/integers/arith-int-068.cvc | 18 ++ .../regress0/arith/integers/arith-int-069.cvc | 18 ++ .../regress0/arith/integers/arith-int-070.cvc | 18 ++ .../regress0/arith/integers/arith-int-071.cvc | 19 ++ .../regress0/arith/integers/arith-int-072.cvc | 19 ++ .../regress0/arith/integers/arith-int-073.cvc | 19 ++ .../regress0/arith/integers/arith-int-074.cvc | 19 ++ .../regress0/arith/integers/arith-int-075.cvc | 19 ++ .../regress0/arith/integers/arith-int-076.cvc | 12 ++ .../regress0/arith/integers/arith-int-077.cvc | 12 ++ .../regress0/arith/integers/arith-int-078.cvc | 12 ++ .../regress0/arith/integers/arith-int-079.cvc | 12 ++ .../regress0/arith/integers/arith-int-080.cvc | 12 ++ .../regress0/arith/integers/arith-int-081.cvc | 8 + .../regress0/arith/integers/arith-int-082.cvc | 8 + .../regress0/arith/integers/arith-int-083.cvc | 8 + .../regress0/arith/integers/arith-int-084.cvc | 8 + .../regress0/arith/integers/arith-int-085.cvc | 9 + .../regress0/arith/integers/arith-int-086.cvc | 14 ++ .../regress0/arith/integers/arith-int-087.cvc | 14 ++ .../regress0/arith/integers/arith-int-088.cvc | 14 ++ .../regress0/arith/integers/arith-int-089.cvc | 14 ++ .../regress0/arith/integers/arith-int-090.cvc | 14 ++ .../regress0/arith/integers/arith-int-091.cvc | 23 +++ .../regress0/arith/integers/arith-int-092.cvc | 23 +++ .../regress0/arith/integers/arith-int-093.cvc | 23 +++ .../regress0/arith/integers/arith-int-094.cvc | 23 +++ .../regress0/arith/integers/arith-int-095.cvc | 23 +++ .../regress0/arith/integers/arith-int-096.cvc | 9 + .../regress0/arith/integers/arith-int-097.cvc | 9 + .../regress0/arith/integers/arith-int-098.cvc | 9 + .../regress0/arith/integers/arith-int-099.cvc | 9 + .../regress0/arith/integers/arith-int-100.cvc | 9 + .../arith/integers/arith-interval.cvc | 8 + 148 files changed, 2559 insertions(+), 82 deletions(-) create mode 100644 src/theory/arith/dio_solver.cpp create mode 100644 src/theory/arith/dio_solver.h create mode 100644 src/util/pseudoboolean.cpp create mode 100644 src/util/pseudoboolean.h create mode 100644 test/regress/regress0/arith/Makefile create mode 100644 test/regress/regress0/arith/integers/Makefile create mode 100644 test/regress/regress0/arith/integers/Makefile.am create mode 100644 test/regress/regress0/arith/integers/arith-int-001.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-002.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-003.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-004.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-005.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-006.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-007.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-008.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-009.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-010.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-011.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-012.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-013.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-014.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-015.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-016.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-017.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-018.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-019.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-020.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-021.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-022.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-023.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-024.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-025.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-026.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-027.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-028.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-029.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-030.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-031.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-032.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-033.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-034.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-035.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-036.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-037.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-038.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-039.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-040.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-041.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-042.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-042.min.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-043.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-044.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-045.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-046.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-047.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-048.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-049.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-050.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-051.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-052.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-053.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-054.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-055.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-056.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-057.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-058.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-059.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-060.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-061.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-062.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-063.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-064.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-065.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-066.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-067.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-068.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-069.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-070.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-071.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-072.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-073.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-074.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-075.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-076.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-077.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-078.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-079.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-080.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-081.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-082.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-083.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-084.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-085.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-086.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-087.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-088.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-089.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-090.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-091.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-092.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-093.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-094.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-095.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-096.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-097.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-098.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-099.cvc create mode 100644 test/regress/regress0/arith/integers/arith-int-100.cvc create mode 100644 test/regress/regress0/arith/integers/arith-interval.cvc diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 5c3e4731b..0ac215f1e 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -509,9 +509,12 @@ public: /** Get the (singleton) type for integers. */ inline TypeNode integerType(); - /** Get the (singleton) type for booleans. */ + /** Get the (singleton) type for reals. */ inline TypeNode realType(); + /** Get the (singleton) type for pseudobooleans. */ + inline TypeNode pseudobooleanType(); + /** Get the (singleton) type for sorts. */ inline TypeNode kindType(); @@ -772,6 +775,11 @@ inline TypeNode NodeManager::realType() { return TypeNode(mkTypeConst(REAL_TYPE)); } +/** Get the (singleton) type for pseudobooleans. */ +inline TypeNode NodeManager::pseudobooleanType() { + return TypeNode(mkTypeConst(PSEUDOBOOLEAN_TYPE)); +} + /** Get the (singleton) type for sorts. */ inline TypeNode NodeManager::kindType() { return TypeNode(mkTypeConst(KIND_TYPE)); diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 077fc5ee2..e162065b0 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -202,6 +202,19 @@ Type::operator RealType() const throw(AssertionException) { return RealType(*this); } +/** Is this the pseudoboolean type? */ +bool Type::isPseudoboolean() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->isPseudoboolean(); +} + +/** Cast to a pseudoboolean type */ +Type::operator PseudobooleanType() const throw(AssertionException) { + NodeManagerScope nms(d_nodeManager); + Assert(isPseudoboolean()); + return PseudobooleanType(*this); +} + /** Is this the bit-vector type? */ bool Type::isBitVector() const { NodeManagerScope nms(d_nodeManager); @@ -435,6 +448,11 @@ RealType::RealType(const Type& t) throw(AssertionException) : Assert(isReal()); } +PseudobooleanType::PseudobooleanType(const Type& t) throw(AssertionException) : + Type(t) { + Assert(isPseudoboolean()); +} + BitVectorType::BitVectorType(const Type& t) throw(AssertionException) : Type(t) { Assert(isBitVector()); diff --git a/src/expr/type.h b/src/expr/type.h index 14ca3baf3..a63ca6cf0 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -46,6 +46,7 @@ class NodeTemplate; class BooleanType; class IntegerType; class RealType; +class PseudobooleanType; class BitVectorType; class ArrayType; class DatatypeType; @@ -225,6 +226,18 @@ public: */ operator RealType() const throw(AssertionException); + /** + * Is this the pseudoboolean type? + * @return true if the type is the pseudoboolean type + */ + bool isPseudoboolean() const; + + /** + * Cast this type to a pseudoboolean type + * @return the PseudobooleanType + */ + operator PseudobooleanType() const throw(AssertionException); + /** * Is this the bit-vector type? * @return true if the type is a bit-vector type @@ -409,6 +422,17 @@ public: RealType(const Type& type) throw(AssertionException); };/* class RealType */ +/** + * Singleton class encapsulating the pseudoboolean type. + */ +class CVC4_PUBLIC PseudobooleanType : public Type { + +public: + + /** Construct from the base type */ + PseudobooleanType(const Type& type) throw(AssertionException); +};/* class PseudobooleanType */ + /** * Class encapsulating a function type. */ diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index b9047307d..76a084204 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -73,18 +73,26 @@ Node TypeNode::mkGroundTerm() const { bool TypeNode::isBoolean() const { return getKind() == kind::TYPE_CONSTANT && - getConst() == BOOLEAN_TYPE; + ( getConst() == BOOLEAN_TYPE || + getConst() == PSEUDOBOOLEAN_TYPE ); } bool TypeNode::isInteger() const { return getKind() == kind::TYPE_CONSTANT && - getConst() == INTEGER_TYPE; + ( getConst() == INTEGER_TYPE || + getConst() == PSEUDOBOOLEAN_TYPE ); } bool TypeNode::isReal() const { - return getKind() == kind::TYPE_CONSTANT - && ( getConst() == REAL_TYPE || - getConst() == INTEGER_TYPE ); + return getKind() == kind::TYPE_CONSTANT && + ( getConst() == REAL_TYPE || + getConst() == INTEGER_TYPE || + getConst() == PSEUDOBOOLEAN_TYPE ); +} + +bool TypeNode::isPseudoboolean() const { + return getKind() == kind::TYPE_CONSTANT && + getConst() == PSEUDOBOOLEAN_TYPE; } bool TypeNode::isArray() const { diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 0f4b122db..3f4e52d36 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -413,6 +413,9 @@ public: /** Is this the Real type? */ bool isReal() const; + /** Is this the Pseudoboolean type? */ + bool isPseudoboolean() const; + /** Is this an array type? */ bool isArray() const; diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index cd4c66664..75a59c6e0 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -53,6 +53,7 @@ tokens { CHECK_TYPE_TOK = 'CHECK_TYPE'; GET_CHILD_TOK = 'GET_CHILD'; GET_OP_TOK = 'GET_OP'; + GET_VALUE_TOK = 'GET_VALUE'; SUBSTITUTE_TOK = 'SUBSTITUTE'; DBG_TOK = 'DBG'; TRACE_TOK = 'TRACE'; @@ -646,6 +647,9 @@ mainCommand[CVC4::Command*& cmd] | GET_OP_TOK formula[f] { UNSUPPORTED("GET_OP command"); } + | GET_VALUE_TOK formula[f] + { cmd = new GetValueCommand(f); } + | SUBSTITUTE_TOK identifier[id,CHECK_NONE,SYM_VARIABLE] COLON type[t,CHECK_DECLARED] EQUAL_TOK formula[f] LBRACKET identifier[id,CHECK_NONE,SYM_VARIABLE] ASSIGN_TOK formula[f] RBRACKET { UNSUPPORTED("SUBSTITUTE command"); } diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 11d633271..8e089a8a3 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -102,6 +102,9 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, case BOOLEAN_TYPE: out << "BOOLEAN"; break; + case PSEUDOBOOLEAN_TYPE: + out << "PSEUDOBOOLEAN"; + break; case KIND_TYPE: out << "TYPE"; break; diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 9b0c4847b..9797e4c67 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -146,7 +146,7 @@ SatLiteral CnfStream::convertAtom(TNode node) { Assert(!isTranslated(node), "atom already mapped!"); - bool theoryLiteral = node.getKind() != kind::VARIABLE; + bool theoryLiteral = node.getKind() != kind::VARIABLE && !node.getType().isPseudoboolean(); SatLiteral lit = newLiteral(node, theoryLiteral); if(node.getKind() == kind::CONST_BOOLEAN) { @@ -396,9 +396,8 @@ SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) { break; case EQUAL: if(node[0].getType().isBoolean()) { - // should have an IFF instead - Unreachable("= Bool Bool shouldn't be possible ?!"); - //nodeLit = handleIff(node[0].iffNode(node[1])); + // normally this is an IFF, but EQUAL is possible with pseudobooleans + nodeLit = handleIff(node[0].iffNode(node[1])); } else { nodeLit = convertAtom(node); } diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 60030bbab..dcfa43424 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -618,7 +618,7 @@ void SmtEnginePrivate::simplifyAssertions() throw(NoSuchFunctionException, Asser Debug("simplify") << "SmtEnginePrivate::simplify()" << std::endl; if(!Options::current()->lazyDefinitionExpansion) { - Debug("simplify") << "SmtEnginePrivate::simplify(): exanding definitions" << std::endl; + Debug("simplify") << "SmtEnginePrivate::simplify(): expanding definitions" << std::endl; TimerStat::CodeTimer codeTimer(d_smt.d_definitionExpansionTime); hash_map cache; for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) { diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am index 7f193b9e3..36ab2cd68 100644 --- a/src/theory/arith/Makefile.am +++ b/src/theory/arith/Makefile.am @@ -32,7 +32,9 @@ libarith_la_SOURCES = \ simplex.h \ simplex.cpp \ theory_arith.h \ - theory_arith.cpp + theory_arith.cpp \ + dio_solver.h \ + dio_solver.cpp EXTRA_DIST = \ kinds diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index d2ecaffe4..8d12e78fe 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -182,7 +182,6 @@ RewriteResponse ArithRewriter::postRewriteAtomConstantRHS(TNode t){ TNode left = t[0]; TNode right = t[1]; - Comparison cmp = Comparison::mkComparison(t.getKind(), Polynomial::parsePolynomial(left), Constant(right)); if(cmp.isBoolean()){ diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp index 77a89b54b..a5fa428c6 100644 --- a/src/theory/arith/arith_static_learner.cpp +++ b/src/theory/arith/arith_static_learner.cpp @@ -24,6 +24,9 @@ #include "util/propositional_query.h" +#include "expr/expr.h" +#include "expr/convenience_node_builders.h" + #include using namespace std; @@ -34,9 +37,10 @@ using namespace CVC4::theory; using namespace CVC4::theory::arith; -ArithStaticLearner::ArithStaticLearner(): +ArithStaticLearner::ArithStaticLearner(SubstitutionMap& pbSubstitutions) : d_miplibTrick(), d_miplibTrickKeys(), + d_pbSubstitutions(pbSubstitutions), d_statistics() {} @@ -105,9 +109,11 @@ void ArithStaticLearner::staticLearning(TNode n, NodeBuilder<>& learned){ postProcess(learned); } + void ArithStaticLearner::clear(){ d_miplibTrick.clear(); d_miplibTrickKeys.clear(); + // do not clear d_pbSubstitutions, as it is shared } @@ -151,11 +157,101 @@ void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet d_minMap[n] = coerceToRational(n); d_maxMap[n] = coerceToRational(n); break; + case OR: { + // Look for things like "x = 0 OR x = 1" (that are defTrue) and + // turn them into a pseudoboolean. We catch "x >= 0 + if(defTrue.find(n) == defTrue.end() || + n.getNumChildren() != 2 || + n[0].getKind() != EQUAL || + n[1].getKind() != EQUAL) { + break; + } + Node var, c1, c2; + if(n[0][0].getMetaKind() == metakind::VARIABLE && + n[0][1].getMetaKind() == metakind::CONSTANT) { + var = n[0][0]; + c1 = n[0][1]; + } else if(n[0][1].getMetaKind() == metakind::VARIABLE && + n[0][0].getMetaKind() == metakind::CONSTANT) { + var = n[0][1]; + c1 = n[0][0]; + } else { + break; + } + if(!var.getType().isInteger() || + !c1.getType().isReal()) { + break; + } + if(var == n[1][0]) { + c2 = n[1][1]; + } else if(var == n[1][1]) { + c2 = n[1][0]; + } else { + break; + } + if(!c2.getType().isReal()) { + break; + } + + Integer k1, k2; + if(c1.getType().getConst() == INTEGER_TYPE) { + k1 = c1.getConst(); + } else { + Rational r = c1.getConst(); + if(r.getDenominator() == 1) { + k1 = r.getNumerator(); + } else { + break; + } + } + if(c2.getType().getConst() == INTEGER_TYPE) { + k2 = c2.getConst(); + } else { + Rational r = c2.getConst(); + if(r.getDenominator() == 1) { + k2 = r.getNumerator(); + } else { + break; + } + } + if(k1 > k2) { + swap(k1, k2); + } + if(k1 + 1 == k2) { + Debug("arith::static") << "==> found " << n << endl + << " which indicates " << var << " \\in { " + << k1 << " , " << k2 << " }" << endl; + c1 = NodeManager::currentNM()->mkConst(k1); + c2 = NodeManager::currentNM()->mkConst(k2); + Node lhs = NodeBuilder<2>(kind::GEQ) << var << c1; + Node rhs = NodeBuilder<2>(kind::LEQ) << var << c2; + Node l = lhs && rhs; + Debug("arith::static") << " learned: " << l << endl; + learned << l; + if(k1 == 0) { + Assert(k2 == 1); + replaceWithPseudoboolean(var); + } + } + break; + } default: // Do nothing break; } } +void ArithStaticLearner::replaceWithPseudoboolean(TNode var) { + AssertArgument(var.getMetaKind() == kind::metakind::VARIABLE, var); + TypeNode pbType = NodeManager::currentNM()->pseudobooleanType(); + Node pbVar = NodeManager::currentNM()->mkVar(string("PB[") + var.toString() + ']', pbType); + d_pbSubstitutions.addSubstitution(var, pbVar); + + if(Debug.isOn("pb")) { + Expr::printtypes::Scope pts(Debug("pb"), true); + Debug("pb") << "will replace " << var << " with " << pbVar << endl; + } +} + void ArithStaticLearner::iteMinMax(TNode n, NodeBuilder<>& learned){ Assert(n.getKind() == kind::ITE); Assert(n[0].getKind() != EQUAL); @@ -341,6 +437,27 @@ void ArithStaticLearner::miplibTrick(TNode var, set& values, NodeBuild } } +void ArithStaticLearner::checkBoundsForPseudobooleanReplacement(TNode n) { + NodeToMinMaxMap::iterator minFind = d_minMap.find(n); + NodeToMinMaxMap::iterator maxFind = d_maxMap.find(n); + + if( n.getType().isInteger() && + minFind != d_minMap.end() && + maxFind != d_maxMap.end() && + ( ( (*minFind).second.getNoninfinitesimalPart() == 1 && + (*minFind).second.getInfinitesimalPart() == 0 ) || + ( (*minFind).second.getNoninfinitesimalPart() == 0 && + (*minFind).second.getInfinitesimalPart() > 0 ) ) && + ( ( (*maxFind).second.getNoninfinitesimalPart() == 1 && + (*maxFind).second.getInfinitesimalPart() == 0 ) || + ( (*maxFind).second.getNoninfinitesimalPart() == 2 && + (*maxFind).second.getInfinitesimalPart() < 0 ) ) ) { + // eligible for pseudoboolean replacement + Debug("pb") << "eligible for pseudoboolean replacement: " << n << endl; + replaceWithPseudoboolean(n); + } +} + void ArithStaticLearner::addBound(TNode n) { NodeToMinMaxMap::iterator minFind = d_minMap.find(n[0]); @@ -349,25 +466,29 @@ void ArithStaticLearner::addBound(TNode n) { Rational constant = coerceToRational(n[1]); DeltaRational bound = constant; - switch(n.getKind()) { + switch(Kind k = n.getKind()) { case kind::LT: bound = DeltaRational(constant, -1); + /* fall through */ case kind::LEQ: if (maxFind == d_maxMap.end() || maxFind->second > bound) { d_maxMap[n[0]] = bound; Debug("arith::static") << "adding bound " << n << endl; + checkBoundsForPseudobooleanReplacement(n[0]); } break; case kind::GT: bound = DeltaRational(constant, 1); + /* fall through */ case kind::GEQ: if (minFind == d_minMap.end() || minFind->second < bound) { d_minMap[n[0]] = bound; Debug("arith::static") << "adding bound " << n << endl; + checkBoundsForPseudobooleanReplacement(n[0]); } break; default: - // nothing else + Unhandled(k); break; } } diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h index 0ed9cbe85..c58778215 100644 --- a/src/theory/arith/arith_static_learner.h +++ b/src/theory/arith/arith_static_learner.h @@ -25,6 +25,7 @@ #include "util/stats.h" #include "theory/arith/arith_utilities.h" +#include "theory/substitutions.h" #include #include @@ -44,6 +45,19 @@ private: VarToNodeSetMap d_miplibTrick; std::list d_miplibTrickKeys; + /** + * Some integer variables are eligible to be replaced by + * pseudoboolean variables. This map collects those eligible + * substitutions. + * + * This is a reference to the substitution map in TheoryArith; as + * it's not "owned" by this static learner, it isn't cleared on + * clear(). This makes sense, as the static learner only + * accumulates information in the substitution map, it never uses it + * (i.e., it's write-only). + */ + SubstitutionMap& d_pbSubstitutions; + /** * Map from a node to it's minimum and maximum. */ @@ -52,7 +66,7 @@ private: NodeToMinMaxMap d_maxMap; public: - ArithStaticLearner(); + ArithStaticLearner(SubstitutionMap& pbSubstitutions); void staticLearning(TNode n, NodeBuilder<>& learned); void addBound(TNode n); @@ -64,11 +78,14 @@ private: void postProcess(NodeBuilder<>& learned); + void replaceWithPseudoboolean(TNode var); void iteMinMax(TNode n, NodeBuilder<>& learned); void iteConstant(TNode n, NodeBuilder<>& learned); void miplibTrick(TNode var, std::set& values, NodeBuilder<>& learned); + void checkBoundsForPseudobooleanReplacement(TNode n); + /** These fields are designed to be accessable to ArithStaticLearner methods. */ class Statistics { public: diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index 78b77eb00..2dee26be4 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -143,7 +143,7 @@ inline bool evaluateConstantPredicate(Kind k, const Rational& left, const Ration } /** - * Returns the appropraite coefficient for the infinitesimal given the kind + * Returns the appropriate coefficient for the infinitesimal given the kind * for an arithmetic atom inorder to represent strict inequalities as inequalities. * x < c becomes x <= c + (-1) * \delta * x > c becomes x >= x + ( 1) * \delta diff --git a/src/theory/arith/arithvar_node_map.h b/src/theory/arith/arithvar_node_map.h index aca61878d..df82fde91 100644 --- a/src/theory/arith/arithvar_node_map.h +++ b/src/theory/arith/arithvar_node_map.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file arithvar_node_map.h + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "cvc4_private.h" #ifndef __CVC4__THEORY__ARITH__ARITHVAR_NODE_MAP_H diff --git a/src/theory/arith/arithvar_set.h b/src/theory/arith/arithvar_set.h index f8a23fee0..68937acc4 100644 --- a/src/theory/arith/arithvar_set.h +++ b/src/theory/arith/arithvar_set.h @@ -2,10 +2,10 @@ /*! \file arithvar_set.h ** \verbatim ** Original author: taking - ** Major contributors: mdeters + ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing @@ -17,13 +17,14 @@ ** \todo document this file **/ -#include -#include "theory/arith/arith_utilities.h" - +#include "cvc4_private.h" #ifndef __CVC4__THEORY__ARITH__ARTIHVAR_SET_H #define __CVC4__THEORY__ARITH__ARTIHVAR_SET_H +#include +#include "theory/arith/arith_utilities.h" + namespace CVC4 { namespace theory { namespace arith { @@ -33,7 +34,7 @@ namespace arith { * This class is designed to provide constant time insertion, deletion, and element_of * and fast iteration. * - * ArithVarSets come in 2 varieties ArithVarSet, and PermissiveBackArithVarSet. + * ArithVarSets come in 2 varieties: ArithVarSet, and PermissiveBackArithVarSet. * The default ArithVarSet assumes that there is no knowledge assumed about ArithVars * that are greater than allocated(). Asking isMember() of such an ArithVar * is an assertion failure. The cost of doing this is that it takes O(M) @@ -324,8 +325,8 @@ public: } }; -}; /* namespace arith */ -}; /* namespace theory */ -}; /* namespace CVC4 */ +}/* CVC4::theory::arith namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ #endif /* __CVC4__THEORY__ARITH__ARTIHVAR_SET_H */ diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp new file mode 100644 index 000000000..151859f21 --- /dev/null +++ b/src/theory/arith/dio_solver.cpp @@ -0,0 +1,118 @@ +/********************* */ +/*! \file dio_solver.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Diophantine equation solver + ** + ** A Diophantine equation solver for the theory of arithmetic. + **/ + +#include "theory/arith/dio_solver.h" + +#include + +using namespace std; + +namespace CVC4 { +namespace theory { +namespace arith { + +/* +static void printEquation(vector& coeffs, + vector& variables, + ostream& out) { + Assert(coeffs.size() == variables.size()); + vector::const_iterator i = coeffs.begin(); + vector::const_iterator j = variables.begin(); + while(i != coeffs.end()) { + out << *i << "*" << *j; + ++i; + ++j; + if(i != coeffs.end()) { + out << " + "; + } + } + out << " = 0"; +} +*/ + +bool DioSolver::solve() { + Trace("integers") << "DioSolver::solve()" << endl; + if(Debug.isOn("integers")) { + ScopedDebug dtab("tableau"); + d_tableau.printTableau(); + } + for(ArithVarSet::const_iterator i = d_tableau.beginBasic(); + i != d_tableau.endBasic(); + ++i) { + Debug("integers") << "going through row " << *i << endl; + + Integer m = 1; + for(Tableau::RowIterator j = d_tableau.rowIterator(*i); !j.atEnd(); ++j) { + Debug("integers") << " column " << (*j).getCoefficient() << " * " << (*j).getColVar() << endl; + m *= (*j).getCoefficient().getDenominator(); + } + Assert(m >= 1); + Debug("integers") << "final multiplier is " << m << endl; + + Integer gcd = 0; + Rational c = 0; + Debug("integers") << "going throw row " << *i << " to find gcd" << endl; + for(Tableau::RowIterator j = d_tableau.rowIterator(*i); !j.atEnd(); ++j) { + Rational r = (*j).getCoefficient(); + ArithVar v = (*j).getColVar(); + r *= m; + Debug("integers") << " column " << r << " * " << v << endl; + Assert(r.getDenominator() == 1); + bool foundConstant = false; + // The tableau doesn't store constants. Constants int he input + // are mapped to slack variables that are constrained with + // bounds in the partial model. So we detect and accumulate all + // variables whose upper bound equals their lower bound, which + // catches these input constants as well as any (contextually) + // eliminated variables. + if(d_partialModel.hasUpperBound(v) && d_partialModel.hasLowerBound(v)) { + DeltaRational b = d_partialModel.getLowerBound(v); + if(b.getInfinitesimalPart() == 0 && b == d_partialModel.getUpperBound(v)) { + r *= b.getNoninfinitesimalPart(); + Debug("integers") << " var " << v << " == [" << b << "], so found a constant part " << r << endl; + c += r; + foundConstant = true; + } + } + if(!foundConstant) { + // calculate gcd of all (NON-constant) coefficients + gcd = (gcd == 0) ? r.getNumerator().abs() : gcd.gcd(r.getNumerator()); + Debug("integers") << " gcd now " << gcd << endl; + } + } + Debug("integers") << "addEquation: gcd is " << gcd << ", c is " << c << endl; + // The gcd must divide c for this equation to be satisfiable. + // If c is not an integer, there's no way it can. + if(c.getDenominator() == 1 && gcd == gcd.gcd(c.getNumerator())) { + Trace("integers") << "addEquation: this eqn is fine" << endl; + } else { + Trace("integers") << "addEquation: eqn not satisfiable, returning false" << endl; + return false; + } + } + + return true; +} + +void DioSolver::getSolution() { + Unimplemented(); +} + +}/* CVC4::theory::arith namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h new file mode 100644 index 000000000..c91ddd994 --- /dev/null +++ b/src/theory/arith/dio_solver.h @@ -0,0 +1,72 @@ +/********************* */ +/*! \file dio_solver.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Diophantine equation solver + ** + ** A Diophantine equation solver for the theory of arithmetic. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__ARITH__DIO_SOLVER_H +#define __CVC4__THEORY__ARITH__DIO_SOLVER_H + +#include "context/context.h" + +#include "theory/arith/tableau.h" +#include "theory/arith/partial_model.h" +#include "theory/arith/arith_utilities.h" +#include "util/rational.h" + +#include +#include + +namespace CVC4 { +namespace theory { +namespace arith { + +class DioSolver { + context::Context* d_context; + const Tableau& d_tableau; + ArithPartialModel& d_partialModel; + +public: + + /** Construct a Diophantine equation solver with the given context. */ + DioSolver(context::Context* ctxt, const Tableau& tab, ArithPartialModel& pmod) : + d_context(ctxt), + d_tableau(tab), + d_partialModel(pmod) { + } + + /** + * Solve the set of Diophantine equations in the tableau. + * + * @return true if the set of equations was solved; false if no + * solution + */ + bool solve(); + + /** + * Get the parameterized solution to this set of Diophantine + * equations. Must be preceded by a call to solve() that returned + * true. */ + void getSolution(); + +};/* class DioSolver */ + +}/* CVC4::theory::arith namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__ARITH__DIO_SOLVER_H */ diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index 1871e897a..db47062bb 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -30,18 +30,28 @@ sort INTEGER_TYPE \ "NodeManager::currentNM()->mkConst(Integer(0))" \ "expr/node_manager.h" \ "Integer type" +sort PSEUDOBOOLEAN_TYPE \ + 2 \ + well-founded \ + "NodeManager::currentNM()->mkConst(Pseudoboolean(0))" \ + "expr/node_manager.h" \ + "Pseudoboolean type" constant CONST_RATIONAL \ ::CVC4::Rational \ ::CVC4::RationalHashStrategy \ "util/rational.h" \ "a multiple-precision rational constant" - constant CONST_INTEGER \ ::CVC4::Integer \ ::CVC4::IntegerHashStrategy \ "util/integer.h" \ "a multiple-precision integer constant" +constant CONST_PSEUDOBOOLEAN \ + ::CVC4::Pseudoboolean \ + ::CVC4::PseudobooleanHashStrategy \ + "util/pseudoboolean.h" \ + "a pseudoboolean constant" operator LT 2 "less than, x < y" operator LEQ 2 "less than or equal, x <= y" diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp index aea1a43d8..b529a8077 100644 --- a/src/theory/arith/normal_form.cpp +++ b/src/theory/arith/normal_form.cpp @@ -254,6 +254,58 @@ Comparison Comparison::parseNormalForm(TNode n) { } } +bool Comparison::pbComparison(Kind k, TNode left, const Rational& right, bool& result) { + AssertArgument(left.getType().isPseudoboolean(), left); + switch(k) { + case kind::LT: + if(right > 1) { + result = true; + return true; + } else if(right <= 0) { + result = false; + return true; + } + break; + case kind::LEQ: + if(right >= 1) { + result = true; + return true; + } else if(right < 0) { + result = false; + return true; + } + break; + case kind::EQUAL: + if(right != 0 && right != 1) { + result = false; + return true; + } + break; + case kind::GEQ: + if(right > 1) { + result = false; + return true; + } else if(right <= 0) { + result = true; + return true; + } + break; + case kind::GT: + if(right >= 1) { + result = false; + return true; + } else if(right < 0) { + result = true; + return true; + } + break; + default: + CheckArgument(false, k, "Bad comparison operator ?!"); + } + + return false; +} + Comparison Comparison::mkComparison(Kind k, const Polynomial& left, const Constant& right) { Assert(isRelationOperator(k)); if(left.isConstant()) { @@ -261,9 +313,16 @@ Comparison Comparison::mkComparison(Kind k, const Polynomial& left, const Consta const Rational& rConst = right.getNode().getConst(); bool res = evaluateConstantPredicate(k, lConst, rConst); return Comparison(res); - } else { - return Comparison(toNode(k, left, right), k, left, right); } + + if(left.getNode().getType().isPseudoboolean()) { + bool result; + if(pbComparison(k, left.getNode(), right.getNode().getConst(), result)) { + return Comparison(result); + } + } + + return Comparison(toNode(k, left, right), k, left, right); } Comparison Comparison::addConstant(const Constant& constant) const { diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h index 5d6ca27e9..d6e79318d 100644 --- a/src/theory/arith/normal_form.h +++ b/src/theory/arith/normal_form.h @@ -702,6 +702,22 @@ private: Comparison(TNode n, Kind k, const Polynomial& l, const Constant& r): NodeWrapper(n), oper(k), left(l), right(r) { } + + /** + * Possibly simplify a comparison with a pseudoboolean-typed LHS. k + * is one of LT, LEQ, EQUAL, GEQ, GT, and left must be PB-typed. If + * possible, "left k right" is fully evaluated, "true" is returned, + * and the result of the evaluation is returned in "result". If no + * evaluation is possible, false is returned and "result" is + * untouched. + * + * For example, pbComparison(kind::EQUAL, "x", 0.5, result) returns + * true, and updates "result" to false, since pseudoboolean variable + * "x" can never equal 0.5. pbComparison(kind::GEQ, "x", 1, result) + * returns false, since "x" can be >= 1, but could also be less. + */ + static bool pbComparison(Kind k, TNode left, const Rational& right, bool& result); + public: Comparison(bool val) : NodeWrapper(NodeManager::currentNM()->mkConst(val)), diff --git a/src/theory/arith/ordered_set.h b/src/theory/arith/ordered_set.h index 43ccd7815..e44ba8687 100644 --- a/src/theory/arith/ordered_set.h +++ b/src/theory/arith/ordered_set.h @@ -53,14 +53,18 @@ public: void addLeq(TNode leq){ Assert(leq.getKind() == kind::LEQ); Assert(rightHandRational(leq) == getValue()); - Assert(!hasLeq()); + // [MGD] With context-dependent pre-registration, we could get the + // same one twice + Assert(!hasLeq() || d_leq == leq); d_leq = leq; } void addGeq(TNode geq){ Assert(geq.getKind() == kind::GEQ); Assert(rightHandRational(geq) == getValue()); - Assert(!hasGeq()); + // [MGD] With context-dependent pre-registration, we could get the + // same one twice + Assert(!hasGeq() || d_geq == geq); d_geq = geq; } diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h index 171c74942..f07e524aa 100644 --- a/src/theory/arith/partial_model.h +++ b/src/theory/arith/partial_model.h @@ -86,7 +86,7 @@ public: /* Initializes a variable to a safe value.*/ void initialize(ArithVar x, const DeltaRational& r); - /* Gets the last assignment to a variable that is known to be conistent. */ + /* Gets the last assignment to a variable that is known to be consistent. */ const DeltaRational& getSafeAssignment(ArithVar x) const; const DeltaRational& getAssignment(ArithVar x, bool safe) const; @@ -183,14 +183,12 @@ private: return 0 <= x && x < d_mapSize; } -}; +};/* class ArithPartialModel */ - - -}; /* namesapce arith */ -}; /* namespace theory */ -}; /* namespace CVC4 */ +}/* CVC4::theory::arith namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp index 367e90301..b432416bd 100644 --- a/src/theory/arith/tableau.cpp +++ b/src/theory/arith/tableau.cpp @@ -115,7 +115,7 @@ void Tableau::setColumnUnused(ArithVar v){ ++colIter; } } -void Tableau::printTableau(){ +void Tableau::printTableau() const { Debug("tableau") << "Tableau::d_activeRows" << endl; ArithVarSet::const_iterator basicIter = beginBasic(), endIter = endBasic(); @@ -125,7 +125,7 @@ void Tableau::printTableau(){ } } -void Tableau::printRow(ArithVar basic){ +void Tableau::printRow(ArithVar basic) const { Debug("tableau") << "{" << basic << ":"; for(RowIterator entryIter = rowIterator(basic); !entryIter.atEnd(); ++entryIter){ const TableauEntry& entry = *entryIter; @@ -135,7 +135,7 @@ void Tableau::printRow(ArithVar basic){ Debug("tableau") << "}" << endl; } -void Tableau::printEntry(const TableauEntry& entry){ +void Tableau::printEntry(const TableauEntry& entry) const { Debug("tableau") << entry.getColVar() << "*" << entry.getCoefficient(); } diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index fa227757a..e14436f8c 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -224,10 +224,10 @@ private: class Iterator { private: EntryID d_curr; - TableauEntryManager& d_entryManager; + const TableauEntryManager& d_entryManager; public: - Iterator(EntryID start, TableauEntryManager& manager) : + Iterator(EntryID start, const TableauEntryManager& manager) : d_curr(start), d_entryManager(manager) {} @@ -244,7 +244,7 @@ private: Iterator& operator++(){ Assert(!atEnd()); - TableauEntry& entry = d_entryManager.get(d_curr); + const TableauEntry& entry = d_entryManager.get(d_curr); d_curr = isRowIterator ? entry.getNextRowID() : entry.getNextColID(); return *this; } @@ -288,13 +288,13 @@ public: return d_basicVariables.end(); } - RowIterator rowIterator(ArithVar v){ + RowIterator rowIterator(ArithVar v) const { Assert(v < d_rowHeads.size()); EntryID head = d_rowHeads[v]; return RowIterator(head, d_entryManager); } - ColIterator colIterator(ArithVar v){ + ColIterator colIterator(ArithVar v) const { Assert(v < d_colHeads.size()); EntryID head = d_colHeads[v]; return ColIterator(head, d_entryManager); @@ -350,9 +350,9 @@ public: /** * Prints the contents of the Tableau to Debug("tableau::print") */ - void printTableau(); - void printRow(ArithVar basic); - void printEntry(const TableauEntry& entry); + void printTableau() const; + void printRow(ArithVar basic) const; + void printEntry(const TableauEntry& entry) const; private: diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 3831536e9..2664aaac3 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -61,10 +61,13 @@ typedef expr::Attribute Slack; TheoryArith::TheoryArith(context::Context* c, OutputChannel& out, Valuation valuation) : Theory(THEORY_ARITH, c, out, valuation), + learner(d_pbSubstitutions), + d_nextIntegerCheckVar(0), d_partialModel(c), d_userVariables(), d_diseq(c), d_tableau(), + d_diosolver(c, d_tableau, d_partialModel), d_restartsCounter(0), d_rowHasBeenAdded(false), d_tableauResetDensity(1.6), @@ -131,13 +134,26 @@ TheoryArith::Statistics::~Statistics(){ } Node TheoryArith::preprocess(TNode atom) { - if (atom.getKind() == kind::EQUAL) { - Node leq = NodeBuilder<2>(kind::LEQ) << atom[0] << atom[1]; - Node geq = NodeBuilder<2>(kind::GEQ) << atom[0] << atom[1]; - return Rewriter::rewrite(leq.andNode(geq)); - } else { - return atom; + Debug("arith::preprocess") << "arith::preprocess() : " << atom << endl; + + Node a = d_pbSubstitutions.apply(atom); + + if (a != atom) { + Debug("pb") << "arith::preprocess() : after pb substitutions: " << a << endl; + a = Rewriter::rewrite(a); + Debug("pb") << "arith::preprocess() : after pb substitutions and rewriting: " << a << endl; + Debug("arith::preprocess") << "arith::preprocess() : after pb substitutions and rewriting: " << a << endl; + } + + if (a.getKind() == kind::EQUAL) { + Node leq = NodeBuilder<2>(kind::LEQ) << a[0] << a[1]; + Node geq = NodeBuilder<2>(kind::GEQ) << a[0] << a[1]; + Node rewritten = Rewriter::rewrite(leq.andNode(geq)); + Debug("arith::preprocess") << "arith::preprocess() : returning " << rewritten << endl; + return rewritten; } + + return a; } Theory::SolveStatus TheoryArith::solve(TNode in, SubstitutionMap& outSubstitutions) { @@ -187,8 +203,16 @@ Theory::SolveStatus TheoryArith::solve(TNode in, SubstitutionMap& outSubstitutio // Add the substitution if not recursive Node rewritten = Rewriter::rewrite(eliminateVar); if (!rewritten.hasSubterm(minVar)) { - outSubstitutions.addSubstitution(minVar, Rewriter::rewrite(eliminateVar)); - return SOLVE_STATUS_SOLVED; + Node elim = Rewriter::rewrite(eliminateVar); + if (!minVar.getType().isInteger() || elim.getType().isInteger()) { + // cannot eliminate integers here unless we know the resulting + // substitution is integral + Debug("simplify") << "TheoryArith::solve(): substitution " << minVar << " |-> " << elim << endl; + outSubstitutions.addSubstitution(minVar, elim); + return SOLVE_STATUS_SOLVED; + } else { + Debug("simplify") << "TheoryArith::solve(): can't substitute b/c it's integer: " << minVar << ":" << minVar.getType() << " |-> " << elim << ":" << elim.getType() << endl; + } } } } @@ -199,7 +223,7 @@ Theory::SolveStatus TheoryArith::solve(TNode in, SubstitutionMap& outSubstitutio case kind::LT: case kind::GEQ: case kind::GT: - if (in[0].getKind() == kind::VARIABLE) { + if (in[0].getMetaKind() == kind::metakind::VARIABLE) { learner.addBound(in); } break; @@ -290,16 +314,19 @@ void TheoryArith::preRegisterTerm(TNode n) { } } } - Debug("arith_preregister") << "end arith::preRegisterTerm("<< n <<")"<< endl; + Debug("arith_preregister") << "end arith::preRegisterTerm(" << n <<")" << endl; } ArithVar TheoryArith::requestArithVar(TNode x, bool basic){ Assert(isLeaf(x) || x.getKind() == PLUS); Assert(!d_arithvarNodeMap.hasArithVar(x)); + Assert(x.getType().isReal());// real or integer ArithVar varX = d_variables.size(); d_variables.push_back(Node(x)); + Debug("integers") << "isInteger[[" << x << "]]: " << x.getType().isInteger() << endl; + d_integerVars.push_back(x.getType().isPseudoboolean() ? 2 : (x.getType().isInteger() ? 1 : 0)); d_simplex.increaseMax(); @@ -570,6 +597,129 @@ void TheoryArith::check(Effort effortLevel){ } } + if(fullEffort(effortLevel) && d_integerVars.size() > 0) { + const ArithVar rrEnd = d_nextIntegerCheckVar; + do { + ArithVar v = d_nextIntegerCheckVar; + short type = d_integerVars[v]; + if(type > 0) { // integer + const DeltaRational& d = d_partialModel.getAssignment(v); + const Rational& r = d.getNoninfinitesimalPart(); + const Rational& i = d.getInfinitesimalPart(); + Trace("integers") << "integers: assignment to [[" << d_arithvarNodeMap.asNode(v) << "]] is " << r << "[" << i << "]" << endl; + if(type == 2) { + // pseudoboolean + if(r.getDenominator() == 1 && i.getNumerator() == 0 && + (r.getNumerator() == 0 || r.getNumerator() == 1)) { + // already pseudoboolean; skip + continue; + } + + TNode var = d_arithvarNodeMap.asNode(v); + Node zero = NodeManager::currentNM()->mkConst(Integer(0)); + Node one = NodeManager::currentNM()->mkConst(Integer(1)); + Node eq0 = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL, var, zero)); + Node eq1 = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL, var, one)); + Node lem = NodeManager::currentNM()->mkNode(kind::OR, eq0, eq1); + Trace("pb") << "pseudobooleans: branch & bound: " << lem << endl; + Trace("integers") << "pseudobooleans: branch & bound: " << lem << endl; + //d_out->lemma(lem); + } + if(r.getDenominator() == 1 && i.getNumerator() == 0) { + // already an integer assignment; skip + continue; + } + + // otherwise, try the Diophantine equation solver + //bool result = d_diosolver.solve(); + //Debug("integers") << "the dio solver returned " << (result ? "true" : "false") << endl; + + // branch and bound + if(r.getDenominator() == 1) { + // r is an integer, but the infinitesimal might not be + if(i.getNumerator() < 0) { + // lemma: v <= r - 1 || v >= r + + TNode var = d_arithvarNodeMap.asNode(v); + Node nrMinus1 = NodeManager::currentNM()->mkConst(r - 1); + Node nr = NodeManager::currentNM()->mkConst(r); + Node leq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::LEQ, var, nrMinus1)); + Node geq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::GEQ, var, nr)); + + Node lem = NodeManager::currentNM()->mkNode(kind::OR, leq, geq); + Trace("integers") << "integers: branch & bound: " << lem << endl; + if(d_valuation.isSatLiteral(lem[0])) { + Debug("integers") << " " << lem[0] << " == " << d_valuation.getSatValue(lem[0]) << endl; + } else { + Debug("integers") << " " << lem[0] << " is not assigned a SAT literal" << endl; + } + if(d_valuation.isSatLiteral(lem[1])) { + Debug("integers") << " " << lem[1] << " == " << d_valuation.getSatValue(lem[1]) << endl; + } else { + Debug("integers") << " " << lem[1] << " is not assigned a SAT literal" << endl; + } + d_out->lemma(lem); + + // split only on one var + break; + } else if(i.getNumerator() > 0) { + // lemma: v <= r || v >= r + 1 + + TNode var = d_arithvarNodeMap.asNode(v); + Node nr = NodeManager::currentNM()->mkConst(r); + Node nrPlus1 = NodeManager::currentNM()->mkConst(r + 1); + Node leq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::LEQ, var, nr)); + Node geq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::GEQ, var, nrPlus1)); + + Node lem = NodeManager::currentNM()->mkNode(kind::OR, leq, geq); + Trace("integers") << "integers: branch & bound: " << lem << endl; + if(d_valuation.isSatLiteral(lem[0])) { + Debug("integers") << " " << lem[0] << " == " << d_valuation.getSatValue(lem[0]) << endl; + } else { + Debug("integers") << " " << lem[0] << " is not assigned a SAT literal" << endl; + } + if(d_valuation.isSatLiteral(lem[1])) { + Debug("integers") << " " << lem[1] << " == " << d_valuation.getSatValue(lem[1]) << endl; + } else { + Debug("integers") << " " << lem[1] << " is not assigned a SAT literal" << endl; + } + d_out->lemma(lem); + + // split only on one var + break; + } else { + Unreachable(); + } + } else { + // lemma: v <= floor(r) || v >= ceil(r) + + TNode var = d_arithvarNodeMap.asNode(v); + Node floor = NodeManager::currentNM()->mkConst(r.floor()); + Node ceiling = NodeManager::currentNM()->mkConst(r.ceiling()); + Node leq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::LEQ, var, floor)); + Node geq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::GEQ, var, ceiling)); + + Node lem = NodeManager::currentNM()->mkNode(kind::OR, leq, geq); + Trace("integers") << "integers: branch & bound: " << lem << endl; + if(d_valuation.isSatLiteral(lem[0])) { + Debug("integers") << " " << lem[0] << " == " << d_valuation.getSatValue(lem[0]) << endl; + } else { + Debug("integers") << " " << lem[0] << " is not assigned a SAT literal" << endl; + } + if(d_valuation.isSatLiteral(lem[1])) { + Debug("integers") << " " << lem[1] << " == " << d_valuation.getSatValue(lem[1]) << endl; + } else { + Debug("integers") << " " << lem[1] << " is not assigned a SAT literal" << endl; + } + d_out->lemma(lem); + + // split only on one var + break; + } + }// if(arithvar is integer-typed) + } while((d_nextIntegerCheckVar = (1 + d_nextIntegerCheckVar == d_variables.size() ? 0 : 1 + d_nextIntegerCheckVar)) != rrEnd); + }// if(full effort) + if(Debug.isOn("paranoid:check_tableau")){ d_simplex.debugCheckTableau(); } if(Debug.isOn("arith::print_model")) { debugPrintModel(); } Debug("arith") << "TheoryArith::check end" << std::endl; @@ -866,7 +1016,9 @@ void TheoryArith::presolve(){ for(VarIter i = d_variables.begin(), end = d_variables.end(); i != end; ++i){ Node variableNode = *i; ArithVar var = d_arithvarNodeMap.asArithVar(variableNode); - if(d_userVariables.isMember(var) && !d_atomDatabase.hasAnyAtoms(variableNode)){ + if(d_userVariables.isMember(var) && + !d_atomDatabase.hasAnyAtoms(variableNode) && + !variableNode.getType().isInteger()){ //The user variable is unconstrained. //Remove this variable permanently permanentlyRemoveVariable(var); diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 0c15c824c..7e14f6b06 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -38,6 +38,7 @@ #include "theory/arith/arith_static_learner.h" #include "theory/arith/arith_prop_manager.h" #include "theory/arith/arithvar_node_map.h" +#include "theory/arith/dio_solver.h" #include "util/stats.h" @@ -68,6 +69,21 @@ private: ArithVarNodeMap d_arithvarNodeMap; + /** + * List of the types of variables in the system. + * "True" means integer, "false" means (non-integer) real. + */ + std::vector d_integerVars; + + /** + * On full effort checks (after determining LA(Q) satisfiability), we + * consider integer vars, but we make sure to do so fairly to avoid + * nontermination (although this isn't a guarantee). To do it fairly, + * we consider variables in round-robin fashion. This is the + * round-robin index. + */ + ArithVar d_nextIntegerCheckVar; + /** * If ArithVar v maps to the node n in d_removednode, * then n = (= asNode(v) rhs) where rhs is a term that @@ -86,8 +102,6 @@ private: */ ArithVarSet d_userVariables; - - /** * List of all of the inequalities asserted in the current context. */ @@ -98,6 +112,23 @@ private: */ Tableau d_tableau; + /** + * A Diophantine equation solver. Accesses the tableau and partial + * model (each in a read-only fashion). + */ + DioSolver d_diosolver; + + /** + * Some integer variables can be replaced with pseudoboolean + * variables internally. This map is built up at static learning + * time for top-level asserted expressions of the shape "x = 0 OR x + * = 1". This substitution map is then applied in preprocess(). + * + * Note that expressions of the shape "x >= 0 AND x <= 1" are + * already substituted for PB versions at solve() time and won't + * appear here. + */ + SubstitutionMap d_pbSubstitutions; /** Counts the number of notifyRestart() calls to the theory. */ uint32_t d_restartsCounter; diff --git a/src/theory/booleans/theory_bool_type_rules.h b/src/theory/booleans/theory_bool_type_rules.h index 70b53a930..09030d331 100644 --- a/src/theory/booleans/theory_bool_type_rules.h +++ b/src/theory/booleans/theory_bool_type_rules.h @@ -34,7 +34,10 @@ public: TNode::iterator child_it = n.begin(); TNode::iterator child_it_end = n.end(); for(; child_it != child_it_end; ++child_it) { - if((*child_it).getType(check) != booleanType) { + if(!(*child_it).getType(check).isBoolean()) { + Debug("pb") << "failed type checking: " << *child_it << std::endl; + Debug("pb") << " integer: " << (*child_it).getType(check).isInteger() << std::endl; + Debug("pb") << " real: " << (*child_it).getType(check).isReal() << std::endl; throw TypeCheckingExceptionPrivate(n, "expecting a Boolean subexpression"); } } diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index f343848d8..3bfb7fdc5 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -90,7 +90,7 @@ class EqualityTypeRule { throw TypeCheckingExceptionPrivate(n, ss.str()); } - if ( lhsType == booleanType ) { + if ( lhsType == booleanType && rhsType == booleanType ) { throw TypeCheckingExceptionPrivate(n, "equality between two boolean terms (use IFF instead)"); } } diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index 44aed8b17..d82e628c1 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -92,7 +92,7 @@ public: * @param safe - whether it is safe to be interrupted */ virtual void lemma(TNode n, bool safe = false) - throw(Interrupted, AssertionException) = 0; + throw(Interrupted, TypeCheckingExceptionPrivate, AssertionException) = 0; /** * Request a split on a new theory atom. This is equivalent to diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp index 8657ed871..76551bc18 100644 --- a/src/theory/substitutions.cpp +++ b/src/theory/substitutions.cpp @@ -161,5 +161,5 @@ void SubstitutionMap::print(ostream& out) const { } } -} -} +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h index 513300a32..f59c17dc0 100644 --- a/src/theory/substitutions.h +++ b/src/theory/substitutions.h @@ -23,6 +23,7 @@ #include #include +#include #include "expr/node.h" namespace CVC4 { @@ -76,6 +77,25 @@ public: return const_cast(this)->apply(t); } + /** + * Clear out the accumulated substitutions, resetting this + * SubstitutionMap to the way it was when first constructed. + */ + void clear() { + d_substitutions.clear(); + d_substitutionCache.clear(); + d_cacheInvalidated = true; + } + + /** + * Swap the contents of this SubstitutionMap with those of another. + */ + void swap(SubstitutionMap& map) { + d_substitutions.swap(map.d_substitutions); + d_substitutionCache.swap(map.d_substitutionCache); + std::swap(d_cacheInvalidated, map.d_cacheInvalidated); + } + /** * Print to the output stream */ diff --git a/src/theory/theory.h b/src/theory/theory.h index d859c60d8..62a8cb4d6 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -442,8 +442,10 @@ public: } /** - * Given an atom of the theory, that comes from the input formula, this is method can rewrite the atom - * into an equivalent form. This is only called just before an input atom to the engine. + * Given an atom of the theory coming from the input formula, this + * method can be overridden in a theory implementation to rewrite + * the atom into an equivalent form. This is only called just + * before an input atom to the engine. */ virtual Node preprocess(TNode atom) { return atom; } diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 662a4925a..2107bcb66 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -149,7 +149,7 @@ class TheoryEngine { } void lemma(TNode node, bool removable = false) - throw(theory::Interrupted, AssertionException) { + throw(theory::Interrupted, TypeCheckingExceptionPrivate, AssertionException) { Trace("theory") << "EngineOutputChannel::lemma(" << node << ")" << std::endl; ++(d_engine->d_statistics.d_statLemma); diff --git a/src/util/Makefile.am b/src/util/Makefile.am index ce13f011d..61ff27c08 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -62,6 +62,8 @@ libutil_la_SOURCES = \ boolean_simplification.cpp \ ite_removal.h \ ite_removal.cpp \ + pseudoboolean.h \ + pseudoboolean.cpp \ node_visitor.h libutil_la_LIBADD = \ diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h index 8c3fc14e5..664027cdc 100644 --- a/src/util/integer_cln_imp.h +++ b/src/util/integer_cln_imp.h @@ -182,7 +182,8 @@ public: return *this; } - /** Raise this Integer to the power exp. + /** + * Raise this Integer to the power exp. * * @param exp the exponent */ @@ -197,6 +198,21 @@ public: } } + /** + * Return the greatest common divisor of this integer with another. + */ + Integer gcd(const Integer& y) const { + cln::cl_I result = cln::gcd(d_value, y.d_value); + return Integer(result); + } + + /** + * Return the absolute value of this integer. + */ + Integer abs() const { + return d_value >= 0 ? *this : -*this; + } + std::string toString(int base = 10) const{ std::stringstream ss; switch(base){ diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h index c1d46ca65..60cee3937 100644 --- a/src/util/integer_gmp_imp.h +++ b/src/util/integer_gmp_imp.h @@ -151,7 +151,8 @@ public: return *this; } - /** Raise this Integer to the power exp. + /** + * Raise this Integer to the power exp. * * @param exp the exponent */ @@ -161,6 +162,22 @@ public: return Integer( result ); } + /** + * Return the greatest common divisor of this integer with another. + */ + Integer gcd(const Integer& y) const { + mpz_class result; + mpz_gcd(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t()); + return Integer(result); + } + + /** + * Return the absolute value of this integer. + */ + Integer abs() const { + return d_value >= 0 ? *this : -*this; + } + std::string toString(int base = 10) const{ return d_value.get_str(base); } diff --git a/src/util/pseudoboolean.cpp b/src/util/pseudoboolean.cpp new file mode 100644 index 000000000..3fa7a774e --- /dev/null +++ b/src/util/pseudoboolean.cpp @@ -0,0 +1,49 @@ +/********************* */ +/*! \file pseudoboolean.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute &of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief A pseudoboolean constant + ** + ** A pseudoboolean constant. + **/ + +#include "util/pseudoboolean.h" + +namespace CVC4 { + +Pseudoboolean::Pseudoboolean(bool b) : + d_value(b) { +} + +Pseudoboolean::Pseudoboolean(int i) { + CheckArgument(i == 0 || i == 1, i); + d_value = (i == 1); +} + +Pseudoboolean::Pseudoboolean(const Integer& i) { + CheckArgument(i == 0 || i == 1, i); + d_value = (i == 1); +} + +Pseudoboolean::operator bool() const { + return d_value; +} + +Pseudoboolean::operator int() const { + return d_value ? 1 : 0; +} + +Pseudoboolean::operator Integer() const { + return d_value ? 1 : 0; +} + +}/* CVC4 namespace */ diff --git a/src/util/pseudoboolean.h b/src/util/pseudoboolean.h new file mode 100644 index 000000000..6d0d4fd26 --- /dev/null +++ b/src/util/pseudoboolean.h @@ -0,0 +1,54 @@ +/********************* */ +/*! \file pseudoboolean.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief A pseudoboolean constant + ** + ** A pseudoboolean constant. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__PSEUDOBOOLEAN_H +#define __CVC4__PSEUDOBOOLEAN_H + +#include "util/integer.h" + +namespace CVC4 { + +class Pseudoboolean { + bool d_value; + +public: + Pseudoboolean(bool b); + Pseudoboolean(int i); + Pseudoboolean(const Integer& i); + + operator bool() const; + operator int() const; + operator Integer() const; + +};/* class Pseudoboolean */ + +struct PseudobooleanHashStrategy { + static inline size_t hash(CVC4::Pseudoboolean pb) { + return int(pb); + } +};/* struct PseudobooleanHashStrategy */ + +inline std::ostream& operator<<(std::ostream& os, CVC4::Pseudoboolean pb) { + return os << int(pb); +} + +}/* CVC4 namespace */ + +#endif /* __CVC4__PSEUDOBOOLEAN_H */ diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h index c05d47175..b97484ff1 100644 --- a/src/util/rational_cln_imp.h +++ b/src/util/rational_cln_imp.h @@ -192,6 +192,14 @@ public: } } + Integer floor() const { + return Integer(cln::floor1(d_value)); + } + + Integer ceiling() const { + return Integer(cln::ceiling1(d_value)); + } + Rational& operator=(const Rational& x){ if(this == &x) return *this; d_value = x.d_value; @@ -226,9 +234,6 @@ public: return d_value >= y.d_value; } - - - Rational operator+(const Rational& y) const{ return Rational( d_value + y.d_value ); } diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h index 7af1b86df..167e0fc22 100644 --- a/src/util/rational_gmp_imp.h +++ b/src/util/rational_gmp_imp.h @@ -151,7 +151,7 @@ public: * Returns the value of denominator of the Rational. * Note that this makes a deep copy of the denominator. */ - Integer getDenominator() const{ + Integer getDenominator() const { return Integer(d_value.get_den()); } @@ -165,11 +165,22 @@ public: return mpq_cmp(d_value.get_mpq_t(), x.d_value.get_mpq_t()); } - int sgn() const { return mpq_sgn(d_value.get_mpq_t()); } + Integer floor() const { + mpz_class q; + mpz_fdiv_q(q.get_mpz_t(), d_value.get_num_mpz_t(), d_value.get_den_mpz_t()); + return Integer(q); + } + + Integer ceiling() const { + mpz_class q; + mpz_cdiv_q(q.get_mpz_t(), d_value.get_num_mpz_t(), d_value.get_den_mpz_t()); + return Integer(q); + } + Rational& operator=(const Rational& x){ if(this == &x) return *this; d_value = x.d_value; @@ -204,9 +215,6 @@ public: return d_value >= y.d_value; } - - - Rational operator+(const Rational& y) const{ return Rational( d_value + y.d_value ); } diff --git a/test/Makefile.am b/test/Makefile.am index 354b81470..a0d2e8049 100644 --- a/test/Makefile.am +++ b/test/Makefile.am @@ -26,7 +26,7 @@ test "X$(AM_COLOR_TESTS)" != Xno \ blu=''; \ std=''; \ } -subdirs_to_check = unit system regress/regress0 regress/regress0/arith regress/regress0/uf regress/regress0/bv regress/regress0/bv/core regress/regress0/arrays regress/regress0/datatypes regress/regress0/lemmas regress/regress0/push-pop regress/regress0/precedence regress/regress1 regress/regress2 regress/regress3 +subdirs_to_check = unit system regress/regress0 regress/regress0/arith regress/regress0/arith/integers regress/regress0/uf regress/regress0/bv regress/regress0/bv/core regress/regress0/arrays regress/regress0/datatypes regress/regress0/lemmas regress/regress0/push-pop regress/regress0/precedence regress/regress1 regress/regress2 regress/regress3 check-recursive: check-pre .PHONY: check-pre check-pre: diff --git a/test/regress/regress0/arith/Makefile b/test/regress/regress0/arith/Makefile new file mode 100644 index 000000000..6b570d785 --- /dev/null +++ b/test/regress/regress0/arith/Makefile @@ -0,0 +1,8 @@ +topdir = ../../../.. +srcdir = test/regress/regress0/arith + +include $(topdir)/Makefile.subdir + +# synonyms for "check" +.PHONY: test +test: check diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am index 700c59b8e..ceb57a8dc 100644 --- a/test/regress/regress0/arith/Makefile.am +++ b/test/regress/regress0/arith/Makefile.am @@ -1,4 +1,7 @@ +SUBDIRS = . integers + TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4 +MAKEFLAGS = -k # These are run for all build profiles. # If a test shouldn't be run in e.g. competition mode, diff --git a/test/regress/regress0/arith/integers/Makefile b/test/regress/regress0/arith/integers/Makefile new file mode 100644 index 000000000..4144299bd --- /dev/null +++ b/test/regress/regress0/arith/integers/Makefile @@ -0,0 +1,8 @@ +topdir = ../../../../.. +srcdir = test/regress/regress0/arith/integers + +include $(topdir)/Makefile.subdir + +# synonyms for "check" +.PHONY: test +test: check diff --git a/test/regress/regress0/arith/integers/Makefile.am b/test/regress/regress0/arith/integers/Makefile.am new file mode 100644 index 000000000..3d7f40c71 --- /dev/null +++ b/test/regress/regress0/arith/integers/Makefile.am @@ -0,0 +1,130 @@ +SUBDIRS = . + +TESTS_ENVIRONMENT = @srcdir@/../../../run_regression @top_builddir@/src/main/cvc4 +MAKEFLAGS = -k + +# These are run for all build profiles. +# If a test shouldn't be run in e.g. competition mode, +# put it below in "TESTS +=" +TESTS = \ + arith-int-001.cvc \ + arith-int-002.cvc \ + arith-int-003.cvc \ + arith-int-004.cvc \ + arith-int-005.cvc \ + arith-int-006.cvc \ + arith-int-007.cvc \ + arith-int-009.cvc \ + arith-int-010.cvc \ + arith-int-011.cvc \ + arith-int-014.cvc \ + arith-int-015.cvc \ + arith-int-016.cvc \ + arith-int-017.cvc \ + arith-int-018.cvc \ + arith-int-019.cvc \ + arith-int-020.cvc \ + arith-int-021.cvc \ + arith-int-023.cvc \ + arith-int-024.cvc \ + arith-int-025.cvc \ + arith-int-026.cvc \ + arith-int-027.cvc \ + arith-int-028.cvc \ + arith-int-029.cvc \ + arith-int-030.cvc \ + arith-int-031.cvc \ + arith-int-032.cvc \ + arith-int-033.cvc \ + arith-int-034.cvc \ + arith-int-035.cvc \ + arith-int-036.cvc \ + arith-int-037.cvc \ + arith-int-038.cvc \ + arith-int-039.cvc \ + arith-int-040.cvc \ + arith-int-041.cvc \ + arith-int-044.cvc \ + arith-int-045.cvc \ + arith-int-046.cvc \ + arith-int-048.cvc \ + arith-int-049.cvc \ + arith-int-051.cvc \ + arith-int-052.cvc \ + arith-int-053.cvc \ + arith-int-054.cvc \ + arith-int-055.cvc \ + arith-int-056.cvc \ + arith-int-057.cvc \ + arith-int-058.cvc \ + arith-int-059.cvc \ + arith-int-060.cvc \ + arith-int-061.cvc \ + arith-int-062.cvc \ + arith-int-063.cvc \ + arith-int-064.cvc \ + arith-int-065.cvc \ + arith-int-066.cvc \ + arith-int-067.cvc \ + arith-int-068.cvc \ + arith-int-069.cvc \ + arith-int-070.cvc \ + arith-int-071.cvc \ + arith-int-072.cvc \ + arith-int-073.cvc \ + arith-int-074.cvc \ + arith-int-075.cvc \ + arith-int-076.cvc \ + arith-int-077.cvc \ + arith-int-078.cvc \ + arith-int-079.cvc \ + arith-int-080.cvc \ + arith-int-081.cvc \ + arith-int-083.cvc \ + arith-int-085.cvc \ + arith-int-086.cvc \ + arith-int-087.cvc \ + arith-int-088.cvc \ + arith-int-089.cvc \ + arith-int-090.cvc \ + arith-int-091.cvc \ + arith-int-092.cvc \ + arith-int-093.cvc \ + arith-int-094.cvc \ + arith-int-095.cvc \ + arith-int-096.cvc \ + arith-int-099.cvc + +EXTRA_DIST = $(TESTS) \ + arith-int-008.cvc \ + arith-int-012.cvc \ + arith-int-013.cvc \ + arith-int-022.cvc \ + arith-int-042.cvc \ + arith-int-042.min.cvc \ + arith-int-043.cvc \ + arith-int-047.cvc \ + arith-int-050.cvc \ + arith-int-082.cvc \ + arith-int-084.cvc \ + arith-int-097.cvc \ + arith-int-098.cvc \ + arith-int-100.cvc + +#if CVC4_BUILD_PROFILE_COMPETITION +#else +#TESTS += \ +# error.cvc +#endif +# +# and make sure to distribute it +#EXTRA_DIST += \ +# error.cvc + +# synonyms for "check" in this directory +.PHONY: regress regress0 test +regress regress0 test: check + +# do nothing in this subdir +.PHONY: regress1 regress2 regress3 +regress1 regress2 regress3: diff --git a/test/regress/regress0/arith/integers/arith-int-001.cvc b/test/regress/regress0/arith/integers/arith-int-001.cvc new file mode 100644 index 000000000..8b559dc7f --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-001.cvc @@ -0,0 +1,15 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (-23 * x0) + (-23 * x1) + (5 * x2) + (-17 * x3) = 7 ; +ASSERT (-14 * x0) + (-14 * x1) + (19 * x2) + (-24 * x3) = 29 ; +ASSERT (-16 * x0) + (-17 * x1) + (8 * x2) + (4 * x3) > -10 ; +ASSERT (6 * x0) + (-10 * x1) + (-22 * x2) + (-22 * x3) >= 0 ; +ASSERT (18 * x0) + (0 * x1) + (27 * x2) + (7 * x3) <= -2 ; +ASSERT (-23 * x0) + (27 * x1) + (24 * x2) + (-23 * x3) > -25 ; +ASSERT (3 * x0) + (32 * x1) + (15 * x2) + (-21 * x3) >= -10 ; +ASSERT (-27 * x0) + (-16 * x1) + (21 * x2) + (-2 * x3) < 30 ; +ASSERT (-25 * x0) + (-18 * x1) + (-23 * x2) + (22 * x3) < -15 ; +ASSERT (-20 * x0) + (0 * x1) + (4 * x2) + (-26 * x3) >= 15 ; +ASSERT (-8 * x0) + (32 * x1) + (9 * x2) + (17 * x3) > -26; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-002.cvc b/test/regress/regress0/arith/integers/arith-int-002.cvc new file mode 100644 index 000000000..41113ea2f --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-002.cvc @@ -0,0 +1,15 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (17 * x0) + (-23 * x1) + (2 * x2) + (-19 * x3) = -18 ; +ASSERT (25 * x0) + (23 * x1) + (21 * x2) + (20 * x3) = 2 ; +ASSERT (-24 * x0) + (-30 * x1) + (-14 * x2) + (13 * x3) <= 15 ; +ASSERT (-26 * x0) + (7 * x1) + (8 * x2) + (14 * x3) <= 16 ; +ASSERT (-1 * x0) + (-3 * x1) + (-19 * x2) + (26 * x3) <= -15 ; +ASSERT (31 * x0) + (19 * x1) + (-19 * x2) + (24 * x3) < -25 ; +ASSERT (8 * x0) + (-27 * x1) + (22 * x2) + (-20 * x3) < -30 ; +ASSERT (25 * x0) + (7 * x1) + (-18 * x2) + (-18 * x3) >= -31 ; +ASSERT (7 * x0) + (-22 * x1) + (-8 * x2) + (-6 * x3) >= -17 ; +ASSERT (-23 * x0) + (14 * x1) + (23 * x2) + (22 * x3) > -29 ; +ASSERT (-6 * x0) + (-6 * x1) + (-19 * x2) + (-4 * x3) > -5; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-003.cvc b/test/regress/regress0/arith/integers/arith-int-003.cvc new file mode 100644 index 000000000..a76f82c56 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-003.cvc @@ -0,0 +1,15 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (17 * x0) + (-7 * x1) + (15 * x2) + (21 * x3) = 19 ; +ASSERT (6 * x0) + (-24 * x1) + (25 * x2) + (-18 * x3) > -25 ; +ASSERT (-26 * x0) + (-28 * x1) + (-23 * x2) + (0 * x3) < -14 ; +ASSERT (-12 * x0) + (16 * x1) + (26 * x2) + (-23 * x3) <= 11 ; +ASSERT (14 * x0) + (6 * x1) + (9 * x2) + (-29 * x3) > 24 ; +ASSERT (5 * x0) + (-10 * x1) + (21 * x2) + (-26 * x3) > -12 ; +ASSERT (31 * x0) + (6 * x1) + (30 * x2) + (10 * x3) <= -25 ; +ASSERT (-18 * x0) + (-25 * x1) + (-24 * x2) + (-30 * x3) >= -18 ; +ASSERT (29 * x0) + (25 * x1) + (29 * x2) + (-31 * x3) < 6 ; +ASSERT (21 * x0) + (-27 * x1) + (-28 * x2) + (-15 * x3) >= 25 ; +ASSERT (-13 * x0) + (10 * x1) + (-7 * x2) + (-10 * x3) <= -4; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-004.cvc b/test/regress/regress0/arith/integers/arith-int-004.cvc new file mode 100644 index 000000000..78d10d4b2 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-004.cvc @@ -0,0 +1,16 @@ +% EXPECT: invalid +% EXIT: 10 + +x0, x1, x2, x3 : INT; +ASSERT (12 * x0) + (-25 * x1) + (21 * x2) + (7 * x3) < 27 ; +ASSERT (9 * x0) + (2 * x1) + (26 * x2) + (-3 * x3) >= 11 ; +ASSERT (3 * x0) + (-29 * x1) + (-4 * x2) + (-17 * x3) > 2 ; +ASSERT (7 * x0) + (-29 * x1) + (12 * x2) + (16 * x3) >= -14 ; +ASSERT (21 * x0) + (32 * x1) + (16 * x2) + (4 * x3) >= -19 ; +ASSERT (6 * x0) + (23 * x1) + (-10 * x2) + (-25 * x3) > 5 ; +ASSERT (-26 * x0) + (4 * x1) + (-23 * x2) + (-30 * x3) >= 25 ; +ASSERT (-4 * x0) + (-13 * x1) + (15 * x2) + (-12 * x3) > -13 ; +ASSERT (-11 * x0) + (31 * x1) + (0 * x2) + (-2 * x3) < 8 ; +ASSERT (7 * x0) + (14 * x1) + (-21 * x2) + (-5 * x3) >= -19 ; +ASSERT (-28 * x0) + (-12 * x1) + (7 * x2) + (-5 * x3) <= 28; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-005.cvc b/test/regress/regress0/arith/integers/arith-int-005.cvc new file mode 100644 index 000000000..b2b1f9bf9 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-005.cvc @@ -0,0 +1,15 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (13 * x0) + (0 * x1) + (6 * x2) + (-30 * x3) = -16 ; +ASSERT (-4 * x0) + (-8 * x1) + (14 * x2) + (-8 * x3) = -11 ; +ASSERT (-23 * x0) + (-26 * x1) + (4 * x2) + (-6 * x3) <= -2 ; +ASSERT (-22 * x0) + (-18 * x1) + (-23 * x2) + (5 * x3) < -32 ; +ASSERT (27 * x0) + (-12 * x1) + (-19 * x2) + (-17 * x3) <= -29 ; +ASSERT (12 * x0) + (21 * x1) + (-22 * x2) + (15 * x3) > 4 ; +ASSERT (-15 * x0) + (16 * x1) + (2 * x2) + (-14 * x3) >= -26 ; +ASSERT (4 * x0) + (4 * x1) + (-21 * x2) + (10 * x3) >= -6 ; +ASSERT (-6 * x0) + (25 * x1) + (-14 * x2) + (8 * x3) >= -31 ; +ASSERT (-23 * x0) + (2 * x1) + (-9 * x2) + (19 * x3) <= 10 ; +ASSERT (21 * x0) + (24 * x1) + (14 * x2) + (-6 * x3) <= 0; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-006.cvc b/test/regress/regress0/arith/integers/arith-int-006.cvc new file mode 100644 index 000000000..cba51db21 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-006.cvc @@ -0,0 +1,11 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (-7 * x0) + (-28 * x1) + (8 * x2) + (29 * x3) = -18 ; +ASSERT (11 * x0) + (2 * x1) + (4 * x2) + (23 * x3) = 6 ; +ASSERT (24 * x0) + (-20 * x1) + (23 * x2) + (-2 * x3) = 19 ; +ASSERT (17 * x0) + (-6 * x1) + (2 * x2) + (-22 * x3) = -31 ; +ASSERT (16 * x0) + (-7 * x1) + (27 * x2) + (17 * x3) = -8; +ASSERT (-5 * x0) + (18 * x1) + (3 * x2) + (-1 * x3) <= 29 ; +ASSERT (9 * x0) + (29 * x1) + (30 * x2) + (23 * x3) >= 21 ; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-007.cvc b/test/regress/regress0/arith/integers/arith-int-007.cvc new file mode 100644 index 000000000..bc49f9688 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-007.cvc @@ -0,0 +1,11 @@ +% EXPECT: invalid +% EXIT: 10 +x0, x1, x2, x3 : INT; +ASSERT (-19 * x0) + (17 * x1) + (30 * x2) + (-31 * x3) <= -20 ; +ASSERT (-3 * x0) + (16 * x1) + (20 * x2) + (-25 * x3) < 28 ; +ASSERT (11 * x0) + (13 * x1) + (-15 * x2) + (-8 * x3) <= 18 ; +ASSERT (-21 * x0) + (0 * x1) + (32 * x2) + (7 * x3) > -31 ; +ASSERT (16 * x0) + (24 * x1) + (8 * x2) + (23 * x3) <= 16 ; +ASSERT (25 * x0) + (-11 * x1) + (-8 * x2) + (14 * x3) <= 17 ; +ASSERT (16 * x0) + (-25 * x1) + (-1 * x2) + (13 * x3) < -26; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-008.cvc b/test/regress/regress0/arith/integers/arith-int-008.cvc new file mode 100644 index 000000000..a524b86b0 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-008.cvc @@ -0,0 +1,11 @@ +% EXPECT: invalid +% EXIT: 10 +x0, x1, x2, x3 : INT; +ASSERT (-12 * x0) + (-15 * x1) + (-31 * x2) + (17 * x3) = -16 ; +ASSERT (11 * x0) + (-5 * x1) + (-8 * x2) + (-17 * x3) > -4 ; +ASSERT (-12 * x0) + (-22 * x1) + (9 * x2) + (-20 * x3) >= 32 ; +ASSERT (24 * x0) + (-32 * x1) + (5 * x2) + (31 * x3) > 20 ; +ASSERT (-30 * x0) + (-4 * x1) + (-4 * x2) + (0 * x3) >= -20 ; +ASSERT (-10 * x0) + (18 * x1) + (17 * x2) + (20 * x3) <= 30 ; +ASSERT (12 * x0) + (-13 * x1) + (4 * x2) + (-27 * x3) > 3; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-009.cvc b/test/regress/regress0/arith/integers/arith-int-009.cvc new file mode 100644 index 000000000..ccb522d37 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-009.cvc @@ -0,0 +1,11 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (-16 * x0) + (-21 * x1) + (32 * x2) + (32 * x3) = -19 ; +ASSERT (-10 * x0) + (-21 * x1) + (13 * x2) + (-7 * x3) = 2 ; +ASSERT (11 * x0) + (15 * x1) + (-8 * x2) + (-24 * x3) = 29 ; +ASSERT (3 * x0) + (-28 * x1) + (-14 * x2) + (-18 * x3) < 5 ; +ASSERT (-18 * x0) + (-13 * x1) + (25 * x2) + (22 * x3) <= -24 ; +ASSERT (-16 * x0) + (-17 * x1) + (-27 * x2) + (4 * x3) >= -5 ; +ASSERT (21 * x0) + (13 * x1) + (20 * x2) + (-1 * x3) < 19; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-010.cvc b/test/regress/regress0/arith/integers/arith-int-010.cvc new file mode 100644 index 000000000..832f4e63a --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-010.cvc @@ -0,0 +1,11 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (19 * x0) + (-2 * x1) + (-29 * x2) + (-24 * x3) = 3 ; +ASSERT (3 * x0) + (11 * x1) + (-14 * x2) + (6 * x3) = 4 ; +ASSERT (-1 * x0) + (-22 * x1) + (4 * x2) + (5 * x3) = -22; +ASSERT (8 * x0) + (-8 * x1) + (18 * x2) + (-14 * x3) < -20 ; +ASSERT (22 * x0) + (27 * x1) + (6 * x2) + (-3 * x3) <= -11 ; +ASSERT (-23 * x0) + (-29 * x1) + (-27 * x2) + (13 * x3) <= 3 ; +ASSERT (8 * x0) + (0 * x1) + (28 * x2) + (0 * x3) >= -29 ; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-011.cvc b/test/regress/regress0/arith/integers/arith-int-011.cvc new file mode 100644 index 000000000..d0cc2e501 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-011.cvc @@ -0,0 +1,6 @@ +% EXPECT: invalid +% EXIT: 10 +x0, x1, x2, x3 : INT; +ASSERT (13 * x0) + (-1 * x1) + (11 * x2) + (10 * x3) = 9 ; +ASSERT (-7 * x0) + (3 * x1) + (-22 * x2) + (16 * x3) >= 9; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-012.cvc b/test/regress/regress0/arith/integers/arith-int-012.cvc new file mode 100644 index 000000000..46127d24f --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-012.cvc @@ -0,0 +1,6 @@ +% EXPECT: invalid +% EXIT: 10 +x0, x1, x2, x3 : INT; +ASSERT (18 * x0) + (32 * x1) + (-11 * x2) + (18 * x3) < -25 ; +ASSERT (-31 * x0) + (16 * x1) + (24 * x2) + (9 * x3) >= -24; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-013.cvc b/test/regress/regress0/arith/integers/arith-int-013.cvc new file mode 100644 index 000000000..e018d7a15 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-013.cvc @@ -0,0 +1,6 @@ +% EXPECT: invalid +% EXIT: 10 +x0, x1, x2, x3 : INT; +ASSERT (-22 * x0) + (-14 * x1) + (4 * x2) + (-12 * x3) > 25 ; +ASSERT (14 * x0) + (11 * x1) + (32 * x2) + (-8 * x3) >= 2; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-014.cvc b/test/regress/regress0/arith/integers/arith-int-014.cvc new file mode 100644 index 000000000..75991b051 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-014.cvc @@ -0,0 +1,6 @@ +% EXPECT: invalid +% EXIT: 10 +x0, x1, x2, x3 : INT; +ASSERT (10 * x0) + (25 * x1) + (10 * x2) + (-28 * x3) <= 20 ; +ASSERT (24 * x0) + (-9 * x1) + (-12 * x2) + (15 * x3) <= 3; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-015.cvc b/test/regress/regress0/arith/integers/arith-int-015.cvc new file mode 100644 index 000000000..00ecbcde2 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-015.cvc @@ -0,0 +1,6 @@ +% EXPECT: invalid +% EXIT: 10 +x0, x1, x2, x3 : INT; +ASSERT (-22 * x0) + (-3 * x1) + (9 * x2) + (-13 * x3) > -31 ; +ASSERT (31 * x0) + (-17 * x1) + (28 * x2) + (-16 * x3) > -28; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-016.cvc b/test/regress/regress0/arith/integers/arith-int-016.cvc new file mode 100644 index 000000000..d01b6c51a --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-016.cvc @@ -0,0 +1,21 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (-13 * x0) + (-4 * x1) + (-20 * x2) + (-26 * x3) = 2 ; +ASSERT (13 * x0) + (13 * x1) + (-14 * x2) + (26 * x3) = -8 ; +ASSERT (-13 * x0) + (1 * x1) + (16 * x2) + (4 * x3) = -22 ; +ASSERT (17 * x0) + (7 * x1) + (32 * x2) + (19 * x3) = 16 ; +ASSERT (11 * x0) + (-8 * x1) + (-10 * x2) + (-10 * x3) <= -1 ; +ASSERT (-25 * x0) + (-18 * x1) + (-10 * x2) + (-19 * x3) <= 32 ; +ASSERT (0 * x0) + (-14 * x1) + (30 * x2) + (-5 * x3) > -13 ; +ASSERT (2 * x0) + (-17 * x1) + (-13 * x2) + (8 * x3) > 1 ; +ASSERT (-4 * x0) + (-1 * x1) + (29 * x2) + (-9 * x3) > -8 ; +ASSERT (-32 * x0) + (26 * x1) + (5 * x2) + (6 * x3) <= -1 ; +ASSERT (-26 * x0) + (3 * x1) + (22 * x2) + (27 * x3) > -2 ; +ASSERT (13 * x0) + (3 * x1) + (1 * x2) + (9 * x3) < 24 ; +ASSERT (-10 * x0) + (22 * x1) + (5 * x2) + (-5 * x3) >= -21 ; +ASSERT (-20 * x0) + (-28 * x1) + (-11 * x2) + (6 * x3) >= -17 ; +ASSERT (14 * x0) + (16 * x1) + (-15 * x2) + (17 * x3) < 27 ; +ASSERT (-23 * x0) + (-4 * x1) + (-19 * x2) + (-23 * x3) < 20 ; +ASSERT (-8 * x0) + (-5 * x1) + (-17 * x2) + (32 * x3) <= 20; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-017.cvc b/test/regress/regress0/arith/integers/arith-int-017.cvc new file mode 100644 index 000000000..2fee71829 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-017.cvc @@ -0,0 +1,21 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (23 * x0) + (-4 * x1) + (-26 * x2) + (-1 * x3) = 10 ; +ASSERT (15 * x0) + (31 * x1) + (31 * x2) + (31 * x3) = 13 ; +ASSERT (19 * x0) + (-15 * x1) + (25 * x2) + (30 * x3) = 23 ; +ASSERT (10 * x0) + (-17 * x1) + (15 * x2) + (13 * x3) < 22 ; +ASSERT (-7 * x0) + (22 * x1) + (8 * x2) + (24 * x3) < 14 ; +ASSERT (24 * x0) + (-12 * x1) + (0 * x2) + (-25 * x3) <= -19 ; +ASSERT (-27 * x0) + (17 * x1) + (-20 * x2) + (-25 * x3) >= 11 ; +ASSERT (3 * x0) + (-12 * x1) + (-18 * x2) + (15 * x3) > -27 ; +ASSERT (-19 * x0) + (24 * x1) + (9 * x2) + (4 * x3) <= 16 ; +ASSERT (28 * x0) + (-20 * x1) + (-21 * x2) + (4 * x3) > -13 ; +ASSERT (-21 * x0) + (-23 * x1) + (-31 * x2) + (-6 * x3) < 6 ; +ASSERT (-30 * x0) + (8 * x1) + (-22 * x2) + (8 * x3) > 14 ; +ASSERT (-1 * x0) + (17 * x1) + (-22 * x2) + (-4 * x3) >= 4 ; +ASSERT (2 * x0) + (-4 * x1) + (10 * x2) + (30 * x3) < -15 ; +ASSERT (29 * x0) + (27 * x1) + (23 * x2) + (-4 * x3) < 21 ; +ASSERT (-28 * x0) + (0 * x1) + (19 * x2) + (7 * x3) <= -18 ; +ASSERT (-20 * x0) + (-7 * x1) + (26 * x2) + (-17 * x3) < 23; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-018.cvc b/test/regress/regress0/arith/integers/arith-int-018.cvc new file mode 100644 index 000000000..c25f8e784 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-018.cvc @@ -0,0 +1,21 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (-11 * x0) + (-26 * x1) + (9 * x2) + (32 * x3) = -11 ; +ASSERT (-5 * x0) + (-11 * x1) + (-10 * x2) + (-31 * x3) = -23 ; +ASSERT (-12 * x0) + (9 * x1) + (-22 * x2) + (11 * x3) = 11 ; +ASSERT (-27 * x0) + (8 * x1) + (-28 * x2) + (-7 * x3) = 23 ; +ASSERT (19 * x0) + (4 * x1) + (5 * x2) + (-10 * x3) >= 2 ; +ASSERT (-6 * x0) + (-20 * x1) + (30 * x2) + (20 * x3) >= 12 ; +ASSERT (19 * x0) + (26 * x1) + (-21 * x2) + (18 * x3) <= -21 ; +ASSERT (8 * x0) + (-29 * x1) + (7 * x2) + (20 * x3) >= 29 ; +ASSERT (-28 * x0) + (6 * x1) + (11 * x2) + (0 * x3) >= -4 ; +ASSERT (-20 * x0) + (-30 * x1) + (17 * x2) + (25 * x3) >= 4 ; +ASSERT (-15 * x0) + (9 * x1) + (9 * x2) + (26 * x3) > 11 ; +ASSERT (-30 * x0) + (-20 * x1) + (-20 * x2) + (14 * x3) <= -27 ; +ASSERT (-22 * x0) + (-11 * x1) + (-6 * x2) + (18 * x3) > -13 ; +ASSERT (-22 * x0) + (-25 * x1) + (22 * x2) + (-24 * x3) <= 1 ; +ASSERT (-24 * x0) + (22 * x1) + (-28 * x2) + (-14 * x3) >= 18 ; +ASSERT (17 * x0) + (31 * x1) + (-13 * x2) + (-23 * x3) < -5 ; +ASSERT (-12 * x0) + (-28 * x1) + (19 * x2) + (-21 * x3) < -27; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-019.cvc b/test/regress/regress0/arith/integers/arith-int-019.cvc new file mode 100644 index 000000000..661eb288b --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-019.cvc @@ -0,0 +1,21 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (25 * x0) + (6 * x1) + (-30 * x2) + (29 * x3) = -5 ; +ASSERT (14 * x0) + (16 * x1) + (24 * x2) + (-7 * x3) <= 31 ; +ASSERT (1 * x0) + (20 * x1) + (14 * x2) + (5 * x3) >= 3 ; +ASSERT (-5 * x0) + (24 * x1) + (-21 * x2) + (-13 * x3) >= -12 ; +ASSERT (9 * x0) + (-16 * x1) + (23 * x2) + (-11 * x3) > -5 ; +ASSERT (-24 * x0) + (26 * x1) + (19 * x2) + (29 * x3) > -27 ; +ASSERT (-30 * x0) + (31 * x1) + (27 * x2) + (-26 * x3) < 23 ; +ASSERT (14 * x0) + (1 * x1) + (0 * x2) + (29 * x3) > 21 ; +ASSERT (-32 * x0) + (-5 * x1) + (27 * x2) + (31 * x3) <= 23 ; +ASSERT (30 * x0) + (10 * x1) + (30 * x2) + (29 * x3) < -28 ; +ASSERT (7 * x0) + (-4 * x1) + (-25 * x2) + (0 * x3) > -28 ; +ASSERT (3 * x0) + (-19 * x1) + (11 * x2) + (-21 * x3) <= 10 ; +ASSERT (-31 * x0) + (21 * x1) + (24 * x2) + (-17 * x3) >= 21 ; +ASSERT (-20 * x0) + (19 * x1) + (6 * x2) + (5 * x3) >= -27 ; +ASSERT (-8 * x0) + (-27 * x1) + (0 * x2) + (13 * x3) >= 12 ; +ASSERT (-21 * x0) + (7 * x1) + (-26 * x2) + (19 * x3) < -10 ; +ASSERT (32 * x0) + (-26 * x1) + (-24 * x2) + (14 * x3) < 13; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-020.cvc b/test/regress/regress0/arith/integers/arith-int-020.cvc new file mode 100644 index 000000000..9c6bf3932 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-020.cvc @@ -0,0 +1,21 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (-32 * x0) + (31 * x1) + (-32 * x2) + (-21 * x3) = 5 ; +ASSERT (32 * x0) + (5 * x1) + (23 * x2) + (-16 * x3) = 8 ; +ASSERT (-17 * x0) + (-17 * x1) + (-22 * x2) + (30 * x3) = -5 ; +ASSERT (30 * x0) + (18 * x1) + (26 * x2) + (6 * x3) = -8 ; +ASSERT (17 * x0) + (-4 * x1) + (-16 * x2) + (-22 * x3) = 11; +ASSERT (0 * x0) + (-26 * x1) + (-15 * x2) + (12 * x3) > 7 ; +ASSERT (-30 * x0) + (4 * x1) + (-1 * x2) + (27 * x3) > 11 ; +ASSERT (23 * x0) + (12 * x1) + (11 * x2) + (-2 * x3) <= -10 ; +ASSERT (-26 * x0) + (-8 * x1) + (7 * x2) + (-18 * x3) > 1 ; +ASSERT (3 * x0) + (0 * x1) + (5 * x2) + (24 * x3) > 2 ; +ASSERT (-13 * x0) + (15 * x1) + (2 * x2) + (2 * x3) <= 17 ; +ASSERT (-24 * x0) + (21 * x1) + (-21 * x2) + (-13 * x3) >= -30 ; +ASSERT (7 * x0) + (-11 * x1) + (2 * x2) + (21 * x3) >= -24 ; +ASSERT (-15 * x0) + (-1 * x1) + (6 * x2) + (-10 * x3) <= -25 ; +ASSERT (-21 * x0) + (8 * x1) + (3 * x2) + (-5 * x3) <= 22 ; +ASSERT (-18 * x0) + (-16 * x1) + (21 * x2) + (20 * x3) >= 9 ; +ASSERT (-17 * x0) + (-10 * x1) + (-20 * x2) + (16 * x3) >= 3 ; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-021.cvc b/test/regress/regress0/arith/integers/arith-int-021.cvc new file mode 100644 index 000000000..bfcf022f5 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-021.cvc @@ -0,0 +1,5 @@ +% EXPECT: invalid +% EXIT: 10 +x0, x1, x2, x3 : INT; +ASSERT (8 * x0) + (-27 * x1) + (29 * x2) + (-13 * x3) < 12; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-022.cvc b/test/regress/regress0/arith/integers/arith-int-022.cvc new file mode 100644 index 000000000..4a439cdb1 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-022.cvc @@ -0,0 +1,5 @@ +% EXPECT: invalid +% EXIT: 10 +x0, x1, x2, x3 : INT; +ASSERT (-24 * x0) + (25 * x1) + (-28 * x2) + (31 * x3) > 18; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-023.cvc b/test/regress/regress0/arith/integers/arith-int-023.cvc new file mode 100644 index 000000000..fa161b2d9 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-023.cvc @@ -0,0 +1,5 @@ +% EXPECT: invalid +% EXIT: 10 +x0, x1, x2, x3 : INT; +ASSERT (29 * x0) + (-19 * x1) + (23 * x2) + (15 * x3) <= 9; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-024.cvc b/test/regress/regress0/arith/integers/arith-int-024.cvc new file mode 100644 index 000000000..c4af43db4 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-024.cvc @@ -0,0 +1,5 @@ +% EXPECT: invalid +% EXIT: 10 +x0, x1, x2, x3 : INT; +ASSERT (4 * x0) + (8 * x1) + (27 * x2) + (-12 * x3) = -5; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-025.cvc b/test/regress/regress0/arith/integers/arith-int-025.cvc new file mode 100644 index 000000000..8d527322d --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-025.cvc @@ -0,0 +1,5 @@ +% EXPECT: invalid +% EXIT: 10 +x0, x1, x2, x3 : INT; +ASSERT (-19 * x0) + (-29 * x1) + (2 * x2) + (26 * x3) >= 3; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-026.cvc b/test/regress/regress0/arith/integers/arith-int-026.cvc new file mode 100644 index 000000000..b08a4e852 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-026.cvc @@ -0,0 +1,22 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (22 * x0) + (25 * x1) + (1 * x2) + (-11 * x3) = 19 ; +ASSERT (-10 * x0) + (-27 * x1) + (6 * x2) + (6 * x3) = 28 ; +ASSERT (0 * x0) + (-30 * x1) + (-31 * x2) + (12 * x3) = -21 ; +ASSERT (29 * x0) + (-6 * x1) + (-12 * x2) + (22 * x3) = -13; +ASSERT (-7 * x0) + (23 * x1) + (-1 * x2) + (-14 * x3) > -6 ; +ASSERT (-27 * x0) + (-31 * x1) + (25 * x2) + (-23 * x3) <= 12 ; +ASSERT (-19 * x0) + (6 * x1) + (0 * x2) + (-28 * x3) > -1 ; +ASSERT (-12 * x0) + (19 * x1) + (2 * x2) + (-4 * x3) <= 12 ; +ASSERT (10 * x0) + (-26 * x1) + (7 * x2) + (-6 * x3) < 12 ; +ASSERT (25 * x0) + (-18 * x1) + (-30 * x2) + (-9 * x3) < -2 ; +ASSERT (-9 * x0) + (-13 * x1) + (-9 * x2) + (-28 * x3) > 18 ; +ASSERT (-12 * x0) + (-28 * x1) + (-21 * x2) + (32 * x3) > 18 ; +ASSERT (-23 * x0) + (-26 * x1) + (-21 * x2) + (-24 * x3) <= 3 ; +ASSERT (-15 * x0) + (13 * x1) + (-4 * x2) + (-1 * x3) <= 0 ; +ASSERT (11 * x0) + (-30 * x1) + (3 * x2) + (-6 * x3) >= 3 ; +ASSERT (28 * x0) + (0 * x1) + (0 * x2) + (-22 * x3) >= 9 ; +ASSERT (-18 * x0) + (15 * x1) + (-27 * x2) + (31 * x3) < 5 ; +ASSERT (10 * x0) + (30 * x1) + (-28 * x2) + (27 * x3) <= -1 ; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-027.cvc b/test/regress/regress0/arith/integers/arith-int-027.cvc new file mode 100644 index 000000000..811726726 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-027.cvc @@ -0,0 +1,22 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (17 * x0) + (29 * x1) + (-11 * x2) + (24 * x3) = 13 ; +ASSERT (16 * x0) + (-20 * x1) + (-5 * x2) + (12 * x3) = 13 ; +ASSERT (-12 * x0) + (-3 * x1) + (-19 * x2) + (4 * x3) = -21 ; +ASSERT (-3 * x0) + (10 * x1) + (-6 * x2) + (-31 * x3) = 21 ; +ASSERT (10 * x0) + (-14 * x1) + (-12 * x2) + (8 * x3) = 5 ; +ASSERT (-4 * x0) + (15 * x1) + (29 * x2) + (2 * x3) = -32 ; +ASSERT (-14 * x0) + (-12 * x1) + (16 * x2) + (-14 * x3) = -8 ; +ASSERT (-31 * x0) + (14 * x1) + (30 * x2) + (-19 * x3) < -20 ; +ASSERT (-5 * x0) + (9 * x1) + (11 * x2) + (-32 * x3) < 3 ; +ASSERT (27 * x0) + (-6 * x1) + (0 * x2) + (30 * x3) <= -20 ; +ASSERT (-15 * x0) + (-13 * x1) + (-21 * x2) + (-5 * x3) > -8 ; +ASSERT (19 * x0) + (31 * x1) + (-16 * x2) + (-8 * x3) > -15 ; +ASSERT (9 * x0) + (-9 * x1) + (-4 * x2) + (-16 * x3) < 21 ; +ASSERT (24 * x0) + (4 * x1) + (28 * x2) + (-14 * x3) >= -1 ; +ASSERT (5 * x0) + (23 * x1) + (-22 * x2) + (-28 * x3) >= -21 ; +ASSERT (-31 * x0) + (14 * x1) + (14 * x2) + (-9 * x3) > -32 ; +ASSERT (25 * x0) + (-18 * x1) + (21 * x2) + (-17 * x3) < -20 ; +ASSERT (1 * x0) + (-29 * x1) + (11 * x2) + (-24 * x3) >= -20; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-028.cvc b/test/regress/regress0/arith/integers/arith-int-028.cvc new file mode 100644 index 000000000..49562ad73 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-028.cvc @@ -0,0 +1,22 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (-31 * x0) + (-5 * x1) + (-28 * x2) + (16 * x3) = 10 ; +ASSERT (3 * x0) + (-20 * x1) + (-11 * x2) + (-2 * x3) = 25 ; +ASSERT (31 * x0) + (28 * x1) + (-20 * x2) + (15 * x3) = -30; +ASSERT (15 * x0) + (-16 * x1) + (29 * x2) + (-2 * x3) >= -6 ; +ASSERT (-29 * x0) + (-17 * x1) + (-7 * x2) + (11 * x3) < 26 ; +ASSERT (-4 * x0) + (14 * x1) + (-29 * x2) + (-7 * x3) >= 28 ; +ASSERT (-29 * x0) + (-25 * x1) + (9 * x2) + (-17 * x3) <= -25 ; +ASSERT (10 * x0) + (-25 * x1) + (28 * x2) + (8 * x3) > 6 ; +ASSERT (10 * x0) + (17 * x1) + (-1 * x2) + (21 * x3) > 24 ; +ASSERT (-19 * x0) + (-29 * x1) + (-26 * x2) + (-7 * x3) <= -11 ; +ASSERT (30 * x0) + (-7 * x1) + (-8 * x2) + (6 * x3) >= -32 ; +ASSERT (-3 * x0) + (24 * x1) + (30 * x2) + (-30 * x3) >= 19 ; +ASSERT (-9 * x0) + (5 * x1) + (17 * x2) + (-24 * x3) < -22 ; +ASSERT (11 * x0) + (-16 * x1) + (-1 * x2) + (26 * x3) >= 1 ; +ASSERT (-13 * x0) + (5 * x1) + (19 * x2) + (4 * x3) >= 27 ; +ASSERT (23 * x0) + (4 * x1) + (30 * x2) + (-28 * x3) > 13 ; +ASSERT (-8 * x0) + (-24 * x1) + (0 * x2) + (22 * x3) < -6 ; +ASSERT (-1 * x0) + (1 * x1) + (-30 * x2) + (12 * x3) >= -26 ; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-029.cvc b/test/regress/regress0/arith/integers/arith-int-029.cvc new file mode 100644 index 000000000..1e8687ec3 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-029.cvc @@ -0,0 +1,22 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (-29 * x0) + (-17 * x1) + (11 * x2) + (1 * x3) = -15 ; +ASSERT (-13 * x0) + (1 * x1) + (-6 * x2) + (-15 * x3) = 32 ; +ASSERT (-19 * x0) + (29 * x1) + (27 * x2) + (-8 * x3) = -4 ; +ASSERT (-28 * x0) + (-15 * x1) + (-20 * x2) + (-1 * x3) = -2 ; +ASSERT (-2 * x0) + (2 * x1) + (3 * x2) + (-4 * x3) = 16 ; +ASSERT (31 * x0) + (22 * x1) + (15 * x2) + (28 * x3) = -19 ; +ASSERT (-32 * x0) + (2 * x1) + (-8 * x2) + (6 * x3) <= -21 ; +ASSERT (-10 * x0) + (23 * x1) + (-9 * x2) + (-26 * x3) < -7 ; +ASSERT (-11 * x0) + (-13 * x1) + (-17 * x2) + (-19 * x3) >= -11 ; +ASSERT (20 * x0) + (11 * x1) + (-11 * x2) + (-7 * x3) <= 14 ; +ASSERT (17 * x0) + (0 * x1) + (-27 * x2) + (-32 * x3) > -1 ; +ASSERT (17 * x0) + (-7 * x1) + (18 * x2) + (-29 * x3) > -19 ; +ASSERT (12 * x0) + (-14 * x1) + (27 * x2) + (5 * x3) <= 23 ; +ASSERT (-2 * x0) + (-6 * x1) + (-6 * x2) + (19 * x3) < -5 ; +ASSERT (-3 * x0) + (-10 * x1) + (-30 * x2) + (18 * x3) >= -27 ; +ASSERT (-18 * x0) + (-25 * x1) + (3 * x2) + (2 * x3) < -25 ; +ASSERT (-19 * x0) + (16 * x1) + (-11 * x2) + (-26 * x3) >= -24 ; +ASSERT (-2 * x0) + (21 * x1) + (25 * x2) + (28 * x3) > 10; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-030.cvc b/test/regress/regress0/arith/integers/arith-int-030.cvc new file mode 100644 index 000000000..1ead5e5a4 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-030.cvc @@ -0,0 +1,22 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (-13 * x0) + (26 * x1) + (-11 * x2) + (17 * x3) = 17 ; +ASSERT (-15 * x0) + (2 * x1) + (-9 * x2) + (17 * x3) = -11 ; +ASSERT (8 * x0) + (-24 * x1) + (20 * x2) + (23 * x3) = -23 ; +ASSERT (-2 * x0) + (26 * x1) + (4 * x2) + (31 * x3) < 31 ; +ASSERT (23 * x0) + (14 * x1) + (-29 * x2) + (-11 * x3) > 14 ; +ASSERT (-19 * x0) + (-32 * x1) + (11 * x2) + (31 * x3) < -4 ; +ASSERT (3 * x0) + (13 * x1) + (-19 * x2) + (26 * x3) >= -20 ; +ASSERT (-6 * x0) + (4 * x1) + (-17 * x2) + (-31 * x3) <= 32 ; +ASSERT (-13 * x0) + (32 * x1) + (-18 * x2) + (7 * x3) < -27 ; +ASSERT (-19 * x0) + (6 * x1) + (-28 * x2) + (-15 * x3) >= 30 ; +ASSERT (30 * x0) + (-24 * x1) + (-10 * x2) + (-4 * x3) >= -9 ; +ASSERT (-4 * x0) + (4 * x1) + (-27 * x2) + (-17 * x3) < 12 ; +ASSERT (-21 * x0) + (13 * x1) + (31 * x2) + (4 * x3) >= -16 ; +ASSERT (-11 * x0) + (30 * x1) + (-20 * x2) + (21 * x3) <= 9 ; +ASSERT (-12 * x0) + (23 * x1) + (2 * x2) + (12 * x3) <= 18 ; +ASSERT (30 * x0) + (8 * x1) + (4 * x2) + (-5 * x3) <= -24 ; +ASSERT (12 * x0) + (22 * x1) + (9 * x2) + (30 * x3) >= -3 ; +ASSERT (10 * x0) + (15 * x1) + (25 * x2) + (-5 * x3) <= 4; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-031.cvc b/test/regress/regress0/arith/integers/arith-int-031.cvc new file mode 100644 index 000000000..3eac975fe --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-031.cvc @@ -0,0 +1,20 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (-21 * x0) + (-24 * x1) + (-31 * x2) + (12 * x3) = -10 ; +ASSERT (-4 * x0) + (22 * x1) + (9 * x2) + (17 * x3) > -20 ; +ASSERT (0 * x0) + (22 * x1) + (-11 * x2) + (-22 * x3) <= 26 ; +ASSERT (17 * x0) + (-11 * x1) + (32 * x2) + (8 * x3) < 20 ; +ASSERT (-30 * x0) + (24 * x1) + (-30 * x2) + (-12 * x3) >= 19 ; +ASSERT (-27 * x0) + (5 * x1) + (31 * x2) + (-12 * x3) <= -24 ; +ASSERT (-12 * x0) + (-23 * x1) + (-27 * x2) + (29 * x3) >= 13 ; +ASSERT (23 * x0) + (-21 * x1) + (24 * x2) + (-17 * x3) >= -20 ; +ASSERT (-30 * x0) + (-27 * x1) + (-21 * x2) + (-11 * x3) < -24 ; +ASSERT (31 * x0) + (-14 * x1) + (-3 * x2) + (-9 * x3) >= 13 ; +ASSERT (8 * x0) + (-2 * x1) + (-13 * x2) + (23 * x3) < 31 ; +ASSERT (-1 * x0) + (9 * x1) + (-29 * x2) + (17 * x3) >= -7 ; +ASSERT (11 * x0) + (-8 * x1) + (-29 * x2) + (-25 * x3) >= -5 ; +ASSERT (19 * x0) + (-32 * x1) + (27 * x2) + (17 * x3) > 17 ; +ASSERT (23 * x0) + (-1 * x1) + (-9 * x2) + (-12 * x3) < -25 ; +ASSERT (16 * x0) + (-22 * x1) + (3 * x2) + (30 * x3) >= 11; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-032.cvc b/test/regress/regress0/arith/integers/arith-int-032.cvc new file mode 100644 index 000000000..0128c4dbd --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-032.cvc @@ -0,0 +1,20 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (4 * x0) + (-29 * x1) + (-9 * x2) + (9 * x3) = 8 ; +ASSERT (-26 * x0) + (-26 * x1) + (26 * x2) + (-18 * x3) = -20 ; +ASSERT (-15 * x0) + (-4 * x1) + (-28 * x2) + (-25 * x3) = 13 ; +ASSERT (17 * x0) + (-29 * x1) + (19 * x2) + (-32 * x3) = 26 ; +ASSERT (20 * x0) + (-29 * x1) + (-32 * x2) + (28 * x3) = -12 ; +ASSERT (17 * x0) + (18 * x1) + (-18 * x2) + (28 * x3) <= 21 ; +ASSERT (-28 * x0) + (-17 * x1) + (-15 * x2) + (30 * x3) > -19 ; +ASSERT (-6 * x0) + (-25 * x1) + (-22 * x2) + (-13 * x3) < -8 ; +ASSERT (12 * x0) + (8 * x1) + (15 * x2) + (-7 * x3) >= 12 ; +ASSERT (14 * x0) + (6 * x1) + (3 * x2) + (25 * x3) > 3 ; +ASSERT (31 * x0) + (5 * x1) + (26 * x2) + (-1 * x3) < -13 ; +ASSERT (31 * x0) + (-27 * x1) + (15 * x2) + (-16 * x3) >= 11 ; +ASSERT (20 * x0) + (-20 * x1) + (25 * x2) + (18 * x3) > 18 ; +ASSERT (-2 * x0) + (-30 * x1) + (25 * x2) + (-9 * x3) < -9 ; +ASSERT (29 * x0) + (-22 * x1) + (-18 * x2) + (-25 * x3) < -2 ; +ASSERT (-12 * x0) + (9 * x1) + (17 * x2) + (-16 * x3) > 3; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-033.cvc b/test/regress/regress0/arith/integers/arith-int-033.cvc new file mode 100644 index 000000000..9dda4dbf8 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-033.cvc @@ -0,0 +1,20 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (-14 * x0) + (16 * x1) + (-16 * x2) + (0 * x3) = -8 ; +ASSERT (3 * x0) + (-20 * x1) + (-12 * x2) + (-3 * x3) = -7 ; +ASSERT (-28 * x0) + (31 * x1) + (32 * x2) + (-11 * x3) = 0 ; +ASSERT (-20 * x0) + (-11 * x1) + (-27 * x2) + (-6 * x3) = -6 ; +ASSERT (-7 * x0) + (-7 * x1) + (17 * x2) + (-25 * x3) <= -15 ; +ASSERT (8 * x0) + (28 * x1) + (8 * x2) + (7 * x3) > -28 ; +ASSERT (25 * x0) + (7 * x1) + (-17 * x2) + (-28 * x3) > 5 ; +ASSERT (-19 * x0) + (0 * x1) + (-20 * x2) + (0 * x3) <= 20 ; +ASSERT (6 * x0) + (2 * x1) + (29 * x2) + (-19 * x3) <= -3 ; +ASSERT (-9 * x0) + (-1 * x1) + (-18 * x2) + (32 * x3) > 11 ; +ASSERT (2 * x0) + (21 * x1) + (0 * x2) + (19 * x3) >= 13 ; +ASSERT (-26 * x0) + (-6 * x1) + (-23 * x2) + (-8 * x3) < -24 ; +ASSERT (-23 * x0) + (22 * x1) + (12 * x2) + (19 * x3) < -27 ; +ASSERT (-25 * x0) + (-31 * x1) + (28 * x2) + (14 * x3) < 14 ; +ASSERT (-29 * x0) + (1 * x1) + (26 * x2) + (-27 * x3) < -14 ; +ASSERT (23 * x0) + (26 * x1) + (-5 * x2) + (6 * x3) <= -19; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-034.cvc b/test/regress/regress0/arith/integers/arith-int-034.cvc new file mode 100644 index 000000000..b8f4dd5f8 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-034.cvc @@ -0,0 +1,20 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (-20 * x0) + (-5 * x1) + (30 * x2) + (-24 * x3) = 12 ; +ASSERT (24 * x0) + (27 * x1) + (18 * x2) + (-5 * x3) = -16 ; +ASSERT (14 * x0) + (11 * x1) + (17 * x2) + (12 * x3) = -5 ; +ASSERT (-29 * x0) + (-29 * x1) + (-16 * x2) + (14 * x3) = 10 ; +ASSERT (30 * x0) + (13 * x1) + (10 * x2) + (24 * x3) = 3 ; +ASSERT (-20 * x0) + (29 * x1) + (28 * x2) + (27 * x3) < -21 ; +ASSERT (-31 * x0) + (17 * x1) + (14 * x2) + (-14 * x3) <= 14 ; +ASSERT (-23 * x0) + (19 * x1) + (28 * x2) + (-2 * x3) > -28 ; +ASSERT (-23 * x0) + (23 * x1) + (19 * x2) + (25 * x3) > 13 ; +ASSERT (-32 * x0) + (8 * x1) + (-24 * x2) + (10 * x3) >= -5 ; +ASSERT (-30 * x0) + (1 * x1) + (-22 * x2) + (12 * x3) >= -30 ; +ASSERT (8 * x0) + (28 * x1) + (17 * x2) + (-7 * x3) < -20 ; +ASSERT (-28 * x0) + (-8 * x1) + (27 * x2) + (25 * x3) >= 7 ; +ASSERT (-15 * x0) + (26 * x1) + (9 * x2) + (15 * x3) > -12 ; +ASSERT (-3 * x0) + (15 * x1) + (-6 * x2) + (-31 * x3) < -24 ; +ASSERT (-26 * x0) + (22 * x1) + (16 * x2) + (30 * x3) <= -2; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-035.cvc b/test/regress/regress0/arith/integers/arith-int-035.cvc new file mode 100644 index 000000000..6adae83fe --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-035.cvc @@ -0,0 +1,20 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (-3 * x0) + (2 * x1) + (17 * x2) + (-4 * x3) = -17 ; +ASSERT (5 * x0) + (-4 * x1) + (22 * x2) + (14 * x3) = -15 ; +ASSERT (8 * x0) + (23 * x1) + (26 * x2) + (-1 * x3) >= -6 ; +ASSERT (-7 * x0) + (4 * x1) + (9 * x2) + (-30 * x3) > -26 ; +ASSERT (-14 * x0) + (-31 * x1) + (-18 * x2) + (-5 * x3) <= 6 ; +ASSERT (15 * x0) + (26 * x1) + (3 * x2) + (-24 * x3) >= 6 ; +ASSERT (13 * x0) + (0 * x1) + (25 * x2) + (-27 * x3) <= -13 ; +ASSERT (11 * x0) + (20 * x1) + (-28 * x2) + (8 * x3) < 0 ; +ASSERT (-10 * x0) + (13 * x1) + (20 * x2) + (19 * x3) >= 29 ; +ASSERT (12 * x0) + (-9 * x1) + (-16 * x2) + (26 * x3) >= -11 ; +ASSERT (-2 * x0) + (32 * x1) + (-6 * x2) + (21 * x3) > -31 ; +ASSERT (-1 * x0) + (-22 * x1) + (-22 * x2) + (-5 * x3) > 29 ; +ASSERT (-8 * x0) + (19 * x1) + (18 * x2) + (32 * x3) >= 12 ; +ASSERT (26 * x0) + (16 * x1) + (-25 * x2) + (29 * x3) < 29 ; +ASSERT (1 * x0) + (-18 * x1) + (11 * x2) + (-10 * x3) > 10 ; +ASSERT (-21 * x0) + (5 * x1) + (-2 * x2) + (-28 * x3) <= -5; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-036.cvc b/test/regress/regress0/arith/integers/arith-int-036.cvc new file mode 100644 index 000000000..94074b8e1 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-036.cvc @@ -0,0 +1,17 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (-9 * x0) + (-21 * x1) + (-25 * x2) + (-1 * x3) = -11 ; +ASSERT (31 * x0) + (-18 * x1) + (5 * x2) + (-11 * x3) = 10 ; +ASSERT (15 * x0) + (5 * x1) + (5 * x2) + (19 * x3) = -29 ; +ASSERT (-9 * x0) + (-23 * x1) + (7 * x2) + (-21 * x3) = 28 ; +ASSERT (-24 * x0) + (-22 * x1) + (30 * x2) + (-31 * x3) = -24 ; +ASSERT (-29 * x0) + (-21 * x1) + (26 * x2) + (-13 * x3) < -12 ; +ASSERT (31 * x0) + (6 * x1) + (-23 * x2) + (30 * x3) < -3 ; +ASSERT (21 * x0) + (-7 * x1) + (-4 * x2) + (-25 * x3) <= -17 ; +ASSERT (4 * x0) + (24 * x1) + (21 * x2) + (8 * x3) <= 19 ; +ASSERT (19 * x0) + (30 * x1) + (14 * x2) + (-23 * x3) > 21 ; +ASSERT (30 * x0) + (3 * x1) + (-28 * x2) + (25 * x3) <= -27 ; +ASSERT (0 * x0) + (-17 * x1) + (-9 * x2) + (-8 * x3) <= 31 ; +ASSERT (-6 * x0) + (-23 * x1) + (21 * x2) + (18 * x3) >= 31; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-037.cvc b/test/regress/regress0/arith/integers/arith-int-037.cvc new file mode 100644 index 000000000..5ad2acd37 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-037.cvc @@ -0,0 +1,17 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (12 * x0) + (14 * x1) + (-22 * x2) + (-6 * x3) = 29 ; +ASSERT (-9 * x0) + (14 * x1) + (-23 * x2) + (-31 * x3) = 4 ; +ASSERT (-10 * x0) + (7 * x1) + (-23 * x2) + (18 * x3) <= -16 ; +ASSERT (-12 * x0) + (7 * x1) + (-16 * x2) + (16 * x3) > -31 ; +ASSERT (10 * x0) + (11 * x1) + (-17 * x2) + (19 * x3) <= 9 ; +ASSERT (-1 * x0) + (-8 * x1) + (-31 * x2) + (16 * x3) > 20 ; +ASSERT (-9 * x0) + (18 * x1) + (9 * x2) + (-14 * x3) <= -8 ; +ASSERT (-9 * x0) + (27 * x1) + (-22 * x2) + (-16 * x3) > 27 ; +ASSERT (-24 * x0) + (-25 * x1) + (-28 * x2) + (29 * x3) <= -9 ; +ASSERT (4 * x0) + (13 * x1) + (27 * x2) + (-5 * x3) >= -22 ; +ASSERT (-20 * x0) + (-14 * x1) + (21 * x2) + (-28 * x3) <= 17 ; +ASSERT (18 * x0) + (-32 * x1) + (-23 * x2) + (-9 * x3) <= -21 ; +ASSERT (19 * x0) + (-9 * x1) + (18 * x2) + (-9 * x3) <= -19; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-038.cvc b/test/regress/regress0/arith/integers/arith-int-038.cvc new file mode 100644 index 000000000..807ea029b --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-038.cvc @@ -0,0 +1,17 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (-24 * x0) + (25 * x1) + (28 * x2) + (-31 * x3) = -1 ; +ASSERT (29 * x0) + (17 * x1) + (-2 * x2) + (-6 * x3) <= 4 ; +ASSERT (-16 * x0) + (-4 * x1) + (-2 * x2) + (-1 * x3) >= -28 ; +ASSERT (4 * x0) + (-26 * x1) + (2 * x2) + (-8 * x3) > 7 ; +ASSERT (-17 * x0) + (-6 * x1) + (11 * x2) + (-9 * x3) > -27 ; +ASSERT (-25 * x0) + (13 * x1) + (-29 * x2) + (15 * x3) > 2 ; +ASSERT (32 * x0) + (-10 * x1) + (15 * x2) + (-25 * x3) < -25 ; +ASSERT (-16 * x0) + (-26 * x1) + (16 * x2) + (3 * x3) > -26 ; +ASSERT (-14 * x0) + (13 * x1) + (4 * x2) + (-24 * x3) >= -14 ; +ASSERT (-5 * x0) + (-21 * x1) + (-7 * x2) + (10 * x3) < 0 ; +ASSERT (0 * x0) + (25 * x1) + (31 * x2) + (30 * x3) <= -25 ; +ASSERT (-1 * x0) + (2 * x1) + (26 * x2) + (4 * x3) <= 4 ; +ASSERT (14 * x0) + (23 * x1) + (18 * x2) + (-18 * x3) > 19; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-039.cvc b/test/regress/regress0/arith/integers/arith-int-039.cvc new file mode 100644 index 000000000..3ee88fe80 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-039.cvc @@ -0,0 +1,17 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (22 * x0) + (21 * x1) + (-18 * x2) + (21 * x3) = 30 ; +ASSERT (-31 * x0) + (22 * x1) + (-20 * x2) + (18 * x3) = -32 ; +ASSERT (12 * x0) + (18 * x1) + (29 * x2) + (17 * x3) = 0 ; +ASSERT (-8 * x0) + (-10 * x1) + (-27 * x2) + (30 * x3) = 32 ; +ASSERT (-21 * x0) + (-2 * x1) + (20 * x2) + (-7 * x3) <= -27 ; +ASSERT (-7 * x0) + (-22 * x1) + (8 * x2) + (20 * x3) > -20 ; +ASSERT (-10 * x0) + (1 * x1) + (21 * x2) + (-6 * x3) > 10 ; +ASSERT (-21 * x0) + (-24 * x1) + (-15 * x2) + (4 * x3) <= 11 ; +ASSERT (-32 * x0) + (10 * x1) + (-21 * x2) + (-17 * x3) <= 5 ; +ASSERT (7 * x0) + (-19 * x1) + (28 * x2) + (27 * x3) <= 14 ; +ASSERT (-32 * x0) + (5 * x1) + (26 * x2) + (-23 * x3) < -23 ; +ASSERT (-28 * x0) + (5 * x1) + (22 * x2) + (25 * x3) < 6 ; +ASSERT (4 * x0) + (17 * x1) + (11 * x2) + (26 * x3) >= 20; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-040.cvc b/test/regress/regress0/arith/integers/arith-int-040.cvc new file mode 100644 index 000000000..5484f7dde --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-040.cvc @@ -0,0 +1,17 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (-1 * x0) + (-24 * x1) + (3 * x2) + (-8 * x3) > -5 ; +ASSERT (29 * x0) + (17 * x1) + (-26 * x2) + (20 * x3) > 11 ; +ASSERT (18 * x0) + (15 * x1) + (-27 * x2) + (8 * x3) > -11 ; +ASSERT (-14 * x0) + (4 * x1) + (27 * x2) + (-9 * x3) < -13 ; +ASSERT (24 * x0) + (11 * x1) + (17 * x2) + (-15 * x3) > 5 ; +ASSERT (-28 * x0) + (-1 * x1) + (10 * x2) + (-12 * x3) > -14 ; +ASSERT (-11 * x0) + (-4 * x1) + (7 * x2) + (-32 * x3) >= 31 ; +ASSERT (18 * x0) + (32 * x1) + (-24 * x2) + (-19 * x3) <= -6 ; +ASSERT (-15 * x0) + (23 * x1) + (-19 * x2) + (-12 * x3) < 2 ; +ASSERT (-21 * x0) + (-8 * x1) + (-30 * x2) + (31 * x3) >= -29 ; +ASSERT (5 * x0) + (-24 * x1) + (-21 * x2) + (-10 * x3) >= -8 ; +ASSERT (-31 * x0) + (-26 * x1) + (13 * x2) + (-7 * x3) <= -32 ; +ASSERT (-18 * x0) + (-11 * x1) + (9 * x2) + (6 * x3) >= 8; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-041.cvc b/test/regress/regress0/arith/integers/arith-int-041.cvc new file mode 100644 index 000000000..a3d8889b2 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-041.cvc @@ -0,0 +1,10 @@ +% EXPECT: invalid +% EXIT: 10 +x0, x1, x2, x3 : INT; +ASSERT (-31 * x0) + (8 * x1) + (16 * x2) + (5 * x3) >= 1 ; +ASSERT (-30 * x0) + (13 * x1) + (-17 * x2) + (13 * x3) < -24 ; +ASSERT (-16 * x0) + (-11 * x1) + (-32 * x2) + (-18 * x3) > -29 ; +ASSERT (32 * x0) + (-2 * x1) + (27 * x2) + (0 * x3) >= -1 ; +ASSERT (12 * x0) + (-17 * x1) + (21 * x2) + (-3 * x3) <= 1 ; +ASSERT (-26 * x0) + (29 * x1) + (-13 * x2) + (15 * x3) <= 2; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-042.cvc b/test/regress/regress0/arith/integers/arith-int-042.cvc new file mode 100644 index 000000000..df9314482 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-042.cvc @@ -0,0 +1,10 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (-9 * x0) + (25 * x1) + (0 * x2) + (13 * x3) = 17 ; +ASSERT (-6 * x0) + (32 * x1) + (2 * x2) + (-32 * x3) = -5 ; +ASSERT (19 * x0) + (25 * x1) + (-32 * x2) + (-29 * x3) <= 14 ; +ASSERT (6 * x0) + (22 * x1) + (-24 * x2) + (-6 * x3) < -21 ; +ASSERT (-18 * x0) + (-21 * x1) + (-29 * x2) + (12 * x3) > 17 ; +ASSERT (-25 * x0) + (-5 * x1) + (-22 * x2) + (-7 * x3) > -21; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-042.min.cvc b/test/regress/regress0/arith/integers/arith-int-042.min.cvc new file mode 100644 index 000000000..e19bdda0e --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-042.min.cvc @@ -0,0 +1,5 @@ +% EXPECT: valid +% EXIT: 20 +x1: INT; +x0: INT; +QUERY NOT (((x0 * 6) + (x1 * 32)) = 1); diff --git a/test/regress/regress0/arith/integers/arith-int-043.cvc b/test/regress/regress0/arith/integers/arith-int-043.cvc new file mode 100644 index 000000000..53f0e9903 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-043.cvc @@ -0,0 +1,10 @@ +% EXPECT: invalid +% EXIT: 10 +x0, x1, x2, x3 : INT; +ASSERT (-21 * x0) + (-23 * x1) + (29 * x2) + (-4 * x3) = 25 ; +ASSERT (20 * x0) + (-19 * x1) + (3 * x2) + (-1 * x3) <= -8 ; +ASSERT (2 * x0) + (-22 * x1) + (-30 * x2) + (-9 * x3) >= 17 ; +ASSERT (21 * x0) + (5 * x1) + (-13 * x2) + (0 * x3) <= 18 ; +ASSERT (9 * x0) + (-5 * x1) + (30 * x2) + (17 * x3) > -12 ; +ASSERT (-2 * x0) + (-27 * x1) + (-5 * x2) + (-23 * x3) < 24; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-044.cvc b/test/regress/regress0/arith/integers/arith-int-044.cvc new file mode 100644 index 000000000..b42affada --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-044.cvc @@ -0,0 +1,11 @@ +% EXPECT: valid +% EXIT: 20 +%%%% down from 24, up from 6, up from 39 +x0, x1, x2, x3 : INT; +ASSERT (-30 * x0) + (18 * x1) + (17 * x2) + (3 * x3) = 0; +ASSERT (-25 * x0) + (-16 * x1) + (17 * x2) + (26 * x3) < 23 ; +ASSERT (-27 * x0) + (9 * x1) + (7 * x2) + (-24 * x3) < -27 ; +ASSERT (14 * x0) + (-27 * x1) + (-10 * x2) + (16 * x3) >= -23 ; +ASSERT (14 * x0) + (-27 * x1) + (-3 * x2) + (2 * x3) > -9 ; +ASSERT (-19 * x0) + (-9 * x1) + (-3 * x2) + (29 * x3) <= 5 ; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-045.cvc b/test/regress/regress0/arith/integers/arith-int-045.cvc new file mode 100644 index 000000000..f70eff09a --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-045.cvc @@ -0,0 +1,10 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (-22 * x0) + (-5 * x1) + (-5 * x2) + (25 * x3) = 22 ; +ASSERT (2 * x0) + (-25 * x1) + (4 * x2) + (-21 * x3) >= 0 ; +ASSERT (30 * x0) + (6 * x1) + (-17 * x2) + (-6 * x3) > 8 ; +ASSERT (28 * x0) + (-17 * x1) + (26 * x2) + (-1 * x3) >= 17 ; +ASSERT (2 * x0) + (-32 * x1) + (30 * x2) + (10 * x3) < -23 ; +ASSERT (22 * x0) + (-18 * x1) + (7 * x2) + (28 * x3) < -26; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-046.cvc b/test/regress/regress0/arith/integers/arith-int-046.cvc new file mode 100644 index 000000000..ec694ad2b --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-046.cvc @@ -0,0 +1,7 @@ +% EXPECT: invalid +% EXIT: 10 +x0, x1, x2, x3 : INT; +ASSERT (2 * x0) + (-6 * x1) + (14 * x2) + (-24 * x3) > 4 ; +ASSERT (-13 * x0) + (-2 * x1) + (-9 * x2) + (-7 * x3) >= 29 ; +ASSERT (-11 * x0) + (28 * x1) + (-20 * x2) + (-2 * x3) >= 31; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-047.cvc b/test/regress/regress0/arith/integers/arith-int-047.cvc new file mode 100644 index 000000000..b5f4cb3a8 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-047.cvc @@ -0,0 +1,7 @@ +% EXPECT: invalid +% EXIT: 10 +x0, x1, x2, x3 : INT; +ASSERT (-14 * x0) + (27 * x1) + (10 * x2) + (1 * x3) = 10; +ASSERT (-29 * x0) + (-26 * x1) + (-16 * x2) + (17 * x3) >= 16 ; +ASSERT (-3 * x0) + (-2 * x1) + (26 * x2) + (30 * x3) < -27 ; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-048.cvc b/test/regress/regress0/arith/integers/arith-int-048.cvc new file mode 100644 index 000000000..76fa395bc --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-048.cvc @@ -0,0 +1,7 @@ +% EXPECT: invalid +% EXIT: 10 +x0, x1, x2, x3 : INT; +ASSERT (-13 * x0) + (-11 * x1) + (-14 * x2) + (21 * x3) = 6 ; +ASSERT (7 * x0) + (5 * x1) + (13 * x2) + (21 * x3) <= 27 ; +ASSERT (15 * x0) + (-11 * x1) + (-19 * x2) + (-13 * x3) < 5; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-049.cvc b/test/regress/regress0/arith/integers/arith-int-049.cvc new file mode 100644 index 000000000..b415776e8 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-049.cvc @@ -0,0 +1,7 @@ +% EXPECT: invalid +% EXIT: 10 +x0, x1, x2, x3 : INT; +ASSERT (-15 * x0) + (-20 * x1) + (-32 * x2) + (-16 * x3) = -19 ; +ASSERT (24 * x0) + (23 * x1) + (22 * x2) + (30 * x3) >= 19 ; +ASSERT (14 * x0) + (-6 * x1) + (28 * x2) + (-22 * x3) < -16; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-050.cvc b/test/regress/regress0/arith/integers/arith-int-050.cvc new file mode 100644 index 000000000..d35f445d8 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-050.cvc @@ -0,0 +1,7 @@ +% EXPECT: invalid +% EXIT: 10 +x0, x1, x2, x3 : INT; +ASSERT (-20 * x0) + (-19 * x1) + (6 * x2) + (32 * x3) > 16 ; +ASSERT (-1 * x0) + (-30 * x1) + (15 * x2) + (7 * x3) < -10 ; +ASSERT (-13 * x0) + (24 * x1) + (27 * x2) + (20 * x3) < -5; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-051.cvc b/test/regress/regress0/arith/integers/arith-int-051.cvc new file mode 100644 index 000000000..8a696d2de --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-051.cvc @@ -0,0 +1,13 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (-13 * x0) + (7 * x1) + (-3 * x2) + (9 * x3) = -3 ; +ASSERT (17 * x0) + (-22 * x1) + (-15 * x2) + (-21 * x3) >= 9 ; +ASSERT (-9 * x0) + (12 * x1) + (23 * x2) + (-24 * x3) >= -30 ; +ASSERT (-13 * x0) + (-3 * x1) + (-15 * x2) + (32 * x3) <= 26 ; +ASSERT (-27 * x0) + (9 * x1) + (-21 * x2) + (-5 * x3) < -9 ; +ASSERT (22 * x0) + (24 * x1) + (-10 * x2) + (-6 * x3) > -1 ; +ASSERT (20 * x0) + (-24 * x1) + (29 * x2) + (-21 * x3) <= 29 ; +ASSERT (25 * x0) + (11 * x1) + (8 * x2) + (-5 * x3) < -29 ; +ASSERT (-12 * x0) + (24 * x1) + (4 * x2) + (27 * x3) < 31; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-052.cvc b/test/regress/regress0/arith/integers/arith-int-052.cvc new file mode 100644 index 000000000..ae7e2c15f --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-052.cvc @@ -0,0 +1,13 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (-25 * x0) + (-23 * x1) + (11 * x2) + (10 * x3) = 7 ; +ASSERT (32 * x0) + (-15 * x1) + (-1 * x2) + (29 * x3) > -25 ; +ASSERT (29 * x0) + (-8 * x1) + (22 * x2) + (20 * x3) < 14 ; +ASSERT (31 * x0) + (-16 * x1) + (-17 * x2) + (-21 * x3) >= 32 ; +ASSERT (-24 * x0) + (-29 * x1) + (9 * x2) + (14 * x3) <= -4 ; +ASSERT (13 * x0) + (13 * x1) + (14 * x2) + (5 * x3) <= 25 ; +ASSERT (5 * x0) + (12 * x1) + (-5 * x2) + (-9 * x3) >= -28 ; +ASSERT (27 * x0) + (19 * x1) + (6 * x2) + (25 * x3) >= -12 ; +ASSERT (24 * x0) + (-26 * x1) + (2 * x2) + (0 * x3) >= -25; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-053.cvc b/test/regress/regress0/arith/integers/arith-int-053.cvc new file mode 100644 index 000000000..3cd2f3df6 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-053.cvc @@ -0,0 +1,13 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (-21 * x0) + (21 * x1) + (23 * x2) + (-20 * x3) = -8 ; +ASSERT (-31 * x0) + (-15 * x1) + (-23 * x2) + (29 * x3) = 17; +ASSERT (28 * x0) + (30 * x1) + (26 * x2) + (2 * x3) < 8 ; +ASSERT (17 * x0) + (-11 * x1) + (6 * x2) + (8 * x3) > 11 ; +ASSERT (20 * x0) + (-14 * x1) + (16 * x2) + (-3 * x3) < 9 ; +ASSERT (-11 * x0) + (2 * x1) + (4 * x2) + (-4 * x3) < -21 ; +ASSERT (25 * x0) + (6 * x1) + (-22 * x2) + (8 * x3) <= 7 ; +ASSERT (-8 * x0) + (9 * x1) + (-13 * x2) + (27 * x3) >= 0 ; +ASSERT (-16 * x0) + (-8 * x1) + (23 * x2) + (25 * x3) >= -13 ; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-054.cvc b/test/regress/regress0/arith/integers/arith-int-054.cvc new file mode 100644 index 000000000..95eb7a6d6 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-054.cvc @@ -0,0 +1,13 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (-31 * x0) + (-29 * x1) + (6 * x2) + (8 * x3) = -10 ; +ASSERT (0 * x0) + (8 * x1) + (-20 * x2) + (12 * x3) = 16 ; +ASSERT (19 * x0) + (-30 * x1) + (8 * x2) + (-4 * x3) = -17 ; +ASSERT (-10 * x0) + (26 * x1) + (11 * x2) + (-31 * x3) = -26; +ASSERT (-22 * x0) + (15 * x1) + (14 * x2) + (3 * x3) <= -3 ; +ASSERT (-15 * x0) + (7 * x1) + (29 * x2) + (16 * x3) >= -6 ; +ASSERT (-20 * x0) + (20 * x1) + (31 * x2) + (-24 * x3) <= 14 ; +ASSERT (2 * x0) + (31 * x1) + (15 * x2) + (-1 * x3) >= -6 ; +ASSERT (-30 * x0) + (-11 * x1) + (26 * x2) + (6 * x3) >= -30 ; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-055.cvc b/test/regress/regress0/arith/integers/arith-int-055.cvc new file mode 100644 index 000000000..6ed1bf4cd --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-055.cvc @@ -0,0 +1,13 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (-21 * x0) + (-4 * x1) + (-28 * x2) + (-7 * x3) = -23 ; +ASSERT (-7 * x0) + (-21 * x1) + (29 * x2) + (11 * x3) = 29 ; +ASSERT (-26 * x0) + (-7 * x1) + (-25 * x2) + (-19 * x3) < -4 ; +ASSERT (4 * x0) + (14 * x1) + (-16 * x2) + (-32 * x3) >= -16 ; +ASSERT (10 * x0) + (-9 * x1) + (20 * x2) + (-27 * x3) <= 31 ; +ASSERT (29 * x0) + (16 * x1) + (25 * x2) + (-1 * x3) < -26 ; +ASSERT (-29 * x0) + (1 * x1) + (11 * x2) + (32 * x3) < 12 ; +ASSERT (-4 * x0) + (-22 * x1) + (0 * x2) + (-29 * x3) < 31 ; +ASSERT (12 * x0) + (-8 * x1) + (-17 * x2) + (-8 * x3) > 8; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-056.cvc b/test/regress/regress0/arith/integers/arith-int-056.cvc new file mode 100644 index 000000000..028c1979b --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-056.cvc @@ -0,0 +1,16 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (-25 * x0) + (23 * x1) + (29 * x2) + (21 * x3) = -2 ; +ASSERT (1 * x0) + (10 * x1) + (-32 * x2) + (-17 * x3) = -2 ; +ASSERT (3 * x0) + (-32 * x1) + (-23 * x2) + (13 * x3) = 16 ; +ASSERT (25 * x0) + (-14 * x1) + (-17 * x2) + (16 * x3) <= 24 ; +ASSERT (1 * x0) + (-21 * x1) + (2 * x2) + (2 * x3) >= 15 ; +ASSERT (24 * x0) + (9 * x1) + (23 * x2) + (-2 * x3) >= -26 ; +%%ASSERT (-25 * x0) + (26 * x1) + (-3 * x2) + (-26 * x3) >= -20 ; +%%ASSERT (4 * x0) + (23 * x1) + (-24 * x2) + (7 * x3) <= -18 ; +%%ASSERT (-16 * x0) + (-24 * x1) + (26 * x2) + (1 * x3) > 15 ; +%%%%ASSERT (1 * x0) + (9 * x1) + (-18 * x2) + (11 * x3) > -3 ; +%%ASSERT (-9 * x0) + (20 * x1) + (15 * x2) + (4 * x3) < -17 ; +%%ASSERT (25 * x0) + (-22 * x1) + (-26 * x2) + (-21 * x3) > 17; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-057.cvc b/test/regress/regress0/arith/integers/arith-int-057.cvc new file mode 100644 index 000000000..1984622c3 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-057.cvc @@ -0,0 +1,16 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (-8 * x0) + (10 * x1) + (-25 * x2) + (-10 * x3) = -18 ; +ASSERT (27 * x0) + (5 * x1) + (8 * x2) + (13 * x3) = -8; +ASSERT (2 * x0) + (22 * x1) + (-13 * x2) + (16 * x3) <= 17 ; +ASSERT (18 * x0) + (18 * x1) + (15 * x2) + (-17 * x3) < -13 ; +ASSERT (-24 * x0) + (-8 * x1) + (31 * x2) + (-25 * x3) > 23 ; +ASSERT (-13 * x0) + (-22 * x1) + (11 * x2) + (28 * x3) >= -6 ; +ASSERT (20 * x0) + (-26 * x1) + (-20 * x2) + (-7 * x3) < -5 ; +ASSERT (-23 * x0) + (8 * x1) + (28 * x2) + (17 * x3) > 23 ; +ASSERT (32 * x0) + (31 * x1) + (-26 * x2) + (29 * x3) <= -1 ; +ASSERT (-2 * x0) + (-11 * x1) + (15 * x2) + (17 * x3) > -27 ; +ASSERT (-13 * x0) + (-30 * x1) + (-25 * x2) + (-18 * x3) <= 24 ; +ASSERT (23 * x0) + (-4 * x1) + (26 * x2) + (32 * x3) >= 23 ; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-058.cvc b/test/regress/regress0/arith/integers/arith-int-058.cvc new file mode 100644 index 000000000..c6c87c64b --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-058.cvc @@ -0,0 +1,16 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (-15 * x0) + (3 * x1) + (31 * x2) + (2 * x3) = -18 ; +ASSERT (-25 * x0) + (-10 * x1) + (15 * x2) + (29 * x3) = -18 ; +ASSERT (-17 * x0) + (31 * x1) + (-11 * x2) + (-29 * x3) = -2 ; +ASSERT (18 * x0) + (11 * x1) + (13 * x2) + (-16 * x3) >= 5 ; +ASSERT (-28 * x0) + (-30 * x1) + (13 * x2) + (-20 * x3) <= -19 ; +ASSERT (-10 * x0) + (-20 * x1) + (-13 * x2) + (-4 * x3) < 3 ; +ASSERT (-30 * x0) + (-5 * x1) + (-15 * x2) + (-1 * x3) > 19 ; +ASSERT (-8 * x0) + (28 * x1) + (17 * x2) + (23 * x3) <= 30 ; +ASSERT (-28 * x0) + (-16 * x1) + (-19 * x2) + (-23 * x3) >= 9 ; +ASSERT (-8 * x0) + (-15 * x1) + (-19 * x2) + (29 * x3) > -28 ; +ASSERT (-27 * x0) + (-12 * x1) + (-2 * x2) + (-29 * x3) >= -5 ; +ASSERT (32 * x0) + (-16 * x1) + (29 * x2) + (-12 * x3) < 26; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-059.cvc b/test/regress/regress0/arith/integers/arith-int-059.cvc new file mode 100644 index 000000000..558789493 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-059.cvc @@ -0,0 +1,16 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (31 * x0) + (-19 * x1) + (0 * x2) + (32 * x3) = -14 ; +ASSERT (12 * x0) + (-25 * x1) + (-32 * x2) + (-18 * x3) = 18 ; +ASSERT (-6 * x0) + (-21 * x1) + (-11 * x2) + (-10 * x3) = 11 ; +ASSERT (22 * x0) + (-7 * x1) + (2 * x2) + (-16 * x3) = 16; +ASSERT (15 * x0) + (-14 * x1) + (29 * x2) + (24 * x3) >= 14 ; +ASSERT (-26 * x0) + (-6 * x1) + (-13 * x2) + (25 * x3) < -4 ; +ASSERT (-24 * x0) + (-22 * x1) + (-21 * x2) + (-6 * x3) > -21 ; +ASSERT (17 * x0) + (-21 * x1) + (25 * x2) + (-13 * x3) >= 16 ; +ASSERT (14 * x0) + (-25 * x1) + (-22 * x2) + (18 * x3) >= -30 ; +ASSERT (-27 * x0) + (8 * x1) + (-12 * x2) + (26 * x3) >= 15 ; +ASSERT (-31 * x0) + (2 * x1) + (19 * x2) + (-11 * x3) >= -27 ; +ASSERT (32 * x0) + (-29 * x1) + (9 * x2) + (-4 * x3) < 3 ; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-060.cvc b/test/regress/regress0/arith/integers/arith-int-060.cvc new file mode 100644 index 000000000..75968a935 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-060.cvc @@ -0,0 +1,16 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (3 * x0) + (8 * x1) + (26 * x2) + (-17 * x3) = 31 ; +ASSERT (-14 * x0) + (25 * x1) + (4 * x2) + (-8 * x3) = 15 ; +ASSERT (-21 * x0) + (26 * x1) + (-10 * x2) + (-28 * x3) = 5; +ASSERT (2 * x0) + (-15 * x1) + (12 * x2) + (22 * x3) < -22 ; +ASSERT (10 * x0) + (24 * x1) + (11 * x2) + (-17 * x3) < 17 ; +ASSERT (26 * x0) + (32 * x1) + (-17 * x2) + (-3 * x3) >= 20 ; +ASSERT (11 * x0) + (26 * x1) + (-23 * x2) + (22 * x3) <= 32 ; +ASSERT (-19 * x0) + (22 * x1) + (-21 * x2) + (-28 * x3) <= -5 ; +ASSERT (-5 * x0) + (-18 * x1) + (10 * x2) + (-27 * x3) < -26 ; +ASSERT (21 * x0) + (-26 * x1) + (25 * x2) + (-13 * x3) < 15 ; +ASSERT (22 * x0) + (-2 * x1) + (3 * x2) + (-21 * x3) < 7 ; +ASSERT (20 * x0) + (-3 * x1) + (27 * x2) + (-21 * x3) < -18 ; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-061.cvc b/test/regress/regress0/arith/integers/arith-int-061.cvc new file mode 100644 index 000000000..68f54742c --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-061.cvc @@ -0,0 +1,24 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (16 * x0) + (20 * x1) + (-8 * x2) + (-27 * x3) = -2 ; +ASSERT (15 * x0) + (9 * x1) + (-1 * x2) + (4 * x3) = 1 ; +ASSERT (-25 * x0) + (19 * x1) + (-26 * x2) + (-20 * x3) = 22 ; +ASSERT (-11 * x0) + (28 * x1) + (-16 * x2) + (-15 * x3) = 15 ; +ASSERT (-11 * x0) + (-25 * x1) + (-16 * x2) + (25 * x3) = -3 ; +ASSERT (-15 * x0) + (-25 * x1) + (11 * x2) + (-24 * x3) = 29 ; +ASSERT (-12 * x0) + (-32 * x1) + (-28 * x2) + (-27 * x3) = -7 ; +ASSERT (16 * x0) + (5 * x1) + (10 * x2) + (-18 * x3) = 18 ; +ASSERT (-2 * x0) + (5 * x1) + (30 * x2) + (29 * x3) = -29 ; +ASSERT (-14 * x0) + (-20 * x1) + (21 * x2) + (1 * x3) = 31 ; +ASSERT (15 * x0) + (-7 * x1) + (-3 * x2) + (-24 * x3) > 3 ; +ASSERT (-16 * x0) + (-30 * x1) + (-31 * x2) + (16 * x3) > -9 ; +ASSERT (12 * x0) + (27 * x1) + (-11 * x2) + (-10 * x3) > -6 ; +ASSERT (0 * x0) + (29 * x1) + (32 * x2) + (9 * x3) <= -24 ; +ASSERT (11 * x0) + (-7 * x1) + (24 * x2) + (-30 * x3) >= 8 ; +ASSERT (1 * x0) + (25 * x1) + (29 * x2) + (15 * x3) <= -13 ; +ASSERT (-25 * x0) + (31 * x1) + (-32 * x2) + (-1 * x3) <= 9 ; +ASSERT (-22 * x0) + (-23 * x1) + (-4 * x2) + (-12 * x3) > 32 ; +ASSERT (22 * x0) + (-1 * x1) + (27 * x2) + (-22 * x3) > 20 ; +ASSERT (-20 * x0) + (-21 * x1) + (1 * x2) + (-32 * x3) >= 16; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-062.cvc b/test/regress/regress0/arith/integers/arith-int-062.cvc new file mode 100644 index 000000000..1c1c54b07 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-062.cvc @@ -0,0 +1,24 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (11 * x0) + (22 * x1) + (19 * x2) + (-8 * x3) = 12 ; +ASSERT (23 * x0) + (-6 * x1) + (-5 * x2) + (26 * x3) = 0 ; +ASSERT (1 * x0) + (-23 * x1) + (22 * x2) + (10 * x3) = -18 ; +ASSERT (-13 * x0) + (-17 * x1) + (-8 * x2) + (-16 * x3) = 16 ; +ASSERT (24 * x0) + (-4 * x1) + (-26 * x2) + (9 * x3) = -26 ; +ASSERT (24 * x0) + (23 * x1) + (17 * x2) + (-10 * x3) >= 5 ; +ASSERT (-12 * x0) + (-12 * x1) + (-13 * x2) + (-22 * x3) <= 9 ; +ASSERT (-7 * x0) + (17 * x1) + (-24 * x2) + (-8 * x3) <= -31 ; +ASSERT (-28 * x0) + (-10 * x1) + (3 * x2) + (-23 * x3) <= -19 ; +ASSERT (12 * x0) + (-16 * x1) + (27 * x2) + (-28 * x3) > -27 ; +ASSERT (-15 * x0) + (-24 * x1) + (12 * x2) + (21 * x3) < 21 ; +ASSERT (6 * x0) + (31 * x1) + (5 * x2) + (-5 * x3) >= 10 ; +ASSERT (-7 * x0) + (-20 * x1) + (-9 * x2) + (-32 * x3) >= 7 ; +ASSERT (3 * x0) + (24 * x1) + (-18 * x2) + (-9 * x3) < -30 ; +ASSERT (-14 * x0) + (22 * x1) + (22 * x2) + (-22 * x3) < -16 ; +ASSERT (1 * x0) + (4 * x1) + (10 * x2) + (28 * x3) > -31 ; +ASSERT (-14 * x0) + (-15 * x1) + (-8 * x2) + (2 * x3) >= 3 ; +ASSERT (13 * x0) + (-27 * x1) + (-14 * x2) + (28 * x3) < 28 ; +ASSERT (26 * x0) + (-12 * x1) + (-21 * x2) + (-16 * x3) < -26 ; +ASSERT (-6 * x0) + (-19 * x1) + (-8 * x2) + (18 * x3) >= 27; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-063.cvc b/test/regress/regress0/arith/integers/arith-int-063.cvc new file mode 100644 index 000000000..77843cbc3 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-063.cvc @@ -0,0 +1,24 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (20 * x0) + (-10 * x1) + (-10 * x2) + (26 * x3) = -9 ; +ASSERT (10 * x0) + (0 * x1) + (16 * x2) + (7 * x3) = 7 ; +ASSERT (6 * x0) + (-10 * x1) + (4 * x2) + (23 * x3) = 10; +ASSERT (-8 * x0) + (12 * x1) + (-19 * x2) + (-17 * x3) >= 21 ; +ASSERT (-20 * x0) + (6 * x1) + (-12 * x2) + (-31 * x3) > -31 ; +ASSERT (32 * x0) + (-6 * x1) + (-14 * x2) + (-32 * x3) >= 13 ; +ASSERT (29 * x0) + (12 * x1) + (17 * x2) + (9 * x3) > 32 ; +ASSERT (1 * x0) + (21 * x1) + (12 * x2) + (23 * x3) <= 14 ; +ASSERT (-12 * x0) + (-9 * x1) + (26 * x2) + (26 * x3) < 3 ; +ASSERT (-8 * x0) + (27 * x1) + (29 * x2) + (-10 * x3) >= 22 ; +ASSERT (-15 * x0) + (29 * x1) + (29 * x2) + (17 * x3) <= 22 ; +ASSERT (-4 * x0) + (0 * x1) + (1 * x2) + (-24 * x3) < -24 ; +ASSERT (25 * x0) + (17 * x1) + (31 * x2) + (-28 * x3) >= -12 ; +ASSERT (32 * x0) + (8 * x1) + (-3 * x2) + (19 * x3) > -19 ; +ASSERT (-27 * x0) + (-18 * x1) + (18 * x2) + (22 * x3) > 26 ; +ASSERT (29 * x0) + (29 * x1) + (4 * x2) + (-6 * x3) >= 8 ; +ASSERT (-12 * x0) + (17 * x1) + (-22 * x2) + (1 * x3) < 30 ; +ASSERT (-24 * x0) + (16 * x1) + (-26 * x2) + (-27 * x3) > 29 ; +ASSERT (9 * x0) + (15 * x1) + (-28 * x2) + (0 * x3) > -2 ; +ASSERT (-5 * x0) + (30 * x1) + (-21 * x2) + (-6 * x3) >= 12 ; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-064.cvc b/test/regress/regress0/arith/integers/arith-int-064.cvc new file mode 100644 index 000000000..0c6847c61 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-064.cvc @@ -0,0 +1,24 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (-8 * x0) + (-11 * x1) + (27 * x2) + (4 * x3) = 6 ; +ASSERT (32 * x0) + (27 * x1) + (31 * x2) + (-13 * x3) = 21 ; +ASSERT (-6 * x0) + (17 * x1) + (-20 * x2) + (11 * x3) < -5 ; +ASSERT (15 * x0) + (-15 * x1) + (-13 * x2) + (-21 * x3) < 27 ; +ASSERT (-24 * x0) + (-22 * x1) + (5 * x2) + (22 * x3) < 23 ; +ASSERT (27 * x0) + (23 * x1) + (-19 * x2) + (20 * x3) >= -8 ; +ASSERT (27 * x0) + (-27 * x1) + (23 * x2) + (17 * x3) < -5 ; +ASSERT (-11 * x0) + (-8 * x1) + (14 * x2) + (-10 * x3) <= 1 ; +ASSERT (12 * x0) + (7 * x1) + (-26 * x2) + (-28 * x3) >= -7 ; +ASSERT (25 * x0) + (-25 * x1) + (5 * x2) + (32 * x3) > -10 ; +ASSERT (-29 * x0) + (-24 * x1) + (26 * x2) + (-31 * x3) < -16 ; +ASSERT (10 * x0) + (29 * x1) + (9 * x2) + (23 * x3) < 13 ; +ASSERT (-26 * x0) + (6 * x1) + (-14 * x2) + (-21 * x3) > -15 ; +ASSERT (24 * x0) + (-14 * x1) + (-32 * x2) + (22 * x3) > -31 ; +ASSERT (-31 * x0) + (-16 * x1) + (-9 * x2) + (-32 * x3) > -19 ; +ASSERT (-1 * x0) + (17 * x1) + (26 * x2) + (-16 * x3) > -27 ; +ASSERT (10 * x0) + (-11 * x1) + (-20 * x2) + (-25 * x3) < -30 ; +ASSERT (-16 * x0) + (9 * x1) + (-10 * x2) + (-8 * x3) < -9 ; +ASSERT (19 * x0) + (10 * x1) + (18 * x2) + (7 * x3) < -30 ; +ASSERT (20 * x0) + (-25 * x1) + (-18 * x2) + (-2 * x3) <= -11; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-065.cvc b/test/regress/regress0/arith/integers/arith-int-065.cvc new file mode 100644 index 000000000..64fe7fd49 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-065.cvc @@ -0,0 +1,24 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (3 * x0) + (-21 * x1) + (-3 * x2) + (6 * x3) = -18 ; +ASSERT (-15 * x0) + (19 * x1) + (-21 * x2) + (-29 * x3) = -8 ; +ASSERT (32 * x0) + (-2 * x1) + (14 * x2) + (5 * x3) = -15 ; +ASSERT (-16 * x0) + (22 * x1) + (0 * x2) + (-26 * x3) >= 18 ; +ASSERT (11 * x0) + (-19 * x1) + (10 * x2) + (26 * x3) >= -20 ; +ASSERT (-25 * x0) + (-24 * x1) + (12 * x2) + (4 * x3) >= -14 ; +ASSERT (-20 * x0) + (-10 * x1) + (21 * x2) + (23 * x3) >= 28 ; +ASSERT (6 * x0) + (-31 * x1) + (11 * x2) + (-3 * x3) <= 4 ; +ASSERT (2 * x0) + (11 * x1) + (-13 * x2) + (-16 * x3) >= 23 ; +ASSERT (-6 * x0) + (-24 * x1) + (24 * x2) + (7 * x3) <= 14 ; +ASSERT (0 * x0) + (3 * x1) + (-14 * x2) + (-19 * x3) >= 15 ; +ASSERT (-31 * x0) + (-27 * x1) + (-32 * x2) + (-28 * x3) <= -15 ; +ASSERT (-11 * x0) + (3 * x1) + (-6 * x2) + (-5 * x3) < -31 ; +ASSERT (-2 * x0) + (-21 * x1) + (2 * x2) + (28 * x3) >= 7 ; +ASSERT (-12 * x0) + (19 * x1) + (-17 * x2) + (-14 * x3) > 11 ; +ASSERT (32 * x0) + (-29 * x1) + (-12 * x2) + (24 * x3) < -9 ; +ASSERT (-19 * x0) + (1 * x1) + (8 * x2) + (4 * x3) <= 3 ; +ASSERT (13 * x0) + (17 * x1) + (22 * x2) + (13 * x3) <= -25 ; +ASSERT (2 * x0) + (-4 * x1) + (-3 * x2) + (19 * x3) <= -12 ; +ASSERT (-16 * x0) + (-20 * x1) + (21 * x2) + (-30 * x3) <= 2; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-066.cvc b/test/regress/regress0/arith/integers/arith-int-066.cvc new file mode 100644 index 000000000..6c7035ded --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-066.cvc @@ -0,0 +1,18 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (28 * x0) + (-8 * x1) + (32 * x2) + (-3 * x3) = -18 ; +ASSERT (-4 * x0) + (5 * x1) + (-2 * x2) + (-17 * x3) > 19 ; +ASSERT (-9 * x0) + (14 * x1) + (-16 * x2) + (15 * x3) > 18 ; +ASSERT (-28 * x0) + (-25 * x1) + (-10 * x2) + (-10 * x3) < -10 ; +ASSERT (19 * x0) + (-4 * x1) + (11 * x2) + (22 * x3) <= -6 ; +ASSERT (2 * x0) + (32 * x1) + (-16 * x2) + (-29 * x3) > 6 ; +ASSERT (-7 * x0) + (9 * x1) + (-25 * x2) + (6 * x3) <= 5 ; +ASSERT (4 * x0) + (-18 * x1) + (-21 * x2) + (12 * x3) >= -32 ; +ASSERT (-27 * x0) + (11 * x1) + (-3 * x2) + (-6 * x3) < 1 ; +ASSERT (10 * x0) + (13 * x1) + (11 * x2) + (28 * x3) > -15 ; +ASSERT (-1 * x0) + (-4 * x1) + (30 * x2) + (6 * x3) > 9 ; +ASSERT (19 * x0) + (14 * x1) + (17 * x2) + (-8 * x3) <= -21 ; +ASSERT (-15 * x0) + (20 * x1) + (9 * x2) + (19 * x3) <= 4 ; +ASSERT (-9 * x0) + (-22 * x1) + (29 * x2) + (-6 * x3) <= 3; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-067.cvc b/test/regress/regress0/arith/integers/arith-int-067.cvc new file mode 100644 index 000000000..fc74cc94c --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-067.cvc @@ -0,0 +1,18 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (-25 * x0) + (-32 * x1) + (-29 * x2) + (-9 * x3) = -2 ; +ASSERT (22 * x0) + (10 * x1) + (-18 * x2) + (2 * x3) = -17 ; +ASSERT (22 * x0) + (6 * x1) + (-9 * x2) + (27 * x3) = 10 ; +ASSERT (1 * x0) + (-26 * x1) + (27 * x2) + (-19 * x3) = 29 ; +ASSERT (-13 * x0) + (18 * x1) + (5 * x2) + (22 * x3) < -10 ; +ASSERT (5 * x0) + (1 * x1) + (4 * x2) + (-7 * x3) > -12 ; +ASSERT (-30 * x0) + (-12 * x1) + (-22 * x2) + (-32 * x3) <= 1 ; +ASSERT (-15 * x0) + (19 * x1) + (22 * x2) + (-9 * x3) >= 12 ; +ASSERT (-6 * x0) + (-16 * x1) + (30 * x2) + (-13 * x3) <= -9 ; +ASSERT (-3 * x0) + (1 * x1) + (10 * x2) + (7 * x3) < -32 ; +ASSERT (5 * x0) + (-17 * x1) + (25 * x2) + (-31 * x3) >= -6 ; +ASSERT (18 * x0) + (28 * x1) + (-6 * x2) + (10 * x3) <= -31 ; +ASSERT (-11 * x0) + (-25 * x1) + (2 * x2) + (-3 * x3) > -3 ; +ASSERT (-14 * x0) + (-28 * x1) + (-2 * x2) + (20 * x3) < -25; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-068.cvc b/test/regress/regress0/arith/integers/arith-int-068.cvc new file mode 100644 index 000000000..d4360159f --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-068.cvc @@ -0,0 +1,18 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (-20 * x0) + (-8 * x1) + (5 * x2) + (-7 * x3) = -7 ; +ASSERT (-30 * x0) + (24 * x1) + (-4 * x2) + (-30 * x3) = 22 ; +ASSERT (31 * x0) + (-32 * x1) + (27 * x2) + (29 * x3) = 23 ; +ASSERT (8 * x0) + (-19 * x1) + (-7 * x2) + (0 * x3) <= -1 ; +ASSERT (-32 * x0) + (30 * x1) + (9 * x2) + (-21 * x3) <= 24 ; +ASSERT (15 * x0) + (-4 * x1) + (27 * x2) + (-26 * x3) >= 23 ; +ASSERT (7 * x0) + (26 * x1) + (-16 * x2) + (21 * x3) >= 16 ; +ASSERT (-24 * x0) + (-17 * x1) + (-9 * x2) + (27 * x3) <= 2 ; +ASSERT (29 * x0) + (-7 * x1) + (-8 * x2) + (32 * x3) <= -2 ; +ASSERT (32 * x0) + (31 * x1) + (7 * x2) + (-26 * x3) < 1 ; +ASSERT (-17 * x0) + (-13 * x1) + (-20 * x2) + (29 * x3) >= -21 ; +ASSERT (-32 * x0) + (27 * x1) + (-29 * x2) + (-11 * x3) >= -23 ; +ASSERT (29 * x0) + (-4 * x1) + (21 * x2) + (-16 * x3) < 23 ; +ASSERT (-15 * x0) + (26 * x1) + (14 * x2) + (13 * x3) <= -29; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-069.cvc b/test/regress/regress0/arith/integers/arith-int-069.cvc new file mode 100644 index 000000000..f877d3108 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-069.cvc @@ -0,0 +1,18 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (-12 * x0) + (20 * x1) + (2 * x2) + (-24 * x3) = 16 ; +ASSERT (-32 * x0) + (27 * x1) + (1 * x2) + (-3 * x3) = -3 ; +ASSERT (13 * x0) + (27 * x1) + (-17 * x2) + (25 * x3) <= -17 ; +ASSERT (27 * x0) + (-30 * x1) + (-16 * x2) + (-3 * x3) > -19 ; +ASSERT (-18 * x0) + (-25 * x1) + (-5 * x2) + (3 * x3) < -10 ; +ASSERT (9 * x0) + (-32 * x1) + (30 * x2) + (11 * x3) >= 23 ; +ASSERT (14 * x0) + (18 * x1) + (-21 * x2) + (-19 * x3) > 9 ; +ASSERT (28 * x0) + (2 * x1) + (23 * x2) + (17 * x3) < -6 ; +ASSERT (13 * x0) + (-17 * x1) + (-1 * x2) + (29 * x3) < -22 ; +ASSERT (-19 * x0) + (22 * x1) + (6 * x2) + (12 * x3) <= -9 ; +ASSERT (24 * x0) + (-14 * x1) + (31 * x2) + (12 * x3) > -26 ; +ASSERT (-1 * x0) + (24 * x1) + (-1 * x2) + (-31 * x3) > -21 ; +ASSERT (-22 * x0) + (28 * x1) + (-27 * x2) + (0 * x3) >= 3 ; +ASSERT (-28 * x0) + (29 * x1) + (-3 * x2) + (-22 * x3) >= -23; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-070.cvc b/test/regress/regress0/arith/integers/arith-int-070.cvc new file mode 100644 index 000000000..65e2fd6d8 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-070.cvc @@ -0,0 +1,18 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (0 * x0) + (-16 * x1) + (14 * x2) + (20 * x3) = 1 ; +ASSERT (-27 * x0) + (-5 * x1) + (-22 * x2) + (-24 * x3) = -7 ; +ASSERT (-3 * x0) + (-28 * x1) + (-15 * x2) + (7 * x3) = -9 ; +ASSERT (27 * x0) + (4 * x1) + (-31 * x2) + (-32 * x3) <= -12 ; +ASSERT (16 * x0) + (6 * x1) + (17 * x2) + (22 * x3) <= 5 ; +ASSERT (-27 * x0) + (-16 * x1) + (1 * x2) + (23 * x3) >= 9 ; +ASSERT (21 * x0) + (-28 * x1) + (-26 * x2) + (-26 * x3) <= -25 ; +ASSERT (-12 * x0) + (-32 * x1) + (-22 * x2) + (-20 * x3) > -32 ; +ASSERT (26 * x0) + (26 * x1) + (30 * x2) + (4 * x3) < 21 ; +ASSERT (-22 * x0) + (-21 * x1) + (0 * x2) + (30 * x3) < 13 ; +ASSERT (13 * x0) + (17 * x1) + (-7 * x2) + (-31 * x3) < 29 ; +ASSERT (-12 * x0) + (30 * x1) + (1 * x2) + (4 * x3) > -24 ; +ASSERT (-23 * x0) + (-2 * x1) + (29 * x2) + (11 * x3) > 26 ; +ASSERT (-18 * x0) + (-16 * x1) + (31 * x2) + (14 * x3) <= 32; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-071.cvc b/test/regress/regress0/arith/integers/arith-int-071.cvc new file mode 100644 index 000000000..e8b7a206c --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-071.cvc @@ -0,0 +1,19 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (22 * x0) + (3 * x1) + (-17 * x2) + (-21 * x3) = -9 ; +ASSERT (-12 * x0) + (-9 * x1) + (-9 * x2) + (-16 * x3) = -12 ; +ASSERT (-5 * x0) + (16 * x1) + (-15 * x2) + (-13 * x3) > 27 ; +ASSERT (16 * x0) + (-4 * x1) + (17 * x2) + (-24 * x3) > -9 ; +ASSERT (3 * x0) + (13 * x1) + (-15 * x2) + (-13 * x3) <= -32 ; +ASSERT (-18 * x0) + (21 * x1) + (-7 * x2) + (2 * x3) >= 13 ; +ASSERT (5 * x0) + (11 * x1) + (-11 * x2) + (-11 * x3) <= 9 ; +ASSERT (-9 * x0) + (8 * x1) + (-25 * x2) + (-14 * x3) >= 10 ; +ASSERT (17 * x0) + (-29 * x1) + (23 * x2) + (7 * x3) <= -31 ; +ASSERT (20 * x0) + (0 * x1) + (1 * x2) + (-6 * x3) <= 23 ; +ASSERT (-25 * x0) + (0 * x1) + (-32 * x2) + (17 * x3) > -14 ; +ASSERT (6 * x0) + (-30 * x1) + (-11 * x2) + (29 * x3) < 28 ; +ASSERT (-19 * x0) + (23 * x1) + (-19 * x2) + (3 * x3) >= 7 ; +ASSERT (29 * x0) + (21 * x1) + (-28 * x2) + (-28 * x3) < 22 ; +ASSERT (28 * x0) + (25 * x1) + (2 * x2) + (-23 * x3) <= -28; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-072.cvc b/test/regress/regress0/arith/integers/arith-int-072.cvc new file mode 100644 index 000000000..7670bb468 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-072.cvc @@ -0,0 +1,19 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (1 * x0) + (-1 * x1) + (-16 * x2) + (6 * x3) = -11 ; +ASSERT (-17 * x0) + (17 * x1) + (-15 * x2) + (24 * x3) = -21 ; +ASSERT (-31 * x0) + (28 * x1) + (-4 * x2) + (31 * x3) = -32 ; +ASSERT (1 * x0) + (-12 * x1) + (29 * x2) + (-6 * x3) = 25 ; +ASSERT (2 * x0) + (7 * x1) + (-24 * x2) + (28 * x3) >= -12 ; +ASSERT (-23 * x0) + (-22 * x1) + (14 * x2) + (-24 * x3) >= 22 ; +ASSERT (23 * x0) + (-21 * x1) + (22 * x2) + (26 * x3) >= -4 ; +ASSERT (25 * x0) + (27 * x1) + (14 * x2) + (5 * x3) <= 9 ; +ASSERT (16 * x0) + (2 * x1) + (24 * x2) + (-11 * x3) < -32 ; +ASSERT (0 * x0) + (23 * x1) + (29 * x2) + (-15 * x3) < -14 ; +ASSERT (5 * x0) + (-12 * x1) + (-7 * x2) + (29 * x3) <= -16 ; +ASSERT (25 * x0) + (26 * x1) + (14 * x2) + (-2 * x3) <= 13 ; +ASSERT (-30 * x0) + (19 * x1) + (24 * x2) + (7 * x3) < -23 ; +ASSERT (24 * x0) + (28 * x1) + (12 * x2) + (-25 * x3) >= -22 ; +ASSERT (27 * x0) + (-13 * x1) + (-16 * x2) + (-3 * x3) < 24; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-073.cvc b/test/regress/regress0/arith/integers/arith-int-073.cvc new file mode 100644 index 000000000..0b0f6b76c --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-073.cvc @@ -0,0 +1,19 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (8 * x0) + (-14 * x1) + (0 * x2) + (7 * x3) = 26 ; +ASSERT (-7 * x0) + (-14 * x1) + (15 * x2) + (31 * x3) = 8 ; +ASSERT (-4 * x0) + (16 * x1) + (3 * x2) + (-1 * x3) = 12 ; +ASSERT (2 * x0) + (24 * x1) + (-7 * x2) + (4 * x3) = 24 ; +ASSERT (26 * x0) + (-8 * x1) + (28 * x2) + (9 * x3) = -12 ; +ASSERT (19 * x0) + (-3 * x1) + (25 * x2) + (10 * x3) <= -19 ; +ASSERT (-13 * x0) + (-16 * x1) + (-14 * x2) + (8 * x3) <= 25 ; +ASSERT (-21 * x0) + (-2 * x1) + (-20 * x2) + (8 * x3) <= -22 ; +ASSERT (16 * x0) + (4 * x1) + (11 * x2) + (-15 * x3) >= -12 ; +ASSERT (-24 * x0) + (-8 * x1) + (2 * x2) + (-24 * x3) <= -22 ; +ASSERT (29 * x0) + (23 * x1) + (-20 * x2) + (8 * x3) > 21 ; +ASSERT (-24 * x0) + (-28 * x1) + (-23 * x2) + (-24 * x3) < -5 ; +ASSERT (-1 * x0) + (17 * x1) + (19 * x2) + (-7 * x3) > -5 ; +ASSERT (24 * x0) + (3 * x1) + (6 * x2) + (10 * x3) <= 15 ; +ASSERT (27 * x0) + (-11 * x1) + (-8 * x2) + (-22 * x3) > -30; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-074.cvc b/test/regress/regress0/arith/integers/arith-int-074.cvc new file mode 100644 index 000000000..1f6578d09 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-074.cvc @@ -0,0 +1,19 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (14 * x0) + (-6 * x1) + (-23 * x2) + (-8 * x3) = -18 ; +ASSERT (-11 * x0) + (12 * x1) + (8 * x2) + (-1 * x3) = -32 ; +ASSERT (24 * x0) + (-10 * x1) + (19 * x2) + (7 * x3) = -30 ; +ASSERT (1 * x0) + (-12 * x1) + (-13 * x2) + (-17 * x3) = -28 ; +ASSERT (-17 * x0) + (14 * x1) + (7 * x2) + (-18 * x3) = -14 ; +ASSERT (7 * x0) + (14 * x1) + (-22 * x2) + (29 * x3) = -6; +ASSERT (15 * x0) + (-6 * x1) + (3 * x2) + (-19 * x3) > 26 ; +ASSERT (-20 * x0) + (-18 * x1) + (-24 * x2) + (5 * x3) >= -1 ; +ASSERT (11 * x0) + (-26 * x1) + (-20 * x2) + (-16 * x3) > -7 ; +ASSERT (31 * x0) + (-2 * x1) + (6 * x2) + (32 * x3) > -22 ; +ASSERT (-25 * x0) + (26 * x1) + (-26 * x2) + (-21 * x3) >= -27 ; +ASSERT (-17 * x0) + (-30 * x1) + (14 * x2) + (17 * x3) <= -19 ; +ASSERT (-16 * x0) + (4 * x1) + (1 * x2) + (-24 * x3) <= -24 ; +ASSERT (-13 * x0) + (29 * x1) + (-27 * x2) + (12 * x3) < -15 ; +ASSERT (26 * x0) + (-2 * x1) + (-28 * x2) + (20 * x3) < -20 ; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-075.cvc b/test/regress/regress0/arith/integers/arith-int-075.cvc new file mode 100644 index 000000000..e6f136797 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-075.cvc @@ -0,0 +1,19 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (-8 * x0) + (29 * x1) + (15 * x2) + (32 * x3) = 32 ; +ASSERT (18 * x0) + (-8 * x1) + (18 * x2) + (22 * x3) = 20 ; +ASSERT (11 * x0) + (9 * x1) + (32 * x2) + (-15 * x3) > 21 ; +ASSERT (12 * x0) + (1 * x1) + (25 * x2) + (-17 * x3) > -13 ; +ASSERT (-20 * x0) + (7 * x1) + (13 * x2) + (-15 * x3) <= -3 ; +ASSERT (32 * x0) + (4 * x1) + (-30 * x2) + (13 * x3) <= -15 ; +ASSERT (-32 * x0) + (-27 * x1) + (20 * x2) + (22 * x3) <= -28 ; +ASSERT (28 * x0) + (23 * x1) + (10 * x2) + (20 * x3) < 9 ; +ASSERT (-30 * x0) + (-32 * x1) + (-28 * x2) + (-30 * x3) > 17 ; +ASSERT (-26 * x0) + (14 * x1) + (30 * x2) + (31 * x3) < 20 ; +ASSERT (21 * x0) + (23 * x1) + (-7 * x2) + (-16 * x3) > -19 ; +ASSERT (6 * x0) + (0 * x1) + (0 * x2) + (21 * x3) < -1 ; +ASSERT (13 * x0) + (29 * x1) + (17 * x2) + (-29 * x3) < -32 ; +ASSERT (22 * x0) + (-9 * x1) + (-25 * x2) + (11 * x3) > 29 ; +ASSERT (-25 * x0) + (-19 * x1) + (22 * x2) + (-27 * x3) >= 10; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-076.cvc b/test/regress/regress0/arith/integers/arith-int-076.cvc new file mode 100644 index 000000000..d0d2bbd59 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-076.cvc @@ -0,0 +1,12 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (-20 * x0) + (0 * x1) + (4 * x2) + (29 * x3) = -15 ; +ASSERT (3 * x0) + (19 * x1) + (21 * x2) + (-32 * x3) = 11 ; +ASSERT (-23 * x0) + (-8 * x1) + (-12 * x2) + (-14 * x3) >= -25 ; +ASSERT (13 * x0) + (30 * x1) + (-12 * x2) + (22 * x3) < -12 ; +ASSERT (-12 * x0) + (-17 * x1) + (20 * x2) + (14 * x3) > -26 ; +ASSERT (-13 * x0) + (-17 * x1) + (-25 * x2) + (27 * x3) <= -29 ; +ASSERT (-8 * x0) + (-31 * x1) + (-3 * x2) + (-22 * x3) > -22 ; +ASSERT (30 * x0) + (11 * x1) + (-32 * x2) + (32 * x3) >= 28; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-077.cvc b/test/regress/regress0/arith/integers/arith-int-077.cvc new file mode 100644 index 000000000..4f2985da8 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-077.cvc @@ -0,0 +1,12 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (26 * x0) + (-28 * x1) + (27 * x2) + (8 * x3) = 31 ; +ASSERT (-32 * x0) + (11 * x1) + (-5 * x2) + (14 * x3) = 2; +ASSERT (3 * x0) + (17 * x1) + (30 * x2) + (31 * x3) < 13 ; +ASSERT (-17 * x0) + (-21 * x1) + (10 * x2) + (8 * x3) > 23 ; +ASSERT (-14 * x0) + (10 * x1) + (11 * x2) + (27 * x3) > -13 ; +ASSERT (-14 * x0) + (24 * x1) + (3 * x2) + (-26 * x3) > 1 ; +ASSERT (-14 * x0) + (20 * x1) + (-2 * x2) + (-24 * x3) > -26 ; +ASSERT (20 * x0) + (-23 * x1) + (30 * x2) + (-30 * x3) < 24 ; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-078.cvc b/test/regress/regress0/arith/integers/arith-int-078.cvc new file mode 100644 index 000000000..d65638290 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-078.cvc @@ -0,0 +1,12 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (17 * x0) + (-14 * x1) + (13 * x2) + (13 * x3) = -18 ; +ASSERT (13 * x0) + (16 * x1) + (-12 * x2) + (19 * x3) = -20 ; +ASSERT (-28 * x0) + (20 * x1) + (-9 * x2) + (9 * x3) = -3 ; +ASSERT (24 * x0) + (22 * x1) + (24 * x2) + (20 * x3) = 5; +ASSERT (-1 * x0) + (-12 * x1) + (20 * x2) + (26 * x3) >= 22 ; +ASSERT (-23 * x0) + (-20 * x1) + (-8 * x2) + (1 * x3) < 2 ; +ASSERT (5 * x0) + (-27 * x1) + (-24 * x2) + (25 * x3) > -21 ; +ASSERT (1 * x0) + (-8 * x1) + (-17 * x2) + (-27 * x3) < -24 ; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-079.cvc b/test/regress/regress0/arith/integers/arith-int-079.cvc new file mode 100644 index 000000000..83a24f245 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-079.cvc @@ -0,0 +1,12 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (6 * x0) + (2 * x1) + (22 * x2) + (-18 * x3) = -15 ; +ASSERT (-8 * x0) + (-25 * x1) + (-25 * x2) + (7 * x3) > 10 ; +ASSERT (8 * x0) + (25 * x1) + (-7 * x2) + (-29 * x3) < -25 ; +ASSERT (27 * x0) + (17 * x1) + (-24 * x2) + (-5 * x3) <= 13 ; +ASSERT (5 * x0) + (-3 * x1) + (0 * x2) + (4 * x3) < -26 ; +ASSERT (25 * x0) + (7 * x1) + (27 * x2) + (-14 * x3) < 30 ; +ASSERT (-22 * x0) + (-17 * x1) + (9 * x2) + (-20 * x3) < -19 ; +ASSERT (31 * x0) + (-16 * x1) + (0 * x2) + (6 * x3) >= 18; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-080.cvc b/test/regress/regress0/arith/integers/arith-int-080.cvc new file mode 100644 index 000000000..f29f91896 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-080.cvc @@ -0,0 +1,12 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (5 * x0) + (-17 * x1) + (15 * x2) + (-15 * x3) = -14 ; +ASSERT (-28 * x0) + (-17 * x1) + (-29 * x2) + (-19 * x3) = 14; +ASSERT (9 * x0) + (-26 * x1) + (-16 * x2) + (-9 * x3) >= 28 ; +ASSERT (14 * x0) + (-32 * x1) + (-31 * x2) + (0 * x3) >= 30 ; +ASSERT (-31 * x0) + (-27 * x1) + (23 * x2) + (4 * x3) >= 21 ; +ASSERT (27 * x0) + (-30 * x1) + (8 * x2) + (13 * x3) < 31 ; +ASSERT (-1 * x0) + (-29 * x1) + (23 * x2) + (10 * x3) < -10 ; +ASSERT (15 * x0) + (-2 * x1) + (22 * x2) + (-28 * x3) >= 2 ; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-081.cvc b/test/regress/regress0/arith/integers/arith-int-081.cvc new file mode 100644 index 000000000..fcf857e29 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-081.cvc @@ -0,0 +1,8 @@ +% EXPECT: invalid +% EXIT: 10 +x0, x1, x2, x3 : INT; +ASSERT (-8 * x0) + (31 * x1) + (-23 * x2) + (-8 * x3) = 8; +ASSERT (24 * x0) + (-2 * x1) + (2 * x2) + (-2 * x3) >= -17 ; +ASSERT (-6 * x0) + (17 * x1) + (27 * x2) + (26 * x3) >= -30 ; +ASSERT (-19 * x0) + (-15 * x1) + (5 * x2) + (-27 * x3) < -3 ; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-082.cvc b/test/regress/regress0/arith/integers/arith-int-082.cvc new file mode 100644 index 000000000..0fbeeb03b --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-082.cvc @@ -0,0 +1,8 @@ +% EXPECT: invalid +% EXIT: 10 +x0, x1, x2, x3 : INT; +ASSERT (-29 * x0) + (-3 * x1) + (27 * x2) + (13 * x3) = -10 ; +ASSERT (7 * x0) + (-17 * x1) + (11 * x2) + (-30 * x3) <= 6 ; +ASSERT (30 * x0) + (17 * x1) + (-3 * x2) + (-31 * x3) > 10 ; +ASSERT (2 * x0) + (9 * x1) + (9 * x2) + (-16 * x3) <= 11; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-083.cvc b/test/regress/regress0/arith/integers/arith-int-083.cvc new file mode 100644 index 000000000..90171f772 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-083.cvc @@ -0,0 +1,8 @@ +% EXPECT: invalid +% EXIT: 10 +x0, x1, x2, x3 : INT; +ASSERT (19 * x0) + (-31 * x1) + (31 * x2) + (28 * x3) = -13 ; +ASSERT (1 * x0) + (13 * x1) + (12 * x2) + (-15 * x3) > -8 ; +ASSERT (7 * x0) + (17 * x1) + (-20 * x2) + (13 * x3) > -26 ; +ASSERT (-17 * x0) + (14 * x1) + (-23 * x2) + (17 * x3) <= -27; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-084.cvc b/test/regress/regress0/arith/integers/arith-int-084.cvc new file mode 100644 index 000000000..f190c5d4d --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-084.cvc @@ -0,0 +1,8 @@ +% EXPECT: invalid +% EXIT: 10 +x0, x1, x2, x3 : INT; +ASSERT (-2 * x0) + (-13 * x1) + (-14 * x2) + (-26 * x3) <= 4 ; +ASSERT (-17 * x0) + (-17 * x1) + (21 * x2) + (-4 * x3) < 18 ; +ASSERT (-31 * x0) + (23 * x1) + (4 * x2) + (29 * x3) > -6 ; +ASSERT (-14 * x0) + (32 * x1) + (-8 * x2) + (-8 * x3) <= -1; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-085.cvc b/test/regress/regress0/arith/integers/arith-int-085.cvc new file mode 100644 index 000000000..281ba0e29 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-085.cvc @@ -0,0 +1,9 @@ +% EXPECT: invalid +% EXIT: 10 +%% down from 3 +x0, x1, x2, x3 : INT; +ASSERT (22 * x0) + (-25 * x1) + (-20 * x2) + (8 * x3) = -6 ; +ASSERT (-9 * x0) + (30 * x1) + (-17 * x2) + (29 * x3) >= -15 ; +ASSERT (21 * x0) + (29 * x1) + (12 * x2) + (-3 * x3) <= -21 ; +ASSERT (-16 * x0) + (-26 * x1) + (11 * x2) + (-12 * x3) >= -14; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-086.cvc b/test/regress/regress0/arith/integers/arith-int-086.cvc new file mode 100644 index 000000000..21c058f7c --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-086.cvc @@ -0,0 +1,14 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (-16 * x0) + (28 * x1) + (2 * x2) + (7 * x3) = -25 ; +ASSERT (-20 * x0) + (-24 * x1) + (4 * x2) + (32 * x3) = -22 ; +ASSERT (19 * x0) + (28 * x1) + (-15 * x2) + (18 * x3) < -9 ; +ASSERT (-10 * x0) + (1 * x1) + (-3 * x2) + (6 * x3) <= 1 ; +ASSERT (-15 * x0) + (-32 * x1) + (28 * x2) + (6 * x3) >= -8 ; +ASSERT (-18 * x0) + (-16 * x1) + (15 * x2) + (-28 * x3) <= 1 ; +ASSERT (-20 * x0) + (-31 * x1) + (20 * x2) + (13 * x3) >= -7 ; +ASSERT (29 * x0) + (16 * x1) + (7 * x2) + (14 * x3) < 11 ; +ASSERT (-10 * x0) + (22 * x1) + (25 * x2) + (24 * x3) >= 5 ; +ASSERT (-3 * x0) + (11 * x1) + (27 * x2) + (11 * x3) <= 9; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-087.cvc b/test/regress/regress0/arith/integers/arith-int-087.cvc new file mode 100644 index 000000000..c403fdf3e --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-087.cvc @@ -0,0 +1,14 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (-4 * x0) + (25 * x1) + (-2 * x2) + (-16 * x3) = 27 ; +ASSERT (-11 * x0) + (26 * x1) + (18 * x2) + (-18 * x3) = -15 ; +ASSERT (-19 * x0) + (-27 * x1) + (-31 * x2) + (15 * x3) = 12; +ASSERT (10 * x0) + (-10 * x1) + (25 * x2) + (-3 * x3) < -30 ; +ASSERT (5 * x0) + (-18 * x1) + (21 * x2) + (-28 * x3) <= -4 ; +ASSERT (-6 * x0) + (15 * x1) + (-10 * x2) + (0 * x3) < -20 ; +ASSERT (10 * x0) + (23 * x1) + (-20 * x2) + (12 * x3) >= -15 ; +ASSERT (-31 * x0) + (-30 * x1) + (12 * x2) + (11 * x3) > 29 ; +ASSERT (26 * x0) + (23 * x1) + (28 * x2) + (-5 * x3) > 8 ; +ASSERT (6 * x0) + (-29 * x1) + (12 * x2) + (16 * x3) < 27 ; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-088.cvc b/test/regress/regress0/arith/integers/arith-int-088.cvc new file mode 100644 index 000000000..04361f9b1 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-088.cvc @@ -0,0 +1,14 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (-19 * x0) + (-9 * x1) + (-27 * x2) + (9 * x3) = -1 ; +ASSERT (-26 * x0) + (11 * x1) + (23 * x2) + (-5 * x3) >= 20 ; +ASSERT (7 * x0) + (28 * x1) + (6 * x2) + (-20 * x3) <= -16 ; +ASSERT (-15 * x0) + (21 * x1) + (5 * x2) + (-2 * x3) <= 11 ; +ASSERT (-5 * x0) + (-16 * x1) + (-16 * x2) + (14 * x3) <= 12 ; +ASSERT (3 * x0) + (28 * x1) + (22 * x2) + (-6 * x3) >= -31 ; +ASSERT (15 * x0) + (-13 * x1) + (10 * x2) + (21 * x3) <= -25 ; +ASSERT (1 * x0) + (-24 * x1) + (-30 * x2) + (25 * x3) > 17 ; +ASSERT (12 * x0) + (-3 * x1) + (0 * x2) + (23 * x3) < -12 ; +ASSERT (16 * x0) + (-9 * x1) + (1 * x2) + (-15 * x3) < -6; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-089.cvc b/test/regress/regress0/arith/integers/arith-int-089.cvc new file mode 100644 index 000000000..5d7b9e2d2 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-089.cvc @@ -0,0 +1,14 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (14 * x0) + (-14 * x1) + (-29 * x2) + (31 * x3) = -15 ; +ASSERT (-14 * x0) + (2 * x1) + (26 * x2) + (29 * x3) = 25 ; +ASSERT (19 * x0) + (-7 * x1) + (-15 * x2) + (12 * x3) = 32 ; +ASSERT (5 * x0) + (32 * x1) + (22 * x2) + (1 * x3) = -13 ; +ASSERT (-12 * x0) + (-9 * x1) + (-30 * x2) + (-13 * x3) >= 0 ; +ASSERT (-9 * x0) + (7 * x1) + (-24 * x2) + (22 * x3) >= 11 ; +ASSERT (28 * x0) + (-5 * x1) + (12 * x2) + (15 * x3) >= 31 ; +ASSERT (5 * x0) + (-6 * x1) + (5 * x2) + (-2 * x3) >= -5 ; +ASSERT (-14 * x0) + (-17 * x1) + (-29 * x2) + (-8 * x3) < -32 ; +ASSERT (20 * x0) + (-19 * x1) + (-27 * x2) + (-20 * x3) >= -2; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-090.cvc b/test/regress/regress0/arith/integers/arith-int-090.cvc new file mode 100644 index 000000000..a9f4b03a4 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-090.cvc @@ -0,0 +1,14 @@ +% EXPECT: invalid +% EXIT: 10 +x0, x1, x2, x3 : INT; +ASSERT (-13 * x0) + (-14 * x1) + (-10 * x2) + (32 * x3) = 11 ; +ASSERT (28 * x0) + (21 * x1) + (-20 * x2) + (-32 * x3) > -31 ; +ASSERT (10 * x0) + (19 * x1) + (-10 * x2) + (-2 * x3) > -31 ; +ASSERT (-31 * x0) + (17 * x1) + (15 * x2) + (31 * x3) > -12 ; +ASSERT (-17 * x0) + (16 * x1) + (17 * x2) + (-11 * x3) >= 17 ; +ASSERT (19 * x0) + (-31 * x1) + (-16 * x2) + (-29 * x3) >= 15 ; +ASSERT (24 * x0) + (-32 * x1) + (27 * x2) + (11 * x3) < 26 ; +ASSERT (-2 * x0) + (5 * x1) + (-21 * x2) + (24 * x3) >= -17 ; +ASSERT (13 * x0) + (11 * x1) + (-28 * x2) + (-5 * x3) > 16 ; +ASSERT (-16 * x0) + (17 * x1) + (22 * x2) + (6 * x3) > 21; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-091.cvc b/test/regress/regress0/arith/integers/arith-int-091.cvc new file mode 100644 index 000000000..ebf728533 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-091.cvc @@ -0,0 +1,23 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (26 * x0) + (32 * x1) + (-26 * x2) + (-26 * x3) = -26 ; +ASSERT (30 * x0) + (17 * x1) + (28 * x2) + (-9 * x3) = -21 ; +ASSERT (15 * x0) + (9 * x1) + (-13 * x2) + (-21 * x3) = -13 ; +ASSERT (-4 * x0) + (16 * x1) + (-5 * x2) + (8 * x3) = -25 ; +ASSERT (-11 * x0) + (26 * x1) + (1 * x2) + (23 * x3) < 6 ; +ASSERT (-31 * x0) + (-25 * x1) + (1 * x2) + (16 * x3) > -8 ; +ASSERT (9 * x0) + (-19 * x1) + (28 * x2) + (15 * x3) < -30 ; +ASSERT (32 * x0) + (18 * x1) + (2 * x2) + (31 * x3) > -7 ; +ASSERT (24 * x0) + (29 * x1) + (20 * x2) + (-16 * x3) >= 3 ; +ASSERT (-1 * x0) + (17 * x1) + (-27 * x2) + (-32 * x3) >= 20 ; +ASSERT (26 * x0) + (-23 * x1) + (6 * x2) + (30 * x3) <= 5 ; +ASSERT (13 * x0) + (6 * x1) + (-26 * x2) + (1 * x3) > -29 ; +ASSERT (26 * x0) + (2 * x1) + (8 * x2) + (-18 * x3) <= 32 ; +ASSERT (-21 * x0) + (28 * x1) + (23 * x2) + (4 * x3) <= -31 ; +ASSERT (26 * x0) + (2 * x1) + (-28 * x2) + (12 * x3) > 6 ; +ASSERT (-20 * x0) + (-22 * x1) + (-16 * x2) + (-21 * x3) <= -1 ; +ASSERT (21 * x0) + (-22 * x1) + (19 * x2) + (32 * x3) <= -10 ; +ASSERT (3 * x0) + (28 * x1) + (-11 * x2) + (0 * x3) > 0 ; +ASSERT (-13 * x0) + (-16 * x1) + (-17 * x2) + (-2 * x3) <= -17; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-092.cvc b/test/regress/regress0/arith/integers/arith-int-092.cvc new file mode 100644 index 000000000..f6622eb0b --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-092.cvc @@ -0,0 +1,23 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (-20 * x0) + (19 * x1) + (16 * x2) + (-27 * x3) = -22 ; +ASSERT (12 * x0) + (-18 * x1) + (-25 * x2) + (-1 * x3) = -22 ; +ASSERT (17 * x0) + (11 * x1) + (24 * x2) + (16 * x3) = -3 ; +ASSERT (15 * x0) + (-10 * x1) + (-15 * x2) + (25 * x3) = -30 ; +ASSERT (7 * x0) + (26 * x1) + (-8 * x2) + (-29 * x3) >= -32 ; +ASSERT (20 * x0) + (25 * x1) + (-23 * x2) + (13 * x3) >= -30 ; +ASSERT (27 * x0) + (-32 * x1) + (-27 * x2) + (13 * x3) >= -12 ; +ASSERT (25 * x0) + (-16 * x1) + (32 * x2) + (-6 * x3) >= -30 ; +ASSERT (32 * x0) + (-18 * x1) + (-6 * x2) + (-32 * x3) <= -26 ; +ASSERT (25 * x0) + (12 * x1) + (25 * x2) + (-14 * x3) > 5 ; +ASSERT (-4 * x0) + (-20 * x1) + (12 * x2) + (-30 * x3) >= 13 ; +ASSERT (8 * x0) + (18 * x1) + (0 * x2) + (-28 * x3) <= 18 ; +ASSERT (-32 * x0) + (-25 * x1) + (23 * x2) + (5 * x3) < 29 ; +ASSERT (7 * x0) + (19 * x1) + (2 * x2) + (-31 * x3) > 7 ; +ASSERT (24 * x0) + (-17 * x1) + (-31 * x2) + (31 * x3) > 0 ; +ASSERT (13 * x0) + (20 * x1) + (-1 * x2) + (17 * x3) > 1 ; +ASSERT (17 * x0) + (26 * x1) + (6 * x2) + (29 * x3) >= -10 ; +ASSERT (-25 * x0) + (4 * x1) + (-22 * x2) + (14 * x3) < -23 ; +ASSERT (24 * x0) + (2 * x1) + (4 * x2) + (2 * x3) < 1; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-093.cvc b/test/regress/regress0/arith/integers/arith-int-093.cvc new file mode 100644 index 000000000..3cb1aed11 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-093.cvc @@ -0,0 +1,23 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (22 * x0) + (-2 * x1) + (-1 * x2) + (-24 * x3) = 8 ; +ASSERT (-6 * x0) + (9 * x1) + (-20 * x2) + (-23 * x3) = 14 ; +ASSERT (-11 * x0) + (4 * x1) + (24 * x2) + (-6 * x3) <= -23 ; +ASSERT (3 * x0) + (5 * x1) + (-5 * x2) + (17 * x3) < -17 ; +ASSERT (-10 * x0) + (-20 * x1) + (-16 * x2) + (-29 * x3) >= 6 ; +ASSERT (-28 * x0) + (1 * x1) + (-22 * x2) + (-16 * x3) >= 4 ; +ASSERT (19 * x0) + (8 * x1) + (-8 * x2) + (-2 * x3) > -23 ; +ASSERT (11 * x0) + (17 * x1) + (30 * x2) + (31 * x3) < -32 ; +ASSERT (23 * x0) + (30 * x1) + (-12 * x2) + (16 * x3) <= 4 ; +ASSERT (-23 * x0) + (-8 * x1) + (21 * x2) + (21 * x3) <= -14 ; +ASSERT (13 * x0) + (15 * x1) + (-6 * x2) + (-1 * x3) >= -8 ; +ASSERT (-21 * x0) + (18 * x1) + (27 * x2) + (-16 * x3) <= 11 ; +ASSERT (30 * x0) + (-6 * x1) + (5 * x2) + (-27 * x3) <= -7 ; +ASSERT (0 * x0) + (3 * x1) + (13 * x2) + (28 * x3) > -21 ; +ASSERT (-15 * x0) + (-20 * x1) + (10 * x2) + (-23 * x3) < 27 ; +ASSERT (24 * x0) + (6 * x1) + (-29 * x2) + (1 * x3) <= -23 ; +ASSERT (-24 * x0) + (-14 * x1) + (-15 * x2) + (8 * x3) > -19 ; +ASSERT (17 * x0) + (15 * x1) + (8 * x2) + (-31 * x3) >= -16 ; +ASSERT (-19 * x0) + (7 * x1) + (-28 * x2) + (20 * x3) < -19; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-094.cvc b/test/regress/regress0/arith/integers/arith-int-094.cvc new file mode 100644 index 000000000..4abce2679 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-094.cvc @@ -0,0 +1,23 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (-7 * x0) + (-11 * x1) + (26 * x2) + (10 * x3) = 31 ; +ASSERT (-17 * x0) + (-20 * x1) + (24 * x2) + (-9 * x3) = -32 ; +ASSERT (5 * x0) + (14 * x1) + (7 * x2) + (-29 * x3) = 31 ; +ASSERT (17 * x0) + (8 * x1) + (23 * x2) + (-26 * x3) <= -12 ; +ASSERT (7 * x0) + (29 * x1) + (24 * x2) + (4 * x3) <= -21 ; +ASSERT (-16 * x0) + (7 * x1) + (7 * x2) + (-29 * x3) < -16 ; +ASSERT (-7 * x0) + (-11 * x1) + (-17 * x2) + (22 * x3) > -11 ; +ASSERT (-10 * x0) + (-17 * x1) + (21 * x2) + (29 * x3) > -7 ; +ASSERT (-28 * x0) + (-26 * x1) + (-24 * x2) + (-21 * x3) < -20 ; +ASSERT (-32 * x0) + (26 * x1) + (-8 * x2) + (2 * x3) >= -18 ; +ASSERT (18 * x0) + (-23 * x1) + (-26 * x2) + (-24 * x3) > -30 ; +ASSERT (-9 * x0) + (31 * x1) + (-26 * x2) + (-22 * x3) < -15 ; +ASSERT (27 * x0) + (-1 * x1) + (10 * x2) + (28 * x3) < -20 ; +ASSERT (-4 * x0) + (-22 * x1) + (-24 * x2) + (2 * x3) < -13 ; +ASSERT (-4 * x0) + (-23 * x1) + (-16 * x2) + (18 * x3) > -20 ; +ASSERT (13 * x0) + (-30 * x1) + (-3 * x2) + (-25 * x3) <= 31 ; +ASSERT (21 * x0) + (-28 * x1) + (22 * x2) + (19 * x3) > 7 ; +ASSERT (-2 * x0) + (-31 * x1) + (24 * x2) + (18 * x3) > 27 ; +ASSERT (-14 * x0) + (-5 * x1) + (-22 * x2) + (1 * x3) <= -15; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-095.cvc b/test/regress/regress0/arith/integers/arith-int-095.cvc new file mode 100644 index 000000000..3aa4b2489 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-095.cvc @@ -0,0 +1,23 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (2 * x0) + (28 * x1) + (3 * x2) + (8 * x3) > -32 ; +ASSERT (-15 * x0) + (21 * x1) + (-11 * x2) + (28 * x3) <= -19 ; +ASSERT (32 * x0) + (29 * x1) + (-1 * x2) + (-10 * x3) < -23 ; +ASSERT (6 * x0) + (-27 * x1) + (29 * x2) + (28 * x3) < 5 ; +ASSERT (-7 * x0) + (-7 * x1) + (-28 * x2) + (32 * x3) <= -32 ; +ASSERT (-10 * x0) + (20 * x1) + (-28 * x2) + (-28 * x3) >= -6 ; +ASSERT (-13 * x0) + (-9 * x1) + (4 * x2) + (-32 * x3) > -1 ; +ASSERT (-21 * x0) + (4 * x1) + (0 * x2) + (-13 * x3) >= -1 ; +ASSERT (18 * x0) + (-21 * x1) + (-16 * x2) + (24 * x3) <= -12 ; +ASSERT (18 * x0) + (-10 * x1) + (-10 * x2) + (-3 * x3) <= -10 ; +ASSERT (-32 * x0) + (9 * x1) + (-24 * x2) + (-19 * x3) < -4 ; +ASSERT (12 * x0) + (20 * x1) + (31 * x2) + (-25 * x3) <= 23 ; +ASSERT (-22 * x0) + (15 * x1) + (-12 * x2) + (-6 * x3) < 18 ; +ASSERT (-25 * x0) + (-8 * x1) + (32 * x2) + (26 * x3) > -20 ; +ASSERT (-30 * x0) + (27 * x1) + (0 * x2) + (27 * x3) >= 7 ; +ASSERT (-8 * x0) + (-2 * x1) + (-6 * x2) + (-21 * x3) <= 21 ; +ASSERT (8 * x0) + (-31 * x1) + (-4 * x2) + (1 * x3) > -11 ; +ASSERT (22 * x0) + (-25 * x1) + (-26 * x2) + (10 * x3) < -32 ; +ASSERT (-12 * x0) + (-13 * x1) + (15 * x2) + (4 * x3) < 26; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-096.cvc b/test/regress/regress0/arith/integers/arith-int-096.cvc new file mode 100644 index 000000000..f409f37af --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-096.cvc @@ -0,0 +1,9 @@ +% EXPECT: invalid +% EXIT: 10 +x0, x1, x2, x3 : INT; +ASSERT (23 * x0) + (24 * x1) + (19 * x2) + (-3 * x3) = -16 ; +ASSERT (2 * x0) + (-13 * x1) + (5 * x2) + (-1 * x3) = 28; +ASSERT (-6 * x0) + (-5 * x1) + (-2 * x2) + (-9 * x3) > -3 ; +ASSERT (30 * x0) + (22 * x1) + (-20 * x2) + (1 * x3) > -12 ; +ASSERT (-8 * x0) + (-25 * x1) + (28 * x2) + (-25 * x3) <= -8 ; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-097.cvc b/test/regress/regress0/arith/integers/arith-int-097.cvc new file mode 100644 index 000000000..f0fca22fb --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-097.cvc @@ -0,0 +1,9 @@ +% EXPECT: invalid +% EXIT: 10 +x0, x1, x2, x3 : INT; +ASSERT (19 * x0) + (-11 * x1) + (-19 * x2) + (5 * x3) = 26 ; +ASSERT (1 * x0) + (-28 * x1) + (-2 * x2) + (15 * x3) < 9 ; +ASSERT (-8 * x0) + (-1 * x1) + (-25 * x2) + (-7 * x3) <= -31 ; +ASSERT (-7 * x0) + (11 * x1) + (-5 * x2) + (-19 * x3) > 32 ; +ASSERT (-22 * x0) + (13 * x1) + (-16 * x2) + (-12 * x3) <= 32; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-098.cvc b/test/regress/regress0/arith/integers/arith-int-098.cvc new file mode 100644 index 000000000..37a472265 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-098.cvc @@ -0,0 +1,9 @@ +% EXPECT: invalid +% EXIT: 10 +x0, x1, x2, x3 : INT; +ASSERT (-28 * x0) + (12 * x1) + (-19 * x2) + (10 * x3) = 16 ; +ASSERT (19 * x0) + (-25 * x1) + (-8 * x2) + (-32 * x3) = 12; +ASSERT (18 * x0) + (21 * x1) + (5 * x2) + (-14 * x3) < -12 ; +ASSERT (-13 * x0) + (32 * x1) + (-5 * x2) + (-13 * x3) <= -15 ; +ASSERT (30 * x0) + (-19 * x1) + (28 * x2) + (-27 * x3) <= -18 ; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-099.cvc b/test/regress/regress0/arith/integers/arith-int-099.cvc new file mode 100644 index 000000000..9ff8724af --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-099.cvc @@ -0,0 +1,9 @@ +% EXPECT: invalid +% EXIT: 10 +x0, x1, x2, x3 : INT; +ASSERT (-31 * x0) + (-20 * x1) + (-30 * x2) + (-28 * x3) = -24 ; +ASSERT (11 * x0) + (-32 * x1) + (-2 * x2) + (8 * x3) <= 16 ; +ASSERT (-10 * x0) + (16 * x1) + (31 * x2) + (19 * x3) >= -21 ; +ASSERT (-15 * x0) + (18 * x1) + (-16 * x2) + (7 * x3) <= -12 ; +ASSERT (14 * x0) + (-1 * x1) + (12 * x2) + (27 * x3) >= -12; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-100.cvc b/test/regress/regress0/arith/integers/arith-int-100.cvc new file mode 100644 index 000000000..a75128232 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-100.cvc @@ -0,0 +1,9 @@ +% EXPECT: invalid +% EXIT: 10 +x0, x1, x2, x3 : INT; +ASSERT (27 * x0) + (-21 * x1) + (-6 * x2) + (-6 * x3) > -15 ; +ASSERT (-5 * x0) + (-10 * x1) + (2 * x2) + (-16 * x3) <= -7 ; +ASSERT (25 * x0) + (25 * x1) + (-15 * x2) + (-32 * x3) > -31 ; +ASSERT (17 * x0) + (-26 * x1) + (9 * x2) + (-28 * x3) >= -29 ; +ASSERT (-10 * x0) + (-18 * x1) + (15 * x2) + (0 * x3) <= 32; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-interval.cvc b/test/regress/regress0/arith/integers/arith-interval.cvc new file mode 100644 index 000000000..e8b229faa --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-interval.cvc @@ -0,0 +1,8 @@ +% EXPECT: valid +% EXIT: 20 +x: INT; +P: INT -> BOOLEAN; + +ASSERT 1 <= x AND x <= 2; +ASSERT P(1) AND P(2); +QUERY P(x); -- 2.30.2