summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-03-22Fix stripConstantEndpoints in strings rewriter (#2883)Andres Noetzli
`TheoryStringsRewriter::stripConstantEndpoints()` returns the stripped endpoints in the vectors `nb` and `ne`. These endpoints were not computed correctly if string literal had to be split. For example: ``` stripConstantEndpoints({ "ABC" }, { "C" }, {}, {}, 1) ``` returned `true` and only "A" for `nb` (instead of "AB") because we mistakenly used the amount of overlap between "ABC" and "C" (which is one) for the length of the stripped prefix. This commit fixes the issue and adds several unit tests.
2019-03-22Use empty vector instead of false in query with null Expr assumption (#2876)makaimann
This solution is less confusing than using a `false` assumption.
2019-03-21 Fix bad comparison in RE solver's addMembership (#2880)Andrew Reynolds
2019-03-21Rewrite selectors correctly applied to constructors (#2875)Andrew Reynolds
2019-03-21Add more NEWS (#2859)Andres Noetzli
2019-03-19Sygus abduction feature (#2744)Andrew Reynolds
2019-03-19Make declare-datatype(s) a standard, non-extended command in the Smt2 ↵Andrew Reynolds
parser. (#2874)
2019-03-19Fix fairness issue with fast sygus enumerator (#2873)Andrew Reynolds
2019-03-18New C++: Remove redundant mkBoundVar function.Aina Niemetz
2019-03-18New C++: Remove redundant mkVar function.Aina Niemetz
s
2019-03-18BitVector: Allow base 10 in constructor. (#2870)Aina Niemetz
2019-03-16Limit --solve-int-as-bv=X to QF_NIA/QF_LIA/QF_IDL (#2868)Andres Noetzli
Fixes #1715. We do not support the `--solve-int-as-bv=X` preprocessing pass with logics other than pure QF_NIA/QF_LIA/QF_IDL. This commit adds a corresponding check and throws an option exception if an incompatible logic has been set.
2019-03-16Enable CryptoMiniSat-backed BV proofs (#2847)Alex Ozdemir
* Connect the plumbing so that BV proofs are enabled when using CryptoMiniSat * Also fixed a bug in CNF-proof generation * Specifically, CNF proofs broke when proving tautological clauses. Now they don't.
2019-03-15New beta-reduction for HOL solving (#2869)Haniel Barbosa
2019-03-15Adding capture avoiding substitution (#2867)Haniel Barbosa
2019-03-14Fix non-variable function head elimination in UF. (#2864)Andrew Reynolds
2019-03-14Fix function term set for theory strings compute care graph. (#2862)Andrew Reynolds
2019-03-14Improve INSTALL instructions. (#2866)Aina Niemetz
2019-03-14Use zero slope tangent planes for transcendental functions (#2803)Andrew Reynolds
2019-03-14Properly handle lambdas in relevant domain (#2853)Andrew Reynolds
2019-03-14 Add getFreeVariables method to node algorithm (#2852)Andrew Reynolds
2019-03-14Disable DCO signing for organization members.Mathias Preiner
2019-03-14Implement proper semantics for TPTP predicate is_rat. (#2861)Andrew Reynolds
2019-03-14 Fix substitution step in ho matching (#2825)Andrew Reynolds
2019-03-14Generalize sygus-rr-verify for fast enumerator (#2829)Andrew Reynolds
2019-03-14check for null assumption in query and replace with false (#2858)makaimann
The default assumption argument in query was a null `Expr`, but the implementation asserted that the assumption is not null: declaration: https://github.com/CVC4/CVC4/blob/68174dedcb4bf9d91241585ab1cc876d2fa83d62/src/smt/smt_engine.h#L593 implementation: https://github.com/CVC4/CVC4/blob/68174dedcb4bf9d91241585ab1cc876d2fa83d62/src/smt/smt_engine.cpp#L3548 The change is to simply check if the assumption is null and replaces it with the `false` expression if it is. It should be `false` not `true` because it is negated in checkSatisfiability (when it's a query) as seen here: https://github.com/CVC4/CVC4/blob/68174dedcb4bf9d91241585ab1cc876d2fa83d62/src/smt/smt_engine.cpp#L3607 Note: I couldn't find a clean way to make `false` the default argument of assumption, because the expression manager is non-static.
2019-03-13Add statistics for proof gen./checking time, size (#2850)Andres Noetzli
This commit adds a statistic that records the total size of all proofs generated by an instance of `SmtEngine`. The commit also moves `SmtEngine::checkProof()` into `smt_engine.cpp` because it needs to know the complete type of `d_stats` (and the separate file for that method didn't seem that useful). Additionally, it changes `smt::SmtEngine::checkProofTime` to `smt::SmtEngine::lfscCheckProofTime` that only measures the time spent in LFSC and adds a statistic `proof::ProofManager::proofProductionTime` that measures the proof production time separately (also works with `get-proof`/`--dump-proof`).
2019-03-13Remove spurious data member. (#2857)Andrew Reynolds
2019-03-12Fix public headers for make install. (#2856)Mathias Preiner
This commit fixes make install, which previously copied all public header files to ${CMAKE_INSTALL_PREFIX}/ instead of ${CMAKE_INSTALL_PREFIX}/cvc4. Further, the old build system modified all #include directives in the installed public header files to use the installed headers, e.g., #include "cvc4_public.h" was changed to #include <cvc4/cvc4_public.h>. Now, after make install the script src/fix-install-headers.sh is executed to change the #include directives accordingly (this should be obsolete with the new C++ API).
2019-03-12Add option --sygus-rr-synth-rec for considering all grammar types ↵Andrew Reynolds
recursively (#2270)
2019-03-12 Move tuple/record update elimination from ppRewrite to expandDefinition (#2839)Andrew Reynolds
2019-02-28ErProof class with LFSC output (#2812)Alex Ozdemir
* ErProof class with LFSC output * Created a TraceCheckProof class * parsable from text * Created an ErProof class * constructible from a TraceCheckProof * writable as LFSC * A bunch of unit tests * Reponded to Mathias's first set of comments. Credits to Mathias for many of the fixes! * Responed to Andres's first set, fixed tests I accidentally deleted a "!" last time, causing stuff to fail. * Use Configuration::isAssertionBuild * Clarified comment * Responded to Andres's 2nd review * Gaurding against a memory error. * Renaming a file. * Aggressively unlinking temporary files.
2019-02-27Use string stream for proofs instead of tmp files (#2841)Andres Noetzli
This commit changes CVC4 to use a string stream instead of a temporary files for proof checking. Note: This change requires a version of LFSC that supports checking streams (see https://github.com/CVC4/LFSC/pull/14). Tested: `make check` passed, changing `holds` to `xholds` in the proof produced by proof_manager.cpp makes the proofs fail.
2019-02-26ClangFormat: Disable DerivePointerAlignment (#2842)Andres Noetzli
The option `DerivePointerAlignment` tries to automatically determine the pointer alignment used by the input. In our case, we would eventually like the code base to be consistent throughtout, so this commit disables that option.
2019-02-13New C++ API: Remove redundant declareFun function. (#2837)Aina Niemetz
2019-02-13Rewrite simple regexp pattern to str.contains (#2827)Andres Noetzli
2019-02-12New C++ API: Remove redundant mkTerm function. (#2836)Aina Niemetz
2019-02-12Delete temporary proof files when aborting CVC4 (#2834)Andres Noetzli
CVC4 was not deleting temporary proof files when crashing or being terminated externally. This commit uses an early `unlink()` to remove the files as soon as CVC4 terminates.
2019-02-11New C++ API: Unit tests for declare* functions. (#2831)Aina Niemetz
2019-02-05Make stripConstantEndpoints() less aggressive (#2830)Andres Noetzli
2019-02-03Add rewrite for contains + const strings replace (#2828)Andres Noetzli
2019-02-02Fix corner case in stripConstantEndpoints (#2824)Andres Noetzli
`stripConstantEndpoints()` was returning `true` when the first argument was a list only containing an empty string, which could lead to rewrite loops. This commit checks for that case and adds a unit test for it.
2019-01-29Fix warning due to catching polymorphic exceptions (#2821)Andres Noetzli
2019-01-29New C++ API: Fix checks for mkTerm. (#2820)Aina Niemetz
This required fixing the OpTerm handling for mkTerm functions in the API.
2019-01-29Strings: Remove redundant replace rewrite (#2822)Andres Noetzli
Pulling the first constant string from a replace if there is no overlap with the search term is subsumed by the rewrite using `stripConstantEndpoints()`.
2019-01-24Extended DRAT signature to operational DRAT (#2815)Alex Ozdemir
* Extended DRAT signature to operational DRAT The DRAT signature now supports both operational and specified DRAT. That is, either kind of proof will be accepted. The goal of this implementation of operational DRAT was to re-use as much of the specified DRAT machinery as possible. However, by writing a separate operational signature, we could make it much more efficient (after all, operational DRAT came about because of a push for efficient cheking). You can run the new AND old DRAT tests by running ``` lfscc sat.plf smt.plf lrat.plf drat.plf drat_test.plf ``` * Apply suggestions from code review (Yoni) Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
2019-01-23Avoid using ProofManager in non-proof CMS build (#2814)Andres Noetzli
PR #2786 changed `CryptoMinisatSolver::addClause()` to register clauses with the bit-vector proof if proofs are turned on. The new code requested the `ProofManager` even when proofs were turned off, which made the `eager-inc-cryptominisat.smt2` regression and our nightlies fail. This commit guards the access to the `ProofManager`, restoring the semantics of the original code when proofs are turned off.
2019-01-22Strings: Strengthen multiset reasoning (#2817)Andres Noetzli
This commit introduces three helper methods for performing multiset reasoning: an entailment check whether a term is always a strict subset of another term in the multiset domain (`checkEntailMultisetSubset()`), a check whether a string term is always homogeneous (`checkEntailHomogeneousString()`), and an overapproximation for the multiset domain (`getMultisetApproximation()`). It also adds unit tests related to multiset reasoning.
2019-01-22 Fix tuple and record CVC printing (#2818)Andrew Reynolds
2019-01-22 Fix parsing of overloaded parametric datatype selectors (#2819)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback