Skip to content

Commit 8a879a9

Browse files
abdoo8080abdoo8080
committed
Use Pedro's cvc5 release.
1 parent be011cf commit 8a879a9

File tree

3 files changed

+185
-2
lines changed

3 files changed

+185
-2
lines changed

‎cvc5/Kind.lean‎

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2231,6 +2231,37 @@ inductive Kind where
22312231
-/
22322232
| FINITE_FIELD_MULT
22332233
/--
2234+
The Ideal generated by one or more finite field polynomials.
2235+
2236+
- Arity: ``n >= 1``
2237+
2238+
- ``1..n:`` Terms of finite field Sort (sorts must match)
2239+
\rst
2240+
.. note::
2241+
2242+
May be returned as the result of an API call, but terms of this kind
2243+
may not be created explicitly via the API and may not appear in
2244+
assertions.
2245+
\endrst
2246+
-/
2247+
| FINITE_FIELD_IDEAL
2248+
/--
2249+
The algebraic variety of a Finite Field Ideal generated by one or
2250+
more finite field polynomials.
2251+
2252+
- Arity: ``n = 1``
2253+
2254+
- ``1:`` Terms of set Sort (Finite Field Ideal has set sort)
2255+
\rst
2256+
.. note::
2257+
2258+
May be returned as the result of an API call, but terms of this kind
2259+
may not be created explicitly via the API and may not appear in
2260+
assertions.
2261+
\endrst
2262+
-/
2263+
| FINITE_FIELD_VARIETY
2264+
/--
22342265
Floating-point constant, created from IEEE-754 bit-vector representation
22352266
of the floating-point value.
22362267

‎cvc5/ProofRule.lean‎

Lines changed: 152 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2436,6 +2436,158 @@ inductive ProofRule where
24362436
| ARITH_TRANS_SINE_APPROX_BELOW_POS
24372437
/--
24382438
\verbatim embed:rst:leading-asterisk
2439+
**Finite Fields - Polynomial Conversion**
2440+
2441+
.. math::
2442+
2443+
\inferrule{- \mid \ell_1, \dots, \ell_n, G}
2444+
{(\ell_1 \land \dots \land l_n) \iff \mathcal V(\langle G \rangle) \neq \emptyset}
2445+
2446+
where each :math:`\ell_i` is a literal in the Finite Fields theory, :math:`G = (g_1, \dots, g_m)`
2447+
in which each :math:`g_i` is a polynomial that represents the literal :math:`\ell_i`.
2448+
\endverbatim
2449+
-/
2450+
| FF_POLY_CONVERSION
2451+
/--
2452+
\verbatim embed:rst:leading-asterisk
2453+
**Finite Fields -- Field Polynomial Inclusion**
2454+
2455+
.. math::
2456+
2457+
\inferrule{\mathcal V(\langle G \rangle) \mid F}
2458+
{\mathcal V(\langle G \cup F \rangle) \neq \emptyset}
2459+
2460+
where each :math:`G, F` are a set of polynomials. In particular, F contains only field polynomials,
2461+
\endverbatim
2462+
-/
2463+
| FF_FIELD_POLYS
2464+
/--
2465+
\verbatim embed:rst:leading-asterisk
2466+
**Finite Fields -- Ideal Membership: Zero**
2467+
2468+
.. math::
2469+
2470+
\inferrule{- \mid G}{0 \in \langle G \rangle}
2471+
2472+
2473+
where :math:`G` is a set of polynomials.
2474+
\endverbatim
2475+
-/
2476+
| FF_IDEAL_ZERO
2477+
/--
2478+
\verbatim embed:rst:leading-asterisk
2479+
**Finite Fields -- Ideal Membership: Generators**
2480+
2481+
.. math::
2482+
2483+
\inferrule{- \mid p, G}{p \in \langle G \rangle}
2484+
2485+
2486+
where :math:`G` is a set of polynomials and :math:`p \in G`
2487+
\endverbatim
2488+
-/
2489+
| FF_IDEAL_GENERATOR
2490+
/--
2491+
\verbatim embed:rst:leading-asterisk
2492+
**Finite Fields -- Ideal Membership: Result of reduction**
2493+
2494+
.. math::
2495+
2496+
\inferrule{p \in \langle G \rangle, r_1 \in \langle G \rangle, \dots, \langle r_k \in \langle G \rangle \mid \mathtt{Seq}_r, \mathtt{reduce}(p, R)}
2497+
{\mathtt{reduce}(p, R) \in \langle G \rangle}
2498+
2499+
where :math:`G` is a set of polynomials, :math:`R = \{r_1, \dots, r_k\}`
2500+
and :math:`\mathtt{Seq}_r` is the sequence of reductors in a :math:`\mathtt{reduce}` operation.
2501+
\endverbatim
2502+
-/
2503+
| FF_IDEAL_REDUCE
2504+
/--
2505+
\verbatim embed:rst:leading-asterisk
2506+
**Finite Fields -- Ideal Membership: Membership Test**
2507+
2508+
.. math::
2509+
2510+
\inferrule{0 \in \langle G \rangle, g_1 \in \langle G \rangle, \dots, \langle g_m \in \langle G \rangle \mid \mathtt{Seq}_r, p}
2511+
{p \in \langle G \rangle}
2512+
2513+
where :math:`G` is a set of polynomials, :math:`p` is the polynomial we are testing the membership
2514+
and :math:`\mathtt{Seq}_r` is the sequence of reductors such that :math:`\mathtt{reduce}(p, R) = 0`.
2515+
\endverbatim
2516+
-/
2517+
| FF_IDEAL_REDUCE_ZERO
2518+
/--
2519+
\verbatim embed:rst:leading-asterisk
2520+
**Finite Fields -- Ideal Membership: S-Polynomials**
2521+
2522+
.. math::
2523+
2524+
\inferrule{p \in \langle G \rangle, q \in \langle G \rangle \mid \mathtt{spoly}(p, q)}
2525+
{\mathtt{spoly}(p, q) \in \langle G \rangle }
2526+
2527+
where :math:`G` is a set of polynomials.
2528+
\endverbatim
2529+
-/
2530+
| FF_IDEAL_SPOLY
2531+
/--
2532+
\verbatim embed:rst:leading-asterisk
2533+
**Finite Fields -- Ideal Membership: Monic Polynomials**
2534+
2535+
.. math::
2536+
2537+
\inferrule{p \in \langle G \rangle \mid \mathtt{monic}(p, q)}
2538+
{\mathtt{monic}(p) \in \langle G \rangle }
2539+
2540+
where :math:`G` is a set of polynomials.
2541+
\endverbatim
2542+
-/
2543+
| FF_IDEAL_MONIC
2544+
/--
2545+
\verbatim embed:rst:leading-asterisk
2546+
**Finite Fields -- Branch on Roots of a univariate polynomial**
2547+
2548+
.. math::
2549+
2550+
\inferrule{\mathcal{V}(\langle G \rangle) \neq \emptyset, p \in \langle G \rangle, g_1 \in \langle G \rangle, \dots, g_m \in \langle G \rangle \mid N, \mathtt{Roots} (p)}
2551+
{\lor_{v \in \mathtt{Roots}(p)} \mathcal V(\langle G \cup \{x - v \}\rangle) \neq \emptyset}
2552+
2553+
where :math:`p` is an univariate polynomial, G is a set of polynomials and N is the
2554+
set of non-assigned variables. This rule unifies both Triangular
2555+
and Univariate present in the paper Ozdemir et al, CAV 2023, "Satisfiability
2556+
Modulo Finite Fields".
2557+
\endverbatim
2558+
-/
2559+
| FF_ROOT_BRANCH
2560+
/--
2561+
\verbatim embed:rst:leading-asterisk
2562+
**Finite Fields -- Exhaustive search through all elements of a finite field**
2563+
2564+
.. math::
2565+
2566+
\inferrule{\mathcal{V}(\langle G \rangle) \neq \emptyset, g_1 \in \langle G \rangle, \dots, g_m \in \langle G \rangle \mid N}
2567+
{\lor_{x \in N} \lor_{v \in F_p} \mathcal V(\langle G \cup \{x - v \}\rangle) \neq \emptyset}
2568+
2569+
where :math:`N` is the set of unassigned variables, :math:`F_p` is the fixed prime field
2570+
and G is a set of polynomials.
2571+
This rule is an analogue of FF_ROOT_BRANCH where instead of restricting our search in the
2572+
roots of a univariate polynomial, we have to look at all possible cases.
2573+
\endverbatim
2574+
-/
2575+
| FF_EXHAUST_BRANCH
2576+
/--
2577+
\verbatim embed:rst:leading-asterisk
2578+
**Finite Fields -- Refutation**
2579+
2580+
.. math::
2581+
2582+
\inferrule{1 \in \langle G \rangle \mid -}
2583+
{\mathcal V(\langle G \rangle) = \emptyset}
2584+
2585+
where :math:`G` is a set of polynomials.
2586+
\endverbatim
2587+
-/
2588+
| FF_ONE_UNSAT
2589+
/--
2590+
\verbatim embed:rst:leading-asterisk
24392591
**External -- LFSC**
24402592
24412593
Place holder for LFSC rules.

‎lakefile.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -18,9 +18,9 @@ def uncompress (file : FilePath) (dir : FilePath) : LogIO PUnit := do
1818
else
1919
unzip file dir
2020

21-
def cvc5.url := "https://github.com/abdoo8080/cvc5/releases/download"
21+
def cvc5.url := "https://github.com/psaccomani15/cvc5/releases/download"
2222

23-
def cvc5.version := "cvc5-1.3.2"
23+
def cvc5.version := "clean-wip"
2424

2525
def cvc5.os :=
2626
if Platform.isWindows then "Win64"

0 commit comments

Comments
 (0)