summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2021-04-21moreAndres Noetzli
2021-04-16works mostlyAndres Noetzli
2020-11-22missing fileAndres Noetzli
2020-11-22missing fileAndres Noetzli
2020-11-22rulesAndres Noetzli
2020-07-06rulesAndres Noetzli
2020-05-30CurrentAndres Noetzli
2020-05-01UpdateAndres Noetzli
2020-04-27rulesAndres Noetzli
2020-04-23Basic support for commutative opsAndres Noetzli
2020-04-15eliminate GetIndex/GetChildAndres Noetzli
2020-04-13LHS eval + optimizationAndres Noetzli
2020-04-12let support and constant eval for rhsAndres Noetzli
2020-04-10Some stuffAndres Noetzli
2020-03-19Simple proof workingAndres Noetzli
2020-03-17ProgressAndres Noetzli
2020-03-16Basic rules compilingAndres Noetzli
2020-03-15Handle cases in --sygus-rr where evaluation is not constant (#4100)Andrew Reynolds
Throws warning instead of error if two terms with the same rewritten form evaluate differently, but the evaluation is non-constant. Fixes #4096 and fixes #4089.
2020-03-13Removing a few deprecated options (#4052)Andrew Reynolds
2020-03-13Generalize type rules for strings to sequences (#3987)Andrew Reynolds
Towards theory of sequences.
2020-03-13Fix case of non-constant value for sygus sampling (#4051)Andrew Reynolds
Fixes #4050.
2020-03-12Convert most instances of dataypes in parsers to the new API (#4054)Andrew Reynolds
I am still accessing Expr-level Datatypes for the sygus v1/v2 parsers (within smt2). This will be addressed in two ways in the future: (1) The sygus v1 parser will be deleted, (2) The sygus v2 parser will be updated to use a "Grammar" object as an extension of the new API, which will hide all calls to the underlying datatype. (See https://github.com/abdoo8080/CVC4/tree/sygus-api). FYI @abdoo8080 . Note I've renamed "mkMutualDatatypeTypes" to "bindMutualDatatypeTypes" to be more accurate and follow the updated name conventions in the parser. The next step will be to handle parametric datatypes, which are not specifically addressed by this PR.
2020-03-12Do not allow quantifiers over real variables in real to int pass. (#4049)Andrew Reynolds
With quantifiers over real variables, --solve-real-as-int is neither sound nor complete. Thus we should abort in this case.
2020-03-12Remove local theory extension option (#4048)Andrew Reynolds
This option was unimplemented and was equivalent to setting the instantiation level of all quantified formulas to 0.
2020-03-12Do not make models for quantified function variables (#4039)Andrew Reynolds
If we combine finite model finding and higher-order, then we could try to find a model find operators whose kind was BOUND_VARIABLE.
2020-03-12New C++ API: Remove support for (reset). (#4037)Aina Niemetz
Supporting SMT-LIB's (reset) command on the API level is dangerous and not required -- it's sufficient to just destroy the solver object and create a new one if necessary. It's dangerous because invalidated objects can be passed in after a reset, and we would need to find a clean way to guard against this. We want to guard against this in the future, but for now it is cleaner to make it explicit (by not having this functionality in the API but forcing the user to destroy and recreate the solver object) that these objects can't be reused.
2020-03-12Ensure legal candidate equalities when using relational triggers (#4035)Andrew Reynolds
2020-03-11Fix double notify in equality engine (#4036)Andrew Reynolds
Fixes #3955. Previously we were getting two calls to notifyNewEqClass from the equality engine for new application nodes, since the notification was being done in an internal call to newNode(...). The proper place to call this is in addTermInternal(...) which is called only once per Node per SAT context. This bug potentially impacted some performance (due to redundant calls), and also broke the contract that notifyNewEqClass should only be called once per node per SAT context. In most cases, this was being handled in a benign way by theory solvers, although an assertion was failing in EqualityQuery, which is fixed by this PR. A block of code changed indentation in this commit.
2020-03-11Hide options for and related to the BV abstraction module. (#4041)Aina Niemetz
All things related to the current BV solver are obsolete in the sense that we are working on a new BV solver implementation. The BV abstraction module has several issues and is quite hacky, it should only be enabled in experimental settings. We don't want to remove it yet though, we want to keep it around for future evaluation purposes. This commit categorizes the option to enable the module and a second option related to the module as 'undocumented'.
2020-03-11Simplifications to the Datatypes API (#4040)Andrew Reynolds
Removes DatatypeSelectorDecl and DatatypeDeclSelfSort. Add selectors is now inlined. A special case is added for the "self selector", instead of using a class as a dummy argument. I updated the Python files, although would be helpful to double check this is correct. Co-authored-by: makaimann <makaim@stanford.edu>
2020-03-11Add automatic Cython binding installation (#3933)makaimann
* Remove getIndices for Kinds * Test importing pycvc4 * Distutils install for pycvc4 * Use full path for cvc4kinds prefix * Remove zip_safe option (not needed for distutils) * Automatically clean up setup.py intermediate files * Rely on make install to install pycvc4 * Run make install when testing python bindings * Fix: Check importing pycvc4 when python bindings are built * Remove one -Wshadow warning for cython-generated files * Put the fake kinds submodule in generated __init__.py * Remove unnecessary file permission options in python CMakeLists * Respect install prefix unless in a virtualenv * Handle python2 print function * Use VIRTUAL_ENV environment variable to check if in python virtualenv * Add header and documentation to setup.py.in * Capitalize CVC4 in PyCVC4Install * Update src/api/python/CMakeLists.txt Co-Authored-By: Mathias Preiner <mathias.preiner@gmail.com> * Simplify CMakeLists for setup.py configuration * Shorten virtualenv check with Mathias's suggestion * Set TRAVIS_CVC4_PYTHON_BINDINGS to no in other builds * minor: bash syntax fix * Move pycvc4 import check to makeInstallCheck * Include installed pycvc4 location on PYTHONPATH * Better way to set PYTHONPATH Co-authored-by: Mathias Preiner <mathias.preiner@gmail.com> Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
2020-03-11Do not enable some SMT-COMP specific options by default (#4038)Andrew Reynolds
Moves SMT-COMP-specific options to the SMT-COMP script. Both of these options have led to issues (segfaults or infinite loops). Issue #789 can be downgraded to "minor" after this PR. Btw, I did not add these specialized options to the "incremental" script of SMT-COMP, since I'm assuming they should not be used there.
2020-03-11Guard against null relevancy condition in SyGuS (#4033)Andrew Reynolds
Fixes #4025. Also makes our sygus default grammar for strings (slightly) better by including a dummy character, which is required for solving the regression added by this PR. A more robust (but unintuitive to the user) solution would be to include str.from_code( Start_Int ).
2020-03-11Add missing datatype functions to new API (#3930)Andrew Reynolds
This is in preparation for migrating the parser to use the Term-level API for datatypes. Notably, this adds the function mkDatatypeSorts for making mutually recursive datatypes. I've added a unit test that demonstrates this method (which mirrors the Expr-level datatype API).
2020-03-11Switch to Nodes for conjecture generator (#4026)Andrew Reynolds
Fixes #4022.
2020-03-11reset-assertions: Update TheoryEngine's PropEngine* (#4032)Andres Noetzli
Fixes #4028. TheoryEngine's pointer was not updated to the new PropEngine when resetting assertions. This commit fixes that. As far as I can tell, this was the only class storing a PropEngine* that isn't owned by PropEngine, so we should hopefully not have other similar issues.
2020-03-11Remove experimental symmetry breaker (#4005)Andrew Reynolds
This never impacted performance positively. Fixes #3997 and fixes #4015. There was a folder that the symmetry breaker was used on regress1/sym. These are simple examples that show when it is possible to find symmetries in SMT; the symmetry breaker is not critical for solving these. For now I'm leaving them as regressions documenting possible benchmarks to target if we revisit this technique.
2020-03-11Fix non-parametrized operators in subgoal generation (#4023)Andrew Reynolds
Fixes #4021. We were previously constructing a malformed HO_APPLY as part of a subgoal for induction.
2020-03-11Remove partial instantiation for local theory extensions (#4020)Andrew Reynolds
Fixes #4019. This feature was never fully implemented.
2020-03-11Fix (#4017)Andrew Reynolds
Fixes #4001. This assertion was more of a conjecture (stating that easy cases of miniscoping are already handled). However some option combinations can break this invariant, regardless the code should do the correct thing.
2020-03-11Fix duplicate variable issue in sygus-qe-preproc (#4013)Andrew Reynolds
2020-03-11Introduce tables in the rewriter (#3742)Andres Noetzli
This commit adds tables in the rewriter that store which function should be used to rewrite which kind. We have separate tables for `EQUAL` because every theory has its own equality rewriter.
2020-03-10Set assertion in `CnfStream::ensureLiteral()` (#3927)Andres Noetzli
Fixes #3814. `CnfProof` has a stack of assertions that are being converted to clauses. `CnfStream::ensureLiteral()` can result in clauses being added to the SAT solver. When adding a clause, we require an assertion that can be associated with the clause (https://github.com/CVC4/CVC4/blob/ba6ade0fc3f4cd339885652bb9bf5c87113c498d/src/prop/minisat/core/Solver.cc#L471-L476). However, in the issue that was reported, the stack was empty, resulting in an assertion failure. This commit fixes the issue by setting the current assertion to be the null node when a literal is being ensured (and changing the proof code to update the assertion associated with a literal if it is currently null). This should be ok since the clauses are not inputs or lemmas (if they are, the assertion associated with the clause will be updated).
2020-03-10bv-gauss-elim: Fix handling of inconsistent case. (#4027)Aina Niemetz
This fixes the case when all rows are inconsistent. Fixes #3999.
2020-03-10Fix real to int for parameterized kinds (#4016)Andrew Reynolds
2020-03-10Fix sort inference for top-level Boolean variables (#4012)Andrew Reynolds
Fixes #4010.
2020-03-10Fix issue with reset-assertions. (#3988)Aina Niemetz
Calling (reset-assertions) in start mode was not handled correctly. Additionally, when calling (check-sat) after (reset-assertions) after a (check-sat) call that answered unsat, we answered unsat instead of sat. This cleans up and fixes reset-assertions) handling.
2020-03-10Logic exception instead of assertion failure for instantiate (#4006)Andrew Reynolds
Fixes #4003. Protects against a (class of) nonsensical option combinations.
2020-03-10Remove assertion in resolution bound inferences (#3980)Andrew Reynolds
* Fix assertion in resolution bound inferences * Format * Minor Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
2020-03-10Consolidate options that disable produceModels (#3973)Andrew Reynolds
Also adds --sort-inference to this list, fixes #3936.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback