| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-05-28 | Formattingdedup_lang | Andres Noetzli | |
| 2018-05-28 | Track input language in a single place | Andres Noetzli | |
| Currently, we store and update the input language in two places: the Input object and the options. The language stored in the Input object was only really used for SMT2 inputs. Storing the input language in two places means that we have to update the language in two places, which duplicates code (e.g. [0] and [1]). This removes the duplicate code and changes the code to track the input language in the options only. This commit is preparation for fixing #1969. [0] https://github.com/CVC4/CVC4/blob/74c1ad7e4a8e93316b7555ac8a1b88ee777335e2/src/smt/smt_engine.cpp#L2359-L2381 [1] https://github.com/CVC4/CVC4/blob/74c1ad7e4a8e93316b7555ac8a1b88ee777335e2/src/parser/smt2/Smt2.g#L1131-L1146 | |||
| 2018-05-28 | Builtin evaluation functions for sygus (#1991) | Andrew Reynolds | |
| 2018-05-27 | Fix cegqi assertions for quantified non-linear cases. (#1999) | Andrew Reynolds | |
| 2018-05-27 | Fix no-cbqi-innermost option name in run script (#1994) | Andres Noetzli | |
| 2018-05-26 | Update SymFPU. (#1992) | Mathias Preiner | |
| 2018-05-25 | Reenable repair const (#1983) | Andrew Reynolds | |
| 2018-05-25 | MiniSat: Be more careful about running proof code (#1982) | Andres Noetzli | |
| In `addClause_()`, we were checking the condition `ca[confl].size() == 1` regardless if proofs were enabled or not, even though both branches of the if statement only do something when proofs are enabled. This lead to issue #1978 occurring even when not generating proofs. Note: This commit is *not* a fix for #1978 but it makes sure that the issue does not occur when not generating proofs/unsat cores. | |||
| 2018-05-25 | Add QF_BV configuration for SMTCOMP'18. (#1981) | Mathias Preiner | |
| 2018-05-25 | Fix various nl assertions. (#1980) | Andrew Reynolds | |
| 2018-05-24 | Fix (#1979) | Andrew Reynolds | |
| 2018-05-24 | Improve simple constant symmetry breaking for sygus (#1977) | Andrew Reynolds | |
| 2018-05-24 | Fix compiler warnings (#1959) | Andres Noetzli | |
| 2018-05-24 | Fix (#1975) | Andrew Reynolds | |
| 2018-05-24 | Fixes for non-linear check model (#1974) | Andrew Reynolds | |
| 2018-05-24 | Fix nl regression for unsat cores. (#1973) | Andrew Reynolds | |
| 2018-05-23 | Remove spurious assertion in nonlinear extension (#1972) | Andrew Reynolds | |
| 2018-05-23 | Towards better symbolic enumeration in SyGuS (#1971) | Haniel Barbosa | |
| 2018-05-23 | Add notions of evaluated kinds in TheoryModel (#1947) | Andrew Reynolds | |
| 2018-05-23 | Remove ProofProxy (#1965) | Andres Noetzli | |
| 2018-05-23 | Generalize check-model in NonLinearExtension for quadratic equations (#1892) | Andrew Reynolds | |
| 2018-05-22 | Set same options for proofs as for unsat cores (#1957) | Andres Noetzli | |
| In SmtEngine::setDefaults() we were setting options such as --simplifciation=none for unsat cores but not proofs. Producing unsat cores relies on the same infrastructure as proofs and should be a subset of the same work in most cases. Thus, this commit changes SmtEngine::setDefaults() to set the same options for proofs as we previously only did for unsat cores. Additionally, it changes the function to only set the simplificationMode to SIMPLIFICATION_MODE_BATCH if proofs and unsat cores are not enabled. Fixes issue #1953. | |||
| 2018-05-22 | Repair constants using symbolic constructors (#1960) | Andrew Reynolds | |
| 2018-05-22 | Parse error for sygus grammar term with multiple let bodies (#1961) | Andrew Reynolds | |
| 2018-05-22 | Disable symmetry breaker for unsat cores (#1958) | Andres Noetzli | |
| Currently, --check-unsat-cores fails for one of our regressions. It turns out that the issue is due to preprocessing done by the symmetry breaker. The symmetry breaker does not add dependencies and thus the generated unsat core is incomplete/wrong. This commit disables the symmetry breaker when we are generating unsat cores (it was previously only disabled when generating proofs). Fixes issue #1953. | |||
| 2018-05-22 | Make sygus infer find function definitions (#1951) | Andrew Reynolds | |
| 2018-05-21 | Infrastructure for strings strategies (#1883) | Andrew Reynolds | |
| 2018-05-21 | Add SymFPU licensing information. (#1952) | Mathias Preiner | |
| 2018-05-21 | Improvements in parsing and printing related to mixed int/real (#1879) | Andrew Reynolds | |
| This eliminates some hacks for dealing with Int/Real. - Eliminates the use of "to_real" to cast decimals like "2.0" that happen to be Int. We now replace these by (/ 2 1) instead of (to_real 2), which has the advantage of being smt-lib compliant for all theories, including QF_LRA. - Eliminates the use of a hack to use "type ascriptions" when returning values from a get-value command. Instead, we use division with 1 when necessary. This affects the output of a few regressions, but we remain smt-lib compliant. - Addresses a bug with printing arbitrary type ascriptions for smt2 terms. This partially addresses #1852. - Updates our printing of negative rationals to be (/ (- n) m) instead of (- (/ n m)), which is consistent with the smt lib standard for real values (http://smtlib.cs.uiowa.edu/theories-Reals.shtml). | |||
| 2018-05-21 | Infrastructure to mark unused sygus strategies (#1950) | Andrew Reynolds | |
| 2018-05-21 | Handle IMPLIES in bool-to-bv and test it in regress0 (#1929) | makaimann | |
| 2018-05-21 | Refactor sygus eval unfold (#1946) | Andrew Reynolds | |
| 2018-05-21 | Remove Eclipse project files (#1928) | Andres Noetzli | |
| No one of the core devs is currently using Eclipse, so the Eclipse project files are essentially useless since they are not guaranteed to be up-to-date. | |||
| 2018-05-21 | Fix compiler warning in hashsmt example (#1927) | Andres Noetzli | |
| Previously, we were using delete for an array allocated on the heap, which caused a warning. @dddejan fixed this and other issues in PR #1909 but after @ajreynol fixed the other issues in a separate PR and to not waste @dddejan's time, I am submitting this fix separately (note: the fix is slightly different in that it changes the array to a vector, making a delete[] unnecessary). | |||
| 2018-05-21 | Assign weight 1 for Boolean variables in SyGuS default grammars (#1948) | Haniel Barbosa | |
| 2018-05-21 | Fix file extension (#1919) | Caleb Donovick | |
| * Fix file extension * Update Makefile | |||
| 2018-05-18 | changing default (#1944) | Haniel Barbosa | |
| 2018-05-18 | Cache isInterpretedFinite (#1943) | Andrew Reynolds | |
| 2018-05-18 | Cegis unif defaults to cegis when no unif (#1942) | Andrew Reynolds | |
| 2018-05-18 | Unified fairness scheme for cegis unif (#1941) | Andrew Reynolds | |
| 2018-05-17 | Catch type errors in sygus grammars for lambda (define-fun) constructors (#1937) | Andrew Reynolds | |
| 2018-05-17 | Fix debugPrint and add regress. (#1934) | Andrew Reynolds | |
| 2018-05-17 | Option to force return values of Bool functions to be constant in CegisUnif ↵ | Haniel Barbosa | |
| (#1930) | |||
| 2018-05-17 | Cegis-specific infrastructure (#1933) | Andrew Reynolds | |
| 2018-05-17 | Internal propagation for refinement lemmas (#1932) | Andrew Reynolds | |
| 2018-05-16 | Improve the separation resolution scheme in cegis unif (#1931) | Andrew Reynolds | |
| 2018-05-15 | Refactor static learning preprocessing pass (#1857) | yoni206 | |
| 2018-05-15 | Refactoring get enumerator values in construct candidate for cegis unif (#1926) | Andrew Reynolds | |
| 2018-05-15 | adding regressions (#1925) | Haniel Barbosa | |
| 2018-05-15 | Building and refining solutions with dynamic condition generation in ↵ | Haniel Barbosa | |
| CegisUnif (#1920) | |||
 |
index : cvc5.git | |
| CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. | git repository hosting |
| summaryrefslogtreecommitdiff |
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback