diff options
Diffstat (limited to 'src/preprocessing/passes/miplib_trick.cpp')
| -rw-r--r-- | src/preprocessing/passes/miplib_trick.cpp | 20 |
1 files changed, 12 insertions, 8 deletions
diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp index 59f046262..66646b766 100644 --- a/src/preprocessing/passes/miplib_trick.cpp +++ b/src/preprocessing/passes/miplib_trick.cpp @@ -33,13 +33,14 @@ #include "theory/trust_substitutions.h" #include "util/rational.h" +using namespace std; +using namespace cvc5::kind; +using namespace cvc5::theory; + namespace cvc5 { namespace preprocessing { namespace passes { -using namespace std; -using namespace cvc5::theory; - namespace { /** @@ -212,7 +213,8 @@ PreprocessingPassResult MipLibTrick::applyInternal( NodeManager* nm = NodeManager::currentNM(); SkolemManager* sm = nm->getSkolemManager(); - Node zero = nm->mkConst(Rational(0)), one = nm->mkConst(Rational(1)); + Node zero = nm->mkConst(CONST_RATIONAL, Rational(0)), + one = nm->mkConst(CONST_RATIONAL, Rational(1)); Node trueNode = nm->mkConst(true); unordered_map<TNode, Node> intVars; @@ -571,15 +573,17 @@ PreprocessingPassResult MipLibTrick::applyInternal( NodeBuilder sumb(kind::PLUS); for (size_t jj = 0; jj < pos.getNumChildren(); ++jj) { - sumb << nm->mkNode( - kind::MULT, nm->mkConst(coef[pos_var][jj]), newVars[jj]); + sumb << nm->mkNode(kind::MULT, + nm->mkConst(CONST_RATIONAL, coef[pos_var][jj]), + newVars[jj]); } sum = sumb; } else { - sum = nm->mkNode( - kind::MULT, nm->mkConst(coef[pos_var][0]), newVars[0]); + sum = nm->mkNode(kind::MULT, + nm->mkConst(CONST_RATIONAL, coef[pos_var][0]), + newVars[0]); } Debug("miplib") << "vars[] " << var << endl << " eq " << rewrite(sum) << endl; |