diff options
Diffstat (limited to 'src')
41 files changed, 943 insertions, 81 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 5c3e4731b..0ac215f1e 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -509,9 +509,12 @@ public: /** Get the (singleton) type for integers. */ inline TypeNode integerType(); - /** Get the (singleton) type for booleans. */ + /** Get the (singleton) type for reals. */ inline TypeNode realType(); + /** Get the (singleton) type for pseudobooleans. */ + inline TypeNode pseudobooleanType(); + /** Get the (singleton) type for sorts. */ inline TypeNode kindType(); @@ -772,6 +775,11 @@ inline TypeNode NodeManager::realType() { return TypeNode(mkTypeConst<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)); diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 077fc5ee2..e162065b0 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -202,6 +202,19 @@ Type::operator RealType() const throw(AssertionException) { return RealType(*this); } +/** Is this the pseudoboolean type? */ +bool Type::isPseudoboolean() const { + NodeManagerScope nms(d_nodeManager); + return d_typeNode->isPseudoboolean(); +} + +/** Cast to a pseudoboolean type */ +Type::operator PseudobooleanType() const throw(AssertionException) { + NodeManagerScope nms(d_nodeManager); + Assert(isPseudoboolean()); + return PseudobooleanType(*this); +} + /** Is this the bit-vector type? */ bool Type::isBitVector() const { NodeManagerScope nms(d_nodeManager); @@ -435,6 +448,11 @@ RealType::RealType(const Type& t) throw(AssertionException) : Assert(isReal()); } +PseudobooleanType::PseudobooleanType(const Type& t) throw(AssertionException) : + Type(t) { + Assert(isPseudoboolean()); +} + BitVectorType::BitVectorType(const Type& t) throw(AssertionException) : Type(t) { Assert(isBitVector()); diff --git a/src/expr/type.h b/src/expr/type.h index 14ca3baf3..a63ca6cf0 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -46,6 +46,7 @@ class NodeTemplate; class BooleanType; class IntegerType; class RealType; +class PseudobooleanType; class BitVectorType; class ArrayType; class DatatypeType; @@ -226,6 +227,18 @@ public: operator RealType() const throw(AssertionException); /** + * Is this the pseudoboolean type? + * @return true if the type is the pseudoboolean type + */ + bool isPseudoboolean() const; + + /** + * Cast this type to a pseudoboolean type + * @return the PseudobooleanType + */ + operator PseudobooleanType() const throw(AssertionException); + + /** * Is this the bit-vector type? * @return true if the type is a bit-vector type */ @@ -410,6 +423,17 @@ public: };/* 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. */ class CVC4_PUBLIC FunctionType : public Type { diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index b9047307d..76a084204 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -73,18 +73,26 @@ Node TypeNode::mkGroundTerm() const { bool TypeNode::isBoolean() const { return getKind() == kind::TYPE_CONSTANT && - getConst<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 { diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 0f4b122db..3f4e52d36 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -413,6 +413,9 @@ public: /** Is this the Real type? */ bool isReal() const; + /** Is this the Pseudoboolean type? */ + bool isPseudoboolean() const; + /** Is this an array type? */ bool isArray() const; diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index cd4c66664..75a59c6e0 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -53,6 +53,7 @@ tokens { CHECK_TYPE_TOK = 'CHECK_TYPE'; GET_CHILD_TOK = 'GET_CHILD'; GET_OP_TOK = 'GET_OP'; + GET_VALUE_TOK = 'GET_VALUE'; SUBSTITUTE_TOK = 'SUBSTITUTE'; DBG_TOK = 'DBG'; TRACE_TOK = 'TRACE'; @@ -646,6 +647,9 @@ mainCommand[CVC4::Command*& cmd] | GET_OP_TOK formula[f] { UNSUPPORTED("GET_OP command"); } + | GET_VALUE_TOK formula[f] + { cmd = new GetValueCommand(f); } + | SUBSTITUTE_TOK identifier[id,CHECK_NONE,SYM_VARIABLE] COLON type[t,CHECK_DECLARED] EQUAL_TOK formula[f] LBRACKET identifier[id,CHECK_NONE,SYM_VARIABLE] ASSIGN_TOK formula[f] RBRACKET { UNSUPPORTED("SUBSTITUTE command"); } diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 11d633271..8e089a8a3 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -102,6 +102,9 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, case BOOLEAN_TYPE: out << "BOOLEAN"; break; + case PSEUDOBOOLEAN_TYPE: + out << "PSEUDOBOOLEAN"; + break; case KIND_TYPE: out << "TYPE"; break; diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 9b0c4847b..9797e4c67 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -146,7 +146,7 @@ SatLiteral CnfStream::convertAtom(TNode node) { Assert(!isTranslated(node), "atom already mapped!"); - bool theoryLiteral = node.getKind() != kind::VARIABLE; + bool theoryLiteral = node.getKind() != kind::VARIABLE && !node.getType().isPseudoboolean(); SatLiteral lit = newLiteral(node, theoryLiteral); if(node.getKind() == kind::CONST_BOOLEAN) { @@ -396,9 +396,8 @@ SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) { break; case EQUAL: if(node[0].getType().isBoolean()) { - // should have an IFF instead - Unreachable("= Bool Bool shouldn't be possible ?!"); - //nodeLit = handleIff(node[0].iffNode(node[1])); + // normally this is an IFF, but EQUAL is possible with pseudobooleans + nodeLit = handleIff(node[0].iffNode(node[1])); } else { nodeLit = convertAtom(node); } diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 60030bbab..dcfa43424 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -618,7 +618,7 @@ void SmtEnginePrivate::simplifyAssertions() throw(NoSuchFunctionException, Asser Debug("simplify") << "SmtEnginePrivate::simplify()" << std::endl; if(!Options::current()->lazyDefinitionExpansion) { - Debug("simplify") << "SmtEnginePrivate::simplify(): exanding definitions" << std::endl; + Debug("simplify") << "SmtEnginePrivate::simplify(): expanding definitions" << std::endl; TimerStat::CodeTimer codeTimer(d_smt.d_definitionExpansionTime); hash_map<TNode, Node, TNodeHashFunction> cache; for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) { diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am index 7f193b9e3..36ab2cd68 100644 --- a/src/theory/arith/Makefile.am +++ b/src/theory/arith/Makefile.am @@ -32,7 +32,9 @@ libarith_la_SOURCES = \ simplex.h \ simplex.cpp \ theory_arith.h \ - theory_arith.cpp + theory_arith.cpp \ + dio_solver.h \ + dio_solver.cpp EXTRA_DIST = \ kinds diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index d2ecaffe4..8d12e78fe 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -182,7 +182,6 @@ RewriteResponse ArithRewriter::postRewriteAtomConstantRHS(TNode t){ TNode left = t[0]; TNode right = t[1]; - Comparison cmp = Comparison::mkComparison(t.getKind(), Polynomial::parsePolynomial(left), Constant(right)); if(cmp.isBoolean()){ diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp index 77a89b54b..a5fa428c6 100644 --- a/src/theory/arith/arith_static_learner.cpp +++ b/src/theory/arith/arith_static_learner.cpp @@ -24,6 +24,9 @@ #include "util/propositional_query.h" +#include "expr/expr.h" +#include "expr/convenience_node_builders.h" + #include <vector> using namespace std; @@ -34,9 +37,10 @@ using namespace CVC4::theory; using namespace CVC4::theory::arith; -ArithStaticLearner::ArithStaticLearner(): +ArithStaticLearner::ArithStaticLearner(SubstitutionMap& pbSubstitutions) : d_miplibTrick(), d_miplibTrickKeys(), + d_pbSubstitutions(pbSubstitutions), d_statistics() {} @@ -105,9 +109,11 @@ void ArithStaticLearner::staticLearning(TNode n, NodeBuilder<>& learned){ postProcess(learned); } + void ArithStaticLearner::clear(){ d_miplibTrick.clear(); d_miplibTrickKeys.clear(); + // do not clear d_pbSubstitutions, as it is shared } @@ -151,11 +157,101 @@ void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet d_minMap[n] = coerceToRational(n); d_maxMap[n] = coerceToRational(n); break; + case OR: { + // Look for things like "x = 0 OR x = 1" (that are defTrue) and + // turn them into a pseudoboolean. We catch "x >= 0 + if(defTrue.find(n) == defTrue.end() || + n.getNumChildren() != 2 || + n[0].getKind() != EQUAL || + n[1].getKind() != EQUAL) { + break; + } + Node var, c1, c2; + if(n[0][0].getMetaKind() == metakind::VARIABLE && + n[0][1].getMetaKind() == metakind::CONSTANT) { + var = n[0][0]; + c1 = n[0][1]; + } else if(n[0][1].getMetaKind() == metakind::VARIABLE && + n[0][0].getMetaKind() == metakind::CONSTANT) { + var = n[0][1]; + c1 = n[0][0]; + } else { + break; + } + if(!var.getType().isInteger() || + !c1.getType().isReal()) { + break; + } + if(var == n[1][0]) { + c2 = n[1][1]; + } else if(var == n[1][1]) { + c2 = n[1][0]; + } else { + break; + } + if(!c2.getType().isReal()) { + break; + } + + Integer k1, k2; + if(c1.getType().getConst<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); @@ -341,6 +437,27 @@ void ArithStaticLearner::miplibTrick(TNode var, set<Rational>& values, NodeBuild } } +void ArithStaticLearner::checkBoundsForPseudobooleanReplacement(TNode n) { + NodeToMinMaxMap::iterator minFind = d_minMap.find(n); + NodeToMinMaxMap::iterator maxFind = d_maxMap.find(n); + + if( n.getType().isInteger() && + minFind != d_minMap.end() && + maxFind != d_maxMap.end() && + ( ( (*minFind).second.getNoninfinitesimalPart() == 1 && + (*minFind).second.getInfinitesimalPart() == 0 ) || + ( (*minFind).second.getNoninfinitesimalPart() == 0 && + (*minFind).second.getInfinitesimalPart() > 0 ) ) && + ( ( (*maxFind).second.getNoninfinitesimalPart() == 1 && + (*maxFind).second.getInfinitesimalPart() == 0 ) || + ( (*maxFind).second.getNoninfinitesimalPart() == 2 && + (*maxFind).second.getInfinitesimalPart() < 0 ) ) ) { + // eligible for pseudoboolean replacement + Debug("pb") << "eligible for pseudoboolean replacement: " << n << endl; + replaceWithPseudoboolean(n); + } +} + void ArithStaticLearner::addBound(TNode n) { NodeToMinMaxMap::iterator minFind = d_minMap.find(n[0]); @@ -349,25 +466,29 @@ void ArithStaticLearner::addBound(TNode n) { Rational constant = coerceToRational(n[1]); DeltaRational bound = constant; - switch(n.getKind()) { + switch(Kind k = n.getKind()) { case kind::LT: bound = DeltaRational(constant, -1); + /* fall through */ case kind::LEQ: if (maxFind == d_maxMap.end() || maxFind->second > bound) { d_maxMap[n[0]] = bound; Debug("arith::static") << "adding bound " << n << endl; + checkBoundsForPseudobooleanReplacement(n[0]); } break; case kind::GT: bound = DeltaRational(constant, 1); + /* fall through */ case kind::GEQ: if (minFind == d_minMap.end() || minFind->second < bound) { d_minMap[n[0]] = bound; Debug("arith::static") << "adding bound " << n << endl; + checkBoundsForPseudobooleanReplacement(n[0]); } break; default: - // nothing else + Unhandled(k); break; } } diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h index 0ed9cbe85..c58778215 100644 --- a/src/theory/arith/arith_static_learner.h +++ b/src/theory/arith/arith_static_learner.h @@ -25,6 +25,7 @@ #include "util/stats.h" #include "theory/arith/arith_utilities.h" +#include "theory/substitutions.h" #include <set> #include <list> @@ -45,6 +46,19 @@ private: 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. */ typedef __gnu_cxx::hash_map<Node, DeltaRational, NodeHashFunction> NodeToMinMaxMap; @@ -52,7 +66,7 @@ private: NodeToMinMaxMap d_maxMap; public: - ArithStaticLearner(); + ArithStaticLearner(SubstitutionMap& pbSubstitutions); void staticLearning(TNode n, NodeBuilder<>& learned); void addBound(TNode n); @@ -64,11 +78,14 @@ private: void postProcess(NodeBuilder<>& learned); + void replaceWithPseudoboolean(TNode var); void iteMinMax(TNode n, NodeBuilder<>& learned); void iteConstant(TNode n, NodeBuilder<>& learned); void miplibTrick(TNode var, std::set<Rational>& values, NodeBuilder<>& learned); + void checkBoundsForPseudobooleanReplacement(TNode n); + /** These fields are designed to be accessable to ArithStaticLearner methods. */ class Statistics { public: diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index 78b77eb00..2dee26be4 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -143,7 +143,7 @@ inline bool evaluateConstantPredicate(Kind k, const Rational& left, const Ration } /** - * Returns the appropraite coefficient for the infinitesimal given the kind + * Returns the appropriate coefficient for the infinitesimal given the kind * for an arithmetic atom inorder to represent strict inequalities as inequalities. * x < c becomes x <= c + (-1) * \delta * x > c becomes x >= x + ( 1) * \delta diff --git a/src/theory/arith/arithvar_node_map.h b/src/theory/arith/arithvar_node_map.h index aca61878d..df82fde91 100644 --- a/src/theory/arith/arithvar_node_map.h +++ b/src/theory/arith/arithvar_node_map.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file arithvar_node_map.h + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "cvc4_private.h" #ifndef __CVC4__THEORY__ARITH__ARITHVAR_NODE_MAP_H diff --git a/src/theory/arith/arithvar_set.h b/src/theory/arith/arithvar_set.h index f8a23fee0..68937acc4 100644 --- a/src/theory/arith/arithvar_set.h +++ b/src/theory/arith/arithvar_set.h @@ -2,10 +2,10 @@ /*! \file arithvar_set.h ** \verbatim ** Original author: taking - ** Major contributors: mdeters + ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing @@ -17,13 +17,14 @@ ** \todo document this file **/ -#include <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 { @@ -33,7 +34,7 @@ namespace arith { * This class is designed to provide constant time insertion, deletion, and element_of * and fast iteration. * - * ArithVarSets come in 2 varieties ArithVarSet, and PermissiveBackArithVarSet. + * ArithVarSets come in 2 varieties: ArithVarSet, and PermissiveBackArithVarSet. * The default ArithVarSet assumes that there is no knowledge assumed about ArithVars * that are greater than allocated(). Asking isMember() of such an ArithVar * is an assertion failure. The cost of doing this is that it takes O(M) @@ -324,8 +325,8 @@ public: } }; -}; /* namespace arith */ -}; /* namespace theory */ -}; /* namespace CVC4 */ +}/* CVC4::theory::arith namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ #endif /* __CVC4__THEORY__ARITH__ARTIHVAR_SET_H */ diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp new file mode 100644 index 000000000..151859f21 --- /dev/null +++ b/src/theory/arith/dio_solver.cpp @@ -0,0 +1,118 @@ +/********************* */ +/*! \file dio_solver.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Diophantine equation solver + ** + ** A Diophantine equation solver for the theory of arithmetic. + **/ + +#include "theory/arith/dio_solver.h" + +#include <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 */ diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h new file mode 100644 index 000000000..c91ddd994 --- /dev/null +++ b/src/theory/arith/dio_solver.h @@ -0,0 +1,72 @@ +/********************* */ +/*! \file dio_solver.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Diophantine equation solver + ** + ** A Diophantine equation solver for the theory of arithmetic. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__ARITH__DIO_SOLVER_H +#define __CVC4__THEORY__ARITH__DIO_SOLVER_H + +#include "context/context.h" + +#include "theory/arith/tableau.h" +#include "theory/arith/partial_model.h" +#include "theory/arith/arith_utilities.h" +#include "util/rational.h" + +#include <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 */ diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index 1871e897a..db47062bb 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -30,18 +30,28 @@ sort INTEGER_TYPE \ "NodeManager::currentNM()->mkConst(Integer(0))" \ "expr/node_manager.h" \ "Integer type" +sort PSEUDOBOOLEAN_TYPE \ + 2 \ + well-founded \ + "NodeManager::currentNM()->mkConst(Pseudoboolean(0))" \ + "expr/node_manager.h" \ + "Pseudoboolean type" constant CONST_RATIONAL \ ::CVC4::Rational \ ::CVC4::RationalHashStrategy \ "util/rational.h" \ "a multiple-precision rational constant" - constant CONST_INTEGER \ ::CVC4::Integer \ ::CVC4::IntegerHashStrategy \ "util/integer.h" \ "a multiple-precision integer constant" +constant CONST_PSEUDOBOOLEAN \ + ::CVC4::Pseudoboolean \ + ::CVC4::PseudobooleanHashStrategy \ + "util/pseudoboolean.h" \ + "a pseudoboolean constant" operator LT 2 "less than, x < y" operator LEQ 2 "less than or equal, x <= y" diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp index aea1a43d8..b529a8077 100644 --- a/src/theory/arith/normal_form.cpp +++ b/src/theory/arith/normal_form.cpp @@ -254,6 +254,58 @@ Comparison Comparison::parseNormalForm(TNode n) { } } +bool Comparison::pbComparison(Kind k, TNode left, const Rational& right, bool& result) { + AssertArgument(left.getType().isPseudoboolean(), left); + switch(k) { + case kind::LT: + if(right > 1) { + result = true; + return true; + } else if(right <= 0) { + result = false; + return true; + } + break; + case kind::LEQ: + if(right >= 1) { + result = true; + return true; + } else if(right < 0) { + result = false; + return true; + } + break; + case kind::EQUAL: + if(right != 0 && right != 1) { + result = false; + return true; + } + break; + case kind::GEQ: + if(right > 1) { + result = false; + return true; + } else if(right <= 0) { + result = true; + return true; + } + break; + case kind::GT: + if(right >= 1) { + result = false; + return true; + } else if(right < 0) { + result = true; + return true; + } + break; + default: + CheckArgument(false, k, "Bad comparison operator ?!"); + } + + return false; +} + Comparison Comparison::mkComparison(Kind k, const Polynomial& left, const Constant& right) { Assert(isRelationOperator(k)); if(left.isConstant()) { @@ -261,9 +313,16 @@ Comparison Comparison::mkComparison(Kind k, const Polynomial& left, const Consta const Rational& rConst = right.getNode().getConst<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 { diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h index 5d6ca27e9..d6e79318d 100644 --- a/src/theory/arith/normal_form.h +++ b/src/theory/arith/normal_form.h @@ -702,6 +702,22 @@ private: Comparison(TNode n, Kind k, const Polynomial& l, const Constant& r): NodeWrapper(n), oper(k), left(l), right(r) { } + + /** + * Possibly simplify a comparison with a pseudoboolean-typed LHS. k + * is one of LT, LEQ, EQUAL, GEQ, GT, and left must be PB-typed. If + * possible, "left k right" is fully evaluated, "true" is returned, + * and the result of the evaluation is returned in "result". If no + * evaluation is possible, false is returned and "result" is + * untouched. + * + * For example, pbComparison(kind::EQUAL, "x", 0.5, result) returns + * true, and updates "result" to false, since pseudoboolean variable + * "x" can never equal 0.5. pbComparison(kind::GEQ, "x", 1, result) + * returns false, since "x" can be >= 1, but could also be less. + */ + static bool pbComparison(Kind k, TNode left, const Rational& right, bool& result); + public: Comparison(bool val) : NodeWrapper(NodeManager::currentNM()->mkConst(val)), diff --git a/src/theory/arith/ordered_set.h b/src/theory/arith/ordered_set.h index 43ccd7815..e44ba8687 100644 --- a/src/theory/arith/ordered_set.h +++ b/src/theory/arith/ordered_set.h @@ -53,14 +53,18 @@ public: void addLeq(TNode leq){ Assert(leq.getKind() == kind::LEQ); Assert(rightHandRational(leq) == getValue()); - Assert(!hasLeq()); + // [MGD] With context-dependent pre-registration, we could get the + // same one twice + Assert(!hasLeq() || d_leq == leq); d_leq = leq; } void addGeq(TNode geq){ Assert(geq.getKind() == kind::GEQ); Assert(rightHandRational(geq) == getValue()); - Assert(!hasGeq()); + // [MGD] With context-dependent pre-registration, we could get the + // same one twice + Assert(!hasGeq() || d_geq == geq); d_geq = geq; } diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h index 171c74942..f07e524aa 100644 --- a/src/theory/arith/partial_model.h +++ b/src/theory/arith/partial_model.h @@ -86,7 +86,7 @@ public: /* Initializes a variable to a safe value.*/ void initialize(ArithVar x, const DeltaRational& r); - /* Gets the last assignment to a variable that is known to be conistent. */ + /* Gets the last assignment to a variable that is known to be consistent. */ const DeltaRational& getSafeAssignment(ArithVar x) const; const DeltaRational& getAssignment(ArithVar x, bool safe) const; @@ -183,14 +183,12 @@ private: return 0 <= x && x < d_mapSize; } -}; +};/* class ArithPartialModel */ - - -}; /* namesapce arith */ -}; /* namespace theory */ -}; /* namespace CVC4 */ +}/* CVC4::theory::arith namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp index 367e90301..b432416bd 100644 --- a/src/theory/arith/tableau.cpp +++ b/src/theory/arith/tableau.cpp @@ -115,7 +115,7 @@ void Tableau::setColumnUnused(ArithVar v){ ++colIter; } } -void Tableau::printTableau(){ +void Tableau::printTableau() const { Debug("tableau") << "Tableau::d_activeRows" << endl; ArithVarSet::const_iterator basicIter = beginBasic(), endIter = endBasic(); @@ -125,7 +125,7 @@ void Tableau::printTableau(){ } } -void Tableau::printRow(ArithVar basic){ +void Tableau::printRow(ArithVar basic) const { Debug("tableau") << "{" << basic << ":"; for(RowIterator entryIter = rowIterator(basic); !entryIter.atEnd(); ++entryIter){ const TableauEntry& entry = *entryIter; @@ -135,7 +135,7 @@ void Tableau::printRow(ArithVar basic){ Debug("tableau") << "}" << endl; } -void Tableau::printEntry(const TableauEntry& entry){ +void Tableau::printEntry(const TableauEntry& entry) const { Debug("tableau") << entry.getColVar() << "*" << entry.getCoefficient(); } diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index fa227757a..e14436f8c 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -224,10 +224,10 @@ private: class Iterator { private: EntryID d_curr; - TableauEntryManager& d_entryManager; + const TableauEntryManager& d_entryManager; public: - Iterator(EntryID start, TableauEntryManager& manager) : + Iterator(EntryID start, const TableauEntryManager& manager) : d_curr(start), d_entryManager(manager) {} @@ -244,7 +244,7 @@ private: Iterator& operator++(){ Assert(!atEnd()); - TableauEntry& entry = d_entryManager.get(d_curr); + const TableauEntry& entry = d_entryManager.get(d_curr); d_curr = isRowIterator ? entry.getNextRowID() : entry.getNextColID(); return *this; } @@ -288,13 +288,13 @@ public: return d_basicVariables.end(); } - RowIterator rowIterator(ArithVar v){ + RowIterator rowIterator(ArithVar v) const { Assert(v < d_rowHeads.size()); EntryID head = d_rowHeads[v]; return RowIterator(head, d_entryManager); } - ColIterator colIterator(ArithVar v){ + ColIterator colIterator(ArithVar v) const { Assert(v < d_colHeads.size()); EntryID head = d_colHeads[v]; return ColIterator(head, d_entryManager); @@ -350,9 +350,9 @@ public: /** * Prints the contents of the Tableau to Debug("tableau::print") */ - void printTableau(); - void printRow(ArithVar basic); - void printEntry(const TableauEntry& entry); + void printTableau() const; + void printRow(ArithVar basic) const; + void printEntry(const TableauEntry& entry) const; private: diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 3831536e9..2664aaac3 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -61,10 +61,13 @@ typedef expr::Attribute<SlackAttrID, bool> Slack; TheoryArith::TheoryArith(context::Context* c, OutputChannel& out, Valuation valuation) : Theory(THEORY_ARITH, c, out, valuation), + learner(d_pbSubstitutions), + d_nextIntegerCheckVar(0), d_partialModel(c), d_userVariables(), d_diseq(c), d_tableau(), + d_diosolver(c, d_tableau, d_partialModel), d_restartsCounter(0), d_rowHasBeenAdded(false), d_tableauResetDensity(1.6), @@ -131,13 +134,26 @@ TheoryArith::Statistics::~Statistics(){ } Node TheoryArith::preprocess(TNode atom) { - if (atom.getKind() == kind::EQUAL) { - Node leq = NodeBuilder<2>(kind::LEQ) << atom[0] << atom[1]; - Node geq = NodeBuilder<2>(kind::GEQ) << atom[0] << atom[1]; - return Rewriter::rewrite(leq.andNode(geq)); - } else { - return atom; + Debug("arith::preprocess") << "arith::preprocess() : " << atom << endl; + + Node a = d_pbSubstitutions.apply(atom); + + if (a != atom) { + Debug("pb") << "arith::preprocess() : after pb substitutions: " << a << endl; + a = Rewriter::rewrite(a); + Debug("pb") << "arith::preprocess() : after pb substitutions and rewriting: " << a << endl; + Debug("arith::preprocess") << "arith::preprocess() : after pb substitutions and rewriting: " << a << endl; + } + + if (a.getKind() == kind::EQUAL) { + Node leq = NodeBuilder<2>(kind::LEQ) << a[0] << a[1]; + Node geq = NodeBuilder<2>(kind::GEQ) << a[0] << a[1]; + Node rewritten = Rewriter::rewrite(leq.andNode(geq)); + Debug("arith::preprocess") << "arith::preprocess() : returning " << rewritten << endl; + return rewritten; } + + return a; } Theory::SolveStatus TheoryArith::solve(TNode in, SubstitutionMap& outSubstitutions) { @@ -187,8 +203,16 @@ Theory::SolveStatus TheoryArith::solve(TNode in, SubstitutionMap& outSubstitutio // Add the substitution if not recursive Node rewritten = Rewriter::rewrite(eliminateVar); if (!rewritten.hasSubterm(minVar)) { - outSubstitutions.addSubstitution(minVar, Rewriter::rewrite(eliminateVar)); - return SOLVE_STATUS_SOLVED; + Node elim = Rewriter::rewrite(eliminateVar); + if (!minVar.getType().isInteger() || elim.getType().isInteger()) { + // cannot eliminate integers here unless we know the resulting + // substitution is integral + Debug("simplify") << "TheoryArith::solve(): substitution " << minVar << " |-> " << elim << endl; + outSubstitutions.addSubstitution(minVar, elim); + return SOLVE_STATUS_SOLVED; + } else { + Debug("simplify") << "TheoryArith::solve(): can't substitute b/c it's integer: " << minVar << ":" << minVar.getType() << " |-> " << elim << ":" << elim.getType() << endl; + } } } } @@ -199,7 +223,7 @@ Theory::SolveStatus TheoryArith::solve(TNode in, SubstitutionMap& outSubstitutio case kind::LT: case kind::GEQ: case kind::GT: - if (in[0].getKind() == kind::VARIABLE) { + if (in[0].getMetaKind() == kind::metakind::VARIABLE) { learner.addBound(in); } break; @@ -290,16 +314,19 @@ void TheoryArith::preRegisterTerm(TNode n) { } } } - Debug("arith_preregister") << "end arith::preRegisterTerm("<< n <<")"<< endl; + Debug("arith_preregister") << "end arith::preRegisterTerm(" << n <<")" << endl; } ArithVar TheoryArith::requestArithVar(TNode x, bool basic){ Assert(isLeaf(x) || x.getKind() == PLUS); Assert(!d_arithvarNodeMap.hasArithVar(x)); + Assert(x.getType().isReal());// real or integer ArithVar varX = d_variables.size(); d_variables.push_back(Node(x)); + Debug("integers") << "isInteger[[" << x << "]]: " << x.getType().isInteger() << endl; + d_integerVars.push_back(x.getType().isPseudoboolean() ? 2 : (x.getType().isInteger() ? 1 : 0)); d_simplex.increaseMax(); @@ -570,6 +597,129 @@ void TheoryArith::check(Effort effortLevel){ } } + if(fullEffort(effortLevel) && d_integerVars.size() > 0) { + const ArithVar rrEnd = d_nextIntegerCheckVar; + do { + ArithVar v = d_nextIntegerCheckVar; + short type = d_integerVars[v]; + if(type > 0) { // integer + const DeltaRational& d = d_partialModel.getAssignment(v); + const Rational& r = d.getNoninfinitesimalPart(); + const Rational& i = d.getInfinitesimalPart(); + Trace("integers") << "integers: assignment to [[" << d_arithvarNodeMap.asNode(v) << "]] is " << r << "[" << i << "]" << endl; + if(type == 2) { + // pseudoboolean + if(r.getDenominator() == 1 && i.getNumerator() == 0 && + (r.getNumerator() == 0 || r.getNumerator() == 1)) { + // already pseudoboolean; skip + continue; + } + + TNode var = d_arithvarNodeMap.asNode(v); + Node zero = NodeManager::currentNM()->mkConst(Integer(0)); + Node one = NodeManager::currentNM()->mkConst(Integer(1)); + Node eq0 = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL, var, zero)); + Node eq1 = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL, var, one)); + Node lem = NodeManager::currentNM()->mkNode(kind::OR, eq0, eq1); + Trace("pb") << "pseudobooleans: branch & bound: " << lem << endl; + Trace("integers") << "pseudobooleans: branch & bound: " << lem << endl; + //d_out->lemma(lem); + } + if(r.getDenominator() == 1 && i.getNumerator() == 0) { + // already an integer assignment; skip + continue; + } + + // otherwise, try the Diophantine equation solver + //bool result = d_diosolver.solve(); + //Debug("integers") << "the dio solver returned " << (result ? "true" : "false") << endl; + + // branch and bound + if(r.getDenominator() == 1) { + // r is an integer, but the infinitesimal might not be + if(i.getNumerator() < 0) { + // lemma: v <= r - 1 || v >= r + + TNode var = d_arithvarNodeMap.asNode(v); + Node nrMinus1 = NodeManager::currentNM()->mkConst(r - 1); + Node nr = NodeManager::currentNM()->mkConst(r); + Node leq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::LEQ, var, nrMinus1)); + Node geq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::GEQ, var, nr)); + + Node lem = NodeManager::currentNM()->mkNode(kind::OR, leq, geq); + Trace("integers") << "integers: branch & bound: " << lem << endl; + if(d_valuation.isSatLiteral(lem[0])) { + Debug("integers") << " " << lem[0] << " == " << d_valuation.getSatValue(lem[0]) << endl; + } else { + Debug("integers") << " " << lem[0] << " is not assigned a SAT literal" << endl; + } + if(d_valuation.isSatLiteral(lem[1])) { + Debug("integers") << " " << lem[1] << " == " << d_valuation.getSatValue(lem[1]) << endl; + } else { + Debug("integers") << " " << lem[1] << " is not assigned a SAT literal" << endl; + } + d_out->lemma(lem); + + // split only on one var + break; + } else if(i.getNumerator() > 0) { + // lemma: v <= r || v >= r + 1 + + TNode var = d_arithvarNodeMap.asNode(v); + Node nr = NodeManager::currentNM()->mkConst(r); + Node nrPlus1 = NodeManager::currentNM()->mkConst(r + 1); + Node leq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::LEQ, var, nr)); + Node geq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::GEQ, var, nrPlus1)); + + Node lem = NodeManager::currentNM()->mkNode(kind::OR, leq, geq); + Trace("integers") << "integers: branch & bound: " << lem << endl; + if(d_valuation.isSatLiteral(lem[0])) { + Debug("integers") << " " << lem[0] << " == " << d_valuation.getSatValue(lem[0]) << endl; + } else { + Debug("integers") << " " << lem[0] << " is not assigned a SAT literal" << endl; + } + if(d_valuation.isSatLiteral(lem[1])) { + Debug("integers") << " " << lem[1] << " == " << d_valuation.getSatValue(lem[1]) << endl; + } else { + Debug("integers") << " " << lem[1] << " is not assigned a SAT literal" << endl; + } + d_out->lemma(lem); + + // split only on one var + break; + } else { + Unreachable(); + } + } else { + // lemma: v <= floor(r) || v >= ceil(r) + + TNode var = d_arithvarNodeMap.asNode(v); + Node floor = NodeManager::currentNM()->mkConst(r.floor()); + Node ceiling = NodeManager::currentNM()->mkConst(r.ceiling()); + Node leq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::LEQ, var, floor)); + Node geq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::GEQ, var, ceiling)); + + Node lem = NodeManager::currentNM()->mkNode(kind::OR, leq, geq); + Trace("integers") << "integers: branch & bound: " << lem << endl; + if(d_valuation.isSatLiteral(lem[0])) { + Debug("integers") << " " << lem[0] << " == " << d_valuation.getSatValue(lem[0]) << endl; + } else { + Debug("integers") << " " << lem[0] << " is not assigned a SAT literal" << endl; + } + if(d_valuation.isSatLiteral(lem[1])) { + Debug("integers") << " " << lem[1] << " == " << d_valuation.getSatValue(lem[1]) << endl; + } else { + Debug("integers") << " " << lem[1] << " is not assigned a SAT literal" << endl; + } + d_out->lemma(lem); + + // split only on one var + break; + } + }// if(arithvar is integer-typed) + } while((d_nextIntegerCheckVar = (1 + d_nextIntegerCheckVar == d_variables.size() ? 0 : 1 + d_nextIntegerCheckVar)) != rrEnd); + }// if(full effort) + if(Debug.isOn("paranoid:check_tableau")){ d_simplex.debugCheckTableau(); } if(Debug.isOn("arith::print_model")) { debugPrintModel(); } Debug("arith") << "TheoryArith::check end" << std::endl; @@ -866,7 +1016,9 @@ void TheoryArith::presolve(){ for(VarIter i = d_variables.begin(), end = d_variables.end(); i != end; ++i){ Node variableNode = *i; ArithVar var = d_arithvarNodeMap.asArithVar(variableNode); - if(d_userVariables.isMember(var) && !d_atomDatabase.hasAnyAtoms(variableNode)){ + if(d_userVariables.isMember(var) && + !d_atomDatabase.hasAnyAtoms(variableNode) && + !variableNode.getType().isInteger()){ //The user variable is unconstrained. //Remove this variable permanently permanentlyRemoveVariable(var); diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 0c15c824c..7e14f6b06 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -38,6 +38,7 @@ #include "theory/arith/arith_static_learner.h" #include "theory/arith/arith_prop_manager.h" #include "theory/arith/arithvar_node_map.h" +#include "theory/arith/dio_solver.h" #include "util/stats.h" @@ -69,6 +70,21 @@ private: 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 * can be used to determine the value of n using getValue(). @@ -86,8 +102,6 @@ private: */ ArithVarSet d_userVariables; - - /** * List of all of the inequalities asserted in the current context. */ @@ -98,6 +112,23 @@ private: */ Tableau d_tableau; + /** + * A Diophantine equation solver. Accesses the tableau and partial + * model (each in a read-only fashion). + */ + DioSolver d_diosolver; + + /** + * Some integer variables can be replaced with pseudoboolean + * variables internally. This map is built up at static learning + * time for top-level asserted expressions of the shape "x = 0 OR x + * = 1". This substitution map is then applied in preprocess(). + * + * Note that expressions of the shape "x >= 0 AND x <= 1" are + * already substituted for PB versions at solve() time and won't + * appear here. + */ + SubstitutionMap d_pbSubstitutions; /** Counts the number of notifyRestart() calls to the theory. */ uint32_t d_restartsCounter; diff --git a/src/theory/booleans/theory_bool_type_rules.h b/src/theory/booleans/theory_bool_type_rules.h index 70b53a930..09030d331 100644 --- a/src/theory/booleans/theory_bool_type_rules.h +++ b/src/theory/booleans/theory_bool_type_rules.h @@ -34,7 +34,10 @@ public: TNode::iterator child_it = n.begin(); TNode::iterator child_it_end = n.end(); for(; child_it != child_it_end; ++child_it) { - if((*child_it).getType(check) != booleanType) { + if(!(*child_it).getType(check).isBoolean()) { + Debug("pb") << "failed type checking: " << *child_it << std::endl; + Debug("pb") << " integer: " << (*child_it).getType(check).isInteger() << std::endl; + Debug("pb") << " real: " << (*child_it).getType(check).isReal() << std::endl; throw TypeCheckingExceptionPrivate(n, "expecting a Boolean subexpression"); } } diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index f343848d8..3bfb7fdc5 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -90,7 +90,7 @@ class EqualityTypeRule { throw TypeCheckingExceptionPrivate(n, ss.str()); } - if ( lhsType == booleanType ) { + if ( lhsType == booleanType && rhsType == booleanType ) { throw TypeCheckingExceptionPrivate(n, "equality between two boolean terms (use IFF instead)"); } } diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index 44aed8b17..d82e628c1 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -92,7 +92,7 @@ public: * @param safe - whether it is safe to be interrupted */ virtual void lemma(TNode n, bool safe = false) - throw(Interrupted, AssertionException) = 0; + throw(Interrupted, TypeCheckingExceptionPrivate, AssertionException) = 0; /** * Request a split on a new theory atom. This is equivalent to diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp index 8657ed871..76551bc18 100644 --- a/src/theory/substitutions.cpp +++ b/src/theory/substitutions.cpp @@ -161,5 +161,5 @@ void SubstitutionMap::print(ostream& out) const { } } -} -} +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h index 513300a32..f59c17dc0 100644 --- a/src/theory/substitutions.h +++ b/src/theory/substitutions.h @@ -23,6 +23,7 @@ #include <utility> #include <vector> +#include <algorithm> #include "expr/node.h" namespace CVC4 { @@ -77,6 +78,25 @@ public: } /** + * 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 */ void print(std::ostream& out) const; diff --git a/src/theory/theory.h b/src/theory/theory.h index d859c60d8..62a8cb4d6 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -442,8 +442,10 @@ public: } /** - * Given an atom of the theory, that comes from the input formula, this is method can rewrite the atom - * into an equivalent form. This is only called just before an input atom to the engine. + * Given an atom of the theory coming from the input formula, this + * method can be overridden in a theory implementation to rewrite + * the atom into an equivalent form. This is only called just + * before an input atom to the engine. */ virtual Node preprocess(TNode atom) { return atom; } diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 662a4925a..2107bcb66 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -149,7 +149,7 @@ class TheoryEngine { } void lemma(TNode node, bool removable = false) - throw(theory::Interrupted, AssertionException) { + throw(theory::Interrupted, TypeCheckingExceptionPrivate, AssertionException) { Trace("theory") << "EngineOutputChannel::lemma(" << node << ")" << std::endl; ++(d_engine->d_statistics.d_statLemma); diff --git a/src/util/Makefile.am b/src/util/Makefile.am index ce13f011d..61ff27c08 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -62,6 +62,8 @@ libutil_la_SOURCES = \ boolean_simplification.cpp \ ite_removal.h \ ite_removal.cpp \ + pseudoboolean.h \ + pseudoboolean.cpp \ node_visitor.h libutil_la_LIBADD = \ diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h index 8c3fc14e5..664027cdc 100644 --- a/src/util/integer_cln_imp.h +++ b/src/util/integer_cln_imp.h @@ -182,7 +182,8 @@ public: return *this; } - /** Raise this Integer to the power <code>exp</code>. + /** + * Raise this Integer to the power <code>exp</code>. * * @param exp the exponent */ @@ -197,6 +198,21 @@ public: } } + /** + * Return the greatest common divisor of this integer with another. + */ + Integer gcd(const Integer& y) const { + cln::cl_I result = cln::gcd(d_value, y.d_value); + return Integer(result); + } + + /** + * Return the absolute value of this integer. + */ + Integer abs() const { + return d_value >= 0 ? *this : -*this; + } + std::string toString(int base = 10) const{ std::stringstream ss; switch(base){ diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h index c1d46ca65..60cee3937 100644 --- a/src/util/integer_gmp_imp.h +++ b/src/util/integer_gmp_imp.h @@ -151,7 +151,8 @@ public: return *this; } - /** Raise this Integer to the power <code>exp</code>. + /** + * Raise this Integer to the power <code>exp</code>. * * @param exp the exponent */ @@ -161,6 +162,22 @@ public: return Integer( result ); } + /** + * Return the greatest common divisor of this integer with another. + */ + Integer gcd(const Integer& y) const { + mpz_class result; + mpz_gcd(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t()); + return Integer(result); + } + + /** + * Return the absolute value of this integer. + */ + Integer abs() const { + return d_value >= 0 ? *this : -*this; + } + std::string toString(int base = 10) const{ return d_value.get_str(base); } diff --git a/src/util/pseudoboolean.cpp b/src/util/pseudoboolean.cpp new file mode 100644 index 000000000..3fa7a774e --- /dev/null +++ b/src/util/pseudoboolean.cpp @@ -0,0 +1,49 @@ +/********************* */ +/*! \file pseudoboolean.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute &of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief A pseudoboolean constant + ** + ** A pseudoboolean constant. + **/ + +#include "util/pseudoboolean.h" + +namespace CVC4 { + +Pseudoboolean::Pseudoboolean(bool b) : + d_value(b) { +} + +Pseudoboolean::Pseudoboolean(int i) { + CheckArgument(i == 0 || i == 1, i); + d_value = (i == 1); +} + +Pseudoboolean::Pseudoboolean(const Integer& i) { + CheckArgument(i == 0 || i == 1, i); + d_value = (i == 1); +} + +Pseudoboolean::operator bool() const { + return d_value; +} + +Pseudoboolean::operator int() const { + return d_value ? 1 : 0; +} + +Pseudoboolean::operator Integer() const { + return d_value ? 1 : 0; +} + +}/* CVC4 namespace */ diff --git a/src/util/pseudoboolean.h b/src/util/pseudoboolean.h new file mode 100644 index 000000000..6d0d4fd26 --- /dev/null +++ b/src/util/pseudoboolean.h @@ -0,0 +1,54 @@ +/********************* */ +/*! \file pseudoboolean.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief A pseudoboolean constant + ** + ** A pseudoboolean constant. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__PSEUDOBOOLEAN_H +#define __CVC4__PSEUDOBOOLEAN_H + +#include "util/integer.h" + +namespace CVC4 { + +class Pseudoboolean { + bool d_value; + +public: + Pseudoboolean(bool b); + Pseudoboolean(int i); + Pseudoboolean(const Integer& i); + + operator bool() const; + operator int() const; + operator Integer() const; + +};/* class Pseudoboolean */ + +struct PseudobooleanHashStrategy { + static inline size_t hash(CVC4::Pseudoboolean pb) { + return int(pb); + } +};/* struct PseudobooleanHashStrategy */ + +inline std::ostream& operator<<(std::ostream& os, CVC4::Pseudoboolean pb) { + return os << int(pb); +} + +}/* CVC4 namespace */ + +#endif /* __CVC4__PSEUDOBOOLEAN_H */ diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h index c05d47175..b97484ff1 100644 --- a/src/util/rational_cln_imp.h +++ b/src/util/rational_cln_imp.h @@ -192,6 +192,14 @@ public: } } + Integer floor() const { + return Integer(cln::floor1(d_value)); + } + + Integer ceiling() const { + return Integer(cln::ceiling1(d_value)); + } + Rational& operator=(const Rational& x){ if(this == &x) return *this; d_value = x.d_value; @@ -226,9 +234,6 @@ public: return d_value >= y.d_value; } - - - Rational operator+(const Rational& y) const{ return Rational( d_value + y.d_value ); } diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h index 7af1b86df..167e0fc22 100644 --- a/src/util/rational_gmp_imp.h +++ b/src/util/rational_gmp_imp.h @@ -151,7 +151,7 @@ public: * Returns the value of denominator of the Rational. * Note that this makes a deep copy of the denominator. */ - Integer getDenominator() const{ + Integer getDenominator() const { return Integer(d_value.get_den()); } @@ -165,11 +165,22 @@ public: return mpq_cmp(d_value.get_mpq_t(), x.d_value.get_mpq_t()); } - int sgn() const { return mpq_sgn(d_value.get_mpq_t()); } + Integer floor() const { + mpz_class q; + mpz_fdiv_q(q.get_mpz_t(), d_value.get_num_mpz_t(), d_value.get_den_mpz_t()); + return Integer(q); + } + + Integer ceiling() const { + mpz_class q; + mpz_cdiv_q(q.get_mpz_t(), d_value.get_num_mpz_t(), d_value.get_den_mpz_t()); + return Integer(q); + } + Rational& operator=(const Rational& x){ if(this == &x) return *this; d_value = x.d_value; @@ -204,9 +215,6 @@ public: return d_value >= y.d_value; } - - - Rational operator+(const Rational& y) const{ return Rational( d_value + y.d_value ); } |