summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--proofs/signatures/CMakeLists.txt4
-rw-r--r--proofs/signatures/rewrites.plf44
-rw-r--r--src/proof/rewrite_proof.cpp4
-rw-r--r--src/proof/rewrite_proof.h3
-rw-r--r--src/theory/bv/theory_bv_rewriter.cpp14
-rw-r--r--src/theory/rewriter.cpp24
-rwxr-xr-xsrc/theory/rewriter/compiler.py31
7 files changed, 116 insertions, 8 deletions
diff --git a/proofs/signatures/CMakeLists.txt b/proofs/signatures/CMakeLists.txt
index 698fa37fe..2b527aef3 100644
--- a/proofs/signatures/CMakeLists.txt
+++ b/proofs/signatures/CMakeLists.txt
@@ -17,6 +17,7 @@ set(core_signature_files
th_real.plf
th_int.plf
th_lira.plf
+ rewrites.plf
)
set(CORE_SIGNATURES "")
@@ -34,5 +35,8 @@ configure_file(
${CMAKE_CURRENT_SOURCE_DIR}/signatures.cpp.in
${CMAKE_CURRENT_BINARY_DIR}/signatures.cpp)
+set_property(DIRECTORY APPEND PROPERTY
+ CMAKE_CONFIGURE_DEPENDS ${core_signature_files})
+
libcvc4_add_sources(GENERATED signatures.cpp)
install(FILES ${core_signature_files} DESTINATION share/cvc4)
diff --git a/proofs/signatures/rewrites.plf b/proofs/signatures/rewrites.plf
new file mode 100644
index 000000000..2b5a7e7cc
--- /dev/null
+++ b/proofs/signatures/rewrites.plf
@@ -0,0 +1,44 @@
+(declare trusted_rewrite_f
+ (! x formula
+ (! y formula
+ (! u (th_holds (iff x y))
+ (! z formula
+ (th_holds (iff x z)))))))
+
+(declare symm_equal
+ (! s sort
+ (! x (term s)
+ (! y (term s)
+ (! z (term s)
+ (! w (term s)
+ (! u1 (th_holds (= s x y))
+ (! u2 (th_holds (= s z w))
+ (th_holds (iff (= s x z) (= s y w)))))))))))
+
+; Apply a unary operator to the original and the rewritten formula
+(declare symm_formula_op1
+ (! op formula_op1
+ (! x formula
+ (! y formula
+ (! u (th_holds (iff x y))
+ (th_holds (iff (op x) (op y))))))))
+
+; Apply a binary operator to the original and the rewritten formulas
+(declare symm_formula_op2
+ (! op formula_op2
+ (! x formula
+ (! y formula
+ (! z formula
+ (! w formula
+ (! u1 (th_holds (iff x z))
+ (! u2 (th_holds (iff y w))
+ (th_holds (iff (op x y) (op z w)))))))))))
+
+(declare neg_idemp
+ (! n mpz
+ (! x (term (BitVec n))
+ (! y (term (BitVec n))
+ (! u (th_holds (= (BitVec n) x (bvneg _ (bvneg _ y))))
+ (th_holds (= (BitVec n) x y)))))))
+
+(declare t_eq_n_f (th_holds (iff true (not false))))
diff --git a/src/proof/rewrite_proof.cpp b/src/proof/rewrite_proof.cpp
index 9f93e1259..e0b7c171c 100644
--- a/src/proof/rewrite_proof.cpp
+++ b/src/proof/rewrite_proof.cpp
@@ -135,12 +135,14 @@ RewriteStep* RewriteProof::getRewrite() const
return d_rewrites[0];
}
-void RewriteProof::registerRewrite(theory::rules::RewriteRule tag)
+void RewriteProof::registerRewrite(theory::rules::RewriteRule tag,
+ Node rewritten)
{
RewriteStep* topRewrite = d_rewrites.back();
d_rewrites.pop_back();
RewriteStep* newRewrite = new RewriteStep(tag, topRewrite->d_original);
newRewrite->d_children.push_back(topRewrite);
+ newRewrite->d_rewritten = rewritten;
d_rewrites.push_back(newRewrite);
}
diff --git a/src/proof/rewrite_proof.h b/src/proof/rewrite_proof.h
index 79b2c38fe..3fd2b7b7f 100644
--- a/src/proof/rewrite_proof.h
+++ b/src/proof/rewrite_proof.h
@@ -32,6 +32,7 @@ struct RewriteStep {
theory::rules::RewriteRule d_tag = theory::rules::RewriteRule::UNKNOWN;
// Node before the rewrite
Node d_original;
+ Node d_rewritten;
// Rewrite proofs for children
std::vector<RewriteStep *> d_children;
// Subproofs
@@ -79,7 +80,7 @@ public:
RewriteStep *getRewrite() const;
RewriteStep *getTopRewrite() const { return d_rewrites.back(); };
- void registerRewrite(theory::rules::RewriteRule tag);
+ void registerRewrite(theory::rules::RewriteRule tag, Node rewritten);
void registerSwap(const unsigned swap_id1, const unsigned swap_id2);
void replaceRewrite(RewriteStep *rewrite);
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 4a7400748..97189aab2 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -410,8 +410,14 @@ RewriteResponse TheoryBVRewriter::RewriteSub(TNode node, bool prerewrite){
}
RewriteResponse TheoryBVRewriter::RewriteNeg(TNode node, bool prerewrite) {
- Node resultNode = node;
-
+ Node resultNode = node;
+
+ RewriteResponse response = rules::NegIdemp(node);
+ if (response.d_node != node)
+ {
+ return response;
+ }
+
resultNode = LinearRewriteStrategy
< RewriteRule<EvalNeg>,
RewriteRule<NegIdemp>,
@@ -655,6 +661,10 @@ RewriteResponse TheoryBVRewriter::RewriteEqual(TNode node, bool prerewrite) {
RewriteRule<SimplifyEq>,
RewriteRule<ReflexivityEq>
>::apply(node);
+ if (resultNode != node)
+ {
+ return RewriteResponse(REWRITE_DONE, resultNode);
+ }
if(RewriteRule<SolveEq>::applies(resultNode)) {
resultNode = RewriteRule<SolveEq>::run<false>(resultNode);
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index ba9bb3a59..c9f7f5f67 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -205,6 +205,12 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node, RewriteProof* rp)
// Perform the pre-rewrite
RewriteResponse response =
preRewrite(rewriteStackTop.getTheoryId(), rewriteStackTop.d_node);
+
+ if (rp != nullptr && response.d_node != rewriteStackTop.d_node)
+ {
+ rp->registerRewrite(response.d_rule, response.d_node);
+ }
+
// Put the rewritten node to the top of the stack
rewriteStackTop.d_node = response.d_node;
TheoryId newTheory = theoryOf(rewriteStackTop.d_node);
@@ -294,6 +300,12 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node, RewriteProof* rp)
// Do the post-rewrite
RewriteResponse response =
postRewrite(rewriteStackTop.getTheoryId(), rewriteStackTop.d_node);
+
+ if (rp != nullptr && response.d_node != rewriteStackTop.d_node)
+ {
+ rp->registerRewrite(response.d_rule, response.d_node);
+ }
+
// We continue with the response we got
TheoryId newTheoryId = theoryOf(response.d_node);
if (newTheoryId != rewriteStackTop.getTheoryId()
@@ -307,8 +319,16 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node, RewriteProof* rp)
== d_rewriteStack->end());
d_rewriteStack->insert(response.d_node);
#endif
- Node rewritten = rewriteTo(newTheoryId, response.d_node, rp);
- rewriteStackTop.d_node = rewritten;
+ if (rp == nullptr)
+ {
+ rewriteStackTop.d_node = rewrite(response.d_node);
+ }
+ else
+ {
+ RewriteProof subRp;
+ Node rewritten = rewriteTo(theoryOf(node), response.d_node, &subRp);
+ rewriteStackTop.d_node = rewritten;
+ }
#ifdef CVC4_ASSERTIONS
d_rewriteStack->erase(response.d_node);
#endif
diff --git a/src/theory/rewriter/compiler.py b/src/theory/rewriter/compiler.py
index 46f9f2e54..75d73d2d4 100755
--- a/src/theory/rewriter/compiler.py
+++ b/src/theory/rewriter/compiler.py
@@ -162,13 +162,13 @@ def gen_rule_printer(rule):
rule_printer_pattern = """
if (step->d_tag == RewriteRule::{})
{{
- os << "({} ";
+ os << "({} _ _ _ ";
printRewriteProof(useCache, tp, step->d_children[0], os, globalLetMap);
os << ")";
return;
}}
"""
- return rule_printer_pattern.format(name_to_enum(rule.name), rule.name)
+ return rule_printer_pattern.format(name_to_enum(rule.name), name_to_enum(rule.name).lower())
def gen_proof_printer(rules):
@@ -223,6 +223,14 @@ def gen_proof_printer(rules):
return;
}}
+ case kind::BITVECTOR_NEG:
+ {{
+ os << "(symm_formula_op1 bvneg _ _ ";
+ printRewriteProof(useCache, tp, step->d_children[0], os, globalLetMap);
+ os << ")";
+ return;
+ }}
+
case kind::IMPLIES:
{{
os << "(symm_formula_op2 impl _ _ _ _ ";
@@ -243,9 +251,28 @@ def gen_proof_printer(rules):
return;
}}
+ case kind::EQUAL:
+ {{
+ os << "(symm_equal _ _ _ _ _ ";
+ printRewriteProof(useCache, tp, step->d_children[0], os, globalLetMap);
+ os << " ";
+ printRewriteProof(useCache, tp, step->d_children[1], os, globalLetMap);
+ os << ")";
+ return;
+ }}
+
default: Unimplemented();
}}
}}
+ else if (step->d_tag == RewriteRule::UNKNOWN)
+ {{
+ os << "(trusted_rewrite_f _ _ ";
+ printRewriteProof(useCache, tp, step->d_children[0], os, globalLetMap);
+ os << " ";
+ tp->printTheoryTerm(step->d_rewritten.toExpr(), os, globalLetMap);
+ os << ")";
+ return;
+ }}
{}
}}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback