diff options
Diffstat (limited to 'src/theory/arith/dio_solver.cpp')
-rw-r--r-- | src/theory/arith/dio_solver.cpp | 118 |
1 files changed, 118 insertions, 0 deletions
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 */ |