From d4dad039c98f7bf30d85f43b0530bdb2a91f294e Mon Sep 17 00:00:00 2001 From: Anna Vasenina Date: Sat, 15 Oct 2022 19:14:52 +0300 Subject: [PATCH 01/10] attempt to fix reals --- src/ae/AeValSolver.hpp | 3 - src/ae/ExprSimpl.hpp | 184 +++++++++++++++++++++----------------- src/ae/MBPUtils.cpp | 34 +------ src/ae/MBPUtils.hpp | 7 -- src/sygus/SyGuSSolver.hpp | 2 +- 5 files changed, 109 insertions(+), 121 deletions(-) diff --git a/src/ae/AeValSolver.hpp b/src/ae/AeValSolver.hpp index 9287cd61d..1c92d6a13 100644 --- a/src/ae/AeValSolver.hpp +++ b/src/ae/AeValSolver.hpp @@ -1267,9 +1267,6 @@ namespace ufo minusSets(ex_qvars, fa_qvars); } - s = convertIntsToReals
(s); - t = convertIntsToReals
(t); - if(debug >= 3) { outs() << "s part: " << s << "\n"; diff --git a/src/ae/ExprSimpl.hpp b/src/ae/ExprSimpl.hpp index 47a8da07c..0016248b8 100644 --- a/src/ae/ExprSimpl.hpp +++ b/src/ae/ExprSimpl.hpp @@ -2355,39 +2355,31 @@ namespace ufo return fla; } - template static Expr convertIntsToReals (Expr exp); + static Expr convertIntsToReals (Expr exp); - template struct IntToReal + struct IntToReal { - IntToReal () {}; + IntToReal () {}; Expr operator() (Expr exp) { - if (isOpX(exp)) + ExprVector args; + for (int i = 0; i < exp->arity(); i++) { - ExprVector args; - for (int i = 0; i < exp->arity(); i++) - { - Expr e = exp->arg(i); - if (isOpX(e)) - e = mkTerm (mpq_class (lexical_cast(e)), exp->getFactory()); - else { - e = convertIntsToReals(e); - e = convertIntsToReals(e); - e = convertIntsToReals(e); - e = convertIntsToReals(e); - } - args.push_back(e); - } - return mknary(args); + Expr e = exp->arg(i); + if (isOpX(e)) + e = mkTerm (mpq_class (lexical_cast(e)), exp->getFactory()); + // else if (bind::isIntConst(exp)) + // e = realConst(fname(exp)); + args.push_back(e); } - return exp; + return mknary(exp->op(), args.begin(), args.end()); } }; - template static Expr convertIntsToReals (Expr exp) + static Expr convertIntsToReals (Expr exp) { - RW> rw(new IntToReal()); + RW rw(new IntToReal()); return dagVisit (rw, exp); } @@ -4558,85 +4550,117 @@ namespace ufo return false; } - static void getLiterals (Expr exp, ExprSet& lits, bool splitEqs = true) + + + enum laType { + REALTYPE = 0, + INTTYPE, + MIXTYPE, + NOTYPE + }; + + /** + * intOrReal - checks expression type + */ + static int intOrReal(Expr s) + { + ExprVector sVec; + bool realType = false, intType = false; + filter(s, bind::IsNumber(), back_inserter(sVec)); + filter(s, bind::IsConst(), back_inserter(sVec)); + for(auto ite : sVec) + { + if(bind::isIntConst(ite) || isOpX(ite)) + intType = true; + else if(bind::isRealConst(ite) || isOpX(ite)) + realType = true; + } + + if(realType && intType) + return MIXTYPE; // a bad case + else if(realType) + return REALTYPE; + else if(intType) + return INTTYPE; + else + return NOTYPE; // unknown + } + + static Expr tryToRemoveMixType(Expr exp) + { + if (intOrReal(exp) != MIXTYPE) + return exp; + + return convertIntsToReals(exp); + } + + static void getLiterals (Expr exp, ExprSet& lits, bool splitEqs = true); + + static void getLiteralsBool(Expr exp, ExprSet& lits, bool splitEqs = true) { - ExprFactory& efac = exp->getFactory(); Expr el = exp->left(); Expr er = exp->right(); - if (isOp(exp) && !splitEqs) - { - if (isNumeric(el) || (isBoolConstOrNegation(el) && isBoolConstOrNegation(er))) + if (isOp(exp) && !splitEqs && isBoolConstOrNegation(el) && isBoolConstOrNegation(er)) { lits.insert(exp); - } - if (isOpX(exp) && isBoolean(er)) - { + } else if (isOpX(exp) || isOpX(exp) || isOpX(exp) || isOpX(exp)) { getLiterals(mkNeg(el), lits, splitEqs); getLiterals(er, lits, splitEqs); getLiterals(mkNeg(er), lits, splitEqs); getLiterals(el, lits, splitEqs); - } - if (isOpX(exp) && isNumeric(el) && !containsOp(exp)) - { - getLiterals(mk(el, er), lits, splitEqs); - getLiterals(mk(el, er), lits, splitEqs); - } - else if (isOpX(exp) && isNumeric(el) && !containsOp(exp)) - { - getLiterals(mk(el, er), lits, splitEqs); - getLiterals(mk(el, er), lits, splitEqs); - } - else if ((isOpX(exp) || isOpX(exp) || isOpX(exp)) && isBoolean(el)) - { - getLiterals(el, lits, splitEqs); - getLiterals(er, lits, splitEqs); - getLiterals(mkNeg(el), lits, splitEqs); - getLiterals(mkNeg(er), lits, splitEqs); - } - else if (isOpX(exp)) - { + } else if (isOpX(exp) || isOpX(exp)) { + for (int i = 0; i < exp->arity(); i++) + getLiterals(exp->arg(i), lits, splitEqs); + } else if (isOpX(exp)) { if (isBoolConst(el)) lits.insert(exp); else getLiterals(mkNeg(el), lits, splitEqs); - } - else if (isOpX(exp)) - { + } else if (isOpX(exp)) { getLiterals(mkNeg(el), lits, splitEqs); getLiterals(er, lits, splitEqs); } - else if (isOpX(exp)) - { - getLiterals(mkNeg(el), lits, splitEqs); - getLiterals(er, lits, splitEqs); - getLiterals(mkNeg(er), lits, splitEqs); - getLiterals(el, lits, splitEqs); - } - else if (bind::typeOf(exp) == mk(efac) && - !containsOp(exp) && !containsOp(exp)) - { - if (isOp(exp)) - { - exp = rewriteDivConstraints(exp); - exp = rewriteModConstraints(exp); - if (isOpX(exp) || isOpX(exp)) - getLiterals(exp, lits, splitEqs); - else lits.insert(exp); - } + } + + static void getLiteralsNumeric(Expr exp, ExprSet& lits, bool splitEqs = true) + { + exp = tryToRemoveMixType(exp); + Expr el = exp->left(); + Expr er = exp->right(); + if (isOp(exp) && !splitEqs) { + lits.insert(exp); + } else if (isOpX(exp) && !containsOp(exp)) { + getLiterals(mk(el, er), lits, splitEqs); + getLiterals(mk(el, er), lits, splitEqs); + } else if (isOpX(exp) && !containsOp(exp)) { + getLiterals(mk(el, er), lits, splitEqs); + getLiterals(mk(el, er), lits, splitEqs); + } else if (isOp(exp)) { + exp = rewriteDivConstraints(exp); + exp = rewriteModConstraints(exp); + if (isOpX(exp) || isOpX(exp)) + getLiterals(exp, lits, splitEqs); else lits.insert(exp); } - else if (isOpX(exp) || isOpX(exp)) - { - for (int i = 0; i < exp->arity(); i++) - getLiterals(exp->arg(i), lits, splitEqs); - } - else if (!isOpX(exp) && !isOpX(exp)) - { + } + + static void getLiterals (Expr exp, ExprSet& lits, bool splitEqs) + { + ExprFactory& efac = exp->getFactory(); + Expr el = exp->left(); + Expr er = exp->right(); + if (isOp(exp) || isOp(exp) && isBoolean(el)) + getLiteralsBool(exp, lits, splitEqs); + else if (isOp(exp) && isNumeric(el)) + getLiteralsNumeric(exp, lits, splitEqs); + else if (bind::typeOf(exp) == mk(efac) && + !containsOp(exp) && !containsOp(exp)) { + lits.insert(exp); + } else if (!isOpX(exp) && !isOpX(exp)) { errs () << "unable lit: " << *exp << "\n"; assert(0); } } - void pprint(Expr exp, int inden, bool upper); template static void pprint(Range& exprs, int inden = 0) @@ -4688,6 +4712,6 @@ namespace ufo } if (upper) outs() << "\n"; } -} +} #endif diff --git a/src/ae/MBPUtils.cpp b/src/ae/MBPUtils.cpp index 5816dac33..eddc6f175 100644 --- a/src/ae/MBPUtils.cpp +++ b/src/ae/MBPUtils.cpp @@ -3,35 +3,6 @@ using namespace ufo; -/** - * intOrReal - checks expression type - */ -int intOrReal(Expr s) -{ - ExprVector sVec; - bool realType = false, intType = false; - filter(s, bind::IsNumber(), back_inserter(sVec)); - filter(s, bind::IsConst(), back_inserter(sVec)); - for(auto ite : sVec) - { - if(bind::isIntConst(ite) || isOpX(ite)) - intType = true; - else if(bind::isRealConst(ite) || isOpX(ite)) - realType = true; - else - assert(false); // Error identifying - } - - if(realType && intType) - return MIXTYPE; // a bad case - else if(realType) - return REALTYPE; - else if(intType) - return INTTYPE; - else - return NOTYPE; // t == true -} - /** * laMergeBounds - merges lower and upper bounds * @@ -333,8 +304,11 @@ Expr ineqPrepare(Expr t, Expr eVar) else if(isInt(eVar) && (intVSreal == INTTYPE)) return t; else if(intVSreal != NOTYPE) + { + // t = tryToRemoveMixType(t); + outs() << "t = " << t << "\n" << "intOrReal: " <::Model &m, SMTUtils &u, int debug); - - enum laType { - REALTYPE = 0, - INTTYPE, - MIXTYPE, - NOTYPE - }; } #endif \ No newline at end of file diff --git a/src/sygus/SyGuSSolver.hpp b/src/sygus/SyGuSSolver.hpp index 4bc4335ea..d14f3202b 100644 --- a/src/sygus/SyGuSSolver.hpp +++ b/src/sygus/SyGuSSolver.hpp @@ -218,7 +218,7 @@ class SyGuSSolver faArgs.push_back(mknary(exArgs)); Expr aeProb = mknary(faArgs); aeProb = regularizeQF(aeProb); - aeProb = convertIntsToReals
(aeProb); + aeProb = tryToRemoveMixType(aeProb); if (debug > 1) { outs() << "Sending to aeval: "; u.print(aeProb); outs() << endl; } From fd5355c4b9777b0cde6218d577f2db02a9c63bd2 Mon Sep 17 00:00:00 2001 From: Anna Vasenina Date: Mon, 17 Oct 2022 14:37:27 +0300 Subject: [PATCH 02/10] fix --- src/ae/ExprSimpl.hpp | 8 ++++---- src/ae/MBPUtils.cpp | 6 ++++-- src/ufo/Expr.hpp | 5 +++++ 3 files changed, 13 insertions(+), 6 deletions(-) diff --git a/src/ae/ExprSimpl.hpp b/src/ae/ExprSimpl.hpp index 0016248b8..b8f6bea32 100644 --- a/src/ae/ExprSimpl.hpp +++ b/src/ae/ExprSimpl.hpp @@ -2369,8 +2369,8 @@ namespace ufo Expr e = exp->arg(i); if (isOpX(e)) e = mkTerm (mpq_class (lexical_cast(e)), exp->getFactory()); - // else if (bind::isIntConst(exp)) - // e = realConst(fname(exp)); + else if (bind::isIntConst(e)) + e = realConst(fname(e)); args.push_back(e); } return mknary(exp->op(), args.begin(), args.end()); @@ -4588,9 +4588,9 @@ namespace ufo static Expr tryToRemoveMixType(Expr exp) { - if (intOrReal(exp) != MIXTYPE) + if (intOrReal(exp) != MIXTYPE) return exp; - + return convertIntsToReals(exp); } diff --git a/src/ae/MBPUtils.cpp b/src/ae/MBPUtils.cpp index eddc6f175..f1c8b93ec 100644 --- a/src/ae/MBPUtils.cpp +++ b/src/ae/MBPUtils.cpp @@ -284,20 +284,22 @@ Expr intQE(ExprSet sSet, Expr eVar, ZSolver::Model &m) */ Expr ineqPrepare(Expr t, Expr eVar) { + int intVSreal = intOrReal(t); if(isOpX(t) && isOp(t->left())) t = mkNeg(t->left()); if(isOp(t)) { + Expr zero = intVSreal == REALTYPE ? mkMPQ("0", eVar->efac()) + : mkMPZ(0, eVar->efac()); // rewrite so that y is on lhs, with positive coef t = simplifyArithm(reBuildCmp( t, mk(t->arg(0), additiveInverse(t->arg(1))), - mkMPZ(0, eVar->efac()))); + zero)); t = ineqSimplifier(eVar, t); } else unreachable(); - int intVSreal = intOrReal(t); if(isReal(eVar) && (intVSreal == REALTYPE)) return t; diff --git a/src/ufo/Expr.hpp b/src/ufo/Expr.hpp index e4cc6cd2d..fd7a0093e 100644 --- a/src/ufo/Expr.hpp +++ b/src/ufo/Expr.hpp @@ -2350,6 +2350,11 @@ namespace expr return mkTerm (mpz_class (a), efac); } + static Expr mkMPQ(std::string a, ExprFactory& efac) + { + return mkTerm (mpq_class (a), efac); + } + struct FAPP_PS { static inline void print (std::ostream &OS, From 011a5d64f16194420deb6ab7a018f3d83aeb7dfa Mon Sep 17 00:00:00 2001 From: Anna Vasenina Date: Mon, 17 Oct 2022 15:37:33 +0300 Subject: [PATCH 03/10] Still not fixed --- src/ae/AeValSolver.hpp | 10 ++- src/ae/ExprSimpl.hpp | 134 ++++++++++++++++++++++++++++++++++++++++- src/ae/MBPUtils.cpp | 50 ++++++++++++--- 3 files changed, 180 insertions(+), 14 deletions(-) diff --git a/src/ae/AeValSolver.hpp b/src/ae/AeValSolver.hpp index 1c92d6a13..ef9d77858 100644 --- a/src/ae/AeValSolver.hpp +++ b/src/ae/AeValSolver.hpp @@ -173,13 +173,14 @@ namespace ufo { ExprSet lits; u.getTrueLiterals(pr, m, lits, true); + outs() << "Lits: { \n"; + for (auto a: lits) + outs() << a << "\n"; + outs() << "}\n"; pr = simplifyArithm(mixQE(conjoin(lits, efac), exp, m, u, debug)); if(m.eval(exp) != exp) modelMap[exp] = mk(exp, m.eval(exp)); - if(debug) - MBPSanityCheck(m, pr); - if(debug >= 2) { outs() << "\nmodel " << partitioning_size << ":\n"; @@ -200,6 +201,9 @@ namespace ufo pprint(pr, 2); } + if(debug) + MBPSanityCheck(m, pr); + for(auto it = lits.begin(); it != lits.end();) { if(contains(*it, exp)) diff --git a/src/ae/ExprSimpl.hpp b/src/ae/ExprSimpl.hpp index b8f6bea32..34ad2e20b 100644 --- a/src/ae/ExprSimpl.hpp +++ b/src/ae/ExprSimpl.hpp @@ -532,6 +532,8 @@ namespace ufo return e; } + static Expr realSimplifyMult(Expr fla); + /** * Helper used in ineqMover */ @@ -539,6 +541,8 @@ namespace ufo Expr l = e->left(); Expr r = e->right(); ExprVector orig_lhs, orig_rhs, lhs, rhs; + ExprVector realCoefs; + outs() << "rewriteHelperM e = " << e << "\n"; // parse @@ -568,6 +572,20 @@ namespace ufo coef -= lexical_cast(subExpr->left()); found = true; } + else if (isOpX(subExpr) && 2 == subExpr->arity() && isOpX(subExpr->left()) && subExpr->right() == var) { + ExprVector tmp; + int skipped = 0; + for (int i = 0; i < (*it)->arity(); ++i) + { + if (subExpr->arg(i) != var) + tmp.push_back(subExpr->arg(i)); + else + skipped++; + } + assert(skipped == 1); + realCoefs.push_back(mk(mkmult(tmp, var->efac()))); + found = true; + } else if (isOp(subExpr) && 2 == subExpr->arity() && isOpX(subExpr->right()) && subExpr->left() == var) { coef -= rational(1, lexical_cast(subExpr->right())); found = true; @@ -577,6 +595,20 @@ namespace ufo coef += lexical_cast((*it)->left()); found = true; } + else if (isOpX(*it) && isRealConst(var)) { + ExprVector tmp; + int skipped = 0; + for (int i = 0; i < (*it)->arity(); ++i) + { + if ((*it)->arg(i) != var) + tmp.push_back((*it)->arg(i)); + else + skipped++; + } + assert(skipped == 1); + realCoefs.push_back(mkmult(tmp, var->efac())); + found = true; + } if (isOp(*it) && 2 == (*it)->arity() && isOpX((*it)->right()) && (*it)->left() == var) { coef += rational(1, lexical_cast((*it)->right())); found = true; @@ -594,7 +626,13 @@ namespace ufo } r = mkplus(rhs, e->getFactory()); - + if (!realCoefs.empty()) + { + l = mkplus(realCoefs, var->efac()); + l = mk(l, var); + outs() << "transformed e: " << e << "to :" << mk(l,r); + return mk(l,r); + } if (coef == 0){ l = mkMPZ (0, e->getFactory()); } else if (coef == 1){ @@ -2213,6 +2251,100 @@ namespace ufo return typeOf(e) == mk(e->getFactory()); } + static Expr realRewriteDivs(Expr fla, Expr var) + { + assert (isOp(fla)); + ExprFactory& efac = var->efac(); + ExprVector plusOpsLeft; + ExprVector plusOpsRight; + int minusOps = 0; + + getAddTerm(fla->left(), plusOpsLeft); + getAddTerm(fla->right(), plusOpsRight); + + ExprSet divs; + for (auto a : plusOpsLeft) + if(isOpX
(a)) + { + divs.insert(a->right()); + if(lexical_cast(a->right())[0] == '-') + minusOps++; + } + for (auto a : plusOpsRight) + if(isOpX
(a)) + { + divs.insert(a->right()); + if(lexical_cast(a->right())[0] == '-') + minusOps++; + } + + for(auto ite = plusOpsLeft.begin(); ite != plusOpsLeft.end(); ite++) + { + if (isOpX
(*ite)) + { + Expr d = (*ite)->right(); + divs.erase(d); + *ite = mk((*ite)->left(), mkmult(divs, efac)); + divs.insert(d); + } + else + *ite = mk(*ite, mkmult(divs, efac)); + } + for(auto ite = plusOpsRight.begin(); ite != plusOpsRight.end(); ite++) + { + if (isOpX
(*ite)) + { + Expr d = (*ite)->right(); + divs.erase(d); + *ite = mk((*ite)->right(), mkmult(divs, efac)); + divs.insert(d); + } + else + *ite = mk(*ite, mkmult(divs, efac)); + } + if (minusOps % 2 == 0) + return (mk(fla->op(), mkplus(plusOpsLeft, efac), mkplus(plusOpsRight,efac))); + return reBuildCmpSym(fla, mkplus(plusOpsRight, efac), mkplus(plusOpsLeft, efac)); + } + + static void realMultHelper(Expr fla, ExprVector& mults) + { + if (!isOpX(fla)) + mults.push_back(fla); + else + { + for (int i = 0; i < fla->arity(); i++) + realMultHelper(fla->arg(i), mults); + } + } + + static Expr realSimplifyMult(Expr fla) + { + ExprFactory& efac = fla->getFactory(); + ExprVector plusOpsLeft; + ExprVector plusOpsRight; + getAddTerm(fla->left(), plusOpsLeft); + getAddTerm(fla->right(), plusOpsRight); + + for(auto ite = plusOpsRight.begin(); ite != plusOpsRight.end(); ite++) + { + if (!isOpX(*ite)) + continue; + ExprVector mults; + realMultHelper(*ite, mults); + *ite = mkmult(mults, efac); + } + for(auto ite = plusOpsLeft.begin(); ite != plusOpsLeft.end(); ite++) + { + if (!isOpX(*ite)) + continue; + ExprVector mults; + realMultHelper(*ite, mults); + *ite = mkmult(mults, efac); + } + return mk(fla->op(), mkplus(plusOpsLeft, efac), mkplus(plusOpsRight, efac)); + } + inline Expr rewriteDivConstraints(Expr fla) { // heuristic for the divisibility constraints diff --git a/src/ae/MBPUtils.cpp b/src/ae/MBPUtils.cpp index f1c8b93ec..6afa9a327 100644 --- a/src/ae/MBPUtils.cpp +++ b/src/ae/MBPUtils.cpp @@ -42,6 +42,20 @@ void laMergeBounds( return isOpX(m.eval(mk(ra, rb))); }); + outs() << "upVec: "; + for (auto a: upVec) + { + outs() << a << " : " << m.eval(a->right()) << ";"; + } + outs() << endl; + + outs() << "loVec: "; + for (auto a: loVec) + { + outs() << a << " : " << m.eval(a->right()) << ";"; + } + outs() << endl; + Expr loBound = loVec.back(); Expr upBound = upVec.front(); @@ -66,18 +80,30 @@ void laMergeBounds( */ Expr lraMultTrans(Expr t, Expr eVar) { + // outs() << "exp: " << t << "eVar: " << eVar << "\n"; Expr lhs = t->left(), rhs = t->right(); + unsigned minOps = 0; while(isOp(lhs)) //until lhs is no longer * { - Expr lOperand = lhs->left(), rOperand = lhs->right(); - bool yOnTheLeft = contains(lOperand, eVar); - - rhs = mk
(rhs, yOnTheLeft ? rOperand : lOperand); - lhs = yOnTheLeft ? lOperand : rOperand; + Expr varOperand; + for (int i = 0; i < lhs->arity(); i++) + { + if (contains(lhs->arg(i), eVar)) + varOperand = lhs->arg(i); + else + { + if (lexical_cast(lhs->arg(i))[0] == '-') + minOps++; + rhs = mk
(rhs, lhs->arg(i)); + } + } + lhs = varOperand; if (!contains(lhs, eVar)) unreachable(); } - return (mk(t->op(), lhs, rhs)); + if (minOps % 2 == 0) + return (mk(t->op(), lhs, rhs)); + return reBuildCmpSym(t, rhs, lhs); } /** @@ -289,13 +315,19 @@ Expr ineqPrepare(Expr t, Expr eVar) t = mkNeg(t->left()); if(isOp(t)) { - Expr zero = intVSreal == REALTYPE ? mkMPQ("0", eVar->efac()) - : mkMPZ(0, eVar->efac()); + Expr zero = intVSreal == INTTYPE ? mkMPZ(0, eVar->efac()) + : mkMPQ("0", eVar->efac()); // rewrite so that y is on lhs, with positive coef t = simplifyArithm(reBuildCmp( t, mk(t->arg(0), additiveInverse(t->arg(1))), zero)); + if (isRealConst(eVar)) { + outs() << "Before: " << t << "\n"; + t = realRewriteDivs(t, eVar); + t = realSimplifyMult(t); + outs() << "After: " << t << "\n"; + } t = ineqSimplifier(eVar, t); } else @@ -307,8 +339,6 @@ Expr ineqPrepare(Expr t, Expr eVar) return t; else if(intVSreal != NOTYPE) { - // t = tryToRemoveMixType(t); - outs() << "t = " << t << "\n" << "intOrReal: " < Date: Wed, 30 Nov 2022 19:14:54 +0300 Subject: [PATCH 04/10] some fixes for div rewriting --- src/ae/AeValSolver.hpp | 4 -- src/ae/ExprSimpl.hpp | 84 +++++++++++++++++++++++++++--------------- src/ae/MBPUtils.cpp | 4 +- 3 files changed, 57 insertions(+), 35 deletions(-) diff --git a/src/ae/AeValSolver.hpp b/src/ae/AeValSolver.hpp index ef9d77858..18f258d03 100644 --- a/src/ae/AeValSolver.hpp +++ b/src/ae/AeValSolver.hpp @@ -173,10 +173,6 @@ namespace ufo { ExprSet lits; u.getTrueLiterals(pr, m, lits, true); - outs() << "Lits: { \n"; - for (auto a: lits) - outs() << a << "\n"; - outs() << "}\n"; pr = simplifyArithm(mixQE(conjoin(lits, efac), exp, m, u, debug)); if(m.eval(exp) != exp) modelMap[exp] = mk(exp, m.eval(exp)); diff --git a/src/ae/ExprSimpl.hpp b/src/ae/ExprSimpl.hpp index 34ad2e20b..c923e7b01 100644 --- a/src/ae/ExprSimpl.hpp +++ b/src/ae/ExprSimpl.hpp @@ -597,6 +597,7 @@ namespace ufo } else if (isOpX(*it) && isRealConst(var)) { ExprVector tmp; + outs() << *it << "\n"; int skipped = 0; for (int i = 0; i < (*it)->arity(); ++i) { @@ -2257,54 +2258,77 @@ namespace ufo ExprFactory& efac = var->efac(); ExprVector plusOpsLeft; ExprVector plusOpsRight; + + ExprVector lhss; + ExprVector rhss; int minusOps = 0; getAddTerm(fla->left(), plusOpsLeft); getAddTerm(fla->right(), plusOpsRight); + outs() <<"in realRewriteDivs\n"; + outs() << "LeftPlus: \n"; + for (auto l : plusOpsLeft) + outs() << l << "\n"; + outs() << "RightPlus: \n"; + for (auto l : plusOpsRight) + outs() << l << "\n"; + ExprSet divs; - for (auto a : plusOpsLeft) - if(isOpX
(a)) - { - divs.insert(a->right()); - if(lexical_cast(a->right())[0] == '-') - minusOps++; - } - for (auto a : plusOpsRight) - if(isOpX
(a)) - { - divs.insert(a->right()); - if(lexical_cast(a->right())[0] == '-') - minusOps++; - } - + for (auto it = plusOpsLeft.begin(); it != plusOpsLeft.end(); it++) + { + if(!contains(*it, var)) + continue; + if(isOpX
(*it)) + divs.insert((*it)->right()); + else if (isOpX(*it) && isOpX
((*it)->left())) + divs.insert((*it)->left()->right()); + } + + + outs() << "Divs: "; + for (auto d : divs) { + outs() << d << " "; + } + outs() << "\n"; + for(auto ite = plusOpsLeft.begin(); ite != plusOpsLeft.end(); ite++) { - if (isOpX
(*ite)) + if (!contains(*ite, var)) { + Expr m = mkmult(divs, efac); + if (m != mkMPZ (1, efac)) + *ite = mk(*ite, m); + } + else if (isOpX
(*ite)) { Expr d = (*ite)->right(); divs.erase(d); - *ite = mk((*ite)->left(), mkmult(divs, efac)); + Expr m = mkmult(divs, efac); + if (m != mkMPZ (1, efac)) + *ite = mk((*ite)->left(), m); + else + *ite = (*ite)->left(); divs.insert(d); } - else - *ite = mk(*ite, mkmult(divs, efac)); - } - for(auto ite = plusOpsRight.begin(); ite != plusOpsRight.end(); ite++) - { - if (isOpX
(*ite)) + else if (isOpX(*ite) && isOpX
((*ite)->left())) { - Expr d = (*ite)->right(); + Expr d = (*ite)->left()->right(); divs.erase(d); - *ite = mk((*ite)->right(), mkmult(divs, efac)); + Expr m = mkmult(divs, efac); + if (m != mkMPZ (1, efac)) + *ite = mk(mk((*ite)->left()->left()), m); + else + *ite = mk((*ite)->left()->left()); divs.insert(d); } - else - *ite = mk(*ite, mkmult(divs, efac)); + else { + Expr m = mkmult(divs, efac); + if (m != mkMPZ (1, efac)) + *ite = mk(*ite, m); + } } - if (minusOps % 2 == 0) - return (mk(fla->op(), mkplus(plusOpsLeft, efac), mkplus(plusOpsRight,efac))); - return reBuildCmpSym(fla, mkplus(plusOpsRight, efac), mkplus(plusOpsLeft, efac)); + return (mk(fla->op(), mkplus(plusOpsLeft, efac), mkplus(plusOpsRight,efac))); + } static void realMultHelper(Expr fla, ExprVector& mults) diff --git a/src/ae/MBPUtils.cpp b/src/ae/MBPUtils.cpp index 6afa9a327..ca13faa9e 100644 --- a/src/ae/MBPUtils.cpp +++ b/src/ae/MBPUtils.cpp @@ -324,9 +324,11 @@ Expr ineqPrepare(Expr t, Expr eVar) zero)); if (isRealConst(eVar)) { outs() << "Before: " << t << "\n"; + t = realRewriteDivs(t, eVar); - t = realSimplifyMult(t); outs() << "After: " << t << "\n"; + t = realSimplifyMult(t); + } t = ineqSimplifier(eVar, t); } From 78b49b8a5835bbbcdb39ed8c799eee44a498a57c Mon Sep 17 00:00:00 2001 From: Anna Vasenina Date: Wed, 30 Nov 2022 20:27:46 +0300 Subject: [PATCH 05/10] fixed cmp construction in RewriteDivs --- src/ae/ExprSimpl.hpp | 63 +++++++++++++++++++++++++++++--------------- 1 file changed, 42 insertions(+), 21 deletions(-) diff --git a/src/ae/ExprSimpl.hpp b/src/ae/ExprSimpl.hpp index c923e7b01..4dcc21f8a 100644 --- a/src/ae/ExprSimpl.hpp +++ b/src/ae/ExprSimpl.hpp @@ -542,7 +542,6 @@ namespace ufo Expr r = e->right(); ExprVector orig_lhs, orig_rhs, lhs, rhs; ExprVector realCoefs; - outs() << "rewriteHelperM e = " << e << "\n"; // parse @@ -597,7 +596,6 @@ namespace ufo } else if (isOpX(*it) && isRealConst(var)) { ExprVector tmp; - outs() << *it << "\n"; int skipped = 0; for (int i = 0; i < (*it)->arity(); ++i) { @@ -621,7 +619,7 @@ namespace ufo if (!lhs.empty()) { - errs() << "WARNING: COULD NOT NORMALIZE w.r.t. " << *var << ": " + outs() << "WARNING: COULD NOT NORMALIZE w.r.t. " << *var << ": " << *conjoin (lhs, e->getFactory()) << "\n"; return e; } @@ -2252,6 +2250,33 @@ namespace ufo return typeOf(e) == mk(e->getFactory()); } + static Expr divSimplifier(Expr fla) + { + Expr tmp = fla; + ExprFactory& efac = fla->getFactory(); + ExprVector dividers; + + while (true) + { + if (isOpX
(tmp)) + { + dividers.push_back(tmp->right()); + tmp = tmp->left(); + } + else if (isOpX(tmp) && isOpX
(tmp->left())) + { + dividers.push_back(tmp->left()->right()); + tmp = additiveInverse(tmp->left()->left()); + } + else + break; + } + + if (dividers.size() == 0) + return fla; + return mk
(tmp, mkmult(dividers, efac)); + } + static Expr realRewriteDivs(Expr fla, Expr var) { assert (isOp(fla)); @@ -2266,32 +2291,27 @@ namespace ufo getAddTerm(fla->left(), plusOpsLeft); getAddTerm(fla->right(), plusOpsRight); - outs() <<"in realRewriteDivs\n"; - outs() << "LeftPlus: \n"; - for (auto l : plusOpsLeft) - outs() << l << "\n"; - outs() << "RightPlus: \n"; - for (auto l : plusOpsRight) - outs() << l << "\n"; + for (auto r : plusOpsRight) + plusOpsLeft.push_back(additiveInverse(r)); ExprSet divs; for (auto it = plusOpsLeft.begin(); it != plusOpsLeft.end(); it++) { if(!contains(*it, var)) continue; - if(isOpX
(*it)) + *it = divSimplifier(*it); + if(isOpX
(*it)) { divs.insert((*it)->right()); - else if (isOpX(*it) && isOpX
((*it)->left())) + if(lexical_cast((*it)->right())[0] == '-') + minusOps++; + } + else if (isOpX(*it) && isOpX
((*it)->left())) { divs.insert((*it)->left()->right()); + if(lexical_cast((*it)->left()->right())[0] == '-') + minusOps++; + } } - - outs() << "Divs: "; - for (auto d : divs) { - outs() << d << " "; - } - outs() << "\n"; - for(auto ite = plusOpsLeft.begin(); ite != plusOpsLeft.end(); ite++) { if (!contains(*ite, var)) { @@ -2327,8 +2347,9 @@ namespace ufo *ite = mk(*ite, m); } } - return (mk(fla->op(), mkplus(plusOpsLeft, efac), mkplus(plusOpsRight,efac))); - + if (minusOps % 2 == 0) + return (mk(fla->op(), mkplus(plusOpsLeft, efac), mkMPZ (0, efac))); + return reBuildCmpSym(fla, mkMPZ (0, efac), mkplus(plusOpsLeft, efac)); } static void realMultHelper(Expr fla, ExprVector& mults) From 8e4a2eaf7022a0682ae80ddd6e5a0524c2a8ba6b Mon Sep 17 00:00:00 2001 From: Anna Vasenina Date: Thu, 1 Dec 2022 19:55:04 +0300 Subject: [PATCH 06/10] some real div fixes --- src/ae/ExprSimpl.hpp | 82 ++++++++++++++++++++++++++++++++++++-------- src/ae/MBPUtils.cpp | 6 ++-- 2 files changed, 71 insertions(+), 17 deletions(-) diff --git a/src/ae/ExprSimpl.hpp b/src/ae/ExprSimpl.hpp index 4dcc21f8a..7ba29ef5f 100644 --- a/src/ae/ExprSimpl.hpp +++ b/src/ae/ExprSimpl.hpp @@ -542,7 +542,7 @@ namespace ufo Expr r = e->right(); ExprVector orig_lhs, orig_rhs, lhs, rhs; ExprVector realCoefs; - + outs() << "In rewrite helper M : e = " << e <<"\n"; // parse getAddTerm(l, orig_lhs); @@ -558,6 +558,12 @@ namespace ufo else rhs.push_back(a); } + outs() << "lhs: "; + for (auto l : lhs) { + outs() << l << " "; + } + outs() << "\n"; + // combine results rational coef(0, 1); for (auto it = lhs.begin(); it != lhs.end(); ) @@ -578,8 +584,10 @@ namespace ufo { if (subExpr->arg(i) != var) tmp.push_back(subExpr->arg(i)); - else + else { skipped++; + // outs() << i << " : " << subExpr->arg(i) << "\n"; + } } assert(skipped == 1); realCoefs.push_back(mk(mkmult(tmp, var->efac()))); @@ -601,8 +609,10 @@ namespace ufo { if ((*it)->arg(i) != var) tmp.push_back((*it)->arg(i)); - else + else { skipped++; + // outs() << i << " : " << (*it)->arg(i) << "\n"; + } } assert(skipped == 1); realCoefs.push_back(mkmult(tmp, var->efac())); @@ -1894,6 +1904,7 @@ namespace ufo } static Expr rewriteMultAdd (Expr exp); + static Expr rewriteDivAdd (Expr exp); inline static void getAddTerm (Expr a, ExprVector &terms) // implementation (mutually recursive) { @@ -1941,6 +1952,12 @@ namespace ufo if (tmp == a) terms.push_back(a); else getAddTerm(tmp, terms); } + else if (isOpX
(a)) + { + Expr tmp = rewriteDivAdd(a); + if (tmp == a) terms.push_back(a); + else getAddTerm(tmp, terms); + } else if (lexical_cast(a) != "0") { bool found = false; @@ -1980,7 +1997,7 @@ namespace ufo { for (auto &b : allrhs) { - unf.push_back(mk(a, b)); + unf.push_back(mk(a, b)); } } return mkplus(unf, exp->getFactory()); @@ -1996,6 +2013,38 @@ namespace ufo return dagVisit (mu, exp); } + struct AddDivDistr + { + AddDivDistr () {}; + + Expr operator() (Expr exp) + { + if (isOpX
(exp) && exp->arity() == 2) + { + Expr lhs = exp->left(); + Expr rhs = exp->right(); + + ExprVector alllhs; + getAddTerm(lhs, alllhs); + + ExprVector unf; + for (auto &a : alllhs) + { + unf.push_back(mk
(a, rhs)); + } + return mkplus(unf, exp->getFactory()); + } + + return exp; + } + }; + + inline static Expr rewriteDivAdd (Expr exp) + { + RW mu(new AddDivDistr()); + return dagVisit (mu, exp); + } + struct FindNonlinAndRewrite { ExprVector& vars; @@ -2250,7 +2299,7 @@ namespace ufo return typeOf(e) == mk(e->getFactory()); } - static Expr divSimplifier(Expr fla) + static Expr divSimplifier(Expr fla, int& minusOps) { Expr tmp = fla; ExprFactory& efac = fla->getFactory(); @@ -2261,13 +2310,24 @@ namespace ufo if (isOpX
(tmp)) { dividers.push_back(tmp->right()); + if(lexical_cast(tmp->right())[0] == '-') + minusOps++; // TODO: complicated divs tmp = tmp->left(); } else if (isOpX(tmp) && isOpX
(tmp->left())) { dividers.push_back(tmp->left()->right()); + if(lexical_cast(tmp->left()->right())[0] == '-') + minusOps++; // TODO: complicated divs tmp = additiveInverse(tmp->left()->left()); } + // else if (isOpX(tmp) && isOpX
(tmp->left())) + // { + // dividers.push_back(tmp->left()->right()); + // if(lexical_cast(tmp->left()->right())[0] == '-') + // minusOps++; // TODO: complicated divs + // tmp = mk(tmp->right(), tmp->left()->left()); + // } else break; } @@ -2299,17 +2359,11 @@ namespace ufo { if(!contains(*it, var)) continue; - *it = divSimplifier(*it); - if(isOpX
(*it)) { + *it = divSimplifier(*it, minusOps); + if(isOpX
(*it)) divs.insert((*it)->right()); - if(lexical_cast((*it)->right())[0] == '-') - minusOps++; - } - else if (isOpX(*it) && isOpX
((*it)->left())) { + else if (isOpX(*it) && isOpX
((*it)->left())) divs.insert((*it)->left()->right()); - if(lexical_cast((*it)->left()->right())[0] == '-') - minusOps++; - } } for(auto ite = plusOpsLeft.begin(); ite != plusOpsLeft.end(); ite++) diff --git a/src/ae/MBPUtils.cpp b/src/ae/MBPUtils.cpp index ca13faa9e..dea782cc5 100644 --- a/src/ae/MBPUtils.cpp +++ b/src/ae/MBPUtils.cpp @@ -324,11 +324,11 @@ Expr ineqPrepare(Expr t, Expr eVar) zero)); if (isRealConst(eVar)) { outs() << "Before: " << t << "\n"; - + t = realSimplifyMult(t); t = realRewriteDivs(t, eVar); - outs() << "After: " << t << "\n"; + outs() << "After rewriteDivs: " << t << "\n"; t = realSimplifyMult(t); - + outs() << "After: " << t << "\n"; } t = ineqSimplifier(eVar, t); } From cfd4df461ecb2e24adacd69f1a84c97e1ac54973 Mon Sep 17 00:00:00 2001 From: Anna Vasenina Date: Sat, 3 Dec 2022 17:56:57 +0300 Subject: [PATCH 07/10] Fixed rewriting, some MBP issue is still present --- src/ae/AeValSolver.hpp | 6 +++++- src/ae/ExprSimpl.hpp | 40 ++++++++++++++++++++++++++++++--------- src/ae/MBPUtils.cpp | 43 ++++++++++++++++++++++-------------------- 3 files changed, 59 insertions(+), 30 deletions(-) diff --git a/src/ae/AeValSolver.hpp b/src/ae/AeValSolver.hpp index 18f258d03..9a8db194b 100644 --- a/src/ae/AeValSolver.hpp +++ b/src/ae/AeValSolver.hpp @@ -171,8 +171,12 @@ namespace ufo ExprMap modelMap; for(auto &exp : v) { - ExprSet lits; + ExprSet lits; u.getTrueLiterals(pr, m, lits, true); + // outs() << "Lits: { \n"; + // for (auto a: lits) + // outs() << a << "\n"; + // outs() << "}\n\n"; pr = simplifyArithm(mixQE(conjoin(lits, efac), exp, m, u, debug)); if(m.eval(exp) != exp) modelMap[exp] = mk(exp, m.eval(exp)); diff --git a/src/ae/ExprSimpl.hpp b/src/ae/ExprSimpl.hpp index 7ba29ef5f..0b8b2a327 100644 --- a/src/ae/ExprSimpl.hpp +++ b/src/ae/ExprSimpl.hpp @@ -542,7 +542,6 @@ namespace ufo Expr r = e->right(); ExprVector orig_lhs, orig_rhs, lhs, rhs; ExprVector realCoefs; - outs() << "In rewrite helper M : e = " << e <<"\n"; // parse getAddTerm(l, orig_lhs); @@ -557,13 +556,7 @@ namespace ufo if (contains (a, var)) lhs.push_back(additiveInverse(a)); else rhs.push_back(a); } - - outs() << "lhs: "; - for (auto l : lhs) { - outs() << l << " "; - } - outs() << "\n"; - + // combine results rational coef(0, 1); for (auto it = lhs.begin(); it != lhs.end(); ) @@ -639,7 +632,6 @@ namespace ufo { l = mkplus(realCoefs, var->efac()); l = mk(l, var); - outs() << "transformed e: " << e << "to :" << mk(l,r); return mk(l,r); } if (coef == 0){ @@ -1908,6 +1900,7 @@ namespace ufo inline static void getAddTerm (Expr a, ExprVector &terms) // implementation (mutually recursive) { + // outs() << "getAddTerm for " << a << "\n"; if (isOpX(a)) { for (auto it = a->args_begin (), end = a->args_end (); it != end; ++it) @@ -1948,6 +1941,32 @@ namespace ufo } else if (isOpX(a)) { + if (a->arity() == 2) { + Expr lhs = a->left(); + Expr rhs = a->right(); + if (isOpX
(lhs)) { + Expr tmp = mk
(mk(rhs, lhs->left() ), lhs->right()); + getAddTerm(tmp, terms); + return; + } + else if (isOpX
(rhs)) { + Expr tmp = mk
(mk(lhs, rhs->left()), rhs->right()); + getAddTerm(tmp, terms); + return; + } + else if (isOpX(lhs) && isOpX
(lhs->left())) { + rhs = additiveInverse(rhs); + Expr tmp = mk
(mk(rhs, lhs->left()->left() ), lhs->left()->right()); + getAddTerm(tmp, terms); + return; + } + else if (isOpX(rhs) && isOpX
(rhs->left())) { + lhs = additiveInverse(lhs); + Expr tmp = mk
(mk(rhs->left()->left(), lhs), rhs->left()->right()); + getAddTerm(tmp, terms); + return; + } + } Expr tmp = rewriteMultAdd(a); if (tmp == a) terms.push_back(a); else getAddTerm(tmp, terms); @@ -2422,11 +2441,13 @@ namespace ufo ExprFactory& efac = fla->getFactory(); ExprVector plusOpsLeft; ExprVector plusOpsRight; + int minusOps = 0; getAddTerm(fla->left(), plusOpsLeft); getAddTerm(fla->right(), plusOpsRight); for(auto ite = plusOpsRight.begin(); ite != plusOpsRight.end(); ite++) { + *ite = divSimplifier(*ite, minusOps); if (!isOpX(*ite)) continue; ExprVector mults; @@ -2435,6 +2456,7 @@ namespace ufo } for(auto ite = plusOpsLeft.begin(); ite != plusOpsLeft.end(); ite++) { + *ite = divSimplifier(*ite, minusOps); if (!isOpX(*ite)) continue; ExprVector mults; diff --git a/src/ae/MBPUtils.cpp b/src/ae/MBPUtils.cpp index dea782cc5..353be2e23 100644 --- a/src/ae/MBPUtils.cpp +++ b/src/ae/MBPUtils.cpp @@ -42,19 +42,19 @@ void laMergeBounds( return isOpX(m.eval(mk(ra, rb))); }); - outs() << "upVec: "; - for (auto a: upVec) - { - outs() << a << " : " << m.eval(a->right()) << ";"; - } - outs() << endl; - - outs() << "loVec: "; - for (auto a: loVec) - { - outs() << a << " : " << m.eval(a->right()) << ";"; - } - outs() << endl; + // outs() << "upVec: "; + // for (auto a: upVec) + // { + // outs() << a << " : " << m.eval(a->right()) << ";"; + // } + // outs() << endl; + + // outs() << "loVec: "; + // for (auto a: loVec) + // { + // outs() << a << " : " << m.eval(a->right()) << ";"; + // } + // outs() << endl; Expr loBound = loVec.back(); Expr upBound = upVec.front(); @@ -323,12 +323,8 @@ Expr ineqPrepare(Expr t, Expr eVar) mk(t->arg(0), additiveInverse(t->arg(1))), zero)); if (isRealConst(eVar)) { - outs() << "Before: " << t << "\n"; - t = realSimplifyMult(t); t = realRewriteDivs(t, eVar); - outs() << "After rewriteDivs: " << t << "\n"; t = realSimplifyMult(t); - outs() << "After: " << t << "\n"; } t = ineqSimplifier(eVar, t); } @@ -380,9 +376,16 @@ Expr ufo::mixQE( sameTypeSet.insert(t); } - if(!sameTypeSet.empty()) - outSet.insert(isReal(eVar) ? realQE(sameTypeSet, eVar, m) - : intQE(sameTypeSet, eVar, m)); + if(!sameTypeSet.empty()) { + Expr o = isReal(eVar) ? realQE(sameTypeSet, eVar, m) : intQE(sameTypeSet, eVar, m); + // outs() << "o is : " << o << std::endl; + outSet.insert(o); + } + + // outs() << "OutSet:\n"; + // for (auto o : outSet) + // outs() << o << "\n"; + // outs() << std::endl; return conjoin(outSet, eVar->getFactory()); } From 261a4cbaaa351eb24a2426fdf6400ca0892f0743 Mon Sep 17 00:00:00 2001 From: Anna Vasenina Date: Mon, 5 Dec 2022 17:06:40 +0300 Subject: [PATCH 08/10] debugging commit --- src/ae/AeValSolver.hpp | 20 +++-- src/ae/ExprSimpl.hpp | 169 ++++++++++++++++++++++++++++++----------- src/ae/MBPUtils.cpp | 34 ++++----- 3 files changed, 154 insertions(+), 69 deletions(-) diff --git a/src/ae/AeValSolver.hpp b/src/ae/AeValSolver.hpp index 9a8db194b..dc261b587 100644 --- a/src/ae/AeValSolver.hpp +++ b/src/ae/AeValSolver.hpp @@ -173,11 +173,12 @@ namespace ufo { ExprSet lits; u.getTrueLiterals(pr, m, lits, true); - // outs() << "Lits: { \n"; - // for (auto a: lits) - // outs() << a << "\n"; - // outs() << "}\n\n"; - pr = simplifyArithm(mixQE(conjoin(lits, efac), exp, m, u, debug)); + outs() << "Lits with var : { \n"; + for (auto a: lits) + if (contains(a, exp)) + outs() << a << "\n"; + outs() << "}\n" << std::endl; + pr = mixQE(conjoin(lits, efac), exp, m, u, debug); if(m.eval(exp) != exp) modelMap[exp] = mk(exp, m.eval(exp)); @@ -199,6 +200,7 @@ namespace ufo } outs() << "projection:\n"; pprint(pr, 2); + outs() << std::endl; } if(debug) @@ -227,10 +229,14 @@ namespace ufo { assert(isOpX(m.eval(pr))); ExprVector args; - for(auto temp : v) + ExprVector argsPr; + for(auto temp : v) { args.push_back(temp->last()); + argsPr.push_back(temp->last()); + } args.push_back(t); - boost::tribool impl = u.implies(pr, mknary(args)); + argsPr.push_back(pr); + boost::tribool impl = u.implies(mknary(argsPr), mknary(args)); tribool_assert(impl); }; diff --git a/src/ae/ExprSimpl.hpp b/src/ae/ExprSimpl.hpp index 0b8b2a327..b144dee6a 100644 --- a/src/ae/ExprSimpl.hpp +++ b/src/ae/ExprSimpl.hpp @@ -4847,68 +4847,147 @@ namespace ufo return convertIntsToReals(exp); } - static void getLiterals (Expr exp, ExprSet& lits, bool splitEqs = true); - - static void getLiteralsBool(Expr exp, ExprSet& lits, bool splitEqs = true) + // static void getLiterals (Expr exp, ExprSet& lits, bool splitEqs = true); + + // static void getLiteralsBool(Expr exp, ExprSet& lits, bool splitEqs = true) + // { + // Expr el = exp->left(); + // Expr er = exp->right(); + // if (isOp(exp) && !splitEqs && isBoolConstOrNegation(el) && isBoolConstOrNegation(er)) { + // lits.insert(exp); + // } else if (isOpX(exp) || isOpX(exp) || isOpX(exp) || isOpX(exp)) { + // getLiterals(mkNeg(el), lits, splitEqs); + // getLiterals(er, lits, splitEqs); + // getLiterals(mkNeg(er), lits, splitEqs); + // getLiterals(el, lits, splitEqs); + // } else if (isOpX(exp) || isOpX(exp)) { + // for (int i = 0; i < exp->arity(); i++) + // getLiterals(exp->arg(i), lits, splitEqs); + // } else if (isOpX(exp)) { + // if (isBoolConst(el)) + // lits.insert(exp); + // else + // getLiterals(mkNeg(el), lits, splitEqs); + // } else if (isOpX(exp)) { + // getLiterals(mkNeg(el), lits, splitEqs); + // getLiterals(er, lits, splitEqs); + // } + // } + + // static void getLiteralsNumeric(Expr exp, ExprSet& lits, bool splitEqs = true) + // { + // exp = tryToRemoveMixType(exp); + // Expr el = exp->left(); + // Expr er = exp->right(); + // if (isOp(exp) && !splitEqs) { + // lits.insert(exp); + // } else if (isOpX(exp) && !containsOp(exp)) { + // getLiterals(mk(el, er), lits, splitEqs); + // getLiterals(mk(el, er), lits, splitEqs); + // } else if (isOpX(exp) && !containsOp(exp)) { + // getLiterals(mk(el, er), lits, splitEqs); + // getLiterals(mk(el, er), lits, splitEqs); + // } else if (isOp(exp)) { + // exp = rewriteDivConstraints(exp); + // exp = rewriteModConstraints(exp); + // if (isOpX(exp) || isOpX(exp)) + // getLiterals(exp, lits, splitEqs); + // else lits.insert(exp); + // } + // } + + // static void getLiterals (Expr exp, ExprSet& lits, bool splitEqs) + // { + // ExprFactory& efac = exp->getFactory(); + // Expr el = exp->left(); + // Expr er = exp->right(); + // if (isOp(exp) || isOp(exp) && isBoolean(el)) + // getLiteralsBool(exp, lits, splitEqs); + // else if (isOp(exp) && isNumeric(el)) + // getLiteralsNumeric(exp, lits, splitEqs); + // else if (bind::typeOf(exp) == mk(efac) && + // !containsOp(exp) && !containsOp(exp)) { + // lits.insert(exp); + // } else if (!isOpX(exp) && !isOpX(exp)) { + // errs () << "unable lit: " << *exp << "\n"; + // assert(0); + // } + // } + + static void getLiterals (Expr exp, ExprSet& lits, bool splitEqs = true) { + ExprFactory& efac = exp->getFactory(); Expr el = exp->left(); Expr er = exp->right(); - if (isOp(exp) && !splitEqs && isBoolConstOrNegation(el) && isBoolConstOrNegation(er)) { + if (isOp(exp) && !splitEqs) + { + if (isNumeric(el) || (isBoolConstOrNegation(el) && isBoolConstOrNegation(er))) lits.insert(exp); - } else if (isOpX(exp) || isOpX(exp) || isOpX(exp) || isOpX(exp)) { + } + if (isOpX(exp) && isBoolean(er)) + { getLiterals(mkNeg(el), lits, splitEqs); getLiterals(er, lits, splitEqs); getLiterals(mkNeg(er), lits, splitEqs); getLiterals(el, lits, splitEqs); - } else if (isOpX(exp) || isOpX(exp)) { - for (int i = 0; i < exp->arity(); i++) - getLiterals(exp->arg(i), lits, splitEqs); - } else if (isOpX(exp)) { + } + if (isOpX(exp) && isNumeric(el) && !containsOp(exp)) + { + getLiterals(mk(el, er), lits, splitEqs); + getLiterals(mk(el, er), lits, splitEqs); + } + else if (isOpX(exp) && isNumeric(el) && !containsOp(exp)) + { + getLiterals(mk(el, er), lits, splitEqs); + getLiterals(mk(el, er), lits, splitEqs); + } + else if ((isOpX(exp) || isOpX(exp) || isOpX(exp)) && isBoolean(el)) + { + getLiterals(el, lits, splitEqs); + getLiterals(er, lits, splitEqs); + getLiterals(mkNeg(el), lits, splitEqs); + getLiterals(mkNeg(er), lits, splitEqs); + } + else if (isOpX(exp)) + { if (isBoolConst(el)) lits.insert(exp); else getLiterals(mkNeg(el), lits, splitEqs); - } else if (isOpX(exp)) { + } + else if (isOpX(exp)) + { getLiterals(mkNeg(el), lits, splitEqs); getLiterals(er, lits, splitEqs); } - } - - static void getLiteralsNumeric(Expr exp, ExprSet& lits, bool splitEqs = true) - { - exp = tryToRemoveMixType(exp); - Expr el = exp->left(); - Expr er = exp->right(); - if (isOp(exp) && !splitEqs) { - lits.insert(exp); - } else if (isOpX(exp) && !containsOp(exp)) { - getLiterals(mk(el, er), lits, splitEqs); - getLiterals(mk(el, er), lits, splitEqs); - } else if (isOpX(exp) && !containsOp(exp)) { - getLiterals(mk(el, er), lits, splitEqs); - getLiterals(mk(el, er), lits, splitEqs); - } else if (isOp(exp)) { - exp = rewriteDivConstraints(exp); - exp = rewriteModConstraints(exp); - if (isOpX(exp) || isOpX(exp)) - getLiterals(exp, lits, splitEqs); - else lits.insert(exp); + else if (isOpX(exp)) + { + getLiterals(mkNeg(el), lits, splitEqs); + getLiterals(er, lits, splitEqs); + getLiterals(mkNeg(er), lits, splitEqs); + getLiterals(el, lits, splitEqs); } - } - - static void getLiterals (Expr exp, ExprSet& lits, bool splitEqs) - { - ExprFactory& efac = exp->getFactory(); - Expr el = exp->left(); - Expr er = exp->right(); - if (isOp(exp) || isOp(exp) && isBoolean(el)) - getLiteralsBool(exp, lits, splitEqs); - else if (isOp(exp) && isNumeric(el)) - getLiteralsNumeric(exp, lits, splitEqs); else if (bind::typeOf(exp) == mk(efac) && - !containsOp(exp) && !containsOp(exp)) { - lits.insert(exp); - } else if (!isOpX(exp) && !isOpX(exp)) { + !containsOp(exp) && !containsOp(exp)) + { + if (isOp(exp)) + { + exp = tryToRemoveMixType(exp); + exp = rewriteDivConstraints(exp); + exp = rewriteModConstraints(exp); + if (isOpX(exp) || isOpX(exp)) + getLiterals(exp, lits, splitEqs); + else lits.insert(exp); + } + else lits.insert(exp); + } + else if (isOpX(exp) || isOpX(exp)) + { + for (int i = 0; i < exp->arity(); i++) + getLiterals(exp->arg(i), lits, splitEqs); + } + else if (!isOpX(exp) && !isOpX(exp)) + { errs () << "unable lit: " << *exp << "\n"; assert(0); } diff --git a/src/ae/MBPUtils.cpp b/src/ae/MBPUtils.cpp index 353be2e23..6d6d8a9a6 100644 --- a/src/ae/MBPUtils.cpp +++ b/src/ae/MBPUtils.cpp @@ -42,19 +42,19 @@ void laMergeBounds( return isOpX(m.eval(mk(ra, rb))); }); - // outs() << "upVec: "; - // for (auto a: upVec) - // { - // outs() << a << " : " << m.eval(a->right()) << ";"; - // } - // outs() << endl; - - // outs() << "loVec: "; - // for (auto a: loVec) - // { - // outs() << a << " : " << m.eval(a->right()) << ";"; - // } - // outs() << endl; + outs() << "upVec: "; + for (auto a: upVec) + { + outs() << a << " : " << m.eval(a->right()) << ";"; + } + outs() << endl; + + outs() << "loVec: "; + for (auto a: loVec) + { + outs() << a << " : " << m.eval(a->right()) << ";"; + } + outs() << endl; Expr loBound = loVec.back(); Expr upBound = upVec.front(); @@ -382,10 +382,10 @@ Expr ufo::mixQE( outSet.insert(o); } - // outs() << "OutSet:\n"; - // for (auto o : outSet) - // outs() << o << "\n"; - // outs() << std::endl; + outs() << "OutSet:\n"; + for (auto o : outSet) + outs() << o << "\n"; + outs() << std::endl; return conjoin(outSet, eVar->getFactory()); } From 6bf6b11fb63673cecf095e2f689e1d4176b8dd47 Mon Sep 17 00:00:00 2001 From: Anna Vasenina Date: Mon, 5 Dec 2022 19:18:17 +0300 Subject: [PATCH 09/10] minor changes --- src/ae/AeValSolver.hpp | 2 +- src/ae/ExprSimpl.hpp | 27 +++++++-------------------- src/ae/MBPUtils.cpp | 13 ++++--------- src/ae/MBPUtils.hpp | 2 +- 4 files changed, 13 insertions(+), 31 deletions(-) diff --git a/src/ae/AeValSolver.hpp b/src/ae/AeValSolver.hpp index dc261b587..889bd3f4b 100644 --- a/src/ae/AeValSolver.hpp +++ b/src/ae/AeValSolver.hpp @@ -171,7 +171,7 @@ namespace ufo ExprMap modelMap; for(auto &exp : v) { - ExprSet lits; + ExprSet lits; u.getTrueLiterals(pr, m, lits, true); outs() << "Lits with var : { \n"; for (auto a: lits) diff --git a/src/ae/ExprSimpl.hpp b/src/ae/ExprSimpl.hpp index b144dee6a..0d6216b72 100644 --- a/src/ae/ExprSimpl.hpp +++ b/src/ae/ExprSimpl.hpp @@ -556,7 +556,7 @@ namespace ufo if (contains (a, var)) lhs.push_back(additiveInverse(a)); else rhs.push_back(a); } - + // combine results rational coef(0, 1); for (auto it = lhs.begin(); it != lhs.end(); ) @@ -570,17 +570,15 @@ namespace ufo coef -= lexical_cast(subExpr->left()); found = true; } - else if (isOpX(subExpr) && 2 == subExpr->arity() && isOpX(subExpr->left()) && subExpr->right() == var) { + else if (isOpX(subExpr) && isRealConst(var)) { ExprVector tmp; int skipped = 0; for (int i = 0; i < (*it)->arity(); ++i) - { + { if (subExpr->arg(i) != var) tmp.push_back(subExpr->arg(i)); - else { + else skipped++; - // outs() << i << " : " << subExpr->arg(i) << "\n"; - } } assert(skipped == 1); realCoefs.push_back(mk(mkmult(tmp, var->efac()))); @@ -602,10 +600,8 @@ namespace ufo { if ((*it)->arg(i) != var) tmp.push_back((*it)->arg(i)); - else { + else skipped++; - // outs() << i << " : " << (*it)->arg(i) << "\n"; - } } assert(skipped == 1); realCoefs.push_back(mkmult(tmp, var->efac())); @@ -622,7 +618,7 @@ namespace ufo if (!lhs.empty()) { - outs() << "WARNING: COULD NOT NORMALIZE w.r.t. " << *var << ": " + errs() << "WARNING: COULD NOT NORMALIZE w.r.t. " << *var << ": " << *conjoin (lhs, e->getFactory()) << "\n"; return e; } @@ -1900,7 +1896,6 @@ namespace ufo inline static void getAddTerm (Expr a, ExprVector &terms) // implementation (mutually recursive) { - // outs() << "getAddTerm for " << a << "\n"; if (isOpX(a)) { for (auto it = a->args_begin (), end = a->args_end (); it != end; ++it) @@ -2016,7 +2011,7 @@ namespace ufo { for (auto &b : allrhs) { - unf.push_back(mk(a, b)); + unf.push_back(mk(a, b)); } } return mkplus(unf, exp->getFactory()); @@ -2340,13 +2335,6 @@ namespace ufo minusOps++; // TODO: complicated divs tmp = additiveInverse(tmp->left()->left()); } - // else if (isOpX(tmp) && isOpX
(tmp->left())) - // { - // dividers.push_back(tmp->left()->right()); - // if(lexical_cast(tmp->left()->right())[0] == '-') - // minusOps++; // TODO: complicated divs - // tmp = mk(tmp->right(), tmp->left()->left()); - // } else break; } @@ -5044,6 +5032,5 @@ namespace ufo } if (upper) outs() << "\n"; } - } #endif diff --git a/src/ae/MBPUtils.cpp b/src/ae/MBPUtils.cpp index 6d6d8a9a6..d41b65836 100644 --- a/src/ae/MBPUtils.cpp +++ b/src/ae/MBPUtils.cpp @@ -80,7 +80,6 @@ void laMergeBounds( */ Expr lraMultTrans(Expr t, Expr eVar) { - // outs() << "exp: " << t << "eVar: " << eVar << "\n"; Expr lhs = t->left(), rhs = t->right(); unsigned minOps = 0; while(isOp(lhs)) //until lhs is no longer * @@ -336,9 +335,7 @@ Expr ineqPrepare(Expr t, Expr eVar) else if(isInt(eVar) && (intVSreal == INTTYPE)) return t; else if(intVSreal != NOTYPE) - { notImplemented(); - } return t; } @@ -376,12 +373,10 @@ Expr ufo::mixQE( sameTypeSet.insert(t); } - if(!sameTypeSet.empty()) { - Expr o = isReal(eVar) ? realQE(sameTypeSet, eVar, m) : intQE(sameTypeSet, eVar, m); - // outs() << "o is : " << o << std::endl; - outSet.insert(o); - } - + if(!sameTypeSet.empty()) + outSet.insert(isReal(eVar) ? realQE(sameTypeSet, eVar, m) + : intQE(sameTypeSet, eVar, m)); + outs() << "OutSet:\n"; for (auto o : outSet) outs() << o << "\n"; diff --git a/src/ae/MBPUtils.hpp b/src/ae/MBPUtils.hpp index 577983c42..09dcd777c 100644 --- a/src/ae/MBPUtils.hpp +++ b/src/ae/MBPUtils.hpp @@ -8,4 +8,4 @@ namespace ufo { Expr mixQE(Expr s, Expr eVar, ZSolver::Model &m, SMTUtils &u, int debug); } -#endif \ No newline at end of file +#endif From 872618a839f0ab027a6670c0cfaecfa66c051ccf Mon Sep 17 00:00:00 2001 From: Anna Vasenina Date: Mon, 5 Dec 2022 19:29:44 +0300 Subject: [PATCH 10/10] Bring back convert ints to reals for DIV --- src/ae/AeValSolver.hpp | 3 +++ src/ae/ExprSimpl.hpp | 41 ++++++++++++++++++++++++++++++++++++--- src/sygus/SyGuSSolver.hpp | 2 +- 3 files changed, 42 insertions(+), 4 deletions(-) diff --git a/src/ae/AeValSolver.hpp b/src/ae/AeValSolver.hpp index 889bd3f4b..59832877e 100644 --- a/src/ae/AeValSolver.hpp +++ b/src/ae/AeValSolver.hpp @@ -1277,6 +1277,9 @@ namespace ufo minusSets(ex_qvars, fa_qvars); } + s = convertIdivToDiv
(s); + t = convertIdivToDiv
(t); + if(debug >= 3) { outs() << "s part: " << s << "\n"; diff --git a/src/ae/ExprSimpl.hpp b/src/ae/ExprSimpl.hpp index 0d6216b72..2c0092633 100644 --- a/src/ae/ExprSimpl.hpp +++ b/src/ae/ExprSimpl.hpp @@ -2598,9 +2598,9 @@ namespace ufo static Expr convertIntsToReals (Expr exp); - struct IntToReal + struct AllIntsToReals { - IntToReal () {}; + AllIntsToReals () {}; Expr operator() (Expr exp) { @@ -2620,7 +2620,42 @@ namespace ufo static Expr convertIntsToReals (Expr exp) { - RW rw(new IntToReal()); + RW rw(new AllIntsToReals()); + return dagVisit (rw, exp); + } + + template static Expr convertIdivToDiv (Expr exp); + template struct IdivToDiv + { + IdivToDiv () {}; + + Expr operator() (Expr exp) + { + if (isOpX(exp)) + { + ExprVector args; + for (int i = 0; i < exp->arity(); i++) + { + Expr e = exp->arg(i); + if (isOpX(e)) + e = mkTerm (mpq_class (lexical_cast(e)), exp->getFactory()); + else { + e = convertIdivToDiv(e); + e = convertIdivToDiv(e); + e = convertIdivToDiv(e); + e = convertIdivToDiv(e); + } + args.push_back(e); + } + return mknary(args); + } + return exp; + } + }; + + template static Expr convertIdivToDiv (Expr exp) + { + RW> rw(new IdivToDiv()); return dagVisit (rw, exp); } diff --git a/src/sygus/SyGuSSolver.hpp b/src/sygus/SyGuSSolver.hpp index d14f3202b..2d0c807e9 100644 --- a/src/sygus/SyGuSSolver.hpp +++ b/src/sygus/SyGuSSolver.hpp @@ -218,7 +218,7 @@ class SyGuSSolver faArgs.push_back(mknary(exArgs)); Expr aeProb = mknary(faArgs); aeProb = regularizeQF(aeProb); - aeProb = tryToRemoveMixType(aeProb); + aeProb = convertIdivToDiv
(aeProb); if (debug > 1) { outs() << "Sending to aeval: "; u.print(aeProb); outs() << endl; }