summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2017-12-06Fixed time stats for MiniSat solve time. (#1431)Aina Niemetz
Also, moved implementation of BVMinisatSatSolver::MinisatNotify::notify to .cpp file.
2017-12-06Remove CDChunkList (#1414)Andres Noetzli
2017-12-05Fix output of --show-trace-tags. (#1430)Mathias Preiner
Now prints each tag in a separate line.
2017-12-04Adding SyGuS grammars for rationals. (#1426)Haniel Barbosa
2017-12-04Eliminate expand definitions from Sygus (#1425)Andrew Reynolds
2017-12-04Fix strings rewriter for strip constant endpoint reverse direction (#1424)Andrew Reynolds
2017-12-04Fix side condition for BITVECTOR_MULT. (#1422)Mathias Preiner
2017-12-03Normalize grammars - 2 (#1420)Haniel Barbosa
This is another step towards addressing #1304 and #1344. This pull request: - Refactors SygusGrammarNorm - Makes SyGusGrammarNorm a default component in the construction of grammar. The linearization of grammars however only occurs if the option --sygus-grammar-norm is used. - Performs a "chain transformation" in the application of the PLUS operator in integer grammars - Removes redundant expansions of definitions from TermDbSygus - Adds a default empty print callback to SygusEmptyPrintCallback This lays the basis for more general linearizations.
2017-12-02Minor improvements to inst match generator (#1415)Andrew Reynolds
2017-12-01Improve rewriter for string replace (#1416)Andrew Reynolds
2017-12-01Fix reset-assertions (#1413)Andres Noetzli
This commit fixes two issues with reset-assertions: - pending pops were not done in SmtEngine, resulting in the following assertion failure: d_userLevels.size() == 0 && d_userContext->getLevel() == 1 - all definitions were erased on reset-assertion in an SMT2 file, leading to errors about undefined types
2017-12-01Minor additions for sygus (#1419)Andrew Reynolds
2017-12-01Refactor and generalize PBE strategies (#1410)Andrew Reynolds
2017-12-01Fix build when Valgrind instrumentation enabledAndres Noetzli
My last commit for the Valgrind instrumentation contained a typo that made the nightlies fail. This commit fixes the issue.
2017-11-30Add debugging tools for ContextMemoryManager (#1407)Andres Noetzli
This commit adds two configuration options that help debugging memory issues with allocations in the ContextMemoryManager: --enable/disable-valgrind: This flag enables/disables Valgrind instrumentation of the ContextMemoryManager. Enabled by default for debug builds if the Valgrind headers are available. --enable/disable-context-memory-manager: This flag enables/disables the use of the ContextMemoryManager. If the flag is disableda dummy ContextMemoryManager is used that does single allocations instead of chunks. The flag is enabled by default.
2017-11-30Add Gaussian Elimination as a preprocessing pass for BV. (#1342)Aina Niemetz
This adds Gaussian Elimination as a preprocessing pass for BV. Gaussian Elimination is only applied if the given bit-width guarantees that no overflows can occur.
2017-11-30Fixes for issue 1404 (#1409)Andrew Reynolds
2017-11-30Remove remaining references to QuantArith (#1408)Andrew Reynolds
2017-11-29Minor improvements and changes to defaults for cbqi bv (#1406)Andrew Reynolds
This makes it so that --cbqi-bv tries at most 2 instantiations per quantified formula (one based on inversions when applicable, one based on model values). This makes it so that we do not have exponential run time in the worst case. This helps significantly for psyco benchmarks which have many quantified variables. Enables --cbqi-bv by default and changes the default inequality mode to eq-boundary (which is the best performer overall), also enables extract removal by default Allows cbqiNestedQE to be used in the BV logic. Adds an option --cbqi-full which indicates whether we should try model value instantiations for bit-vectors (by default, this is done only for the pure BV logic).
2017-11-29Improve caching in term formula removal (#1398)Andrew Reynolds
2017-11-29Adding missing break statements. CID 1362756. (#1394)Tim King
2017-11-29Simplifying the conditions in checkLetBinding to avoid using iterator… (#1372)Tim King
2017-11-28Improve the rewriter for SINE. (#1221)Andrew Reynolds
2017-11-28Improve rewrite for string substr (#1337)Andrew Reynolds
2017-11-28Improve trigger filter instances (#1402)Andrew Reynolds
2017-11-28Removing throw specifiers from internal Printer hierarchy. (#1393)Tim King
2017-11-27Fix models for --solve-real-as-int. (#1371)Andrew Reynolds
2017-11-25Fixes for higher-order (#1405)Andrew Reynolds
2017-11-24(Refactor) Instantiate utility (#1387)Andrew Reynolds
2017-11-24Implement tangent and secant planes for transcendental functions (#1401)Andrew Reynolds
2017-11-23Ho parsing and regressions (#1350)Andrew Reynolds
2017-11-22Converting defined functions and let expressions from Sygus grammars to ↵Haniel Barbosa
lambdas (#1403) This partially solves issue #1344. Definitions are expanded when the grammar normalizer is called. When this becomes default then the code that expands definitions elsewhere will be removed. The PR also contains minor changes to the PrintCallback and SygusGrammarNormalize module.
2017-11-22Sygus Lambda Grammars (#1390)Andrew Reynolds
2017-11-22Transcendental tangent planes utilities (#1288)Andrew Reynolds
2017-11-21Adding infrastructure for normalizing SyGuS grammars (#1397)Haniel Barbosa
* minor Using string previously computed * adding option * starting module for simplifying grammars * more * more * fix * fix * fix * fix * fix * removing unused command * removing unused command * removing unnecessary quantifier engine * adding lambda support * transient * reverting changes * starting normalization of integers * removing unnecessary objects * using for_each * rebuilding given datatypes * recrating types as given * bug fixing * minor * reverting space changes * addressing review * addressing review
2017-11-21Cegqi bv remove extract terms preprocess pass (#1376)Andrew Reynolds
* Preprocess extract -> concat pass for cegqi bv. * Add sygus bench * Fixes, infrastructure. * Minor fixes. * Try * Minor * Minor * Document * Format * Improving debug messages. * Address * Format * Overlapping extracts. * Format * Minor * Address review. * Format * Comment * Format
2017-11-20Initializes members of QuantInfo. Resolves CID 1362929. (#1391)Tim King
2017-11-19Removing an unused variable from SygusInput. Resolves CID 1362932. (#1392)Tim King
2017-11-18Ho instantiation (#1204)Andrew Reynolds
* Higher-order instantiation. * Add missing files. * Document inst match generators, make collectHoVarApplyTerms iterative. * More documentation. * More documentation. * More documentation. * More documentation * Refactoring, documentation. * More documentation. * Fix comment, reference issue. * More documentation. Fix ho trigger for the changes from master. * Minor * More documentation. * More documentation. * More * More documentation, make indexing and lookup in TriggerTrie iterative instead of recursive. * More * Minor improvements to comments. * Remove an unimplemented optimization from an old version of cached multi-trigger matching. Update and improve documentation in inst match generator. * Improve documentation for ho_trigger. * Update ho trigger to not access now private member of TermDb. * Address comments. * Address * Clang format
2017-11-18Names the Effort enum of QuantConflictFind class. (#1354)Tim King
* Changes the Effort level of QuantConflictFind to an enum class. Adding a third value to the enum to indicate not being set. Minor refactoring related to this change. Resolves CID 1172043. * Fixing a missed assertion. Fixing a few compiler warnings. * Switching back to an enum from an enum class.
2017-11-17(Refactor) Document and clean single invocation partition. (#1364)Andrew Reynolds
* Documenting single invocation partiion. * More * More encapsulation. * More, documentation complete. * Split to own file. * Format * Fully encapsulate. * Format * Improvements to doc. * Format * Address * Format * Missed comment * Newline * Address * Format
2017-11-17Add random number generator. (#1370)Aina Niemetz
This adds a deterministic (seeded) random number generator (RNG). It implements the xorshift* generator (see S. Vigna, An experimental exploration of Marsaglia's xorshift generators, scrambled. ACM Trans. Math. Softw. 42(4): 30:1-30:23, 2016).
2017-11-16(Refactor) Arithmetic monomial sum (#1381)Andrew Reynolds
* Add arithmetic monomial sum utility. * Clang format * Fix * Address review. * Fix missed comment. * Format * Fix
2017-11-15Initializes BitVectorProof::d_isAssumptionConflict. Resolves CID 1362898. ↵Tim King
(#1374)
2017-11-15Sygus print callbacks (#1348)Andrew Reynolds
* Initial infrastructure for sygus printing. * Minor * Minor improvements * Format * Minor * Empty constructor printer. * Format * Minor * Format * Address.
2017-11-15Removes an unused variable from Theory. (#1375)Tim King
2017-11-15Initializing members of Datatype. Addresses CIDs 1362897, 1362912, 1362923 ↵Tim King
and 1362931. (#1373)
2017-11-15Adding garbage collection for Proof objects. (#1294)Tim King
2017-11-14Make QEffort an enum (#1366)Andrew Reynolds
* Make QEffort an enum. * Format * Minor * Fix
2017-11-14(Refactor) Split sygus term db (#1335)Andrew Reynolds
* Split explain utility, invariance tests. * Split extended rewriter. * Remove unused function. * Minor * Move generic term utilities to term_util. * Documentation, minor. * Make arguments private in eval invariance. * Document * More documentation. * Clang format. * Fix, improve. * Format * Address review. * Address missed comment. * Add line breaks * Format
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback