diff --git a/README.md b/README.md index a2d128f..2197aa7 100644 --- a/README.md +++ b/README.md @@ -7,10 +7,6 @@ cvc5 solver in Lean. It was designed to support the needs of the [lean-smt] tactic. The FFI allows Lean programs to interact with cvc5 by calling its functions and accessing its API. -## Limitations - -- Minimal interface to the cvc5 solver (contributions are welcome!) - ## Getting Started To use `lean-smt` in your project, add the following lines to your list of @@ -38,6 +34,24 @@ your system. If you are using Windows, you need to have `clang` and `libc++` (version 19) installed on your `MSYS2` environment. Build this library by running `lake build` in the root directory of the project. +## Missing features + +Term API: + +- [`getStringValue`](https://github.com/cvc5/cvc5/blob/cf59add20e053647145edb5f8151a2785c1d703e/include/cvc5/cvc5.h#L1600-L1607) + +Solver API: + +- [statistics](https://github.com/cvc5/cvc5/blob/cf59add20e053647145edb5f8151a2785c1d703e/include/cvc5/cvc5.h#L3410-L3425) +- [option info](https://github.com/cvc5/cvc5/blob/cf59add20e053647145edb5f8151a2785c1d703e/include/cvc5/cvc5.h#L3240-L3279) +- [driver options](https://github.com/cvc5/cvc5/blob/cf59add20e053647145edb5f8151a2785c1d703e/include/cvc5/cvc5.h#L3211-L3223) +- [plugins](https://github.com/cvc5/cvc5/blob/cf59add20e053647145edb5f8151a2785c1d703e/include/cvc5/cvc5.h#L3616-L3619) + +Input parser: + +- [`setStreamInput`](https://github.com/cvc5/cvc5/blob/cf59add20e053647145edb5f8151a2785c1d703e/include/cvc5/cvc5_parser.h#L251-L259) +- [dedicated parser errors](https://github.com/cvc5/cvc5/blob/cf59add20e053647145edb5f8151a2785c1d703e/include/cvc5/cvc5_parser.h#L348-L352) + ## Contributing Contributions to the Lean cvc5 FFI project are welcome! If you would like to contribute, please diff --git a/cvc5.lean b/cvc5.lean index d019d69..ed1d6c6 100644 --- a/cvc5.lean +++ b/cvc5.lean @@ -2643,9 +2643,30 @@ extern_def getVersion : (solver : Solver) → Env String -/ extern_def setOption : (solver : Solver) → (option value : String) → Env Unit +/-- Push (a) level(s) to the assertion stack. + +```smtlib +(push ) +``` + +- `nscopes`: The number of levels to push. +-/ +extern_def push : (solver : Solver) → (nscopes : UInt32 := 1) → Env Unit + /-- Remove all assertions. -/ extern_def resetAssertions : (solver : Solver) → Env Unit +/-- Set info. + +```smtlib +(set-info ) +``` + +- `keyword`: The info flag. +- `value`: The value of the info flag. +-/ +extern_def setInfo : (solver : Solver) → (keyword value : String) → Env Unit + /-- Set logic. - `logic`: The logic to set. @@ -2711,6 +2732,145 @@ extern_def checkSat : (solver : Solver) → Env Result -/ extern_def checkSatAssuming : (solver : Solver) → (assumptions : Array Term) → Env Result +/-- Declare uninterpreted sort. + +```smtlib +(declare-sort ) +``` + +- `symbol`: The name of the sort. +- `arity`: The arity of the sort. +- `fresh`: If true, then this function always returns a new sort. Otherwise, it will always return + the same sort for each call with the given arity and symbol where `fresh` is `false`. +-/ +extern_def declareSort : + (solver : Solver) → (symbol : String) → (arity : UInt32) → (fresh : Bool := true) + → Env cvc5.Sort + +/-- Define n-ary function. + +```smtlib +(define-fun ) +``` + +- `symbol`: The name of the function. +- `boundVars`: The parameters to this function. +- `sort`: The sort of the return value of this function. +- `body`: The function body. +- `global`: Determines whether this definition is global (*i.e.* persists when popping the context). +-/ +extern_def defineFun : (solver : Solver) + → (symbol : String) → (boundVars : Array Term) → (sort : cvc5.Sort) → (body : Term) + → (global : Bool := false) + → Env Term + +/-- Define recursive function. + +```smtlib +(define-fun-rec ) +``` + +- `symbol`: The name of the function. +- `boundVars`: The parameters to this function. +- `sort`: The sort of the return value of this function. +- `body`: The function body. +- `global`: Determines whether this definition is global (*i.e.* persists when popping the context). +-/ +extern_def defineFunRec : (solver : Solver) + → (symbol : String) → (boundVars : Array Term) → (sort : cvc5.Sort) → (body : Term) + → (global : Bool := false) + → Env Term + +/-- Define recursive function. + +```smtlib +(define-fun-rec ) +``` + +Create parameter `fn` with `TermManager.mkConst`. + +- `fn`: The sorted function. +- `bound_vars`: The parameters to this function. +- `term` The function body. +- `global` Determines whether this definition is global (*i.e.* persists when popping the context). +-/ +extern_def defineFunRecTerm : (solver : Solver) + → (fn : Term) → (boundVars : Array Term) → (body : Term) + → (global : Bool := false) + → Env Term + +/-- Define recursive functions. + +```smtlib +(define-funs-rec + ( _1 ... _n ) + ( _1 ... _n ) +) +``` + +- `funs`: The sorted functions, each created with `TermManager.mkConst`. +- `boundVars`: The list of parameters to the functions. +- `bodies`: The list of function bodies of the functions. +- `global`: Determines whether this definition is global (*i.e.* persists when popping the context). +-/ +extern_def defineFunsRec : (solver : Solver) + → (funs : Array Term) → (boundVars : Array (Array Term)) → (bodies : Array Term) + → (global : Bool := false) + → Env Unit + +/-- Get the list of asserted formulas. + +```smtlib +(get-assertions) +``` +-/ +extern_def getAssertions : (solver : Solver) → Env (Array Term) + +/-- Get info from the solver. + +```smtlib +(get-info ) +``` + +- `flag`: The info flag. +-/ +extern_def getInfo : (solver : Solver) → (flag : String) → Env String + +/-- Get the value of a given option. + +```smtlib +(get-option ) +``` + +- `option`: The option for which the value is queried. +-/ +extern_def getOption : (solver : Solver) → (option : String) → Env String + +/-- Get all option names that can be used with `setOption`, `getOption`, and `getOptionInfo`. -/ +extern_def getOptionNames : (solver : Solver) → Env (Array String) + +/-- Get the set of unsat (*failed*) assumptions. + +```smtlib +(get-unsat-assumptions) +``` + +Requires to enable option `produce-unsat-assumption`. +-/ +extern_def getUnsatAssumptions : (solver : Solver) → Env (Array Term) + +/-- Create datatype sort. + +```smtlib +(declare-datatype ) +``` + +- `symbol`: The name of the datatype sort. +- `ctors`: The constructor declarations of the datatype sort. +-/ +extern_def declareDatatype : + (solver : Solver) → (symbol : String) → (ctors : Array DatatypeConstructorDecl) → Env cvc5.Sort + /-- Get the unsatisfiable core. @@ -2733,11 +2893,77 @@ Returns a set of terms representing the unsatisfiable core. -/ extern_def getUnsatCore : (solver : Solver) → Env (Array Term) +/-- Get the lemmas used to derive unsatisfiability. + +```smtlib +(get-unsat-core-lemmas) +``` + +Requires the SAT proof unsat core mode, so to enable option `unsat-cores-mode=sat-proof`. + +**Warning**: this function is experimental and may change in future versions. +-/ +extern_def getUnsatCoreLemmas : (solver : Solver) → Env (Array Term) + +/-- Get a timeout core. + +This function computes a subset of the current assertions that couse a timeout. It may make multiple +checks for satisfiability internally, each limited by the timeout value given by +`timeout-core-timeout`. + +If the result is unknown and the reason is timeout, then returned the set of assertions corresponds +to a subset of the current assertions that cause a timeout in the specified time +`timeout-core-timeout`. If the result is unsat, then the list of formulas correspond to an unsat +core for the current assertions. Otherwise, the result is sat, indicating that the current +assertions are satisfiable, and the returned set of assertions is empty. + +```smtlib +(get-timeout-core) +``` + +**Warning**: this function is experimental and may change in future versions. +-/ +extern_def getTimeoutCore : (solver : Solver) → Env (Result × Array Term) + +/-- Get a timeout core of the given assumptions. + +This function computes a subset of the current assertions that couse a timeout when added to the +current assertions `timeout-core-timeout`. + +If the result is unknown and the reason is timeout, then returned the set of assertions corresponds +to a subset of the given assertions that cause a timeout when added to the current assertions in the +specified time `timeout-core-timeout`. If the result is unsat, then the set of assumptions together +with the current assertions correspond to an unsat core for the current assertions. Otherwise, the +result is sat, indicating that the given assumptions plus the current assertions are satisfiable, +and the returned set of assertions is empty. + +**NB:** this command does not require being preceeded by a call to `checkSat`. + +```smtlib +(get-timeout-core (*)) +``` + +**Warning**: this function is experimental and may change in future versions. +-/ +extern_def getTimeoutCoreAssuming : + (solver : Solver) → (assumptions : Array Term) → Env (Result × Array Term) + /-- Get a proof associated with the most recent call to `checkSat`. Requires to enable option `produce-proofs`. + +```smtlib +(get-proof :c) +``` + +**NB:** requires to enable option `produce-proofs`. + +**Warning**: this function is experimental and may change in future versions. + +- `c`: The component of the proof to return. -/ -extern_def getProof : (solver : Solver) → Env (Array Proof) +extern_def getProof : + (solver : Solver) → (c : ProofComponent := ProofComponent.FULL) → Env (Array Proof) /-- Get the values of the given term in the current model. @@ -2778,13 +3004,396 @@ The current model interprets the uninterpreted sort `s` as a finite sort whose d -/ extern_def getModelDomainElements (solver : Solver) (s : cvc5.Sort) : Env (Array Term) +/-- Determine if the model value of the given free constant was essential for showing +satisfiability of the last `checkSat` query based on the current model. + +For any free constant `v`, this will only return false if `model-cores` has been set to true. + +**Warning**: this function is experimental and may change in future versions. + +- `v`: The term in question. +-/ +extern_def isModelCoreSymbol : (solver : Solver) → (v: Term) → Env Bool + +/-- Get the model. + +```smtlib +(get-model) +``` + +Requires to enable option `produce-models`. + +**Warning**: this function is experimental and may change in future versions. + +- `sorts`: The list of uninterpreted sorts that should be printed in the model. +- `consts`: The list of free constants that should be printed in the model. A subset of these may be + printed based on `isModelCoreSymbol`. +-/ +extern_def getModel : + (solver : Solver) → (sorts : Array cvc5.Sort) → (consts : Array Term) → Env String + +/-- Do quantifier elimination. + +```smtlib +(get-qe ) +``` + +**NB:** Quantifier elimination is only complete for logics such as LRA, LIA, and BV. + +**Warning**: this function is experimental and may change in future versions. + +- `q`: A quantified formula of the form `QX_1 ... QX_n, P(x_1...x_i, y_1...y_j)` where `QX` is a set + of quantified variables of the form `Q x_1...x_k` and `P(x_1...x_i, y_1...y_j)` is a + quantifier-free formula. + +Returns a formula `Φ` such that, given the current set of formulas `A` asserted to this solver: +- `(a ∧ Q)` and (A ∧ Φ) are equivalent, and +- `Φ` is a quantifier-free formula containing only free variables in `y_1...y_n`. +-/ +extern_def getQuantifierElimination : (solver : Solver) → (q : Term) → Env Term + +/-- Do partial quantifier elimination, which can be used for incrementally computing the result of a + quantifier elimination. + +```smtlib +(get-qe-disjunct ) +``` + + +**NB:** Quantifier elimination is only complete for logics such as LRA, LIA, and BV. + +**Warning**: this function is experimental and may change in future versions. + +- `q`: A quantified formula of the form `QX_1 ... QX_n, P(x_1...x_i, y_1...y_j)` where `QX` is a set + of quantified variables of the form `Q x_1...x_k` and `P(x_1...x_i, y_1...y_j)` is a + quantifier-free formula. + +Returns a formula `Φ` such that, given the current set of formulas `A` asserted to this solver: +- `A ∧ q → A ∧ Φ` if `Q` is `∀`, and `A ∧ Φ → A ∧ q` if `Q` is `∃`; +- `Φ` is a quantifier-free formula containing only free variables in `y_1...y_n`; +- if `Q` is `∃`, let `A ∧ Q_n` be the formula `A ∧ ¬ (Φ ∧ Q_1) ∧ ... ∧ ¬ (Φ ∧ Q_n)` where for each + `i ∈ [1, n]`, formula `Φ ∧ Q_i` is the result of calling `getQuantifierEliminationDisjunct` for + `q` with the set of assertions `A ∧ Q_{i-1}`. + + Similarly, if `Q` is `∀`, then let `A ∧ Q_n` be `A ∧ (Φ ∧ Q_1) ∧ ... ∧ (Φ ∧ Q_n)` where `Φ ∧ Q_i` + is the same as above. + + In either case, we have that `Φ ∧ Q_j` will eventually be true or false, for some finite `j`. +-/ +extern_def getQuantifierEliminationDisjunct : (solver : Solver) → (q : Term) → Env Term + +/-- When using separation logic, sets the location sort and the datatype sort to the given ones. + +This function should be invoked exactly once, before any separation logic constraints are provided. + +**Warning**: this function is experimental and may change in future versions. + +- `locSort`: The location sort of the heap. +- `dataSort`: The data sort of the heap. +-/ +extern_def declareSepHeap : + (solver : Solver) → (locSort : cvc5.Sort) → (dataSort : cvc5.Sort) → Env Unit + +/-- When using separation logic, obtain the term for the heap. + +**Warning**: this function is experimental and may change in future versions. +-/ +extern_def getValueSepHeap : (solver : Solver) → Env Term + +/-- When using separation logic, obtain the term for nil. + +**Warning**: this function is experimental and may change in future versions. +-/ +extern_def getValueSepNil : (solver : Solver) → Env Term + +/-- Declare a symbolic pool of terms with the given initial value. + +For details on how pools are used to specify instructions for quantifier instantiation, see +`Kind.INST_POOL` + +```smtlib +(declare-pool ( * )) +``` + +**Warning**: this function is experimental and may change in future versions. + +- `symbol`: The name of the pool. +- `sort`: The sort of the elements of the pool. +- `initValue` The initial value of the pool. +-/ +extern_def declarePool : + (solver : Solver) → (symbol : String) → (sort : cvc5.Sort) → (initValue : Array Term) → Env Term + +/-- Declare an oracle function with reference to an implementation. + +Oracle functions have a different semantics with respect to ordinary declared functions. In +particular, for an input to be satisfiable, its oracle functions are implicitly universally +quantified. + +This function is used in part for implementing this command: + +```smtlib +(declare-oracle-fun ( * ) ) +``` + +In particular, the above command is implemented by constructing a function over terms that wraps a +call to binary sym via a text interface. + +**Warning**: this function is experimental and may change in future versions. + +- `symbol`: The name of the oracle. +- `sorts`: The sorts of the parameters to this function. +- `sort`: The sort of the return value of this function. +- `fn`: The function that implements the oracle function. + +# TODO + +Causes the tests to crash in a very weird way, see `cvc5Test/Unit/ApiSolverOracleFun.lean`. +-/ +extern_def declareOracleFun : + (solver : Solver) → (symbol : String) + → (sorts : Array cvc5.Sort) → (sort : cvc5.Sort) + → (fn : Array Term → Env Term) + → Env Term + +/-- Pop (a) level(s) from the assertion stack. + +```smtlib +(pop ) +``` + +- `nscopes`: The number of levels to pop. +-/ +extern_def pop : (solver : Solver) → (nscopes : UInt32 := 1) → Env Unit + +/-- Get an interpolant if one exists, the null term otherwise. + +Given that `A → B` is valid, this function determines a term `I` over the shared variables of `A` and `B`, such that `A → I` and `I → B` are valid. `A` is the current set of assertions and `B` is the conjecture, given as `conj`. + +```smtlib +(get-interpolant ) +``` + +**NB:** in SMT-LIB, `` assigns a symbol to the interpolant. + +**NB:** Requires option `produce-interpolants` to be set to a mode different from `none`. + +**Warning**: this function is experimental and may change in future versions. + +- `conj`: The conjecture term. +-/ +extern_def getInterpolantSimple : (solver : Solver) → (conj : Term) → Env Term + +/-- Get an interpolant if one exists, the null term otherwise. + +Given that `A → B` is valid, this function determines a term `I` over the shared variables of `A` +and `B`, such that `A → I` and `I → B` are valid. `I` is constructed from the given grammar. `A` is +the current set of assertions and `B` is the conjecture, given as `conj`. + +```smtlib +(get-interpolant ) +``` + +**NB:** in SMT-LIB, `` assigns a symbol to the interpolant. + +**NB:** Requires option `produce-interpolants` to be set to a mode different from `none`. + +**Warning**: this function is experimental and may change in future versions. + +- `conj`: The conjecture term. +- `grammar`: The grammar for the interpolant `I`. +-/ +extern_def getInterpolantOfGrammar : + (solver : Solver) → (conj : Term) → (grammar : Grammar) → Env Term + +/-- Get an interpolant if one exists, the null term otherwise. + +Given that `A → B` is valid, this function determines a term `I` over the shared variables of `A` +and `B`, such that `A → I` and `I → B` are valid. If a grammar `G` is provided, `I` is constructed +from `G`. `A` is the current set of assertions and `B` is the conjecture, given as `conj`. + +```smtlib +(get-interpolant ) +(get-interpolant ) +``` + +**NB:** in SMT-LIB, `` assigns a symbol to the interpolant. + +**NB:** Requires option `produce-interpolants` to be set to a mode different from `none`. + +**Warning**: this function is experimental and may change in future versions. + +- `conj`: The conjecture term. +- `grammar`: The optional grammar for the interpolant `I`. +-/ +def getInterpolant + (solver : Solver) (conj : Term) (grammar : Option Grammar := none) +: Env Term := + if let some grammar := grammar + then solver.getInterpolantOfGrammar conj grammar + else solver.getInterpolantSimple conj + +/-- Get the next interpolant if any, the null term otherwise. + +Can only be called immediately after a successful call to `getInterpolant`, +`getInterpolantOfGrammar`, `getInterpolant?`, `getInterpolantNext`, or `getInterpolantNext`. It is +guaranteed to produce a syntactically different interpolant *w.r.t.* the last returned interpolant +if successful. + +```smtlib +(get-interpolant-next) +``` + +Requires to enable incremental mode, and option `produce-interpolants` to be set to a mode different +from `none`. + +**Warning**: this function is experimental and may change in future versions. + +Returns a term `I` such that `A → I` and `I → B` and valid, where `A` is the current set of +assertions and `B` is given in the input by `conj`, or the null term if such a term cannot be found. +-/ +extern_def getInterpolantNext : (solver : Solver) → Env Term + +/-- Get an abduct if one exists, the null term otherwise. + +```smtlib +(get-abduct ) +``` + +**NB:** Requires to enable option `produce-abducts`. + +**Warning**: this function is experimental and may change in future versions. + +- `conj`: The conjecture term. + +Returns a term `C` such that `A ∧ C` is satisfiable, and `A ∧ ¬B ∧ C` is unsatisfiable, where `A` is +the current set of assertions and `B` is given in the input by `conj`, or the null term if such a +term cannot be found. +-/ +private extern_def getAbductSimple : (solver : Solver) → (conj : Term) → Env Term + +/-- Get an abduct if one exists, the null term otherwise. + +```smtlib +(get-abduct ) +``` + +**NB:** Requires to enable option `produce-abducts`. + +**Warning**: this function is experimental and may change in future versions. + +- `conj`: The conjecture term. +- `grammar`: The grammar for the abduct `C`. + +Returns a term `C` such that `A ∧ C` is satisfiable, and `A ∧ ¬B ∧ C` is unsatisfiable, where `A` is +the current set of assertions and `B` is given in the input by `conj`, or the null term if such a +term cannot be found. +-/ +extern_def getAbductOfGrammar : + (solver : Solver) → (conj : Term) → (grammar : Grammar) → Env Term + +/-- Get an abduct if one exists. + +```smtlib +(get-abduct ) +(get-abduct ) +``` + +**NB:** Requires to enable option `produce-abducts`. + +**Warning**: this function is experimental and may change in future versions. + +- `conj`: The conjecture term. +- `grammar`: The optional grammar for the abduct `C`. + +Returns a term `C` such that `A ∧ C` is satisfiable, and `A ∧ ¬B ∧ C` is unsatisfiable, where `A` is +the current set of assertions and `B` is given in the input by `conj`, or the null term if such a +term cannot be found. +-/ +def getAbduct + (solver : Solver) (conj : Term) (grammar : Option Grammar := none) +: Env Term := + if let some grammar := grammar + then solver.getAbductOfGrammar conj grammar + else solver.getAbductSimple conj + +/-- Get the next interpolant if any, the null term otherwise. + +Can only be called immediately after a successful call to `getAbduct`, `getAbductOfGrammar`, +`getAbduct?`, `getAbductNext`, or `getAbductNext?`. It is guaranteed to produce a syntactically +different abduct *w.r.t.* the last returned abduct if successful. + +```smtlib +(get-abduct-next) +``` + +Requires to enable incremental mode, and option `produce-abducts`. + +**Warning**: this function is experimental and may change in future versions. + +Returns a term `C` such that `A ∧ C` is satisfiable, and `A ∧ ¬B ∧ C` is unsatisfiable, where `A` is +the current set of assertions and `B` is given in the input by the last call to a `getAbduct`-like +function, or the null term if such a term cannot be found. +-/ +extern_def getAbductNext : (solver : Solver) → Env Term + +/-- Block the current model. Can be called only if immediately preceded by a SAT or INVALID query. + +```smtlib +(block-model) +``` + +**NB:** requires enabling option `produce-models`. + +**Warning**: this function is experimental and may change in future versions. + +- `mode`: The mode to use for blocking. +-/ +extern_def blockModel : (solver : Solver) → (mode : BlockModelsMode) → Env Unit + +/-- Block the current model values of (at least) the values in `terms`. + +Can be called only if immediately preceded by a SAT query. + +```smtlib +(block-model-values ( + )) +``` + +**NB:** requires enabling option `produce-models`. + +**Warning**: this function is experimental and may change in future versions. + +- `terms`: The model values to block. +-/ +extern_def blockModelValues : (solver : Solver) → (terms : Array Term) → Env Unit + +/-- Produce a string containing information about all instantiations made by the quantifier module. + +**Warning**: this function is experimental and may change in future versions. +-/ +extern_def getInstantiations : (solver : Solver) → Env String + /-- Prints a proof as a string in a selected proof format mode. Other aspects of printing are taken from the solver options. +**Warning**: this function is experimental and may change in future versions. + - `proof`: A proof, usually obtained from `getProof`. +- `format`: The proof format used to print the proof. Must be `ProofFormat.NONE` if the proof is + from a component other than `ProofComponent.FULL`. +-/ +extern_def proofToString : + (solver : Solver) → (proof : Proof) → (format : ProofFormat := ProofFormat.DEFAULT) → Env String + +/-- Get a list of learned literals that are entailed by the current set of assertions. + +**Warning**: this function is experimental and may change in future versions. + +- `t`: The type of learned literals to return. -/ -extern_def proofToString : (solver : Solver) → Proof → Env String +extern_def getLearnedLiterals : + (solver : Solver) → (t : LearnedLitType := LearnedLitType.INPUT) → Env (Array Term) /-- Create a Sygus grammar. diff --git a/cvc5Test/Unit/ApiSolver.lean b/cvc5Test/Unit/ApiSolver.lean index 44153d9..f63b9b3 100644 --- a/cvc5Test/Unit/ApiSolver.lean +++ b/cvc5Test/Unit/ApiSolver.lean @@ -14,7 +14,1498 @@ import cvc5Test.Init namespace cvc5.Test -/-! # Synthesis/sygus -/ +test![TestApiBlackSolver, pow2Large1] tm solver => do + -- Based on https://github.com/cvc5/cvc5-projects/issues/371 + let string ← tm.getStringSort + let s4 ← tm.mkArraySort string int + let s7 ← tm.mkArraySort int string + let t10 ← tm.mkIntegerOfString "68038927088685865242724985643" + let t74 ← tm.mkIntegerOfString "8416288636405" + let mut ctors := #[] + let mut dtConsDecl ← tm.mkDatatypeConstructorDecl "_x109" + dtConsDecl ← dtConsDecl.addSelector "_x108" s7 + ctors := ctors.push dtConsDecl + dtConsDecl ← tm.mkDatatypeConstructorDecl "_x113" + dtConsDecl ← dtConsDecl.addSelector "_x110" s4 + dtConsDecl ← dtConsDecl.addSelector "_x111" int + dtConsDecl ← dtConsDecl.addSelector "_x112" s7 + ctors := ctors.push dtConsDecl + let s11 ← solver.declareDatatype "_x107" ctors + let t82 ← tm.mkConst s11 "_x114" + let t180 ← tm.mkTerm Kind.POW2 #[t10] + let t258 ← tm.mkTerm Kind.GEQ #[t74, t180] + solver.assertFormula t258 + solver.simplify t82 true |> assertError + "The exponent of the POW(^) operator can only be a positive integral constant below 67108864. \ + Exception occurred in:\n \ + (int.pow2 68038927088685865242724985643)" + +test![TestApiBlackSolver, pow2Large2] tm solver => do + -- Based on https://github.com/cvc5/cvc5-projects/issues/333 + let t1 ← tm.mkBitVector 63 <| (1 : UInt64) <<< 62 + let t2 ← tm.mkTerm Kind.BITVECTOR_UBV_TO_INT #[t1] + let t3 ← tm.mkTerm Kind.POW2 #[t2] + let t4 ← tm.mkTerm Kind.DISTINCT #[t3, t2] + solver.checkSatAssuming #[t4] |> assertError + "The exponent of the POW(^) operator can only be a positive integral constant below 67108864. \ + Exception occurred in:\n \ + (int.pow2 4611686018427387904)" + +test![TestApiBlackSolver, pow2Large3] tm solver => do + -- Based on https://github.com/cvc5/cvc5-projects/issues/339 + let t203 ← tm.mkIntegerOfString "6135470354240554220207" + let t262 ← tm.mkTerm Kind.POW2 #[t203] + let t536 ← tm.mkTermOfOp (← tm.mkOp Kind.INT_TO_BITVECTOR #[49]) #[t262] + -- should not throw an exception, will not simplify + solver.simplify t536 |> assertOkDiscard + +test![TestApiBlackSolver, recoverableException] tm solver => do + solver.setOption "produce-models" "true" + let x ← tm.mkConst (← tm.getBooleanSort) "x" + solver.assertFormula (← (← x.eqTerm x).notTerm) + solver.getValue x |> assertError + "cannot get value unless after a SAT or UNKNOWN response." + +test![TestApiBlackSolver, simplify] tm solver => do + let bvSort ← tm.mkBitVectorSort 32 + let funSort1 ← tm.mkFunctionSort #[bvSort, bvSort] bvSort + let funSort2 ← tm.mkFunctionSort #[uninterpreted] int + let consListSort ← do + let mut consListSpec ← tm.mkDatatypeDecl "list" + let mut cons ← tm.mkDatatypeConstructorDecl "cons" + cons ← cons.addSelector "head" int + cons ← cons.addSelectorSelf "tail" + consListSpec ← consListSpec.addConstructor cons + let nil ← tm.mkDatatypeConstructorDecl "nil" + consListSpec ← consListSpec.addConstructor nil + tm.mkDatatypeSort consListSpec + + let x ← tm.mkConst bvSort "x" + solver.simplify x |> assertOkDiscard + let a ← tm.mkConst bvSort "a" + solver.simplify a |> assertOkDiscard + let b ← tm.mkConst bvSort "b" + solver.simplify b |> assertOkDiscard + let tru ← tm.mkTrue + let x_eq_x ← tm.mkTerm Kind.EQUAL #[x, x] + assertNe tru x_eq_x + assertEq tru (← solver.simplify x_eq_x) + let x_eq_b ← tm.mkTerm Kind.EQUAL #[x, b] + assertNe tru x_eq_b + assertNe tru (← solver.simplify x_eq_b) + + let i1 ← tm.mkConst int "i1" + solver.simplify i1 |> assertOkDiscard + let i2 ← tm.mkTerm Kind.MULT #[i1, ← tm.mkInteger 23] + solver.simplify i2 |> assertOkDiscard + assertNe i1 i2 + assertNe i1 (← solver.simplify i2) + let i3 ← tm.mkTerm Kind.ADD #[i1, ← tm.mkInteger 0] + solver.simplify i3 |> assertOkDiscard + assertNe i1 i3 + assertEq i1 (← solver.simplify i3) + + let consList ← consListSort.getDatatype + let cons ← consList.getConstructor "cons" + let nil ← consList.getConstructor "nil" + let dt1 ← tm.mkTerm Kind.APPLY_CONSTRUCTOR #[ + ← cons.getTerm, + ← tm.mkInteger 0, + ← tm.mkTerm Kind.APPLY_CONSTRUCTOR #[← nil.getTerm], + ] + solver.simplify dt1 |> assertOkDiscard + let dt2 ← tm.mkTerm Kind.APPLY_SELECTOR #[ + ← cons.getSelector "head" >>= DatatypeSelector.getTerm, + dt1 + ] + solver.simplify dt2 |> assertOkDiscard + + let b1 ← tm.mkVar bvSort "b1" + solver.simplify b1 |> assertOkDiscard + let b2 ← tm.mkVar bvSort "b1" + solver.simplify b2 |> assertOkDiscard + let b3 ← tm.mkVar uninterpreted "b3" + solver.simplify b3 |> assertOkDiscard + let v1 ← tm.mkVar bvSort "v1" + solver.simplify v1 |> assertOkDiscard + let v2 ← tm.mkVar int "v2" + solver.simplify v2 |> assertOkDiscard + let f1 ← tm.mkVar funSort1 "f1" + solver.simplify f1 |> assertOkDiscard + let f2 ← tm.mkVar funSort2 "f2" + solver.simplify f2 |> assertOkDiscard + solver.defineFunsRec #[f1, f2] #[#[b1, b2], #[b3]] #[v1, v2] + solver.simplify f1 |> assertOkDiscard + solver.simplify f2 |> assertOkDiscard + + let tm' ← TermManager.new + let solver' ← Solver.new tm' + solver'.simplify x |> assertError + "Given term is not associated with the term manager of this solver" + +test![TestApiBlackSolver, simplifyApplySubs] tm solver => do + solver.setOption "incremental" "true" + let x ← tm.mkConst int "x" + let zero ← tm.mkInteger 0 + let eq ← tm.mkTerm Kind.EQUAL #[x, zero] + solver.assertFormula eq + solver.checkSat |> assertOkDiscard + + assertEq x (← solver.simplify x false) + assertEq zero (← solver.simplify x true) + +test![TestApiBlackSolver, assertFormula] tm solver => do + solver.assertFormula (← tm.mkTrue) |> assertOkDiscard + solver.assertFormula (Term.null ()) |> assertError + "invalid null argument for 'term'" + let tm' ← TermManager.new + let solver' ← Solver.new tm' + solver'.assertFormula (← tm.mkTrue) |> assertError + "Given term is not associated with the term manager of this solver" + +test![TestApiBlackSolver, checkSatAssuming] tm solver => do + solver.setOption "incremental" "false" + solver.checkSatAssuming #[← tm.mkTrue] |> assertOkDiscard + solver.checkSatAssuming #[← tm.mkTrue] |> assertError + "cannot make multiple queries unless incremental solving is enabled (try --incremental)" + let tm' ← TermManager.new + let solver' ← Solver.new tm' + solver'.checkSatAssuming #[← tm.mkTrue] |> assertError + "invalid term in 'assumptions' at index 0, \ + expected a term associated with the term manager of this solver" + +test![TestApiBlackSolver, checkSatAssuming1] tm solver => do + let x ← tm.mkConst bool "x" + let y ← tm.mkConst bool "y" + let z ← tm.mkTerm Kind.AND #[x, y] + solver.setOption "incremental" "true" + solver.checkSatAssuming #[← tm.mkTrue] |> assertOkDiscard + solver.checkSatAssuming #[Term.null ()] |> assertError + "invalid null term in 'assumptions' at index 0" + solver.checkSatAssuming #[← tm.mkTrue] |> assertOkDiscard + solver.checkSatAssuming #[z] |> assertOkDiscard + +test![TestApiBlackSolver, checkSatAssuming2] tm solver => do + solver.setOption "incremental" "true" + + let uToIntSort ← tm.mkFunctionSort #[uninterpreted] int + let intPredSort ← tm.mkFunctionSort #[int] bool + + let n := Term.null () + -- constants + let x ← tm.mkConst uninterpreted "x" + let y ← tm.mkConst uninterpreted "y" + -- functions + let f ← tm.mkConst uToIntSort "f" + let p ← tm.mkConst intPredSort "p" + -- values + let zero ← tm.mkInteger 0 + let one ← tm.mkInteger 1 + -- terms + let f_x ← tm.mkTerm Kind.APPLY_UF #[f, x] + let f_y ← tm.mkTerm Kind.APPLY_UF #[f, y] + let sum ← tm.mkTerm Kind.ADD #[f_x, f_y] + let p_0 ← tm.mkTerm Kind.APPLY_UF #[p, zero] + let p_f_y ← tm.mkTerm Kind.APPLY_UF #[p, f_y] + -- assertions + let assertions ← tm.mkTerm Kind.AND #[ + ← tm.mkTerm Kind.LEQ #[zero, f_x], -- `0 ≤ f(x)` + ← tm.mkTerm Kind.LEQ #[zero, f_y], -- `0 ≤ f(y)` + ← tm.mkTerm Kind.LEQ #[sum, one], -- `f(x) + f(y) ≤ 1` + ← p_0.notTerm, -- `¬ p(0)` + p_f_y, -- `p(f(y))` + ] + + solver.checkSatAssuming #[← tm.mkTrue] |> assertOkDiscard + solver.assertFormula assertions + solver.checkSatAssuming #[← tm.mkTerm Kind.DISTINCT #[x, y]] |> assertOkDiscard + solver.checkSatAssuming #[← tm.mkFalse, ← tm.mkTerm Kind.DISTINCT #[x, y]] |> assertOkDiscard + solver.checkSatAssuming #[n] |> assertError + "invalid null term in 'assumptions' at index 0" + solver.checkSatAssuming #[n, ← tm.mkTerm Kind.DISTINCT #[x, y]] |> assertError + "invalid null term in 'assumptions' at index 0" + +test![TestApiBlackSolver, declareFunFresh] tm solver => do + let t1 ← solver.declareFun "b" #[] bool true + let t2 ← solver.declareFun "b" #[] bool false + let t3 ← solver.declareFun "b" #[] bool false + assertNe t1 t2 + assertNe t1 t3 + assertEq t2 t3 + let t4 ← solver.declareFun "c" #[] bool false + assertNe t2 t4 + let t5 ← solver.declareFun "b" #[] int false + assertNe t2 t5 + + let tm' ← TermManager.new + let solver' ← Solver.new tm' + solver'.declareFun "b" #[] int false |> assertError + "Given sort is not associated with the term manager of this solver" + +test![TestApiBlackSolver, declareDatatype] tm solver => do + let lin ← tm.mkDatatypeConstructorDecl "lin" + let ctors0 := #[lin] + solver.declareDatatype "" ctors0 |> assertOkDiscard + + let nil ← tm.mkDatatypeConstructorDecl "nil" + let ctors1 := #[nil] + solver.declareDatatype "a" ctors1 |> assertOkDiscard + + let cons ← tm.mkDatatypeConstructorDecl "cons" + let nil2 ← tm.mkDatatypeConstructorDecl "nil" + let ctors2 := #[cons, nil2] + solver.declareDatatype "b" ctors2 |> assertOkDiscard + + let cons2 ← tm.mkDatatypeConstructorDecl "cons" + let nil3 ← tm.mkDatatypeConstructorDecl "nil" + let ctors3 := #[cons2, nil3] + solver.declareDatatype "" ctors3 |> assertOkDiscard + + -- must have at least one constructor + let mut ctors4 := #[] + solver.declareDatatype "c" ctors4 |> assertError + "invalid argument '[]' for 'ctors', \ + expected a datatype declaration with at least one constructor" + -- constructor may not be reused + let ctor1 ← tm.mkDatatypeConstructorDecl "_x21" + let ctor2 ← tm.mkDatatypeConstructorDecl "_x31" + solver.declareDatatype "_x17" #[ctor1, ctor2] |> assertOkDiscard + solver.declareDatatype "_x86" #[ctor1, ctor2] |> assertError + "cannot use a constructor for multiple datatypes" + + let tm' ← TermManager.new + let solver' ← Solver.new tm' + let nnil ← tm.mkDatatypeConstructorDecl "nil" + solver'.declareDatatype "a" #[nnil] |> assertError + "invalid datatype constructor declaration in 'ctorsr' at index 0, \ + expected a datatype constructor declaration associated with \ + the term manager of this solver object" + +test![TestApiBlackSolver, declareFun] tm solver => do + let bvSort ← tm.mkBitVectorSort 32 + let funSort ← tm.mkFunctionSort #[uninterpreted] int + solver.declareFun "f1" #[] bvSort |> assertOkDiscard + solver.declareFun "f3" #[bvSort, int] bvSort |> assertOkDiscard + solver.declareFun "f2" #[] funSort |> assertError + "invalid argument '(-> u Int)' for 'sort', expected non-function sort as codomain sort" + -- functions as arguments is allowed + solver.declareFun "f4" #[bvSort, funSort] bvSort |> assertOkDiscard + solver.declareFun "f5" #[bvSort, bvSort] funSort |> assertError + "invalid argument '(-> u Int)' for 'sort', expected non-function sort as codomain sort" + +test![TestApiBlackSolver, declareSort] tm solver => do + solver.declareSort "s" 0 |> assertOkDiscard + solver.declareSort "s" 2 |> assertOkDiscard + solver.declareSort "" 2 |> assertOkDiscard + +test![TestApiBlackSolver, declareSortFresh] tm solver => do + let t1 ← solver.declareSort "b" 0 true + let t2 ← solver.declareSort "b" 0 false + let t3 ← solver.declareSort "b" 0 false + assertNe t1 t2 + assertNe t1 t3 + assertEq t2 t3 + let t4 ← solver.declareSort "c" 0 false + assertNe t2 t4 + let t5 ← solver.declareSort "b" 1 false + assertNe t2 t5 + +test![TestApiBlackSolver, defineFun] tm solver => do + let bvSort ← tm.mkBitVectorSort 32 + let funSort ← tm.mkFunctionSort #[uninterpreted] int + let b1 ← tm.mkVar bvSort "b1" + let b2 ← tm.mkVar int "b2" + let b3 ← tm.mkVar funSort "b3" + let v1 ← tm.mkConst bvSort "v1" + let v2 ← tm.mkConst funSort "v2" + solver.defineFun "f" #[] bvSort v1 |> assertOkDiscard + solver.defineFun "ff" #[b1, b2] bvSort v1 |> assertOkDiscard + solver.defineFun "ff" #[v1, b2] bvSort v1 |> assertError + "invalid bound variable in 'bound_vars' at index 0, expected a bound variable" + solver.defineFun "fff" #[b1] bvSort v2 |> assertError + "invalid sort of function body 'v2', expected '(_ BitVec 32)', found '(-> u Int)'" + solver.defineFun "ffff" #[b1] funSort v2 |> assertError + "invalid argument '(-> u Int)' for 'sort', expected non-function sort as codomain sort" + -- b3 has function sort, which is allowed as an argument + solver.defineFun "fffff" #[b1, b3] bvSort v1 |> assertOkDiscard + + let tm' ← TermManager.new + let solver' ← Solver.new tm' + let bvSort' ← tm'.mkBitVectorSort 32 + let v1' ← tm'.mkConst bvSort' "v1" + let b1' ← tm'.mkVar bvSort' "b1" + let b2' ← tm'.mkVar (← tm'.getIntegerSort) "b2" + solver'.defineFun "f" #[] bvSort v1' |> assertError + "Given sort is not associated with the term manager of this solver" + solver'.defineFun "f" #[] bvSort' v1 |> assertError + "Given term is not associated with the term manager of this solver" + solver'.defineFun "ff" #[b1, b2'] bvSort' v1' |> assertError + "invalid term in 'bound_vars' at index 0, \ + expected a term associated with the term manager of this solver" + solver'.defineFun "ff" #[b1', b2] bvSort' v1' |> assertError + "invalid term in 'bound_vars' at index 1, \ + expected a term associated with the term manager of this solver" + solver'.defineFun "ff" #[b1', b2'] bvSort v1' |> assertError + "Given sort is not associated with the term manager of this solver" + solver'.defineFun "ff" #[b1', b2'] bvSort' v1 |> assertError + "Given term is not associated with the term manager of this solver" + +test![TestApiBlackSolver, defineFunGlobal] tm solver => do + let bTrue ← tm.mkBoolean true + -- `(define-fun f () Bool true)` + let f ← solver.defineFun "f" #[] bool bTrue true + let b ← tm.mkVar bool "b" + -- `(define-fun g (b Bool) Bool b)` + let g ← solver.defineFun "g" #[b] bool b true + + -- `(assert (or (not f) (not (g true))))` + tm.mkTerm Kind.OR #[ + ← f.notTerm, ← (← tm.mkTerm Kind.APPLY_UF #[g, bTrue]).notTerm + ] >>= solver.assertFormula + assertTrue (← solver.checkSat).isUnsat + solver.resetAssertions + -- `(assert (or (not f) (not (g true))))` + tm.mkTerm Kind.OR #[ + ← f.notTerm, ← (← tm.mkTerm Kind.APPLY_UF #[g, bTrue]).notTerm + ] >>= solver.assertFormula + assertTrue (← solver.checkSat).isUnsat + + let tm' ← TermManager.new + let solver' ← Solver.new tm' + solver'.defineFun "f" #[] bool bTrue true |> assertError + "Given sort is not associated with the term manager of this solver" + +test![TestApiBlackSolver, defineFunRec] tm solver => do + let bvSort ← tm.mkBitVectorSort 32 + let funSort1 ← tm.mkFunctionSort #[bvSort, bvSort] bvSort + let funSort2 ← tm.mkFunctionSort #[uninterpreted] int + let b1 ← tm.mkVar bvSort "b1" + let b11 ← tm.mkVar bvSort "b1" + let b2 ← tm.mkVar int "b2" + let b3 ← tm.mkVar funSort2 "b3" + let v1 ← tm.mkConst bvSort "v1" + let v2 ← tm.mkConst int "v2" + let v3 ← tm.mkConst funSort2 "v3" + let f1 ← tm.mkConst funSort1 "f1" + let f2 ← tm.mkConst funSort2 "f2" + let f3 ← tm.mkConst bvSort "f3" + solver.defineFunRec "f" #[] bvSort v1 |> assertOkDiscard + solver.defineFunRec "ff" #[b1, b2] bvSort v1 |> assertOkDiscard + solver.defineFunRecTerm f1 #[b1, b11] v1 |> assertOkDiscard + solver.defineFunRec "fff" #[b1] bvSort v3 |> assertError + "invalid sort of function body 'v3', expected '(_ BitVec 32)'" + solver.defineFunRec "ff" #[b1, v2] bvSort v1 |> assertError + "invalid bound variable in 'bound_vars' at index 1, expected a bound variable" + solver.defineFunRec "ffff" #[b1] funSort2 v3 |> assertError + "invalid argument '(-> u Int)' for 'sort', expected non-function sort as codomain sort" + -- b3 has function sort, which is allowed as an argument + solver.defineFunRec "fffff" #[b1, b3] bvSort v1 |> assertOkDiscard + solver.defineFunRecTerm f1 #[b1] v1 |> assertError + "invalid size of argument 'bound_vars', expected '2'" + solver.defineFunRecTerm f1 #[b1, b11] v2 |> assertError + "invalid sort of function body 'v2', expected '(_ BitVec 32)'" + solver.defineFunRecTerm f1 #[b1, b11] v3 |> assertError + "invalid sort of function body 'v3', expected '(_ BitVec 32)'" + solver.defineFunRecTerm f2 #[b1] v2 |> assertError + "invalid sort of parameter in 'bound_vars' at index 0, expected sort 'u'" + solver.defineFunRecTerm f3 #[b1] v1 |> assertError + "invalid argument 'f3' for 'fun', expected function or nullary symbol" + + let tm' ← TermManager.new + let solver' ← Solver.new tm' + let bvSort2 ← tm'.mkBitVectorSort 32 + let v12 ← tm'.mkConst bvSort2 "v1" + let b12 ← tm'.mkVar bvSort2 "b1" + let b22 ← tm'.mkVar (← tm'.getIntegerSort) "b2" + solver'.defineFunRec "f" #[] bvSort2 v12 |> assertOkDiscard + solver'.defineFunRec "ff" #[b12, b22] bvSort2 v12 |> assertOkDiscard + solver'.defineFunRec "f" #[] bvSort v12 |> assertError + "Given sort is not associated with the term manager of this solver" + solver'.defineFunRec "f" #[] bvSort2 v1 |> assertError + "Given term is not associated with the term manager of this solver" + solver'.defineFunRec "ff" #[b1, b22] bvSort2 v12 |> assertError + "invalid term in 'bound_vars' at index 0, \ + expected a term associated with the term manager of this solver" + solver'.defineFunRec "ff" #[b12, b2] bvSort2 v12 |> assertError + "invalid term in 'bound_vars' at index 1, \ + expected a term associated with the term manager of this solver" + solver'.defineFunRec "ff" #[b12, b22] bvSort v12 |> assertError + "Given sort is not associated with the term manager of this solver" + solver'.defineFunRec "ff" #[b12, b22] bvSort2 v1 |> assertError + "Given term is not associated with the term manager of this solver" + +test![TestApiBlackSolver, defineFunRecWrongLogic] tm solver => do + solver.setLogic "QF_BV" + let bvSort ← tm.mkBitVectorSort 32 + let funSort ← tm.mkFunctionSort #[bvSort, bvSort] bvSort + let b ← tm.mkVar bvSort "b" + let v ← tm.mkConst bvSort "v" + let f ← tm.mkConst funSort "f" + solver.defineFunRec "f" #[] bvSort v |> assertError + "recursive function definitions require a logic with quantifiers" + solver.defineFunRecTerm f #[b, b] v |> assertError + "recursive function definitions require a logic with quantifiers" + +test![TestApiBlackSolver, defineFunRecGlobal] tm solver => do + solver.push + let bTrue ← tm.mkBoolean true + -- `(define-fun f () Bool true)` + let f ← solver.defineFunRec "f" #[] bool bTrue true + let b ← tm.mkVar bool "b" + -- `(define-fun g (b Boll) Bool b)` + let g ← do + let funSort ← tm.mkFunctionSort #[bool] bool + solver.defineFunRecTerm (← tm.mkConst funSort "g") #[b] b true + + -- `(assert (or (not f) (not (g true))))` + tm.mkTerm Kind.OR #[ + ← f.notTerm, ← (← tm.mkTerm Kind.APPLY_UF #[g, bTrue]).notTerm + ] >>= solver.assertFormula + assertTrue (← solver.checkSat).isUnsat + solver.pop + -- `(assert (or (not f) (not (g true))))` + tm.mkTerm Kind.OR #[ + ← f.notTerm, ← (← tm.mkTerm Kind.APPLY_UF #[g, bTrue]).notTerm + ] >>= solver.assertFormula + assertTrue (← solver.checkSat).isUnsat + + let tm' ← TermManager.new + let solver' ← Solver.new tm' + let bool' ← tm'.getBooleanSort + let b' ← tm'.mkVar bool' "b" + let g ← tm.mkConst (← tm.mkFunctionSort #[bool] bool) "g" + let g' ← tm'.mkConst (← tm'.mkFunctionSort #[bool'] bool') "g" + -- the original test does not check anything about `solver'.defineFunRecTerm`, it just creates + solver'.defineFunRecTerm g #[b'] b' true |> assertError + "Given term is not associated with the term manager of this solver" + solver'.defineFunRecTerm g' #[b] b true |> assertError + "Given term is not associated with the term manager of this solver" + +test![TestApiBlackSolver, defineFunsRec] tm solver => do + let bvSort ← tm.mkBitVectorSort 32 + let funSort1 ← tm.mkFunctionSort #[bvSort, bvSort] bvSort + let funSort2 ← tm.mkFunctionSort #[uninterpreted] int + let b1 ← tm.mkVar bvSort "b1" + let b11 ← tm.mkVar bvSort "b1" + let b2 ← tm.mkVar int "b2" + let b4 ← tm.mkVar uninterpreted "b4" + let v1 ← tm.mkConst bvSort "v1" + let v2 ← tm.mkConst int "v2" + let v4 ← tm.mkConst uninterpreted "v4" + let f1 ← tm.mkConst funSort1 "f1" + let f2 ← tm.mkConst funSort2 "f2" + let f3 ← tm.mkConst bvSort "f3" + + solver.defineFunsRec #[f1, f2] #[#[b1, b11], #[b4]] #[v1, v2] |> assertOkDiscard + solver.defineFunsRec #[f1, f2] #[#[v1, b11], #[b4]] #[v1, v2] |> assertError + "invalid bound variable in 'bvars' at index 0, expected a bound variable" + solver.defineFunsRec #[f1, f3] #[#[b1, b11], #[b4]] #[v1, v2] |> assertError + "invalid argument 'f3' for 'fun', expected function or nullary symbol" + solver.defineFunsRec #[f1, f2] #[#[b1], #[b4]] #[v1, v2] |> assertError + "invalid size of argument 'bvars', expected '2'" + solver.defineFunsRec #[f1, f2] #[#[b1, b2], #[b4]] #[v1, v2] |> assertError + "invalid sort of parameter in 'bvars' at index 1, expected sort '(_ BitVec 32)'" + solver.defineFunsRec #[f1, f2] #[#[b1, b11], #[b4]] #[v1, v4] |> assertError + "invalid sort of function body in 'terms' at index 1, expected 'Int'" + + let tm' ← TermManager.new + let solver' ← Solver.new tm' + let int' ← tm'.getIntegerSort + let uSort2 ← tm'.mkUninterpretedSort "U" + let bvSort2 ← tm'.mkBitVectorSort 32 + let funSort12 ← tm'.mkFunctionSort #[bvSort2, bvSort2] bvSort2 + let funSort22 ← tm'.mkFunctionSort #[uSort2] int' + let b12 ← tm'.mkVar bvSort2 "b1" + let b112 ← tm'.mkVar bvSort2 "b1" + let b42 ← tm'.mkVar uSort2 "b4" + let v12 ← tm'.mkConst bvSort2 "v1" + let v22 ← tm'.mkConst int' "v2" + let f12 ← tm'.mkConst funSort12 "f1" + let f22 ← tm'.mkConst funSort22 "f2" + solver'.defineFunsRec #[f12, f22] #[#[b12, b112], #[b42]] #[v12, v22] |> assertOk + solver'.defineFunsRec #[f1, f22] #[#[b12, b112], #[b42]] #[v12, v22] |> assertError + "invalid term in 'funs' at index 0, \ + expected a term associated with the term manager of this solver" + solver'.defineFunsRec #[f12, f2] #[#[b12, b112], #[b42]] #[v12, v22] |> assertError + "invalid term in 'funs' at index 1, \ + expected a term associated with the term manager of this solver" + solver'.defineFunsRec #[f12, f22] #[#[b1, b112], #[b42]] #[v12, v22] |> assertError + "invalid term in 'bvars' at index 0, \ + expected a term associated with the term manager of this solver" + solver'.defineFunsRec #[f12, f22] #[#[b12, b11], #[b42]] #[v12, v22] |> assertError + "invalid term in 'bvars' at index 1, \ + expected a term associated with the term manager of this solver" + solver'.defineFunsRec #[f12, f22] #[#[b12, b112], #[b4]] #[v12, v22] |> assertError + "invalid term in 'bvars' at index 0, \ + expected a term associated with the term manager of this solver" + solver'.defineFunsRec #[f12, f22] #[#[b12, b112], #[b42]] #[v1, v22] |> assertError + "invalid term in 'terms' at index 0, \ + expected a term associated with the term manager of this solver" + solver'.defineFunsRec #[f12, f22] #[#[b12, b112], #[b42]] #[v12, v2] |> assertError + "invalid term in 'terms' at index 1, \ + expected a term associated with the term manager of this solver" + +test![TestApiBlackSolver, defineFunsRecWrongLogic] tm solver => do + solver.setLogic "QF_BV" + let bvSort ← tm.mkBitVectorSort 32 + let funSort1 ← tm.mkFunctionSort #[bvSort, bvSort] bvSort + let funSort2 ← tm.mkFunctionSort #[uninterpreted] int + let b ← tm.mkVar bvSort "b" + let u ← tm.mkVar uninterpreted "u" + let v1 ← tm.mkConst bvSort "v1" + let v2 ← tm.mkConst int "v2" + let f1 ← tm.mkConst funSort1 "f1" + let f2 ← tm.mkConst funSort2 "f2" + solver.defineFunsRec #[f1, f2] #[#[b, b], #[u]] #[v1, v2] |> assertError + "recursive function definitions require a logic with quantifiers" + +test![TestApiBlackSolver, defineFunsRecGlobal] tm solver => do + let fSort ← tm.mkFunctionSort #[bool] bool + + solver.push + let bTrue ← tm.mkBoolean true + let b ← tm.mkVar bool "b" + let gSym ← tm.mkConst fSort "g" + -- `(define-funs-rec ((g ((b Bool)) Bool)) (b))` + solver.defineFunsRec #[gSym] #[#[b]] #[b] true + + -- `(assert (not (g true)))` + tm.mkTerm Kind.APPLY_UF #[gSym, bTrue] >>= Term.notTerm >>= solver.assertFormula + assertTrue (← solver.checkSat).isUnsat + solver.pop + -- `(assert (not (g true)))` + tm.mkTerm Kind.APPLY_UF #[gSym, bTrue] >>= Term.notTerm >>= solver.assertFormula + assertTrue (← solver.checkSat).isUnsat + +test![TestApiBlackSolver, defineFunsRecGlobal] tm solver => do + let a ← tm.mkConst bool "a" + let b ← tm.mkConst bool "b" + solver.assertFormula a + solver.assertFormula b + let asserts := #[a, b] + assertEq asserts (← solver.getAssertions) + +test![TestApiBlackSolver, getInfo] tm solver => do + solver.getInfo "name" |> assertOkDiscard + solver.getInfo "asdf" |> assertError "unrecognized flag: asdf." + +test![TestApiBlackSolver, getOption] tm solver => do + solver.getOption "incremental" |> assertOkDiscard + solver.getOption "asdf" |> assertError + "Error in option parsing: Unrecognized option key or setting: asdf" + +test![TestApiBlackSolver, getOptionNames] tm solver => do + let names ← solver.getOptionNames + assertTrue (100 < names.size) + names.findIdx? (· == "verbose") |>.isSome |> assertTrue + names.findIdx? (· == "foobar") |>.isSome |> assertFalse + +-- test![TestApiBlackSolver, getOptionInfo] tm solver => do + +test![TestApiBlackSolver, getUnsatAssumptions1] tm solver => do + solver.setOption "incremental" "false" + solver.checkSatAssuming #[(← tm.mkFalse)] |> assertOkDiscard + solver.getUnsatAssumptions |> assertError + "cannot get unsat assumptions unless explicitly enabled (try --produce-unsat-assumptions)" + +test![TestApiBlackSolver, getUnsatAssumptions2] tm solver => do + solver.setOption "incremental" "true" + solver.setOption "produce-unsat-assumptions" "false" + solver.checkSatAssuming #[(← tm.mkFalse)] |> assertOkDiscard + solver.getUnsatAssumptions |> assertError + "cannot get unsat assumptions unless explicitly enabled (try --produce-unsat-assumptions)" + +test![TestApiBlackSolver, getUnsatAssumptions3] tm solver => do + solver.setOption "incremental" "true" + solver.setOption "produce-unsat-assumptions" "true" + solver.checkSatAssuming #[(← tm.mkFalse)] |> assertOkDiscard + solver.getUnsatAssumptions |> assertOkDiscard + solver.checkSatAssuming #[(← tm.mkTrue)] |> assertOkDiscard + solver.getUnsatAssumptions |> assertError "cannot get unsat assumptions unless in unsat mode." + +test![TestApiBlackSolver, getUnsatCore1] tm solver => do + solver.setOption "incremental" "false" + solver.assertFormula (← tm.mkFalse) + solver.checkSat |> assertOkDiscard + solver.getUnsatCore |> assertError + "cannot get unsat core unless explicitly enabled (try --produce-unsat-cores)" + +test![TestApiBlackSolver, getUnsatCore2] tm solver => do + solver.setOption "incremental" "true" + solver.setOption "produce-unsat-cores" "false" + solver.assertFormula (← tm.mkFalse) + solver.checkSat |> assertOkDiscard + solver.getUnsatCore |> assertError + "cannot get unsat core unless explicitly enabled (try --produce-unsat-cores)" + +test![TestApiBlackSolver, getUnsatCoreAndProof] tm solver => do + solver.setOption "incremental" "true" + solver.setOption "produce-unsat-cores" "true" + solver.setOption "produce-proofs" "true" + + + let uToIntSort ← tm.mkFunctionSort #[uninterpreted] int + let intPredSort ← tm.mkFunctionSort #[int] bool + + let x ← tm.mkConst uninterpreted "x" + let y ← tm.mkConst uninterpreted "y" + let f ← tm.mkConst uToIntSort "f" + let p ← tm.mkConst intPredSort "p" + let zero ← tm.mkInteger 0 + let one ← tm.mkInteger 1 + let f_x ← tm.mkTerm Kind.APPLY_UF #[f, x] + let f_y ← tm.mkTerm Kind.APPLY_UF #[f, y] + let sum ← tm.mkTerm Kind.ADD #[f_x, f_y] + let p_0 ← tm.mkTerm Kind.APPLY_UF #[p, zero] + let p_f_y ← tm.mkTerm Kind.APPLY_UF #[p, f_y] + tm.mkTerm Kind.GT #[zero, f_x] >>= solver.assertFormula + tm.mkTerm Kind.GT #[zero, f_y] >>= solver.assertFormula + tm.mkTerm Kind.GT #[sum, one] >>= solver.assertFormula + solver.assertFormula p_0 + p_f_y.notTerm >>= solver.assertFormula + assertTrue (← solver.checkSat).isUnsat + + let uc ← assertOk solver.getUnsatCore + assertFalse uc.isEmpty + + solver.getProof |> assertOkDiscard + solver.getProof ProofComponent.SAT |> assertOkDiscard + + solver.resetAssertions + for t in uc do + solver.assertFormula t + let res ← solver.checkSat + assertTrue res.isUnsat + solver.getProof |> assertOkDiscard + +test![TestApiBlackSolver, getUnsatCoreAndLemmas1] tm solver => do + solver.setOption "produce-unsat-cores" "true" + solver.setOption "unsat-cores-mode" "sat-proof" + -- cannot ask before a check sat + solver.getUnsatCoreLemmas |> assertError "cannot get unsat core unless in unsat mode." + + tm.mkFalse >>= solver.assertFormula + assertTrue (← solver.checkSat).isUnsat + solver.getUnsatCoreLemmas |> assertOkDiscard + +test![TestApiBlackSolver, getUnsatCoreAndLemmas2] tm solver => do + solver.setOption "incremental" "true" + solver.setOption "produce-unsat-cores" "true" + solver.setOption "produce-proofs" "true" + + + let uToIntSort ← tm.mkFunctionSort #[uninterpreted] int + let intPredSort ← tm.mkFunctionSort #[int] bool + + let x ← tm.mkConst uninterpreted "x" + let y ← tm.mkConst uninterpreted "y" + let f ← tm.mkConst uToIntSort "f" + let p ← tm.mkConst intPredSort "p" + let zero ← tm.mkInteger 0 + let one ← tm.mkInteger 1 + let f_x ← tm.mkTerm Kind.APPLY_UF #[f, x] + let f_y ← tm.mkTerm Kind.APPLY_UF #[f, y] + let sum ← tm.mkTerm Kind.ADD #[f_x, f_y] + let p_0 ← tm.mkTerm Kind.APPLY_UF #[p, zero] + let p_f_y ← tm.mkTerm Kind.APPLY_UF #[p, f_y] + tm.mkTerm Kind.GT #[zero, f_x] >>= solver.assertFormula + tm.mkTerm Kind.GT #[zero, f_y] >>= solver.assertFormula + tm.mkTerm Kind.GT #[sum, one] >>= solver.assertFormula + solver.assertFormula p_0 + p_f_y.notTerm >>= solver.assertFormula + assertTrue (← solver.checkSat).isUnsat + + solver.getUnsatCoreLemmas |> assertOkDiscard + +test![TestApiBlackSolver, getAbduct] tm solver => do + solver.setLogic "QF_LIA" + solver.setOption "produce-abducts" "true" + solver.setOption "incremental" "false" + + let zero ← tm.mkInteger 0 + let x ← tm.mkConst int "x" + let y ← tm.mkConst int "y" + + -- assumptions for abduction `x > 0` + tm.mkTerm Kind.GT #[x, zero] >>= solver.assertFormula + -- conjecture for abduction `y > 0` + let conj ← tm.mkTerm Kind.GT #[y, zero] + -- call the abduction api, while the resulting abduct is the output + let output ← solver.getAbduct conj + -- we expect the resulting output to be a boolean formula + assertTrue (¬ output.isNull ∧ (← output.getSort).isBoolean) + + -- try with a grammar, a simple grammar admitting true + let truen ← tm.mkBoolean true + let start ← tm.mkVar bool + let mut g ← solver.mkGrammar #[] #[start] + let conj2 ← tm.mkTerm Kind.GT #[x, zero] + solver.getAbduct conj2 g |> assertError + "invalid grammar, must have at least one rule for each non-terminal symbol" + g ← g.addRule start truen + -- call the abduction api, while the resulting abduct is the output + let output2 ← solver.getAbduct conj2 g + -- abduct must be true + assertEq truen output2 + + let tm' ← TermManager.new + let solver' ← Solver.new tm' + solver'.setOption "produce-abducts" "true" + let int' ← tm'.getIntegerSort + let xx ← tm'.mkConst int' "x" + let yy ← tm'.mkConst int' "y" + let zzero ← tm'.mkInteger 0 + let sstart ← tm'.getBooleanSort >>= tm'.mkVar + tm'.mkTerm Kind.GT #[← tm'.mkTerm Kind.ADD #[xx, yy], zzero] >>= solver'.assertFormula + let mut gg ← solver'.mkGrammar #[] #[sstart] + gg ← tm'.mkTrue >>= gg.addRule sstart + let cconj2 ← tm'.mkTerm Kind.EQUAL #[zzero, zzero] + solver'.getAbduct cconj2 gg |> assertOkDiscard + solver'.getAbduct conj2 |> assertError + "Given term is not associated with the term manager of this solver" + solver'.getAbduct conj2 gg |> assertError + "Given term is not associated with the term manager of this solver" + solver'.getAbduct cconj2 g |> assertError + "Given grammar is not associated with the term manager of this solver" + +test![TestApiBlackSolver, getAbduct2] tm solver => do + solver.setLogic "QF_LIA" + solver.setOption "incremental" "false" + let zero ← tm.mkInteger 0 + let x ← tm.mkConst int "x" + let y ← tm.mkConst int "y" + -- assumptions for abduction: `x > 0` + tm.mkTerm Kind.GT #[x, zero] >>= solver.assertFormula + -- conjecture for abduction: `y > 0` + let conj ← tm.mkTerm Kind.GT #[y, zero] + -- fails due to option not set + solver.getAbduct conj |> assertError + "cannot get abduct unless abducts are enabled (try --produce-abducts)" + +test![TestApiBlackSolver, getAbductNext] tm solver => do + solver.setLogic "QF_LIA" + solver.setOption "produce-abducts" "true" + solver.setOption "incremental" "true" + + let zero ← tm.mkInteger 0 + let x ← tm.mkConst int "x" + let y ← tm.mkConst int "y" + + -- assumptions for abduction: `x > 0` + tm.mkTerm Kind.GT #[x, zero] >>= solver.assertFormula + -- conjecture for abduction: `y > 0` + let conj ← tm.mkTerm Kind.GT #[y, zero] + -- call the abduction api, while the resulting abduct is the output + let output ← solver.getAbduct conj + let output2 ← solver.getAbductNext + -- should produce a different output + assertNe output output2 + +test![TestApiBlackSolver, getInterpolant] tm solver => do + solver.setLogic "QF_LIA" + solver.setOption "produce-interpolants" "true" + solver.setOption "incremental" "false" + + let zero ← tm.mkInteger 0 + let x ← tm.mkConst int "x" + let y ← tm.mkConst int "y" + let z ← tm.mkConst int "z" + + -- assumptions for interpolation: `x + y > 0 ∧ x < 0` + tm.mkTerm Kind.GT #[← tm.mkTerm Kind.ADD #[x, y], zero] >>= solver.assertFormula + tm.mkTerm Kind.LT #[x, zero] >>= solver.assertFormula + -- conjecture for interpolation: `y + z > 0 ∨ z < 0` + let conj ← tm.mkTerm Kind.OR #[ + ← tm.mkTerm Kind.GT #[← tm.mkTerm Kind.ADD #[y, z], zero], + ← tm.mkTerm Kind.LT #[z, zero], + ] + -- call the interpolation api, while the resulting interpolant is the output + let output ← solver.getInterpolant conj + -- we expect the resulting output to be a boolean formula + assertTrue (← output.getSort).isBoolean + + -- try with a grammar, a simple grammar admitting true + let truen ← tm.mkBoolean true + let start ← tm.mkVar bool + let mut g ← solver.mkGrammar #[] #[start] + let conj2 ← tm.mkTerm Kind.EQUAL #[zero, zero] + solver.getInterpolant conj2 g |> assertError + "invalid grammar, must have at least one rule for each non-terminal symbol" + g ← g.addRule start truen |> assertOk + -- call the interpolation api, while the resulting interpolant is the output + let output2 ← solver.getInterpolant conj2 g + -- interpolant must be true + assertEq truen output2 + + let tm' ← TermManager.new + let solver' ← Solver.new tm' + solver'.setOption "produce-interpolants" "true" + let zzero ← tm'.mkInteger 0 + let sstart ← tm'.getBooleanSort >>= tm'.mkVar + let mut gg ← solver'.mkGrammar #[] #[sstart] + gg ← tm'.mkTrue >>= gg.addRule sstart + let cconj2 ← tm'.mkTerm Kind.EQUAL #[zzero, zzero] + solver'.getInterpolant cconj2 gg |> assertOkDiscard + solver'.getInterpolant conj2 |> assertError + "Given term is not associated with the term manager of this solver" + solver'.getInterpolant conj2 gg |> assertError + "Given term is not associated with the term manager of this solver" + solver'.getInterpolant cconj2 g |> assertError + "Given grammar is not associated with the term manager of this solver" + +test![TestApiBlackSolver, getInterpolantNext] tm solver => do + solver.setLogic "QF_LIA" + solver.setOption "produce-interpolants" "true" + solver.setOption "incremental" "true" + + let zero ← tm.mkInteger 0 + let x ← tm.mkConst int "x" + let y ← tm.mkConst int "y" + let z ← tm.mkConst int "z" + -- assumptions for interpolation: `x + y > 0 ∧ x < 0` + tm.mkTerm Kind.GT #[← tm.mkTerm Kind.ADD #[x, y], zero] >>= solver.assertFormula + tm.mkTerm Kind.LT #[x, zero] >>= solver.assertFormula + -- conjecture for interpolation: `y + z > 0 ∨ z < 0` + let conj ← tm.mkTerm Kind.OR #[ + ← tm.mkTerm Kind.GT #[← tm.mkTerm Kind.ADD #[y, z], zero], + ← tm.mkTerm Kind.LT #[z, zero], + ] + let output ← solver.getInterpolant conj + let output2 ← solver.getInterpolantNext + + -- we expect the next output to be distinct + assertNe output output2 + +test![TestApiBlackSolver, declarePool] tm solver => do + let setSort ← tm.mkSetSort int + let zero ← tm.mkInteger 0 + let x ← tm.mkConst int "x" + let y ← tm.mkConst int "y" + -- declare a ppol with initial value `{0, x, y}` + let p ← solver.declarePool "p" int #[zero, x, y] + -- pool should have the same sort + assertTrue ((← p.getSort) == setSort) + solver.declarePool "i" (Sort.null ()) #[] |> assertError "invalid null argument for 'sort'" + + let tm' ← TermManager.new + let solver' ← Solver.new tm' + let int' ← tm'.getIntegerSort + let zero' ← tm'.mkInteger 0 + let x' ← tm'.mkConst int' "x" + let y' ← tm'.mkConst int' "y" + solver'.declarePool "p" int #[zero', x', y'] |> assertError + "Given sort is not associated with the term manager of this solver" + solver'.declarePool "p" int' #[zero, x', y'] |> assertError + "invalid term in 'initValue' at index 0, \ + expected a term associated with the term manager of this solver" + solver'.declarePool "p" int' #[zero', x, y'] |> assertError + "invalid term in 'initValue' at index 1, \ + expected a term associated with the term manager of this solver" + solver'.declarePool "p" int' #[zero', x', y] |> assertError + "invalid term in 'initValue' at index 2, \ + expected a term associated with the term manager of this solver" + +-- test![TestApiBlackSolver, getDriverOptions] tm solver => do + +-- test![TestApiBlackSolver, getStatistics] tm solver => do + +-- test![TestApiBlackSolver, printStatisticsSafe] tm solver => do + +test![TestApiBlackSolver, getProofAndProofToString] tm solver => do + solver.setOption "produce-proofs" "true" + + let uToIntSort ← tm.mkFunctionSort #[uninterpreted] int + let intPredSort ← tm.mkFunctionSort #[int] bool + + let x ← tm.mkConst uninterpreted "x" + let y ← tm.mkConst uninterpreted "y" + let f ← tm.mkConst uToIntSort "f" + let p ← tm.mkConst intPredSort "p" + let zero ← tm.mkInteger 0 + let one ← tm.mkInteger 1 + let f_x ← tm.mkTerm Kind.APPLY_UF #[f, x] + let f_y ← tm.mkTerm Kind.APPLY_UF #[f, y] + let sum ← tm.mkTerm Kind.ADD #[f_x, f_y] + let p_0 ← tm.mkTerm Kind.APPLY_UF #[p, zero] + let p_f_y ← tm.mkTerm Kind.APPLY_UF #[p, f_y] + tm.mkTerm Kind.GT #[zero, f_x] >>= solver.assertFormula + tm.mkTerm Kind.GT #[zero, f_y] >>= solver.assertFormula + tm.mkTerm Kind.GT #[sum, one] >>= solver.assertFormula + solver.assertFormula p_0 + p_f_y.notTerm >>= solver.assertFormula + assertTrue (← solver.checkSat).isUnsat + + let mut proofs ← solver.getProof |> assertOk + assertFalse proofs.isEmpty + let mut printedProof ← solver.proofToString proofs[0]! |> assertOk + assertFalse printedProof.isEmpty + printedProof ← solver.proofToString proofs[0]! ProofFormat.ALETHE |> assertOk + assertFalse printedProof.isEmpty + proofs ← solver.getProof ProofComponent.SAT |> assertOk + printedProof ← solver.proofToString proofs[0]! ProofFormat.NONE |> assertOk + assertFalse printedProof.isEmpty + +-- test![TestApiBlackSolver, proofToStringAssertionNames] tm solver => do + +-- test![TestApiBlackSolver, getDifficulty] tm solver => do +-- test![TestApiBlackSolver, getDifficulty2] tm solver => do +-- test![TestApiBlackSolver, getDifficulty3] tm solver => do + +test![TestApiBlackSolver, getLearnedLiterals] tm solver => do + solver.setOption "produce-learned-literals" "true" + -- cannot ask before a check sat + solver.getLearnedLiterals |> assertError + "cannot get learned literals unless after a UNSAT, SAT or UNKNOWN response." + solver.checkSat |> assertOkDiscard + solver.getLearnedLiterals |> assertOkDiscard + solver.getLearnedLiterals LearnedLitType.PREPROCESS |> assertOkDiscard + +test![TestApiBlackSolver, getLearnedLiterals2] tm solver => do + solver.setOption "produce-learned-literals" "true" + let x ← tm.mkConst int "x" + let y ← tm.mkConst int "y" + let zero ← tm.mkInteger 0 + let ten ← tm.mkInteger 10 + let f0 ← tm.mkTerm Kind.GEQ #[x, ten] + let f1 ← tm.mkTerm Kind.OR #[← tm.mkTerm Kind.GEQ #[zero, x], ← tm.mkTerm Kind.GEQ #[y, zero]] + solver.assertFormula f0 + solver.assertFormula f1 + solver.checkSat |> assertOkDiscard + solver.getLearnedLiterals |> assertOkDiscard + +test![TestApiBlackSolver, getTimeoutCore] tm solver => do + solver.setOption "timeout-core-timeout" "100" + solver.setOption "produce-unsat-cores" "true" + let x ← tm.mkConst int "x" + let tt ← tm.mkBoolean true + let hard ← tm.mkTerm Kind.EQUAL + #[← tm.mkTerm Kind.MULT #[x, x], ← tm.mkIntegerOfString "501240912901901249014210220059591"] + solver.assertFormula tt + solver.assertFormula hard + let (res, terms) ← solver.getTimeoutCore + assertTrue res.isUnknown + assertEq 1 terms.size + assertEq hard terms[0]! + +test![TestApiBlackSolver, getTimeoutCoreUnsat] tm solver => do + solver.setOption "produce-unsat-cores" "true" + let ff ← tm.mkBoolean false + let tt ← tm.mkBoolean true + solver.assertFormula tt + solver.assertFormula ff + solver.assertFormula tt + let (res, terms) ← solver.getTimeoutCore + assertTrue res.isUnsat + assertEq 1 terms.size + assertEq ff terms[0]! + +test![TestApiBlackSolver, getTimeoutCoreAssuming] tm solver => do + solver.setOption "produce-unsat-cores" "true" + let ff ← tm.mkBoolean false + let tt ← tm.mkBoolean true + solver.assertFormula tt + let (res, terms) ← solver.getTimeoutCoreAssuming #[ff, tt] + assertTrue res.isUnsat + assertEq 1 terms.size + assertEq ff terms[0]! + +test![TestApiBlackSolver, getTimeoutCoreAssumingEmpty] tm solver => do + solver.setOption "produce-unsat-cores" "true" + solver.getTimeoutCoreAssuming #[] |> assertError + "cannot get timeout core assuming an empty set of assumptions" + +test![TestApiBlackSolver, getValue1] tm solver => do + solver.setOption "produce-models" "false" + let t ← tm.mkTrue + solver.assertFormula t + solver.checkSat |> assertOkDiscard + solver.getValue t |> assertError + "cannot get value unless model generation is enabled (try --produce-models)" + +test![TestApiBlackSolver, getValue2] tm solver => do + solver.setOption "produce-models" "true" + let t ← tm.mkFalse + solver.assertFormula t + solver.checkSat |> assertOkDiscard + solver.getValue t |> assertError "cannot get value unless after a SAT or UNKNOWN response." + +test![TestApiBlackSolver, getValue3] tm solver => do + solver.setOption "produce-models" "true" + let uToIntSort ← tm.mkFunctionSort #[uninterpreted] int + let intPredSort ← tm.mkFunctionSort #[int] bool + + let x ← tm.mkConst uninterpreted "x" + let y ← tm.mkConst uninterpreted "y" + let z ← tm.mkConst uninterpreted "z" + let f ← tm.mkConst uToIntSort "f" + let p ← tm.mkConst intPredSort "p" + let zero ← tm.mkInteger 0 + let one ← tm.mkInteger 1 + let f_x ← tm.mkTerm Kind.APPLY_UF #[f, x] + let f_y ← tm.mkTerm Kind.APPLY_UF #[f, y] + let sum ← tm.mkTerm Kind.ADD #[f_x, f_y] + let p_0 ← tm.mkTerm Kind.APPLY_UF #[p, zero] + let p_f_y ← tm.mkTerm Kind.APPLY_UF #[p, f_y] + + tm.mkTerm Kind.LEQ #[zero, f_x] >>= solver.assertFormula + tm.mkTerm Kind.LEQ #[zero, f_y] >>= solver.assertFormula + tm.mkTerm Kind.LEQ #[sum, one] >>= solver.assertFormula + p_0.notTerm >>= solver.assertFormula + solver.assertFormula p_f_y + assertTrue (← solver.checkSat).isSat + solver.getValue x |> assertOkDiscard + solver.getValue y |> assertOkDiscard + solver.getValue z |> assertOkDiscard + solver.getValue sum |> assertOkDiscard + solver.getValue p_f_y |> assertOkDiscard + + let a := #[← solver.getValue x, ← solver.getValue y, ← solver.getValue z] + let b ← solver.getValues #[x, y, z] + assertEq a b + + (← Solver.new tm).getValue x |> assertError + "cannot get value unless model generation is enabled (try --produce-models)" + + let _ ← do + let solver' ← Solver.new tm + solver'.setOption "produce-models" "true" + solver'.getValue x |> assertError + "cannot get value unless after a SAT or UNKNOWN response." + + let _ ← do + let solver' ← Solver.new tm + solver'.setOption "produce-models" "true" + solver'.checkSat |> assertOkDiscard + solver'.getValue x |> assertOkDiscard + + let tm' ← TermManager.new + let solver' ← Solver.new tm' + solver'.setOption "produce-models" "true" + solver'.checkSat |> assertOkDiscard + solver'.getValue (← tm.mkConst bool "x") |> assertError + "Given term is not associated with the term manager of this solver" + +test![TestApiBlackSolver, getModelDomainElements] tm solver => do + solver.setOption "produce-models" "true" + let x ← tm.mkConst uninterpreted "x" + let y ← tm.mkConst uninterpreted "y" + let z ← tm.mkConst uninterpreted "z" + let f ← tm.mkTerm Kind.DISTINCT #[x, y, z] + solver.assertFormula f + solver.checkSat |> assertOkDiscard + let elems ← solver.getModelDomainElements uninterpreted + assertEq 3 elems.size + solver.getModelDomainElements int |> assertError + "expected an uninterpreted sort as argument to getModelDomainElements." + +test![TestApiBlackSolver, getModelDomainElements2] tm solver => do + solver.setOption "produce-models" "true" + solver.setOption "finite-model-find" "true" + let x ← tm.mkVar uninterpreted "x" + let y ← tm.mkVar uninterpreted "y" + let eq ← tm.mkTerm Kind.EQUAL #[x, y] + let bvl ← tm.mkTerm Kind.VARIABLE_LIST #[x, y] + let f ← tm.mkTerm Kind.FORALL #[bvl, eq] + solver.assertFormula f + solver.checkSat |> assertOkDiscard + let elems ← solver.getModelDomainElements uninterpreted + -- a module for the above must interpret `u` as size 1 + assertEq 1 elems.size + +test![TestApiBlackSolver, isModelCoreSymbol] tm solver => do + solver.setOption "produce-models" "true" + solver.setOption "model-cores" "simple" + let x ← tm.mkConst uninterpreted "x" + let y ← tm.mkConst uninterpreted "y" + let z ← tm.mkConst uninterpreted "z" + let zero ← tm.mkInteger 0 + let f ← tm.mkTerm Kind.NOT #[← tm.mkTerm Kind.EQUAL #[x, y]] + solver.assertFormula f + solver.checkSat |> assertOkDiscard + assertTrue (← solver.isModelCoreSymbol x) + assertTrue (← solver.isModelCoreSymbol y) + assertFalse (← solver.isModelCoreSymbol z) + solver.isModelCoreSymbol zero |> assertError + "expected a free constant as argument to isModelCoreSymbol." + + let tm' ← TermManager.new + let solver' ← Solver.new tm' + solver'.setOption "produce-models" "true" + solver'.checkSat |> assertOkDiscard + solver'.isModelCoreSymbol (← tm.mkConst uninterpreted "x") |> assertError + "Given term is not associated with the term manager of this solver" + +test![TestApiBlackSolver, getModel] tm solver => do + solver.setOption "produce-models" "true" + let x ← tm.mkConst uninterpreted "x" + let y ← tm.mkConst uninterpreted "y" + -- -- not used in original test + -- let z ← tm.mkConst uninterpreted "z" + let f ← tm.mkTerm Kind.NOT #[← tm.mkTerm Kind.EQUAL #[x, y]] + solver.assertFormula f + solver.checkSat |> assertOkDiscard + let sorts := #[uninterpreted] + let terms := #[x, y] + solver.getModel sorts terms |> assertOkDiscard + solver.getModel sorts (terms.push <| Term.null ()) |> assertError + "invalid null term in 'vars' at index 2" + +test![TestApiBlackSolver, getModel2] tm solver => do + solver.setOption "produce-models" "true" + solver.getModel #[] #[] |> assertError + "cannot get model unless after a SAT or UNKNOWN response." + +test![TestApiBlackSolver, getModel3] tm solver => do + solver.setOption "produce-models" "true" + solver.checkSat |> assertOkDiscard + solver.getModel #[] #[] |> assertOkDiscard + solver.getModel #[int] #[] |> assertError + "expected an uninterpreted sort as argument to getModel." + +test![TestApiBlackSolver, getQuantifierElimitation] tm solver => do + let x ← tm.mkVar bool "x" + let term ← tm.mkTerm Kind.FORALL #[ + ← tm.mkTerm Kind.VARIABLE_LIST #[ x ], + ← tm.mkTerm Kind.OR #[x, ← tm.mkTerm Kind.NOT #[ x ]] + ] + solver.getQuantifierElimination (Term.null ()) |> assertError "invalid null argument for 'q'" + solver.getQuantifierElimination (← tm.mkBoolean false) |> assertError + "Expecting a quantified formula as argument to get-qe." + solver.getQuantifierElimination term |> assertOkDiscard + + let tm' ← TermManager.new + let solver' ← Solver.new tm' + solver'.checkSat |> assertOkDiscard + solver'.getQuantifierElimination term |> assertError + "Given term is not associated with the term manager of this solver" + +test![TestApiBlackSolver, getQuantifierElimitationDisjunct] tm solver => do + let x ← tm.mkVar bool "x" + let term ← tm.mkTerm Kind.FORALL #[ + ← tm.mkTerm Kind.VARIABLE_LIST #[ x ], + ← tm.mkTerm Kind.OR #[x, ← tm.mkTerm Kind.NOT #[ x ]] + ] + solver.getQuantifierEliminationDisjunct (Term.null ()) |> assertError + "invalid null argument for 'q'" + solver.getQuantifierEliminationDisjunct (← tm.mkBoolean false) |> assertError + "Expecting a quantified formula as argument to get-qe." + solver.getQuantifierEliminationDisjunct term |> assertOkDiscard + + let tm' ← TermManager.new + let solver' ← Solver.new tm' + solver'.checkSat |> assertOkDiscard + solver'.getQuantifierEliminationDisjunct term |> assertError + "Given term is not associated with the term manager of this solver" + +test![TestApiBlackSolver, declareSepHeap] tm solver => do + solver.setLogic "ALL" + solver.setOption "incremental" "false" + solver.declareSepHeap int int |> assertOk + -- cannot declare separation logic heap more than once + solver.declareSepHeap int int |> assertError + "ERROR: cannot declare heap types for separation logic more than once. \ + We are declaring heap of type Int -> Int, but we already have Int -> Int" + + let tm' ← TermManager.new + let _ ← do + let int' ← tm'.getIntegerSort + let solver' ← Solver.new tm' + -- no logic set yet + solver'.declareSepHeap int' int' |> assertError + "cannot call 'declareSepHeap()' if logic is not set" + let _ ← do + let real' ← tm'.getRealSort + let solver' ← Solver.new tm' + solver'.setLogic "ALL" + solver'.declareSepHeap int real' |> assertError + "Given sort is not associated with the term manager of this solver" + let _ ← do + let bool' ← tm'.getBooleanSort + let solver' ← Solver.new tm' + solver'.setLogic "ALL" + solver'.declareSepHeap bool' int |> assertError + "Given sort is not associated with the term manager of this solver" + +/-- Helper function for `testGetSeparatior{Heap,Nil}TermX`. + +Asserts and checks some simple separation logic constraints. +-/ +def checkSimpleSeparationConstraints (tm : TermManager) (solver : Solver) : Env Unit := do + let int ← tm.getIntegerSort + -- declare the separation heap + solver.declareSepHeap int int + let x ← tm.mkConst int "x" + let p ← tm.mkConst int "p" + let heap ← tm.mkTerm Kind.SEP_PTO #[p, x] + solver.assertFormula heap + let nil ← tm.mkSepNil int + tm.mkInteger 5 >>= nil.eqTerm >>= solver.assertFormula + solver.checkSat |> assertOkDiscard + +test![TestApiBlackSolver, getValueSepHeap1] tm solver => do + solver.setLogic "QF_BV" + solver.setOption "incremental" "false" + solver.setOption "produce-models" "true" + let t ← tm.mkTrue + solver.assertFormula t + solver.getValueSepHeap |> assertError + "cannot obtain separation logic expressions if not using the separation logic theory." + +test![TestApiBlackSolver, getValueSepHeap2] tm solver => do + solver.setLogic "ALL" + solver.setOption "incremental" "false" + solver.setOption "produce-models" "false" + checkSimpleSeparationConstraints tm solver + solver.getValueSepHeap |> assertError + "cannot get separation heap term unless model generation is enabled (try --produce-models)" + +test![TestApiBlackSolver, getValueSepHeap3] tm solver => do + solver.setLogic "ALL" + solver.setOption "incremental" "false" + solver.setOption "produce-models" "true" + let t ← tm.mkFalse + solver.assertFormula t + solver.checkSat |> assertOkDiscard + solver.getValueSepHeap |> assertError + "can only get separtion heap term after SAT or UNKNOWN response." + +test![TestApiBlackSolver, getValueSepHeap4] tm solver => do + solver.setLogic "ALL" + solver.setOption "incremental" "false" + solver.setOption "produce-models" "true" + let t ← tm.mkTrue + solver.assertFormula t + solver.checkSat |> assertOkDiscard + solver.getValueSepHeap |> assertError "Failed to obtain heap/nil expressions from theory model." + +test![TestApiBlackSolver, getValueSepHeap5] tm solver => do + solver.setLogic "ALL" + solver.setOption "incremental" "false" + solver.setOption "produce-models" "true" + checkSimpleSeparationConstraints tm solver + solver.getValueSepHeap |> assertOkDiscard + +test![TestApiBlackSolver, getValueSepNil1] tm solver => do + solver.setLogic "QF_BV" + solver.setOption "incremental" "false" + solver.setOption "produce-models" "true" + let t ← tm.mkTrue + solver.assertFormula t + solver.getValueSepNil |> assertError + "cannot obtain separation logic expressions if not using the separation logic theory." + +test![TestApiBlackSolver, getValueSepNil2] tm solver => do + solver.setLogic "ALL" + solver.setOption "incremental" "false" + solver.setOption "produce-models" "false" + checkSimpleSeparationConstraints tm solver + solver.getValueSepNil |> assertError + "cannot get separation nil term unless model generation is enabled (try --produce-models)" + +test![TestApiBlackSolver, getValueSepNil3] tm solver => do + solver.setLogic "ALL" + solver.setOption "incremental" "false" + solver.setOption "produce-models" "true" + let t ← tm.mkFalse + solver.assertFormula t + solver.checkSat |> assertOkDiscard + solver.getValueSepNil |> assertError + "can only get separtion nil term after SAT or UNKNOWN response." + +test![TestApiBlackSolver, getValueSepNil4] tm solver => do + solver.setLogic "ALL" + solver.setOption "incremental" "false" + solver.setOption "produce-models" "true" + let t ← tm.mkTrue + solver.assertFormula t + solver.checkSat |> assertOkDiscard + solver.getValueSepNil |> assertError "Failed to obtain heap/nil expressions from theory model." + +test![TestApiBlackSolver, getValueSepNil5] tm solver => do + solver.setLogic "ALL" + solver.setOption "incremental" "false" + solver.setOption "produce-models" "true" + checkSimpleSeparationConstraints tm solver + solver.getValueSepNil |> assertOkDiscard + +test![TestApiBlackSolver, push1] tm solver => do + solver.setOption "incremental" "true" + solver.push 1 |> assertOkDiscard + solver.setOption "incremental" "false" |> assertError + "invalid call to 'setOption' for option 'incremental', solver is already fully initialized" + solver.setOption "incremental" "true" |> assertError + "invalid call to 'setOption' for option 'incremental', solver is already fully initialized" + +test![TestApiBlackSolver, push2] tm solver => do + solver.setOption "incremental" "false" + solver.push 1 |> assertError "cannot push when not solving incrementally (use --incremental)" + +test![TestApiBlackSolver, pop1] tm solver => do + solver.setOption "incremental" "false" + solver.pop 1 |> assertError "cannot pop when not solving incrementally (use --incremental)" + +test![TestApiBlackSolver, pop2] tm solver => do + solver.setOption "incremental" "true" + solver.pop 1 |> assertError "cannot pop beyond first pushed context" + +test![TestApiBlackSolver, pop3] tm solver => do + solver.setOption "incremental" "true" + solver.push 1 |> assertOkDiscard + solver.pop 1 |> assertOkDiscard + solver.pop 1 |> assertError "cannot pop beyond first pushed context" + +test![TestApiBlackSolver, blockModel1] tm solver => do + let x ← tm.mkConst bool "x" + x.eqTerm x >>= solver.assertFormula + solver.checkSat |> assertOkDiscard + solver.blockModel BlockModelsMode.LITERALS |> assertError + "cannot get value unless model generation is enabled (try --produce-models)" + +test![TestApiBlackSolver, blockModel2] tm solver => do + solver.setOption "produce-models" "true" + let x ← tm.mkConst bool "x" + x.eqTerm x >>= solver.assertFormula + solver.blockModel BlockModelsMode.LITERALS |> assertError + "can only block model after SAT or UNKNOWN response." + +test![TestApiBlackSolver, blockModel3] tm solver => do + solver.setOption "produce-models" "true" + let x ← tm.mkConst bool "x" + x.eqTerm x >>= solver.assertFormula + solver.checkSat |> assertOkDiscard + solver.blockModel BlockModelsMode.LITERALS |> assertOkDiscard + +test![TestApiBlackSolver, blockModelValues1] tm solver => do + solver.setOption "produce-models" "true" + let x ← tm.mkConst bool "x" + x.eqTerm x >>= solver.assertFormula + solver.checkSat |> assertOkDiscard + solver.blockModelValues #[] |> assertError + "invalid size of argument 'terms', expected a non-empty set of terms" + solver.blockModelValues #[Term.null ()] |> assertError "invalid null term in 'terms' at index 0" + solver.blockModelValues #[← tm.mkBoolean false] |> assertOkDiscard + + let tm' ← TermManager.new + let solver' ← Solver.new tm' + solver'.setOption "produce-models" "true" + solver'.checkSat |> assertOkDiscard + solver'.blockModelValues #[← tm.mkFalse] |> assertError + "invalid term in 'terms' at index 0, \ + expected a term associated with the term manager of this solver" + +test![TestApiBlackSolver, blockModelValues2] tm solver => do + solver.setOption "produce-models" "true" + let x ← tm.mkConst bool "x" + x.eqTerm x >>= solver.assertFormula + solver.checkSat |> assertOkDiscard + solver.blockModelValues #[ x ] |> assertOkDiscard + +test![TestApiBlackSolver, blockModelValues3] tm solver => do + let x ← tm.mkConst bool "x" + x.eqTerm x >>= solver.assertFormula + solver.checkSat |> assertOkDiscard + solver.blockModelValues #[ x ] |> assertError + "cannot get value unless model generation is enabled (try --produce-models)" + +test![TestApiBlackSolver, blockModelValues4] tm solver => do + solver.setOption "produce-models" "true" + let x ← tm.mkConst bool "x" + x.eqTerm x >>= solver.assertFormula + solver.blockModelValues #[ x ] |> assertError + "can only block model values after SAT or UNKNOWN response." + +test![TestApiBlackSolver, blockModelValues5] tm solver => do + solver.setOption "produce-models" "true" + let x ← tm.mkConst bool "x" + x.eqTerm x >>= solver.assertFormula + solver.checkSat |> assertOkDiscard + solver.blockModelValues #[ x ] |> assertOkDiscard + +test![TestApiBlackSolver, getInstantiations] tm solver => do + let p ← solver.declareFun "p" #[int] bool + let x ← tm.mkVar int "x" + let bvl ← tm.mkTerm Kind.VARIABLE_LIST #[ x ] + let app ← tm.mkTerm Kind.APPLY_UF #[p, x] + let q ← tm.mkTerm Kind.FORALL #[bvl, app] + solver.assertFormula q + let five ← tm.mkInteger 5 + let app2 ← tm.mkTerm Kind.NOT #[← tm.mkTerm Kind.APPLY_UF #[p, five]] + solver.assertFormula app2 + solver.getInstantiations |> assertError + "cannot get instantiations unless after a UNSAT, SAT or UNKNOWN response." + solver.checkSat |> assertOkDiscard + solver.getInstantiations |> assertOkDiscard + +test![TestApiBlackSolver, setInfo] tm solver => do + let err s := s!"\ + unrecognized keyword: {s}, expected 'source', 'category', \ + 'difficulty', 'filename', 'license', 'name', 'notes', 'smt-lib-version' or 'status'\ + " + solver.setInfo "cvc5-lagic" "QF_BV" |> assertError (err "cvc5-lagic") + solver.setInfo "cvc2-logic" "QF_BV" |> assertError (err "cvc2-logic") + solver.setInfo "cvc5-logic" "asdf" |> assertError (err "cvc5-logic") + + let test (key val : String) : Env Unit := solver.setInfo key val |> assertOk + + let v := "asdf" + test "source" v + test "category" v + test "difficulty" v + test "filename" v + test "license" v + test "name" v + test "notes" v + + test "smt-lib-version" "2" + -- -- following two tests output garbage to `stderr` + -- test "smt-lib-version" "2.0" + -- test "smt-lib-version" "2.5" + test "smt-lib-version" "2.6" + solver.setInfo "smt-lib-version" ".0" |> assertError + "invalid argument '.0' for 'value', expected '2.0', '2.5', '2.6', '2.7'" + + test "status" "sat" + test "status" "unsat" + test "status" "unknown" + solver.setInfo "status" "asdf" |> assertError + "invalid argument 'asdf' for 'value', expected 'sat', 'unsat' or 'unknown'" + +test![TestApiBlackSolver, setLogic] tm solver => do + solver.setLogic "AUFLIRA" + solver.setLogic "AF_BV" |> assertError "invalid call to 'setLogic', logic is already set" + tm.mkTrue >>= solver.assertFormula + solver.setLogic "AUFLIRA" |> assertError "invalid call to 'setLogic', logic is already set" + +test![TestApiBlackSolver, isLogicSet] tm solver => do + assertFalse (← solver.isLogicSet) + solver.setLogic "QF_BV" + assertTrue (← solver.isLogicSet) + +test![TestApiBlackSolver, getLogic] tm solver => do + solver.getLogic |> assertError "invalid call to 'getLogic', logic has not yet been set" + solver.setLogic "QF_BV" + assertEq "QF_BV" (← solver.getLogic) + +test![TestApiBlackSolver, setOption] tm solver => do + solver.setOption "bv-sat-solver" "cadical" |> assertOkDiscard + solver.setOption "bv-sat-solver" "1" |> assertError + "Error in option parsing: unknown option for --bv-sat-solver: `1'. Try --bv-sat-solver=help." + tm.mkTrue >>= solver.assertFormula + solver.setOption "bv-sat-solver" "cadical" |> assertError + "invalid call to 'setOption' for option 'bv-sat-solver', solver is already fully initialized" + +test![TestApiBlackSolver, resetAssertions] tm solver => do + solver.setOption "incremental" "true" |> assertOkDiscard + + let bvSort ← tm.mkBitVectorSort 4 + let one ← tm.mkBitVector 4 1 + let x ← tm.mkConst bvSort "x" + let ule ← tm.mkTerm Kind.BITVECTOR_ULE #[x, one] + let srem ← tm.mkTerm Kind.BITVECTOR_SREM #[one, x] + solver.push 4 + let slt ← tm.mkTerm Kind.BITVECTOR_SLT #[srem, one] + solver.resetAssertions + solver.checkSatAssuming #[slt, ule] |> assertOkDiscard test![TestApiBlackSolver, declareSygusVar] tm solver => do solver.setOption "sygus" "true" @@ -38,7 +1529,7 @@ test![TestApiBlackSolver, declareSygusVar] tm solver => do solver'.declareSygusVar "" bool |> assertError "Given sort is not associated with the term manager of this solver" -test![TestApiBlackSolver, declareSygusVar] tm solver => do +test![TestApiBlackSolver, mkGrammar] tm solver => do let nullTerm := Term.null () let boolTerm ← tm.mkBoolean true let boolVar ← tm.mkVar bool @@ -161,10 +1652,11 @@ test![TestApiBlackSolver, getSygusAssumptions] tm solver => do solver.addSygusAssume fls assertEq (← solver.getSygusAssumptions) #[tru, fls] -test![TestApiBlackSolver, getSygusAssumptions] tm solver => do +test![TestApiBlackSolver, addSygusInvConstraint] tm solver => do solver.setOption "sygus" "true" let nullTerm := Term.null () let intTerm ← tm.mkInteger 1 + let real ← tm.getRealSort let inv ← solver.declareFun "inv" #[real] bool let pre ← solver.declareFun "pre" #[real] bool @@ -348,3 +1840,257 @@ test![TestApiBlackSolver, findSynth2] tm solver => do let term ← solver.findSynthNext assertFalse term.isNull assertTrue (← term.getSort).isBoolean + +test![TestApiBlackSolver, tupleProject] tm solver => do + let elements := #[ + ← tm.mkBoolean true, ← tm.mkInteger 3, ← tm.mkString "C", + ← tm.mkTerm Kind.SET_SINGLETON #[← tm.mkString "Z"], + ] + + let tuple ← tm.mkTuple elements + + let indices1 := #[] + let indices2 := #[0] + let indices3 := #[0, 1] + let indices4 := #[0, 0, 2, 2, 3, 3, 0] + let indices5 := #[4] + let indices6 := #[0, 4] + + tm.mkTermOfOp (← tm.mkOp Kind.TUPLE_PROJECT indices1) #[tuple] |> assertOkDiscard + tm.mkTermOfOp (← tm.mkOp Kind.TUPLE_PROJECT indices2) #[tuple] |> assertOkDiscard + tm.mkTermOfOp (← tm.mkOp Kind.TUPLE_PROJECT indices3) #[tuple] |> assertOkDiscard + tm.mkTermOfOp (← tm.mkOp Kind.TUPLE_PROJECT indices4) #[tuple] |> assertOkDiscard + + tm.mkTermOfOp (← tm.mkOp Kind.TUPLE_PROJECT indices5) #[tuple] |> assertError + "Project index 4 in term \ + ((_ tuple.project 4) (tuple true 3 \"C\" (set.singleton \"Z\"))) is >= 4 \ + which is the length of tuple (tuple true 3 \"C\" (set.singleton \"Z\"))\n" + tm.mkTermOfOp (← tm.mkOp Kind.TUPLE_PROJECT indices6) #[tuple] |> assertError + "Project index 4 in term \ + ((_ tuple.project 0 4) (tuple true 3 \"C\" (set.singleton \"Z\"))) is >= 4 \ + which is the length of tuple (tuple true 3 \"C\" (set.singleton \"Z\"))\n" + + let indices := #[0, 3, 2, 0, 1, 2] + + let op ← tm.mkOp Kind.TUPLE_PROJECT indices + let projection ← tm.mkTermOfOp op #[tuple] + + let datatype ← (← tuple.getSort).getDatatype + let constructor := datatype[0]! + + for index in indices do + let selectorTerm ← constructor[index]!.getTerm + let selectedTerm ← tm.mkTerm Kind.APPLY_SELECTOR #[selectorTerm, tuple] + let simplifiedTerm ← solver.simplify selectedTerm + assertEq elements[index]! simplifiedTerm + + projection.toString + |> assertEq "((_ tuple.project 0 3 2 0 1 2) (tuple true 3 \"C\" (set.singleton \"Z\")))" + +-- test![TestApiBlackSolver, output] tm solver => do + +test![TestApiBlackSolver, getDatatypeArity] tm solver => do + let ctor1 ← tm.mkDatatypeConstructorDecl "_x21" + let ctor2 ← tm.mkDatatypeConstructorDecl "_x31" + let s3 ← solver.declareDatatype "_x17" #[ctor1, ctor2] + assertEq 0 (← s3.getDatatypeArity) + +test![TestApiBlackSolver, declareOracleFunError] tm solver => do + -- cannot declare without option + solver.declareOracleFun "f" #[int] int (fun _input => tm.mkInteger 0) |> assertError + "cannot call declareOracleFun unless oracles is enabled (use --oracles)" + solver.setOption "oracles" "true" + let nullSort := Sort.null () + -- -- bad sort + solver.declareOracleFun "f" #[nullSort] int (fun _input => tm.mkInteger 0) |> assertError + "invalid null domain sort in 'sorts' at index 0" + +test![TestApiBlackSolver, declareOracleFunUnsat] tm solver => do + solver.setOption "oracles" "true" + let oracle (terms : Array Term) : Env Term := do + if let some term := terms[0]? then + if let some val := term.getUInt32Value? then + return ← val.toNat.succ |> Int.ofNat |> tm.mkInteger + tm.mkInteger 0 + -- `f` is the function implementing `(lambda ((x Int)) (+ x 1))` + let f ← solver.declareOracleFun "f" #[int] int oracle + let three ← tm.mkInteger 3 + let five ← tm.mkInteger 5 + let eq ← tm.mkTerm Kind.EQUAL #[← tm.mkTerm Kind.APPLY_UF #[f, three], five] + solver.assertFormula eq + -- `(f 3) = 5` + assertTrue (← solver.checkSat).isUnsat + + let tm' ← TermManager.new + let solver' ← Solver.new tm' + solver'.setOption "oracles" "true" + let int' ← tm'.getIntegerSort + let oracle' (terms : Array Term) : Env Term := do + if let some term := terms[0]? then + if let some val := term.getUInt32Value? then + return ← val.toNat.succ |> Int.ofNat |> tm'.mkInteger + tm'.mkInteger 0 + solver'.declareOracleFun "f" #[int'] int oracle' |> assertError + "Given sort is not associated with the term manager of this solver" + solver'.declareOracleFun "f" #[int] int' oracle' |> assertError + "invalid domain sort in 'sorts' at index 0, \ + expected a sort associated with the term manager of this solver object" + + -- this cannot be caught during declaration, is caught during check-sat + let f2 ← solver'.declareOracleFun "f2" #[int'] int' oracle + let eq2 ← tm'.mkTerm Kind.EQUAL #[ + ← tm'.mkTerm Kind.APPLY_UF #[f2, ← tm'.mkInteger 3], ← tm'.mkInteger 5 + ] + solver'.assertFormula eq2 + solver'.checkSat |> assertError + "Evaluated an oracle call that is not associated with the term manager of this solver" + + -- added from the original test to check we're handling nested errors properly + let tm'' ← TermManager.new + let solver'' ← Solver.new tm'' + solver''.setOption "oracles" "true" + let int'' ← tm''.getIntegerSort + let f3 ← solver''.declareOracleFun "f3" #[int''] int'' + fun _ => throw (Error.error "internal failure") + let eq3 ← tm''.mkTerm Kind.EQUAL #[ + ← tm''.mkTerm Kind.APPLY_UF #[f3, ← tm''.mkInteger 3], ← tm''.mkInteger 5 + ] + solver''.assertFormula eq3 + solver''.checkSat |> assertError "internal failure" + +test![TestApiBlackSolver, declareOracleFunSat] tm solver => do + let int ← tm.getIntegerSort + solver.setOption "oracles" "true" + solver.setOption "produce-models" "true" + -- `f` is the function implementing `(lambda ((x Int)) (% x 10))` + let f ← solver.declareOracleFun "f" #[int] int fun terms => do + if let some term := terms[0]? then + if let some val := term.getUInt32Value? then + return ← tm.mkInteger (val.toNat % 10) + tm.mkInteger 0 + let seven ← tm.mkInteger 7 + let x ← tm.mkConst int "x" + let lb ← tm.mkTerm Kind.GEQ #[x, ← tm.mkInteger 0] + solver.assertFormula lb + let ub ← tm.mkTerm Kind.LEQ #[x, ← tm.mkInteger 100] + solver.assertFormula ub + let eq ← tm.mkTerm Kind.EQUAL #[← tm.mkTerm Kind.APPLY_UF #[f, x], seven] + solver.assertFormula eq + -- `x ≥ 0 ∧ x ≤ 100 ∧ (f x) = 7` + assertTrue (← solver.checkSat).isSat + let xval ← solver.getValue x + assertTrue xval.isUInt32Value + assertEq 7 (xval.getUInt32Value!.toNat % 10) + +test![TestApiBlackSolver, declareOracleFunSat2] tm solver => do + solver.setOption "oracles" "true" + solver.setOption "produce-models" "true" + -- `eq` is the function implementing `(lambda ((x Int) (y Int)) (= x y))` + let eq ← solver.declareOracleFun "eq" #[int, int] bool fun terms => do + if let some t1 := terms[0]? then + if let some t2 := terms[1]? then + return ← tm.mkBoolean (t1 == t2) + throw (Error.error "expected exactly two terms") + let x ← tm.mkConst int "x" + let y ← tm.mkConst int "y" + let neq ← tm.mkTerm Kind.NOT #[← tm.mkTerm Kind.APPLY_UF #[eq, x, y]] + solver.assertFormula neq + -- `(not (eq x y))` + assertTrue (← solver.checkSat).isSat + let xval ← solver.getValue x + let yval ← solver.getValue y + assertNe xval yval + +-- #TODO `Plugin`-related functions not implemented +-- test![TestApiBlackSolver, pluginUnsat] tm solver => do +-- test![TestApiBlackSolver, pluginListen] tm solver => do +-- test![TestApiBlackSolver, pluginListenCadical] tm solver => do + +test![TestApiBlackSolver, verticalBars] tm solver => do + let a ← solver.declareFun "|a |" #[] real + assertEq "|a |" a.toString + +test![TestApiBlackSolver, getVersion] tm solver => do + solver.getVersion |> assertOkDiscard + +test![TestApiBlackSolver, multipleSolvers] tm _solver => do + let (value1, zero, definedFunction) ← do + let s1 ← Solver.new tm + s1.setLogic "ALL" + s1.setOption "produce-models" "true" + let f1 ← s1.declareFun "f1" #[] int + let x ← tm.mkVar int "x" + let zero ← tm.mkInteger 0 + let definedFunction ← s1.defineFun "f" #[ x ] int zero + f1.eqTerm zero >>= s1.assertFormula + s1.checkSat |> assertOkDiscard + let value1 ← s1.getValue f1 + pure (value1, zero, definedFunction) + assertEq zero value1 + let value2 ← do + let s2 ← Solver.new tm + s2.setLogic "ALL" + s2.setOption "produce-models" "true" + let f2 ← s2.declareFun "f2" #[] int + f2.eqTerm value1 >>= s2.assertFormula + s2.checkSat |> assertOkDiscard + s2.getValue f2 + assertEq value1 value2 + let value3 ← do + let s3 ← Solver.new tm + s3.setLogic "ALL" + s3.setOption "produce-models" "true" + let f3 ← s3.declareFun "f3" #[] int + let apply ← tm.mkTerm Kind.APPLY_UF #[definedFunction, zero] + f3.eqTerm apply >>= s3.assertFormula + s3.checkSat |> assertOkDiscard + s3.getValue f3 + assertEq value1 value3 + +test![TestApiBlackSolver, basicFiniteField] tm solver => do + solver.setOption "produce-models" "true" + + let F ← tm.mkFiniteFieldSort 5 + let a ← tm.mkConst F "a" + let b ← tm.mkConst F "b" + assertEq 5 F.getFiniteFieldSize! + + let inv ← tm.mkTerm Kind.EQUAL + #[← tm.mkTerm Kind.FINITE_FIELD_MULT #[a, b], ← tm.mkFiniteFieldElem 1 F] + let aIsTwo ← tm.mkTerm Kind.EQUAL #[a, ← tm.mkFiniteFieldElem 2 F] + + solver.assertFormula inv + solver.assertFormula aIsTwo + -- -- #TODO requires a cvc5 dyn-lib with *cocoa* linked + -- assertTrue (← solver.checkSat).isSat + -- assertEq 2 (← solver.getValue a).getFiniteFieldValue! + -- assertEq (-2) (← solver.getValue b).getFiniteFieldValue! + + let bIsTwo ← tm.mkTerm Kind.EQUAL #[b, ← tm.mkFiniteFieldElem 2 F] + solver.assertFormula bIsTwo + -- -- #TODO requires a cvc5 dyn-lib with *cocoa* linked + -- assertFalse (← solver.checkSat).isSat + +test![TestApiBlackSolver, basicFiniteField] tm solver => do + solver.setOption "produce-models" "true" + + let F ← tm.mkFiniteFieldSortOfString "101" 2 + let a ← tm.mkConst F "a" + let b ← tm.mkConst F "b" + assertEq 5 F.getFiniteFieldSize! + + let inv ← tm.mkTerm Kind.EQUAL + #[← tm.mkTerm Kind.FINITE_FIELD_MULT #[a, b], ← tm.mkFiniteFieldElemOfString "1" F 3] + let aIsTwo ← tm.mkTerm Kind.EQUAL #[a, ← tm.mkFiniteFieldElemOfString "10" F 2] + + solver.assertFormula inv + solver.assertFormula aIsTwo + -- -- #TODO requires a cvc5 dyn-lib with *cocoa* linked + -- assertTrue (← solver.checkSat).isSat + -- assertEq 2 (← solver.getValue a).getFiniteFieldValue! + -- assertEq (-2) (← solver.getValue b).getFiniteFieldValue! + + let bIsTwo ← tm.mkTerm Kind.EQUAL #[b, ← tm.mkFiniteFieldElemOfString "2" F] + solver.assertFormula bIsTwo + -- -- #TODO requires a cvc5 dyn-lib with *cocoa* linked + -- assertFalse (← solver.checkSat).isSat diff --git a/ffi/ffi.cpp b/ffi/ffi.cpp index b4b4b4a..b1cc02e 100644 --- a/ffi/ffi.cpp +++ b/ffi/ffi.cpp @@ -3481,6 +3481,17 @@ LEAN_EXPORT lean_obj_res solver_resetAssertions(lean_obj_arg solver) CVC5_LEAN_API_TRY_CATCH_ENV_END; } +LEAN_EXPORT lean_obj_res solver_setInfo(lean_obj_arg solver, + lean_obj_arg keyword, + lean_obj_arg value) +{ + CVC5_LEAN_API_TRY_CATCH_ENV_BEGIN; + solver_unbox(solver)->setInfo(lean_string_cstr(keyword), + lean_string_cstr(value)); + return env_val(mk_unit_unit()); + CVC5_LEAN_API_TRY_CATCH_ENV_END; +} + LEAN_EXPORT lean_obj_res solver_setLogic(lean_obj_arg solver, lean_object* logic) { @@ -3565,6 +3576,196 @@ LEAN_EXPORT lean_obj_res solver_checkSatAssuming(lean_obj_arg solver, CVC5_LEAN_API_TRY_CATCH_ENV_END; } +LEAN_EXPORT lean_obj_res solver_declareDatatype(lean_obj_arg solver, + lean_obj_arg symbol, + lean_obj_arg ctors) +{ + CVC5_LEAN_API_TRY_CATCH_ENV_BEGIN; + std::vector ctorVec; + for (size_t i = 0, n = lean_array_size(ctors); i < n; ++i) + { + ctorVec.push_back(*datatypeConstructorDecl_unbox(lean_array_get( + datatypeConstructorDecl_box(new DatatypeConstructorDecl()), + ctors, + lean_usize_to_nat(i)))); + } + return env_val(sort_box(new Sort(solver_unbox(solver)->declareDatatype( + lean_string_cstr(symbol), ctorVec)))); + CVC5_LEAN_API_TRY_CATCH_ENV_END; +} + +LEAN_EXPORT lean_obj_res solver_declareSort(lean_obj_arg solver, + lean_obj_arg symbol, + uint32_t arity, + uint8_t fresh) +{ + CVC5_LEAN_API_TRY_CATCH_ENV_BEGIN; + return env_val(sort_box(new Sort(solver_unbox(solver)->declareSort( + lean_string_cstr(symbol), arity, bool_unbox(fresh))))); + CVC5_LEAN_API_TRY_CATCH_ENV_END; +} + +LEAN_EXPORT lean_obj_res solver_defineFun(lean_obj_arg solver, + lean_obj_arg symbol, + lean_obj_arg boundVars, + lean_obj_arg sort, + lean_obj_arg body, + uint8_t global) +{ + CVC5_LEAN_API_TRY_CATCH_ENV_BEGIN; + std::vector boundVarVec; + for (size_t i = 0, n = lean_array_size(boundVars); i < n; ++i) + { + boundVarVec.push_back(*term_unbox( + lean_array_get(term_box(new Term()), boundVars, lean_usize_to_nat(i)))); + } + Term term = solver_unbox(solver)->defineFun(lean_string_cstr(symbol), + boundVarVec, + *sort_unbox(sort), + *term_unbox(body), + bool_unbox(global)); + return env_val(term_box(new Term(term))); + CVC5_LEAN_API_TRY_CATCH_ENV_END; +} + +LEAN_EXPORT lean_obj_res solver_defineFunRec(lean_obj_arg solver, + lean_obj_arg symbol, + lean_obj_arg boundVars, + lean_obj_arg sort, + lean_obj_arg body, + uint8_t global) +{ + CVC5_LEAN_API_TRY_CATCH_ENV_BEGIN; + std::vector boundVarVec; + for (size_t i = 0, n = lean_array_size(boundVars); i < n; ++i) + { + boundVarVec.push_back(*term_unbox( + lean_array_get(term_box(new Term()), boundVars, lean_usize_to_nat(i)))); + } + Term term = solver_unbox(solver)->defineFunRec(lean_string_cstr(symbol), + boundVarVec, + *sort_unbox(sort), + *term_unbox(body), + bool_unbox(global)); + return env_val(term_box(new Term(term))); + CVC5_LEAN_API_TRY_CATCH_ENV_END; +} + +LEAN_EXPORT lean_obj_res solver_defineFunRecTerm(lean_obj_arg solver, + lean_obj_arg fun, + lean_obj_arg boundVars, + lean_obj_arg body, + uint8_t global) +{ + CVC5_LEAN_API_TRY_CATCH_ENV_BEGIN; + std::vector boundVarVec; + for (size_t i = 0, n = lean_array_size(boundVars); i < n; ++i) + { + boundVarVec.push_back(*term_unbox( + lean_array_get(term_box(new Term()), boundVars, lean_usize_to_nat(i)))); + } + Term term = solver_unbox(solver)->defineFunRec( + *term_unbox(fun), boundVarVec, *term_unbox(body), bool_unbox(global)); + return env_val(term_box(new Term(term))); + CVC5_LEAN_API_TRY_CATCH_ENV_END; +} + +LEAN_EXPORT lean_obj_res solver_defineFunsRec(lean_obj_arg solver, + lean_obj_arg funs, + lean_obj_arg boundVars, + lean_obj_arg bodies, + uint8_t global) +{ + CVC5_LEAN_API_TRY_CATCH_ENV_BEGIN; + std::vector funVec; + for (size_t i = 0, n = lean_array_size(funs); i < n; ++i) + { + funVec.push_back(*term_unbox( + lean_array_get(term_box(new Term()), funs, lean_usize_to_nat(i)))); + } + std::vector> boundVarVecVec; + for (size_t i = 0, n = lean_array_size(boundVars); i < n; ++i) + { + std::vector boundVarVec; + lean_obj_res boundVarArray = + lean_array_get(lean_mk_empty_array(), boundVars, lean_usize_to_nat(i)); + for (size_t j = 0, n = lean_array_size(boundVarArray); j < n; ++j) + { + boundVarVec.push_back(*term_unbox(lean_array_get( + term_box(new Term()), boundVarArray, lean_usize_to_nat(j)))); + } + boundVarVecVec.push_back(boundVarVec); + } + std::vector bodyVec; + for (size_t i = 0, n = lean_array_size(bodies); i < n; ++i) + { + bodyVec.push_back(*term_unbox( + lean_array_get(term_box(new Term()), bodies, lean_usize_to_nat(i)))); + } + solver_unbox(solver)->defineFunsRec( + funVec, boundVarVecVec, bodyVec, bool_unbox(global)); + return env_val(mk_unit_unit()); + CVC5_LEAN_API_TRY_CATCH_ENV_END; +} + +LEAN_EXPORT lean_obj_res solver_getAssertions(lean_obj_arg solver) +{ + CVC5_LEAN_API_TRY_CATCH_ENV_BEGIN; + std::vector assertionVec = solver_unbox(solver)->getAssertions(); + lean_object* assertions = lean_mk_empty_array(); + for (const Term& assertion : assertionVec) + { + assertions = lean_array_push(assertions, term_box(new Term(assertion))); + } + return env_val(assertions); + CVC5_LEAN_API_TRY_CATCH_ENV_END; +} + +LEAN_EXPORT lean_obj_res solver_getInfo(lean_obj_arg solver, lean_obj_arg flag) +{ + CVC5_LEAN_API_TRY_CATCH_ENV_BEGIN; + return env_val(lean_mk_string( + solver_unbox(solver)->getInfo(lean_string_cstr(flag)).c_str())); + CVC5_LEAN_API_TRY_CATCH_ENV_END; +} + +LEAN_EXPORT lean_obj_res solver_getOption(lean_obj_arg solver, + lean_obj_arg option) +{ + CVC5_LEAN_API_TRY_CATCH_ENV_BEGIN; + return env_val(lean_mk_string( + solver_unbox(solver)->getOption(lean_string_cstr(option)).c_str())); + CVC5_LEAN_API_TRY_CATCH_ENV_END; +} + +LEAN_EXPORT lean_obj_res solver_getOptionNames(lean_obj_arg solver) +{ + CVC5_LEAN_API_TRY_CATCH_ENV_BEGIN; + std::vector optionNameVec = + solver_unbox(solver)->getOptionNames(); + lean_object* optionNames = lean_mk_empty_array(); + for (const std::string& optionName : optionNameVec) + { + optionNames = + lean_array_push(optionNames, lean_mk_string(optionName.c_str())); + } + return env_val(optionNames); + CVC5_LEAN_API_TRY_CATCH_ENV_END; +} + +LEAN_EXPORT lean_obj_res solver_getUnsatAssumptions(lean_obj_arg solver) +{ + CVC5_LEAN_API_TRY_CATCH_ENV_BEGIN; + std::vector assertions = solver_unbox(solver)->getUnsatAssumptions(); + lean_object* as = lean_mk_empty_array(); + for (const Term& assertion : assertions) + { + as = lean_array_push(as, term_box(new Term(assertion))); + } + return env_val(as); + CVC5_LEAN_API_TRY_CATCH_ENV_END; +} + LEAN_EXPORT lean_obj_res solver_getUnsatCore(lean_obj_arg solver) { CVC5_LEAN_API_TRY_CATCH_ENV_BEGIN; @@ -3578,10 +3779,61 @@ LEAN_EXPORT lean_obj_res solver_getUnsatCore(lean_obj_arg solver) CVC5_LEAN_API_TRY_CATCH_ENV_END; } -LEAN_EXPORT lean_obj_res solver_getProof(lean_obj_arg solver) +LEAN_EXPORT lean_obj_res solver_getUnsatCoreLemmas(lean_obj_arg solver) { CVC5_LEAN_API_TRY_CATCH_ENV_BEGIN; - std::vector proofs = solver_unbox(solver)->getProof(); + std::vector assertions = solver_unbox(solver)->getUnsatCoreLemmas(); + lean_object* as = lean_mk_empty_array(); + for (const Term& assertion : assertions) + { + as = lean_array_push(as, term_box(new Term(assertion))); + } + return env_val(as); + CVC5_LEAN_API_TRY_CATCH_ENV_END; +} + +LEAN_EXPORT lean_obj_res solver_getTimeoutCore(lean_obj_arg solver) +{ + CVC5_LEAN_API_TRY_CATCH_ENV_BEGIN; + std::pair> pair = + solver_unbox(solver)->getTimeoutCore(); + std::vector termVec = std::get<1>(pair); + lean_object* terms = lean_mk_empty_array(); + for (const Term& term : termVec) + { + terms = lean_array_push(terms, term_box(new Term(term))); + } + return env_val(prod_mk(result_box(new Result(std::get<0>(pair))), terms)); + CVC5_LEAN_API_TRY_CATCH_ENV_END; +} + +LEAN_EXPORT lean_obj_res solver_getTimeoutCoreAssuming(lean_obj_arg solver, + lean_obj_arg assumptions) +{ + CVC5_LEAN_API_TRY_CATCH_ENV_BEGIN; + std::vector formulas; + for (size_t i = 0, n = lean_array_size(assumptions); i < n; ++i) + { + formulas.push_back(*term_unbox(lean_array_get( + term_box(new Term()), assumptions, lean_usize_to_nat(i)))); + } + std::pair> pair = + solver_unbox(solver)->getTimeoutCoreAssuming(formulas); + std::vector termVec = std::get<1>(pair); + lean_object* terms = lean_mk_empty_array(); + for (const Term& term : termVec) + { + terms = lean_array_push(terms, term_box(new Term(term))); + } + return env_val(prod_mk(result_box(new Result(std::get<0>(pair))), terms)); + CVC5_LEAN_API_TRY_CATCH_ENV_END; +} + +LEAN_EXPORT lean_obj_res solver_getProof(lean_obj_arg solver, uint8_t pc) +{ + CVC5_LEAN_API_TRY_CATCH_ENV_BEGIN; + std::vector proofs = solver_unbox(solver)->getProof( + static_cast(pc)); lean_object* ps = lean_mk_empty_array(); for (const Proof& proof : proofs) { @@ -3634,12 +3886,272 @@ LEAN_EXPORT lean_obj_res solver_getModelDomainElements(lean_obj_arg solver, CVC5_LEAN_API_TRY_CATCH_ENV_END; } +LEAN_EXPORT lean_obj_res solver_isModelCoreSymbol(lean_obj_arg solver, + lean_obj_arg v) +{ + CVC5_LEAN_API_TRY_CATCH_ENV_BEGIN; + return env_bool(solver_unbox(solver)->isModelCoreSymbol(*term_unbox(v))); + CVC5_LEAN_API_TRY_CATCH_ENV_END; +} + +LEAN_EXPORT lean_obj_res solver_getModel(lean_obj_arg solver, + lean_obj_arg sorts, + lean_obj_arg consts) +{ + CVC5_LEAN_API_TRY_CATCH_ENV_BEGIN; + std::vector sortVec; + for (size_t i = 0, n = lean_array_size(sorts); i < n; ++i) + { + sortVec.push_back( + *sort_unbox(lean_array_fget(sorts, lean_usize_to_nat(i)))); + } + std::vector constVec; + for (size_t i = 0, n = lean_array_size(consts); i < n; ++i) + { + constVec.push_back(*term_unbox( + lean_array_get(term_box(new Term()), consts, lean_usize_to_nat(i)))); + } + return env_val(lean_mk_string( + solver_unbox(solver)->getModel(sortVec, constVec).c_str())); + CVC5_LEAN_API_TRY_CATCH_ENV_END; +} + +LEAN_EXPORT lean_obj_res solver_getQuantifierElimination(lean_obj_arg solver, + lean_obj_arg term) +{ + CVC5_LEAN_API_TRY_CATCH_ENV_BEGIN; + return env_val(term_box(new Term( + solver_unbox(solver)->getQuantifierElimination(*term_unbox(term))))); + CVC5_LEAN_API_TRY_CATCH_ENV_END; +} + +LEAN_EXPORT lean_obj_res +solver_getQuantifierEliminationDisjunct(lean_obj_arg solver, lean_obj_arg term) +{ + CVC5_LEAN_API_TRY_CATCH_ENV_BEGIN; + return env_val( + term_box(new Term(solver_unbox(solver)->getQuantifierEliminationDisjunct( + *term_unbox(term))))); + CVC5_LEAN_API_TRY_CATCH_ENV_END; +} + +LEAN_EXPORT lean_obj_res solver_declareSepHeap(lean_obj_arg solver, + lean_obj_arg locSort, + lean_obj_arg dataSort) +{ + CVC5_LEAN_API_TRY_CATCH_ENV_BEGIN; + solver_unbox(solver)->declareSepHeap(*sort_unbox(locSort), + *sort_unbox(dataSort)); + return env_val(mk_unit_unit()); + CVC5_LEAN_API_TRY_CATCH_ENV_END; +} + +LEAN_EXPORT lean_obj_res solver_getValueSepHeap(lean_obj_arg solver) +{ + CVC5_LEAN_API_TRY_CATCH_ENV_BEGIN; + return env_val(term_box(new Term(solver_unbox(solver)->getValueSepHeap()))); + CVC5_LEAN_API_TRY_CATCH_ENV_END; +} + +LEAN_EXPORT lean_obj_res solver_getValueSepNil(lean_obj_arg solver) +{ + CVC5_LEAN_API_TRY_CATCH_ENV_BEGIN; + return env_val(term_box(new Term(solver_unbox(solver)->getValueSepNil()))); + CVC5_LEAN_API_TRY_CATCH_ENV_END; +} + +LEAN_EXPORT lean_obj_res solver_push(lean_obj_arg solver, uint32_t nscopes) +{ + CVC5_LEAN_API_TRY_CATCH_ENV_BEGIN; + solver_unbox(solver)->push(nscopes); + return env_val(mk_unit_unit()); + CVC5_LEAN_API_TRY_CATCH_ENV_END; +} + +LEAN_EXPORT lean_obj_res solver_declarePool(lean_obj_arg solver, + lean_obj_arg symbol, + lean_obj_arg sort, + lean_obj_arg initValue) +{ + CVC5_LEAN_API_TRY_CATCH_ENV_BEGIN; + std::vector initValueVec; + for (size_t i = 0, n = lean_array_size(initValue); i < n; ++i) + { + initValueVec.push_back(*term_unbox( + lean_array_get(term_box(new Term()), initValue, lean_usize_to_nat(i)))); + } + return env_val(term_box(new Term(solver_unbox(solver)->declarePool( + lean_string_cstr(symbol), *sort_unbox(sort), initValueVec)))); + CVC5_LEAN_API_TRY_CATCH_ENV_END; +} + +LEAN_EXPORT lean_obj_res solver_declareOracleFun(lean_obj_arg solver, + lean_obj_arg symbol, + lean_obj_arg sorts, + lean_obj_arg sort, + lean_obj_arg fn) +{ + CVC5_LEAN_API_TRY_CATCH_ENV_BEGIN; + std::vector sortVec; + for (size_t i = 0, n = lean_array_size(sorts); i < n; ++i) + { + sortVec.push_back( + *sort_unbox(lean_array_fget(sorts, lean_usize_to_nat(i)))); + } + std::function&)> fun = + [fn](const std::vector& termVec) { + lean_object* terms = lean_mk_empty_array(); + for (const Term& elem : termVec) + { + terms = lean_array_push(terms, term_box(new Term(elem))); + } + // increment `fn`'s ref count as `lean_apply_2` decrements it + lean_inc(fn); + lean_object* except = lean_apply_2(fn, terms, lean_box(0)); + if (lean_obj_tag(except) == 1) + { + lean_object* term = lean_ctor_get(except, 0); + Term t = *term_unbox(term); + lean_dec_ref(except); + return t; + } + else if (lean_obj_tag(except) == 0) + { + lean_object* error = lean_ctor_get(except, 0); + lean_inc(error); + lean_dec_ref(except); + throw error; + } + else + { + throw std::string( + "unexpected lean-obj-tag in 'Solver.declareOracleFun'"); + } + }; + Term t = solver_unbox(solver)->declareOracleFun( + lean_string_cstr(symbol), sortVec, *sort_unbox(sort), fun); + return env_val(term_box(new Term(t))); + CVC5_LEAN_API_TRY_CATCH_ENV_END; +} + +LEAN_EXPORT lean_obj_res solver_pop(lean_obj_arg solver, uint32_t nscopes) +{ + CVC5_LEAN_API_TRY_CATCH_ENV_BEGIN; + solver_unbox(solver)->pop(nscopes); + return env_val(mk_unit_unit()); + CVC5_LEAN_API_TRY_CATCH_ENV_END; +} + +LEAN_EXPORT lean_obj_res solver_getInterpolantSimple(lean_obj_arg solver, + lean_obj_arg conj) +{ + CVC5_LEAN_API_TRY_CATCH_ENV_BEGIN; + return env_val(term_box( + new Term(solver_unbox(solver)->getInterpolant(*term_unbox(conj))))); + CVC5_LEAN_API_TRY_CATCH_ENV_END; +} + +LEAN_EXPORT lean_obj_res solver_getInterpolantOfGrammar(lean_obj_arg solver, + lean_obj_arg conj, + lean_obj_arg grammar) +{ + CVC5_LEAN_API_TRY_CATCH_ENV_BEGIN; + return env_val(term_box(new Term(solver_unbox(solver)->getInterpolant( + *term_unbox(conj), *mut_grammar_unbox(grammar))))); + CVC5_LEAN_API_TRY_CATCH_ENV_END; +} + +LEAN_EXPORT lean_obj_res solver_getInterpolantNext(lean_obj_arg solver) +{ + CVC5_LEAN_API_TRY_CATCH_ENV_BEGIN; + return env_val( + term_box(new Term(solver_unbox(solver)->getInterpolantNext()))); + CVC5_LEAN_API_TRY_CATCH_ENV_END; +} + +LEAN_EXPORT lean_obj_res solver_getAbductSimple(lean_obj_arg solver, + lean_obj_arg conj) +{ + CVC5_LEAN_API_TRY_CATCH_ENV_BEGIN; + return env_val( + term_box(new Term(solver_unbox(solver)->getAbduct(*term_unbox(conj))))); + CVC5_LEAN_API_TRY_CATCH_ENV_END; +} + +LEAN_EXPORT lean_obj_res solver_getAbductOfGrammar(lean_obj_arg solver, + lean_obj_arg conj, + lean_obj_arg grammar) +{ + CVC5_LEAN_API_TRY_CATCH_ENV_BEGIN; + return env_val(term_box(new Term(solver_unbox(solver)->getAbduct( + *term_unbox(conj), *mut_grammar_unbox(grammar))))); + CVC5_LEAN_API_TRY_CATCH_ENV_END; +} + +LEAN_EXPORT lean_obj_res solver_getAbductNext(lean_obj_arg solver) +{ + CVC5_LEAN_API_TRY_CATCH_ENV_BEGIN; + return env_val(term_box(new Term(solver_unbox(solver)->getAbductNext()))); + CVC5_LEAN_API_TRY_CATCH_ENV_END; +} + +LEAN_EXPORT lean_obj_res solver_blockModel(lean_obj_arg solver, uint8_t mode) +{ + CVC5_LEAN_API_TRY_CATCH_ENV_BEGIN; + solver_unbox(solver)->blockModel( + static_cast(mode)); + return env_val(mk_unit_unit()); + CVC5_LEAN_API_TRY_CATCH_ENV_END; +} + +LEAN_EXPORT lean_obj_res solver_blockModelValues(lean_obj_arg solver, + lean_obj_arg terms) +{ + CVC5_LEAN_API_TRY_CATCH_ENV_BEGIN; + std::vector termVec; + for (size_t i = 0, n = lean_array_size(terms); i < n; ++i) + { + termVec.push_back(*term_unbox( + lean_array_get(term_box(new Term()), terms, lean_usize_to_nat(i)))); + } + solver_unbox(solver)->blockModelValues(termVec); + return env_val(mk_unit_unit()); + CVC5_LEAN_API_TRY_CATCH_ENV_END; +} + +LEAN_EXPORT lean_obj_res solver_getInstantiations(lean_obj_arg solver) +{ + CVC5_LEAN_API_TRY_CATCH_ENV_BEGIN; + return env_val( + lean_mk_string(solver_unbox(solver)->getInstantiations().c_str())); + CVC5_LEAN_API_TRY_CATCH_ENV_END; +} + LEAN_EXPORT lean_obj_res solver_proofToString(lean_obj_arg solver, - lean_obj_arg proof) + lean_obj_arg proof, + uint8_t pf) { CVC5_LEAN_API_TRY_CATCH_ENV_BEGIN; return env_val(lean_mk_string( - solver_unbox(solver)->proofToString(*proof_unbox(proof)).c_str())); + solver_unbox(solver) + ->proofToString(*proof_unbox(proof), + static_cast(pf)) + .c_str())); + CVC5_LEAN_API_TRY_CATCH_ENV_END; +} + +LEAN_EXPORT lean_obj_res solver_getLearnedLiterals(lean_obj_arg solver, + uint8_t llt) +{ + CVC5_LEAN_API_TRY_CATCH_ENV_BEGIN; + std::vector termVec = solver_unbox(solver)->getLearnedLiterals( + static_cast(llt)); + lean_object* terms = lean_mk_empty_array(); + for (const Term& term : termVec) + { + terms = lean_array_push(terms, term_box(new Term(term))); + } + return env_val(terms); CVC5_LEAN_API_TRY_CATCH_ENV_END; }