/** 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();
return TypeNode(mkTypeConst<TypeConstant>(REAL_TYPE));
}
+/** Get the (singleton) type for pseudobooleans. */
+inline TypeNode NodeManager::pseudobooleanType() {
+ return TypeNode(mkTypeConst<TypeConstant>(PSEUDOBOOLEAN_TYPE));
+}
+
/** Get the (singleton) type for sorts. */
inline TypeNode NodeManager::kindType() {
return TypeNode(mkTypeConst<TypeConstant>(KIND_TYPE));
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);
Assert(isReal());
}
+PseudobooleanType::PseudobooleanType(const Type& t) throw(AssertionException) :
+ Type(t) {
+ Assert(isPseudoboolean());
+}
+
BitVectorType::BitVectorType(const Type& t) throw(AssertionException) :
Type(t) {
Assert(isBitVector());
class BooleanType;
class IntegerType;
class RealType;
+class PseudobooleanType;
class BitVectorType;
class ArrayType;
class DatatypeType;
*/
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
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.
*/
bool TypeNode::isBoolean() const {
return getKind() == kind::TYPE_CONSTANT &&
- getConst<TypeConstant>() == BOOLEAN_TYPE;
+ ( getConst<TypeConstant>() == BOOLEAN_TYPE ||
+ getConst<TypeConstant>() == PSEUDOBOOLEAN_TYPE );
}
bool TypeNode::isInteger() const {
return getKind() == kind::TYPE_CONSTANT &&
- getConst<TypeConstant>() == INTEGER_TYPE;
+ ( getConst<TypeConstant>() == INTEGER_TYPE ||
+ getConst<TypeConstant>() == PSEUDOBOOLEAN_TYPE );
}
bool TypeNode::isReal() const {
- return getKind() == kind::TYPE_CONSTANT
- && ( getConst<TypeConstant>() == REAL_TYPE ||
- getConst<TypeConstant>() == INTEGER_TYPE );
+ return getKind() == kind::TYPE_CONSTANT &&
+ ( getConst<TypeConstant>() == REAL_TYPE ||
+ getConst<TypeConstant>() == INTEGER_TYPE ||
+ getConst<TypeConstant>() == PSEUDOBOOLEAN_TYPE );
+}
+
+bool TypeNode::isPseudoboolean() const {
+ return getKind() == kind::TYPE_CONSTANT &&
+ getConst<TypeConstant>() == PSEUDOBOOLEAN_TYPE;
}
bool TypeNode::isArray() const {
/** Is this the Real type? */
bool isReal() const;
+ /** Is this the Pseudoboolean type? */
+ bool isPseudoboolean() const;
+
/** Is this an array type? */
bool isArray() const;
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';
| 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"); }
case BOOLEAN_TYPE:
out << "BOOLEAN";
break;
+ case PSEUDOBOOLEAN_TYPE:
+ out << "PSEUDOBOOLEAN";
+ break;
case KIND_TYPE:
out << "TYPE";
break;
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) {
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);
}
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<TNode, Node, TNodeHashFunction> cache;
for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
simplex.h \
simplex.cpp \
theory_arith.h \
- theory_arith.cpp
+ theory_arith.cpp \
+ dio_solver.h \
+ dio_solver.cpp
EXTRA_DIST = \
kinds
TNode left = t[0];
TNode right = t[1];
-
Comparison cmp = Comparison::mkComparison(t.getKind(), Polynomial::parsePolynomial(left), Constant(right));
if(cmp.isBoolean()){
#include "util/propositional_query.h"
+#include "expr/expr.h"
+#include "expr/convenience_node_builders.h"
+
#include <vector>
using namespace std;
using namespace CVC4::theory::arith;
-ArithStaticLearner::ArithStaticLearner():
+ArithStaticLearner::ArithStaticLearner(SubstitutionMap& pbSubstitutions) :
d_miplibTrick(),
d_miplibTrickKeys(),
+ d_pbSubstitutions(pbSubstitutions),
d_statistics()
{}
postProcess(learned);
}
+
void ArithStaticLearner::clear(){
d_miplibTrick.clear();
d_miplibTrickKeys.clear();
+ // do not clear d_pbSubstitutions, as it is shared
}
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<TypeConstant>() == INTEGER_TYPE) {
+ k1 = c1.getConst<Integer>();
+ } else {
+ Rational r = c1.getConst<Rational>();
+ if(r.getDenominator() == 1) {
+ k1 = r.getNumerator();
+ } else {
+ break;
+ }
+ }
+ if(c2.getType().getConst<TypeConstant>() == INTEGER_TYPE) {
+ k2 = c2.getConst<Integer>();
+ } else {
+ Rational r = c2.getConst<Rational>();
+ 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);
}
}
+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]);
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;
}
}
#include "util/stats.h"
#include "theory/arith/arith_utilities.h"
+#include "theory/substitutions.h"
#include <set>
#include <list>
VarToNodeSetMap d_miplibTrick;
std::list<TNode> 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.
*/
NodeToMinMaxMap d_maxMap;
public:
- ArithStaticLearner();
+ ArithStaticLearner(SubstitutionMap& pbSubstitutions);
void staticLearning(TNode n, NodeBuilder<>& learned);
void addBound(TNode n);
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<Rational>& values, NodeBuilder<>& learned);
+ void checkBoundsForPseudobooleanReplacement(TNode n);
+
/** These fields are designed to be accessable to ArithStaticLearner methods. */
class Statistics {
public:
}
/**
- * 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
+/********************* */
+/*! \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
/*! \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
** \todo document this file
**/
-#include <vector>
-#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 <vector>
+#include "theory/arith/arith_utilities.h"
+
namespace CVC4 {
namespace theory {
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)
}
};
-}; /* namespace arith */
-}; /* namespace theory */
-}; /* namespace CVC4 */
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
#endif /* __CVC4__THEORY__ARITH__ARTIHVAR_SET_H */
--- /dev/null
+/********************* */
+/*! \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 <iostream>
+
+using namespace std;
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+/*
+static void printEquation(vector<Rational>& coeffs,
+ vector<ArithVar>& variables,
+ ostream& out) {
+ Assert(coeffs.size() == variables.size());
+ vector<Rational>::const_iterator i = coeffs.begin();
+ vector<ArithVar>::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 */
--- /dev/null
+/********************* */
+/*! \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 <vector>
+#include <utility>
+
+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 */
"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"
}
}
+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()) {
const Rational& rConst = right.getNode().getConst<Rational>();
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<Rational>(), result)) {
+ return Comparison(result);
+ }
+ }
+
+ return Comparison(toNode(k, left, right), k, left, right);
}
Comparison Comparison::addConstant(const Constant& constant) const {
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)),
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;
}
/* 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;
return 0 <= x && x < d_mapSize;
}
-};
+};/* class ArithPartialModel */
-
-
-}; /* namesapce arith */
-}; /* namespace theory */
-}; /* namespace CVC4 */
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
++colIter;
}
}
-void Tableau::printTableau(){
+void Tableau::printTableau() const {
Debug("tableau") << "Tableau::d_activeRows" << endl;
ArithVarSet::const_iterator basicIter = beginBasic(), endIter = endBasic();
}
}
-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;
Debug("tableau") << "}" << endl;
}
-void Tableau::printEntry(const TableauEntry& entry){
+void Tableau::printEntry(const TableauEntry& entry) const {
Debug("tableau") << entry.getColVar() << "*" << entry.getCoefficient();
}
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)
{}
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;
}
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);
/**
* 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:
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),
}
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) {
// 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;
+ }
}
}
}
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;
}
}
}
- 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();
}
}
+ 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;
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);
#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"
ArithVarNodeMap d_arithvarNodeMap;
+ /**
+ * List of the types of variables in the system.
+ * "True" means integer, "false" means (non-integer) real.
+ */
+ std::vector<short> 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
*/
ArithVarSet d_userVariables;
-
-
/**
* List of all of the inequalities asserted in the current context.
*/
*/
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;
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");
}
}
throw TypeCheckingExceptionPrivate(n, ss.str());
}
- if ( lhsType == booleanType ) {
+ if ( lhsType == booleanType && rhsType == booleanType ) {
throw TypeCheckingExceptionPrivate(n, "equality between two boolean terms (use IFF instead)");
}
}
* @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
}
}
-}
-}
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
#include <utility>
#include <vector>
+#include <algorithm>
#include "expr/node.h"
namespace CVC4 {
return const_cast<SubstitutionMap*>(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
*/
}
/**
- * 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; }
}
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);
boolean_simplification.cpp \
ite_removal.h \
ite_removal.cpp \
+ pseudoboolean.h \
+ pseudoboolean.cpp \
node_visitor.h
libutil_la_LIBADD = \
return *this;
}
- /** Raise this Integer to the power <code>exp</code>.
+ /**
+ * Raise this Integer to the power <code>exp</code>.
*
* @param exp the exponent
*/
}
}
+ /**
+ * 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){
return *this;
}
- /** Raise this Integer to the power <code>exp</code>.
+ /**
+ * Raise this Integer to the power <code>exp</code>.
*
* @param exp the exponent
*/
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);
}
--- /dev/null
+/********************* */
+/*! \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 */
--- /dev/null
+/********************* */
+/*! \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 */
}
}
+ 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;
return d_value >= y.d_value;
}
-
-
-
Rational operator+(const Rational& y) const{
return Rational( d_value + y.d_value );
}
* 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());
}
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;
return d_value >= y.d_value;
}
-
-
-
Rational operator+(const Rational& y) const{
return Rational( d_value + y.d_value );
}
blu='\e[1;34m'; \
std='\e[m'; \
}
-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:
--- /dev/null
+topdir = ../../../..
+srcdir = test/regress/regress0/arith
+
+include $(topdir)/Makefile.subdir
+
+# synonyms for "check"
+.PHONY: test
+test: check
+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,
--- /dev/null
+topdir = ../../../../..
+srcdir = test/regress/regress0/arith/integers
+
+include $(topdir)/Makefile.subdir
+
+# synonyms for "check"
+.PHONY: test
+test: check
--- /dev/null
+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:
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% EXPECT: invalid
+% EXIT: 10
+x0, x1, x2, x3 : INT;
+ASSERT (8 * x0) + (-27 * x1) + (29 * x2) + (-13 * x3) < 12;
+QUERY FALSE;
--- /dev/null
+% EXPECT: invalid
+% EXIT: 10
+x0, x1, x2, x3 : INT;
+ASSERT (-24 * x0) + (25 * x1) + (-28 * x2) + (31 * x3) > 18;
+QUERY FALSE;
--- /dev/null
+% EXPECT: invalid
+% EXIT: 10
+x0, x1, x2, x3 : INT;
+ASSERT (29 * x0) + (-19 * x1) + (23 * x2) + (15 * x3) <= 9;
+QUERY FALSE;
--- /dev/null
+% EXPECT: invalid
+% EXIT: 10
+x0, x1, x2, x3 : INT;
+ASSERT (4 * x0) + (8 * x1) + (27 * x2) + (-12 * x3) = -5;
+QUERY FALSE;
--- /dev/null
+% EXPECT: invalid
+% EXIT: 10
+x0, x1, x2, x3 : INT;
+ASSERT (-19 * x0) + (-29 * x1) + (2 * x2) + (26 * x3) >= 3;
+QUERY FALSE;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% EXPECT: valid
+% EXIT: 20
+x1: INT;
+x0: INT;
+QUERY NOT (((x0 * 6) + (x1 * 32)) = 1);
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% 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;
--- /dev/null
+% EXPECT: valid
+% EXIT: 20
+x: INT;
+P: INT -> BOOLEAN;
+
+ASSERT 1 <= x AND x <= 2;
+ASSERT P(1) AND P(2);
+QUERY P(x);
projects / cvc5.git / commitdiff