From: Haniel Barbosa Date: Thu, 25 Mar 2021 04:26:17 +0000 (-0300) Subject: Deleting old LFSC signatures (#6194) X-Git-Tag: cvc5-1.0.0~2032 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b3c6975af6354eb027aa52d6a23386b5dd0ef1cd;p=cvc5.git Deleting old LFSC signatures (#6194) --- diff --git a/proofs/signatures/CMakeLists.txt b/proofs/signatures/CMakeLists.txt deleted file mode 100644 index 698fa37fe..000000000 --- a/proofs/signatures/CMakeLists.txt +++ /dev/null @@ -1,38 +0,0 @@ -# These CORE_PLFs are combined to give a "master signature" against which -# proofs are checked internally when using --check-proofs. To add support for -# more theories, just list them here in the same order you would to the LFSC -# proof-checker binary. - -set(core_signature_files - sat.plf - er.plf - smt.plf - th_base.plf - lrat.plf - drat.plf - th_arrays.plf - th_bv.plf - th_bv_bitblast.plf - th_bv_rewrites.plf - th_real.plf - th_int.plf - th_lira.plf -) - -set(CORE_SIGNATURES "") - -foreach(f ${core_signature_files}) - file(READ ${f} tmp) - set(CORE_SIGNATURES "${CORE_SIGNATURES}\n${tmp}") -endforeach(f) - -string(REPLACE "\\" "\\\\" CORE_SIGNATURES "${CORE_SIGNATURES}") -string(REPLACE "\"" "\\\"" CORE_SIGNATURES "${CORE_SIGNATURES}") -string(REPLACE "\n" "\\n\\\n" CORE_SIGNATURES "${CORE_SIGNATURES}") - -configure_file( - ${CMAKE_CURRENT_SOURCE_DIR}/signatures.cpp.in - ${CMAKE_CURRENT_BINARY_DIR}/signatures.cpp) - -libcvc4_add_sources(GENERATED signatures.cpp) -install(FILES ${core_signature_files} DESTINATION share/cvc4) diff --git a/proofs/signatures/drat.plf b/proofs/signatures/drat.plf deleted file mode 100644 index 20795901f..000000000 --- a/proofs/signatures/drat.plf +++ /dev/null @@ -1,393 +0,0 @@ -; Deps: lrat.plf -; -; Implementation of DRAT checking. -; -; Unfortunately, there are **two** different notions of DRAT floating around in -; the world: -; * Specified DRAT : This is a reasonable proof format -; * Operational DRAT : This is a variant of specified DRAT warped by the -; details of common SAT solver architectures. -; -; Both are detailed in this paper, along with their differences: -; http://fmv.jku.at/papers/RebolaPardoBiere-POS18.pdf -; -; This signature contains implementations for a checker for each. -; **Specified DRAT** is first. - -; A DRAT proof itself: a list of addition or deletion instructions. -(declare DRATProof type) -(declare DRATProofn DRATProof) -(declare DRATProofa (! c clause (! p DRATProof DRATProof))) -(declare DRATProofd (! c clause (! p DRATProof DRATProof))) - -; ==================== ; -; Functional Programs ; -; ==================== ; - -; Are two clauses equal (i.e., if interpretted as sets of literals, are those -; sets equal?) -; -; Assumes that marks 1,2,3,4 are clear for the constituent variables, and -; leaves them clear afterwards. -; -; Since clauses are sets, it is insufficient to do list equality. -; We could sort them, but that would require defining an order on our variables, -; and incurring the cost of sorting. -; -; -; Instead, we do the following: -; 1. Sweep the first clause, marking variables with flags 1,3 (pos) and 2,4 (neg) -; 2. Sweep the second clause, erasing marks 1,2. Returning FALSE if no mark 3,4. -; 3. Unsweep the first clause, returning FALSE on marks 1,2. -; Also unmarking 3,4, and 1,2 if needed -; -; So the mark 1 means (seen as + in c1, but not yet in c2) -; the mark 3 means (seen as + in c1) -; the mark 2 means (seen as - in c1, but not yet in c2) -; the mark 4 means (seen as - in c1) -; -; This implementation **does not**: -; 1. assume that clauses do not have duplicates -; (so the clause [x v x v ~y] is an accceptable input) -; 2. assume that clauses are non-tautological -; (so the clause [x v ~x] is an acceptable input) -; -; TODO(aozdemir) This implementation could be further optimized b/c once c1 is -; drained, we need not continue to pattern match on it. -(program clause_eq ((c1 clause) (c2 clause)) bool - (match - c1 - (cln (match - c2 - (cln tt) - ((clc c2h c2t) (match - c2h - ((pos v) - (ifmarked1 - v - (do (markvar1 v) - (clause_eq c1 c2t)) - (ifmarked3 - v - (clause_eq c1 c2t) - ff))) - ((neg v) - (ifmarked2 - v - (do (markvar2 v) - (clause_eq c1 c2t)) - (ifmarked4 - v - (clause_eq c1 c2t) - ff))))))) - ((clc c1h c1t) (match - c1h - ((pos v) - (ifmarked3 - v - (clause_eq c1t c2) - (do (markvar3 v) - (do (markvar1 v) - (let res (clause_eq c1t c2) - (do (markvar3 v) - (ifmarked1 - v - (do (markvar1 v) ff) - res))))))) - ((neg v) - (ifmarked4 - v - (clause_eq c1t c2) - (do (markvar4 v) - (do (markvar2 v) - (let res (clause_eq c1t c2) - (do (markvar4 v) - (ifmarked2 - v - (do (markvar2 v) ff) - res))))))))))) - - -; Does this formula contain bottom as one of its clauses? -(program cnf_has_bottom ((cs cnf)) bool - (match cs - (cnfn ff) - ((cnfc c rest) (match c - (cln tt) - ((clc l c') (cnf_has_bottom rest)))))) - -; Return a new cnf with one copy of this clause removed. -; If the clause is absent, returns the original cnf. -(program cnf_remove_clause ((c clause) (cs cnf)) cnf - (match cs - (cnfn cnfn) - ((cnfc c' cs') - (match (clause_eq c c') - (tt cs') - (ff (cnfc c' (cnf_remove_clause c cs'))))))) - -; return (c1 union (c2 \ ~l)) -; Significant for how a RAT is defined. -(program clause_pseudo_resolvent ((c1 clause) (c2 clause)) clause - (clause_dedup (clause_append c1 - (clause_remove_all - (lit_flip (clause_head c1)) c2)))) - -; Given a formula, `cs` and a clause `c`, return all pseudo resolvents, i.e. all -; (c union (c' \ ~head(c))) -; for c' in cs, where c' contains ~head(c) -(program collect_pseudo_resolvents ((cs cnf) (c clause)) cnf - (match cs - (cnfn cnfn) - ((cnfc c' cs') - (let rest_of_resolvents (collect_pseudo_resolvents cs' c) - (match (clause_contains_lit c' (lit_flip (clause_head c))) - (tt (cnfc (clause_pseudo_resolvent - c - c') - rest_of_resolvents)) - (ff rest_of_resolvents)))))) - -; =============================================================== ; -; Unit Propegation implementation (manipulates global assignment) ; -; =============================================================== ; -; See the lrat file for a description of the global assignment. - -; The result of search for a unit clause in -(declare UnitSearchResult type) -; There was a unit, and -; this is the (previously floating) literal that is now satisfied. -; this is a version of the input cnf with satisfied clauses removed. -(declare USRUnit (! l lit (! f cnf UnitSearchResult))) -; There was an unsat clause -(declare USRBottom UnitSearchResult) -; There was no unit. -(declare USRNoUnit UnitSearchResult) - -; If a UnitSearchResult is a Unit, containing a cnf, adds this clause to that -; cnf. Otherwise, returns the UnitSearchResult unmodified. -(program USR_add_clause ((c clause) (usr UnitSearchResult)) UnitSearchResult - (match usr - ((USRUnit l f) (USRUnit l (cnfc c f))) - (USRBottom USRBottom) - (USRNoUnit USRNoUnit))) - -; Searches through the clauses, looking for a unit clause. -; Reads the global assignment. Possibly assigns one variable. -; Returns -; USRBottom if there is an unsat clause -; (USRUnit l f) if there is a unit, with lit l, and -; f is the cnf with some SAT clauses removed. -; USRNoUnit if there is no unit -(program unit_search ((f cnf)) UnitSearchResult - (match f - (cnfn USRNoUnit) - ((cnfc c f') - (match (clause_check_unit_and_maybe_mark c) - (MRSat (unit_search f')) - ((MRUnit l) (USRUnit l f')) - (MRUnsat USRBottom) - (MRNotUnit (USR_add_clause c (unit_search f'))))))) - - -; Given the current global assignment, does the formula `f` imply bottom via -; unit propegation? Leaves the global assignment in the same state that it was -; initially. -(program unit_propegates_to_bottom ((f cnf)) bool - (match (unit_search f) - (USRBottom tt) - ((USRUnit l f') (let result (unit_propegates_to_bottom f') - (do (lit_un_mk_sat l) - result))) - (USRNoUnit ff))) - -; ================================== ; -; High-Level DRAT checking functions ; -; ================================== ; - -; Is this clause an AT? -(program is_at ((cs cnf) (c clause)) bool - (match (is_t c) - (tt tt) - (ff (do (clause_mk_all_unsat c) - (let r (unit_propegates_to_bottom cs) - (do (clause_un_mk_all_unsat c) - r)))))) - -; Are all of these clauses ATs? -(program are_all_at ((cs cnf) (clauses cnf)) bool - (match clauses - (cnfn tt) - ((cnfc c clauses') - (match (is_at cs c) - (tt (are_all_at cs clauses')) - (ff ff))))) - -; Is the clause `c` a RAT for the formula `cs`? -(program is_rat ((cs cnf) (c clause)) bool - (match (is_t c) - (tt tt) - (ff (match (is_at cs c) - (tt tt) - (ff (match c - (cln ff) - ((clc a b) (are_all_at ; dedent - cs - (collect_pseudo_resolvents cs c))))))))) - -; Is this proof a valid DRAT proof of bottom? -(program is_specified_drat_proof ((f cnf) (proof DRATProof)) bool - (match proof - (DRATProofn (cnf_has_bottom f)) - ((DRATProofa c p) (match - (is_rat f c) - (tt (is_specified_drat_proof (cnfc c f) p)) - (ff ff))) - ((DRATProofd c p) - (is_specified_drat_proof (cnf_remove_clause c f) p)))) - - -; =============================== ; -; Operational DRAT implementation ; -; =============================== ; - -; Operation DRAT is defined in the paper "Two Flavors of DRAT". -; Below is an extension of the DRAT signature to handle it. - -; Notes on types. -; For operational DRAT it is useful to manifest partial assignments in values -; (although we still use the global assignment in some places). To this end, -; literals are used to represent single-variable assignments ((pos v) denotes -; {v maps to true}) and clauses are partial assignments by way of being -; literal lists. - -; Copy the partial assignment represented by a clause into the global -; assignment. Fails if that clause represents an inconsistent partial -; assignment (e.g. v is both true and false) -(program clause_into_global ((a clause)) Unit - (match a - (cln unit) - ((clc l rest) - (do (lit_mk_sat l) (clause_into_global rest))))) - -; Remove the partial assignment represented by c from the global assignment -(program clause_undo_into_global ((a clause)) Unit - (match a - (cln unit) - ((clc l rest) - (do (lit_un_mk_sat l) (clause_undo_into_global rest))))) - -; Does this clause have no floating literals w.r.t. the global assignment? -(program clause_no_floating ((c clause)) bool - (match c - (cln tt) - ((clc l rest) (match (lit_is_floating l) - (tt ff) - (ff (clause_no_floating rest)))))) - -; Does this clause have no sat literals w.r.t. the global assignment? -(program clause_no_sat ((c clause)) bool - (match c - (cln tt) - ((clc l rest) (match (lit_is_sat l) - (tt ff) - (ff (clause_no_sat rest)))))) - -; Does this clause have one sat literal w.r.t. the global assignment? -(program clause_one_sat ((c clause)) bool - (match c - (cln ff) - ((clc l rest) (match (lit_is_sat l) - (tt (clause_no_sat rest)) - (ff (clause_one_sat rest)))))) - -; Is this clause a unit clause w.r.t. the global assignment? -; This notion is defined as: -; * A clause where no literals are floating, and exactly one is sat. -(program clause_is_unit_wrt_up_model ((c clause) (up_model clause)) bool - (let c' (clause_dedup c) - (do (clause_into_global up_model) - (let result (match (clause_no_floating c') - (tt (clause_one_sat c')) - (ff ff)) - (do (clause_undo_into_global up_model) - result))))) - -; Result from constructing a UP model (defined in "Two Flavors of DRAT") -; Technically, we're constructing the shared UP model -- the intersection of all -; UP models. -; Informally, this is just the partial assignment implied by UP. -; -; This type is necessary, because constructing a UP model can reveal an -; inconsistent UP model -- one which assigns some variable to true and false. -; This would break our machinery, so we special case it. -(declare UPConstructionResult type) -; An actual model -(declare UPCRModel (! up_model clause UPConstructionResult)) -; Bottom is implied! -(declare UPCRBottom UPConstructionResult) - - -; Do unit propagation on `f`, constructing a UP model for it. -(program build_up_model ((f cnf)) UPConstructionResult - (match (unit_search f) - (USRBottom UPCRBottom) - (USRNoUnit (UPCRModel cln)) - ((USRUnit l f') - (let result (build_up_model f') - (do (lit_un_mk_sat l) - (match result - (UPCRBottom UPCRBottom) - ((UPCRModel model) (UPCRModel (clc l model))))))))) - -; Given some starting assignment (`up_model`), continue UP to construct a larger -; model. -(program extend_up_model ((f cnf) (up_model clause)) UPConstructionResult - (do (clause_into_global up_model) - (let result (build_up_model f) - (do (clause_undo_into_global up_model) - (match result - (UPCRBottom UPCRBottom) - ((UPCRModel up_model') - (UPCRModel (clause_append up_model up_model')))))))) - -; Helper for `is_operational_drat_proof` which takes a UP model for the working -; formula. The UP model is important for determining which clause deletions -; actually are executed in operational DRAT. Passing the UP model along -; prevents it from being fully recomputed every time. -(program is_operational_drat_proof_h ((f cnf) (up_model clause) (pf DRATProof)) bool - (match pf - (DRATProofn (cnf_has_bottom f)) - ((DRATProofd c pf') - (match (clause_is_unit_wrt_up_model c up_model) - (tt (is_operational_drat_proof_h f up_model pf')) - (ff (is_operational_drat_proof_h - (cnf_remove_clause c f) up_model pf')))) - ((DRATProofa c pf') - (let f' (cnfc c f) - (match (is_rat f c) - (tt (match (extend_up_model f' up_model) - (UPCRBottom tt) - ((UPCRModel up_model') - (is_operational_drat_proof_h f' up_model' pf')))) - (ff ff)))))) - -; Is this an operational DRAT proof of bottom for this formula? -(program is_operational_drat_proof ((f cnf) (pf DRATProof)) bool - (match (build_up_model f) - (UPCRBottom tt) - ((UPCRModel model) (is_operational_drat_proof_h f model pf)))) - -; Is this a specified or operational DRAT proof of bottom for this formula? -(program is_drat_proof ((f cnf) (pf DRATProof)) bool - (match (is_specified_drat_proof f pf) - (tt tt) - (ff (is_operational_drat_proof f pf)))) - -(declare drat_proof_of_bottom - (! f cnf - (! proof_of_formula (cnf_holds f) - (! proof DRATProof - (! sc (^ (is_drat_proof f proof) tt) - bottom))))) - diff --git a/proofs/signatures/er.plf b/proofs/signatures/er.plf deleted file mode 100644 index 6a8a059a2..000000000 --- a/proofs/signatures/er.plf +++ /dev/null @@ -1,130 +0,0 @@ -; Deps: sat.plf - -; This file exists to support the **definition introduction** (or **extension**) -; rule in the paper: -; "Extended Resolution Simulates DRAT" -; which can be found at http://www.cs.utexas.edu/~marijn/publications/ijcar18.pdf -; -; The core idea of extended resolution is that given **any** formula f -; involving the variables from some SAT problem, one can introduce the -; constraint -; -; new <=> f -; -; without changing satisfiability, where "new" is a fresh variable. -; -; This signature does not provide axioms for facilitating full use of this -; idea. Instead, this signature facilitates use of one specific kind of -; extension, that of the form: -; -; new <=> old v (~l_1 ^ ~l_2 ^ ... ^ ~l_n) -; -; which translates into the clauses: -; -; new v l_1 v l_2 v ... v l_n -; new v ~old -; for each i <= n: l_i v ~new v old -; -; This kind of extension is (a) sufficient to simulate DRAT proofs and (b) easy -; to convert to clauses, which is why we use it. - -; A definition witness value for: -; new <=> old v (~others_1 ^ ~others_2 ^ ... ^ ~others_n) -; It witnesses the fact that new was fresh when it was defined by the above. -; -; Thus it witnesses that the above, when added to the formula consisting of the -; conjunction all the already-proven clauses, produces an equisatisfiable -; formula. -(declare definition (! new var (! old lit (! others clause type)))) - -; Given `old` and `others`, this takes a continuation which expects -; 1. a fresh variable `new` -; 2. a definition witness value for: -; new <=> old v (~others_1 ^ ~others_2 ^ ... ^ ~others_n) -; -; Aside: -; In programming a **continuation** of some computation is a function that -; takes the results of that computation as arguments to produce a final -; result. -; -; In proof-construction a **continuation** of some reasoning is a function -; that takes the results of that reasoning as arguments to proof a final -; result. -; -; That definition witness value can be clausified using the rule below. -; -; There need to be two different rules because the side-condition for -; clausification needs access to the new variable, which doesn't exist except -; inside the continuation, which is out-of-scope for any side-condition -; associated with this rule. -(declare decl_definition - (! old lit - (! others clause ; List of vars - (! pf_continuation (! new var (! def (definition new old others) - (holds cln))) - (holds cln))))) - -; 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: -; -; new <=> old v (~l_1 ^ ~l_2 ^ ... ^ ~l_n) -; -; into the clauses: -; -; new v l_1 v l_2 v ... v l_n -; new v ~old -; for each i <= n: l_i v ~new v old (encoded as (cnf_holds ...)) -(declare clausify_definition - (! new var - (! old lit - (! others clause - ; Given a definition { new <-> old v (~l_1 ^ ~l_2 ^ ... ^ ~l_n) } - (! def (definition new old others) - (! negOld lit - (! mkNegOld (^ (lit_flip old) negOld) - ; If you can prove bottom from its clausal representation - (! pf_continuation - ; new v l_1 v l_2 v ... v l_n - (! pf_c1 (holds (clc (pos new) others)) - ; new v ~old - (! pf_c2 (holds (clc (pos new) (clc negOld cln))) - ; for each i <= n: l_i v ~new v old - (! 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))))))))) - -; 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 `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))))))) diff --git a/proofs/signatures/lrat.plf b/proofs/signatures/lrat.plf deleted file mode 100644 index c10f8d6c8..000000000 --- a/proofs/signatures/lrat.plf +++ /dev/null @@ -1,568 +0,0 @@ -; LRAT Proof signature -; LRAT format detailed in "Efficient Certified RAT Verification" -; Link: https://www.cs.utexas.edu/~marijn/publications/lrat.pdf -; Author: aozdemir -; Deps: sat.plf smt.plf - - -; A general note about the design of the side conditions: -; Some side-conditions make use of a _global assignment_ encoded in -; 0 (true) / 1 (false) marks on variables. - -; Unit (https://en.wikipedia.org/wiki/Unit_type) -; For functions that don't return anything -(declare Unit type) ; The type with only one value (like `void` in C) -(declare unit Unit) ; That value - -; Boolean operator (not short-circuiting) -(program bool_or ((l bool) (r bool)) bool (match l (ff r) (tt tt))) -(program bool_and ((l bool) (r bool)) bool (match l (tt r) (ff ff))) -(program bool_not ((b bool)) bool (match b (tt ff) (ff tt))) -(program bool_eq ((l bool) (r bool)) bool - (match l - (tt (match r - (tt tt) - (ff ff))) - (ff (match r - (tt ff) - (ff tt))))) - -; =================== ; -; Working CNF formula ; -; =================== ; - -; Represents a CNF formula as a map from clause indices to clauses -; Should be sorted ascending, always! -; Here, and for all collections, the suffix "n" denotes the empty collection and -; the suffix "c" denotes the constructor for the collection in the style of lisp's -; "cons cells" -(declare CMap type) -(declare CMapn CMap) -(declare CMapc (! i mpz (! c clause (! r CMap CMap)))) - -; ================= ; -; LRAT Proof Format ; -; ================= ; - -; CI lists are lists of clause indices. -; They represent clauses to delete. -; They must be sorted. -(declare CIList type) -(declare CIListn CIList) -(declare CIListc (! z mpz (! zs CIList CIList))) - -; Traces are a list of clause indices into the working CNF formula -; They represent the clauses that will be unit in a unit propegation to bottom -; Thus their elements are *not* in value order. -(declare Trace type) -(declare Tracen Trace) -(declare Tracec (! z mpz (! zs Trace Trace))) - -; RAT Hint list -; Each hint is -; * An index indicating a clause in the working CNF formula to resolve with -; * A trace indicating how UP should be done after that resolution -(declare RATHints type) -(declare RATHintsn RATHints) -(declare RATHintsc - (! target mpz - (! trace Trace - (! rest RATHints - RATHints)))) - -; LRAT proof -(declare LRATProof type) -(declare LRATProofn LRATProof) -; Deletion (includes a list of clause indices to delete) -(declare LRATProofd (! cis CIList (! rest LRATProof LRATProof))) -; Addition: a clause index, a clause, RUP trace for that clause, and hints for -; what resolutions should happen then, and how those resolutions imply bottom -; via UP. -; If the list of hints is empty, then bottom is already implied. -(declare LRATProofa - (! ci mpz - (! c clause - (! t Trace - (! h RATHints - (! rest LRATProof - LRATProof)))))) - -; ========================================== ; -; Functional programs for manipulating types ; -; ========================================== ; - -; Are two literal equal? -(program lit_eq ((l1 lit) (l2 lit)) bool - (match l1 - ((pos v1) (match l2 - ((pos v2) (ifequal v1 v2 tt ff)) - ((neg v2) ff))) - ((neg v1) (match l2 - ((pos v2) ff) - ((neg v2) (ifequal v1 v2 tt ff)))))) - -; Remove **all** occurrences of a literal from clause -(program clause_remove_all ((l lit) (c clause)) clause - (match c - (cln cln) - ((clc l' c') - (let rest_res (clause_remove_all l c') - (match (lit_eq l l') - (tt rest_res) - (ff (clc l' rest_res))))))) - -; Return the clause's first literal -; fails on an empty clause -(program clause_head ((c clause)) lit - (match c - (cln (fail lit)) - ((clc l c') l))) - -; Does a clause contain some literal? -(program clause_contains_lit ((c clause) (l lit)) bool - (match c - ((clc l' c') (match (lit_eq l l') - (tt tt) - (ff (clause_contains_lit c' l)))) - (cln ff))) - -; Append two traces -(program Trace_concat ((t1 Trace) (t2 Trace)) Trace - (match t1 - (Tracen t2) - ((Tracec h1 r1) (Tracec h1 (Trace_concat r1 t2))))) - -; Return whether a list of RAT hits is empty -(program RATHints_is_empty ((h RATHints)) bool - (match h - (RATHintsn tt) - ((RATHintsc a b c) ff))) - -; Insert into a CMap, preserving order -(program CMap_insert ((i mpz) (c clause) (cs CMap)) CMap - (match cs - (CMapn (CMapc i c CMapn)) - ((CMapc i' c' r) - (mp_ifneg (mpz_sub i i') - (CMapc i c cs) - (CMapc i' c' (CMap_insert i c r)))))) - -; Get from a CMap -(program CMap_get ((i mpz) (cs CMap)) clause - (match cs - (CMapn (fail clause)) - ((CMapc i' c r) - (mp_ifzero (mpz_sub i i') - c - (CMap_get i r))))) - -; Remove from CMap. Only removes one element. -(program CMap_remove ((i mpz) (cs CMap)) CMap - (match cs - (CMapn CMapn) - ((CMapc i' c r) - (mp_ifzero (mpz_sub i i') - r - (CMapc i' c (CMap_remove i r)))))) - -; Remove many indices from a CMap. Asuumes the input list is sorted. -(program CMap_remove_many ((is CIList) (cs CMap)) CMap - (match - is - (CIListn cs) - ((CIListc i is') - (match - cs - (CMapn (fail CMap)) ; All deletion indices must be valid! - ((CMapc ci c cs') - (mp_ifzero (mpz_sub i ci) - (CMap_remove_many is' cs') - (CMapc ci c (CMap_remove_many is cs')))))))) - -; Given a map of clauses and a literal, return all indices in the map -; corresponding to clauses that could resolve against that literal. i.e. for x, -; return the indices of all clauses containing x. -(program collect_resolution_targets_w_lit ((cs CMap) (l lit)) CIList - (match cs - (CMapn CIListn) - ((CMapc i c cs') - (let rest_solution (collect_resolution_targets_w_lit cs' l) - (match (clause_contains_lit c l) - (tt (CIListc i rest_solution)) - (ff rest_solution)))))) - -; Given a clause and a maps of clauses, return all indices in the map -; corresponding to clauses which could resolve with this one on its first -; literal -(program collect_resolution_targets ((cs CMap) (c clause)) CIList - (collect_resolution_targets_w_lit cs (lit_flip (clause_head c)))) - -; Is this clause a tautology? -; Internally uses mark 5 to flag variables that occur (+) -; and mark 6 to flag variables that occur (-) -(program is_t ((c clause)) bool - (match - c - (cln ff) - ((clc l c') (match - l - ((pos v) - (ifmarked5 - v - (is_t c') - (ifmarked6 - v - tt - (do - (markvar5 v) - (let r (is_t c') (do (markvar5 v) r)))))) - ((neg v) - (ifmarked6 - v - (is_t c') - (ifmarked5 - v - tt - (do - (markvar6 v) - (let r (is_t c') (do (markvar6 v) r)))))))))) - -; ===================================================================== ; -; Programs for manipulating and querying the global variable assignment ; -; ===================================================================== ; - -; This assignment marks values of type `var`. -; It marks a variable with 1 if that variable is true -; It marks a variable with 2 if that variable is false -; A variable should not be marked with both! -; A variable may be marked with neither, indicating that variable is presently -; unassigned, which we call "floating". - -; Mark the variable within to satisfy this literal. -; fails if the literal is already UNSAT -(program lit_mk_sat ((l lit)) Unit - (match l - ((pos v) (ifmarked2 v - (fail Unit) - (ifmarked1 v unit (do (markvar1 v) unit)))) - ((neg v) (ifmarked1 v - (fail Unit) - (ifmarked2 v unit (do (markvar2 v) unit)))))) - -; Mark the variable within to falsify this literal. -; fails is the literal is already SAT -(program lit_mk_unsat ((l lit)) Unit - (match l - ((neg v) (ifmarked2 v - (fail Unit) - (ifmarked1 v unit (do (markvar1 v) unit)))) - ((pos v) (ifmarked1 v - (fail Unit) - (ifmarked2 v unit (do (markvar2 v) unit)))))) - -; Unmarks the variable within a satisfied literal to render it neither satisfied nor falsified -; fails if the literal is not already satisfied -(program lit_un_mk_sat ((l lit)) Unit - (match l - ((pos v) (ifmarked1 v (do (markvar1 v) unit) (fail Unit))) - ((neg v) (ifmarked2 v (do (markvar2 v) unit) (fail Unit))))) - -; Unmarks the variable within a falsified literal to render it neither satisfied nor falsified -; fails if the literal is not already falsified -(program lit_un_mk_unsat ((l lit)) Unit - (match l - ((pos v) (ifmarked2 v (do (markvar2 v) unit) (fail Unit))) - ((neg v) (ifmarked1 v (do (markvar1 v) unit) (fail Unit))))) - -; Is a literal presently satisfied? -(program lit_is_sat ((l lit)) bool - (match l - ((pos v) (ifmarked1 v tt ff)) - ((neg v) (ifmarked2 v tt ff)))) - -; Is a literal presently falsified? -(program lit_is_unsat ((l lit)) bool - (match l - ((pos v) (ifmarked2 v tt ff)) - ((neg v) (ifmarked1 v tt ff)))) - -; Is a literal presently neither satisfied nor falsified? -(program lit_is_floating ((l lit)) bool - (bool_not (bool_or (lit_is_sat l) (lit_is_unsat l)))) - -; Does this clause contain a floating literal? -(program clause_has_floating ((c clause)) bool - (match c - (cln ff) - ((clc l c') (match (lit_is_floating l) - (tt tt) - (ff (clause_has_floating c')))))) - -; Is this clause falsified? i.e. are all its clauses falsified? -(program clause_is_unsat ((c clause)) bool - (match c - (cln tt) - ((clc l c') (match (lit_is_unsat l) - (tt (clause_is_unsat c')) - (ff ff))))) - -; Is this clause presently satisfied? -(program clause_is_sat ((c clause)) bool - (match c - (cln ff) - ((clc l c') (match (lit_is_sat l) - (tt tt) - (ff (clause_is_sat c')))))) - -; Falsify **all** contained literals. -; Fails on a tautological clause -(program clause_mk_all_unsat ((c clause)) Unit - (match c - (cln unit) - ((clc l c') (do - (lit_mk_unsat l) - (clause_mk_all_unsat c'))))) - -; Unfalsifies **all** contained literals -; Fails on a clause with duplicate literals -(program clause_un_mk_all_unsat ((c clause)) Unit - (match c - (cln unit) - ((clc l c') (do - (lit_un_mk_unsat l) - (clause_un_mk_all_unsat c'))))) - -; Get the first floating literal out of this clause. -; fails if there are no floating literals -(program clause_first_floating ((c clause)) lit - (match c - (cln (fail lit)) - ((clc l c') (match (lit_is_floating l) - (tt l) - (ff (clause_first_floating c')))))) - -; ===================================== ; -; High-Level Programs for LRAT Checking ; -; ===================================== ; - -; The return type for verifying that a clause is unit and modifying the global -; assignment to satisfy it -(declare MarkResult type) -; The clause is unit, and this is the (previoiusly floating) literal that is now satisfied. -(declare MRUnit (! l lit MarkResult)) -; The clause was unsat! -(declare MRUnsat MarkResult) -; The clauss was already satisfied. -(declare MRSat MarkResult) -; The clause had multiple floating literals. -(declare MRNotUnit MarkResult) - -; Determine whether this clause is sat, unsat, unit, or not unit, and if it is -; unit, it modifies the global assignment to satisfy the clause, and returns -; the literal that was made SAT by the new mark. -; -; If `c` is a tautology, reports `MRSat`, since it is (trivially) satisfied. -(program clause_check_unit_and_maybe_mark ((c clause)) MarkResult - (match (clause_is_sat c) - (tt MRSat) - (ff (match (clause_is_unsat c) - (tt MRUnsat) - (ff (match (is_t c) - (tt MRSat) - (ff ; Dedent - (match (clause_has_floating c) - (tt (let first (clause_first_floating c) - (do (lit_mk_sat first) - (match (clause_has_floating c) - (tt (do (lit_un_mk_sat first) MRNotUnit)) - (ff (MRUnit first)))))) - ; Unreachable. If clause is not floating it must have been SAT or UNSAT. - (ff (fail MarkResult)) - )))))))) - -; The return type for the process of Trace-guided unit propegation -(declare UPResult type) -; The trace guided unit propegation correctly, but that unit propegation did not end in an empty clause -(declare UPR_Ok UPResult) -; The trace guided unit propegation correctly to an empty clause -(declare UPR_Bottom UPResult) -; The trace was malformed, -;; i.e. at some point indicates that a non-unit, non-empty clause should be examined -(declare UPR_Broken UPResult) - -; Execute the unit propegation indicated by the trace. Report whether that -; unit propegation succeeds and produces bottom, fails, or succeeds but does -; not produce bottom. -; -; If the trace tries to propegate through a TAUT clause, fails. -(program do_up ((cs CMap) (t Trace)) UPResult - (match - t - (Tracen UPR_Ok) - ((Tracec i r) (match (clause_check_unit_and_maybe_mark (CMap_get i cs)) - ((MRUnit l) - (let res (do_up cs r) - (do (lit_un_mk_sat l) res))) - (MRUnsat UPR_Bottom) - (MRSat UPR_Broken) - (MRNotUnit UPR_Broken))))) - - -; Determine whether a list of indices agrees with the list of indices latent in -; a list of hints. Both lists should be sorted. -(program resolution_targets_match ( - (computed CIList) - (given RATHints)) bool - (match given - (RATHintsn - (match computed - (CIListn tt) - ((CIListc a b) ff))) - ((RATHintsc hint_idx t given') - (match computed - ((CIListc comp_idx computed') - (mp_ifzero (mpz_sub hint_idx comp_idx) - (resolution_targets_match computed' given') - (ff))) - (CIListn ff))))) - - -; Determines whether `t` is a witness that `c` is an Assymetric Tautology in `cs`. -; -; Does unit propegation in the formula `cs`, beginning by falsifying -; all literals in `c`, and then looking at the clauses indicated by `t`. -; Assumes no marks, and cleans up marks afterwards. -; -; Fails if `c` has duplicates -(program is_at_trace ((cs CMap) (c clause) (t Trace)) UPResult - (match (is_t c) - (ff - (do - (clause_mk_all_unsat c) - (let result (do_up cs t) - (do (clause_un_mk_all_unsat c) result)))) - (tt - UPR_Bottom))) - - - -; List of (clause, trace) pairs -(declare CTPairs type) -(declare CTPn CTPairs) -(declare CTPc (! c clause (! t Trace (! rest CTPairs CTPairs)))) - -; For each RAT hint, construct the pseudo-resolvant for that hint, and the net -; trace for that hint. Return a list of these. -; -; Pseudo resolvant: if l v C is the clause, and D is another clause containing -; ~l, then l v C v (D \ ~l) is the pseudo-resolvant, which is the actual -; resolant, plut l, which would be implied by UP. -; -; The net trace is the global trace (`t`), plut the trace for that specific -; resolvant. -(program construct_ct_pairs ( - (cs CMap) - (c clause) - (t Trace) - (hints RATHints) - ) CTPairs - (match hints - (RATHintsn CTPn) - ((RATHintsc i ht hints') - (CTPc - (clause_dedup (clause_append c - (clause_remove_all (lit_flip (clause_head c)) - (CMap_get i cs)))) - (Trace_concat t ht) - (construct_ct_pairs cs c t hints'))))) - -; Goes through a list of clause, trace pairs and verifies that each clause is -; an AT via that trace. -; Fails if any putative AT is a TAUT or contains duplicates -(program are_all_at_trace ( - (cs CMap) - (l CTPairs) - ) UPResult - (match l - (CTPn UPR_Bottom) - ((CTPc c t l') - (match (is_at_trace cs c t) - (UPR_Ok UPR_Ok) - (UPR_Broken UPR_Broken) - (UPR_Bottom (are_all_at_trace cs l')))))) - -; Is this trace, and list of hints, proof that `c` is an Resolution Assymeytic -; Tautology? -; Fails is the hints are empty (which means `c` should be AT) and `c` contains -; duplicates) -(program is_rat_trace ((cs CMap) (c clause) (t Trace) (hints RATHints)) UPResult - (match - (RATHints_is_empty hints) - (tt ; Empty RAT hints -- the clause must be AT - (is_at_trace cs c t)) - (ff ; Ew -- we must verify this is a RAT - (match (resolution_targets_match - (collect_resolution_targets cs c) - hints) - (ff ; Resolution targets disagree with hints. - UPR_Broken) - (tt - (are_all_at_trace cs (construct_ct_pairs cs c t hints))))))) - -; Is this proof an LRAT proof of bottom? -; Fails if any added AT is a TAUT or contains duplicates OR if any added RAT -; produces pseudo-resolvants which are TAUT or contain duplicates -(program is_lrat_proof_of_bottom ((f CMap) (proof LRATProof)) bool - (match proof - ((LRATProofd indices rest) - (is_lrat_proof_of_bottom - (CMap_remove_many indices f) - rest)) - ((LRATProofa idx c trace hints rest) - (match (is_rat_trace f c trace hints) - (UPR_Bottom - (match - c - (cln tt) - ((clc a b) - (is_lrat_proof_of_bottom (CMap_insert idx c f) rest)))) - (UPR_Ok ff) - (UPR_Broken ff))) - (LRATProofn ff)) - ) - - -; Proof of a CMap from clause proofs. -; The idx is unelidable b/c it is unspecified. -; Robust against clauses with duplicat literals, but not against tautological -; clauses. -(declare CMap_holds (! c CMap type)) -(declare CMapn_proof (CMap_holds CMapn)) -(declare CMapc_proof - (! idx mpz ; Not elidable! - (! c clause - (! deduped_c clause - (! rest CMap - (! proof_c (holds c) - (! proof_rest (CMap_holds rest) - (! sc (^ (clause_dedup c) deduped_c) - (CMap_holds (CMapc idx deduped_c rest)))))))))) - -(define bottom (holds cln)) -(declare lrat_proof_of_bottom - (! cm CMap - (! proof_cm (CMap_holds cm) - (! proof LRATProof - (! sc (^ (is_lrat_proof_of_bottom cm proof) tt) - bottom))))) - - -; TODO(aozdemir) Reducing the amount of checking that resides in side-conditions. -; Steps -; 1. Unroll the traversal of is_lrat_proof_of_bottom into a serialized -; sequence of axiom applications. -; The axioms would likely correspond to DELETE, IS T, IS AT, IS RAT. -; They would manipulate a CMap by way of side-conditions. -; 2. Unroll AT checks by manifesting the assignment in data rather than marks, -; and having axioms like IS_UNSAT, IS_UNIT_ON_LITERAL. -; 3. Unroll RAT checks in a similar fashion, although more painfully. diff --git a/proofs/signatures/sat.plf b/proofs/signatures/sat.plf deleted file mode 100644 index 574191493..000000000 --- a/proofs/signatures/sat.plf +++ /dev/null @@ -1,173 +0,0 @@ -(declare bool type) -(declare tt bool) -(declare ff bool) - -(declare var type) - -(declare lit type) -(declare pos (! x var lit)) -(declare neg (! x var lit)) - -; Flip the polarity of the literal -(program lit_flip ((l lit)) lit - (match l - ((pos v) (neg v)) - ((neg v) (pos v)))) - -(declare clause type) -(declare cln clause) -(declare clc (! x lit (! c clause clause))) - -; A list of clauses, CNF if interpretted as a formula, -; but also sometimes just a list -(declare cnf type) -(declare cnfn cnf) -(declare cnfc (! h clause (! t cnf cnf))) - -; constructs for general clauses for R, Q, satlem - -(declare concat_cl (! c1 clause (! c2 clause clause))) -(declare clr (! l lit (! c clause clause))) - -; code to check resolutions - -(program clause_append ((c1 clause) (c2 clause)) clause - (match c1 (cln c2) ((clc l c1') (clc l (clause_append c1' c2))))) - -; we use marks as follows: -; -- mark 1 to record if we are supposed to remove a positive occurrence of the variable. -; -- mark 2 to record if we are supposed to remove a negative occurrence of the variable. -; -- mark 3 if we did indeed remove the variable positively -; -- mark 4 if we did indeed remove the variable negatively -(program simplify_clause ((c clause)) clause - (match c - (cln cln) - ((clc l c1) - (match l - ; Set mark 1 on v if it is not set, to indicate we should remove it. - ; After processing the rest of the clause, set mark 3 if we were already - ; supposed to remove v (so if mark 1 was set when we began). Clear mark3 - ; if we were not supposed to be removing v when we began this call. - ((pos v) - (let m (ifmarked v tt (do (markvar v) ff)) - (let c' (simplify_clause c1) - (match m - (tt (do (ifmarked3 v v (markvar3 v)) c')) - (ff (do (ifmarked3 v (markvar3 v) v) (markvar v) (clc l c'))))))) - ; the same as the code for tt, but using different marks. - ((neg v) - (let m (ifmarked2 v tt (do (markvar2 v) ff)) - (let c' (simplify_clause c1) - (match m - (tt (do (ifmarked4 v v (markvar4 v)) c')) - (ff (do (ifmarked4 v (markvar4 v) v) (markvar2 v) (clc l c'))))))))) - ((concat_cl c1 c2) (clause_append (simplify_clause c1) (simplify_clause c2))) - ((clr l c1) - (match l - ; set mark 1 to indicate we should remove v, and fail if - ; mark 3 is not set after processing the rest of the clause - ; (we will set mark 3 if we remove a positive occurrence of v). - ((pos v) - (let m (ifmarked v tt (do (markvar v) ff)) - (let m3 (ifmarked3 v (do (markvar3 v) tt) ff) - (let c' (simplify_clause c1) - (ifmarked3 v (do (match m3 (tt v) (ff (markvar3 v))) - (match m (tt v) (ff (markvar v))) c') - (fail clause)))))) - ; same as the tt case, but with different marks. - ((neg v) - (let m2 (ifmarked2 v tt (do (markvar2 v) ff)) - (let m4 (ifmarked4 v (do (markvar4 v) tt) ff) - (let c' (simplify_clause c1) - (ifmarked4 v (do (match m4 (tt v) (ff (markvar4 v))) - (match m2 (tt v) (ff (markvar2 v))) c') - (fail clause)))))) - )))) - - -; resolution proofs - -(declare holds (! c clause type)) - -(declare R (! c1 clause (! c2 clause - (! u1 (holds c1) - (! u2 (holds c2) - (! n var - (holds (concat_cl (clr (pos n) c1) - (clr (neg n) c2))))))))) - -(declare Q (! c1 clause (! c2 clause - (! u1 (holds c1) - (! u2 (holds c2) - (! n var - (holds (concat_cl (clr (neg n) c1) - (clr (pos n) c2))))))))) - -(declare satlem_simplify - (! c1 clause - (! c2 clause - (! c3 clause - (! u1 (holds c1) - (! r (^ (simplify_clause c1) c2) - (! u2 (! x (holds c2) (holds c3)) - (holds c3)))))))) - -(declare satlem - (! c clause - (! c2 clause - (! u (holds c) - (! u2 (! v (holds c) (holds c2)) - (holds c2)))))) - - -; Returns a copy of `c` with any duplicate literals removed. -; Never fails. -; Uses marks 3 & 4. Expects them to be clear before hand, and leaves them clear -; afterwards. -(program clause_dedup ((c clause)) clause - (match c - (cln cln) - ((clc l rest) - (match l - ((pos v) (ifmarked3 - v - (clause_dedup rest) - (do (markvar3 v) - (let result (clc (pos v) (clause_dedup rest)) - (do (markvar3 v) result))))) - ((neg v) (ifmarked4 - v - (clause_dedup rest) - (do (markvar4 v) - (let result (clc (neg v) (clause_dedup rest)) - (do (markvar4 v) result))))))))) - -(declare cnf_holds (! c cnf type)) -(declare cnfn_proof (cnf_holds cnfn)) -(declare cnfc_proof - (! c clause - (! deduped_c clause - (! rest cnf - (! proof_c (holds c) - (! proof_rest (cnf_holds rest) - (! sc (^ (clause_dedup c) deduped_c) - (cnf_holds (cnfc c rest))))))))) - -; A little example to demonstrate simplify_clause. -; It can handle nested clr's of both polarities, -; and correctly cleans up marks when it leaves a -; clr or clc scope. Uncomment and run with -; --show-runs to see it in action. -; -; (check -; (% v1 var -; (% u1 (holds (concat_cl (clr (neg v1) (clr (pos v1) (clc (pos v1) (clr (pos v1) (clc (pos v1) (clc (neg v1) cln)))))) -; (clc (pos v1) (clc (pos v1) cln)))) -; (satlem _ _ _ u1 (\ x x)))))) - - -;(check -; (% v1 var -; (% u1 (holds (clr (neg v1) (concat_cl (clc (neg v1) cln) -; (clr (neg v1) (clc (neg v1) cln))))) -; (satlem _ _ _ u1 (\ x x)))))) diff --git a/proofs/signatures/signatures.cpp.in b/proofs/signatures/signatures.cpp.in deleted file mode 100644 index 37c152b2f..000000000 --- a/proofs/signatures/signatures.cpp.in +++ /dev/null @@ -1,10 +0,0 @@ -namespace CVC4 { -namespace proof { - -extern const char *const plf_signatures; -const char *const plf_signatures = "\ -@CORE_SIGNATURES@\ -"; - -} // namespace proof -} // namespace CVC4 diff --git a/proofs/signatures/smt.plf b/proofs/signatures/smt.plf deleted file mode 100644 index 9f6e71986..000000000 --- a/proofs/signatures/smt.plf +++ /dev/null @@ -1,506 +0,0 @@ -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -; -; SMT syntax and semantics (not theory-specific) -; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -; Deps: sat.plf - -(declare formula type) -(declare th_holds (! f formula type)) - -; standard logic definitions -(declare true formula) -(declare false formula) - -(define formula_op1 - (! f formula - formula)) - -(define formula_op2 - (! 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) -(declare impl formula_op2) -(declare iff formula_op2) -(declare xor formula_op2) -(declare ifte formula_op3) - -; terms -(declare sort type) -(declare term (! t sort type)) ; declared terms in formula - -; standard definitions for =, ite, let and flet -(declare = (! s sort - (! x (term s) - (! y (term s) - formula)))) -(declare ite (! s sort - (! f formula - (! t1 (term s) - (! t2 (term s) - (term s)))))) -(declare let (! s sort - (! t (term s) - (! f (! v (term s) formula) - formula)))) -(declare flet (! f1 formula - (! f2 (! v formula formula) - formula))) - -; We view applications of predicates as terms of sort "Bool". -; Such terms can be injected as atomic formulas using "p_app". -(declare Bool sort) ; the special sort for predicates -(declare p_app (! x (term Bool) formula)) ; propositional application of term - -; boolean terms -(declare t_true (term Bool)) -(declare t_false (term Bool)) -(declare t_t_neq_f - (th_holds (not (= Bool t_true t_false)))) -(declare pred_eq_t - (! x (term Bool) - (! u (th_holds (p_app x)) - (th_holds (= Bool x t_true))))) - -(declare pred_eq_f - (! x (term Bool) - (! u (th_holds (not (p_app x))) - (th_holds (= Bool x t_false))))) - -(declare f_to_b - (! f formula - (term Bool))) - -(declare true_preds_equal - (! x1 (term Bool) - (! x2 (term Bool) - (! u1 (th_holds (p_app x1)) - (! u2 (th_holds (p_app x2)) - (th_holds (= Bool x1 x2))))))) - -(declare false_preds_equal - (! x1 (term Bool) - (! x2 (term Bool) - (! u1 (th_holds (not (p_app x1))) - (! u2 (th_holds (not (p_app x2))) - (th_holds (= Bool x1 x2))))))) - -(declare pred_refl_pos - (! x1 (term Bool) - (! u1 (th_holds (p_app x1)) - (th_holds (= Bool x1 x1))))) - -(declare pred_refl_neg - (! x1 (term Bool) - (! u1 (th_holds (not (p_app x1))) - (th_holds (= Bool x1 x1))))) - -(declare pred_not_iff_f - (! x (term Bool) - (! u (th_holds (not (iff false (p_app x)))) - (th_holds (= Bool t_true x))))) - -(declare pred_not_iff_f_2 - (! x (term Bool) - (! u (th_holds (not (iff (p_app x) false))) - (th_holds (= Bool x t_true))))) - -(declare pred_not_iff_t - (! x (term Bool) - (! u (th_holds (not (iff true (p_app x)))) - (th_holds (= Bool t_false x))))) - -(declare pred_not_iff_t_2 - (! x (term Bool) - (! u (th_holds (not (iff (p_app x) true))) - (th_holds (= Bool x t_false))))) - -(declare pred_iff_f - (! x (term Bool) - (! u (th_holds (iff false (p_app x))) - (th_holds (= Bool t_false x))))) - -(declare pred_iff_f_2 - (! x (term Bool) - (! u (th_holds (iff (p_app x) false)) - (th_holds (= Bool x t_false))))) - -(declare pred_iff_t - (! x (term Bool) - (! u (th_holds (iff true (p_app x))) - (th_holds (= Bool t_true x))))) - -(declare pred_iff_t_2 - (! x (term Bool) - (! u (th_holds (iff (p_app x) true)) - (th_holds (= Bool x t_true))))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -; -; CNF Clausification -; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -; binding between an LF var and an (atomic) formula - -(declare atom (! v var (! p formula type))) - -; binding between two LF vars -(declare bvatom (! sat_v var (! bv_v var type))) - -(declare decl_atom - (! f formula - (! u (! v var - (! a (atom v f) - (holds cln))) - (holds cln)))) - -;; declare atom enhanced with mapping -;; between SAT prop variable and BVSAT prop variable -(declare decl_bvatom - (! f formula - (! u (! v var - (! bv_v var - (! a (atom v f) - (! bva (atom bv_v f) - (! vbv (bvatom v bv_v) - (holds cln)))))) - (holds cln)))) - - -; clausify a formula directly -(declare clausify_form - (! f formula - (! v var - (! 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))) - -(declare th_let_pf - (! f formula - (! u (th_holds f) - (! u2 (! v (th_holds f) (holds cln)) - (holds cln))))) - - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -; -; Natural deduction rules : used for CNF -; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -;; for eager bit-blasting -(declare iff_symm - (! f formula - (th_holds (iff f f)))) - - -;; contradiction - -(declare contra - (! f formula - (! r1 (th_holds f) - (! r2 (th_holds (not f)) - (th_holds false))))) - -; truth -(declare truth (th_holds true)) - -;; not not - -(declare not_not_intro - (! f formula - (! u (th_holds f) - (th_holds (not (not f)))))) - -(declare not_not_elim - (! f formula - (! u (th_holds (not (not f))) - (th_holds f)))) - -;; or elimination - -(declare or_elim_1 - (! f1 formula - (! f2 formula - (! u1 (th_holds (not f1)) - (! u2 (th_holds (or f1 f2)) - (th_holds f2)))))) - -(declare or_elim_2 - (! f1 formula - (! f2 formula - (! u1 (th_holds (not f2)) - (! u2 (th_holds (or f1 f2)) - (th_holds f1)))))) - -(declare not_or_elim - (! f1 formula - (! f2 formula - (! u2 (th_holds (not (or f1 f2))) - (th_holds (and (not f1) (not f2))))))) - -;; and elimination - -(declare and_elim_1 - (! f1 formula - (! f2 formula - (! u (th_holds (and f1 f2)) - (th_holds f1))))) - -(declare and_elim_2 - (! f1 formula - (! f2 formula - (! u (th_holds (and f1 f2)) - (th_holds f2))))) - -(declare not_and_elim - (! f1 formula - (! f2 formula - (! u2 (th_holds (not (and f1 f2))) - (th_holds (or (not f1) (not f2))))))) - -;; impl elimination - -(declare impl_intro (! f1 formula - (! f2 formula - (! i1 (! u (th_holds f1) - (th_holds f2)) - (th_holds (impl f1 f2)))))) - -(declare impl_elim - (! f1 formula - (! f2 formula - (! u2 (th_holds (impl f1 f2)) - (th_holds (or (not f1) f2)))))) - -(declare not_impl_elim - (! f1 formula - (! f2 formula - (! u (th_holds (not (impl f1 f2))) - (th_holds (and f1 (not f2))))))) - -;; iff elimination - -(declare iff_elim_1 - (! f1 formula - (! f2 formula - (! u1 (th_holds (iff f1 f2)) - (th_holds (or (not f1) f2)))))) - -(declare iff_elim_2 - (! f1 formula - (! f2 formula - (! u1 (th_holds (iff f1 f2)) - (th_holds (or f1 (not f2))))))) - -(declare not_iff_elim - (! f1 formula - (! f2 formula - (! u2 (th_holds (not (iff f1 f2))) - (th_holds (iff f1 (not f2))))))) - -; xor elimination - -(declare xor_elim_1 - (! f1 formula - (! f2 formula - (! u1 (th_holds (xor f1 f2)) - (th_holds (or (not f1) (not f2))))))) - -(declare xor_elim_2 - (! f1 formula - (! f2 formula - (! u1 (th_holds (xor f1 f2)) - (th_holds (or f1 f2)))))) - -(declare not_xor_elim - (! f1 formula - (! f2 formula - (! u2 (th_holds (not (xor f1 f2))) - (th_holds (iff f1 f2)))))) - -;; ite elimination - -(declare ite_elim_1 - (! a formula - (! b formula - (! c formula - (! u2 (th_holds (ifte a b c)) - (th_holds (or (not a) b))))))) - -(declare ite_elim_2 - (! a formula - (! b formula - (! c formula - (! u2 (th_holds (ifte a b c)) - (th_holds (or a c))))))) - -(declare ite_elim_3 - (! a formula - (! b formula - (! c formula - (! u2 (th_holds (ifte a b c)) - (th_holds (or b c))))))) - -(declare not_ite_elim_1 - (! a formula - (! b formula - (! c formula - (! u2 (th_holds (not (ifte a b c))) - (th_holds (or (not a) (not b)))))))) - -(declare not_ite_elim_2 - (! a formula - (! b formula - (! c formula - (! u2 (th_holds (not (ifte a b c))) - (th_holds (or a (not c)))))))) - -(declare not_ite_elim_3 - (! a formula - (! b formula - (! c formula - (! u2 (th_holds (not (ifte a b c))) - (th_holds (or (not b) (not c)))))))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -; -; For theory lemmas -; - make a series of assumptions and then derive a contradiction (or false) -; - then the assumptions yield a formula like "v1 -> v2 -> ... -> vn -> false" -; - In CNF, it becomes a clause: "~v1, ~v2, ..., ~vn" -; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(declare ast - (! v var - (! f formula - (! C clause - (! r (atom v f) ;this is specified - (! u (! o (th_holds f) - (holds C)) - (holds (clc (neg v) C)))))))) - -(declare asf - (! v var - (! f formula - (! C clause - (! r (atom v f) - (! u (! o (th_holds (not f)) - (holds C)) - (holds (clc (pos v) C)))))))) - -;; Bitvector lemma constructors to assume -;; the unit clause containing the assumptions -;; it also requires the mapping between bv_v and v -;; The resolution proof proving false will use bv_v as the definition clauses use bv_v -;; but the Problem clauses in the main SAT solver will use v so the learned clause is in terms of v -(declare bv_asf - (! v var - (! bv_v var - (! f formula - (! C clause - (! r (atom v f) ;; passed in - (! x (bvatom v bv_v) ; establishes the equivalence of v to bv_ - (! 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 - (! f formula - (! C clause - (! r (atom v f) ; this is specified - (! x (bvatom v bv_v) ; establishes the equivalence of v to bv_v - (! u (! o (holds (clc (pos bv_v) cln)) - (holds C)) - (holds (clc (neg v) C)))))))))) - -;; Numeric primitives - -(program mpz_sub ((x mpz) (y mpz)) mpz - (mp_add x (mp_mul (~1) y))) - -(program mp_ispos ((x mpz)) formula - (mp_ifneg x false true)) - -(program mpz_eq ((x mpz) (y mpz)) formula - (mp_ifzero (mpz_sub x y) true false)) - -(program mpz_lt ((x mpz) (y mpz)) formula - (mp_ifneg (mpz_sub x y) true false)) - -(program mpz_lte ((x mpz) (y mpz)) formula - (mp_ifneg (mpz_sub x y) true (mpz_eq x y))) - -;; Example: -;; -;; Given theory literals (F1....Fn), and an input formula A of the form (th_holds (or F1 (or F2 .... (or F{n-1} Fn))))). -;; -;; We introduce atoms (a1,...,an) to map boolean literals (v1,...,vn) top literals (F1,...,Fn). -;; Do this at the beginning of the proof: -;; -;; (decl_atom F1 (\ v1 (\ a1 -;; (decl_atom F2 (\ v2 (\ a2 -;; .... -;; (decl_atom Fn (\ vn (\ an -;; -;; A is then clausified by the following proof: -;; -;;(satlem _ _ -;;(asf _ _ _ a1 (\ l1 -;;(asf _ _ _ a2 (\ l2 -;;... -;;(asf _ _ _ an (\ ln -;;(clausify_false -;; -;; (contra _ -;; (or_elim_1 _ _ l{n-1} -;; ... -;; (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). -;; -;; Polarity of literals should be considered, say we have A of the form (th_holds (or (not F1) (or F2 (not F3)))). -;; Where necessary, we use "ast" instead of "asf", introduce negations by "not_not_intro" for pattern matching, and flip -;; the arguments of contra: -;; -;;(satlem _ _ -;;(ast _ _ _ a1 (\ l1 -;;(asf _ _ _ a2 (\ l2 -;;(ast _ _ _ a3 (\ l3 -;;(clausify_false -;; -;; (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/proofs/signatures/th_arrays.plf b/proofs/signatures/th_arrays.plf deleted file mode 100644 index 5517d9a4f..000000000 --- a/proofs/signatures/th_arrays.plf +++ /dev/null @@ -1,65 +0,0 @@ -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -; -; Theory of Arrays -; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -; Deps: th_base.plf - -; sorts - -(declare Array (! s1 sort (! s2 sort sort))) ; s1 is index, s2 is element - -; functions -(declare write (! s1 sort - (! s2 sort - (term (arrow (Array s1 s2) - (arrow s1 - (arrow s2 (Array s1 s2)))))))) - -(declare read (! s1 sort - (! s2 sort - (term (arrow (Array s1 s2) - (arrow s1 s2)))))) - -; inference rules - -; read( a[i] = b, i ) == b -(declare row1 (! s1 sort - (! s2 sort - (! t1 (term (Array s1 s2)) - (! t2 (term s1) - (! t3 (term s2) - (th_holds (= _ - (apply _ _ (apply _ _ (read s1 s2) (apply _ _ (apply _ _ (apply _ _ (write s1 s2) t1) t2) t3)) t2) t3)))))))) - -; read( a[i] = b, j ) == read( a, j ) if i != j -(declare row (! s1 sort - (! s2 sort - (! t2 (term s1) - (! t3 (term s1) - (! t1 (term (Array s1 s2)) - (! t4 (term s2) - (! u (th_holds (not (= _ t2 t3))) - (th_holds (= _ (apply _ _ (apply _ _ (read s1 s2) (apply _ _ (apply _ _ (apply _ _ (write s1 s2) t1) t2) t4)) t3) - (apply _ _ (apply _ _ (read s1 s2) t1) t3))))))))))) - -; i == j if read( a, j ) != read( a[i] = b, j ) -(declare negativerow (! s1 sort - (! s2 sort - (! t2 (term s1) - (! t3 (term s1) - (! t1 (term (Array s1 s2)) - (! t4 (term s2) - (! u (th_holds (not (= _ - (apply _ _ (apply _ _ (read s1 s2) (apply _ _ (apply _ _ (apply _ _ (write s1 s2) t1) t2) t4)) t3) - (apply _ _ (apply _ _ (read s1 s2) t1) t3)))) - (th_holds (= _ t2 t3)))))))))) - -(declare ext (! s1 sort - (! s2 sort - (! t1 (term (Array s1 s2)) - (! t2 (term (Array s1 s2)) - (! u1 (! k (term s1) - (! u2 (th_holds (or (= _ t1 t2) (not (= _ (apply _ _ (apply _ _ (read s1 s2) t1) k) (apply _ _ (apply _ _ (read s1 s2) t2) k))))) - (holds cln))) - (holds cln))))))) diff --git a/proofs/signatures/th_base.plf b/proofs/signatures/th_base.plf deleted file mode 100644 index d5182007e..000000000 --- a/proofs/signatures/th_base.plf +++ /dev/null @@ -1,96 +0,0 @@ - - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -; -; Theory of Equality and Congruence Closure -; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -; Deps: smt.plf - -; sorts : - -(declare arrow (! s1 sort (! s2 sort sort))) ; function constructor - -; functions : - -(declare apply (! s1 sort - (! s2 sort - (! t1 (term (arrow s1 s2)) - (! t2 (term s1) - (term s2)))))) - - -; inference rules : - -(declare trust (th_holds false)) ; temporary -(declare trust_f (! f formula (th_holds f))) ; temporary - -(declare refl - (! s sort - (! t (term s) - (th_holds (= s t t))))) - -(declare symm (! s sort - (! x (term s) - (! y (term s) - (! u (th_holds (= _ x y)) - (th_holds (= _ y x))))))) - -(declare trans (! s sort - (! x (term s) - (! y (term s) - (! z (term s) - (! u (th_holds (= _ x y)) - (! u (th_holds (= _ y z)) - (th_holds (= _ x z))))))))) - -(declare negsymm (! s sort - (! x (term s) - (! y (term s) - (! u (th_holds (not (= _ x y))) - (th_holds (not (= _ y x)))))))) - -(declare negtrans1 (! s sort - (! x (term s) - (! y (term s) - (! z (term s) - (! u (th_holds (not (= _ x y))) - (! u (th_holds (= _ y z)) - (th_holds (not (= _ x z)))))))))) - -(declare negtrans2 (! s sort - (! x (term s) - (! y (term s) - (! z (term s) - (! u (th_holds (= _ x y)) - (! u (th_holds (not (= _ y z))) - (th_holds (not (= _ x z)))))))))) - -(declare cong (! s1 sort - (! s2 sort - (! a1 (term (arrow s1 s2)) - (! b1 (term (arrow s1 s2)) - (! a2 (term s1) - (! b2 (term s1) - (! u1 (th_holds (= _ a1 b1)) - (! u2 (th_holds (= _ a2 b2)) - (th_holds (= _ (apply _ _ a1 a2) (apply _ _ b1 b2)))))))))))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -; Examples - -; an example of "(p1 or p2(0)) and t1=t2(1)" -;(! p1 (term Bool) -;(! p2 (term (arrow Int Bool)) -;(! t1 (term Int) -;(! t2 (term (arrow Int Int)) -;(! F (th_holds (and (or (p_app p1) (p_app (apply _ _ p2 0))) -; (= _ t1 (apply _ _ t2 1)))) -; ... - -; another example of "p3(a,b)" -;(! a (term Int) -;(! b (term Int) -;(! p3 (term (arrow Int (arrow Int Bool))) ; arrow is right assoc. -;(! F (th_holds (p_app (apply _ _ (apply _ _ p3 a) b))) ; apply is left assoc. -; ... diff --git a/proofs/signatures/th_bv.plf b/proofs/signatures/th_bv.plf deleted file mode 100644 index f0ced51c7..000000000 --- a/proofs/signatures/th_bv.plf +++ /dev/null @@ -1,176 +0,0 @@ -;;;; TEMPORARY: - -(declare trust-bad (th_holds false)) - -; helper stuff - -(program mpz_ ((x mpz) (y mpz)) formula - (mp_ifzero (mpz_sub x y) true false)) - - -; "bitvec" is a term of type "sort" -; (declare BitVec sort) -(declare BitVec (!n mpz sort)) - -; bit type -(declare bit type) -(declare b0 bit) -(declare b1 bit) - -; bit vector type used for constants -(declare bv type) -(declare bvn bv) -(declare bvc (! b bit (! v bv bv))) - -; calculate the length of a bitvector -;; (program bv_len ((v bv)) mpz -;; (match v -;; (bvn 0) -;; ((bvc b v') (mp_add (bv_len v') 1)))) - - -; a bv constant term -(declare a_bv - (! n mpz - (! v bv - (term (BitVec n))))) - -(program bv_constants_are_disequal ((x bv) (y bv)) formula - (match x - (bvn (fail formula)) - ((bvc bx x') - (match y - (bvn (fail formula)) - ((bvc by y') (match bx - (b0 (match by (b0 (bv_constants_are_disequal x' y')) (b1 (true)))) - (b1 (match by (b0 (true)) (b1 (bv_constants_are_disequal x' y')))) - )) - )) -)) - -(declare bv_disequal_constants - (! n mpz - (! x bv - (! y bv - (! c (^ (bv_constants_are_disequal x y) true) - (th_holds (not (= (BitVec n) (a_bv n x) (a_bv n y))))))))) - -; a bv variable -(declare var_bv type) -; a bv variable term -(declare a_var_bv - (! n mpz - (! v var_bv - (term (BitVec n))))) - -; bit vector binary operators -(define bvop2 - (! n mpz - (! x (term (BitVec n)) - (! y (term (BitVec n)) - (term (BitVec n)))))) - -(declare bvand bvop2) -(declare bvor bvop2) -(declare bvxor bvop2) -(declare bvnand bvop2) -(declare bvnor bvop2) -(declare bvxnor bvop2) -(declare bvmul bvop2) -(declare bvadd bvop2) -(declare bvsub bvop2) -(declare bvudiv bvop2) -(declare bvurem bvop2) -(declare bvsdiv bvop2) -(declare bvsrem bvop2) -(declare bvsmod bvop2) -(declare bvshl bvop2) -(declare bvlshr bvop2) -(declare bvashr bvop2) - -; bit vector unary operators -(define bvop1 - (! n mpz - (! x (term (BitVec n)) - (term (BitVec n))))) - - -(declare bvneg bvop1) -(declare bvnot bvop1) -(declare rotate_left bvop1) -(declare rotate_right bvop1) - -(declare bvcomp - (! n mpz - (! t1 (term (BitVec n)) - (! t2 (term (BitVec n)) - (term (BitVec 1)))))) - - -(declare concat - (! n mpz - (! m mpz - (! m' mpz - (! t1 (term (BitVec m)) - (! t2 (term (BitVec m')) - (term (BitVec n)))))))) - -;; side-condition fails in signature only?? -;; (! s (^ (mp_add m m') n) - -;; (declare repeat bvopp) - -(declare extract - (! n mpz - (! i mpz - (! j mpz - (! m mpz - (! t2 (term (BitVec m)) - (term (BitVec n)))))))) - -(declare zero_extend - (! n mpz - (! i mpz - (! m mpz - (! t2 (term (BitVec m)) - (term (BitVec n))))))) - -(declare sign_extend - (! n mpz - (! i mpz - (! m mpz - (! t2 (term (BitVec m)) - (term (BitVec n))))))) - -(declare repeat - (! n mpz - (! i mpz - (! m mpz - (! t2 (term (BitVec m)) - (term (BitVec n))))))) - - - -;; TODO: add checks for valid typing for these operators -;; (! c1 (^ (mpz_lte i j) -;; (! c2 (^ (mpz_lt i n) true) -;; (! c3 (^ (mp_ifneg i false true) true) -;; (! c4 (^ (mp_ifneg j false true) true) -;; (! s (^ (mp_add (mpz_sub i j) 1) m) - - -; bit vector predicates -(define bvpred - (! n mpz - (! x (term (BitVec n)) - (! y (term (BitVec n)) - formula)))) - -(declare bvult bvpred) -(declare bvule bvpred) -(declare bvugt bvpred) -(declare bvuge bvpred) -(declare bvslt bvpred) -(declare bvsle bvpred) -(declare bvsgt bvpred) -(declare bvsge bvpred) diff --git a/proofs/signatures/th_bv_bitblast.plf b/proofs/signatures/th_bv_bitblast.plf deleted file mode 100644 index f01b388ed..000000000 --- a/proofs/signatures/th_bv_bitblast.plf +++ /dev/null @@ -1,694 +0,0 @@ -; bit blasted terms as list of formulas -(declare bblt type) -(declare bbltn bblt) -(declare bbltc (! f formula (! v bblt bblt))) - -; calculate the length of a bit-blasted term -(program bblt_len ((v bblt)) mpz - (match v - (bbltn 0) - ((bbltc b v') (mp_add (bblt_len v') 1)))) - - -; (bblast_term x y) means term y corresponds to bit level interpretation x -(declare bblast_term - (! n mpz - (! x (term (BitVec n)) - (! y bblt - type)))) - -; FIXME: for unsupported bit-blast terms -(declare trust_bblast_term - (! n mpz - (! x (term (BitVec n)) - (! y bblt - (bblast_term n x y))))) - - -; Binds a symbol to the bblast_term to be used later on. -(declare decl_bblast - (! n mpz - (! b bblt - (! t (term (BitVec n)) - (! bb (bblast_term n t b) - (! s (^ (bblt_len b) n) - (! u (! v (bblast_term n t b) (holds cln)) - (holds cln)))))))) - -(declare decl_bblast_with_alias - (! n mpz - (! b bblt - (! t (term (BitVec n)) - (! a (term (BitVec n)) - (! bb (bblast_term n t b) - (! e (th_holds (= _ t a)) - (! s (^ (bblt_len b) n) - (! u (! v (bblast_term n a b) (holds cln)) - (holds cln)))))))))) - -; a predicate to represent the n^th bit of a bitvector term -(declare bitof - (! x var_bv - (! n mpz formula))) - - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; -;; BITBLASTING RULES -;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; BITBLAST CONSTANT -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(program bblast_const ((v bv) (n mpz)) bblt - (mp_ifneg n (match v (bvn bbltn) - (default (fail bblt))) - (match v ((bvc b v') (bbltc (match b (b0 false) (b1 true)) (bblast_const v' (mp_add n (~ 1))))) - (default (fail bblt))))) - -(declare bv_bbl_const (! n mpz - (! f bblt - (! v bv - (! c (^ (bblast_const v (mp_add n (~ 1))) f) - (bblast_term n (a_bv n v) f)))))) - - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; BITBLAST VARIABLE -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(program bblast_var ((x var_bv) (n mpz)) bblt - (mp_ifneg n bbltn - (bbltc (bitof x n) (bblast_var x (mp_add n (~ 1)))))) - -(declare bv_bbl_var (! n mpz - (! x var_bv - (! f bblt - (! c (^ (bblast_var x (mp_add n (~ 1))) f) - (bblast_term n (a_var_bv n x) f)))))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; BITBLAST CONCAT -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(program bblast_concat ((x bblt) (y bblt)) bblt - (match x - (bbltn (match y ((bbltc by y') (bbltc by (bblast_concat x y'))) - (bbltn bbltn))) - ((bbltc bx x') (bbltc bx (bblast_concat x' y))))) - -(declare bv_bbl_concat (! n mpz - (! m mpz - (! m1 mpz - (! x (term (BitVec m)) - (! y (term (BitVec m1)) - (! xb bblt - (! yb bblt - (! rb bblt - (! xbb (bblast_term m x xb) - (! ybb (bblast_term m1 y yb) - (! c (^ (bblast_concat xb yb ) rb) - (bblast_term n (concat n m m1 x y) rb))))))))))))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; BITBLAST EXTRACT -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(program bblast_extract_rec ((x bblt) (i mpz) (j mpz) (n mpz)) bblt - (match x - ((bbltc bx x') (mp_ifneg (mpz_sub (mpz_sub j n) 1) - (mp_ifneg (mpz_sub (mpz_sub n i) 1) - (bbltc bx (bblast_extract_rec x' i j (mpz_sub n 1))) - (bblast_extract_rec x' i j (mpz_sub n 1))) - - bbltn)) - (bbltn bbltn))) - -(program bblast_extract ((x bblt) (i mpz) (j mpz) (n mpz)) bblt - (bblast_extract_rec x i j (mpz_sub n 1))) - -(declare bv_bbl_extract (! n mpz - (! i mpz - (! j mpz - (! m mpz - (! x (term (BitVec m)) - (! xb bblt - (! rb bblt - (! xbb (bblast_term m x xb) - (! c ( ^ (bblast_extract xb i j m) rb) - (bblast_term n (extract n i j m x) rb))))))))))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; BITBLAST ZERO/SIGN EXTEND -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(program extend_rec ((x bblt) (i mpz) (b formula)) bblt - (mp_ifneg i x - (bbltc b (extend_rec x (mpz_sub i 1) b))))) - -(program bblast_zextend ((x bblt) (i mpz)) bblt - (extend_rec x (mpz_sub i 1) false)) - -(declare bv_bbl_zero_extend (! n mpz - (! k mpz - (! m mpz - (! x (term (BitVec m)) - (! xb bblt - (! rb bblt - (! xbb (bblast_term m x xb) - (! c ( ^ (bblast_zextend xb k m) rb) - (bblast_term n (zero_extend n k m x) rb)))))))))) - -(program bblast_sextend ((x bblt) (i mpz)) bblt - (match x (bbltn (fail bblt)) - ((bbltc xb x') (extend_rec x (mpz_sub i 1) xb)))) - -(declare bv_bbl_sign_extend (! n mpz - (! k mpz - (! m mpz - (! x (term (BitVec m)) - (! xb bblt - (! rb bblt - (! xbb (bblast_term m x xb) - (! c ( ^ (bblast_sextend xb k) rb) - (bblast_term n (sign_extend n k m x) rb)))))))))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; BITBLAST BVAND -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(program bblast_bvand ((x bblt) (y bblt)) bblt - (match x - (bbltn (match y (bbltn bbltn) (default (fail bblt)))) - ((bbltc bx x') (match y - (bbltn (fail bblt)) - ((bbltc by y') (bbltc (and bx by) (bblast_bvand x' y'))))))) - -(declare bv_bbl_bvand (! n mpz - (! x (term (BitVec n)) - (! y (term (BitVec n)) - (! xb bblt - (! yb bblt - (! rb bblt - (! xbb (bblast_term n x xb) - (! ybb (bblast_term n y yb) - (! c (^ (bblast_bvand xb yb ) rb) - (bblast_term n (bvand n x y) rb))))))))))) -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; BITBLAST BVNOT -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(program bblast_bvnot ((x bblt)) bblt - (match x - (bbltn bbltn) - ((bbltc bx x') (bbltc (not bx) (bblast_bvnot x'))))) - -(declare bv_bbl_bvnot (! n mpz - (! x (term (BitVec n)) - (! xb bblt - (! rb bblt - (! xbb (bblast_term n x xb) - (! c (^ (bblast_bvnot xb ) rb) - (bblast_term n (bvnot n x) rb)))))))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; BITBLAST BVOR -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(program bblast_bvor ((x bblt) (y bblt)) bblt - (match x - (bbltn (match y (bbltn bbltn) (default (fail bblt)))) - ((bbltc bx x') (match y - (bbltn (fail bblt)) - ((bbltc by y') (bbltc (or bx by) (bblast_bvor x' y'))))))) - -(declare bv_bbl_bvor (! n mpz - (! x (term (BitVec n)) - (! y (term (BitVec n)) - (! xb bblt - (! yb bblt - (! rb bblt - (! xbb (bblast_term n x xb) - (! ybb (bblast_term n y yb) - (! c (^ (bblast_bvor xb yb ) rb) - (bblast_term n (bvor n x y) rb))))))))))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; BITBLAST BVXOR -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(program bblast_bvxor ((x bblt) (y bblt)) bblt - (match x - (bbltn (match y (bbltn bbltn) (default (fail bblt)))) - ((bbltc bx x') (match y - (bbltn (fail bblt)) - ((bbltc by y') (bbltc (xor bx by) (bblast_bvxor x' y'))))))) - -(declare bv_bbl_bvxor (! n mpz - (! x (term (BitVec n)) - (! y (term (BitVec n)) - (! xb bblt - (! yb bblt - (! rb bblt - (! xbb (bblast_term n x xb) - (! ybb (bblast_term n y yb) - (! c (^ (bblast_bvxor xb yb ) rb) - (bblast_term n (bvxor n x y) rb))))))))))) - - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; BITBLAST BVADD -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -;; return the carry bit after adding x y -;; FIXME: not the most efficient thing in the world -(program bblast_bvadd_carry ((a bblt) (b bblt) (carry formula)) formula -(match a - ( bbltn (match b (bbltn carry) (default (fail formula)))) - ((bbltc ai a') (match b - (bbltn (fail formula)) - ((bbltc bi b') (or (and ai bi) (and (xor ai bi) (bblast_bvadd_carry a' b' carry)))))))) - -;; ripple carry adder where carry is the initial carry bit -(program bblast_bvadd ((a bblt) (b bblt) (carry formula)) bblt -(match a - ( bbltn (match b (bbltn bbltn) (default (fail bblt)))) - ((bbltc ai a') (match b - (bbltn (fail bblt)) - ((bbltc bi b') (bbltc (xor (xor ai bi) (bblast_bvadd_carry a' b' carry)) - (bblast_bvadd a' b' carry))))))) - - -(program reverse_help ((x bblt) (acc bblt)) bblt -(match x - (bbltn acc) - ((bbltc xi x') (reverse_help x' (bbltc xi acc))))) - - -(program reverseb ((x bblt)) bblt - (reverse_help x bbltn)) - - -; AJR: use this version? -;(program bblast_bvadd_2h ((a bblt) (b bblt) (carry formula)) bblt -;(match a -; ( bbltn (match b (bbltn bbltn) (default (fail bblt)))) -; ((bbltc ai a') (match b -; (bbltn (fail bblt)) -; ((bbltc bi b') -; (let carry' (or (and ai bi) (and (xor ai bi) carry)) -; (bbltc (xor (xor ai bi) carry) -; (bblast_bvadd_2h a' b' carry')))))))) - -;(program bblast_bvadd_2 ((a bblt) (b bblt) (carry formula)) bblt -;(let ar (reverseb a) ;; reverse a and b so that we can build the circuit -;(let br (reverseb b) ;; from the least significant bit up -;(let ret (bblast_bvadd_2h ar br carry) -; (reverseb ret))))) - -(declare bv_bbl_bvadd (! n mpz - (! x (term (BitVec n)) - (! y (term (BitVec n)) - (! xb bblt - (! yb bblt - (! rb bblt - (! xbb (bblast_term n x xb) - (! ybb (bblast_term n y yb) - (! c (^ (bblast_bvadd xb yb false) rb) - (bblast_term n (bvadd n x y) rb))))))))))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; BITBLAST BVNEG -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(program bblast_zero ((n mpz)) bblt -(mp_ifzero n bbltn - (bbltc false (bblast_zero (mp_add n (~1)))))) - -(program bblast_bvneg ((x bblt) (n mpz)) bblt - (bblast_bvadd (bblast_bvnot x) (bblast_zero n) true)) - - -(declare bv_bbl_bvneg (! n mpz - (! x (term (BitVec n)) - (! xb bblt - (! rb bblt - (! xbb (bblast_term n x xb) - (! c (^ (bblast_bvneg xb n) rb) - (bblast_term n (bvneg n x) rb)))))))) - - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; BITBLAST BVMUL -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - - -;; shift add multiplier - -;; (program concat ((a bblt) (b bblt)) bblt -;; (match a (bbltn b) -;; ((bbltc ai a') (bbltc ai (concat a' b))))) - - -(program top_k_bits ((a bblt) (k mpz)) bblt - (mp_ifzero k bbltn - (match a (bbltn (fail bblt)) - ((bbltc ai a') (bbltc ai (top_k_bits a' (mpz_sub k 1))))))) - -(program bottom_k_bits ((a bblt) (k mpz)) bblt - (reverseb (top_k_bits (reverseb a) k))) - -;; assumes the least signigicant bit is at the beginning of the list -(program k_bit ((a bblt) (k mpz)) formula -(mp_ifneg k (fail formula) -(match a (bbltn (fail formula)) - ((bbltc ai a') (mp_ifzero k ai (k_bit a' (mpz_sub k 1))))))) - -(program and_with_bit ((a bblt) (bt formula)) bblt -(match a (bbltn bbltn) - ((bbltc ai a') (bbltc (and bt ai) (and_with_bit a' bt))))) - -;; a is going to be the current result -;; carry is going to be false initially -;; b is the and of a and b[k] -;; res is going to be bbltn initially -(program mult_step_k_h ((a bblt) (b bblt) (res bblt) (carry formula) (k mpz)) bblt -(match a - (bbltn (match b (bbltn res) (default (fail bblt)))) - ((bbltc ai a') - (match b (bbltn (fail bblt)) - ((bbltc bi b') - (mp_ifneg (mpz_sub k 1) - (let carry_out (or (and ai bi) (and (xor ai bi) carry)) - (let curr (xor (xor ai bi) carry) - (mult_step_k_h a' b' (bbltc curr res) carry_out (mpz_sub k 1)))) - (mult_step_k_h a' b (bbltc ai res) carry (mpz_sub k 1)) -)))))) - -;; assumes that a, b and res have already been reversed -(program mult_step ((a bblt) (b bblt) (res bblt) (n mpz) (k mpz)) bblt -(let k' (mpz_sub n k ) -(let ak (top_k_bits a k') -(let b' (and_with_bit ak (k_bit b k)) - (mp_ifzero (mpz_sub k' 1) - (mult_step_k_h res b' bbltn false k) - (let res' (mult_step_k_h res b' bbltn false k) - (mult_step a b (reverseb res') n (mp_add k 1)))))))) - - -(program bblast_bvmul ((a bblt) (b bblt) (n mpz)) bblt -(let ar (reverseb a) ;; reverse a and b so that we can build the circuit -(let br (reverseb b) ;; from the least significant bit up -(let res (and_with_bit ar (k_bit br 0)) - (mp_ifzero (mpz_sub n 1) ;; if multiplying 1 bit numbers no need to call mult_step - res - (mult_step ar br res n 1)))))) - -(declare bv_bbl_bvmul (! n mpz - (! x (term (BitVec n)) - (! y (term (BitVec n)) - (! xb bblt - (! yb bblt - (! rb bblt - (! xbb (bblast_term n x xb) - (! ybb (bblast_term n y yb) - (! c (^ (bblast_bvmul xb yb n) rb) - (bblast_term n (bvmul n x y) rb))))))))))) - - - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; BITBLAST EQUALS -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -; bit blast x = y -; for x,y of size n, it will return a conjunction (x.0 = y.0 ^ ( ... ^ (x.{n-1} = y.{n-1}))) -; f is the accumulator formula that builds the equality in the right order -(program bblast_eq_rec ((x bblt) (y bblt) (f formula)) formula - (match x - (bbltn (match y (bbltn f) (default (fail formula)))) - ((bbltc fx x') (match y - (bbltn (fail formula)) - ((bbltc fy y') (bblast_eq_rec x' y' (and (iff fx fy) f))))) - (default (fail formula)))) - -(program bblast_eq ((x bblt) (y bblt)) formula - (match x - ((bbltc bx x') (match y ((bbltc by y') (bblast_eq_rec x' y' (iff bx by))) - (default (fail formula)))) - (default (fail formula)))) - - -;; TODO: a temporary bypass for rewrites that we don't support yet. As soon -;; as we do, remove this rule. - -(declare bv_bbl_=_false - (! n mpz - (! x (term (BitVec n)) - (! y (term (BitVec n)) - (! bx bblt - (! by bblt - (! f formula - (! bbx (bblast_term n x bx) - (! bby (bblast_term n y by) - (! c (^ (bblast_eq bx by) f) - (th_holds (iff (= (BitVec n) x y) false)))))))))))) - -(declare bv_bbl_= - (! n mpz - (! x (term (BitVec n)) - (! y (term (BitVec n)) - (! bx bblt - (! by bblt - (! f formula - (! bbx (bblast_term n x bx) - (! bby (bblast_term n y by) - (! c (^ (bblast_eq bx by) f) - (th_holds (iff (= (BitVec n) x y) f)))))))))))) - -(declare bv_bbl_=_swap - (! n mpz - (! x (term (BitVec n)) - (! y (term (BitVec n)) - (! bx bblt - (! by bblt - (! f formula - (! bbx (bblast_term n x bx) - (! bby (bblast_term n y by) - (! c (^ (bblast_eq by bx) f) - (th_holds (iff (= (BitVec n) x y) f)))))))))))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; BITBLAST BVULT -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(program bblast_bvult ((x bblt) (y bblt) (n mpz)) formula -(match x - ( bbltn (fail formula)) - ((bbltc xi x') (match y - (bbltn (fail formula)) - ((bbltc yi y') (mp_ifzero n - (and (not xi) yi) - (or (and (iff xi yi) (bblast_bvult x' y' (mp_add n (~1)))) (and (not xi) yi)))))))) - -(declare bv_bbl_bvult - (! n mpz - (! x (term (BitVec n)) - (! y (term (BitVec n)) - (! bx bblt - (! by bblt - (! f formula - (! bbx (bblast_term n x bx) - (! bby (bblast_term n y by) - (! c (^ (bblast_bvult bx by (mp_add n (~1))) f) - (th_holds (iff (bvult n x y) f)))))))))))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; BITBLAST BVSLT -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(program bblast_bvslt ((x bblt) (y bblt) (n mpz)) formula -(match x - ( bbltn (fail formula)) - ((bbltc xi x') (match y - (bbltn (fail formula)) - ((bbltc yi y') (mp_ifzero (mpz_sub n 1) - (and xi (not yi)) - (or (and (iff xi yi) - (bblast_bvult x' y' (mpz_sub n 2))) - (and xi (not yi))))))))) - -(declare bv_bbl_bvslt - (! n mpz - (! x (term (BitVec n)) - (! y (term (BitVec n)) - (! bx bblt - (! by bblt - (! f formula - (! bbx (bblast_term n x bx) - (! bby (bblast_term n y by) - (! c (^ (bblast_bvslt bx by n) f) - (th_holds (iff (bvslt n x y) f)))))))))))) - - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; BITBLAST BVCOMP -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(program bblast_bvcomp ((x bblt) (y bblt) (n mpz)) bblt - (match x ((bbltc bx x') (match y ((bbltc by y') - (bbltc (bblast_eq_rec x' y' (iff bx by)) bbltn)) - (default (fail bblt)))) - (default (fail bblt)) - )) - -(declare bv_bbl_bvcomp (! n mpz - (! x (term (BitVec n)) - (! y (term (BitVec n)) - (! xb bblt - (! yb bblt - (! rb bblt - (! xbb (bblast_term n x xb) - (! ybb (bblast_term n y yb) - (! c (^ (bblast_bvcomp xb yb n) rb) - (bblast_term 1 (bvcomp n x y) rb))))))))))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; -;; BITBLASTING CONNECTORS -;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - - -; bit-blasting connections - -(declare intro_assump_t - (! f formula - (! v var - (! C clause - (! h (th_holds f) - (! a (atom v f) - (! u (! unit (holds (clc (pos v) cln)) - (holds C)) - (holds C)))))))) - -(declare intro_assump_f - (! f formula - (! v var - (! C clause - (! h (th_holds (not f)) - (! a (atom v f) - (! u (! unit (holds (clc (neg v) cln)) - (holds C)) - (holds C)))))))) - - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; -;; REWRITE RULES -;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - - -; rewrite rule : -; x + y = y + x -(declare bvadd_symm - (! n mpz - (! x (term (BitVec n)) - (! y (term (BitVec n)) - (th_holds (= (BitVec n) (bvadd _ x y) (bvadd _ y x))))))) - -;; (declare bvcrazy_rewrite -;; (! n mpz -;; (! x (term (BitVec n)) -;; (! y (term (BitVec n)) -;; (! xn bv_poly -;; (! yn bv_poly -;; (! hxn (bv_normalizes x xn) -;; (! hyn (bv_normalizes y yn) -;; (! s (^ (rewrite_scc xn yn) true) -;; (! u (! x (term (BitVec n)) (holds cln)) -;; (holds cln))))))))))) - -;; (th_holds (= (BitVec n) (bvadd x y) (bvadd y x))))))) - - - -; necessary? -;; (program calc_bvand ((a bv) (b bv)) bv -;; (match a -;; (bvn (match b (bvn bvn) (default (fail bv)))) -;; ((bvc ba a') (match b -;; ((bvc bb b') (bvc (match ba (b0 b0) (b1 bb)) (calc_bvand a' b'))) -;; (default (fail bv)))))) - -;; ; rewrite rule (w constants) : -;; ; a & b = c -;; (declare bvand_const (! c bv -;; (! a bv -;; (! b bv -;; (! u (^ (calc_bvand a b) c) -;; (th_holds (= BitVec (bvand (a_bv a) (a_bv b)) (a_bv c)))))))) - - -;; making constant bit-vectors -(program mk_ones ((n mpz)) bv - (mp_ifzero n bvn (bvc b1 (mk_ones (mpz_sub n 1))))) - -(program mk_zero ((n mpz)) bv - (mp_ifzero n bvn (bvc b0 (mk_ones (mpz_sub n 1))))) - - - -;; (bvxnor a b) => (bvnot (bvxor a b)) -;; (declare bvxnor_elim -;; (! n mpz -;; (! a (term (BitVec n)) -;; (! b (term (BitVec n)) -;; (! a' (term (BitVec n)) -;; (! b' (term (BitVec n)) -;; (! rwa (rw_term _ a a') -;; (! rwb (rw_term _ b b') -;; (rw_term n (bvxnor _ a b) -;; (bvnot _ (bvxor _ a' b'))))))))))) - - - -;; ;; (bvxor a 0) => a -;; (declare bvxor_zero -;; (! n mpz -;; (! zero_bits bv -;; (! sc (^ (mk_zero n) zero_bits) -;; (! a (term (BitVec n)) -;; (! b (term (BitVec n)) -;; (! a' (term (BitVec n)) -;; (! rwa (rw_term _ a a') -;; (! rwb (rw_term _ b (a_bv _ zero_bits)) -;; (rw_term _ (bvxor _ a b) -;; a')))))))))) - -;; ;; (bvxor a 11) => (bvnot a) -;; (declare bvxor_one -;; (! n mpz -;; (! one_bits bv -;; (! sc (^ (mk_ones n) one_bits) -;; (! a (term (BitVec n)) -;; (! b (term (BitVec n)) -;; (! a' (term (BitVec n)) -;; (! rwa (rw_term _ a a') -;; (! rwb (rw_term _ b (a_bv _ one_bits)) -;; (rw_term _ (bvxor _ a b) -;; (bvnot _ a'))))))))))) - - -;; ;; (bvnot (bvnot a)) => a -;; (declare bvnot_idemp -;; (! n mpz -;; (! a (term (BitVec n)) -;; (! a' (term (BitVec n)) -;; (! rwa (rw_term _ a a') -;; (rw_term _ (bvnot _ (bvnot _ a)) -;; a')))))) diff --git a/proofs/signatures/th_bv_rewrites.plf b/proofs/signatures/th_bv_rewrites.plf deleted file mode 100644 index bf5dea9e9..000000000 --- a/proofs/signatures/th_bv_rewrites.plf +++ /dev/null @@ -1,22 +0,0 @@ -; -; Equality swap -; - -(declare rr_bv_eq - (! n mpz - (! t1 (term (BitVec n)) - (! t2 (term (BitVec n)) - (th_holds (iff (= (BitVec n) t2 t1) (= (BitVec n) t1 t2))))))) - -; -; Additional rules... -; - -; -; Default, if nothing else applied -; - -(declare rr_bv_default - (! t1 formula - (! t2 formula - (th_holds (iff t1 t2)))))) diff --git a/proofs/signatures/th_int.plf b/proofs/signatures/th_int.plf deleted file mode 100644 index 9a0a2d63c..000000000 --- a/proofs/signatures/th_int.plf +++ /dev/null @@ -1,25 +0,0 @@ -(declare Int sort) - -(define arithpred_Int (! x (term Int) - (! y (term Int) - formula))) - -(declare >_Int arithpred_Int) -(declare >=_Int arithpred_Int) -(declare <_Int arithpred_Int) -(declare <=_Int arithpred_Int) - -(define arithterm_Int (! x (term Int) - (! y (term Int) - (term Int)))) - -(declare +_Int arithterm_Int) -(declare -_Int arithterm_Int) -(declare *_Int arithterm_Int) ; is * ok to use? -(declare /_Int arithterm_Int) ; is / ok to use? - -; a constant term -(declare a_int (! x mpz (term Int))) - -; unary negation -(declare u-_Int (! t (term Int) (term Int))) diff --git a/proofs/signatures/th_lira.plf b/proofs/signatures/th_lira.plf deleted file mode 100644 index e3f6df112..000000000 --- a/proofs/signatures/th_lira.plf +++ /dev/null @@ -1,429 +0,0 @@ -; Deps: th_real.plf th_int.plf smt.plf sat.plf - -; Some axiom arguments are marked "; Omit", because they can be deduced from -; other arguments and should be replaced with a "_" when invoking the axiom. - -;; ====================================== ;; -;; Arith Terms, Predicates, & Conversions ;; -;; ====================================== ;; - -; Types for arithmetic variables -; Specifically a real -(declare real_var type) -; Specifically an integer -(declare int_var type) - -; Functions to map them to terms -(declare term_real_var (! v real_var (term Real))) -(declare term_int_var (! v int_var (term Int))) - -; A function to cast an integer term to real. -(declare term_int_to_real (! i (term Int) (term Real))) - - -; The recursive functions `reify_int_term` and `reify_real_term` work -; together to reify or "make real" an integer term. That is, to convert it to -; a real term. More precisely, they take an integer term and return a real -; term in which any integer variables are immediately converted to real terms, -; and all non-leaves in the term are real-sorted. -; -; They explicitly do not work on integer division, because such a conversion -; would not be correct when integer division is involved. - -; This function recursively converts an integer term to a real term. -(program reify_int_term ((t (term Int))) (term Real) - (match t - ((term_int_var v) (term_int_to_real (term_int_var v))) - ((a_int i) (a_real (mpz_to_mpq i))) - ((+_Int x y) (+_Real (reify_int_term x) (reify_int_term y))) - ((-_Int x y) (-_Real (reify_int_term x) (reify_int_term y))) - ((u-_Int x) (u-_Real (reify_int_term x))) - ((*_Int x y) (*_Real (reify_int_term x) (reify_int_term y))) - ; Reifying integer division is an error, since it changes the value! - ((/_Int x y) (fail (term Real))) - )) - -; This function recursively converts a real term to a real term. -; It will never change the top-level node in the term (since that node is -; real), but it may change subterms... -(program reify_real_term ((t (term Real))) (term Real) - (match t - ((term_real_var v) (term_real_var v)) - ((a_real v) (a_real v)) - ; We've found an integer term -- reify it! - ((term_int_to_real t') (reify_int_term t')) - ((+_Real x y) (+_Real (reify_real_term x) (reify_real_term y))) - ((-_Real x y) (-_Real (reify_real_term x) (reify_real_term y))) - ((u-_Real x) (u-_Real (reify_real_term x))) - ((*_Real x y) (*_Real (reify_real_term x) (reify_real_term y))) - ((/_Real x y) (/_Real (reify_real_term x) (reify_real_term y))) - )) - -; Predicates of the form (term Integer) (comparison) (term Real) -(define arithpred_IntReal (! x (term Int) - (! y (term Real) - formula))) -(declare >_IntReal arithpred_IntReal) -(declare >=_IntReal arithpred_IntReal) -(declare <_IntReal arithpred_IntReal) -(declare <=_IntReal arithpred_IntReal) - -; From an arith predicate, compute the equivalent real predicate -; All arith predicates are (possibly negated) >='s with a real on the right. -; Technically it's a real literal on the right, but we don't assume that here. -(program reify_arith_pred ((p formula)) formula - (match p - ((not p') (not (reify_arith_pred p'))) - ((>=_Real x y) (>=_Real (reify_real_term x) (reify_real_term y))) - ((>=_Int x y) (>=_Real (reify_int_term x) (reify_int_term y))) - ((>=_IntReal x y) (>=_Real (reify_int_term x) (reify_real_term y))) - (default (fail formula)) - )) - -; From an arith predicate, prove the equivalent real predicate -(declare pf_reified_arith_pred - (! p formula - (! p' formula - (! pf (th_holds p) - (! reify_sc (^ (reify_arith_pred p) p') - (th_holds p')))))) - -;; ========================== ;; -;; Int Bound Tightening Rules ;; -;; ========================== ;; - -; Returns whether `ceil` is the ceiling of `q`. -(program is_ceil ((q mpq) (ceil mpz)) bool - (let diff (mp_add (mpz_to_mpq ceil) (mp_neg q)) - (mp_ifneg diff - ff - (mp_ifneg (mp_add diff (~ 1/1)) - tt - ff)))) - -; Returns whether `n` is the greatest integer less than `q`. -(program is_greatest_integer_below ((n mpz) (q mpq)) bool - (is_ceil q (mp_add n 1))) - - -; Negates terms of the form: -; (a) k OR -; (b) x OR -; (c) k * x -; where k is a constant and x is a variable. -; Otherwise fails. -; This aligns closely with the LFSCArithProof::printLinearMonomialNormalizer -; function. -(program negate_linear_monomial_int_term ((t (term Int))) (term Int) - (match t - ((term_int_var v) (*_Int (a_int (~ 1)) (term_int_var v))) - ((a_int k) (a_int (mp_neg k))) - ((*_Int x y) - (match x - ((a_int k) - (match y - ((term_int_var v) (*_Int (a_int (mp_neg k)) y)) - (default (fail (term Int))))) - (default (fail (term Int))))) - (default (fail (term Int))) - )) - -; This function negates linear integer terms---sums of terms of the form -; recognized by `negate_linear_monomial_int_term`. -(program negate_linear_int_term ((t (term Int))) (term Int) - (match t - ((term_int_var v) (negate_linear_monomial_int_term t)) - ((a_int i) (negate_linear_monomial_int_term t)) - ((+_Int x y) (+_Int (negate_linear_int_term x) (negate_linear_int_term y))) - ((*_Int x y) (negate_linear_monomial_int_term t)) - (default (fail (term Int))) - )) - -; Statement that z is the greatest integer less than z'. -(declare holds_neg_of_greatest_integer_below_int - (! z mpz - (! z' mpz - type))) - -; For proving statements of the above form. -(declare check_neg_of_greatest_integer_below_int - (! z mpz - (! z' mpz - (! sc_check (^ (is_greatest_integer_below (mp_neg z) (mpz_to_mpq z')) tt) - (holds_neg_of_greatest_integer_below_int z z'))))) - -; Axiom for tightening [Int] < i into -[Int] >= -(i - 1). -; Note that [Int] < i is actually not([Int] >= i) -(declare tighten_not_>=_IntInt - (! t (term Int) ; Omit - (! neg_t (term Int) ; Omit - (! old_bound mpz ; Omit - (! neg_int_bound mpz ; Omit - (! pf_step (holds_neg_of_greatest_integer_below_int neg_int_bound old_bound) - ; Note that even when the RHS is an integer, we convert it to real and use >_IntReal - (! pf_real_bound (th_holds (not (>=_IntReal t (term_int_to_real (a_int old_bound))))) - (! sc_neg (^ (negate_linear_int_term t) neg_t) - (th_holds (>=_IntReal neg_t (term_int_to_real (a_int neg_int_bound)))))))))))) - -;; ======================================== ;; -;; Linear Combinations and Affine functions ;; -;; ======================================== ;; - -; Unifying type for both kinds of arithmetic variables -(declare arith_var type) -(declare av_from_int (! v int_var arith_var)) -(declare av_from_real (! v real_var arith_var)) - -; Total order type -- return value for the comparison of two things -(declare ord type) -(declare ord_lt ord) -(declare ord_eq ord) -(declare ord_gt ord) - -; Compare two arith vars. Integers come before reals, and otherwise we use the -; LFSC ordering -(program arith_var_cmp ((v1 arith_var) (v2 arith_var)) ord - (match v1 - ((av_from_int i1) - (match v2 - ((av_from_int i2) - (ifequal i1 i2 - ord_eq - (compare i1 i2 ord_lt ord_gt))) - ((av_from_real r2) ord_lt))) - ((av_from_real r1) - (match v2 - ((av_from_int i2) ord_gt) - ((av_from_real r2) - (ifequal r1 r2 - ord_eq - (compare r1 r2 ord_lt ord_gt))))))) - -; Type for linear combinations of variables -; NB: Functions below will assume that the list is always sorted by variable! -(declare lc type) -(declare lc_null lc) -(declare lc_cons (! c mpq (! v arith_var (! rest lc lc)))) - -; Sum of linear combinations. -(program lc_add ((l1 lc) (l2 lc)) lc - (match l1 - (lc_null l2) - ((lc_cons c1 v1 l1') - (match l2 - (lc_null l1) - ((lc_cons c2 v2 l2') - (match (arith_var_cmp v1 v2) - (ord_lt (lc_cons c1 v1 (lc_add l1' l2))) - (ord_eq - (let c (mp_add c1 c2) - (mp_ifzero c - (lc_add l1' l2') - (lc_cons c v1 (lc_add l1' l2'))))) - (ord_gt (lc_cons c2 v2 (lc_add l1 l2'))))))))) - -; Scaling a linear combination -(program lc_mul_c ((l lc) (c mpq)) lc - (match l - (lc_null l) - ((lc_cons c' v' l') (lc_cons (mp_mul c c') v' (lc_mul_c l' c))))) - -; Negating a linear combination -(program lc_neg ((l lc)) lc - (lc_mul_c l (~ 1/1))) - -; An affine function of variables (a linear combination + a constant) -(declare aff type) -(declare aff_cons (! c mpq (! l lc aff))) - -; Sum of affine functions -(program aff_add ((p1 aff) (p2 aff)) aff - (match p1 - ((aff_cons c1 l1) - (match p2 - ((aff_cons c2 l2) (aff_cons (mp_add c1 c2) (lc_add l1 l2))))))) - -; Scaling an affine function -(program aff_mul_c ((p aff) (c mpq)) aff - (match p - ((aff_cons c' l') (aff_cons (mp_mul c' c) (lc_mul_c l' c))))) - -; Negating an affine function -(program aff_neg ((p aff)) aff - (aff_mul_c p (~ 1/1))) - -; Subtracting affine functions -(program aff_sub ((p1 aff) (p2 aff)) aff - (aff_add p1 (aff_neg p2))) - -;; ================================= ;; -;; Proving (Real) terms to be affine ;; -;; ================================= ;; - -; truth type for some real term being affine -; * `t` the real term -; * `a` the equivalent affine function -(declare is_aff (! t (term Real) (! a aff type))) - -; Constants are affine -(declare is_aff_const - (! x mpq - (is_aff (a_real x) (aff_cons x lc_null)))) - -; Real variables are affine -(declare is_aff_var_real - (! v real_var - (is_aff (term_real_var v) - (aff_cons 0/1 (lc_cons 1/1 (av_from_real v) lc_null))))) - -; Int variables are affine -(declare is_aff_var_int - (! v int_var - (is_aff (term_int_to_real (term_int_var v)) - (aff_cons 0/1 (lc_cons 1/1 (av_from_int v) lc_null))))) - -; affine functions are closed under addition -(declare is_aff_+ - (! x (term Real) ; Omit - (! aff_x aff ; Omit - (! y (term Real) ; Omit - (! aff_y aff ; Omit - (! aff_z aff ; Omit - (! is_affx (is_aff x aff_x) - (! is_affy (is_aff y aff_y) - (! a (^ (aff_add aff_x aff_y) aff_z) - (is_aff (+_Real x y) aff_z)))))))))) - -; affine functions are closed under subtraction -(declare is_aff_- - (! x (term Real) ; Omit - (! aff_x aff ; Omit - (! y (term Real) ; Omit - (! aff_y aff ; Omit - (! aff_z aff ; Omit - (! is_affx (is_aff x aff_x) - (! is_affy (is_aff y aff_y) - (! a (^ (aff_sub aff_x aff_y) aff_z) - (is_aff (-_Real x y) aff_z)))))))))) - -; affine functions are closed under left-multiplication by scalars -(declare is_aff_mul_c_L - (! y (term Real) ; Omit - (! aff_y aff ; Omit - (! aff_z aff ; Omit - (! x mpq - (! is_affy (is_aff y aff_y) - (! a (^ (aff_mul_c aff_y x) aff_z) - (is_aff (*_Real (a_real x) y) aff_z)))))))) - -; affine functions are closed under right-multiplication by scalars -(declare is_aff_mul_c_R - (! y (term Real) ; Omit - (! aff_y aff ; Omit - (! aff_z aff ; Omit - (! x mpq - (! is_affy (is_aff y aff_y) - (! a (^ (aff_mul_c aff_y x) aff_z) - (is_aff (*_Real y (a_real x)) aff_z)))))))) - -;; ========================== ;; -;; Bounds on Affine Functions ;; -;; ========================== ;; - -; Bounds that an affine function might satisfy -(declare bound type) -(declare bound_pos bound) ; > 0 -(declare bound_non_neg bound) ; >= 0 - -; formulas over affine functions -; the statement that `a` satisfies `b` for all inputs -(declare bounded_aff (! a aff (! b bound formula))) - -; Sum of two bounds (the bound satisfied by the sum of two functions satisfying -; the input bounds) -(program bound_add ((b bound) (b2 bound)) bound - (match b - (bound_pos bound_pos) - (bound_non_neg b2))) - -; The implication of `a1` satisfying `b` and `a2` satisfying `b2`, obtained by -; summing the inequalities. -(program bounded_aff_add ((a1 aff) (b bound) (a2 aff) (b2 bound)) formula - (bounded_aff (aff_add a1 a2) (bound_add b b2))) - - -; The implication of scaling the inequality of `a1` satisfying `b`. -(program bounded_aff_mul_c ((a1 aff) (b bound) (c mpq)) formula - (match (mpq_ispos c) - (tt (bounded_aff (aff_mul_c a1 c) b)) - (ff (fail formula)))) - -; Does an affine function actuall satisfy a bound, for some input? -(program bound_respected ((b bound) (a aff)) bool - (match a - ((aff_cons c combo) - (match combo - (lc_null - (match b - (bound_pos (mpq_ispos c)) - (bound_non_neg (mp_ifneg c ff tt)))) - (default tt))))) - -;; =================================== ;; -;; Axioms for bounded affine functions ;; -;; =================================== ;; - -; Always true (used as a initial value when summing many bounds together) -(declare bounded_aff_ax_0_>=_0 - (th_holds (bounded_aff (aff_cons 0/1 lc_null) bound_non_neg))) - -; Contradiction axiom: an affine function that does not respect its bounds -(declare bounded_aff_contra - (! a aff ; Omit - (! b bound ; Omit - (! pf (th_holds (bounded_aff a b)) - (! sc (^ (bound_respected b a) ff) - (th_holds false)))))) - -; Rule for summing two affine bounds to get a third -(declare bounded_aff_add - (! a1 aff ; Omit - (! a2 aff ; Omit - (! b bound ; Omit - (! b2 bound ; Omit - (! ba_sum formula ; Omit - (! pf_a1 (th_holds (bounded_aff a1 b)) - (! pf_a2 (th_holds (bounded_aff a2 b2)) - (! sc (^ (bounded_aff_add a1 b a2 b2) ba_sum) - (th_holds ba_sum)))))))))) - -; Rule for scaling an affine bound -(declare bounded_aff_mul_c - (! a aff ; Omit - (! b bound ; Omit - (! ba formula ; Omit - (! c mpq - (! pf_a (th_holds (bounded_aff a b)) - (! sc (^ (bounded_aff_mul_c a b c) ba) - (th_holds ba)))))))) - - -; [y >= x] implies that the aff. function y - x is >= 0 -(declare aff_>=_from_term - (! y (term Real) ; Omit - (! x (term Real) ; Omit - (! p aff ; Omit - (! pf_affine (is_aff (-_Real y x) p) - (! pf_term_bound (th_holds (>=_Real y x)) - (th_holds (bounded_aff p bound_non_neg)))))))) - -; not [y >= x] implies that the aff. function -(y - x) is > 0 -(declare aff_>_from_term - (! y (term Real) ; Omit - (! x (term Real) ; Omit - (! p aff ; Omit - (! p_n aff ; Omit - (! pf_affine (is_aff (-_Real y x) p) - (! pf_term_bound (th_holds (not (>=_Real y x))) - (! sc_neg (^ (aff_neg p) p_n) - (th_holds (bounded_aff p_n bound_pos)))))))))) diff --git a/proofs/signatures/th_quant.plf b/proofs/signatures/th_quant.plf deleted file mode 100644 index 9fa697978..000000000 --- a/proofs/signatures/th_quant.plf +++ /dev/null @@ -1,80 +0,0 @@ -(declare forall (! s sort - (! t (term s) - (! f formula - formula)))) - -;This program recursively checks the instantiation. -;Composite terms (such as "apply _ _ ...") are handled recursively. -;Then, if ti and t are equal, we return true. Otherwise, we first verify that t is the variable for which ti is substitued (ifmarked). if this is the case, ti should be equal to k. - -(program is_inst_t ((ti term) (t term) (k term)) bool - (match t - ((apply s1 s2 t1 t2) - (match ti - ((apply si1 si2 ti1 ti2) - (match (is_inst_t ti1 t1 k) (tt (is_inst_t ti2 t2 k)) (ff ff))) - (default ff))) - (default (ifequal ti t tt (ifmarked t (ifequal ti k tt ff) ff))))) - - -(program is_inst_f ((fi formula) (f formula) (k term)) bool - (match f - ((and f1 f2) (match fi - ((and fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff))) - (default ff))) - ((or f1 f2) (match fi - ((or fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff))) - (default ff))) - ((impl f1 f2) (match fi - ((impl fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff))) - (default ff))) - ((not f1) (match fi - ((not fi1) (is_inst_f fi1 f1 k)) - (default ff))) - ((iff f1 f2) (match fi - ((iff fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff))) - (default ff))) - ((xor f1 f2) (match fi - ((xor fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff))) - (default ff))) - ((ifte f1 f2 f3) (match fi - ((ifte fi1 fi2 fi3) (match (is_inst_f fi1 f1 k) - (tt (match (is_inst_f fi2 f2 k) (tt (is_inst_f fi3 f3 k)) (ff ff))) - (ff ff))) - (default ff))) - ((= s t1 t2) (match fi - ((= s ti1 ti2) (match (is_inst_t ti1 t1 k) (tt (is_inst_t ti2 t2 k)) (ff ff))) - (default ff))) - ((forall s t1 f1) (match fi - ((forall s ti1 fi1) (is_inst_f fi1 f1 k)) - (default ff))) - (default ff))) - -(program is_inst ((fi formula) (f formula) (t term) (k term)) bool - (do (markvar t) - (let f1 (is_inst_f fi f k) - (do (markvar t) f1)))) - -(declare skolem - (! s sort - (! t (term s) - (! f formula - (! p (th_holds (not (forall s t f))) - (! u (! k (term s) - (! fi formula - (! p1 (th_holds (not fi)) - (! r (^ (is_inst fi f t k) tt) - (holds cln))))) - (holds cln))))))) - -(declare inst - (! s sort - (! t (term s) - (! f formula - (! k (term s) - (! fi formula - (! p (th_holds (forall s t f)) - (! r (^ (is_inst fi f t k) tt) - (! u (! p1 (th_holds fi) - (holds cln)) - (holds cln)))))))))) diff --git a/proofs/signatures/th_real.plf b/proofs/signatures/th_real.plf deleted file mode 100644 index dfedb28ed..000000000 --- a/proofs/signatures/th_real.plf +++ /dev/null @@ -1,34 +0,0 @@ -; Deps: smt.plf -(declare Real sort) - -(define arithpred_Real (! x (term Real) - (! y (term Real) - formula))) -(declare >_Real arithpred_Real) -(declare >=_Real arithpred_Real) -(declare <_Real arithpred_Real) -(declare <=_Real arithpred_Real) - -(define arithterm_Real (! x (term Real) - (! y (term Real) - (term Real)))) - -(declare +_Real arithterm_Real) -(declare -_Real arithterm_Real) -(declare *_Real arithterm_Real) ; is * ok to use? -(declare /_Real arithterm_Real) ; is / ok to use? - -; a constant term -(declare a_real (! x mpq (term Real))) - -(declare >=0_Real (! x (term Real) formula)) -(declare =0_Real (! x (term Real) formula)) -(declare >0_Real (! x (term Real) formula)) -(declare distinct0_Real (! x (term Real) formula)) - -; unary negation -(declare u-_Real (! t (term Real) (term Real))) - -; Is this rational positive? -(program mpq_ispos ((x mpq)) bool - (mp_ifneg x ff (mp_ifzero x ff tt))) diff --git a/test/signatures/CMakeLists.txt b/test/signatures/CMakeLists.txt deleted file mode 100644 index ffc8de55b..000000000 --- a/test/signatures/CMakeLists.txt +++ /dev/null @@ -1,43 +0,0 @@ -##################### -## CMakeLists.txt -## Top contributors (to current version): -## Andres Noetzli -## This file is part of the CVC4 project. -## Copyright (c) 2009-2021 by the authors listed in the file AUTHORS -## in the top-level source directory and their institutional affiliations. -## All rights reserved. See the file COPYING in the top-level source -## directory for licensing information. -## -set(lfsc_test_file_list - drat_test.plf - er_test.plf - example-arrays.plf - example.plf - example-quant.plf - ex_bv.plf - ex-mem.plf - lrat_test.plf - th_lira_test.plf -) - -set(test_script ${CMAKE_CURRENT_LIST_DIR}/run_test.py) - -macro(lfsc_test file) - set(test_name "signatures/${file}") - add_test( - NAME "${test_name}" - COMMAND - "${PYTHON_EXECUTABLE}" - "${test_script}" - "${LFSC_BINARY}" - "${CMAKE_CURRENT_LIST_DIR}/${file}" - "${CMAKE_SOURCE_DIR}/proofs/signatures" - WORKING_DIRECTORY ${CMAKE_CURRENT_LIST_DIR} - ) - - set_tests_properties("${test_name}" PROPERTIES LABELS "signatures") -endmacro() - -foreach(file ${lfsc_test_file_list}) - lfsc_test(${file}) -endforeach() diff --git a/test/signatures/README.md b/test/signatures/README.md deleted file mode 100644 index 4ac8cb131..000000000 --- a/test/signatures/README.md +++ /dev/null @@ -1,32 +0,0 @@ -# Signature Tests - -This directory contains tests of our LFSC proof signatures. To run just the -tests in this directory, the test label `signatures` can be used (`ctest -L -signatures`). - -## Adding a New Signature Test - -To add a new signature test file, add the file to git, for example: - -``` -git add test/signatures/new_signature_test.plf -``` - -Also add it to [CMakeLists.txt](CMakeLists.txt) in this directory and declare -the dependencies of the test as explained below. - -The signature tests are prefixed with `signatures/`, so the test for -`example.plf` will have the name `signatures/example.plf`. - -## Test Dependencies - -Tests can declare the signature files that they depend on using the `; Deps:` -directive followed by a space-separated list of files. For example: - -``` -; Deps: sat.plf smt.plf -``` - -indicates that the test depends on `sat.plf` and `smt.plf`. The run script -automatically searches for the listed files in `proofs/signatures` as well as -the directory of the test input. diff --git a/test/signatures/drat_test.plf b/test/signatures/drat_test.plf deleted file mode 100644 index d66e48f8d..000000000 --- a/test/signatures/drat_test.plf +++ /dev/null @@ -1,434 +0,0 @@ -; Deps: drat.plf -(declare TestSuccess type) - -; Test for clause_eq -(declare test_clause_eq - (! a clause - (! b clause - (! result bool - (! sc (^ - (bool_and - (bool_eq (clause_eq a b) result) - (bool_and - (bool_eq (clause_eq b a) result) - (bool_and - (bool_eq (clause_eq a a) tt) - (bool_eq (clause_eq b b) tt)))) - tt) - TestSuccess))))) - -(check - (% a var - (% b var - (@ c1 (clc (pos a) (clc (neg b) cln)) - (@ c2 (clc (pos a) (clc (neg b) cln)) - (: TestSuccess - (test_clause_eq c1 c2 tt))))))) - -(check - (% a var - (% b var - (@ c1 (clc (neg a) (clc (neg b) cln)) - (@ c2 (clc (pos a) (clc (neg b) cln)) - (: TestSuccess - (test_clause_eq c1 c2 ff))))))) - -(check - (% a var - (% b var - (@ c1 (clc (pos a) (clc (pos b) cln)) - (@ c2 (clc (pos a) (clc (neg b) cln)) - (: TestSuccess - (test_clause_eq c1 c2 ff))))))) - -(check - (% a var - (% b var - (@ c1 (clc (pos a) (clc (pos a) cln)) - (@ c2 (clc (pos a) (clc (neg b) cln)) - (: TestSuccess - (test_clause_eq c1 c2 ff))))))) - -(check - (% a var - (% b var - (@ c1 (clc (neg b) (clc (pos a) (clc (neg a) cln))) - (@ c1 (clc (neg a) (clc (neg b) (clc (pos a) cln))) - (: TestSuccess - (test_clause_eq c1 c2 ff))))))) - - -(check - (% a var - (% b var - (@ c1 (clc (pos a) (clc (pos a) (clc (neg b) cln))) - (@ c2 (clc (pos a) (clc (neg b) cln)) - (: TestSuccess - (test_clause_eq c1 c2 tt))))))) - -(check - (% a var - (% b var - (@ c1 (clc (pos a) (clc (pos a) (clc (neg b) cln))) - (@ c2 (clc (pos a) (clc (neg b) (clc (neg b) cln))) - (: TestSuccess - (test_clause_eq c1 c2 tt))))))) - -(check - (% a var - (% b var - (@ c1 (clc (pos a) (clc (pos a) (clc (neg a) cln))) - (@ c2 (clc (pos a) (clc (neg a) (clc (neg a) cln))) - (: TestSuccess - (test_clause_eq c1 c2 tt))))))) - -(check - (% a var - (% b var - (@ c1 cln - (@ c2 (clc (pos a) (clc (neg a) (clc (neg a) cln))) - (: TestSuccess - (test_clause_eq c1 c2 ff))))))) - -(declare check_rat - (! f cnf - (! c clause - (! b bool - (! sc (^ (is_rat f c) b) - bottom))))) - -(declare trust_cnf (! f cnf (cnf_holds f))) - -; RAT Test 1 -; Formula: (-p, -a) ^ (-p, b) ^( b, c) ^ (-c, a) -; Candidate RAT: (p, a) -; Answer: true -(check - (% va var - (% vb var - (% vc var - (% vp var - (check_rat - (cnfc (clc (neg vp) (clc (neg va) cln)) - (cnfc (clc (neg vp) (clc (pos vb) cln)) - (cnfc (clc (pos vb) (clc (pos vc) cln)) - (cnfc (clc (neg vc) (clc (pos va) cln)) cnfn)))) - (clc (pos vp) (clc (pos va) cln)) - tt)))))) - -; RAT Test 2 -; Formula: -; p cnf 4 8 -; 1 2 -3 0 -; -1 -2 3 0 -; 2 3 -4 0 -; -2 -3 4 0 -; -1 -3 -4 0 -; 1 3 4 0 -; -1 2 4 0 -; 1 -2 -4 0 -; Candidate RAT: -1 -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (check_rat - (cnfc (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) - (cnfc (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) - (cnfc (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) - (cnfc (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) - (cnfc (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) - (cnfc (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) - (cnfc (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) - (cnfc (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) - cnfn)))))))) - (clc (neg v1) cln) - tt)))))) - -; RAT Test 3 -; Formula: -; p cnf 4 9 -; 1 2 -3 0 -; -1 -2 3 0 -; 2 3 -4 0 -; -2 -3 4 0 -; -1 -3 -4 0 -; 1 3 4 0 -; -1 2 4 0 -; 1 -2 -4 0 -; -1 0 -; Candidate RAT: 2 -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (check_rat - (cnfc (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) - (cnfc (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) - (cnfc (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) - (cnfc (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) - (cnfc (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) - (cnfc (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) - (cnfc (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) - (cnfc (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) - (cnfc (clc (neg v1) cln) - cnfn))))))))) - (clc (pos v2) cln) - tt)))))) - -; RAT Test 4 -; Formula: -; p cnf 4 2 -; 2 -3 0 -; 1 -4 0 -; Candidate RAT: 3 -; Answer: false -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (check_rat - (cnfc (clc (pos v2) (clc (neg v3) cln)) - (cnfc (clc (pos v1) (clc (neg v4) cln)) cnfn)) - (clc (pos v3) cln) - ff)))))) - - -; DRAT Test 1 (from Example 1 @ https://www.cs.utexas.edu/~marijn/drat-trim/) -; without deletions -; Formula: -; p cnf 4 8 -; 1 2 -3 0 -; -1 -2 3 0 -; 2 3 -4 0 -; -2 -3 4 0 -; -1 -3 -4 0 -; 1 3 4 0 -; -1 2 4 0 -; 1 -2 -4 -; Proof: -; -1 0 -; 2 0 -; 0 -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (: - (holds cln) - (drat_proof_of_bottom _ - (trust_cnf (cnfc (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) - (cnfc (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) - (cnfc (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) - (cnfc (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) - (cnfc (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) - (cnfc (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) - (cnfc (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) - (cnfc (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) - cnfn))))))))) - (DRATProofa (clc (neg v1) cln) - (DRATProofa (clc (pos v2) cln) - (DRATProofa cln - DRATProofn)))))))))) - - -; DRAT Test 2 (from Example 1 @ https://www.cs.utexas.edu/~marijn/drat-trim/) -; with deletions -; Formula: -; p cnf 4 8 -; 1 2 -3 0 -; -1 -2 3 0 -; 2 3 -4 0 -; -2 -3 4 0 -; -1 -3 -4 0 -; 1 3 4 0 -; -1 2 4 0 -; 1 -2 -4 -; Proof: -; -1 0 -; d -1 -2 3 0 -; d -1 -3 -4 0 -; d -1 2 4 0 -; 2 0 -; d 1 2 -3 0 -; d 2 3 -4 0 -; 0 -(check - (% v1 var (% v2 var (% v3 var (% v4 var - (: (holds cln) - (drat_proof_of_bottom _ - (trust_cnf - (cnfc (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) - (cnfc (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) - (cnfc (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) - (cnfc (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) - (cnfc (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) - (cnfc (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) - (cnfc (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) - (cnfc (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) - cnfn))))))))) - (DRATProofa (clc (neg v1) cln) - (DRATProofd (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) - (DRATProofd (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) - (DRATProofd (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) - (DRATProofa (clc (pos v2) cln) - (DRATProofd (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) - (DRATProofd (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) - (DRATProofa cln - DRATProofn))))))))))))))) - -; ===================================== ; -; Test Suite from "Two Flavors of DRAT" ; -; ===================================== ; - -; The paper includes a number of proofs which explore specified and operational -; DRAT validity. - -; Our test predicate for asserting the specified and operational validity of -; DRAT proofs -(declare spec_oper_test - (! f cnf - (! proof DRATProof - (! spec_validity bool - (! oper_validity bool - (! sc (^ (bool_and - (bool_eq (is_specified_drat_proof f proof) spec_validity) - (bool_eq (is_operational_drat_proof f proof) oper_validity) - ) tt) - TestSuccess)))))) - - -(declare x var) -(declare y var) -(declare z var) -(declare w var) -(define ex_1_formula - (cnfc (clc (pos x) (clc (pos y) (clc (pos z) cln))) - (cnfc (clc (neg x) (clc (pos y) (clc (pos z) cln))) - (cnfc (clc (pos x) (clc (neg y) (clc (pos z) cln))) - (cnfc (clc (neg x) (clc (neg y) (clc (pos z) cln))) - (cnfc (clc (pos x) (clc (pos y) (clc (neg z) cln))) - (cnfc (clc (neg x) (clc (pos y) (clc (neg z) cln))) - (cnfc (clc (pos x) (clc (neg y) (clc (neg z) cln))) - (cnfc (clc (neg x) (clc (neg y) (clc (neg z) cln))) - cnfn))))))))) - -; Spec-valid, operationally-invalid -(define ex_1_pf_pi - (DRATProofa (clc (pos x) (clc (pos y) cln)) - (DRATProofa (clc (pos x) cln) - (DRATProofa (clc (pos w) (clc (neg x) cln)) - (DRATProofd (clc (pos w) (clc (neg x) cln)) - (DRATProofa (clc (neg w) (clc (neg x) cln)) - (DRATProofa (clc (pos w) (clc (pos x) cln)) - (DRATProofa (clc (pos y) (clc (pos w) cln)) - (DRATProofa cln - DRATProofn))))))))) - -(check - (: TestSuccess - (spec_oper_test ex_1_formula ex_1_pf_pi tt ff))) - -; Spec-invalid, operationally valid -(define ex_1_pf_sigma - (DRATProofa (clc (pos x) (clc (pos y) cln)) - (DRATProofa (clc (pos x) cln) - (DRATProofd (clc (pos x) cln) - (DRATProofa (clc (pos w) (clc (neg y) cln)) - (DRATProofa (clc (neg w) (clc (neg y) cln)) - (DRATProofa (clc (pos w) cln) - (DRATProofa cln - DRATProofn)))))))) - -(check - (: TestSuccess - (spec_oper_test ex_1_formula ex_1_pf_sigma ff tt))) - -(declare x1 var) -(declare x2 var) -(declare x3 var) -(declare x4 var) -(declare x5 var) -(declare x6 var) -(declare x7 var) -(declare x8 var) -(declare x9 var) -(declare x10 var) - -(define ex_2_formula - (cnfc (clc (pos x1) cln) - (cnfc (clc (neg x1) (clc (pos x2) cln)) - (cnfc (clc (neg x1) (clc (neg x2) (clc (pos x3) cln))) - (cnfc (clc (neg x1) (clc (neg x3) (clc (pos x4) cln))) - (cnfc (clc (pos x5) (clc (pos x6) cln)) - (cnfc (clc (neg x2) (clc (neg x5) (clc (pos x7) cln))) - (cnfc (clc (neg x1) (clc (neg x5) (clc (pos x6) cln))) - (cnfc (clc (neg x5) (clc (neg x6) (clc (pos x4) cln))) - (cnfc (clc (neg x3) (clc (neg x6) (clc (pos x8) cln))) - (cnfc (clc (neg x6) (clc (neg x4) (clc (pos x3) cln))) - (cnfc (clc (neg x8) (clc (pos x5) cln)) - (cnfc (clc (neg x3) (clc (pos x9) (clc (pos x10) cln))) - (cnfc (clc (neg x4) (clc (neg x9) (clc (pos x10) cln))) - (cnfc (clc (neg x10) (clc (pos x9) cln)) - (cnfc (clc (neg x9) (clc (pos x7) cln)) - (cnfc (clc (neg x7) (clc (neg x8) (clc (neg x9) (clc (neg x10) cln)))) - cnfn))))))))))))))))) - -; Spec-valid, operationally-valid -(define ex_2_pf_tau - (DRATProofa (clc (pos x5) cln) - (DRATProofa (clc (pos x4) cln) - (DRATProofa (clc (pos x9) cln) - (DRATProofa cln - DRATProofn))))) - -(check - (: TestSuccess - (spec_oper_test ex_2_formula ex_2_pf_tau tt tt))) - -; Spec-valid, operationally unspecified in the paper, but its operationally valid. -(define ex_3_pf_tau_prime - (DRATProofa (clc (pos x5) cln) - (DRATProofd (clc (neg x1) (clc (pos x2) cln)) - (DRATProofa (clc (pos x9) cln) - (DRATProofa cln - DRATProofn))))) - -(check - (: TestSuccess - (spec_oper_test ex_2_formula ex_3_pf_tau_prime tt tt))) - -; Spec-invalid, operationally-invalid -(define ex_4_pf_pi_prime - (DRATProofa (clc (pos x) (clc (pos y) cln)) - (DRATProofa (clc (pos x) cln) - (DRATProofa (clc (pos w) (clc (neg x) cln)) - (DRATProofa (clc (neg w) (clc (neg x) cln)) - (DRATProofa (clc (pos w) (clc (pos x) cln)) - (DRATProofa (clc (pos y) (clc (pos w) cln)) - (DRATProofa cln - DRATProofn)))))))) - -(check - (: TestSuccess - (spec_oper_test ex_1_formula ex_4_pf_pi_prime ff ff))) - - -; Spec-valid, operationally valid -(define ex_5_pf_sigma_prime - (DRATProofa (clc (pos x) (clc (pos y) cln)) - (DRATProofa (clc (pos x) cln) - (DRATProofa (clc (pos w) (clc (neg y) cln)) - (DRATProofa (clc (neg w) (clc (neg y) cln)) - (DRATProofa (clc (pos w) cln) - (DRATProofa cln - DRATProofn))))))) - -(check - (: TestSuccess - (spec_oper_test ex_1_formula ex_5_pf_sigma_prime tt tt))) - diff --git a/test/signatures/er_test.plf b/test/signatures/er_test.plf deleted file mode 100644 index 671efdb46..000000000 --- a/test/signatures/er_test.plf +++ /dev/null @@ -1,89 +0,0 @@ -; Deps: er.plf - -; This is a circuitous proof that uses the definition introduction and -; unrolling rules -(check - (% v1 var - (% v2 var - (% pf_c1 (holds (clc (pos v1) (clc (pos v2) cln))) - (% pf_c2 (holds (clc (neg v1) (clc (pos v2) cln))) - (% pf_c3 (holds (clc (pos v1) (clc (neg v2) cln))) - (% pf_c4 (holds (clc (neg v1) (clc (neg v2) cln))) - (: (holds cln) - (decl_definition - (neg v1) - (clc (neg v2) cln) - (\ v3 - (\ 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_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 - (satlem_simplify _ _ _ (R _ _ pf_c9 pf_c7 v3) (\ pf_c10 ; ~v2 ~v1 - (satlem_simplify _ _ _ (Q _ _ pf_c10 pf_c8 v2) (\ pf_c11 ; ~v1 - (satlem_simplify _ _ _ (Q _ _ pf_c11 pf_c3 v1) (\ pf_c12 ; ~v2 - (satlem_simplify _ _ _ (Q _ _ pf_c12 pf_c8 v2) (\ pf_c13 ; empty - pf_c13 - )) - )) - )) - )) - )) - )) - ) - ))) - ) - )) - ) - ) - )))) - )) -) - -; This is a test of ER proof produced by drat2er on Example 1 from: -; https://www.cs.utexas.edu/~marijn/drat-trim/ -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (% pf_c1 (holds (clc (pos v1) (clc (pos v2) (clc (neg v3) cln)))) - (% pf_c2 (holds (clc (neg v1) (clc (neg v2) (clc (pos v3) cln)))) - (% pf_c3 (holds (clc (pos v2) (clc (pos v3) (clc (neg v4) cln)))) - (% pf_c4 (holds (clc (neg v2) (clc (neg v3) (clc (pos v4) cln)))) - (% pf_c5 (holds (clc (neg v1) (clc (neg v3) (clc (neg v4) cln)))) - (% pf_c6 (holds (clc (pos v1) (clc (pos v3) (clc (pos v4) cln)))) - (% pf_c7 (holds (clc (neg v1) (clc (pos v2) (clc (pos v4) cln)))) - (% pf_c8 (holds (clc (pos v1) (clc (neg v2) (clc (neg v4) cln)))) - (: (holds cln) - (decl_definition - (neg v1) - cln - (\ v5 - (\ 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: (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 - (satlem_simplify _ _ _ (Q _ _ (R _ _ pf_c2 pf_c5 v3) pf_c8 v1) (\ pf_c14 - (satlem_simplify _ _ _ (Q _ _ (R _ _ pf_c7 pf_c2 v2) pf_c6 v1) (\ pf_c15 - (satlem_simplify _ _ _ (Q _ _ (R _ _ pf_c7 pf_c5 v4) pf_c1 v1) (\ pf_c16 - (satlem_simplify _ _ _ (R _ _ (Q _ _ pf_c3 pf_c15 v4) pf_c16 v3) (\ pf_c17 - (satlem_simplify _ _ _ (Q _ _ (R _ _ (Q _ _ pf_c4 pf_c15 v3) pf_c14 v4) pf_c17 v2) (\ pf_c18 - pf_c18 - )))))))))))))))) - ))) - ) - )) - ) - ) - )))))))) - )))) -) diff --git a/test/signatures/ex-mem.plf b/test/signatures/ex-mem.plf deleted file mode 100644 index 87d1053c4..000000000 --- a/test/signatures/ex-mem.plf +++ /dev/null @@ -1,64 +0,0 @@ -; Deps: sat.plf smt.plf th_base.plf - -(check -(% s sort -(% a (term s) -(% b (term s) -(% c (term s) -(% f (term (arrow s s)) - -; -------------------- declaration of input formula ----------------------------------- - -(% A1 (th_holds (= s a b)) -(% A2 (th_holds (= s b c)) -(% A3 (th_holds (not (= s a c))) - -; ------------------- specify that the following is a proof of the empty clause ----------------- - -(: (holds cln) - -; ---------- use atoms (a1, a2, a3) to map theory literals to boolean literals (v1, v2, v3) ------ - -(decl_atom (= s a b) (\ v1 (\ a1 -(decl_atom (= s b c) (\ v2 (\ a2 -(decl_atom (= s a c) (\ v3 (\ a3 - -; --------------------------- proof of theory lemma --------------------------------------------- - -(satlem _ _ (ast _ _ _ a1 (\ l1 (ast _ _ _ a2 (\ l2 (asf _ _ _ a3 (\ l3 (clausify_false (contra _ (trans _ _ _ _ l1 l2) l3)))))))) (\ CT1 - -; -------------------- clausification of input formulas ----------------------------------------- - -(satlem _ _ -(asf _ _ _ a1 (\ l1 -(clausify_false - (contra _ A1 l1) -))) (\ C1 -; C1 is the clause ( v1 ) - -(satlem _ _ -(asf _ _ _ a2 (\ l2 -(clausify_false - (contra _ A2 l2) -))) (\ C2 -; C2 is the clause ( v2 ) - -(satlem _ _ -(ast _ _ _ a3 (\ l3 -(clausify_false - (contra _ l3 A3) -))) (\ C3 -; C3 is the clause ( ~v3 ) - - -; -------------------- resolution proof ------------------------------------------------------------ - -(satlem_simplify _ _ _ - -(R _ _ -(R _ _ C2 -(R _ _ C1 CT1 v1) v2) C3 v3) - -(\ x x)) - -))))))))))))))))))))))))))) diff --git a/test/signatures/ex_bv.plf b/test/signatures/ex_bv.plf deleted file mode 100644 index a4f5ad816..000000000 --- a/test/signatures/ex_bv.plf +++ /dev/null @@ -1,60 +0,0 @@ -; Deps: sat.plf smt.plf th_base.plf th_bv.plf th_bv_bitblast.plf - -; (a = b) ^ (a = b & 00000) ^ (b = 11111) is UNSAT - -(check -(% a var_bv -(% b var_bv -(% f1 (th_holds (= (BitVec 4) (a_var_bv _ a) (a_var_bv _ b))) -(% f2 (th_holds (= (BitVec 4) (a_var_bv _ a) (bvand 4 (a_var_bv 4 b) (a_bv _ (bvc b0 (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn))))))))) -(% f3 (th_holds (= (BitVec 4) (a_var_bv _ b) (a_bv _ (bvc b1 (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn)))))))) -(: (holds cln) - -;; (decl_bv_term_var 5 a (\ ba1 -;; (decl_bv_term_var 5 b (\ ba2 -;; (decl_bv_term_const _ (bvc b0 (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn))))) (\ c (\ ba3 -;; (decl_bv_term_const _ (bvc b1 (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn))))) (\ d (\ ba4 - -(decl_atom (bitof a 4) (\ v1 (\ a1 -(decl_atom (bitof b 4) (\ v2 (\ a2 - -; bitblasting terms -(decl_bblast _ _ _ (bv_bbl_var 4 a _ ) (\ bt1 -(decl_bblast _ _ _ (bv_bbl_var 4 b _ ) (\ bt2 -(decl_bblast _ _ _ (bv_bbl_const 4 _ (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn))))) (\ bt3 -(decl_bblast _ _ _ (bv_bbl_const 4 _ (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn))))) (\ bt4 -(decl_bblast _ _ _ (bv_bbl_bvand 4 _ _ _ _ _ bt1 bt3) (\ bt5 - -; bitblasting formulas -(th_let_pf _ (bv_bbl_= _ _ _ _ _ _ bt1 bt2) (\ bf1 -(th_let_pf _ (bv_bbl_bvult _ _ _ _ _ _ bt1 bt5) (\ bf2 -(th_let_pf _ (bv_bbl_= _ _ _ _ _ _ bt2 bt4) (\ bf3 - -; CNFication -; a.4 V ~b.4 -(satlem _ _ -(asf _ _ _ a1 (\ l1 -(ast _ _ _ a2 (\ l2 -(clausify_false - trust -))))) (\ C2 - -; ~a.4 -(satlem _ _ -(ast _ _ _ a1 (\ l1 -(clausify_false - trust -))) (\ C3 - -; b.4 -(satlem _ _ -(asf _ _ _ a2 (\ l2 -(clausify_false - trust -))) (\ C6 - - -(satlem_simplify _ _ _ -(R _ _ (R _ _ C6 C2 v2) C3 v1) (\ x x)) - -))))))))))))))))))))))))))))))))))))))))))))) diff --git a/test/signatures/example-arrays.plf b/test/signatures/example-arrays.plf deleted file mode 100644 index 0e840274f..000000000 --- a/test/signatures/example-arrays.plf +++ /dev/null @@ -1,139 +0,0 @@ -; Deps: sat.plf smt.plf th_base.plf th_arrays.plf - -; -------------------------------------------------------------------------------- -; literals : -; L1 : a = write( a, i, read( a, i ) -; L2 : read( a, k ) = read( write( a, i, read( a, i ) ), k ) -; L3 : i = k - -; input : -; ~L1 - -; (extenstionality) lemma : -; L1 or ~L2 - -; theory conflicts : -; L2 or ~L3 -; L2 or L3 - - -; With the theory lemma, the input is unsatisfiable. -; -------------------------------------------------------------------------------- - - -; (0) -------------------- term declarations ----------------------------------- - -(check -(% I sort -(% E sort -(% a (term (Array I E)) -(% i (term I) - - -; (1) -------------------- input formula ----------------------------------- - -(% A1 (th_holds (not (= (Array I E) a (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i))))) - - - - -; (2) ------------------- specify that the following is a proof of the empty clause ----------------- - -(: (holds cln) - - - - -; (3) -------------------- theory lemmas prior to rewriting/preprocess/CNF ----------------- -; --- these should introduce (th_holds ...) - - -; extensionality lemma : notice this also introduces skolem k -(ext _ _ a (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i)) (\ k (\ A2 - - - - -; (4) -------------------- map theory literals to boolean variables -; --- maps all theory literals involved in proof to boolean literals - -(decl_atom (= (Array I E) a (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i))) (\ v1 (\ a1 -(decl_atom (= E (apply _ _ (apply _ _ (read I E) a) k) (apply _ _ (apply _ _ (read I E) (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i))) k)) (\ v2 (\ a2 -(decl_atom (= I i k) (\ v3 (\ a3 - - - -; (5) -------------------- theory conflicts --------------------------------------------- -; --- these should introduce (holds ...) - -(satlem _ _ -(asf _ _ _ a3 (\ l3 -(asf _ _ _ a2 (\ l2 -(clausify_false - - ; use read over write rule "row" - (contra _ (symm _ _ _ (row _ _ _ _ a (apply _ _ (apply _ _ (read I E) a) i) l3)) l2) - -))))) (\ CT1 -; CT1 is the clause ( v2 V v3 ) - -(satlem _ _ -(ast _ _ _ a3 (\ l3 -(asf _ _ _ a2 (\ l2 -(clausify_false - - ; use read over write rule "row1" - (contra _ (symm _ _ _ - (trans _ _ _ _ - (symm _ _ _ (cong _ _ _ _ _ _ - (refl _ (apply _ _ (read I E) (apply _ _ (apply _ _ (apply _ _ (write I E) a) i) (apply _ _ (apply _ _ (read I E) a) i)))) - l3)) - (trans _ _ _ _ - (row1 _ _ a i (apply _ _ (apply _ _ (read I E) a) i)) - (cong _ _ _ _ _ _ (refl _ (apply _ _ (read I E) a)) l3) - ))) - l2) - -))))) (\ CT2 -; CT2 is the clause ( v2 V ~v3 ) - - -; (6) -------------------- clausification ----------------------------------------- -; --- these should introduce (holds ...) - -(satlem _ _ -(ast _ _ _ a1 (\ l1 -(clausify_false - -; input formula A1 is ( ~a1 ) -; the following is a proof of a1 ^ ( ~a1 ) => false - - (contra _ l1 A1) - -))) (\ C1 -; C1 is the clause ( ~v1 ) - - -(satlem _ _ -(asf _ _ _ a1 (\ l1 -(ast _ _ _ a2 (\ l2 -(clausify_false - -; lemma A2 is ( a1 V ~a2 ) -; the following is a proof of ~a1 ^ a2 ^ ( a1 V ~a2 ) => false - - (contra _ l2 (or_elim_1 _ _ l1 A2)) - -))))) (\ C2 -; C2 is the clause ( v1 V ~v2 ) - - -; (7) -------------------- resolution proof ------------------------------------------------------------ - -(satlem_simplify _ _ _ - -(R _ _ (R _ _ CT1 CT2 v3) (R _ _ C2 C1 v1) v2) - -(\ x x)) - -))))))))))))))))))))))))))) diff --git a/test/signatures/example-quant.plf b/test/signatures/example-quant.plf deleted file mode 100644 index 611fd182c..000000000 --- a/test/signatures/example-quant.plf +++ /dev/null @@ -1,95 +0,0 @@ -; Deps: sat.plf smt.plf th_base.plf th_quant.plf - -; -------------------------------------------------------------------------------- -; literals : -; L1 : forall x. x != x -; L2 : t = t - -; input : -; L1 - -; (instantiation) lemma : -; L1 => L2 - -; theory conflicts : -; ~L2 - - -; With the theory lemma, the input is unsatisfiable. -; -------------------------------------------------------------------------------- - - -; (0) -------------------- term declarations ----------------------------------- - -(check -(% s sort -(% t (term s) - - -; (1) -------------------- input formula ----------------------------------- - -(% x (term s) -(% A1 (th_holds (forall _ x (not (= _ x x)))) - - - -; (2) ------------------- specify that the following is a proof of the empty clause ----------------- - -(: (holds cln) - - - -; (3) -------------------- theory lemmas prior to rewriting/preprocess/CNF ----------------- -; --- these should introduce (th_holds ...) - - -; instantiation lemma -(inst _ _ _ t (not (= _ t t)) A1 (\ A2 - - - - -; (4) -------------------- map theory literals to boolean variables -; --- maps all theory literals involved in proof to boolean literals - -(decl_atom (forall _ x (not (= _ x x))) (\ v1 (\ a1 -(decl_atom (= _ t t) (\ v2 (\ a2 - - - - -; (5) -------------------- theory conflicts --------------------------------------------- -; --- these should introduce (holds ...) - -(satlem _ _ -(asf _ _ _ a2 (\ l2 -(clausify_false - - (contra _ (refl _ t) l2) - -))) (\ CT1 -; CT1 is the clause ( v2 ) - - -; (6) -------------------- clausification ----------------------------------------- -; --- these should introduce (holds ...) - -(satlem _ _ -(ast _ _ _ a2 (\ l2 -(clausify_false - - (contra _ l2 A2) - -))) (\ C1 -; C1 is the clause ( ~v2 ) - - -; (7) -------------------- resolution proof ------------------------------------------------------------ - -(satlem_simplify _ _ _ - -(R _ _ CT1 C1 v2) - -(\ x x)) - -)))))))))))))))))) diff --git a/test/signatures/example.plf b/test/signatures/example.plf deleted file mode 100644 index 775557fa6..000000000 --- a/test/signatures/example.plf +++ /dev/null @@ -1,116 +0,0 @@ -; Deps: sat.plf smt.plf th_base.plf - -; -------------------------------------------------------------------------------- -; input : -; ( a = b ) -; ( b = f(c) ) -; ( a != f(c) V a != b ) - -; theory lemma (by transitivity) : -; ( a != b V b != f(c) V a = f(c) ) - - -; With the theory lemma, the input is unsatisfiable. -; -------------------------------------------------------------------------------- - - - -(check -(% s sort -(% a (term s) -(% b (term s) -(% c (term s) -(% f (term (arrow s s)) - -; -------------------- declaration of input formula ----------------------------------- - -(% A1 (th_holds (= s a b)) -(% A2 (th_holds (= s b (apply _ _ f c))) -(% A3 (th_holds (or (not (= s a (apply _ _ f c))) (not (= s a b)))) - - -; ------------------- specify that the following is a proof of the empty clause ----------------- - -(: (holds cln) - -; ---------- use atoms (a1, a2, a3) to map theory literals to boolean literals (v1, v2, v3) ------ - -(decl_atom (= s a b) (\ v1 (\ a1 -(decl_atom (= s b (apply _ _ f c)) (\ v2 (\ a2 -(decl_atom (= s a (apply _ _ f c)) (\ v3 (\ a3 - - -; --------------------------- proof of theory lemma --------------------------------------------- - -(satlem _ _ -(ast _ _ _ a1 (\ l1 -(ast _ _ _ a2 (\ l2 -(asf _ _ _ a3 (\ l3 -(clausify_false - -; this should be a proof of l1 ^ l2 ^ ~l3 => false -; this is done by theory proof rules (currently just use "trust") - - trust - -))))))) (\ CT -; CT is the clause ( ~v1 V ~v2 V v3 ) - -; -------------------- clausification of input formulas ----------------------------------------- - -(satlem _ _ -(asf _ _ _ a1 (\ l1 -(clausify_false - -; input formula A1 is ( ~l1 ) -; the following should be a proof of l1 ^ ( ~l1 ) => false -; this is done by natural deduction rules - - (contra _ A1 l1) - -))) (\ C1 -; C1 is the clause ( v1 ) - - -(satlem _ _ -(asf _ _ _ a2 (\ l2 -(clausify_false - -; input formula A2 is ( ~l2 ) -; the following should be a proof of l2 ^ ( ~l2 ) => false -; this is done by natural deduction rules - - (contra _ A2 l2) - -))) (\ C2 -; C2 is the clause ( v2 ) - - -(satlem _ _ -(ast _ _ _ a3 (\ l3 -(ast _ _ _ a1 (\ l1 -(clausify_false - -; input formula A3 is ( ~a3 V ~a1 ) -; the following should be a proof of a3 ^ a1 ^ ( ~a3 V ~a1 ) => false -; this is done by natural deduction rules - - (contra _ l1 (or_elim_1 _ _ (not_not_intro _ l3) A3)) - -))))) (\ C3 -; C3 is the clause ( ~v3 V ~v1 ) - - - -; -------------------- resolution proof ------------------------------------------------------------ - -(satlem_simplify _ _ _ - -(R _ _ C1 -(R _ _ C2 -(R _ _ CT C3 v3) v2) v1) - -(\ x x)) - -)))))))))))))))))))))))))) -) diff --git a/test/signatures/lrat_test.plf b/test/signatures/lrat_test.plf deleted file mode 100644 index 466216ff9..000000000 --- a/test/signatures/lrat_test.plf +++ /dev/null @@ -1,892 +0,0 @@ -; Deps: lrat.plf -(declare test_clause_append - (! c1 clause - (! c2 clause - (! cr clause - (! sc (^ (clause_append c1 c2) cr) type))))) - -; Test passes if the (test_clause_append ...) application is well-typed. -(check - (% v1 var - (% v2 var - (% v3 var - (test_clause_append - (clc (pos v1) (clc (neg v2) cln)) - (clc (pos v3) (clc (neg v2) cln)) - (clc (pos v1) (clc (neg v2) (clc (pos v3) (clc (neg v2) cln)))) - ) - ))) -) - -; Test passes if the (test_clause_append ...) application is well-typed. -(check - (% v2 var - (% v3 var - (test_clause_append - cln - (clc (pos v3) (clc (neg v2) cln)) - (clc (pos v3) (clc (neg v2) cln)) - ) - )) -) - -; Test passes if the (test_clause_append ...) application is well-typed. -(check - (% v2 var - (% v3 var - (test_clause_append - (clc (pos v3) (clc (neg v2) cln)) - cln - (clc (pos v3) (clc (neg v2) cln)) - ) - )) -) - -(declare test_CMap_remove_many - (! is CIList - (! cs CMap - (! csr CMap - (! sc (^ (CMap_remove_many is cs) csr) type))))) - -; Test passes if the (test_CMap_remove_many ...) application is well-typed. -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (@ c1 (clc (pos v4) (clc (neg v2) cln)) - (@ c2 (clc (neg v3) (clc (neg v1) cln)) - (@ c3 (clc (neg v2) (clc (pos v3) cln)) - (@ c4 (clc (neg v3) (clc (neg v4) cln)) - (@ cs_in (CMapc 0 c1 (CMapc 3 c2 (CMapc 4 c3 (CMapc 5 c3 (CMapc 6 c4 CMapn))))) - (@ cs_out (CMapc 3 c2 (CMapc 5 c3 CMapn)) - (@ is_in (CIListc 0 (CIListc 4 (CIListc 6 CIListn))) - (test_CMap_remove_many - is_in - cs_in - cs_out - ) - ))) - )))) - )))) -) - -; Test passes if the (test_CMap_remove_many ...) application is well-typed. -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (@ c1 (clc (pos v4) (clc (neg v2) cln)) - (@ c2 (clc (neg v3) (clc (neg v1) cln)) - (@ c3 (clc (neg v2) (clc (pos v3) cln)) - (@ c4 (clc (neg v3) (clc (neg v4) cln)) - (@ cs_in (CMapc 0 c1 (CMapc 3 c2 (CMapc 4 c3 (CMapc 5 c3 (CMapc 6 c4 CMapn))))) - (@ cs_out (CMapc 0 c1 (CMapc 3 c2 (CMapc 5 c3 (CMapc 6 c4 CMapn)))) - (@ is_in (CIListc 4 CIListn) - (test_CMap_remove_many - is_in - cs_in - cs_out - ) - ))) - )))) - )))) -) - -(declare test_clause_remove_all - (! l lit - (! c clause - (! c' clause - (! sc (^ (clause_remove_all l c) c') type))))) - -; Test passes if the (test_clause_remove_all ...) application is well-typed. -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (@ c1 (clc (pos v4) (clc (neg v2) (clc (neg v2) (clc (pos v2) (clc (pos v1) cln))))) - (@ c2 (clc (pos v4) (clc (pos v2) (clc (pos v1) cln))) - (test_clause_remove_all - (neg v2) - c1 - c2 - ) - )) - )))) -) - -(declare test_collect_resolution_targets - (! cs CMap - (! c clause - (! is CIList - (! sc (^ (collect_resolution_targets cs c) is) type))))) - -; Test passes if the (test_collect_resolution_targets ...) application is well-typed. -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (@ c1 (clc (pos v3) (clc (neg v2) cln)) - (@ c2 (clc (neg v3) (clc (neg v1) cln)) - (@ c3 (clc (neg v2) (clc (pos v3) cln)) - (@ c4 (clc (neg v3) (clc (pos v3) cln)) - (@ ct (clc (neg v3) (clc (neg v4) cln)) - (@ cs_in (CMapc 0 c1 (CMapc 3 c2 (CMapc 4 c3 (CMapc 5 c3 (CMapc 6 c4 CMapn))))) - (@ is_out (CIListc 0 (CIListc 4 (CIListc 5 (CIListc 6 CIListn)))) - (test_collect_resolution_targets - cs_in - ct - is_out - ) - ))) - )))) - )))) -) - -(declare test_resolution_targets_match - (! c CIList - (! g RATHints - (! ans bool - (! sc (^ (resolution_targets_match c g) ans) type))))) - -; Test passes if the (test_resolution_targets_match ...) application is well-typed. -(check - (@ idxs_in (CIListc 0 (CIListc 4 (CIListc 5 (CIListc 6 CIListn)))) - (@ hints_in - (RATHintsc 0 Tracen - (RATHintsc 4 Tracen - (RATHintsc 5 Tracen - (RATHintsc 6 Tracen - RATHintsn)))) - (test_resolution_targets_match - idxs_in - hints_in - tt - ) - )) -) - -; Test passes if the (test_resolution_targets_match ...) application is well-typed. -(check - (@ idxs_in (CIListc 0 (CIListc 2 (CIListc 5 (CIListc 6 CIListn)))) - (@ hints_in - (RATHintsc 0 Tracen - (RATHintsc 4 Tracen - (RATHintsc 5 Tracen - (RATHintsc 6 Tracen - RATHintsn)))) - (test_resolution_targets_match - idxs_in - hints_in - ff - ) - )) -) - -(declare test_is_at_trace - (! cs CMap - (! c clause - (! t Trace - (! r UPResult - (! sc (^ (is_at_trace cs c t) r) type)))))) - -; Test passes if the (test_is_at_trace ...) application is well-typed. -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (@ c1 (clc (pos v3) (clc (neg v2) cln)) - (@ c2 (clc (neg v3) (clc (neg v1) cln)) - (@ c3 (clc (neg v2) (clc (pos v1) cln)) - (@ c4 (clc (neg v3) (clc (pos v2) cln)) - (@ cs (CMapc 0 c1 (CMapc 3 c2 (CMapc 5 c3 (CMapc 6 c4 CMapn)))) - (@ c (clc (neg v3) cln) - (@ t (Tracec 3 (Tracec 5 (Tracec 6 Tracen))) - (test_is_at_trace - cs - c - t - UPR_Bottom - ) - ))) - )))) - )))) -) - -; Test passes if the (test_is_at_trace ...) application is well-typed. -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (@ c1 (clc (pos v3) (clc (neg v2) cln)) - (@ c2 (clc (neg v3) (clc (neg v1) cln)) - (@ c3 (clc (neg v2) (clc (pos v1) cln)) - (@ c4 (clc (neg v3) (clc (pos v2) cln)) - (@ cs (CMapc 0 c1 (CMapc 3 c2 (CMapc 5 c3 (CMapc 6 c4 CMapn)))) - (@ c (clc (neg v3) cln) - (@ t (Tracec 3 (Tracec 5 Tracen)) - (test_is_at_trace - cs - c - t - UPR_Ok - ) - ))) - )))) - )))) -) - -; Test passes if the (test_is_at_trace ...) application is well-typed. -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (@ c1 (clc (pos v3) (clc (neg v2) cln)) - (@ c2 (clc (neg v3) (clc (neg v1) cln)) - (@ c3 (clc (neg v2) (clc (pos v1) cln)) - (@ c4 (clc (neg v3) (clc (pos v2) cln)) - (@ cs (CMapc 1 c1 (CMapc 2 c2 (CMapc 3 c3 (CMapc 4 c4 CMapn)))) - (@ c (clc (neg v3) cln) - (@ t (Tracec 2 (Tracec 1 Tracen)) - (test_is_at_trace - cs - c - t - UPR_Broken - ) - ))) - )))) - )))) -) - -(declare test_is_rat_trace (! cs CMap - (! c clause - (! t Trace - (! h RATHints - (! r UPResult - (! sc (^ (is_rat_trace cs c t h) r) type))))))) - -; Test passes if the (test_is_rat_trace ...) application is well-typed. -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (@ c1 (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) - (@ c2 (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) - (@ c3 (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) - (@ c4 (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) - (@ c5 (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) - (@ c6 (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) - (@ c7 (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) - (@ c8 (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) - (@ cs (CMapc 1 c1 - (CMapc 2 c2 - (CMapc 3 c3 - (CMapc 4 c4 - (CMapc 5 c5 - (CMapc 6 c6 - (CMapc 7 c7 - (CMapc 8 c8 CMapn)))))))) - (@ c (clc (pos v1) cln) - (@ t Tracen - (@ h (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen)) - (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen)) - (RATHintsc 7 (Tracec 6 (Tracec 1 Tracen)) - RATHintsn))) - (test_is_rat_trace - cs - c - t - h - UPR_Bottom - ) - )))) - )))))))) - )))) -) - -; Test passes if the (test_is_rat_trace ...) application is well-typed. -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (@ c1 (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) - (@ c2 (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) - (@ c3 (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) - (@ c4 (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) - (@ c5 (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) - (@ c6 (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) - (@ c7 (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) - (@ c8 (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) - (@ cs (CMapc 1 c1 - (CMapc 2 c2 - (CMapc 3 c3 - (CMapc 4 c4 - (CMapc 5 c5 - (CMapc 6 c6 - (CMapc 7 c7 - (CMapc 8 c8 CMapn)))))))) - (@ c (clc (pos v1) cln) - (@ t Tracen - (@ h (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen)) - (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen)) - RATHintsn)) - (test_is_rat_trace - cs - c - t - h - UPR_Broken - ) - )))) - )))))))) - )))) -) - -; Test passes if the (test_is_rat_trace ...) application is well-typed. -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (@ c1 (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) - (@ c2 (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) - (@ c3 (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) - (@ c4 (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) - (@ c5 (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) - (@ c6 (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) - (@ c7 (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) - (@ c8 (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) - (@ cs (CMapc 1 c1 - (CMapc 2 c2 - (CMapc 3 c3 - (CMapc 4 c4 - (CMapc 5 c5 - (CMapc 6 c6 - (CMapc 7 c7 - (CMapc 8 c8 CMapn)))))))) - (@ c (clc (pos v1) cln) - (@ t Tracen - (@ h (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen)) - (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen)) - (RATHintsc 7 (Tracec 3 (Tracec 1 Tracen)) - RATHintsn))) - (test_is_rat_trace - cs - c - t - h - UPR_Broken - ) - )))) - )))))))) - )))) -) - -; Test passes if the (test_is_rat_trace ...) application is well-typed. -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (@ c1 (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) - (@ c2 (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) - (@ c3 (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) - (@ c4 (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) - (@ c5 (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) - (@ c6 (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) - (@ c7 (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) - (@ c8 (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) - (@ cs (CMapc 1 c1 - (CMapc 2 c2 - (CMapc 3 c3 - (CMapc 4 c4 - (CMapc 5 c5 - (CMapc 6 c6 - (CMapc 7 c7 - (CMapc 8 c8 CMapn)))))))) - (@ c (clc (pos v1) cln) - (@ t Tracen - (@ h (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen)) - (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen)) - (RATHintsc 7 (Tracec 3 Tracen) - RATHintsn))) - (test_is_rat_trace - cs - c - t - h - UPR_Broken - ) - )))) - )))))))) - )))) -) - -; Test passes if the (test_is_rat_trace ...) application is well-typed. -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (@ c1 (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) - (@ c2 (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) - (@ c3 (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) - (@ c4 (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) - (@ c5 (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) - (@ c6 (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) - (@ c7 (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) - (@ c8 (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) - (@ c9 (clc (pos v1) cln) - (@ cs (CMapc 1 c1 - (CMapc 2 c2 - (CMapc 3 c3 - (CMapc 4 c4 - (CMapc 5 c5 - (CMapc 6 c6 - (CMapc 7 c7 - (CMapc 8 c8 - (CMapc 9 c9 - CMapn))))))))) - (@ c (clc (pos v2) cln) - (@ t (Tracec 9 (Tracec 7 (Tracec 5 (Tracec 3 Tracen)))) - (@ h RATHintsn - (test_is_rat_trace - cs - c - t - h - UPR_Bottom - ) - )))) - ))))))))) - )))) -) - -; Test passes if the (test_is_rat_trace ...) application is well-typed. -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (@ c1 (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) - (@ c2 (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) - (@ c3 (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) - (@ c4 (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) - (@ c5 (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) - (@ c6 (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) - (@ c7 (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) - (@ c8 (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) - (@ c9 (clc (pos v1) cln) - (@ c10 (clc (pos v2) cln) - (@ cs (CMapc 1 c1 - (CMapc 2 c2 - (CMapc 3 c3 - (CMapc 4 c4 - (CMapc 5 c5 - (CMapc 6 c6 - (CMapc 7 c7 - (CMapc 8 c8 - (CMapc 9 c9 - (CMapc 10 c10 - CMapn)))))))))) - (@ c cln - (@ t (Tracec 9 (Tracec 10 (Tracec 2 (Tracec 4 (Tracec 5 Tracen))))) - (@ h RATHintsn - (test_is_rat_trace - cs - c - t - h - UPR_Bottom - ) - )))) - )))))))))) - )))) -) - -(declare test_is_lrat_proof_of_bottom - (! f CMap - (! p LRATProof - (! r bool - (! sc (^ (is_lrat_proof_of_bottom f p) r) type))))) - -; Test passes if the (test_is_lrat_proof_of_bottom ...) application is well-typed. -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (@ c1 (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) - (@ c2 (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) - (@ c3 (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) - (@ c4 (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) - (@ c5 (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) - (@ c6 (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) - (@ c7 (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) - (@ c8 (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) - (@ cs (CMapc 1 c1 - (CMapc 2 c2 - (CMapc 3 c3 - (CMapc 4 c4 - (CMapc 5 c5 - (CMapc 6 c6 - (CMapc 7 c7 - (CMapc 8 c8 - CMapn)))))))) - (@ p - (LRATProofa 9 - (clc (pos v1) cln) - Tracen - (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen)) - (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen)) - (RATHintsc 7 (Tracec 6 (Tracec 1 Tracen)) - RATHintsn))) - (LRATProofd (CIListc 1 (CIListc 6 (CIListc 8 CIListn))) - (LRATProofa 10 - (clc (pos v2) cln) - (Tracec 9 (Tracec 7 (Tracec 5 (Tracec 3 Tracen)))) - RATHintsn - (LRATProofd (CIListc 3 (CIListc 7 CIListn)) - (LRATProofa 11 - cln - (Tracec 9 (Tracec 10 (Tracec 2 (Tracec 4 (Tracec 5 Tracen))))) - RATHintsn - LRATProofn))))) - (test_is_lrat_proof_of_bottom - cs - p - tt - ) - )) - )))))))) - )))) -) - -; Test passes if the (test_is_lrat_proof_of_bottom ...) application is well-typed. -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (@ c1 (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) - (@ c2 (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) - (@ c3 (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) - (@ c4 (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) - (@ c5 (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) - (@ c6 (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) - (@ c7 (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) - (@ c8 (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) - (@ cs (CMapc 1 c1 - (CMapc 2 c2 - (CMapc 3 c3 - (CMapc 4 c4 - (CMapc 5 c5 - (CMapc 6 c6 - (CMapc 7 c7 - (CMapc 8 c8 - CMapn)))))))) - (@ p - (LRATProofa 9 - (clc (pos v1) cln) - Tracen - (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen)) - (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen)) - (RATHintsc 7 (Tracec 6 (Tracec 1 Tracen)) - RATHintsn))) - (LRATProofd (CIListc 1 (CIListc 6 (CIListc 8 CIListn))) - (LRATProofa 10 - (clc (pos v2) cln) - (Tracec 9 (Tracec 7 (Tracec 5 (Tracec 3 Tracen)))) - RATHintsn - (LRATProofd (CIListc 3 (CIListc 7 CIListn)) - (LRATProofa 11 - cln - (Tracec 9 (Tracec 10 (Tracec 2 (Tracec 4 Tracen)))) - RATHintsn - LRATProofn))))) - (test_is_lrat_proof_of_bottom - cs - p - ff - ) - )) - )))))))) - )))) -) - -; Proof from Figure 2 of "Efficient Certified RAT Verification" -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (% pf_c1 (holds (clc (pos v1) (clc (pos v2) (clc (neg v3) cln)))) - (% pf_c2 (holds (clc (neg v1) (clc (neg v2) (clc (pos v3) cln)))) - (% pf_c3 (holds (clc (pos v2) (clc (pos v3) (clc (neg v4) cln)))) - (% pf_c4 (holds (clc (neg v2) (clc (neg v3) (clc (pos v4) cln)))) - (% pf_c5 (holds (clc (neg v1) (clc (neg v3) (clc (neg v4) cln)))) - (% pf_c6 (holds (clc (pos v1) (clc (pos v3) (clc (pos v4) cln)))) - (% pf_c7 (holds (clc (neg v1) (clc (pos v2) (clc (pos v4) cln)))) - (% pf_c8 (holds (clc (pos v1) (clc (neg v2) (clc (neg v4) cln)))) - (@ pf_cmap - (CMapc_proof 1 _ _ _ pf_c1 - (CMapc_proof 2 _ _ _ pf_c2 - (CMapc_proof 3 _ _ _ pf_c3 - (CMapc_proof 4 _ _ _ pf_c4 - (CMapc_proof 5 _ _ _ pf_c5 - (CMapc_proof 6 _ _ _ pf_c6 - (CMapc_proof 7 _ _ _ pf_c7 - (CMapc_proof 8 _ _ _ pf_c8 - CMapn_proof)))))))) - (@ lrat_proof_witness - (LRATProofa 9 - (clc (pos v1) cln) - Tracen - (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen)) - (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen)) - (RATHintsc 7 (Tracec 6 (Tracec 1 Tracen)) - RATHintsn))) - (LRATProofd (CIListc 1 (CIListc 6 (CIListc 8 CIListn))) - (LRATProofa 10 - (clc (pos v2) cln) - (Tracec 9 (Tracec 7 (Tracec 5 (Tracec 3 Tracen)))) - RATHintsn - (LRATProofd (CIListc 3 (CIListc 7 CIListn)) - (LRATProofa 11 - cln - (Tracec 9 (Tracec 10 (Tracec 2 (Tracec 4 (Tracec 5 Tracen))))) - RATHintsn - LRATProofn))))) - (: - (holds cln) - (lrat_proof_of_bottom _ pf_cmap lrat_proof_witness)) - )) - )))))))) - )))) -) - -; Proof from Figure 2 of "Efficient Certified RAT Verification" -; With duplicates -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (% pf_c1 (holds (clc (pos v1) (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))))) - (% pf_c2 (holds (clc (neg v1) (clc (neg v2) (clc (pos v3) cln)))) - (% pf_c3 (holds (clc (pos v2) (clc (pos v3) (clc (pos v3) (clc (pos v3) (clc (neg v4) cln)))))) - (% pf_c4 (holds (clc (neg v2) (clc (neg v3) (clc (pos v4) cln)))) - (% pf_c5 (holds (clc (neg v1) (clc (neg v3) (clc (neg v4) (clc (neg v4) cln))))) - (% pf_c6 (holds (clc (pos v1) (clc (pos v3) (clc (pos v3) (clc (pos v4) cln))))) - (% pf_c7 (holds (clc (neg v1) (clc (pos v2) (clc (pos v4) cln)))) - (% pf_c8 (holds (clc (pos v1) (clc (neg v2) (clc (neg v2) (clc (neg v4) cln))))) - (@ pf_cmap - (CMapc_proof 1 _ _ _ pf_c1 - (CMapc_proof 2 _ _ _ pf_c2 - (CMapc_proof 3 _ _ _ pf_c3 - (CMapc_proof 4 _ _ _ pf_c4 - (CMapc_proof 5 _ _ _ pf_c5 - (CMapc_proof 6 _ _ _ pf_c6 - (CMapc_proof 7 _ _ _ pf_c7 - (CMapc_proof 8 _ _ _ pf_c8 - CMapn_proof)))))))) - (@ lrat_proof_witness - (LRATProofa 9 - (clc (pos v1) cln) - Tracen - (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen)) - (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen)) - (RATHintsc 7 (Tracec 6 (Tracec 1 Tracen)) - RATHintsn))) - (LRATProofd (CIListc 1 (CIListc 6 (CIListc 8 CIListn))) - (LRATProofa 10 - (clc (pos v2) cln) - (Tracec 9 (Tracec 7 (Tracec 5 (Tracec 3 Tracen)))) - RATHintsn - (LRATProofd (CIListc 3 (CIListc 7 CIListn)) - (LRATProofa 11 - cln - (Tracec 9 (Tracec 10 (Tracec 2 (Tracec 4 (Tracec 5 Tracen))))) - RATHintsn - LRATProofn))))) - (: - (holds cln) - (lrat_proof_of_bottom _ pf_cmap lrat_proof_witness)) - )) - )))))))) - )))) -) - -; Clauses 1 and 9 are identical. -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (% pf_c1 (holds (clc (pos v1) (clc (pos v2) (clc (neg v3) cln)))) - (% pf_c2 (holds (clc (neg v1) (clc (neg v2) (clc (pos v3) cln)))) - (% pf_c3 (holds (clc (pos v2) (clc (pos v3) (clc (neg v4) cln)))) - (% pf_c4 (holds (clc (neg v2) (clc (neg v3) (clc (pos v4) cln)))) - (% pf_c5 (holds (clc (neg v1) (clc (neg v3) (clc (neg v4) cln)))) - (% pf_c6 (holds (clc (pos v1) (clc (pos v3) (clc (pos v4) cln)))) - (% pf_c7 (holds (clc (neg v1) (clc (pos v2) (clc (pos v4) cln)))) - (% pf_c8 (holds (clc (pos v1) (clc (neg v2) (clc (neg v4) cln)))) - (% pf_c9 (holds (clc (pos v1) (clc (pos v2) (clc (neg v3) cln)))) - (@ pf_cmap - (CMapc_proof 1 _ _ _ pf_c1 - (CMapc_proof 2 _ _ _ pf_c2 - (CMapc_proof 3 _ _ _ pf_c3 - (CMapc_proof 4 _ _ _ pf_c4 - (CMapc_proof 5 _ _ _ pf_c5 - (CMapc_proof 6 _ _ _ pf_c6 - (CMapc_proof 7 _ _ _ pf_c7 - (CMapc_proof 8 _ _ _ pf_c8 - (CMapc_proof 9 _ _ _ pf_c9 - CMapn_proof))))))))) - (@ lrat_proof_witness - (LRATProofa 10 - (clc (pos v1) cln) - Tracen - (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen)) - (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen)) - (RATHintsc 7 (Tracec 6 (Tracec 9 Tracen)) - RATHintsn))) - (LRATProofd (CIListc 1 (CIListc 6 (CIListc 8 (CIListc 9 CIListn)))) - (LRATProofa 11 - (clc (pos v2) cln) - (Tracec 10 (Tracec 7 (Tracec 5 (Tracec 3 Tracen)))) - RATHintsn - (LRATProofd (CIListc 3 (CIListc 7 CIListn)) - (LRATProofa 12 - cln - (Tracec 10 (Tracec 11 (Tracec 2 (Tracec 4 (Tracec 5 Tracen))))) - RATHintsn - LRATProofn))))) - (: - (holds cln) - (lrat_proof_of_bottom _ pf_cmap lrat_proof_witness)) - )) - ))))))))) - )))) -) - -; Clauses 1 and 9 are logically identical, but the literals have been reordered. -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (% pf_c1 (holds (clc (pos v1) (clc (pos v2) (clc (neg v3) cln)))) - (% pf_c2 (holds (clc (neg v1) (clc (neg v2) (clc (pos v3) cln)))) - (% pf_c3 (holds (clc (pos v2) (clc (pos v3) (clc (neg v4) cln)))) - (% pf_c4 (holds (clc (neg v2) (clc (neg v3) (clc (pos v4) cln)))) - (% pf_c5 (holds (clc (neg v1) (clc (neg v3) (clc (neg v4) cln)))) - (% pf_c6 (holds (clc (pos v1) (clc (pos v3) (clc (pos v4) cln)))) - (% pf_c7 (holds (clc (neg v1) (clc (pos v2) (clc (pos v4) cln)))) - (% pf_c8 (holds (clc (pos v1) (clc (neg v2) (clc (neg v4) cln)))) - (% pf_c9 (holds (clc (neg v3) (clc (pos v2) (clc (pos v1) cln)))) - (@ pf_cmap - (CMapc_proof 1 _ _ _ pf_c1 - (CMapc_proof 2 _ _ _ pf_c2 - (CMapc_proof 3 _ _ _ pf_c3 - (CMapc_proof 4 _ _ _ pf_c4 - (CMapc_proof 5 _ _ _ pf_c5 - (CMapc_proof 6 _ _ _ pf_c6 - (CMapc_proof 7 _ _ _ pf_c7 - (CMapc_proof 8 _ _ _ pf_c8 - (CMapc_proof 9 _ _ _ pf_c9 - CMapn_proof))))))))) - (@ lrat_proof_witness - (LRATProofa 10 - (clc (pos v1) cln) - Tracen - (RATHintsc 2 (Tracec 6 (Tracec 8 Tracen)) - (RATHintsc 5 (Tracec 1 (Tracec 8 Tracen)) - (RATHintsc 7 (Tracec 6 (Tracec 9 Tracen)) - RATHintsn))) - (LRATProofd (CIListc 1 (CIListc 6 (CIListc 8 (CIListc 9 CIListn)))) - (LRATProofa 11 - (clc (pos v2) cln) - (Tracec 10 (Tracec 7 (Tracec 5 (Tracec 3 Tracen)))) - RATHintsn - (LRATProofd (CIListc 3 (CIListc 7 CIListn)) - (LRATProofa 12 - cln - (Tracec 10 (Tracec 11 (Tracec 2 (Tracec 4 (Tracec 5 Tracen))))) - RATHintsn - LRATProofn))))) - (: - (holds cln) - (lrat_proof_of_bottom _ pf_cmap lrat_proof_witness)) - )) - ))))))))) - )))) -) - -; Proof from Figure 1 of "Efficient Certified RAT Verification" -(check - (% v1 var - (% v2 var - (% v3 var - (% v4 var - (% pf_c1 (holds (clc (pos v1) (clc (pos v2) (clc (neg v3) cln)))) - (% pf_c2 (holds (clc (neg v1) (clc (neg v2) (clc (pos v3) cln)))) - (% pf_c3 (holds (clc (pos v2) (clc (pos v3) (clc (neg v4) cln)))) - (% pf_c4 (holds (clc (neg v2) (clc (neg v3) (clc (pos v4) cln)))) - (% pf_c5 (holds (clc (neg v1) (clc (neg v3) (clc (neg v4) cln)))) - (% pf_c6 (holds (clc (pos v1) (clc (pos v3) (clc (pos v4) cln)))) - (% pf_c7 (holds (clc (neg v1) (clc (pos v2) (clc (pos v4) cln)))) - (% pf_c8 (holds (clc (pos v1) (clc (neg v2) (clc (neg v4) cln)))) - (@ pf_cmap - (CMapc_proof 1 _ _ _ pf_c1 - (CMapc_proof 2 _ _ _ pf_c2 - (CMapc_proof 3 _ _ _ pf_c3 - (CMapc_proof 4 _ _ _ pf_c4 - (CMapc_proof 5 _ _ _ pf_c5 - (CMapc_proof 6 _ _ _ pf_c6 - (CMapc_proof 7 _ _ _ pf_c7 - (CMapc_proof 8 _ _ _ pf_c8 - CMapn_proof)))))))) - (@ lrat_proof_witness - (LRATProofa 9 - (clc (pos v1) (clc (pos v2) cln)) - (Tracec 1 (Tracec 6 (Tracec 3 Tracen))) - RATHintsn - (LRATProofd (CIListc 1 CIListn) - (LRATProofa 10 - (clc (pos v1) (clc (pos v3) cln)) - (Tracec 9 (Tracec 8 (Tracec 6 Tracen))) - RATHintsn - (LRATProofd (CIListc 6 CIListn) - (LRATProofa 11 - (clc (pos v1) cln) - (Tracec 10 (Tracec 9 (Tracec 4 (Tracec 8 Tracen)))) - RATHintsn - (LRATProofd (CIListc 8 (CIListc 9 (CIListc 10 CIListn))) - (LRATProofa 12 - (clc (pos v2) cln) - (Tracec 11 (Tracec 7 (Tracec 5 (Tracec 3 Tracen)))) - RATHintsn - (LRATProofd (CIListc 3 (CIListc 7 CIListn)) - (LRATProofa 13 - cln - (Tracec 11 (Tracec 12 (Tracec 2 (Tracec 4 (Tracec 5 Tracen))))) - RATHintsn - LRATProofn - ))))))))) - (: - (holds cln) - (lrat_proof_of_bottom _ pf_cmap lrat_proof_witness)) - )) - )))))))) - )))) -) diff --git a/test/signatures/run_test.py b/test/signatures/run_test.py deleted file mode 100644 index 4cfefe05f..000000000 --- a/test/signatures/run_test.py +++ /dev/null @@ -1,132 +0,0 @@ -#!/usr/bin/env python -##################### -## run_test.py -## Top contributors (to current version): -## Andres Noetzli, Alex Ozdemir -## This file is part of the CVC4 project. -## Copyright (c) 2009-2021 by the authors listed in the file AUTHORS -## in the top-level source directory and their institutional affiliations. -## All rights reserved. See the file COPYING in the top-level source -## directory for licensing information. -## - -import argparse -import re -import os.path -import sys -import subprocess - - -class TestConfiguration(object): - """Represents a test to run.""" - def __init__(self): - """Initialized from program arguments. - Exists with code 2 and prints usage message on invalid arguments.""" - parser = argparse.ArgumentParser( - description='Runs `lfscc on a test file.') - parser.add_argument('lfscc_binary') - parser.add_argument('input') - parser.add_argument('include_dirs', nargs='*') - args = parser.parse_args() - - self.lfscc = args.lfscc_binary - self.dep_graph = DepGraph(args.input, args.include_dirs) - - -class DepGraph(object): - """Represents a dependency graph of LFSC input files""" - def __init__(self, root_path, include_dirs): - """Creates a dependency graph rooted a `root_path`. - Computes a root-last topological sort. - Exits with exitcode 1 on cyclic dependencies""" - - # Root of the graph - self._r = root_path - - # Nodes (paths) that have been visited - self._visited = set() - - # Nodes (paths) that have been ordered - self._ordered_set = set() - - # The order of nodes (paths). Root is last. - self._ordered_paths = [] - - self.include_dirs = include_dirs - - # Start DFS topo-order - self._visit(root_path) - - def _visit(self, p): - """Puts the descendents of p in the order, parent-last""" - node = TestFile(p, self.include_dirs) - self._visited.add(p) - for n in node.dep_paths: - if n not in self._ordered_set: - if n in self._visited: - # Our child is is an ancestor our ours!? - print("{} and {} are in a dependency cycle".format(p, n)) - sys.exit(1) - else: - self._visit(n) - self._ordered_paths.append(p) - self._ordered_set.add(p) - - def getPathsInOrder(self): - return self._ordered_paths - - -class TestFile(object): - """Represents a testable input file to LFSC""" - def __init__(self, path, include_dirs): - """Read the file at `path` and determine its immediate dependencies""" - self.path = path - self._get_config_map() - self.deps = self.config_map['deps'].split() if ( - 'deps' in self.config_map) else [] - self.dir = os.path.dirname(self.path) - self.dep_paths = [] - include_paths = include_dirs + [self.dir] - for dep in self.deps: - found_dep = False - for include_path in include_paths: - dep_path = os.path.join(include_path, dep) - if os.path.isfile(dep_path): - self.dep_paths.append(dep_path) - found_dep = True - break - assert found_dep - - def _get_comment_lines(self): - """Return an iterator over comment lines, ;'s included""" - with open(self.path, 'r') as test_file: - return (line for line in test_file.readlines() if \ - re.match(r'^\s*;.*$', line) is not None) - - def _get_config_map(self): - """Populate self.config_map. - Config variables are set using the syntax - ; Var Name Spaces Okay: space separated values""" - m = {} - for l in self._get_comment_lines(): - match = re.match(r'^.*;\s*(\w+(?:\s+\w+)*)\s*:(.*)$', l) - if match is not None: - m[match.group(1).replace(' ', '').lower()] = match.group(2) - self.config_map = m - - -def main(): - configuration = TestConfiguration() - cmd = [configuration.lfscc] + configuration.dep_graph.getPathsInOrder() - result = subprocess.Popen(cmd, - stderr=subprocess.STDOUT, - stdout=subprocess.PIPE) - (stdout, _) = result.communicate() - if 0 != result.returncode: - if stdout: - print(stdout.decode()) - return result.returncode - - -if __name__ == '__main__': - sys.exit(main()) diff --git a/test/signatures/th_lira_test.plf b/test/signatures/th_lira_test.plf deleted file mode 100644 index d1fbe59f4..000000000 --- a/test/signatures/th_lira_test.plf +++ /dev/null @@ -1,294 +0,0 @@ -; Deps: th_lira.plf -;; Proof (from predicates on linear polynomials) that the following imply bottom -; -; -x - 1/2 y + 2 >= 0 -; x + y - 8 >= 0 -; x - y + 0 >= 0 -; -(check - ; Variables - (% x real_var - (% y real_var - ; linear combinations - (@ m1 (lc_cons (~ 1/1) (av_from_real x) (lc_cons (~ 1/2) (av_from_real y) lc_null)) - (@ m2 (lc_cons 1/1 (av_from_real x) (lc_cons 1/1 (av_from_real y) lc_null)) - (@ m3 (lc_cons 1/1 (av_from_real x) (lc_cons (~ 1/1) (av_from_real y) lc_null)) - ; affine functions - (@ p1 (aff_cons 2/1 m1) - (@ p2 (aff_cons (~ 8/1) m2) - (@ p3 (aff_cons 0/1 m3) - ; Proofs of affine bounds - (% pf_nonneg_1 (th_holds (bounded_aff p1 bound_non_neg)) - (% pf_nonneg_2 (th_holds (bounded_aff p2 bound_non_neg)) - (% pf_nonneg_3 (th_holds (bounded_aff p3 bound_non_neg)) - (: - (th_holds false) - (bounded_aff_contra _ _ - (bounded_aff_add _ _ _ _ _ - (bounded_aff_mul_c _ _ _ 4/1 pf_nonneg_1) - (bounded_aff_add _ _ _ _ _ - (bounded_aff_mul_c _ _ _ 3/1 pf_nonneg_2) - (bounded_aff_add _ _ _ _ _ - (bounded_aff_mul_c _ _ _ 1/1 pf_nonneg_3) - bounded_aff_ax_0_>=_0))))) - ))))) - )))) - )) -) - -;; Proof (from predicates on real terms) that the following imply bottom -; -; -x - 1/2 y >= 2 -; x + y >= 8 -; x - y >= 0 -; -(check - ; Declarations - ; Variables - (% x real_var - (% y real_var - ; real predicates - (@ f1 (>=_Real (+_Real (*_Real (a_real (~ 1/1)) (term_real_var x)) (*_Real (a_real (~ 1/2)) (term_real_var y))) (a_real (~ 2/1))) - (@ f2 (>=_Real (+_Real (*_Real (a_real 1/1) (term_real_var x)) (*_Real (a_real 1/1) (term_real_var y))) (a_real 8/1)) - (@ f3 (>=_Real (+_Real (*_Real (a_real 1/1) (term_real_var x)) (*_Real (a_real (~ 1/1)) (term_real_var y))) (a_real 0/1)) - ; proof of real predicates - (% pf_f1 (th_holds f1) - (% pf_f2 (th_holds f2) - (% pf_f3 (th_holds f3) - - - ; Normalization - ; real term -> linear polynomial normalization witnesses - (@ n1 (aff_>=_from_term _ _ _ - (is_aff_- _ _ _ _ _ - (is_aff_+ _ _ _ _ _ - (is_aff_mul_c_L _ _ _ (~ 1/1) (is_aff_var_real x)) - (is_aff_mul_c_L _ _ _ (~ 1/2) (is_aff_var_real y))) - (is_aff_const (~ 2/1))) - pf_f1) - (@ n2 (aff_>=_from_term _ _ _ - (is_aff_- _ _ _ _ _ - (is_aff_+ _ _ _ _ _ - (is_aff_mul_c_L _ _ _ 1/1 (is_aff_var_real x)) - (is_aff_mul_c_L _ _ _ 1/1 (is_aff_var_real y))) - (is_aff_const 8/1)) - pf_f2) - (@ n3 (aff_>=_from_term _ _ _ - (is_aff_- _ _ _ _ _ - (is_aff_+ _ _ _ _ _ - (is_aff_mul_c_L _ _ _ 1/1 (is_aff_var_real x)) - (is_aff_mul_c_L _ _ _ (~ 1/1) (is_aff_var_real y))) - (is_aff_const 0/1)) - pf_f3) - - ; derivation of a contradiction using farkas coefficients - (: - (th_holds false) - (bounded_aff_contra _ _ - (bounded_aff_add _ _ _ _ _ - (bounded_aff_mul_c _ _ _ 4/1 n1) - (bounded_aff_add _ _ _ _ _ - (bounded_aff_mul_c _ _ _ 3/1 n2) - (bounded_aff_add _ _ _ _ _ - (bounded_aff_mul_c _ _ _ 1/1 n3) - bounded_aff_ax_0_>=_0))))) - ))) - ))) - ))) - )) -) - -;; Term proof, 2 premises of the form (>=), one of the form (not >=) -;; Proof (from predicates on real terms) that the following imply bottom -; -; -x + y >= 2 -; x + y >= 2 -; not[ y >= -2] => [y < -2] => [-y > 2] -; -(check - ; Declarations - ; Variables - (% x real_var - (% y real_var - ; real predicates - (@ f1 (>=_Real - (+_Real (*_Real (a_real (~ 1/1)) (term_real_var x)) (term_real_var y)) - (a_real 2/1)) - (@ f2 (>=_Real - (+_Real (term_real_var x) (term_real_var y)) - (a_real 2/1)) - (@ f3 (not (>=_Real (term_real_var y) (a_real (~ 2/1)))) - - ; Normalization - ; proof of real predicates - (% pf_f1 (th_holds f1) - (% pf_f2 (th_holds f2) - (% pf_f3 (th_holds f3) - ; real term -> linear polynomial normalization witnesses - (@ n1 (aff_>=_from_term _ _ _ - (is_aff_- _ _ _ _ _ - (is_aff_+ _ _ _ _ _ - (is_aff_mul_c_L _ _ _ (~ 1/1) (is_aff_var_real x)) - (is_aff_var_real y)) - (is_aff_const 2/1)) - pf_f1) - (@ n2 (aff_>=_from_term _ _ _ - (is_aff_- _ _ _ _ _ - (is_aff_+ _ _ _ _ _ - (is_aff_var_real x) - (is_aff_var_real y)) - (is_aff_const 2/1)) - pf_f2) - (@ n3 (aff_>_from_term _ _ _ _ - (is_aff_- _ _ _ _ _ - (is_aff_var_real y) - (is_aff_const (~ 2/1))) - pf_f3) - - ; derivation of a contradiction using farkas coefficients - (: - (th_holds false) - (bounded_aff_contra _ _ - (bounded_aff_add _ _ _ _ _ - (bounded_aff_mul_c _ _ _ 1/1 n1) - (bounded_aff_add _ _ _ _ _ - (bounded_aff_mul_c _ _ _ 1/1 n2) - (bounded_aff_add _ _ _ _ _ - (bounded_aff_mul_c _ _ _ 2/1 n3) - bounded_aff_ax_0_>=_0))))) - ))) - ))) - ))) - )) -) - -;; Term proof, 2 premises of the form (>=), one of the form (not >=) -;; x is a real, -;; y is an integer -;; Proof (from predicates on real terms) that the following imply bottom -; -; -x + y >= 2 -; x + y >= 2 -; not[ y >= -2] => [y < -2] => [-y > 2] -; -(check - ; Declarations - ; Variables - (% x real_var - (% y int_var - ; real predicates - (@ f1 (>=_Real - (+_Real (*_Real (a_real (~ 1/1)) (term_real_var x)) (term_int_to_real (term_int_var y))) - (a_real 2/1)) - (@ f2 (>=_Real - (+_Real (term_real_var x) (term_int_to_real (term_int_var y))) - (a_real 2/1)) - (@ f3 (not (>=_IntReal (term_int_var y) (a_real (~ 2/1)))) - - ; Normalization - ; proof of real predicates - (% pf_f1 (th_holds f1) - (% pf_f2 (th_holds f2) - (% pf_f3 (th_holds f3) - ; real term -> linear polynomial normalization witnesses - (@ n1 (aff_>=_from_term _ _ _ - (is_aff_- _ _ _ _ _ - (is_aff_+ _ _ _ _ _ - (is_aff_mul_c_L _ _ _ (~ 1/1) (is_aff_var_real x)) - (is_aff_var_int y)) - (is_aff_const 2/1)) - (pf_reified_arith_pred _ _ pf_f1)) - (@ n2 (aff_>=_from_term _ _ _ - (is_aff_- _ _ _ _ _ - (is_aff_+ _ _ _ _ _ - (is_aff_var_real x) - (is_aff_var_int y)) - (is_aff_const 2/1)) - (pf_reified_arith_pred _ _ pf_f2)) - (@ n3 (aff_>_from_term _ _ _ _ - (is_aff_- _ _ _ _ _ - (is_aff_var_int y) - (is_aff_const (~ 2/1))) - (pf_reified_arith_pred _ _ pf_f3)) - - ; derivation of a contradiction using farkas coefficients - (: - (th_holds false) - (bounded_aff_contra _ _ - (bounded_aff_add _ _ _ _ _ - (bounded_aff_mul_c _ _ _ 1/1 n1) - (bounded_aff_add _ _ _ _ _ - (bounded_aff_mul_c _ _ _ 1/1 n2) - (bounded_aff_add _ _ _ _ _ - (bounded_aff_mul_c _ _ _ 2/1 n3) - bounded_aff_ax_0_>=_0))))) - ))) - ))) - ))) - )) -) - -;; Term proof, 2 premises of the form (>=), one of the form (not >=) -;; x is a real, -;; y is an integer, and needs tightening -;; Proof (from predicates on real terms) that the following imply bottom -; -; -x >= -1/2 -; x + y >= 0 -; not[ y >= 0] => [y < 0] => [-y >= 1] -; -(check - ; Declarations - ; Variables - (% x real_var - (% y int_var - ; real predicates - (@ f1 (>=_Real - (*_Real (a_real (~ 1/1)) (term_real_var x)) - (a_real (~ 1/2))) - (@ f2 (>=_Real - (+_Real (term_real_var x) (term_int_to_real (term_int_var y))) - (a_real 0/1)) - (@ f3 (not (>=_IntReal (*_Int (a_int 1) (term_int_var y)) (term_int_to_real (a_int 0)))) - - ; Normalization - ; proof of real predicates - (% pf_f1 (th_holds f1) - (% pf_f2 (th_holds f2) - (% pf_f3 (th_holds f3) - ; real term -> linear polynomial normalization witnesses - (@ n1 (aff_>=_from_term _ _ _ - (is_aff_- _ _ _ _ _ - (is_aff_mul_c_L _ _ _ (~ 1/1) (is_aff_var_real x)) - (is_aff_const (~ 1/2))) - (pf_reified_arith_pred _ _ pf_f1)) - (@ n2 (aff_>=_from_term _ _ _ - (is_aff_- _ _ _ _ _ - (is_aff_+ _ _ _ _ _ - (is_aff_var_real x) - (is_aff_var_int y)) - (is_aff_const 0/1)) - (pf_reified_arith_pred _ _ pf_f2)) - (@ n3 (aff_>=_from_term _ _ _ - (is_aff_- _ _ _ _ _ - (is_aff_mul_c_L _ _ _ (~ 1/1) (is_aff_var_int y)) - (is_aff_const 1/1)) - (pf_reified_arith_pred _ _ - (tighten_not_>=_IntInt _ _ _ _ (check_neg_of_greatest_integer_below_int 1 0) pf_f3))) - - ; derivation of a contradiction using farkas coefficients - (: - (th_holds false) - (bounded_aff_contra _ _ - (bounded_aff_add _ _ _ _ _ - (bounded_aff_mul_c _ _ _ 1/1 n1) - (bounded_aff_add _ _ _ _ _ - (bounded_aff_mul_c _ _ _ 1/1 n2) - (bounded_aff_add _ _ _ _ _ - (bounded_aff_mul_c _ _ _ 1/1 n3) - bounded_aff_ax_0_>=_0))))) - ))) - ))) - ))) - )) -)