* theories now get either an assertion from the SAT solver (normalized) or an (dis-)equality between two shared terms that is non-normalized
static RewriteResponse preRewrite(TNode n);
static RewriteResponse postRewrite(TNode n);
- static Node rewriteEquality(TNode equality) {
- // Arithmetic owns the domain, so this is totally ok
- return Rewriter::rewrite(equality);
- }
static void init() { }
}
}
// Propagate equality between shared terms
- Node equality = Rewriter::rewriteEquality(theory::THEORY_UF, t1.eqNode(t2));
- return d_arrays.propagate(equality);
+ return d_arrays.propagate(t1.eqNode(t2));
} else {
if (t1.getType().isArray()) {
if (!d_arrays.isShared(t1) || !d_arrays.isShared(t2)) {
return true;
}
}
- Node equality = Rewriter::rewriteEquality(theory::THEORY_UF, t1.eqNode(t2));
- return d_arrays.propagate(equality.notNode());
+ return d_arrays.propagate(t1.eqNode(t2).notNode());
}
return true;
}
return RewriteResponse(REWRITE_DONE, node);
}
- static Node rewriteEquality(TNode node) {
- return postRewrite(node).node;
- }
-
static inline void init() {}
static inline void shutdown() {}
return preRewrite(node);
}
- static Node rewriteEquality(TNode node) {
- Unreachable();
- return node;
- }
-
static void init() {}
static void shutdown() {}
}
}
- static inline Node rewriteEquality(TNode equality) {
- Unreachable();
- return equality;
- }
-
static inline void init() {}
static inline void shutdown() {}
BVDebug("bitvector-bitblast") << "Bitblasting node " << node <<"\n";
++d_statistics.d_numAtoms;
// the bitblasted definition of the atom
- Node atom_bb = d_atomBBStrategies[node.getKind()](node, this);
+ Node atom_bb = Rewriter::rewrite(d_atomBBStrategies[node.getKind()](node, this));
// asserting that the atom is true iff the definition holds
Node atom_definition = mkNode(kind::IFF, node, atom_bb);
- // do boolean simplifications if possible
- Node rewritten = Rewriter::rewrite(atom_definition);
if (!Options::current()->bitvectorEagerBitblast) {
- d_cnfStream->convertAndAssert(rewritten, true, false);
+ d_cnfStream->convertAndAssert(atom_definition, true, false);
d_bitblastedAtoms.insert(node);
} else {
- d_bvOutput->lemma(rewritten, false);
+ d_bvOutput->lemma(atom_definition, false);
}
}
static RewriteResponse preRewrite(TNode node);
- static Node rewriteEquality(TNode node) {
- Debug("bitvector") << "TheoryBV::rewriteEquality(" << node << ")" << std::endl;
- return postRewrite(node).node;
- }
-
static void init();
static void shutdown();
return RewriteResponse(REWRITE_DONE, in);
}
- static Node rewriteEquality(TNode equality) {
- return postRewrite(equality).node;
- }
-
static inline void init() {}
static inline void shutdown() {}
post_rewrite_get_cache=
post_rewrite_set_cache=
-rewrite_equality_calls=
-
seen_theory=false
seen_theory_builtin=false
post_rewrite_set_cache="${post_rewrite_set_cache} case ${theory_id}: return RewriteAttibute<${theory_id}>::setPostRewriteCache(node, cache);
"
- rewrite_equality_calls="${rewrite_equality_calls} case ${theory_id}: return ${class}::rewriteEquality(node);
-"
-
lineno=${BASH_LINENO[0]}
check_theory_seen
}
rewriter_includes \
pre_rewrite_calls \
post_rewrite_calls \
- rewrite_equality_calls \
pre_rewrite_get_cache \
post_rewrite_get_cache \
pre_rewrite_set_cache \
public:
static RewriteResponse preRewrite(TNode in);
static RewriteResponse postRewrite(TNode in);
- static Node rewriteEquality(TNode equality) {
- return postRewrite(equality).node;
- }
static inline void init() {}
static inline void shutdown() {}
private:
return rewriteTo(theory::Theory::theoryOf(node), node);
}
-Node Rewriter::rewriteEquality(theory::TheoryId theoryId, TNode node) {
- Assert(node.getKind() == kind::EQUAL);
- Trace("rewriter") << "Rewriter::rewriteEquality(" << theoryId << "," << node << ")"<< std::endl;
- Node result = Rewriter::callRewriteEquality(theoryId, node);
- Trace("rewriter") << "Rewriter::rewriteEquality(" << theoryId << "," << node << ") => " << result << std::endl;
- Assert(result.getKind() == kind::EQUAL || result.isConst());
- return result;
-}
-
Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
#ifdef CVC4_ASSERTIONS
*/
static Node rewrite(TNode node);
- /**
- * Rewrite an equality between two terms that are already in normal form, so
- * that the equality is in theory-normal form.
- */
- static Node rewriteEquality(theory::TheoryId theoryId, TNode node);
-
/**
* Should be called before the rewriter gets used for the first time.
*/
* Should be called to clean up any state.
*/
static void shutdown();
+
+
};/* class Rewriter */
}/* CVC4::theory namespace */
}
}
-Node Rewriter::callRewriteEquality(theory::TheoryId theoryId, TNode node) {
- switch(theoryId) {
-${rewrite_equality_calls}
- default:
- Unreachable();
- }
-}
-
Node Rewriter::getPreRewriteCache(theory::TheoryId theoryId, TNode node) {
switch(theoryId) {
${pre_rewrite_get_cache}
return RewriteResponse(REWRITE_DONE, node);
}
- /**
- * Rewrite an equality, in case special handling is required.
- */
- static Node rewriteEquality(TNode equality) {
- // often this will suffice
- return postRewrite(equality).node;
- }
-
/**
* Initialize the rewriter.
*/
Assert(!d_sharedTerms.areDisequal(carePair.a, carePair.b), "Please don't care about stuff you were notified about");
// The equality in question
- Node equality = Rewriter::rewriteEquality(carePair.theory, carePair.a.eqNode(carePair.b));
+ Node equality = carePair.a < carePair.b ?
+ carePair.a.eqNode(carePair.b) :
+ carePair.b.eqNode(carePair.a);
// Normalize the equality
Node normalizedEquality = Rewriter::rewrite(equality);
}
return;
}
-
- // We are left with internal distribution of shared literals
- Assert(atom.getKind() == kind::EQUAL);
- Node normalizedAtom = Rewriter::rewriteEquality(toTheoryId, atom);
- Node normalizedAssertion = polarity ? normalizedAtom : normalizedAtom.notNode();
-
- // If we normalize to true or false, it's a special case
- if (normalizedAtom.isConst()) {
- if (polarity == normalizedAtom.getConst<bool>()) {
- // Trivially true, just ignore
- return;
+
+ // See if it rewrites to true or false directly
+ Node normalizedLiteral = Rewriter::rewrite(assertion);
+ if (normalizedLiteral.isConst()) {
+ if (normalizedLiteral.getConst<bool>()) {
+ // trivially true, but theories need to share even trivially true facts
+ // unless of course it is the theory that normalized it
+ if (Theory::theoryOf(atom) == toTheoryId) {
+ return;
+ }
} else {
// Mark the propagation for explanations
- if (markPropagation(normalizedAssertion, assertion, toTheoryId, fromTheoryId)) {
+ if (markPropagation(normalizedLiteral, assertion, toTheoryId, fromTheoryId)) {
// Get the explanation (conflict will figure out where it came from)
- conflict(normalizedAssertion, toTheoryId);
+ conflict(normalizedLiteral, toTheoryId);
} else {
Unreachable();
}
return;
}
}
-
- // Try and assert
+
+ // Normalize to lhs < rhs
+ Assert(atom.getKind() == kind::EQUAL);
+ Assert(atom[0] != atom[1]);
+ Node normalizedAtom = atom;
+ if (atom[0] > atom[1]) {
+ normalizedAtom = atom[1].eqNode(atom[0]);
+ }
+ Node normalizedAssertion = polarity ? normalizedAtom : normalizedAtom.notNode();
+
+ // Try and assert (note that we assert the non-normalized one)
if (markPropagation(normalizedAssertion, assertion, toTheoryId, fromTheoryId)) {
// Check if has been pre-registered with the theory
- bool preregistered = d_propEngine->isSatLiteral(normalizedAssertion) && Theory::theoryOf(normalizedAtom) == toTheoryId;
+ bool preregistered = d_propEngine->isSatLiteral(normalizedAssertion) && Theory::theoryOf(normalizedAssertion) == toTheoryId;
// Assert away
theoryOf(toTheoryId)->assertFact(normalizedAssertion, preregistered);
d_factsAsserted = true;
Assert(properConflict(fullConflict));
lemma(fullConflict, true, true);
} else {
- Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "):" << std::endl;
-
// When only one theory, the conflict should need no processing
+ Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << ")" << std::endl;
Assert(properConflict(conflict));
lemma(conflict, true, true);
}
return RewriteResponse(REWRITE_DONE, node);
}
- static Node rewriteEquality(TNode equality) {
- return postRewrite(equality).node;
- }
-
static inline void init() {}
static inline void shutdown() {}
bug00.smt \
bug338.smt2 \
bug347.smt \
+ bug348.smt \
try5_small_difret_functions_wp_su.set_char_quoting.il.wp.delta01.smt \
diseqprop.01.smt \
wchains010ue.delta01.smt \
--- /dev/null
+(benchmark B_
+:logic QF_AUFBV
+:extrafuns ((start2 BitVec[32]))
+:extrafuns ((start1 BitVec[32]))
+:extrafuns ((a1 Array[32:8]))
+:status unsat
+:formula
+(let (?n1 bv0[1])
+(let (?n2 bv0[8])
+(let (?n3 (store a1 start1 ?n2))
+(let (?n4 bv3[32])
+(let (?n5 (bvadd ?n4 start1))
+(let (?n6 (store ?n3 ?n5 ?n2))
+(let (?n7 bv0[32])
+(let (?n8 (select ?n6 ?n7))
+(let (?n9 (bvnot ?n8))
+(let (?n10 (select ?n6 ?n7))
+(let (?n11 (bvnot ?n10))
+(let (?n12 (bvand ?n9 ?n11))
+(let (?n13 (bvnot ?n12))
+(let (?n14 (bvand ?n8 ?n10))
+(let (?n15 (bvnot ?n14))
+(let (?n16 (bvand ?n13 ?n15))
+(let (?n17 (bvnot ?n16))
+(let (?n18 (bvand ?n9 ?n17))
+(let (?n19 (bvnot ?n18))
+(let (?n20 (bvand ?n8 ?n16))
+(let (?n21 (bvnot ?n20))
+(let (?n22 (bvand ?n19 ?n21))
+(let (?n23 (store ?n6 ?n7 ?n22))
+(let (?n24 (bvnot ?n22))
+(let (?n25 (bvand ?n17 ?n24))
+(let (?n26 (bvnot ?n25))
+(let (?n27 (bvand ?n16 ?n22))
+(let (?n28 (bvnot ?n27))
+(let (?n29 (bvand ?n26 ?n28))
+(let (?n30 (store ?n23 ?n7 ?n29))
+(let (?n31 (bvadd ?n4 start2))
+(let (?n32 (select ?n30 ?n31))
+(let (?n33 (bvnot ?n32))
+(let (?n34 (select ?n30 start2))
+(let (?n35 (bvnot ?n34))
+(let (?n36 (bvand ?n33 ?n35))
+(let (?n37 (bvnot ?n36))
+(let (?n38 (bvand ?n32 ?n34))
+(let (?n39 (bvnot ?n38))
+(let (?n40 (bvand ?n37 ?n39))
+(let (?n41 (bvnot ?n40))
+(let (?n42 (bvand ?n33 ?n41))
+(let (?n43 (bvnot ?n42))
+(let (?n44 (bvand ?n32 ?n40))
+(let (?n45 (bvnot ?n44))
+(let (?n46 (bvand ?n43 ?n45))
+(let (?n47 (store ?n30 ?n31 ?n46))
+(let (?n48 (bvnot ?n46))
+(let (?n49 (bvand ?n41 ?n48))
+(let (?n50 (bvnot ?n49))
+(let (?n51 (bvand ?n40 ?n46))
+(let (?n52 (bvnot ?n51))
+(let (?n53 (bvand ?n50 ?n52))
+(let (?n54 (store ?n47 start2 ?n53))
+(let (?n55 (select ?n54 ?n7))
+(let (?n56 (bvnot ?n55))
+(let (?n57 (select ?n54 start2))
+(let (?n58 (bvnot ?n57))
+(let (?n59 (bvand ?n56 ?n58))
+(let (?n60 (bvnot ?n59))
+(let (?n61 (bvand ?n55 ?n57))
+(let (?n62 (bvnot ?n61))
+(let (?n63 (bvand ?n60 ?n62))
+(let (?n64 (bvnot ?n63))
+(let (?n65 (bvand ?n56 ?n64))
+(let (?n66 (bvnot ?n65))
+(let (?n67 (bvand ?n55 ?n63))
+(let (?n68 (bvnot ?n67))
+(let (?n69 (bvand ?n66 ?n68))
+(let (?n70 (store ?n54 ?n7 ?n69))
+(let (?n71 (bvnot ?n69))
+(let (?n72 (bvand ?n64 ?n71))
+(let (?n73 (bvnot ?n72))
+(let (?n74 (bvand ?n63 ?n69))
+(let (?n75 (bvnot ?n74))
+(let (?n76 (bvand ?n73 ?n75))
+(let (?n77 (store ?n70 start2 ?n76))
+(let (?n78 (select ?n77 ?n7))
+(let (?n79 (bvnot ?n78))
+(let (?n80 (select ?n77 ?n7))
+(let (?n81 (bvnot ?n80))
+(let (?n82 (bvand ?n79 ?n81))
+(let (?n83 (bvnot ?n82))
+(let (?n84 (bvand ?n78 ?n80))
+(let (?n85 (bvnot ?n84))
+(let (?n86 (bvand ?n83 ?n85))
+(let (?n87 (bvnot ?n86))
+(let (?n88 (bvand ?n79 ?n87))
+(let (?n89 (bvnot ?n88))
+(let (?n90 (bvand ?n78 ?n86))
+(let (?n91 (bvnot ?n90))
+(let (?n92 (bvand ?n89 ?n91))
+(let (?n93 (store ?n77 ?n7 ?n92))
+(let (?n94 (bvnot ?n92))
+(let (?n95 (bvand ?n87 ?n94))
+(let (?n96 (bvnot ?n95))
+(let (?n97 (bvand ?n86 ?n92))
+(let (?n98 (bvnot ?n97))
+(let (?n99 (bvand ?n96 ?n98))
+(let (?n100 (store ?n93 ?n7 ?n99))
+(let (?n101 (store a1 ?n5 ?n2))
+(let (?n102 (store ?n101 start1 ?n2))
+(let (?n103 (select ?n102 ?n7))
+(let (?n104 (store ?n102 ?n7 ?n103))
+(let (?n105 (select ?n102 ?n7))
+(let (?n106 (store ?n104 ?n7 ?n105))
+(let (?n107 (select ?n106 start2))
+(let (?n108 (store ?n106 ?n31 ?n107))
+(let (?n109 (select ?n106 ?n31))
+(let (?n110 (store ?n108 start2 ?n109))
+(let (?n111 (select ?n110 start2))
+(let (?n112 (store ?n110 ?n7 ?n111))
+(let (?n113 (select ?n110 ?n7))
+(let (?n114 (store ?n112 start2 ?n113))
+(let (?n115 (select ?n114 ?n7))
+(let (?n116 (store ?n114 ?n7 ?n115))
+(let (?n117 (select ?n114 ?n7))
+(let (?n118 (store ?n116 ?n7 ?n117))
+(flet ($n119 (= ?n100 ?n118))
+(let (?n120 bv1[1])
+(let (?n121 (ite $n119 ?n120 ?n1))
+(let (?n122 (bvnot ?n121))
+(flet ($n123 (= ?n1 ?n122))
+(flet ($n124 (not $n123))
+$n124
+)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
projects / cvc5.git / commitdiff