summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--proofs/signatures/smt.plf34
-rw-r--r--src/proof/array_proof.cpp18
-rw-r--r--src/proof/array_proof.h2
-rw-r--r--src/proof/cnf_proof.cpp3
-rw-r--r--src/proof/proof_manager.cpp3
-rw-r--r--src/proof/theory_proof.cpp84
-rw-r--r--src/proof/theory_proof.h20
-rw-r--r--src/proof/uf_proof.cpp21
-rw-r--r--src/proof/uf_proof.h2
-rw-r--r--test/regress/regress0/bt-test-00.smt21
-rw-r--r--test/regress/regress0/bt-test-01.smt21
-rw-r--r--test/regress/regress0/bug217.smt21
12 files changed, 128 insertions, 62 deletions
diff --git a/proofs/signatures/smt.plf b/proofs/signatures/smt.plf
index fa89a457f..6d04c3004 100644
--- a/proofs/signatures/smt.plf
+++ b/proofs/signatures/smt.plf
@@ -20,13 +20,13 @@
(! f1 formula
(! f2 formula
formula)))
-
+
(define formula_op3
(! f1 formula
(! f2 formula
(! f3 formula
formula))))
-
+
(declare not formula_op1)
(declare and formula_op2)
(declare or formula_op2)
@@ -76,6 +76,10 @@
(! u (th_holds (not (p_app x)))
(th_holds (= Bool x t_false)))))
+(declare f_to_b
+ (! f formula
+ (term Bool)))
+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;
; CNF Clausification
@@ -107,8 +111,8 @@
(! vbv (bvatom v bv_v)
(holds cln))))))
(holds cln))))
-
-
+
+
; clausify a formula directly
(declare clausify_form
(! f formula
@@ -116,14 +120,14 @@
(! a (atom v f)
(! u (th_holds f)
(holds (clc (pos v) cln)))))))
-
+
(declare clausify_form_not
(! f formula
(! v var
(! a (atom v f)
(! u (th_holds (not f))
(holds (clc (neg v) cln)))))))
-
+
(declare clausify_false
(! u (th_holds false)
(holds cln)))
@@ -134,7 +138,7 @@
(! u2 (! v (th_holds f) (holds cln))
(holds cln)))))
-
+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;
; Natural deduction rules : used for CNF
@@ -191,7 +195,7 @@
(! f2 formula
(! u2 (th_holds (not (or f1 f2)))
(th_holds (and (not f1) (not f2)))))))
-
+
;; and elimination
(declare and_elim_1
@@ -211,7 +215,7 @@
(! f2 formula
(! u2 (th_holds (not (and f1 f2)))
(th_holds (or (not f1) (not f2)))))))
-
+
;; impl elimination
(declare impl_intro (! f1 formula
@@ -231,7 +235,7 @@
(! f2 formula
(! u (th_holds (not (impl f1 f2)))
(th_holds (and f1 (not f2)))))))
-
+
;; iff elimination
(declare iff_elim_1
@@ -358,10 +362,10 @@
(! u (! o (holds (clc (neg bv_v) cln)) ;; l binding to be used in proof
(holds C))
(holds (clc (pos v) C))))))))))
-
+
(declare bv_ast
(! v var
- (! bv_v var
+ (! bv_v var
(! f formula
(! C clause
(! r (atom v f) ; this is specified
@@ -397,7 +401,7 @@
;; ...
;; (or_elim_1 _ _ l2
;; (or_elim_1 _ _ l1 A))))) ln)
-;;
+;;
;;))))))) (\ C
;;
;; We now have the free variable C, which should be the clause (v1 V ... V vn).
@@ -415,9 +419,7 @@
;; (contra _ l3
;; (or_elim_1 _ _ l2
;; (or_elim_1 _ _ (not_not_intro l1) A))))
-;;
+;;
;;))))))) (\ C
;;
;; C should be the clause (~v1 V v2 V ~v3 )
-
-
diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp
index cc60d8c07..af158f37b 100644
--- a/src/proof/array_proof.cpp
+++ b/src/proof/array_proof.cpp
@@ -1197,8 +1197,11 @@ void LFSCArrayProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetM
Assert ((term.getKind() == kind::SELECT) || (term.getKind() == kind::PARTIAL_SELECT_0) || (term.getKind() == kind::PARTIAL_SELECT_1) || (term.getKind() == kind::STORE));
switch (term.getKind()) {
- case kind::SELECT:
+ case kind::SELECT: {
Assert(term.getNumChildren() == 2);
+
+ bool convertToBool = (term[1].getType().isBoolean() && !d_proofEngine->printsAsBool(term[1]));
+
os << "(apply _ _ (apply _ _ (read ";
printSort(ArrayType(term[0].getType()).getIndexType(), os);
os << " ";
@@ -1206,9 +1209,12 @@ void LFSCArrayProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetM
os << ") ";
printTerm(term[0], os, map);
os << ") ";
+ if (convertToBool) os << "(f_to_b ";
printTerm(term[1], os, map);
+ if (convertToBool) os << ")";
os << ") ";
return;
+ }
case kind::PARTIAL_SELECT_0:
Assert(term.getNumChildren() == 1);
@@ -1381,7 +1387,15 @@ void LFSCArrayProof::printDeferredDeclarations(std::ostream& os, std::ostream& p
}
void LFSCArrayProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap) {
- // Nothing to do here at this point.
+ // Nothing to do here at this point.
+}
+
+bool LFSCArrayProof::printsAsBool(const Node &n)
+{
+ if (n.getKind() == kind::SELECT)
+ return true;
+
+ return false;
}
} /* CVC4 namespace */
diff --git a/src/proof/array_proof.h b/src/proof/array_proof.h
index 61f168a16..eaf2f47fb 100644
--- a/src/proof/array_proof.h
+++ b/src/proof/array_proof.h
@@ -125,6 +125,8 @@ public:
virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap);
+
+ bool printsAsBool(const Node &n);
};
diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp
index 69b613f28..d1a228ecb 100644
--- a/src/proof/cnf_proof.cpp
+++ b/src/proof/cnf_proof.cpp
@@ -350,8 +350,9 @@ void LFSCCnfProof::printAtomMapping(const std::set<Node>& atoms,
prop::SatVariable var = getLiteral(atom).getSatVariable();
//FIXME hideous
LFSCTheoryProofEngine* pe = (LFSCTheoryProofEngine*)ProofManager::currentPM()->getTheoryProofEngine();
- // pe->printLetTerm(atom.toExpr(), os);
+ if (pe->printsAsBool(atom.toExpr())) os << "(p_app ";
pe->printBoundTerm(atom.toExpr(), os, letMap);
+ if (pe->printsAsBool(atom.toExpr())) os << ")";
os << " (\\ " << ProofManager::getVarName(var, d_name);
os << " (\\ " << ProofManager::getAtomName(var, d_name) << "\n";
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 5ce615366..ddd2029fb 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -565,6 +565,7 @@ void LFSCProof::toStream(std::ostream& out) {
Debug("pf::pm") << "\t assertion = " << *it3 << std::endl;
std::set<Node> atoms;
+
NodePairSet rewrites;
// collects the atoms in the clauses
d_cnfProof->collectAtomsAndRewritesForLemmas(used_lemmas, atoms, rewrites);
@@ -779,7 +780,9 @@ void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions,
//TODO
os << "(trust_f ";
+ if (ProofManager::currentPM()->getTheoryProofEngine()->printsAsBool(*it)) os << "(p_app ";
ProofManager::currentPM()->getTheoryProofEngine()->printTheoryTerm((*it).toExpr(), os, globalLetMap);
+ if (ProofManager::currentPM()->getTheoryProofEngine()->printsAsBool(*it)) os << ")";
os << ") ";
os << "(\\ "<< ProofManager::getPreprocessedAssertionName(*it, "") << "\n";
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index 156c90e47..65f66ce29 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -299,14 +299,6 @@ void LFSCTheoryProofEngine::performExtraRegistrations() {
}
}
-void LFSCTheoryProofEngine::treatBoolsAsFormulas(bool value) {
- TheoryProofTable::const_iterator it = d_theoryProofTable.begin();
- TheoryProofTable::const_iterator end = d_theoryProofTable.end();
- for (; it != end; ++it) {
- it->second->treatBoolsAsFormulas(value);
- }
-}
-
void LFSCTheoryProofEngine::registerTermsFromAssertions() {
ProofManager::assertions_iterator it = ProofManager::currentPM()->begin_assertions();
ProofManager::assertions_iterator end = ProofManager::currentPM()->end_assertions();
@@ -330,7 +322,11 @@ void LFSCTheoryProofEngine::printAssertions(std::ostream& os, std::ostream& pare
// Assertions appear before the global let map, so we use a dummpMap to avoid letification here.
ProofLetMap dummyMap;
+
+ bool convertFromBool = (it->getType().isBoolean() && printsAsBool(*it));
+ if (convertFromBool) os << "(p_app ";
printBoundTerm(*it, os, dummyMap);
+ if (convertFromBool) os << ")";
os << ")\n";
paren << ")";
@@ -843,31 +839,47 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const Pro
Kind k = term.getKind();
switch(k) {
- case kind::ITE:
+ case kind::ITE: {
os << (term.getType().isBoolean() ? "(ifte ": "(ite _ ");
+ bool booleanCase = term[0].getType().isBoolean();
+ if (booleanCase && printsAsBool(term[0])) os << "(p_app ";
printBoundTerm(term[0], os, map);
+ if (booleanCase && printsAsBool(term[0])) os << ")";
+
os << " ";
printBoundTerm(term[1], os, map);
os << " ";
printBoundTerm(term[2], os, map);
os << ")";
return;
+ }
+
+ case kind::EQUAL: {
+ bool booleanCase = term[0].getType().isBoolean();
- case kind::EQUAL:
os << "(";
- if( term[0].getType().isBoolean() ){
+ if (booleanCase) {
os << "iff ";
- }else{
+ } else {
os << "= ";
printSort(term[0].getType(), os);
os << " ";
}
+
+ if (booleanCase && printsAsBool(term[0])) os << "(p_app ";
printBoundTerm(term[0], os, map);
+ if (booleanCase && printsAsBool(term[0])) os << ")";
+
os << " ";
+
+ if (booleanCase && printsAsBool(term[1])) os << "(p_app ";
printBoundTerm(term[1], os, map);
+ if (booleanCase && printsAsBool(term[1])) os << ") ";
os << ")";
+
return;
+ }
case kind::DISTINCT:
// Distinct nodes can have any number of chidlren.
@@ -917,9 +929,11 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const Pro
// arguments, so we have to flatten chained operators, like =.
Kind op = term.getOperator().getConst<Chain>().getOperator();
std::string op_str;
- if( op==kind::EQUAL && term[0].getType().isBoolean() ){
+ bool booleanCase;
+ if (op==kind::EQUAL && term[0].getType().isBoolean()) {
+ booleanCase = term[0].getType().isBoolean();
op_str = "iff";
- }else{
+ } else {
op_str = utils::toLFSCKind(op);
}
size_t n = term.getNumChildren();
@@ -930,9 +944,13 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const Pro
paren << ")";
}
os << "(" << op_str << " ";
+ if (booleanCase && printsAsBool(term[i - 1])) os << "(p_app ";
printBoundTerm(term[i - 1], os, map);
+ if (booleanCase && printsAsBool(term[i - 1])) os << ")";
os << " ";
+ if (booleanCase && printsAsBool(term[i])) os << "(p_app ";
printBoundTerm(term[i], os, map);
+ if (booleanCase && printsAsBool(term[i])) os << ")";
os << ")";
if(i + 1 < n) {
os << " ";
@@ -1049,6 +1067,15 @@ bool TheoryProofEngine::supportedTheory(theory::TheoryId id) {
id == theory::THEORY_BOOL);
}
+bool TheoryProofEngine::printsAsBool(const Node &n) {
+ if (!n.getType().isBoolean()) {
+ return false;
+ }
+
+ theory::TheoryId theory_id = theory::Theory::theoryOf(n);
+ return getTheoryProof(theory_id)->printsAsBool(n);
+}
+
BooleanProof::BooleanProof(TheoryProofEngine* proofEngine)
: TheoryProof(NULL, proofEngine)
{}
@@ -1068,10 +1095,7 @@ void BooleanProof::registerTerm(Expr term) {
void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) {
Assert (term.getType().isBoolean());
if (term.isVariable()) {
- if (d_treatBoolsAsFormulas)
- os << "(p_app " << ProofManager::sanitize(term) <<")";
- else
- os << ProofManager::sanitize(term);
+ os << ProofManager::sanitize(term);
return;
}
@@ -1116,7 +1140,11 @@ void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLe
std::ostringstream paren;
os << " ";
for (unsigned i = 0; i < term.getNumChildren(); ++i) {
+
+ if (printsAsBool(term[i])) os << "(p_app ";
d_proofEngine->printBoundTerm(term[i], os, map);
+ if (printsAsBool(term[i])) os << ")";
+
os << " ";
if(i < term.getNumChildren() - 2) {
os << "(" << utils::toLFSCKind(k) << " ";
@@ -1128,17 +1156,16 @@ void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLe
// this is for binary and unary operators
for (unsigned i = 0; i < term.getNumChildren(); ++i) {
os << " ";
+ if (printsAsBool(term[i])) os << "(p_app ";
d_proofEngine->printBoundTerm(term[i], os, map);
+ if (printsAsBool(term[i])) os << ")";
}
os << ")";
}
return;
case kind::CONST_BOOLEAN:
- if (d_treatBoolsAsFormulas)
- os << (term.getConst<bool>() ? "true" : "false");
- else
- os << (term.getConst<bool>() ? "t_true" : "t_false");
+ os << (term.getConst<bool>() ? "true" : "false");
return;
default:
@@ -1182,6 +1209,19 @@ void LFSCBooleanProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
Unreachable("No boolean lemmas yet!");
}
+bool LFSCBooleanProof::printsAsBool(const Node &n)
+{
+ Kind k = n.getKind();
+ switch (k) {
+ case kind::BOOLEAN_TERM_VARIABLE:
+ case kind::VARIABLE:
+ return true;
+
+ default:
+ return false;
+ }
+}
+
void TheoryProof::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap) {
// By default, we just print a trust statement. Specific theories can implement
// better proofs.
diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h
index 34248f7eb..bbdb7d6d7 100644
--- a/src/proof/theory_proof.h
+++ b/src/proof/theory_proof.h
@@ -151,9 +151,9 @@ public:
void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap);
- virtual void treatBoolsAsFormulas(bool value) {};
-
virtual void printTheoryTerm(Expr term, std::ostream& os, const ProofLetMap& map) = 0;
+
+ bool printsAsBool(const Node &n);
};
class LFSCTheoryProofEngine : public TheoryProofEngine {
@@ -182,7 +182,6 @@ public:
void performExtraRegistrations();
- void treatBoolsAsFormulas(bool value);
void finalizeBvConflicts(const IdToSatClause& lemmas, std::ostream& os);
private:
@@ -294,7 +293,11 @@ public:
*/
virtual void printRewriteProof(std::ostream& os, const Node &n1, const Node &n2);
- virtual void treatBoolsAsFormulas(bool value) {}
+ // Return true if node prints as bool, false if it prints as a formula.
+ virtual bool printsAsBool(const Node &n) {
+ // Most nodes print as formulas, so this is the default.
+ return false;
+ }
};
class BooleanProof : public TheoryProof {
@@ -318,7 +321,7 @@ public:
class LFSCBooleanProof : public BooleanProof {
public:
LFSCBooleanProof(TheoryProofEngine* proofEngine)
- : BooleanProof(proofEngine), d_treatBoolsAsFormulas(true)
+ : BooleanProof(proofEngine)
{}
virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map);
virtual void printOwnedSort(Type type, std::ostream& os);
@@ -328,12 +331,7 @@ public:
virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap);
- void treatBoolsAsFormulas(bool value) {
- d_treatBoolsAsFormulas = value;
- }
-
-private:
- bool d_treatBoolsAsFormulas;
+ bool printsAsBool(const Node &n);
};
} /* CVC4 namespace */
diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp
index 41262051c..d3da2bcdb 100644
--- a/src/proof/uf_proof.cpp
+++ b/src/proof/uf_proof.cpp
@@ -701,17 +701,13 @@ void LFSCUFProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap&
Assert (theory::Theory::theoryOf(term) == theory::THEORY_UF);
if (term.getKind() == kind::VARIABLE ||
- term.getKind() == kind::SKOLEM) {
+ term.getKind() == kind::SKOLEM ||
+ term.getKind() == kind::BOOLEAN_TERM_VARIABLE) {
os << term;
return;
}
- if (term.getKind() == kind::BOOLEAN_TERM_VARIABLE) {
- os << "(p_app " << term << ")";
- return;
- }
Assert (term.getKind() == kind::APPLY_UF);
- d_proofEngine->treatBoolsAsFormulas(false);
if(term.getType().isBoolean()) {
os << "(p_app ";
@@ -722,13 +718,15 @@ void LFSCUFProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap&
}
os << func << " ";
for (unsigned i = 0; i < term.getNumChildren(); ++i) {
+ bool convertToBool = (term[i].getType().isBoolean() && !d_proofEngine->printsAsBool(term[i]));
+ if (convertToBool) os << "(f_to_b ";
d_proofEngine->printBoundTerm(term[i], os, map);
+ if (convertToBool) os << ")";
os << ")";
}
if(term.getType().isBoolean()) {
os << ")";
}
- d_proofEngine->treatBoolsAsFormulas(true);
}
void LFSCUFProof::printOwnedSort(Type type, std::ostream& os) {
@@ -803,4 +801,13 @@ void LFSCUFProof::printAliasingDeclarations(std::ostream& os, std::ostream& pare
// Nothing to do here at this point.
}
+bool LFSCUFProof::printsAsBool(const Node &n)
+{
+ Debug("gk::temp") << "\nUF printsAsBool: " << n << std::endl;
+ if (n.getKind() == kind::BOOLEAN_TERM_VARIABLE)
+ return true;
+
+ return false;
+}
+
} /* namespace CVC4 */
diff --git a/src/proof/uf_proof.h b/src/proof/uf_proof.h
index ff0f9a879..221a50f43 100644
--- a/src/proof/uf_proof.h
+++ b/src/proof/uf_proof.h
@@ -71,6 +71,8 @@ public:
virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap);
+
+ bool printsAsBool(const Node &n);
};
diff --git a/test/regress/regress0/bt-test-00.smt2 b/test/regress/regress0/bt-test-00.smt2
index cd3e1137e..517806542 100644
--- a/test/regress/regress0/bt-test-00.smt2
+++ b/test/regress/regress0/bt-test-00.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE: --no-check-proofs
; EXPECT: unsat
(set-logic QF_UF)
(set-info :smt-lib-version 2.0)
diff --git a/test/regress/regress0/bt-test-01.smt2 b/test/regress/regress0/bt-test-01.smt2
index 918dcf9ec..e17bd2d7a 100644
--- a/test/regress/regress0/bt-test-01.smt2
+++ b/test/regress/regress0/bt-test-01.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE: --no-check-proofs
; EXPECT: unsat
(set-logic QF_UF)
(set-info :smt-lib-version 2.0)
diff --git a/test/regress/regress0/bug217.smt2 b/test/regress/regress0/bug217.smt2
index 34cfcad33..4d2e828b5 100644
--- a/test/regress/regress0/bug217.smt2
+++ b/test/regress/regress0/bug217.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE: --no-check-proofs
; EXPECT: unsat
(set-logic QF_UF)
(set-info :status unsat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback