Skip to content

Commit

Permalink
bb working
Browse files Browse the repository at this point in the history
  • Loading branch information
@yoni206
yoni206 committed Aug 1, 2024
1 parent cdcd125 commit 90996d7
Show file tree
Hide file tree
Showing 5 changed files with 44 additions and 103 deletions.
3 changes: 0 additions & 3 deletions src/theory/bv/int_blaster.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -156,10 +156,7 @@ Node IntBlaster::intBlast(Node n,
std::map<Node, Node>& skolems)
{
// make sure the node is re-written
std::cout << " panda before rr: " << n << std::endl;
n = rewrite(n);
std::cout << " panda after rr: " << n << std::endl;


// helper vector for traversal.
std::vector<Node> toVisit;
Expand Down
56 changes: 28 additions & 28 deletions src/theory/bv/theory_bv.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@
#include "theory/bv/bv_solver_bitblast_internal.h"
#include "theory/bv/theory_bv_rewrite_rules_normalization.h"
#include "theory/bv/theory_bv_rewrite_rules_simplification.h"
#include "theory/bv/theory_bv_rewrite_rules_operator_elimination.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/ee_setup_info.h"
#include "theory/trust_substitutions.h"
Expand Down Expand Up @@ -283,34 +284,33 @@ TrustNode TheoryBV::ppRewrite(TNode t, std::vector<SkolemLemma>& lems)
}
}

if (options().smt.solveBVAsInt == options::SolveBVAsIntMode::OFF) {
std::cout << "panda hey" << std::endl;
if (RewriteRule<NegoEliminate>::applies(t))
{
res = RewriteRule<NegoEliminate>::run<false>(t);
} else if (RewriteRule<UaddoEliminate>::applies(t))
{
res = RewriteRule<UaddoEliminate>::run<false>(t);
} else if (RewriteRule<SaddoEliminate>::applies(t))
{
res = RewriteRule<SaddoEliminate>::run<false>(t);
} else if (RewriteRule<UmuloEliminate>::applies(t))
{
res = RewriteRule<UmuloEliminate>::run<false>(t);
} else if (RewriteRule<SmuloEliminate>::applies(t))
{
res = RewriteRule<SmuloEliminate>::run<false>(t);
} else if (RewriteRule<UsuboEliminate>::applies(t))
{
res = RewriteRule<UsuboEliminate>::run<false>(t);
} else if (RewriteRule<SsuboEliminate>::applies(t))
{
res = RewriteRule<SsuboEliminate>::run<false>(t);
} else if (RewriteRule<SdivoEliminate>::applies(t))
{
res = RewriteRule<SdivoEliminate>::run<false>(t);
}
}
if (options().smt.solveBVAsInt == options::SolveBVAsIntMode::OFF) {
if (RewriteRule<NegoEliminate>::applies(t))
{
res = RewriteRule<NegoEliminate>::run<false>(t);
} else if (RewriteRule<UaddoEliminate>::applies(t))
{
res = RewriteRule<UaddoEliminate>::run<false>(t);
} else if (RewriteRule<SaddoEliminate>::applies(t))
{
res = RewriteRule<SaddoEliminate>::run<false>(t);
} else if (RewriteRule<UmuloEliminate>::applies(t))
{
res = RewriteRule<UmuloEliminate>::run<false>(t);
} else if (RewriteRule<SmuloEliminate>::applies(t))
{
res = RewriteRule<SmuloEliminate>::run<false>(t);
} else if (RewriteRule<UsuboEliminate>::applies(t))
{
res = RewriteRule<UsuboEliminate>::run<false>(t);
} else if (RewriteRule<SsuboEliminate>::applies(t))
{
res = RewriteRule<SsuboEliminate>::run<false>(t);
} else if (RewriteRule<SdivoEliminate>::applies(t))
{
res = RewriteRule<SdivoEliminate>::run<false>(t);
}
}

Trace("theory-bv-pp-rewrite") << "to " << res << "\n";
if (res != t)
Expand Down
16 changes: 16 additions & 0 deletions src/theory/bv/theory_bv_rewrite_rules.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -341,6 +341,14 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) {
case CompEliminate : out << "CompEliminate"; return out;
case XnorEliminate : out << "XnorEliminate"; return out;
case SignExtendEliminate : out << "SignExtendEliminate"; return out;
case NegoEliminate: out << "NegoEliminate"; return out;
case UaddoEliminate: out << "UaddoEliminate"; return out;
case SaddoEliminate: out << "SaddoEliminate"; return out;
case UmuloEliminate: out << "UmuloEliminate"; return out;
case SmuloEliminate: out << "SmuloEliminate"; return out;
case UsuboEliminate: out << "SsuboEliminate"; return out;
case SsuboEliminate: out << "SsuboEliminate"; return out;
case SdivoEliminate: out << "SdivoEliminate"; return out;
case NotIdemp : out << "NotIdemp"; return out;
case UleSelf: out << "UleSelf"; return out;
case FlattenAssocCommut: out << "FlattenAssocCommut"; return out;
Expand Down Expand Up @@ -618,6 +626,14 @@ struct AllRewriteRules {
RewriteRule<SmodEliminate> rule145;
RewriteRule<UgtUrem> rule146;
RewriteRule<UltOnes> rule147;
RewriteRule<NegoEliminate> rule148;
RewriteRule<UaddoEliminate> rule149;
RewriteRule<SaddoEliminate> rule150;
RewriteRule<UmuloEliminate> rule151;
RewriteRule<SmuloEliminate> rule152;
RewriteRule<UsuboEliminate> rule153;
RewriteRule<SsuboEliminate> rule154;
RewriteRule<SdivoEliminate> rule155;
};

template<> inline
Expand Down
64 changes: 0 additions & 64 deletions src/theory/bv/theory_bv_rewriter.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -710,70 +710,6 @@ RewriteResponse TheoryBVRewriter::RewriteEqual(TNode node, bool prerewrite)
}
}

RewriteResponse TheoryBVRewriter::RewriteNego(TNode node, bool prerewrite)
{
Node resultNode =
LinearRewriteStrategy<RewriteRule<NegoEliminate>>::apply(node);

return RewriteResponse(REWRITE_AGAIN, resultNode);
}

RewriteResponse TheoryBVRewriter::RewriteUaddo(TNode node, bool prerewrite)
{
Node resultNode =
LinearRewriteStrategy<RewriteRule<UaddoEliminate>>::apply(node);

return RewriteResponse(REWRITE_AGAIN, resultNode);
}

RewriteResponse TheoryBVRewriter::RewriteSaddo(TNode node, bool prerewrite)
{
Node resultNode =
LinearRewriteStrategy<RewriteRule<SaddoEliminate>>::apply(node);

return RewriteResponse(REWRITE_AGAIN, resultNode);
}

RewriteResponse TheoryBVRewriter::RewriteUmulo(TNode node, bool prerewrite)
{
Node resultNode =
LinearRewriteStrategy<RewriteRule<UmuloEliminate>>::apply(node);

return RewriteResponse(REWRITE_AGAIN, resultNode);
}

RewriteResponse TheoryBVRewriter::RewriteSmulo(TNode node, bool prerewrite)
{
Node resultNode =
LinearRewriteStrategy<RewriteRule<SmuloEliminate>>::apply(node);

return RewriteResponse(REWRITE_AGAIN, resultNode);
}

RewriteResponse TheoryBVRewriter::RewriteUsubo(TNode node, bool prerewrite)
{
Node resultNode =
LinearRewriteStrategy<RewriteRule<UsuboEliminate>>::apply(node);

return RewriteResponse(REWRITE_AGAIN, resultNode);
}

RewriteResponse TheoryBVRewriter::RewriteSsubo(TNode node, bool prerewrite)
{
Node resultNode =
LinearRewriteStrategy<RewriteRule<SsuboEliminate>>::apply(node);

return RewriteResponse(REWRITE_AGAIN, resultNode);
}

RewriteResponse TheoryBVRewriter::RewriteSdivo(TNode node, bool prerewrite)
{
Node resultNode =
LinearRewriteStrategy<RewriteRule<SdivoEliminate>>::apply(node);

return RewriteResponse(REWRITE_AGAIN, resultNode);
}

RewriteResponse TheoryBVRewriter::IdentityRewrite(TNode node, bool prerewrite)
{
return RewriteResponse(REWRITE_DONE, node);
Expand Down
8 changes: 0 additions & 8 deletions src/theory/bv/theory_bv_rewriter.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -89,14 +89,6 @@ class TheoryBVRewriter : public TheoryRewriter
static RewriteResponse RewriteRotateLeft(TNode node, bool prerewrite = false);
static RewriteResponse RewriteRedor(TNode node, bool prerewrite = false);
static RewriteResponse RewriteRedand(TNode node, bool prerewrite = false);
static RewriteResponse RewriteNego(TNode node, bool prerewrite = false);
static RewriteResponse RewriteUaddo(TNode node, bool prerewrite = false);
static RewriteResponse RewriteSaddo(TNode node, bool prerewrite = false);
static RewriteResponse RewriteUmulo(TNode node, bool prerewrite = false);
static RewriteResponse RewriteSmulo(TNode node, bool prerewrite = false);
static RewriteResponse RewriteUsubo(TNode node, bool prerewrite = false);
static RewriteResponse RewriteSsubo(TNode node, bool prerewrite = false);
static RewriteResponse RewriteSdivo(TNode node, bool prerewrite = false);
static RewriteResponse RewriteEagerAtom(TNode node, bool prerewrite = false);
static RewriteResponse RewriteSize(TNode node, bool prerewrite = false);
static RewriteResponse RewriteConstBvSym(TNode node, bool prerewrite = false);
Expand Down

0 comments on commit 90996d7

Please sign in to comment.