(holds cln)))
(holds cln)))))
-; Takes a `list` of literals and a clause, `suffix`, adds the suffix to each
-; literal and returns a list of clauses as a `cnf`.
-(program clause_add_suffix_all ((list clause) (suffix clause)) cnf
- (match list
- (cln cnfn)
- ((clc l rest) (cnfc (clc l suffix)
- (clause_add_suffix_all rest suffix)))))
+; Represents multiple conjoined clauses.
+; There is a list, `heads` of literals, each of which is suffixed by the
+; same `tail`.
+(declare common_tail_cnf_t type)
+(declare common_tail_cnf
+ (! heads clause
+ (! tail clause common_tail_cnf_t)))
+
+; A member of this type is a proof of a common_tail_cnf.
+(declare common_tail_cnf_holds
+ (! cnf common_tail_cnf_t type))
; This translates a definition witness value for the def:
;
(! def (definition new old others)
(! negOld lit
(! mkNegOld (^ (lit_flip old) negOld)
- (! provenCnf cnf
- (! mkProvenCnf (^ (clause_add_suffix_all
- others
- (clc (neg new) (clc old cln))) provenCnf)
; If you can prove bottom from its clausal representation
(! pf_continuation
; new v l_1 v l_2 v ... v l_n
; new v ~old
(! pf_c2 (holds (clc (pos new) (clc negOld cln)))
; for each i <= n: l_i v ~new v old
- (! pf_cs (cnf_holds provenCnf)
+ (! pf_cs (common_tail_cnf_holds
+ (common_tail_cnf
+ others
+ (clc (neg new) (clc old cln))))
(holds cln))))
; Then you've proven bottom
- (holds cln)))))))))))
+ (holds cln)))))))))
-; This axiom is useful for converting a proof of some CNF formula (a value of
-; type (cnf_holds ...)) into proofs of the constituent clauses (many values of
-; type (holds ...)).
+; These axioms are useful for converting a proof of some CNF formula represented
+; using the `common_tail_cnf` type (a value of type `common_tail_cnf_holds`),
+; into proofs of its constituent clauses (many values of type `holds`).
; Given
-; 1. a proof of some cnf, first ^ rest, and
-; 2. a proof continuation that
-; a. takes in proofs of
-; i. first and
-; ii. rest and
-; b. proceeds to prove bottom,
-; proves bottom.
-(declare cnfc_unroll_towards_bottom
- (! first clause
- (! rest cnf
- (! pf (cnf_holds (cnfc first rest))
- (! pf_continuation (! r1 (holds first) (! r2 (cnf_holds rest) (holds cln)))
- (holds cln))))))
-
+; 1. a proof of some `common_tail_cnf`
+; Then
+; 1. the first axiom gives you a proof of the first `clause` therein and
+; 2. the second gives you a proof of the rest of the `common_tail_cnf`.
+(declare common_tail_cnf_prove_head
+ (! first lit
+ (! rest clause
+ (! tail clause
+ (! pf (common_tail_cnf_holds (common_tail_cnf (clc first rest) tail))
+ (holds (clc first tail)))))))
+(declare common_tail_cnf_prove_tail
+ (! first lit
+ (! rest clause
+ (! tail clause
+ (! pf (common_tail_cnf_holds (common_tail_cnf (clc first rest) tail))
+ (common_tail_cnf_holds (common_tail_cnf rest tail)))))))
; Depends on er.plf
-; Type for representing success when testing a side-condition
-(declare TestSuccess type)
-
-; Test for clause_add_suffix_all
-(declare test_clause_add_suffix_all
- (! list clause
- (! suffix clause
- (! result cnf
- (! (^ (clause_add_suffix_all list suffix) result)
- TestSuccess)))))
-
-(check
- (% a lit
- (% b lit
- (% c lit
- (test_clause_add_suffix_all
- (clc a (clc b cln))
- (clc c cln)
- (cnfc (clc a (clc c cln))
- (cnfc (clc b (clc c cln))
- cnfn))
- )
- )))
-)
-
; This is a circuitous proof that uses the definition introduction and
; unrolling rules
(check
(clc (neg v2) cln)
(\ v3
(\ def3
- (clausify_definition _ _ _ def3 _ _
+ (clausify_definition _ _ _ def3 _
(\ pf_c5 ; type: (holds (clc (pos v3) (clc (neg v2) cln)))
(\ pf_c6 ; type: (holds (clc (pos v3) (clc (pos v1) cln)))
- (\ pf_cnf3 ; type: (cnf_holds (cnfc (clc (neg v2) (clc (neg v3) (clc (neg v1) cln))) cnfn))
- (cnfc_unroll_towards_bottom _ _ pf_cnf3
- (\ pf_c7 ; type: (clc (neg v2) (clc (neg v3) (clc (neg v1) cln)))
- (\ pf_cnfn
+ (\ pf_cnf ; type: (common_tail_cnf (clc (neg v2) cln) (clc (neg v3) (clc (neg v1) cln)))
+ (@ pf_c7 (common_tail_cnf_prove_head _ _ _ pf_cnf)
; Clauses
(satlem_simplify _ _ _ (R _ _ pf_c1 pf_c2 v1) (\ pf_c8 ; v2
(satlem_simplify _ _ _ (R _ _ pf_c8 pf_c5 v2) (\ pf_c9 ; v3
))
))
))
- )))
+ )
)))
)
))
cln
(\ v5
(\ def1
- (clausify_definition _ _ _ def1 _ _
+ (clausify_definition _ _ _ def1 _
(\ pf_c9 ; type: (holds (clc (pos def1v) cln))
(\ pf_c10 ; type: (holds (clc (pos def1v) (clc (pos v1) cln)))
- (\ idc0 ; type: (cnf_holds cnfn)
+ (\ idc0 ; type: (common_tail_cnf cln _)
(satlem_simplify _ _ _ (R _ _ pf_c10 pf_c7 v1) (\ pf_c11
(satlem_simplify _ _ _ (R _ _ pf_c10 pf_c5 v1) (\ pf_c12
(satlem_simplify _ _ _ (R _ _ pf_c10 pf_c2 v1) (\ pf_c13
#include <fstream>
#include <iostream>
#include <iterator>
+#include <sstream>
#include <unordered_set>
#include "base/check.h"
// Print Definitions
for (const ErDefinition& def : d_definitions)
{
- os << "\n (decl_rat_elimination_def ("
+ os << "\n (decl_definition ("
<< (def.d_oldLiteral.isNegated() ? "neg " : "pos ")
<< ProofManager::getVarName(def.d_oldLiteral.getSatVariable(), "bb")
<< ") ";
TraceCheckIdx firstDefClause = d_inputClauseIds.size() + 1;
for (const ErDefinition& def : d_definitions)
{
- os << "\n (clausify_rat_elimination_def _ _ _ "
- << "er.def " << def.d_newVariable << " _ _ (\\ er.c" << firstDefClause
+ os << "\n (clausify_definition _ _ _ "
+ << "er.def" << def.d_newVariable << " _ (\\ er.c" << firstDefClause
<< " (\\ er.c" << (firstDefClause + 1) << " (\\ er.cnf"
<< def.d_newVariable;
}
parenCount += 4 * d_definitions.size();
- // Unroll proofs of CNFs to proofs of clauses
+ // Unroll proofs of CNF to proofs of clauses
firstDefClause = d_inputClauseIds.size() + 1;
for (const ErDefinition& def : d_definitions)
{
for (size_t i = 0, n = def.d_otherLiterals.size(); i < n; ++i)
{
- os << "\n (cnfc_unroll _ _ ";
- os << "er.cnf" << def.d_newVariable;
+ // Compute the name of the CNF proof we're unrolling in this step
+ std::ostringstream previousCnfProof;
+ previousCnfProof << "er.cnf" << def.d_newVariable;
if (i != 0)
{
- os << ".u" << i;
+ // For all but the first unrolling, the previous CNF has an unrolling
+ // number attached
+ previousCnfProof << ".u" << i;
}
- os << " (\\ er.c" << (firstDefClause + 2 + i);
- os << " (\\ er.cnf" << def.d_newVariable << ".u" << (i + 1);
+
+ // Prove the first clause in the CNF
+ os << "\n (@ ";
+ os << "er.c" << (firstDefClause + 2 + i);
+ os << " (common_tail_cnf_prove_head _ _ _ " << previousCnfProof.str()
+ << ")";
+
+ // Prove the rest of the CNF
+ os << "\n (@ ";
+ os << "er.cnf" << def.d_newVariable << ".u" << (i + 1);
+ os << " (common_tail_cnf_prove_tail _ _ _ " << previousCnfProof.str()
+ << ")";
}
- parenCount += 3 * def.d_otherLiterals.size();
+ parenCount += 2 * def.d_otherLiterals.size();
firstDefClause += 2 + def.d_otherLiterals.size();
}
target_link_libraries(${name} main-test)
target_include_directories(${name} PRIVATE ${CxxTest_INCLUDE_DIR})
target_compile_definitions(${name} PRIVATE ${CVC4_CXXTEST_FLAGS_BLACK})
+ if(USE_LFSC)
+ # We don't link against LFSC, because CVC4 is already linked against it.
+ target_include_directories(${name} PRIVATE ${LFSC_INCLUDE_DIR})
+ endif()
if(${is_white})
target_compile_options(${name} PRIVATE -fno-access-control)
endif()
#include <cctype>
#include <iostream>
#include <iterator>
+#include <string>
#include <unordered_map>
#include <vector>
+#include "base/configuration_private.h"
#include "proof/clause_id.h"
#include "proof/er/er_proof.h"
#include "prop/sat_solver_types.h"
#include "utils.h"
+#if IS_LFSC_BUILD
+#include "lfscc.h"
+
+namespace CVC4 {
+namespace proof {
+extern const char* const plf_signatures;
+} // namespace proof
+} // namespace CVC4
+#endif
+
+
using namespace CVC4;
using namespace CVC4::proof::er;
using namespace CVC4::prop;
pf.outputAsLfsc(lfsc);
std::string out = R"EOF(
- (decl_rat_elimination_def
+ (decl_definition
(neg bb.v0)
cln
(\ er.v4
(\ er.def4
- (clausify_rat_elimination_def _ _ _ er.def4 _ _
+ (clausify_definition _ _ _ er.def4 _
(\ er.c9
(\ er.c10
(\ er.cnf4
SatLiteral(0, false), SatLiteral(1, true), SatLiteral(3, true)});
ErProof pf(clauses, usedIds, std::move(tc));
- std::ostringstream lfsc;
- pf.outputAsLfsc(lfsc);
+ std::ostringstream actual_pf_body;
+ pf.outputAsLfsc(actual_pf_body);
+
+#if IS_LFSC_BUILD
+ std::string pf_header = R"EOF(
+ (check
+ (% bb.v0 var
+ (% bb.v1 var
+ (% bb.v2 var
+ (% bb.v3 var
+ (% bb.pb1 (holds (clc (pos bb.v0) (clc (pos bb.v1) (clc (neg bb.v2) cln))))
+ (% bb.pb2 (holds (clc (neg bb.v0) (clc (neg bb.v1) (clc (pos bb.v2) cln))))
+ (% bb.pb3 (holds (clc (pos bb.v1) (clc (pos bb.v2) (clc (neg bb.v3) cln))))
+ (% bb.pb4 (holds (clc (neg bb.v1) (clc (neg bb.v2) (clc (pos bb.v3) cln))))
+ (% bb.pb5 (holds (clc (neg bb.v0) (clc (neg bb.v2) (clc (neg bb.v3) cln))))
+ (% bb.pb6 (holds (clc (pos bb.v0) (clc (pos bb.v2) (clc (pos bb.v3) cln))))
+ (% bb.pb7 (holds (clc (neg bb.v0) (clc (pos bb.v1) (clc (pos bb.v3) cln))))
+ (% bb.pb8 (holds (clc (pos bb.v0) (clc (neg bb.v1) (clc (neg bb.v3) cln))))
+ (: (holds cln)
+ )EOF";
- std::string out = R"EOF(
- (decl_rat_elimination_def
- (neg bb.v0)
- (clc (pos bb.v1) (clc (pos bb.v3) cln))
- (\ er.v4
- (\ er.def4
- (decl_rat_elimination_def
- (pos bb.v2)
- cln
- (\ er.v5
- (\ er.def5
- (clausify_rat_elimination_def _ _ _ er.def4 _ _
- (\ er.c9
- (\ er.c10
- (\ er.cnf4
- (clausify_rat_elimination_def _ _ _ er.def5 _ _
- (\ er.c13
- (\ er.c14
- (\ er.cnf5
- (cnfc_unroll _ _ er.cnf4
- (\ er.c11
- (\ er.cnf4.u1
- (cnfc_unroll _ _ er.cnf4.u1
- (\ er.c12
- (\ er.cnf4.u2
- (satlem_simplify _ _ _
- (R _ _ (R _ _ (Q _ _ (Q _ _ er.c11 bb.pb1 bb.v0)
- er.c10 er.v4)
- bb.pb7 bb.v0)
- bb.pb4 bb.v1) (\ er.c15
- (satlem_simplify _ _ _
- (Q _ _ (R _ _ bb.pb2 bb.pb5 bb.v2) bb.pb8 bb.v0) (\ er.c16
- (satlem_simplify _ _ _
- (Q _ _ (R _ _ bb.pb7 bb.pb2 bb.v1) bb.pb6 bb.v0) (\ er.c17
- (satlem_simplify _ _ _
- (Q _ _ (R _ _ bb.pb7 bb.pb5 bb.v3) bb.pb1 bb.v0) (\ er.c18
- (satlem_simplify _ _ _
- (R _ _ (Q _ _ bb.pb3 er.c17 bb.v3) er.c18 bb.v2) (\ er.c19
- (satlem_simplify _ _ _
- (Q _ _ (R _ _ (Q _ _ bb.pb4 er.c17 bb.v2) er.c16 bb.v3)
- er.c19 bb.v1) (\ er.c20
- er.c20 ; (holds cln)
- ))))))))))))
- )))
- )))
- )))
- )
- )))
- )
- ))
- )
- ))
+ std::string pf_footer = R"EOF(
+ )
+ ))))))))
+ ))))
)
)EOF";
- TS_ASSERT_EQUALS(filterWhitespace(lfsc.str()), filterWhitespace(out));
+ std::stringstream actual_pf;
+ actual_pf << proof::plf_signatures << pf_header << actual_pf_body.str() << pf_footer;
+
+ lfscc_init();
+ lfscc_check_file(actual_pf, false, false, false, false, false, false, false);
+#endif
}
projects / cvc5.git / commitdiff